OAI/Analysis/AffineBernstein/ThinSlices.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.thinSlice line 21

   Source comment

   Thin slices and rescalings before reordering the k+1 base coordinates.

   def thinSlice (C : Set (Space k × (ℝ × Space d))) (ε : ℝ) : Set (Space d) :=
   …

   Mentions: OAI.AffineBernstein.Space

2. def OAI.AffineBernstein.thinRescaling line 24
3. structure OAI.AffineBernstein.IsSupportedSplitModel line 29

   Source comment

   Supports and the original orthant after a support-coordinate split.

   structure IsSupportedSplitModel (C : Set (Space k × (ℝ × Space d))) : Prop where
   …

   Mentions: OAI.AffineBernstein.Space

4. theorem OAI.AffineBernstein.IsSupportedSplitModel.zero_mem line 43
5. theorem OAI.AffineBernstein.IsSupportedSplitModel.one_mem line 46
6. theorem OAI.AffineBernstein.IsSupportedSplitModel.base_mono line 49
7. theorem OAI.AffineBernstein.IsSupportedSplitModel.slice_interior_zero line 59

   Source comment

   Every slice at a sufficiently low positive support level contains a real ball about zero, obtained by contraction of the interior ball at (1,0).

   theorem slice_interior_zero {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) :
       (0 : Space d) ∈ interior (thinSlice C ε) := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.thinSlice

8. theorem OAI.AffineBernstein.IsSupportedSplitModel.slice_closed line 78
9. theorem OAI.AffineBernstein.IsSupportedSplitModel.slice_convex line 81
10. theorem OAI.AffineBernstein.IsSupportedSplitModel.slice_compact line 86
11. theorem OAI.AffineBernstein.IsSupportedSplitModel.rescaling_closed line 94
12. theorem OAI.AffineBernstein.IsSupportedSplitModel.rescaling_convex line 97
13. theorem OAI.AffineBernstein.IsSupportedSplitModel.rescaling_one_slice line 107
14. theorem OAI.AffineBernstein.IsSupportedSplitModel.rescaling_cap_bound line 121

    Source comment

    The uniform cap bound has constant 2*T*R for an arbitrary slice outer radius R (including d=0).

    theorem rescaling_cap_bound {ε T R : ℝ} (hε : 0 < ε) (hε2 : 2 * ε ≤ 1)
        (A : Space d ≃L[ℝ] Space d) (hT : 1 ≤ T)
        (hR : A '' thinSlice C ε ⊆ closedBall 0 R)
        {s : Space k} {r : ℝ} {z : Space d}
        (hp : (s, (r, z)) ∈ thinRescaling C ε A)
        (hs : ∀ i, s i ≤ T) (hr : r ≤ T) : ‖z‖ ≤ 2 * T * R := by
    …

    Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.thinSlice, OAI.AffineBernstein.thinRescaling

15. theorem OAI.AffineBernstein.LocalDistanceConverges.mem_of_eventually_mem line 176

    Source comment

    Eventual membership of a fixed point is sufficient for passage to the local limit, including initial rescalings on which it is not yet present.

    theorem LocalDistanceConverges.mem_of_eventually_mem
        {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E]
        {Cj : ℕ → Set E} {C : Set E} (h : LocalDistanceConverges Cj C)
        (hc : IsClosed C) (hne : C.Nonempty) {x : E}
        (hx : ∀ᶠ j in atTop, x ∈ Cj j) : x ∈ C := by
    …

    Mentions: OAI.AffineBernstein.LocalDistanceConverges

16. theorem OAI.AffineBernstein.LocalDistanceConverges.thin_limit line 190

    Source comment

    All the geometric properties of the (k+1)-direction model supplied by the thin-slice limit. The new base is still written (s,r), before reindexing it as R^(k+1). This theorem includes the zero-dimensional transverse endpoint.

    theorem LocalDistanceConverges.thin_limit
        {C C₀ : Set (Space k × (ℝ × Space d))} (hC : IsSupportedSplitModel C)
        {ε : ℕ → ℝ} (hε : ∀ j, 0 < ε j) (hε2 : ∀ j, 2 * ε j ≤ 1)
        (hεt : Tendsto ε atTop (𝓝 0))
        (A : ℕ → (Space d ≃L[ℝ] Space d))
        (h : LocalDistanceConverges (fun j => thinRescaling C (ε j) (A j)) C₀)
        (hclosed : IsClosed C₀) (hconvex : Convex ℝ C₀) (hne : C₀.Nonempty)
        {cj : ℕ → Space d} {c : Space d} (hc : Tendsto cj atTop (𝓝 c)) {R : ℝ}
        (hinner : ∀ j, closedBall (cj j) 1 ⊆ A j '' thinSlice C (ε j))
        (houter : ∀ j, A j '' thinSlice C (ε j) ⊆ closedBall 0 R) :
        (∀ s : Space k, (∀ i, 0 ≤ s i) → ∀ r : ℝ, 0 ≤ r → (s, (r, 0)) ∈ C₀) ∧
        (∀ p ∈ C₀, (∀ i, 0 ≤ p.1 i) ∧ 0 ≤ p.2.1) ∧
    …

    Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.IsSupportedSplitModel, OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.thinRescaling, OAI.AffineBernstein.thinSlice