EuclideanAffineImprovement.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The strict Euclidean candidate for harmonic affine improvement

theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.affine_candidate line 15

Source documentation

The Taylor coefficients give a normalized local L² affine candidate.

theorem EuclideanHarmonicModel.affine_candidate {n : ℕ} {S ρ C : ℝ}
    (w : EuclideanHarmonicModel n S) (_hS : 0 < S) (hρ : 0 < ρ)
    (hρS : ρ ≤ S / 2) (hC : 0 ≤ C)
    (hbound : ∀ z ∈ ball (0 : Euclidean n) (S / 2),
      ‖fderiv ℝ (fderiv ℝ w.value) z‖ ≤ C) :
    ∃ (c : ℝ) (v : Euclidean n),
      ‖∑ i, affineErrorCoefficients c (fun j => v j) i •
        w.moments (show ρ ≤ S by linarith) i‖ ≤ C * ρ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.EuclideanHarmonicModel, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.affineErrorCoefficients