ModelCenteringFurther.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.strictConvexOn_of_hasDerivWithinAt2_pos line 93
Source comment
Intrinsic convergence always entails convergence of base points. Completeness prevents a finite base endpoint from being lost when graph paths make a sequence intrinsically Cauchy. A chord bound along a family of segments turns ordinary Cauchy control of base and height into control for the actual graph metric. Restricting a monotone-height ray to any oriented subsegment gives the uniform chord bound used to exhibit an intrinsic Cauchy tail. A bounded ray with monotone graph height cannot end at a missing finite base point of a complete graph. This proves the metric step rather than assuming properness of the embedding. A differentiable convex function on a finite half-open interval has a monotone tail (in one of the two orientations). The tangent line at the initial point bounds a convex ray from below, so an upper bound on a finite ray implies a two-sided bound. Completeness forbids any bounded convex ray from reaching a missing finite endpoint. Convexity and two-sided variation, not a growth hypothesis, produce the required metric Cauchy sequence. The metric obstruction applied to an arbitrary bounded-height sequence, not merely points already lying on a fixed ray. This is the core boundary properness argument in geometry.tex:36–55. Actual height sublevels are closed in the ambient base space. No convex extension of u to missing boundary points is used. Finite boundary blow-up, derived from the manuscript's literal Euclidean intrinsic completeness assumption. The epigraph is genuinely closed in Rⁿ × R. Completeness was not silently replaced by properness of the graph embedding. Strict version of the second-derivative test, with specified derivatives.
```
theorem strictConvexOn_of_hasDerivWithinAt2_pos {D : Set ℝ} (hD : Convex ℝ D)
    {f f' f'' : ℝ → ℝ} (hf : ContinuousOn f D)
    (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x)
    (hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x)
    (hf''₀ : ∀ x ∈ interior D, 0 < f'' x) : StrictConvexOn ℝ D f := by
…
```

theorem OAI.AffineBernstein.strictConvexOn_segment line 107

Source comment

The standing Hessian hypothesis gives strict convexity on every nonconstant base segment, with the literal coordinate Hessian, not an abstract Hessian.

