OAI/Geometry/SurfaceImmersion/Correction/ChartedMeanFamilyData.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A finite charted phase family with its actual solvers and amplitudes, packaged for assembling different coordinate patches on one surface.

  1. structure OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanFamilyData line 13
  2. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanFamilyData.mean line 26
  3. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanFamilyData.Fits line 30
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanFamilyData.mean_smooth line 33
  5. def OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanFamilyData.quadraticMean line 38

    Source documentation

    The actual zero-phase tensor of the finite free family in original coordinates.

    def quadraticMean (d : ChartedMeanFamilyData P ε τ s r ρ R reference)
    (hρ : 0 < ρ) (δ : ℝ) (q : ℕ) (f : SmallModes.Base → Tensor) : SmallModes.Base → Tensor :=
…

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.ChartedMeanFamilyData, OAI.ClosedSurfaceR4.SmallModes.Base

  6. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.uniform_chartedFamilyData_majorants line 45