ModelLimit.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.LocalDistanceConverges.isModelShape_of_normalized line 21

Source comment

Normalized model limits retain the genuine geometric model conditions. The fixed inner balls prevent collapse; the distinguished-fiber outer bound controls every cap by the already proved recession/fiber inequalities.

theorem LocalDistanceConverges.isModelShape_of_normalized
    (h : LocalDistanceConverges Cj C) (hj : ∀ j, IsModelShape (Cj j))
    (hclosed : IsClosed C) (hconvex : Convex ℝ C) (hne : C.Nonempty)
    {cj : ℕ → Space m} {c : Space m} (hc : Tendsto cj atTop (𝓝 c))
    {R : ℝ}
    (hinner : ∀ j, closedBall (cj j) 1 ⊆ modelFiber (Cj j)
      (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))))
    (houter : ∀ j, modelFiber (Cj j) (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))) ⊆ closedBall 0 R) :
    IsModelShape C := by
…

Mentions: OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.Space, OAI.AffineBernstein.modelFiber

theorem OAI.AffineBernstein.model_base_contraction line 93
Source comment
The shrinking factor avoids any positivity assumption on approximating base coordinates. It tends to one and contracts each coordinate below one.
```
theorem model_base_contraction (s : Space k) (i : Fin k) :
    (1 + ‖s - WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))‖)⁻¹ * s i ≤ 1 := by
…
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.LocalDistanceConverges.exists_exact_fiber_approximating line 103
Source comment
Exact-fiber approximation in geometry.tex:285–300. The actual contracting points are used, not an assumed commutation of slicing with local limits.
```
theorem LocalDistanceConverges.exists_exact_fiber_approximating
    (h : LocalDistanceConverges Cj C) (hj : ∀ j, IsModelShape (Cj j))
    {y : Space m} (hy : y ∈ modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ)))) :
    ∃ yj : ℕ → Space m,
      (∀ j, yj j ∈ modelFiber (Cj j) (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ)))) ∧
      Tendsto yj atTop (𝓝 y) := by
…
```
Mentions: OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.Space, OAI.AffineBernstein.modelFiber

theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_infDist_fiber_lt_uniform line 130

Source comment

Uniform reverse Hausdorff inclusion follows by compactness of the actual positive limit fiber and the preceding exact approximations.

theorem LocalDistanceConverges.eventually_infDist_fiber_lt_uniform
    (h : LocalDistanceConverges Cj C) (hj : ∀ j, IsModelShape (Cj j))
    (hC : IsModelShape C) {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ j in atTop, ∀ y ∈ modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))),
      infDist y (modelFiber (Cj j) (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ)))) < ε := by
…

Mentions: OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.modelFiber

theorem OAI.AffineBernstein.LocalDistanceConverges.tendsto_hausdorffDist_fibers line 156

Source comment

Exact-fiber Hausdorff convergence with a common outer radius. This is stronger than pointwise local convergence but follows from the model recession structure; arbitrary slices of arbitrary converging bodies need not converge.

theorem LocalDistanceConverges.tendsto_hausdorffDist_fibers
    (h : LocalDistanceConverges Cj C) (hj : ∀ j, IsModelShape (Cj j))
    (hC : IsModelShape C) {R : ℝ}
    (hR : ∀ j, modelFiber (Cj j) (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))) ⊆ closedBall 0 R) :
    Tendsto (fun j => hausdorffDist (modelFiber (Cj j) (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))))
      (modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))))) atTop (𝓝 0) := by
…

Mentions: OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.modelFiber

theorem OAI.AffineBernstein.LocalDistanceConverges.zero_mem_frontier_fiber_of_asymmetry line 190

Source comment

A failure of all growing centering constants forces the origin onto the boundary of the limit fiber. No centering stability is assumed.

theorem LocalDistanceConverges.zero_mem_frontier_fiber_of_asymmetry
    (h : LocalDistanceConverges Cj C) (hj : ∀ j, IsModelShape (Cj j))
    (hC : IsModelShape C) {R : ℝ}
    (hR : ∀ j, modelFiber (Cj j) (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))) ⊆ closedBall 0 R)
    (hfail : ∀ j : ℕ, 1 ≤ j →
      ¬ -(modelFiber (Cj j) (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ)))) ⊆
        (j : ℝ) • modelFiber (Cj j) (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ)))) :
    (0 : Space m) ∈ frontier (modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ)))) := by
…

Mentions: OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.modelFiber, OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.IsModelShape.support_from_fiber line 240
Source comment
A fiber support at zero extends to the whole model by the same actual contraction and recession operation used for exact-fiber approximation.
```
theorem IsModelShape.support_from_fiber (hC : IsModelShape C)
    (ell : Space m →L[ℝ] ℝ)
    (hell : ∀ y ∈ modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))), 0 ≤ ell y) :
    ∀ p ∈ C, 0 ≤ ell p.2 := by
…
```
Mentions: OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.Space, OAI.AffineBernstein.modelFiber
theorem OAI.AffineBernstein.IsModelShape.exists_global_support_of_zero_boundary line 257
Source comment
The nonzero supporting functional whose new positive coordinate is used in the thin-slice blowup. Hahn–Banach is reused from pinned Mathlib.
```
theorem IsModelShape.exists_global_support_of_zero_boundary (hC : IsModelShape C)
    (hzero : (0 : Space m) ∉ interior (modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))))) :
    ∃ ell : Space m →L[ℝ] ℝ, ell ≠ 0 ∧ (∀ p ∈ C, 0 ≤ ell p.2) := by
…
```
Mentions: OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.Space, OAI.AffineBernstein.modelFiber