OAI/Geometry/SurfaceImmersion/Correction/SupportedModeOperators.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The geometric finite differential parametrix as a linear map on actual compactly supported smooth fields.

  1. lemma OAI.ClosedSurfaceR4.SmallModes.tsupport_conjugatedD line 19
  2. def OAI.ClosedSurfaceR4.SmallModes.conjugatedDLM line 27
  3. lemma OAI.ClosedSurfaceR4.SmallModes.conjugatedDLM_apply line 49
  4. def OAI.ClosedSurfaceR4.SmallModes.forcedMode line 54

    Source documentation

    All correction depths preserve the same compact support.

    def forcedMode (τ : ℝ) (h : ModeDomain G U) (K : Compacts Base)
    (hKU : (K : Set Base) ⊆ U) (q : ℕ) (f : SupportedField (F := Fin 3 → ℂ) K) :
…

    Mentions: OAI.ClosedSurfaceR4.SmallModes.ModeDomain, OAI.ClosedSurfaceR4.SmallModes.Base

  5. lemma OAI.ClosedSurfaceR4.SmallModes.forcedMode_apply line 63
  6. lemma OAI.ClosedSurfaceR4.SmallModes.forcedMode_sub line 67
  7. def OAI.ClosedSurfaceR4.SmallModes.forcedModeLM line 88
  8. lemma OAI.ClosedSurfaceR4.SmallModes.forcedModeLM_apply line 111