CenteredPoissonPinching.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Full Bochner mass from the centered Poisson pair estimates

theorem OAI.RegularPointCoordinates.local_cutoff_smul_representative line 19
Source documentation
A local scalar multiple of the common cutoff is the indicated constant.
```
theorem local_cutoff_smul_representative (S : Set X) (eta : SobolevSpace μ hQ)
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict S] fun _ => (1 : ℝ)) (c : ℝ) :
    SobolevSpace.toLp μ hQ (c • eta) =ᵐ[μ.restrict S] fun _ => c := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp

theorem OAI.RegularPointCoordinates.centered_poisson_directional_mass line 30

Source documentation

Centering and exact frame changes preserve every input to the full mass estimate. The mass tested here is the actual joint Poisson measure.

theorem centered_poisson_directional_mass {n : ℕ}
    (u : Fin n → SobolevSpace μ hQ) (f : Fin 2 → SobolevSpace μ hQ)
    (eta : SobolevSpace μ hQ) (z delta b : Euclidean n) (c : ℝ)
    (F N : Euclidean n ≃L[ℝ] Euclidean n)
    (Hpair : Euclidean n →L[ℝ] SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X (Euclidean (n + 2)))
    {p : X} {r rho C κ beta P H D : ℝ} {L : ℝ≥0}
    (chi : GoodLaplacianCutoff μ hQ p rho C)
    (hrho : 0 < rho) (hroom : rho < r)
    (hC : 0 ≤ C) (hκ : 0 ≤ κ) (hH : 0 ≤ H) (hD : 0 ≤ D)
    (hvol : 0 < μ.real (ball p rho))
    (heta : SobolevSpace.toLp μ hQ eta =ᵐ[μ.restrict (closedBall p (2 * rho))] fun _ => (1 : ℝ))
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.SobolevSpace.toLp