OAI/Geometry/SurfaceImmersion/Atlas/SupportedCoordinateChange.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Isometric linear coordinate changes preserve the supported weighted seminorms exactly.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.weightedBound_comp_isometry line 17
  2. def OAI.ClosedSurfaceR4.JetPolynomial.pushSupported line 30
  3. def OAI.ClosedSurfaceR4.JetPolynomial.pullSupported line 37
  4. def OAI.ClosedSurfaceR4.JetPolynomial.supportedCoordinateEquiv line 44
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.supportedCoordinateEquiv_norm line 67
  6. def OAI.ClosedSurfaceR4.JetPolynomial.planeCoordinateIsometry line 84

    Source documentation

    The two coordinate conventions used by the geometric and jet formulas.

    def planeCoordinateIsometry : (Fin 2 → ℝ) ≃ₗᵢ[ℝ] ℝ × ℝ where
…