AdaptedSmoothingAtlas.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Smoothing atlases whose actual centers index prescribed neighborhoods.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_smoothingAtlas_subordinate_locally_one line 16

Source documentation

The finite atlas retains the point indexing of prescribed neighborhoods. Its outer cutoffs equal one on a neighborhood of every weight-support point.

theorem exists_smoothingAtlas_subordinate_locally_one (V : M → Set M)
    (hV : ∀ p, IsOpen (V p)) (hpV : ∀ p, p ∈ V p) :
    ∃ A : SmoothingAtlas M,
      (∀ i : A.centers, tsupport (A.weight i) ⊆ V (i : M)) ∧
      ∀ (i : A.centers) (x : M), x ∈ tsupport (A.weight i) →
        A.outer i =ᶠ[𝓝 x] (fun _ => 1) := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_smoothingAtlas_subordinate line 56
Source documentation
The finite atlas weights are subordinate to their actual centers' prescribed open neighborhoods.
```
theorem exists_smoothingAtlas_subordinate (V : M → Set M)
    (hV : ∀ p, IsOpen (V p)) (hpV : ∀ p, p ∈ V p) :
    ∃ A : SmoothingAtlas M, ∀ i : A.centers, tsupport (A.weight i) ⊆ V (i : M) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas