LBoundJ

import Mathlib

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- `ℓ(j)`, Eq. (11.40). -/
noncomputable def LBoundJ {H L : Type*} [Fintype H] [Fintype L] [Nonempty H] [Nonempty L]
    (U : H → (K → ℤ) → WithBot ℝ) (C : L → (K → ℤ) → WithTop ℝ) (x : H → (K → ℤ))
    (y : L → (K → ℤ)) (j : K) : ℝ :=
  max
    ((Finset.univ : Finset H).sup' Finset.univ_nonempty
      (fun h => (U h (fun k => x h k + (if k = j then (1:ℤ) else 0))).unbotD 0 - (U h (x h)).unbotD 0))
    ((Finset.univ : Finset L).sup' Finset.univ_nonempty
      (fun l => (C l (y l) - C l (fun k => y l k - (if k = j then (1:ℤ) else 0))).untopD 0))

end DiscreteConvex.EconomicEquilibriumB