Berge's maximum theorem

Consider maximising a continuous objective f x y over a constraint set Γ x that moves with the parameter x. Berge's maximum theorem says that if Γ is continuous -- upper and lower hemicontinuous -- with nonempty compact values, then the value of the problem varies continuously with x, and the set of maximisers varies upper hemicontinuously.

The two halves need the two halves of the continuity of Γ, and it is worth keeping track of which: upper hemicontinuity gives upper semicontinuity of the value, lower hemicontinuity gives lower semicontinuity of it. Neither alone suffices.

Mathlib supplies the hemicontinuity definitions (UpperHemicontinuousAt, LowerHemicontinuousAt) but not this theorem.

Main definitions

• LeanEconomics.maxValue f Γ x : the value sSup (f x '' Γ x) of the problem at x.
• LeanEconomics.argmax f Γ x : the set of maximisers at x.

Main results

• LeanEconomics.continuousAt_maxValue : the maximum theorem -- the value function is continuous.
• LeanEconomics.upperHemicontinuousAt_argmax : the maximiser correspondence is upper hemicontinuous.
• LeanEconomics.argmax_nonempty, LeanEconomics.isCompact_argmax : it has nonempty compact values.

A check on the hypotheses

Berge's hypotheses are strong enough to be worth checking they can all hold at once: continuous_maxValue_const instantiates them at a constraint set that does not move with the parameter. Without such a witness the theorems above could be vacuous.

Implementation notes

eventually_forall_lt is the engine. It says that a strict bound on f over Γ x persists into a neighbourhood of x, and it is proved from the generalized tube lemma together with upper hemicontinuity. Upper semicontinuity of the value follows at once, and so does the hard half of upper hemicontinuity of argmax, applied there to the correspondence x ↦ Γ x ∩ Vᶜ. Stating it without reference to a supremum is what lets it serve the second purpose, where that correspondence may take empty values.

References

• Berge, Espaces topologiques: Fonctions multivoques, 1959.
• Stokey, Lucas and Prescott, Recursive Methods in Economic Dynamics.

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

The value of the problem max f x y subject to y ∈ Γ x.

Equations

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

def LeanEconomics.argmax {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Preorder Z] (f : X → Y → Z) (Γ : X → Set Y) (x : X) : Set Y

The set of maximisers of f x over Γ x. The codomain is any preorder, so that the same definition serves the extended-real objectives of LeanEconomics.Topology.BergeEReal.

Equations

• LeanEconomics.argmax f Γ x = {y : Y | y ∈ Γ x ∧ IsMaxOn (f x) (Γ x) y}

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

The objective as a function of the choice alone, with the parameter fixed.

theorem LeanEconomics.bddAbove_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → ℝ} {Γ : X → Set Y} {x : X} (hf : Continuous ↿f) (hΓc : IsCompact (Γ x)) : BddAbove (f x '' Γ x)

theorem LeanEconomics.le_maxValue {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → ℝ} {Γ : X → Set Y} {x : X} (hf : Continuous ↿f) (hΓc : IsCompact (Γ x)) {y : Y} (hy : y ∈ Γ x) : f x y ≤ maxValue f Γ x

theorem LeanEconomics.maxValue_le {X : Type u_1} {Y : Type u_2} {f : X → Y → ℝ} {Γ : X → Set Y} {x : X} {c : ℝ} (hΓne : (Γ x).Nonempty) (h : ∀ y ∈ Γ x, f x y ≤ c) : maxValue f Γ x ≤ c

theorem LeanEconomics.eventually_forall_lt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → ℝ} {Γ : X → Set Y} {x : X} {c : ℝ} (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. A strict upper bound on the objective over the constraint set survives into a neighbourhood of the parameter. This is the generalized tube lemma combined with upper hemicontinuity, and it makes no nonemptiness assumption, which matters because it is applied below to a correspondence that may be empty-valued.

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

Upper hemicontinuity of the constraint set gives upper semicontinuity of the value.

theorem LeanEconomics.lowerSemicontinuousAt_maxValue {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → ℝ} {Γ : X → Set Y} {x : X} (hf : Continuous ↿f) (hΓne : ∀ (x : X), (Γ x).Nonempty) (hΓc : ∀ (x : X), IsCompact (Γ x)) (hlhc : LowerHemicontinuousAt Γ x) : LowerSemicontinuousAt (maxValue f Γ) x

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

theorem LeanEconomics.continuousAt_maxValue {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → ℝ} {Γ : 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 (maxValue f Γ) x

Berge's maximum theorem, the value function half: if the constraint correspondence is continuous with nonempty compact values and the objective is continuous, then the value of the problem is continuous in the parameter.

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

The value function is continuous, given continuity of the correspondence everywhere.

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

A maximiser exists: the constraint set is compact and the objective continuous.

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

theorem LeanEconomics.maxValue_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → ℝ} {Γ : X → Set Y} {x : X} (hf : Continuous ↿f) (hΓc : IsCompact (Γ x)) {y : Y} (hy : y ∈ argmax f Γ x) : maxValue f Γ x = f x y

At a maximiser the objective equals the value of the problem.

theorem LeanEconomics.upperHemicontinuousAt_argmax {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → ℝ} {Γ : 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) : UpperHemicontinuousAt (argmax f Γ) x

Berge's maximum theorem, the maximiser half: the set of maximisers is upper hemicontinuous. It need not be lower hemicontinuous -- a maximiser can appear abruptly when a tie is reached -- which is why the conclusion is one-sided.

theorem LeanEconomics.continuous_of_upperHemicontinuous_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Γ : X → Set Y} {g : X → Y} (huhc : UpperHemicontinuous Γ) (hsingle : ∀ (x : X), Γ x = {g x}) : Continuous g

A single-valued upper hemicontinuous correspondence is a continuous function. This is how the second half of Berge becomes a continuity statement about the optimal policy, once the maximiser is known to be unique.

theorem LeanEconomics.continuousOn_of_upperHemicontinuous_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Γ : X → Set Y} {g : X → Y} {s : Set X} (huhc : UpperHemicontinuous Γ) (hsingle : ∀ x ∈ s, Γ x = {g x}) : ContinuousOn g s

The same, on a set: single-valuedness is only needed where the conclusion is wanted. This is the version the household models need, since the optimal action is unique on the region where the value function is concave, not necessarily everywhere.

A constraint set that does not move

The degenerate case, recorded to show the hypotheses of the theorems above are simultaneously satisfiable.

theorem LeanEconomics.upperHemicontinuous_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (K : Set Y) : UpperHemicontinuous fun (x : X) => K

theorem LeanEconomics.lowerHemicontinuous_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (K : Set Y) : LowerHemicontinuous fun (x : X) => K

theorem LeanEconomics.continuous_maxValue_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → ℝ} (K : Set Y) (hf : Continuous ↿f) (hKne : K.Nonempty) (hKc : IsCompact K) : Continuous (maxValue f fun (x : X) => K)

Berge is not vacuous. With a fixed compact nonempty constraint set every hypothesis of the maximum theorem holds, and the value of the problem is continuous in the parameter.