Berge's maximum theorem for extended-real objectives

LeanEconomics.Topology.Berge proves the maximum theorem for a real-valued objective. Here the objective may take the value -∞, which is what a reward like log c does at zero consumption.

Allowing -∞ is what lets a dynamic program be posed without a floor on the reward. Every model in this library that uses a floor does so to keep the reward real-valued and bounded, and then has to prove separately that the floor never binds. With an extended-real objective the floor is unnecessary from the start.

What changes, and what does not

Less than one might expect, and two of the changes make the proof simpler: EReal is a complete lattice, so le_sSup and sSup_le carry no boundedness or nonemptiness side conditions, unlike their conditionally-complete counterparts.

Upper semicontinuity here goes through attainment rather than interpolation: the supremum over a nonempty compact set is achieved, so a strict bound at every point of the set is a strict bound on the supremum. (DenselyOrdered EReal does exist in Mathlib, as instDenselyOrderedEReal, so the interpolating proof would work too; the argmax half below uses it.)

Main results

• LeanEconomics.continuous_maxValueE : the maximum theorem for EReal-valued objectives.

noncomputable def LeanEconomics.maxValueE {X : Type u_1} {Y : Type u_2} (f : X → Y → EReal) (Γ : X → Set Y) (x : X) : EReal

The value of a maximisation problem whose objective may be -∞. No boundedness hypothesis is needed: EReal is a complete lattice.

Equations

• LeanEconomics.maxValueE f Γ x = sSup (f x '' Γ x)

theorem LeanEconomics.le_maxValueE {X : Type u_1} {Y : Type u_2} {f : X → Y → EReal} {Γ : X → Set Y} {x : X} {y : Y} (hy : y ∈ Γ x) : f x y ≤ maxValueE f Γ x

theorem LeanEconomics.maxValueE_le {X : Type u_1} {Y : Type u_2} {f : X → Y → EReal} {Γ : X → Set Y} {x : X} {c : EReal} (h : ∀ y ∈ Γ x, f x y ≤ c) : maxValueE f Γ x ≤ c

theorem LeanEconomics.continuous_fiberE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → EReal} (hf : Continuous ↿f) (x : X) : Continuous (f x)

theorem LeanEconomics.eventually_forall_ltE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → EReal} {Γ : X → Set Y} {x : X} {c : EReal} (hf : Continuous ↿f) (hΓc : IsCompact (Γ x)) (huhc : UpperHemicontinuousAt Γ x) (hc : ∀ y ∈ Γ x, f x y < c) : ∀ᶠ (x' : X) in nhds x, ∀ y ∈ Γ x', f x' y < c

The engine, exactly as in the real case: a strict upper bound over the constraint set survives into a neighbourhood of the parameter.

theorem LeanEconomics.upperSemicontinuousAt_maxValueE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → EReal} {Γ : X → Set Y} {x : X} (hf : Continuous ↿f) (hΓne : ∀ (x : X), (Γ x).Nonempty) (hΓc : ∀ (x : X), IsCompact (Γ x)) (huhc : UpperHemicontinuousAt Γ x) : UpperSemicontinuousAt (maxValueE f Γ) x

Upper hemicontinuity of the constraint set gives upper semicontinuity of the value. This goes through attainment of the supremum rather than interpolating a midpoint.

theorem LeanEconomics.lowerSemicontinuousAt_maxValueE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → EReal} {Γ : X → Set Y} {x : X} (hf : Continuous ↿f) (hlhc : LowerHemicontinuousAt Γ x) : LowerSemicontinuousAt (maxValueE f Γ) x

Lower hemicontinuity of the constraint set gives lower semicontinuity of the value.

theorem LeanEconomics.continuousAt_maxValueE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → EReal} {Γ : X → Set Y} {x : X} (hf : Continuous ↿f) (hΓne : ∀ (x : X), (Γ x).Nonempty) (hΓc : ∀ (x : X), IsCompact (Γ x)) (huhc : UpperHemicontinuousAt Γ x) (hlhc : LowerHemicontinuousAt Γ x) : ContinuousAt (maxValueE f Γ) x

Berge's maximum theorem for an extended-real objective.

theorem LeanEconomics.continuous_maxValueE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → EReal} {Γ : X → Set Y} (hf : Continuous ↿f) (hΓne : ∀ (x : X), (Γ x).Nonempty) (hΓc : ∀ (x : X), IsCompact (Γ x)) (huhc : UpperHemicontinuous Γ) (hlhc : LowerHemicontinuous Γ) : Continuous (maxValueE f Γ)

theorem LeanEconomics.maxValueE_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → EReal} {Γ : X → Set Y} {x : X} (hf : Continuous ↿f) (hΓne : (Γ x).Nonempty) (hΓc : IsCompact (Γ x)) : ∃ y ∈ Γ x, maxValueE f Γ x = f x y

At a maximiser the objective equals the value, exactly as in the real case.

theorem LeanEconomics.maxValueE_eq_of_mem_argmax {X : Type u_1} {Y : Type u_2} {f : X → Y → EReal} {Γ : X → Set Y} {x : X} {y : Y} (hy : y ∈ argmax f Γ x) : maxValueE f Γ x = f x y

At a maximiser the objective equals the value. In EReal this needs no side conditions, the order being complete.

theorem LeanEconomics.argmaxE_nonempty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → EReal} {Γ : X → Set Y} {x : X} (hf : Continuous ↿f) (hΓne : (Γ x).Nonempty) (hΓc : IsCompact (Γ x)) : (argmax f Γ x).Nonempty

A maximiser exists.

theorem LeanEconomics.upperHemicontinuousAt_argmaxE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → EReal} {Γ : X → Set Y} {x : X} (hf : Continuous ↿f) (hΓc : ∀ (x : X), IsCompact (Γ x)) (huhc : UpperHemicontinuousAt Γ x) (hlhc : LowerHemicontinuousAt Γ x) : UpperHemicontinuousAt (argmax f Γ) x

Berge's maximum theorem, the maximiser half, for an extended-real objective. The proof is the real one unchanged: away from an open set containing the maximisers the objective is strictly below the value, that gap survives into a neighbourhood by the engine, and lower semicontinuity of the value keeps the value above the gap.

theorem LeanEconomics.upperHemicontinuous_argmaxE {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → EReal} {Γ : X → Set Y} (hf : Continuous ↿f) (hΓc : ∀ (x : X), IsCompact (Γ x)) (huhc : UpperHemicontinuous Γ) (hlhc : LowerHemicontinuous Γ) : UpperHemicontinuous (argmax f Γ)