UBoundJ

import Mathlib

namespace DiscreteConvex.EconomicEquilibriumB

open Classical
open scoped Pointwise
variable {K : Type*} [Fintype K] [DecidableEq K]
/-- `u(j)`, Eq. (11.41). -/
noncomputable def UBoundJ {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) : ℝ :=
  min
    ((Finset.univ : Finset H).inf' Finset.univ_nonempty
      (fun h => (U h (x h)).unbotD 0 - (U h (fun k => x h k - (if k = j then (1:ℤ) else 0))).unbotD 0))
    ((Finset.univ : Finset L).inf' Finset.univ_nonempty
      (fun l => (C l (fun k => y l k + (if k = j then (1:ℤ) else 0)) - C l (y l)).untopD 0))

end DiscreteConvex.EconomicEquilibriumB