OAI/Geometry/SurfaceImmersion/Atlas/QualitativePhaseTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Good phase directions pass between surface coordinate charts.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.Good.tensor_ne_zero line 12
  2. theorem OAI.ClosedSurfaceR4.actual_phase_good_at line 23

    Source documentation

    The quantitative overlap theorem implies the qualitative phase condition, with no externally supplied determinant or size constants.

    theorem actual_phase_good_at {F : M → Space}
    (hF : ContMDiff planeModel spaceModel ∞ F) (q p : M) {a : M}
    (hap : a ∈ (coordinateChart p).source) (haq : a ∈ (coordinateChart q).source)
    (ξ : Base)
    (hD : NormalFrame.gramDet
      (coordDeriv dx (coordinateMap F q) (coordinateChart q a))
      (coordDeriv dy (coordinateMap F q) (coordinateChart q a)) ≠ 0)
    (hgood : Good (realSecondTensor (coordinateMap F q) (coordinateChart q a)) ξ) :
    Good (realSecondTensor (coordinateMap F p) (coordinateChart p a))
      (atlasPhaseCovector q p ξ a) := by
…

    Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.NormalFrame.gramDet, OAI.ClosedSurfaceR4.coordinateMap, OAI.ClosedSurfaceR4.atlasPhaseCovector