OAI/Algebra/GroupRing/GeneralPosition.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GroupRingTopology.Attachment.radialRetraction line 16
2. lemma OAI.GroupRingTopology.Attachment.radialRetraction_base line 20
3. lemma OAI.GroupRingTopology.Attachment.radialRetraction_cell line 21
4. def OAI.GroupRingTopology.Attachment.radialPaths line 25
5. lemma OAI.GroupRingTopology.Attachment.radialPaths_base line 35
6. lemma OAI.GroupRingTopology.Attachment.radialPaths_cell line 37
7. def OAI.GroupRingTopology.Attachment.puncturedInclusion line 43
8. def OAI.GroupRingTopology.Attachment.radialEnd line 44
9. def OAI.GroupRingTopology.Attachment.radialHomotopy line 47

   Source documentation

   The punctured attachment deformation-retracts to the original space.

   def radialHomotopy : (puncturedInclusion a).Homotopy (radialEnd a) where
   …

   Mentions: OAI.GroupRingTopology.Attachment.puncturedInclusion, OAI.GroupRingTopology.Attachment.radialEnd

10. lemma OAI.GroupRingTopology.Attachment.radialHomotopy_base line 62
11. lemma OAI.GroupRingTopology.Attachment.cell_eq_openCell_iff line 65
12. lemma OAI.GroupRingTopology.Attachment.openCell_disjoint line 88
13. lemma OAI.GroupRingTopology.Attachment.openCell_selection_closed line 94
14. lemma OAI.GroupRingTopology.Attachment.compact_finitely_many_openCells line 119

    Source documentation

    The weak adjunction topology prevents compact sets from meeting infinitely many of the new open cells. No local-finiteness assumption is needed.

    lemma compact_finitely_many_openCells {K : Set (Space a)} (hK : IsCompact K) :
        {i : ι | (K ∩ Set.range (openCell a i)).Nonempty}.Finite := by
    …

    Mentions: OAI.GroupRingTopology.Attachment.Space, OAI.GroupRingTopology.Attachment.openCell

15. def OAI.GroupRingTopology.Cellular.patchFun line 150
16. lemma OAI.GroupRingTopology.Cellular.patchFun_on line 154
17. lemma OAI.GroupRingTopology.Cellular.patchFun_off line 157
18. lemma OAI.GroupRingTopology.Cellular.continuous_patchFun line 160
19. def OAI.GroupRingTopology.Cellular.patch line 180
20. lemma OAI.GroupRingTopology.Cellular.patch_on line 184
21. lemma OAI.GroupRingTopology.Cellular.patch_off line 188
22. def OAI.GroupRingTopology.Cellular.patchHomotopy line 194

    Source documentation

    Homotopies on a closed subset glue to the stationary homotopy outside it, provided they are stationary on the frontier.

    def patchHomotopy {A : Set X} (hA : IsClosed A) (f : C(X,Y)) (g : C(A,Y))
        (H : (f.restrict A).Homotopy g)
        (hboundary : ∀ (t : unitInterval) (x : A), (x:X) ∈ frontier A → H (t,x) = f x) :
        f.Homotopy (patch hA f g (fun x hx => by simpa using hboundary 1 x hx)) := by
    …

    Mentions: OAI.GroupRingTopology.Cellular.patch

23. lemma OAI.GroupRingTopology.GeneralPosition.lipschitz_mul line 230
24. def OAI.GroupRingTopology.GeneralPosition.lipschitzAlgebra line 251
25. lemma OAI.GroupRingTopology.GeneralPosition.lipschitzAlgebra_separates line 259
26. lemma OAI.GroupRingTopology.GeneralPosition.exists_lipschitz_approximation line 266

    Source documentation

    Uniform Lipschitz approximation on an arbitrary compact metric space.

    lemma exists_lipschitz_approximation (f : C(K,ℝ)) {ε : ℝ} (hε : 0 < ε) :
        ∃ g : C(K,ℝ), (∃ L, LipschitzWith L g) ∧ ∀ x, ‖g x-f x‖ < ε := by
    …

27. lemma OAI.GroupRingTopology.GeneralPosition.exists_lipschitz_vector_approximation line 279
28. lemma OAI.GroupRingTopology.GeneralPosition.exists_missing_point line 302

    Source documentation

    A Lipschitz image of smaller Hausdorff dimension misses points in every positive-radius ball of Euclidean target space.

    lemma exists_missing_point {n : ℕ} {g : K → Fin n → ℝ} {L : ℝ≥0}
        (hg : LipschitzWith L g) (hdim : dimH (Set.univ : Set K) < n)
        (c : Fin n → ℝ) {r : ℝ} (hr : 0 < r) :
        ∃ a ∈ Metric.ball c r, a ∉ Set.range g := by
    …

29. lemma OAI.GroupRingTopology.GeneralPosition.exists_nonzero_approximation line 313

    Source documentation

    Every map from a compact metric space of dimension less than n can be uniformly approximated by a map into punctured ℝ^n.

    lemma exists_nonzero_approximation {n : ℕ} (f : C(K,Fin n → ℝ))
        (hdim : dimH (Set.univ : Set K) < n) {ε : ℝ} (hε : 0 < ε) :
        ∃ g : C(K,Fin n → ℝ), (∀ x, g x ≠ 0) ∧ ∀ x, ‖g x-f x‖ < ε := by
    …

30. def OAI.GroupRingTopology.GeneralPosition.cutoff line 337
31. lemma OAI.GroupRingTopology.GeneralPosition.cutoff_nonneg line 338
32. lemma OAI.GroupRingTopology.GeneralPosition.cutoff_le_one line 339
33. lemma OAI.GroupRingTopology.GeneralPosition.cutoff_small line 340
34. lemma OAI.GroupRingTopology.GeneralPosition.cutoff_large line 345
35. lemma OAI.GroupRingTopology.GeneralPosition.continuous_cutoff line 348
36. lemma OAI.GroupRingTopology.GeneralPosition.exists_relative_nonzero_approximation line 352

    Source documentation

    General position relative to the region already far from the origin.

    lemma exists_relative_nonzero_approximation {n : ℕ} (f : C(K,Fin n → ℝ))
        (hdim : dimH (Set.univ : Set K) < n) {δ : ℝ} (hδ : 0 < δ) :
        ∃ g : C(K,Fin n → ℝ), (∀ x, g x ≠ 0) ∧
          (∀ x, 2*δ ≤ ‖f x‖ → g x = f x) ∧ ∀ x, ‖g x-f x‖ < δ/2 := by
    …

37. lemma OAI.GroupRingTopology.GeneralPosition.relative_interpolation_bound line 381

    Source documentation

    The straight-line homotopy from the original to the perturbed map stays inside any disk of radius 4δ, and is stationary outside the core of radius 2δ.

    lemma relative_interpolation_bound {n : ℕ} {f g : K → Fin n → ℝ} {δ : ℝ} (hδ : 0 < δ)
        (hfix : ∀ x, 2*δ ≤ ‖f x‖ → g x = f x)
        (hdist : ∀ x, ‖g x-f x‖ < δ/2)
        (x : K) (hx : ‖f x‖ ≤ 4*δ) (t : unitInterval) :
        ‖f x+(t:ℝ) • (g x-f x)‖ ≤ 4*δ := by
    …