NormalizedDistancePoisson.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform scale-correct Poisson replacement of squared distance

theorem OAI.RegularPointCoordinates.normalized_distance_poisson_estimates line 21

Source documentation

One torsion constant works for every center, radius and full positive source. The height, gradient and energy-density errors have the exact radius factors needed by the dyadic radial argument.

theorem normalized_distance_poisson_estimates {d C : ℝ} (hd : 1 < d) (hC : 0 < C) :
    ∃ H : ℝ, 0 < H ∧ ∀ (p : X) (r R D : ℝ) (hR : 0 ≤ R),
    ∀ χ : GoodLaplacianCutoff μ hQ p R D,
      0 < r → r ≤ R → μ (ball p r) ≠ ∞ → 0 < μ.real (ball p r) →
      ∀ P : ℝ, 0 ≤ P →
      (∀ φ : SobolevSpace.dirichlet μ hQ (ball p r),
        ‖SobolevSpace.toLp μ hQ φ.val‖ ^ 2 ≤ P * energyForm μ hQ φ.val φ.val) →
      (∀ φ : SobolevSpace.dirichlet μ hQ (ball p r),
        (∫ x in ball p r, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
          (C * r ^ 2 * (μ.real (ball p r)) ^ (1 / d - 1)) * energyForm μ hQ φ.val φ.val) →
      (∀ᵐ x ∂μ.restrict (ball p R),
        localGamma μ hQ (inwardSobolev μ hQ p R) (inwardSobolev μ hQ p R) x = 1) →
…

Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.inwardSobolev