SmoothingTransition.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The coordinate transitions that transport each localized smoothing error.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transition line 17
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transition_smooth line 19
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.pairWeight line 28
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.pairSupport line 30
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.pairWeight_smooth line 35
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.pairWeight_support line 38
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.pairSupport_compact line 41
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.pairSupport_transition line 46
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localize_restore line 60
Source documentation
Writing a restored component in another chart is multiplication by a fixed smooth weight followed by the fixed transition.
```
lemma localize_restore (i j : A.centers) (h : Base → V) :
    localize (i : M) (A.weight i) (restore (j : M) (A.outer j) h) =
      fun x => A.pairWeight i j x • h (transition (i : M) (j : M) x) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.restore, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transition
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.pair_weighted_bound line 76
Source documentation
Each overlap transports a global weighted bound with fixed constants.
```
theorem pair_weighted_bound (i j : A.centers) (m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (h : Base → V) (s C : ℝ),
      0 < s → s ≤ 1 → 0 ≤ C → ContDiff ℝ ∞ h → WeightedBound Set.univ s m C h →
      WeightedBound Set.univ s m (D * C)
        (localize (i : M) (A.weight i) (restore (j : M) (A.outer j) h)) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.WeightedBound, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.restore