OAI/Geometry/RCD/Sobolev/PoissonPairDefect.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full two-center source in the common Poisson defect units

  1. theorem OAI.RegularPointCoordinates.poisson_pair_defect_bound line 17

    Source documentation

    Both positive source masses and the curvature remainder are controlled by the sum of the two original normalized defects.

    theorem poisson_pair_defect_bound {n : ℕ} {κ r0 : ℝ} {p₁ p₂ : X}
    (S₁ : DyadicDistanceSources μ hQ n κ p₁ r0)
    (S₂ : DyadicDistanceSources μ hQ n κ p₂ r0) (i : ℕ)
    {C A : ℝ} (hκ : 0 ≤ κ) (hC : 0 ≤ C) :
    let s := distanceSourceRadius r0 i
…

    Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.distanceSourceRadius