OAI/Analysis/AffineBernstein/NormalizedCaps.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_caps_radius line 20

   Source comment

   Quantitative cap transfer: a given limit radius costs only one unit. The constant does not depend on the sequence or its limit set.

   theorem LocalDistanceConverges.eventually_caps_radius
       {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E]
       {Cj : ℕ → Set E} {C : Set E} (h : LocalDistanceConverges Cj C)
       (hcl : IsClosed C) (hclj : ∀ j, IsClosed (Cj j))
       (hcvj : ∀ j, Convex ℝ (Cj j)) (hnej : ∀ j, (Cj j).Nonempty)
       (ell : E →L[ℝ] ℝ) (b R : ℝ)
       (hcap : C ∩ {x | ell x ≤ b} ⊆ closedBall 0 R)
       {q : E} (hq : q ∈ C) (hqb : ell q < b) :
       ∀ᶠ j in atTop, Cj j ∩ {x | ell x ≤ b} ⊆ ball 0 (R+1) := by
   …

   Mentions: OAI.AffineBernstein.LocalDistanceConverges

2. def OAI.AffineBernstein.positiveBaseForm line 67

   Source comment

   The positive base functional occurring in normalized model caps.

   def positiveBaseForm {k m : ℕ} (a : Fin k → ℝ) : (Space k × Space m) →L[ℝ] ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

3. lemma OAI.AffineBernstein.positiveBaseForm_apply line 70
4. lemma OAI.AffineBernstein.norm_le_sqrt_card_mul_of_coord_le line 74
5. lemma OAI.AffineBernstein.IsModelShape.normalized_cap_box line 83
6. lemma OAI.AffineBernstein.IsModelShape.normalized_cap_radius line 101
7. lemma OAI.AffineBernstein.IsModelShape.normalized_center_ball line 116

   Source comment

   Uniform interior ball about (1,0), with an explicit positive radius.

   lemma IsModelShape.normalized_center_ball {k m : ℕ} {C : Set (Space k × Space m)}
       (hC : IsModelShape C) {r : ℝ} (hr : 0 < r)
       (hin : closedBall (0 : Space m) r ⊆
         modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ)))) :
       closedBall ((WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))), (0 : Space m))
         (min (1/4) (r/4)) ⊆ interior C := by
   …

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

8. theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_normalized_cap_radius line 137

   Source comment

   Eventual cap bounds with constants fixed before the approximating sequence.

   theorem LocalDistanceConverges.eventually_normalized_cap_radius
       {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 B α : ℝ} {a : Fin k → ℝ}
       (hB : 0 < B) (hα : 0 < α) (ha : ∀ i, α ≤ a i)
       (hout : modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))) ⊆ closedBall 0 R) :
       ∀ᶠ j in atTop, Cj j ∩ {p | positiveBaseForm a p ≤ B} ⊆
         ball 0 (max (Real.sqrt k * max 1 (B/α)) (max 1 (B/α)*R)+1) := by
   …

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

9. theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_normalized_fiber_outer line 151

   Source comment

   Uniform outer fiber bounds on an entire fixed positive box. A single containing cap gives one index, rather than using pointwise convergence.

   theorem LocalDistanceConverges.eventually_normalized_fiber_outer
       {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 : ℝ} (hb : 1 ≤ b)
       (hout : modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))) ⊆ closedBall 0 R) :
       ∀ᶠ j in atTop, ∀ s : Space k, (∀ i, s i ∈ Icc a b) →
         modelFiber (Cj j) s ⊆ closedBall 0
           (max (Real.sqrt k * max 1 (k*b+1)) (max 1 (k*b+1)*R)+1) := by
   …

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

10. theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_normalized_fibers line 179

    Source comment

    Simultaneous two-sided bounds and nonempty fiber interiors. The parameters in the radii are fixed before an approximating index is chosen.

    theorem LocalDistanceConverges.eventually_normalized_fibers
        {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 R a b : ℝ}
        (hr : 0 < r) (ha : 0 < a) (ha1 : a ≤ 1) (hb : 1 ≤ b)
        (hin : closedBall (0 : Space m) r ⊆
          modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))))
        (hout : modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))) ⊆ closedBall 0 R) :
        ∀ᶠ j in atTop, ∀ s : Space k, (∀ i, s i ∈ Icc a b) →
          closedBall (0 : Space m) (a*r/2) ⊆ modelFiber (Cj j) s ∧
          0 ∈ interior (modelFiber (Cj j) s) ∧
    …

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

11. theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_normalized_center_ball line 200

    Source comment

    One explicit interior ball survives in every large approximant.

    theorem LocalDistanceConverges.eventually_normalized_center_ball
        {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 : ℝ} (hr : 0 < r)
        (hin : closedBall (0 : Space m) r ⊆
          modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ)))) :
        ∀ᶠ j in atTop, closedBall
          ((WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))), (0 : Space m))
          (min (1/4) (r/4)) ⊆ Cj j := by
    …

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