OAI/Geometry/RCD/Sobolev/ActualPoissonDifference.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.actual_poisson_difference_mass_le line 20

   Source documentation

   The scalar shifts cancel for the difference of two actual same-scale replacements. The ordinary full Bochner mass is bounded by the sum of their two actual source budgets, including all singular parts.

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

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