InteriorLimits.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.ball_subset_of_infDist_lt line 19

Source comment

Quantitative inner containment from distance-function closeness. This is an actual projection argument for convex bodies, not an assumed stability axiom.

theorem ball_subset_of_infDist_lt {K : Set E} (hK : IsClosed K)
    (hcv : Convex ℝ K) (hne : K.Nonempty) (a : E) {r : ℝ} (hr : 0 < r)
    (happ : ∀ y ∈ Metric.closedBall a r, infDist y K < r / 2) :
    Metric.ball a (r / 2) ⊆ K := by
…

theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_ball_subset_interior line 62

Source comment

An interior ball of the limit has a fixed smaller ball lying in the interiors of all late approximants.

theorem LocalDistanceConverges.eventually_ball_subset_interior
    {Cj : ℕ → Set E} {C : Set E} (h : LocalDistanceConverges Cj C)
    (hclj : ∀ j, IsClosed (Cj j)) (hcvj : ∀ j, Convex ℝ (Cj j))
    (hnej : ∀ j, (Cj j).Nonempty) {a : E} {r : ℝ} (hr : 0 < r)
    (hball : Metric.closedBall a r ⊆ C) :
    ∀ᶠ j in atTop, Metric.ball a (r / 2) ⊆ interior (Cj j) := by
…

Mentions: OAI.AffineBernstein.LocalDistanceConverges

theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_compact_subset_interior line 82

Source comment

Compact subsets of the interior are eventually interior subsets of the approximants, as required by the model normalization argument.

theorem LocalDistanceConverges.eventually_compact_subset_interior
    {Cj : ℕ → Set E} {C S : Set E} (h : LocalDistanceConverges Cj C)
    (hclj : ∀ j, IsClosed (Cj j)) (hcvj : ∀ j, Convex ℝ (Cj j))
    (hnej : ∀ j, (Cj j).Nonempty) (hS : IsCompact S)
    (hSC : S ⊆ interior C) : ∀ᶠ j in atTop, S ⊆ interior (Cj j) := by
…

Mentions: OAI.AffineBernstein.LocalDistanceConverges

structure OAI.AffineBernstein.IsModelShape line 110
Source comment
The geometric conditions of a k-model, in its distinguished coordinates. Membership in the affine local-limit family is separate from these conditions.
```
structure IsModelShape {k m : ℕ} (C : Set (Space k × Space m)) : Prop where
…
```
Mentions: OAI.AffineBernstein.Space
def OAI.AffineBernstein.modelFiber line 119
Source comment
The transverse fiber, including lower-dimensional and boundary fibers.
```
def modelFiber {k m : ℕ} (C : Set (Space k × Space m)) (s : Space k) : Set (Space m) :=
…
```
Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.closed_convex_add_of_ray line 124

Source comment

The ray containment recession argument in geometry.tex does not need full-dimensionality.

theorem closed_convex_add_of_ray {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {C : Set E} (hc : IsClosed C) (hv : Convex ℝ C) {x v : E}
    (hx : x ∈ C) (hray : ∀ t : ℝ, 0 ≤ t → t • v ∈ C) : x + v ∈ C := by
…

theorem OAI.AffineBernstein.IsModelShape.zero_mem line 144
theorem OAI.AffineBernstein.IsModelShape.add_nonnegative_base line 147
theorem OAI.AffineBernstein.IsModelShape.fiber_mono line 155
theorem OAI.AffineBernstein.IsModelShape.fiber_zero line 161
theorem OAI.AffineBernstein.IsModelShape.fiber_convex line 164
theorem OAI.AffineBernstein.IsModelShape.fiber_closed line 170
theorem OAI.AffineBernstein.IsModelShape.fiber_compact line 173
theorem OAI.AffineBernstein.IsModelShape.fiber_contract line 181
theorem OAI.AffineBernstein.IsModelShape.fiber_interior_nonempty line 194
Source comment
Every strictly positive fiber is full dimensional; this proof also covers m=0, using the ordinary topology of the zero-dimensional space.
```
theorem fiber_interior_nonempty {s : Space k} (hs : ∀ i, 0 < s i) :
    (interior (modelFiber C s)).Nonempty := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.modelFiber

theorem OAI.AffineBernstein.IsModelShape.fiber_box_bound line 224

Source comment

Monotonicity and homothety turn a bound on the distinguished fiber into a uniform bound on every fixed base box.

theorem fiber_box_bound {R T : ℝ} (hT : 1 ≤ T)
    (hR : modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1 : ℝ))) ⊆ Metric.closedBall 0 R)
    {s : Space k} (hs : ∀ i, s i ≤ T) {y : Space m} (hy : y ∈ modelFiber C s) :
    ‖y‖ ≤ T * R := by
…

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