AtlasJetCoordinateRelation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual localized atlas maps on a coordinate overlap. The transition scalar is the square of the outer cutoff. A nonzero partition weight gives the needed equality of germs without any extra plateau hypothesis.

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.transitionScalar line 23
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.transitionScalar_smoothOn line 26
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.outer_eventually_one_of_weight_ne_zero line 31
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorChartRead_transition line 41
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorChartRead_transition_eventually line 55
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.jetChartMap_transition line 66
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.jetChartMap_transition_eventually line 75
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.weighted_jetChartMap_transition line 87
Source documentation
The partition weight removes the boundary case where a germ equal to one is unavailable. This identity holds on the whole transition domain.
```
lemma weighted_jetChartMap_transition (i j : A.centers) (G : M → Space)
    {x : Base} (hx : x ∈ (transition (i : M) (j : M)).source) :
    (A.weight i ((chart (i : M)).symm x)) ^ 2 •
        A.jetChartMap j G (transition (i : M) (j : M) x) =
      (A.weight i ((chart (i : M)).symm x)) ^ 2 •
        (A.transitionScalar i j x • A.jetChartMap i G x) := by
…
```
Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transition, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.compact_jetChartMap_transition line 101

Source documentation

A fixed compact overlap has a globally smooth transition scalar. It is chosen before the map, and retains both the weighted identity everywhere and the unweighted identity of germs on the nonzero weight locus.

theorem compact_jetChartMap_transition (i j : A.centers) {K : Set Base}
    (hK : IsCompact K) (hKe : K ⊆ (transition (i : M) (j : M)).source) :
    ∃ U : Set Base, IsOpen U ∧ K ⊆ U ∧
      U ⊆ (transition (i : M) (j : M)).source ∧
      ∃ a : Base → ℝ, ContDiff ℝ ∞ a ∧ EqOn a (A.transitionScalar i j) U ∧
        (∀ (G : M → Space) (x : Base), x ∈ U →
          (A.weight i ((chart (i : M)).symm x)) ^ 2 •
              A.jetChartMap j G (transition (i : M) (j : M) x) =
            (A.weight i ((chart (i : M)).symm x)) ^ 2 • (a x • A.jetChartMap i G x)) ∧
        (∀ (G : M → Space) (x : Base), x ∈ U →
          A.weight i ((chart (i : M)).symm x) ≠ 0 →
            (fun y => A.jetChartMap j G (transition (i : M) (j : M) y)) =ᶠ[𝓝 x]
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.transition, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart