NormalizedRadialError.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative radial smallness in normalized harmonic coordinates

theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.gradient_le line 18
Source documentation
The cutoff gradient bound follows from its actual Lipschitz representative.
```
theorem GoodLaplacianCutoff.gradient_le {p : X} {r C : ℝ} (hr : 0 < r) (hC : 0 ≤ C)
    (χ : GoodLaplacianCutoff μ hQ p r C) :
    ∀ᵐ x ∂μ, localGamma μ hQ χ.sobolev χ.sobolev x ≤ (C / r) ^ 2 := by
…
```
Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.localGamma
theorem OAI.RegularPointCoordinates.gram_integral_bound line 30
theorem OAI.RegularPointCoordinates.gram_column_integral_bound line 45

theorem OAI.RegularPointCoordinates.normalized_coordinate_radial_error line 67

Source documentation

The manuscript's qualitative radial estimate, with an explicit modulus: metric error epsilon and first-order Gram error epsilon give a squared radial error at most a dimensional constant times epsilon*r^2*volume. Global boundedness may be obtained by boundedLocalVersion; it preserves all local quantities in this statement.

theorem normalized_coordinate_radial_error {n : ℕ} {p : X} {r ε Cχ Q : ℝ}
    (hr : 0 < r) (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (hCχ : 0 ≤ Cχ) (hQb : 0 ≤ Q)
    (u : Fin n → SobolevSpace μ hQ) (v : X → Euclidean n)
    (hfirst : FirstOrderSplittingOn μ hQ p (4 * r) ε u v)
    (hv : v p = 0)
    (hmetric : IsPointedApproximation p 0 r 4 ε (fun x => r⁻¹ • v x))
    (hub : ∀ j, ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ (u j) x| ≤ 5 * r)
    (q : SobolevSpace μ hQ)
    (hq : SobolevSpace.toLp μ hQ q =ᵐ[μ.restrict (ball p (4 * r))] fun x => dist p x ^ 2 / 2)
    (hqbound : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ q x| ≤ Q)
    (heik : ∀ᵐ x ∂μ.restrict (ball p (4 * r)), localGamma μ hQ q q x = 2 * SobolevSpace.toLp μ hQ q x)
    (χ : GoodLaplacianCutoff μ hQ p r Cχ)
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.IsPointedApproximation, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.GoodLaplacianCutoff