InterceptContinuity.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Compactness and uniqueness imply continuous dependence of minimizers. No differentiability or inverse-function theorem is used.

theorem OAI.Problem358.CompactArgmin.tendsto_of_unique_minimizer line 18

Source documentation

A compactly constrained family of minimizers converges to the unique minimizer of the limiting continuous objective. The feasible set may be noncompact.

theorem tendsto_of_unique_minimizer {l : Filter I} {p : I → P} {p₀ : P}
    {c : I → C} {c₀ : C} {S K : Set C} {F : P × C → ℝ}
    (hK : IsCompact K) (hS : IsClosed S) (hF : Continuous F)
    (hp : Tendsto p l (𝓝 p₀)) (hbounded : ∀ᶠ i in l, c i ∈ K)
    (hfeasible : ∀ᶠ i in l, c i ∈ S)
    (hmin : ∀ᶠ i in l, ∀ z ∈ S, F (p i, c i) ≤ F (p i, z))
    (hunique : ∀ z ∈ S, IsMinOn (fun w => F (p₀, w)) S z → z = c₀) :
    Tendsto c l (𝓝 c₀) := by
…

theorem OAI.Problem358.CompactArgmin.continuousAt_unique_minimizer line 41

Source documentation

Local compact bounds and uniqueness give continuity of an arbitrary selected minimizer.

theorem continuousAt_unique_minimizer {c : P → C} {p : P}
    {S K : Set C} {F : P × C → ℝ}
    (hK : IsCompact K) (hS : IsClosed S) (hF : Continuous F)
    (hbounded : ∀ᶠ q in 𝓝 p, c q ∈ K)
    (hfeasible : ∀ᶠ q in 𝓝 p, c q ∈ S)
    (hmin : ∀ᶠ q in 𝓝 p, ∀ z ∈ S, F (q, c q) ≤ F (q, z))
    (hunique : ∀ z ∈ S, IsMinOn (fun w => F (p, w)) S z → z = c p) :
    ContinuousAt c p :=
…

theorem OAI.Problem358.MaxPotential.continuous_joint_potential line 64
Source documentation
Finite affine maxima depend jointly continuously on sites, intercepts, and source points.
```
theorem continuous_joint_potential {d : ℕ} :
    Continuous (fun p : ((ι → E d) × (ι → ℝ)) × E d =>
      potential p.1.1 p.1.2 p.2) := by
…
```
Mentions: OAI.Problem358.MaxPotential.potential

theorem OAI.Problem358.MaxPotential.continuous_uniform_integral_potential line 77

Source documentation

The integrated finite affine objective is jointly continuous in all sites and intercepts.

theorem continuous_uniform_integral_potential {d : ℕ} {K : Set (E d)}
    (hK : IsCompact K) (hne : (interior K).Nonempty) :
    Continuous (fun p : (ι → E d) × (ι → ℝ) =>
      ∫ x, potential p.1 p.2 x ∂uniformMeasure K) := by
…

Mentions: OAI.Problem358.MaxPotential.potential

theorem OAI.Problem358.MaxPotential.continuousAt_uniform_intercept_selection line 102

Source documentation

Any normalized minimizing intercept selection depends continuously on the sites at every injective configuration. This needs neither moving-cell derivatives nor IFT.

theorem continuousAt_uniform_intercept_selection {d : ℕ} {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (c : (ι → E d) → ι → ℝ)
    (hc0 : ∀ y, ∑ i, m i * c y i = 0)
    (hcmin : ∀ y (a : ι → ℝ), (∑ i, m i * a i) = 0 →
      (∫ x, potential y (c y) x ∂uniformMeasure K) ≤ ∫ x, potential y a x ∂uniformMeasure K)
    (y : ι → E d) (hy : Function.Injective y) : ContinuousAt c y := by
…

Mentions: OAI.Problem358.MaxPotential.potential

theorem OAI.Problem358.MaxPotential.exists_continuous_uniform_intercept_selection line 134

Source documentation

A globally defined normalized minimizer selection exists, and is continuous on the open set of pairwise distinct sites.

theorem exists_continuous_uniform_intercept_selection {d : ℕ} {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1) :
    ∃ c : (ι → E d) → ι → ℝ,
      (∀ y, ∑ i, m i * c y i = 0) ∧
      (∀ y (a : ι → ℝ), (∑ i, m i * a i) = 0 →
        (∫ x, potential y (c y) x ∂uniformMeasure K) ≤ ∫ x, potential y a x ∂uniformMeasure K) ∧
      ContinuousOn c {y | Function.Injective y} := by
…

Mentions: OAI.Problem358.MaxPotential.potential

theorem OAI.Problem358.FixedMassIntercepts.isOpen_injective_sites line 172
Source documentation
Distinct finite site configurations form an open subset of the ambient coordinate space.
```
theorem isOpen_injective_sites : IsOpen {y : ι → E d | Function.Injective y} := by
…
```

theorem OAI.Problem358.FixedMassIntercepts.intercepts_minimize line 196

Source documentation

The actual prescribed intercepts minimize the integrated affine potential.

theorem intercepts_minimize {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (y : ι → E d) (hy : Function.Injective y) (a : ι → ℝ)
    (ha : ∑ i, m i * a i = 0) :
    (∫ x, MaxPotential.potential y (intercepts hK hconv hne m hm hsum y) x
      ∂uniformMeasure K) ≤ ∫ x, MaxPotential.potential y a x ∂uniformMeasure K := by
…

Mentions: OAI.Problem358.MaxPotential.potential, OAI.Problem358.FixedMassIntercepts.intercepts

theorem OAI.Problem358.FixedMassIntercepts.continuousAt_intercepts_coe line 220

Source documentation

Canonical closed-cell intercepts are continuous at every distinct-site configuration. This compactness argument is independent of the moving-boundary C1 theorem.

theorem continuousAt_intercepts_coe {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (y : ι → E d) (hy : Function.Injective y) :
    ContinuousAt (fun z => (intercepts hK hconv hne m hm hsum z : ι → ℝ)) y := by
…

Mentions: OAI.Problem358.FixedMassIntercepts.intercepts

theorem OAI.Problem358.FixedMassIntercepts.intercepts_eq_zero_of_not_injective line 241

Source documentation

On repeated-site configurations the chosen extension is exactly zero.

theorem intercepts_eq_zero_of_not_injective {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (y : ι → E d) (hy : ¬Function.Injective y) :
    intercepts hK hconv hne m hm hsum y = 0 := by
…

Mentions: OAI.Problem358.FixedMassIntercepts.intercepts

theorem OAI.Problem358.FixedMassIntercepts.measurable_intercepts_coe line 250
Source documentation
The actual normalized intercept choice is globally Borel measurable, including at repeated-site configurations, where its value was explicitly set to zero.
```
theorem measurable_intercepts_coe {K : Set (E d)}
    (hK : IsCompact K) (hconv : Convex ℝ K) (hne : (interior K).Nonempty)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1) :
    Measurable (fun y => (intercepts hK hconv hne m hm hsum y : ι → ℝ)) := by
…
```
Mentions: OAI.Problem358.FixedMassIntercepts.intercepts