OAI/Analysis/AffineBernstein/ConvexLocalLimits.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.LocalDistanceConverges line 17

   Source comment

   The local distance-function topology used in geometry.tex:70–101. Sets are separately required to be nonempty and closed when those properties enter.

   def LocalDistanceConverges (Cj : ℕ → Set E) (C : Set E) : Prop :=
   …

2. theorem OAI.AffineBernstein.LocalDistanceConverges.pointwise line 21
3. theorem OAI.AffineBernstein.LocalDistanceConverges.exists_approximating line 30
4. theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_disjoint_compact line 42
5. theorem OAI.AffineBernstein.LocalDistanceConverges.mem_of_tendsto line 64
6. theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_bounded_caps line 78

   Source comment

   Uniform cap compactness, geometry.tex:104–125. The proof traps a chord on a fixed compact sphere, rather than choosing escaping directions.

   theorem LocalDistanceConverges.eventually_bounded_caps
       {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 : ℝ)
       (hbounded : Bornology.IsBounded (C ∩ {x | ell x ≤ b}))
       {q : E} (hq : q ∈ C) (hqb : ell q < b) :
       ∃ R > 0, ∀ᶠ j in atTop, Cj j ∩ {x | ell x ≤ b} ⊆ Metric.ball 0 R := by
   …

   Mentions: OAI.AffineBernstein.LocalDistanceConverges

7. theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_infDist_cap_lt_at line 126

   Source comment

   A point on the top of a limit cap is approximated from strictly below its top by contracting toward a fixed strict point.

   theorem LocalDistanceConverges.eventually_infDist_cap_lt_at
       {Cj : ℕ → Set E} {C : Set E} (h : LocalDistanceConverges Cj C)
       (hclj : ∀ j, IsClosed (Cj j)) (hnej : ∀ j, (Cj j).Nonempty)
       (hcv : Convex ℝ C) (ell : E →L[ℝ] ℝ) {b : ℝ}
       {q : E} (hq : q ∈ C) (hqb : ell q < b)
       {x : E} (hx : x ∈ C) (hxb : ell x ≤ b) {ε : ℝ} (hε : 0 < ε) :
       ∀ᶠ j in atTop, infDist x (Cj j ∩ {y | ell y ≤ b}) < ε := by
   …

   Mentions: OAI.AffineBernstein.LocalDistanceConverges

8. theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_infDist_cap_lt_uniform line 161

   Source comment

   Reverse Hausdorff inclusion for a compact cap.

   theorem LocalDistanceConverges.eventually_infDist_cap_lt_uniform
       {Cj : ℕ → Set E} {C : Set E} (h : LocalDistanceConverges Cj C)
       (hclj : ∀ j, IsClosed (Cj j)) (hnej : ∀ j, (Cj j).Nonempty)
       (hcv : Convex ℝ C) (ell : E →L[ℝ] ℝ) {b : ℝ}
       (hcap : IsCompact (C ∩ {x | ell x ≤ b}))
       {q : E} (hq : q ∈ C) (hqb : ell q < b) {ε : ℝ} (hε : 0 < ε) :
       ∀ᶠ j in atTop, ∀ x ∈ C ∩ {y | ell y ≤ b},
         infDist x (Cj j ∩ {y | ell y ≤ b}) < ε := by
   …

   Mentions: OAI.AffineBernstein.LocalDistanceConverges

9. theorem OAI.AffineBernstein.LocalDistanceConverges.tendsto_hausdorffDist_caps line 182

   Source comment

   Full Hausdorff cap convergence, geometry.tex:104–125, with no asserted smoothness of the limiting boundary.

   theorem LocalDistanceConverges.tendsto_hausdorffDist_caps
       {Cj : ℕ → Set E} {C : Set E} (h : LocalDistanceConverges Cj C)
       (hcl : IsClosed C) (hcv : Convex ℝ C)
       (hclj : ∀ j, IsClosed (Cj j)) (hcvj : ∀ j, Convex ℝ (Cj j))
       (hnej : ∀ j, (Cj j).Nonempty) (ell : E →L[ℝ] ℝ) {b : ℝ}
       (hcap : IsCompact (C ∩ {x | ell x ≤ b}))
       {q : E} (hq : q ∈ C) (hqb : ell q < b) :
       Tendsto (fun j => hausdorffDist (Cj j ∩ {x | ell x ≤ b})
         (C ∩ {x | ell x ≤ b})) atTop (𝓝 0) := by
   …

   Mentions: OAI.AffineBernstein.LocalDistanceConverges

10. theorem OAI.AffineBernstein.isCompact_nonneg_unitLipschitz line 224
11. theorem OAI.AffineBernstein.exists_distance_function_subsequence line 258
12. theorem OAI.AffineBernstein.distance_function_limit_representation line 272
13. theorem OAI.AffineBernstein.exists_convex_local_limit line 311

    Source comment

    Local compactness of nonempty closed convex sets meeting a fixed bounded set, the extraction used in geometry.tex:70–101. The topology and the limit are literal sets and Euclidean distance functions.

    theorem exists_convex_local_limit {Cj : ℕ → Set E}
        (hcl : ∀ j, IsClosed (Cj j)) (hcv : ∀ j, Convex ℝ (Cj j))
        (hne : ∀ j, (Cj j).Nonempty) {R : ℝ}
        (hbound : ∀ j, infDist (0 : E) (Cj j) ≤ R) :
        ∃ (C : Set E) (φ : ℕ → ℕ), StrictMono φ ∧ IsClosed C ∧ C.Nonempty ∧
          Convex ℝ C ∧ LocalDistanceConverges (fun j => Cj (φ j)) C := by
    …

    Mentions: OAI.AffineBernstein.LocalDistanceConverges