theorem strictConvexOn_segment {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    {x y : Space n} (hx : x ∈ Ω) (hy : y ∈ Ω) (hxy : y ≠ x) :
    StrictConvexOn ℝ (Icc (0 : ℝ) 1) (fun t => u (x + t • (y - x))) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian

def OAI.AffineBernstein.tangentHeight line 141
Source comment
The tangent-plane height used in all source sections.
```
def tangentHeight {n : ℕ} (u : Space n → ℝ) (a x : Space n) : ℝ :=
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.tangentHeight_self line 144
theorem OAI.AffineBernstein.tangentHeight_pos line 147
theorem OAI.AffineBernstein.convexOn_tangentHeight line 166
theorem OAI.AffineBernstein.continuousOn_tangentHeight line 183

theorem OAI.AffineBernstein.isClosed_tangent_sublevel line 191

Source comment

Tangent-plane sublevels are closed, by closedness of the actual epigraph. No implicit completeness-invariance under a shear is needed.

theorem isClosed_tangent_sublevel {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hne : Ω.Nonempty) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hcv : ConvexOn ℝ Ω u)
    (hc : EuclideanGraphComplete Ω u) (a : Space n) (t : ℝ) :
    IsClosed {x | x ∈ Ω ∧ tangentHeight u a x ≤ t} := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.tangentHeight

theorem OAI.AffineBernstein.tangentHeight_coercive line 208

Source comment

A finite-radius positive support gap yields a linear coercivity bound. This replaces only the choice of constants in geometry.tex:56–67, not any standing hypothesis or conclusion.

theorem tangentHeight_coercive {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    {a : Space n} (ha : a ∈ Ω) :
    ∃ r > 0, ∃ m > 0, ∀ x ∈ Ω, r ≤ ‖x - a‖ →
      m * ‖x - a‖ ≤ r * tangentHeight u a x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.tangentHeight

theorem OAI.AffineBernstein.isCompact_tangent_sublevel line 258
Source comment
The compact tangent sections required throughout the manuscript, proved from PD Hessian, convexity of the open base, and intrinsic graph completeness.
```
theorem isCompact_tangent_sublevel {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (hc : EuclideanGraphComplete Ω u) {a : Space n} (ha : a ∈ Ω) (t : ℝ) :
    IsCompact {x | x ∈ Ω ∧ tangentHeight u a x ≤ t} := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.tangentHeight
theorem OAI.AffineBernstein.tangentHeight_nonneg line 276

theorem OAI.AffineBernstein.interior_epigraph line 287

Source comment

Interior of the epigraph, including the correct restriction to the open base domain. This is a local continuity fact and needs no completeness.

theorem interior_epigraph {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {u : Space n → ℝ} (hu : ContinuousOn u Ω) :
    interior {p : Space n × ℝ | p.1 ∈ Ω ∧ u p.1 ≤ p.2} =
      {p | p.1 ∈ Ω ∧ u p.1 < p.2} := by
…

Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.frontier_epigraph_of_complete line 313
theorem OAI.AffineBernstein.epigraph_interior_nonempty line 330

theorem OAI.AffineBernstein.isCompact_tangent_cap line 338

Source comment

Compactness of the entire tangent cap, not just its projection.

theorem isCompact_tangent_cap {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (hc : EuclideanGraphComplete Ω u) {a : Space n} (ha : a ∈ Ω) (t : ℝ) :
    IsCompact {p : Space n × ℝ | p.1 ∈ Ω ∧ u p.1 ≤ p.2 ∧
      p.2 - u a - fderiv ℝ u a (p.1 - a) ≤ t} := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete

def OAI.AffineBernstein.tangentSection line 378
Source comment
The manuscript's open tangent section.
```
def tangentSection {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ)
    (a : Space n) (t : ℝ) : Set (Space n) :=
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.closure_tangentSection line 385
Source comment
For positive height the closed sublevel is precisely the closure of the open tangent section. Completeness supplies closedness; convexity supplies approximation from the section interior.
```
theorem closure_tangentSection {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (hc : EuclideanGraphComplete Ω u) {a : Space n} (ha : a ∈ Ω)
    {t : ℝ} (ht : 0 < t) :
    closure (tangentSection Ω u a t) = {x | x ∈ Ω ∧ tangentHeight u a x ≤ t} := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.tangentSection, OAI.AffineBernstein.tangentHeight
def OAI.AffineBernstein.SectionBalance line 416
Source comment
Source equation uniform-section-balance, in unshifted coordinates; equivalently, -ρ(closure S-a) ⊆ closure S-a.
```
def SectionBalance {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ) (ρ : ℝ) : Prop :=
…
```
Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.sectionBalance_reflection line 422

Source comment

A direct form of the closed-section reflection, with arbitrary finite height (zero included). No balance conclusion is assumed about the domain.

theorem sectionBalance_reflection {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (hc : EuclideanGraphComplete Ω u) {ρ : ℝ} (hbal : SectionBalance Ω u ρ)
    {a x : Space n} (ha : a ∈ Ω) (hx : x ∈ Ω) :
    a - ρ • (x - a) ∈ Ω ∧
    tangentHeight u a (a - ρ • (x - a)) ≤ tangentHeight u a x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.SectionBalance, OAI.AffineBernstein.tangentHeight

theorem OAI.AffineBernstein.eq_univ_of_dilation line 440
Source comment
An open set containing a point and invariant under one dilation about it of factor greater than one is the whole vector space.
```
theorem eq_univ_of_dilation {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
    {a : Space n} (ha : a ∈ Ω) {c : ℝ} (hc : 1 < c)
    (hexpand : ∀ x ∈ Ω, a + c • (x - a) ∈ Ω) : Ω = univ := by
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.eq_univ_of_sectionBalance line 465
Source comment
The domain-extension conclusion of rigidity.tex:38–87. Uniform reflection of actual tangent sections, once proved by the model argument, forces all rays to continue. This lemma does not assume whole-domain solvability.
```
theorem eq_univ_of_sectionBalance {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hne : Ω.Nonempty) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (hc : EuclideanGraphComplete Ω u) {ρ : ℝ} (hρ : 0 < ρ)
    (hbal : SectionBalance Ω u ρ) : Ω = univ := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.SectionBalance

theorem OAI.AffineBernstein.gap_doubling_of_sectionBalance line 479

Source comment

The exact gap-doubling constants from rigidity.tex, proved before assuming that the base is all of Rⁿ. Thus the same calculation supplies ray extension.

theorem gap_doubling_of_sectionBalance {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (hc : EuclideanGraphComplete Ω u) {ρ : ℝ} (hρ : 0 < ρ)
    (hbal : SectionBalance Ω u ρ) {a x : Space n} (ha : a ∈ Ω) (hx : x ∈ Ω) :
    a + (1 + ρ / 2) • (x - a) ∈ Ω ∧
    tangentHeight u a (a + (1 + ρ / 2) • (x - a)) ≤
      ((2 + ρ) * (1 + ρ) / ρ) * tangentHeight u a x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.SectionBalance, OAI.AffineBernstein.tangentHeight

theorem OAI.AffineBernstein.tangentHeight_ray_mono line 532

Source comment

Convexity of the actual support gap gives its monotonicity on every ray.

theorem tangentHeight_ray_mono {n : ℕ} {u : Space n → ℝ}
    (hu : ConvexOn ℝ univ u) (hmin : ∀ a x, 0 ≤ tangentHeight u a x)
    (a e : Space n) {r s : ℝ} (hr : 0 ≤ r) (hrs : r ≤ s) :
    tangentHeight u a (a + r • e) ≤ tangentHeight u a (a + s • e) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.tangentHeight

theorem OAI.AffineBernstein.normalized_value_le_quarter line 552

Source comment

The normalization B₁⊆{v<1}, at a zero tangent, gives v≤1/4 on B₁/₄.

theorem normalized_value_le_quarter {n : ℕ} {v : Space n → ℝ}
    (hv : ConvexOn ℝ univ v) (hzero : v 0 = 0) (hdzero : fderiv ℝ v 0 = 0)
    (hinner : Metric.ball 0 1 ⊆ tangentSection univ v 0 1)
    {x : Space n} (hx : ‖x‖ < 1 / 4) : v x ≤ 1 / 4 := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.tangentSection

theorem OAI.AffineBernstein.fixed_radius_gap_of_sectionBalance line 569

Source comment

Source fixed-radius-gap. The proof uses reflected closed sections directly, rather than choosing the intersection with their radial boundary.

theorem fixed_radius_gap_of_sectionBalance {n : ℕ} {v : Space n → ℝ}
    (hv : ContDiff ℝ ∞ v) (hp : ∀ x, (hessian v x).PosDef)
    (hc : EuclideanGraphComplete univ v)
    (hzero : v 0 = 0) (hdzero : fderiv ℝ v 0 = 0)
    {ρ R : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hR : 1 ≤ R)
    (hbal : SectionBalance univ v ρ)
    (hinner : Metric.ball 0 1 ⊆ tangentSection univ v 0 1)
    (houter : tangentSection univ v 0 1 ⊆ Metric.ball 0 R)
    {x e : Space n} (hx : ‖x‖ < 1 / 4) (he : ‖e‖ = 1) :
    (1 / 4 : ℝ) ≤ tangentHeight v x (x + (2 * R / ρ) • e) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.SectionBalance, OAI.AffineBernstein.tangentSection, OAI.AffineBernstein.tangentHeight

def OAI.AffineBernstein.modulusIterates line 618
Source comment
Exact integer in rigidity.tex: N(r)=max(0,ceil(log_beta(R*/r))). The natural-number ceiling incorporates max with zero.
```
def modulusIterates (ρ R r : ℝ) : ℕ :=
…
```
def OAI.AffineBernstein.normalizedModulus line 622
Source comment
Exact lower modulus b(r)=1/(8 A^N(r)) from the manuscript.
```
def normalizedModulus (ρ R r : ℝ) : ℝ :=
…
```
theorem OAI.AffineBernstein.normalizedModulus_pos line 625
theorem OAI.AffineBernstein.modulusIterates_spec line 630

theorem OAI.AffineBernstein.gap_doubling_iterate line 641

Source comment

Iterate the source's doubling inequality for the actual gap at a point.

theorem gap_doubling_iterate {n : ℕ} {u : Space n → ℝ}
    (hu : ContDiff ℝ ∞ u) (hp : ∀ x, (hessian u x).PosDef)
    (hc : EuclideanGraphComplete univ u) {ρ : ℝ} (hρ : 0 < ρ)
    (hbal : SectionBalance univ u ρ) (a x : Space n) (k : ℕ) :
    tangentHeight u a (a + (1 + ρ / 2) ^ k • (x - a)) ≤
      ((2 + ρ) * (1 + ρ) / ρ) ^ k * tangentHeight u a x := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.SectionBalance, OAI.AffineBernstein.tangentHeight

theorem OAI.AffineBernstein.normalized_modulus_of_sectionBalance line 668

Source comment

Uniform normalized modulus, rigidity.tex:118–175. Every quantifier is uniform in the normalized function, point and direction; only rho and R occur in the explicit modulus. The section balance producer remains separate.

theorem normalized_modulus_of_sectionBalance {n : ℕ} {v : Space n → ℝ}
    (hv : ContDiff ℝ ∞ v) (hp : ∀ x, (hessian v x).PosDef)
    (hc : EuclideanGraphComplete univ v)
    (hzero : v 0 = 0) (hdzero : fderiv ℝ v 0 = 0)
    {ρ R : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hR : 1 ≤ R)
    (hbal : SectionBalance univ v ρ)
    (hinner : Metric.ball 0 1 ⊆ tangentSection univ v 0 1)
    (houter : tangentSection univ v 0 1 ⊆ Metric.ball 0 R)
    {x : Space n} (hx : x ∈ Metric.ball 0 (1 / 4)) {r : ℝ} (hr : 0 < r) :
    tangentSection univ v x (normalizedModulus ρ R r) ⊆ Metric.ball x r := by
…

def OAI.AffineBernstein.tangentModelEquiv line 715
Source comment
The manuscript's epigraph; the domain is not silently replaced by all of space. Literal tangent affine coordinates, ordered as one base direction and n transverse directions.
```
def tangentModelEquiv {n : ℕ} (u : Space n → ℝ) (a : Space n) :
    (Space n × ℝ) ≃ᴬ[ℝ] (Space 1 × Space n) := by
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.tangentModelEquiv_apply line 735
theorem OAI.AffineBernstein.tangentModelEquiv_fst line 741
theorem OAI.AffineBernstein.tangentModelEquiv_snd line 747
theorem OAI.AffineBernstein.tangent_epigraph_isModelShape line 753
Source comment
Completeness supplies an actual one-direction model in the affine family.
```
theorem tangent_epigraph_isModelShape {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (hc : EuclideanGraphComplete Ω u) {a : Space n} (ha : a ∈ Ω) :
    IsModelShape (tangentModelEquiv u a '' sourceEpigraph Ω u) := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.tangentModelEquiv, OAI.AffineBernstein.sourceEpigraph
theorem OAI.AffineBernstein.tangent_epigraph_in_family line 788
theorem OAI.AffineBernstein.tangent_model_fiber line 798
theorem OAI.AffineBernstein.model_dimension line 823
Source comment
A model's direction number is bounded by the actual ambient dimension, using an invertible affine map from its approximating sequence.
```
theorem model_dimension {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {D : Set E} {k m : ℕ} {C : Set (Space k × Space m)}
    (hf : InAffineLimitFamily D C) : k+m = Module.finrank ℝ E := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.InAffineLimitFamily

theorem OAI.AffineBernstein.exists_maximal_model line 832

Source comment

A maximal direction number exists; this is genuine finite-dimensional maximality rather than a postulated geometric estimate.

theorem exists_maximal_model {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {D : Set E}
    (h1 : ∃ m, ∃ C : Set (Space 1 × Space m), IsModelShape C ∧ InAffineLimitFamily D C) :
    ∃ (k m : ℕ) (C : Set (Space k × Space m)), 1 ≤ k ∧ IsModelShape C ∧
      InAffineLimitFamily D C ∧ ∀ (r d : ℕ) (C' : Set (Space r × Space d)),
      IsModelShape C' → InAffineLimitFamily D C' → r ≤ k := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.InAffineLimitFamily

theorem OAI.AffineBernstein.sectionBalance_of_no_two_model line 855
Source comment
Once the geometric/analytic exclusion of two-direction models is proved, all tangent sections (all centers and heights) inherit one common balance. This is a faithful integration lemma, not the main theorem.
```
theorem sectionBalance_of_no_two_model {n : ℕ} {Ω : Set (Space n)}
    (hΩ : IsOpen Ω) (hne : Ω.Nonempty) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (hc : EuclideanGraphComplete Ω u)
    (hno : ∀ (d : ℕ), n = d+1 → ∀ C : Set (Space 2 × Space d),
      IsModelShape C → InAffineLimitFamily (sourceEpigraph Ω u) C → False) :
    ∃ ρ : ℝ, 0 < ρ ∧ ρ ≤ 1 ∧ SectionBalance Ω u ρ := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.EuclideanGraphComplete, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.InAffineLimitFamily, OAI.AffineBernstein.sourceEpigraph, OAI.AffineBernstein.SectionBalance