OAI/Geometry/SurfaceImmersion/Atlas/PhaseSupportCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transfer compact phase supports between the two plane coordinate conventions.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.jetSupport line 11
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.modeSupport_jetSupport line 14
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.onModeSupport line 29

    Source documentation

    The function is unchanged; only its compact-support index is transferred.

    def onModeSupport (K : Compacts SmallModes.Base) (f : SupportedField (F := E) K) :
…

    Mentions: OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.JetPolynomial.SupportedField

  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.onModeSupport_apply line 33
  5. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.onModeSupportLM line 36
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.onModeSupport_seminorm line 42