OAI/Geometry/SurfaceImmersion/Correction/LinearMeanReconstruction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual leading mean reconstructs the input tensor on an inner domain where the common cutoff is one. Outside this domain its exact formula retains the cutoff square.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.supportedPhaseCutoff line 16

    Source documentation

    The supported phase-chart cutoff with its inverse frequency factor.

    def supportedPhaseCutoff {K : Compacts SmallModes.Base}
    (χ : SupportedField (F := ℝ) K)
…

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

  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.supportedPhaseCutoff_eval_source line 23
  3. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.linear_mean_reconstruction_on line 33