OAI/Geometry/RCD/Sobolev/PoissonMassUnits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full Poisson mass budget in the original normalized source units

  1. theorem OAI.RegularPointCoordinates.poisson_pair_mass_units line 17

    Source documentation

    Source and curvature terms are paid by the same original normalized Poisson defect, with a constant independent of the dyadic radius.

    theorem poisson_pair_mass_units {n : ℕ} {κ root q A : ℝ} {p z : X}
    (S1 : DyadicDistanceSources μ hQ n κ p root)
    (S2 : DyadicDistanceSources μ hQ n κ z root)
    (hκ : 0 ≤ κ) (hq : 0 ≤ q) (i : ℕ) :
    let s := distanceSourceRadius root i
…

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