OAI/Geometry/SurfaceImmersion/Correction/NormalizedPerturbedMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normalization of the actual corrected metric mean by the seed amplitude.

  1. def OAI.ClosedSurfaceR4.RealModes.normalizedPerturbedMean line 15
  2. lemma OAI.ClosedSurfaceR4.RealModes.perturbed_seed_mean_identity line 23
  3. theorem OAI.ClosedSurfaceR4.RealModes.normalizedPerturbedMean_bound line 38

    Source documentation

    The normalized metric mean retains one small factor for every fixed output order, with a finite explicitly identified input order.

    theorem normalizedPerturbedMean_bound (δ τ : ℝ) (hF : ContDiff ℝ ∞ F) (h : RealModeDomain F U)
    (K : Compacts Base) (hKU : (K : Set Base) ⊆ U) {s : ℝ≥0} {ε : ℝ} {p L : ℕ}
    (hδ : 0 < δ) (hτ : 0 < τ) (hs : 0 < (s : ℝ)) (hτs : τ ≤ s) (hs1 : s ≤ 1) (hε : 0 ≤ ε)
    (hsmall : τ / s + ε / τ ^ p ≤ 1)
    (B D : ℕ → ℝ) (hB : ∀ m, 0 ≤ B m) (hD : ∀ m, 0 ≤ D m)
    (hc : ∀ m, ReconstructionCoefficientBound (fun p => complexify (F p)) U s (m + 1) (B m))
    (R : SupportedField (F := Ambient 4) K →ₗ[ℝ] SupportedField (F := Fin 3 → ℂ) K)
…

    Mentions: OAI.ClosedSurfaceR4.RealModes.RealModeDomain, OAI.ClosedSurfaceR4.RealModes.complexify