LocalPoissonDimensionalDensity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional density bound for the actual Poisson measure

This is a consequence of the scalar weak Bochner inequality of Han, Theorem 3.3. Countable compact exhaustion retains the prescribed full measure and proves the density bound on the whole interior ball.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_dimensional_density line 21

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_shifted_density line 47

Source documentation

Completing the one-dimensional square supplies every scalar shift, without a separate assertion about the local dimension.

theorem NoncollapsedRCD.local_poisson_shifted_density {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2≤n)
    (hscalar : ScalarDimensionalBochner (hausdorff n X) hX.quadratic K n)
    (f : SobolevSpace (hausdorff n X) hX.quadratic) (c κ : ℝ) (hK : -κ≤K)
    {p : X} {r : ℝ} (hr : 0<r)
    (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p (8*r)) f c)
    (L : ℝ≥0)
    (hL : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8*r)),
      localGamma (hausdorff n X) hX.quadratic f f x≤(L:ℝ)^2)
    (F₀ : SobolevSpace (hausdorff n X) hX.quadratic) (σ : Measure X) [IsFiniteMeasure σ]
    (hF₀ : SobolevSpace.toLp (hausdorff n X) hX.quadratic F₀
      =ᵐ[(hausdorff n X).restrict (ball p (2*r))] localGamma (hausdorff n X) hX.quadratic f f)
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.ScalarDimensionalBochner, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp