ActualPoissonMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Full shifted mass of an actual dyadic Poisson replacement

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.local_density_error line 19
Source documentation
The energy-density error is valid on each common interior ball, with the actual squared-distance datum on its right side.
```
theorem DyadicDistanceReplacements.local_density_error
    {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
    (z : X) {R : ℝ} (hroom : R + dist z p ≤ distanceSourceRadius r0 i) :
    let s := distanceSourceRadius r0 i
…
```
Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius
theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.local_energy_error line 60
Source documentation
The same global Poisson energy error controls every local testing ball. It concerns the actual datum selected by the replacement family.
```
theorem DyadicDistanceReplacements.local_energy_error
    {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ) (Ω : Set X) :
    let s := distanceSourceRadius r0 i
…
```
Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.shifted_mass_le line 78

Source documentation

The cutoff calculation for an actual replacement retains the full shifted measure. Both its source and curvature errors have the correct length units; no mass estimate is assumed.

theorem DyadicDistanceReplacements.shifted_mass_le
    {n : ℕ} {κ r0 B J C A Cχ : ℝ} {p z : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
    (hκ : 0 ≤ κ) (hCχ : 0 ≤ Cχ)
    (hroom : dist z p ≤ distanceSourceRadius r0 i / 4)
    {U : E →L[ℝ] SobolevSpace μ hQ} {M : PositiveBilinearMeasure X E}
    {L : ℝ≥0} {v : E} (ell : E →ₗ[ℝ] ℝ)
    [IsFiniteMeasure (μ.restrict (ball z (2 * (distanceSourceRadius r0 i / 32))))]
    (G : LocalHarmonicEnergy μ hQ U M κ z (distanceSourceRadius r0 i / 32) L v)
    (hv : U v = T.replacement i)
    (hell : ell v = (n : ℝ) + κ * (4 * distanceSourceRadius r0 i) ^ 2)
…

Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.LocalHarmonicEnergy