OAI/Geometry/SurfaceImmersion/Atlas/CrossAtlasJetRelation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Localized jets can be transported between independently chosen atlases.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_transitionScalar line 19
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_transitionScalar_smoothOn line 22
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_vectorChartRead_transition line 29
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_vectorChartRead_transition_eventually line 43
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_jetChartMap_transition line 54
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_jetChartMap_transition_eventually line 63
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_weighted_jetChartMap_transition line 75

    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 cross_weighted_jetChartMap_transition (i : A.centers) (j : B.centers) (G : M → Space)
    {x : Base} (hx : x ∈ (transition (i : M) (j : M)).source) :
    (A.weight i ((chart (i : M)).symm x)) ^ 2 •
        B.jetChartMap j G (transition (i : M) (j : M) x) =
      (A.weight i ((chart (i : M)).symm x)) ^ 2 •
        (A.cross_transitionScalar B i j x • A.jetChartMap i G x) := by
…

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

  8. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_compact_jetChartMap_transition line 89

    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 cross_compact_jetChartMap_transition (i : A.centers) (j : B.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.cross_transitionScalar B i j) U ∧
        (∀ (G : M → Space) (x : Base), x ∈ U →
          (A.weight i ((chart (i : M)).symm x)) ^ 2 •
              B.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 => B.jetChartMap j G (transition (i : M) (j : M) y)) =ᶠ[𝓝 x]
…

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