NormedCompactInterior.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_normed_compact_subset line 23

Source comment

Compact inner containment for the literal (possibly non-Hilbert) ambient norm. In particular the product coordinate norm creates no hidden instance.

theorem LocalDistanceConverges.eventually_normed_compact_subset
    {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 ⊆ Cj j := by
…

Mentions: OAI.AffineBernstein.LocalDistanceConverges

lemma OAI.AffineBernstein.IsModelShape.fiber_small_ball line 49

Source comment

The lower inclusion in geometry.tex (normalized-fiber-box), with the source's exact radius a*r. It is a convexity/recession consequence.

lemma IsModelShape.fiber_small_ball {k m : ℕ} {C : Set (Space k × Space m)}
    (hC : IsModelShape C) {r a : ℝ} (ha : 0 < a) (ha1 : a ≤ 1)
    (hin : closedBall (0 : Space m) r ⊆
      modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))))
    {s : Space k} (hs : ∀ i, a ≤ s i) :
    closedBall (0 : Space m) (a*r) ⊆ modelFiber C s := by
…

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

lemma OAI.AffineBernstein.IsModelShape.normalized_fiber_box line 66

lemma OAI.AffineBernstein.IsModelShape.normalized_fiber_interior line 80

Source comment

Strictly smaller transverse balls over a positive box lie in the actual ambient interior; this is what local convex-set convergence transfers.

lemma IsModelShape.normalized_fiber_interior {k m : ℕ} {C : Set (Space k × Space m)}
    (hC : IsModelShape C) {r a : ℝ} (hr : 0 < r) (ha : 0 < a) (ha1 : a ≤ 1)
    (hin : closedBall (0 : Space m) r ⊆
      modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))))
    {s : Space k} (hs : ∀ i, a ≤ s i) {y : Space m} (hy : ‖y‖ ≤ a*r/2) :
    (s,y) ∈ interior C := by
…

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

theorem OAI.AffineBernstein.uniform_model_fiber_normalization line 109

Source comment

Centering gives the exact normalization constants before the model and positive fiber are selected. No compactness modulus or analytic estimate is assumed. This is the first part of the manuscript's normalized-fibers corollary.

theorem uniform_model_fiber_normalization {k m : ℕ} (hm : 1 ≤ m)
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E]
    {D : Set E} (hD : IsClosed D) (hneD : D.Nonempty)
    (hmax : ∀ (d : ℕ), m = d+1 → ∀ C' : Set (Space (k+1) × Space d),
      IsModelShape C' → InAffineLimitFamily D C' → False) :
    ∃ c : ℝ, 1 ≤ c ∧ ∀ C : Set (Space k × Space m),
      IsModelShape C → InAffineLimitFamily D C → ∀ s : Space k, ∀ hs : ∀ i, 0 < s i,
      ∃ A : Space m ≃L[ℝ] Space m,
        let C' := ((positiveBaseEquiv s hs).prodCongr A) '' C
…

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

theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_normalized_fiber_inner line 149

Source comment

The lower-box bound transfers to every approximant simultaneously over that box, not separately at each s. The radius is uniform in the model.

theorem LocalDistanceConverges.eventually_normalized_fiber_inner
    {k m : ℕ} {Cj : ℕ → Set (Space k × Space m)} {C : Set (Space k × Space m)}
    (h : LocalDistanceConverges Cj C) (hC : IsModelShape C)
    (hclj : ∀ j, IsClosed (Cj j)) (hcvj : ∀ j, Convex ℝ (Cj j))
    (hnej : ∀ j, (Cj j).Nonempty) {r a b : ℝ}
    (hr : 0 < r) (ha : 0 < a) (ha1 : a ≤ 1)
    (hin : closedBall (0 : Space m) r ⊆
      modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ)))) :
    ∀ᶠ j in atTop, ∀ s : Space k, (∀ i, s i ∈ Icc a b) →
      closedBall (0 : Space m) (a*r/2) ⊆ modelFiber (Cj j) s := by
…

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