CircularSmoothingAtlas.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

A finite smoothing atlas whose positive loci are actual coordinate disks. The cutoffs are flat circular functions, not arbitrary subordinate bumps.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion line 19
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateDisk line 22
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularDiskClosure line 26
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump line 29
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion_compact line 33
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump_nonneg line 41
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump_pos_iff line 49
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateDisk_open line 61
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.mem_circularCoordinateDisk line 68
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularDiskClosure_compact line 80
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularDiskClosure_source line 87
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump_smooth_support line 93
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_circularCoordinateDisk_subordinate line 110
Source documentation
The disks can be chosen inside any given neighborhood of their centers.
```
lemma exists_circularCoordinateDisk_subordinate (p : M) {V : Set M}
    (hV : IsOpen V) (hpV : p ∈ V) :
    ∃ r : ℝ, 0 < r ∧
      circularCoordinateRegion p r ⊆ (coordinateChart p).target ∧
      circularDiskClosure p r ⊆ V := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularDiskClosure

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_finite_circular_cutoffs line 138

Source documentation

A finite collection of actual circular coordinate disks covers the surface. Its flat cutoffs are smooth and subordinate to the given cover.

theorem exists_finite_circular_cutoffs (V : M → Set M)
    (hV : ∀ p, IsOpen (V p)) (hpV : ∀ p, p ∈ V p) :
    ∃ (t : Finset M) (r : t → ℝ),
      (∀ i : t, 0 < r i) ∧
      (∀ i : t, circularCoordinateRegion (i : M) (r i) ⊆ (coordinateChart (i : M)).target) ∧
      (∀ i : t, circularDiskClosure (i : M) (r i) ⊆ V i) ∧
      (∀ x : M, ∃ i : t, x ∈ circularCoordinateDisk (i : M) (r i)) ∧
      (∀ i : t, ContMDiff planeModel 𝓘(ℝ) ∞ (circularManifoldBump (i : M) (r i))) ∧
      (∀ i : t, tsupport (circularManifoldBump (i : M) (r i)) ⊆ V i) := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularDiskClosure, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateDisk, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalize_finite_positive_cutoffs line 165

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_circular_smoothingAtlas line 206

Source documentation

A finite atlas with circular positive loci. Outer cutoffs are identically one near their supports, and all data stay inside the prescribed neighborhoods.

theorem exists_circular_smoothingAtlas (V : M → Set M)
    (hV : ∀ p, IsOpen (V p)) (hpV : ∀ p, p ∈ V p) :
    ∃ (A : SmoothingAtlas M) (r : A.centers → ℝ),
      (∀ i : A.centers, 0 < r i) ∧
      (∀ i : A.centers, circularCoordinateRegion (i : M) (r i) ⊆ (coordinateChart (i : M)).target) ∧
      (∀ i : A.centers, circularDiskClosure (i : M) (r i) ⊆ V i) ∧
      (∀ i x, 0 ≤ A.weight i x) ∧
      (∀ i x, 0 < A.weight i x ↔ x ∈ circularCoordinateDisk (i : M) (r i)) ∧
      (∀ i, tsupport (A.weight i) ⊆ V i) ∧
      ∀ i x, x ∈ tsupport (A.weight i) → A.outer i =ᶠ[𝓝 x] (fun _ => 1) := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularDiskClosure, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateDisk