Remark — continuity of the best value φ_ι

Proved

SocialEquilibrium.Existence.bestValue_continuousAt

by mikedeng1 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

best-responsecontinuitymaximum-theoremp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

In Debreu's abstract economy, fix an agent $\iota$ and a point $\bar a^0_\iota$ . If $A_\iota$ (with non-void values) has a compact graph $G_\iota$ and is continuous at $\bar a^0_\iota$ , and $f_\iota$ is a continuous function from $G_\iota$ to the completed real line, then

\varphi_\iota(\bar a_\iota)=\max_{a_\iota\in A_\iota(\bar a_\iota)}f_\iota(\bar a_\iota,a_\iota)

is continuous at $\bar a^0_\iota$ .

The continuity of $\varphi_\iota$ is a joint hypothesis on $f_\iota$ and $A_\iota$ in the THEOREM; the Remark replaces it by conditions on each of them separately, and is what the COROLLARY on saddle points uses.

Preamble

import Mathlib
import Definitions.Def_SocialEquilibrium_Existence_graph
import Definitions.Def_SocialEquilibrium_Existence_Game

Formal statement

namespace SocialEquilibrium.Existence

/-- Debreu (1952), §2, p. 889, Remark: if `A_ι` (with non-void values) has a compact graph `G_ι`
and is continuous at `ā⁰_ι`, and `f_ι` is a continuous function from `G_ι` to the completed real
line, then `φ_ι` is continuous at `ā⁰_ι`. -/
theorem bestValue_continuousAt {ι : Type*} [Fintype ι] [DecidableEq ι]
    {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace ℝ (E i)]
    [∀ i, FiniteDimensional ℝ (E i)]
    (X : ∀ i, Set (E i)) (A : ∀ i : ι, Others X i → Set (X i))
    (f : ι → (∀ j, X j) → EReal) (i : ι) (ā₀ : Others X i)
    (hA : ∀ ā : Others X i, (A i ā).Nonempty)
    (hG : IsCompact (graph (A i)))
    (hf : ContinuousOn (fun p : Others X i × X i => f i (join X i p.1 p.2)) (graph (A i)))
    (hAc : ConstraintContinuousAt A i ā₀) :
    ContinuousAt (bestValue X A f i) ā₀ := by sorry

end SocialEquilibrium.Existence

Source

Debreu, A Social Equilibrium Existence Theorem, Proc. Natl. Acad. Sci. USA 38(10), 1952, p. 889, Remark

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting.

$\iota$ is a finite set of agents with decidable equality.
Each $E_j$ is a finite-dimensional real normed space, and $X_j \subseteq E_j$ .
$\bar{\mathfrak A}_i = \prod_{j\ne i} X_j$ , with product-of-subspace topologies.
$A_j$ are constraint maps, and $f_j$ are payoffs into $[-\infty,+\infty]$ , which carries its order topology.
An agent $i$ and a point $\bar a^0$ are fixed.

The best value is $\varphi_i(\bar a) = \sup\{f_i(\bar a, b) : b \in A_i(\bar a)\}$ .

Hypotheses.

$A_i(\bar a) \ne \varnothing$ for every $\bar a \in \bar{\mathfrak A}_i$ .
The graph $G_i = \{(\bar a,b) : b \in A_i(\bar a)\}$ is compact.
$(\bar a, b) \mapsto f_i(\bar a, b)$ is continuous on $G_i$ .
For every $a^0 \in A_i(\bar a^0)$ and every sequence $\bar a^n \to \bar a^0$ , there is a sequence $a^n \to a^0$ with $a^n \in A_i(\bar a^n)$ for all $n$ .

Claim. $\varphi_i : \bar{\mathfrak A}_i \to [-\infty,+\infty]$ is continuous at the point $\bar a^0$ .

Degenerate cases. Hypotheses 1 and 2 make $\bar{\mathfrak A}_i$ compact. Continuity is with respect to the topology of $[-\infty,+\infty]$ , so values $\pm\infty$ are allowed and handled by that topology. If $\bar{\mathfrak A}_i$ is a single point (for example, when there is one agent), the claim is trivial.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph