PositiveDistancePoisson.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual Poisson replacement of the positive squared distance

theorem OAI.RegularPointCoordinates.positive_distance_poisson_estimates line 21

Source documentation

The torsion constant is chosen uniformly before the ball and source. All replacement and error conclusions concern the constructed squared distance, not an abstract radial test function.

theorem positive_distance_poisson_estimates {d C V : ℝ} (hd : 1 < d)
    (hC : 0 ≤ C) (hV : 0 ≤ V) :
    ∃ H : ℝ, 0 < H ∧ ∀ (p : X) (r R D : ℝ) (hR : 0 ≤ R),
    ∀ χ : GoodLaplacianCutoff μ hQ p R D,
      0 < r → r ≤ R → μ (ball p r) ≠ ∞ → μ.real (ball p r) ≤ V →
      ∀ 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 * energyForm μ hQ φ.val φ.val) →
      (∀ᵐ x ∂μ.restrict (ball p R),
…

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