LocalRadialSmallness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Qualitative radial smallness for the actual dyadic distance datum

theorem OAI.RegularPointCoordinates.local_normalized_radial_error line 20

Source documentation

The global extensions of the original harmonic coordinates need not be bounded: clipping preserves their actual local radial error.

theorem local_normalized_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))
    (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χ)
    (hvol : 0 < μ.real (ball p (4 * r))) (j : Fin n) :
…

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

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.local_radial_error line 54

Source documentation

The same canonical distance datum used for the Poisson corrections satisfies the local qualitative estimate. Its value and eikonal properties are derived from the actual source family.

theorem DyadicDistanceReplacements.local_radial_error {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
    {ε Cχ : ℝ} (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (hCχ : 0 ≤ Cχ)
    (u : Fin n → SobolevSpace μ hQ) (v : X → Euclidean n)
    (hfirst : FirstOrderSplittingOn μ hQ p (4 * (distanceSourceRadius r0 i / 64)) ε u v)
    (hv : v p = 0)
    (hmetric : IsPointedApproximation p 0 (distanceSourceRadius r0 i / 64) 4 ε
      (fun x => (distanceSourceRadius r0 i / 64)⁻¹ • v x))
    (χ : GoodLaplacianCutoff μ hQ p (distanceSourceRadius r0 i / 64) Cχ)
    (hvol : 0 < μ.real (ball p (4 * (distanceSourceRadius r0 i / 64)))) (j : Fin n) :
    let r := distanceSourceRadius r0 i / 64
…

Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.IsPointedApproximation, OAI.RegularPointCoordinates.GoodLaplacianCutoff