CovectorRadialSmallness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Qualitative radial smallness in every constant covector

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.local_covector_radial_error line 19

Source documentation

The same actual radial smallness holds in every direction, with the squared covector norm and only a dimensional loss.

theorem DyadicDistanceReplacements.local_covector_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)))) (b : Euclidean 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

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.local_covector_fit_smallness line 53

Source documentation

The actual dimensionless affine fit inherits the qualitative bound.

theorem DyadicDistanceReplacements.local_covector_fit_smallness {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)))) (b : Euclidean n) :
    let r := distanceSourceRadius r0 i / 64
…