LocalPoissonGradientMeasure.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Full Poisson energy measures from the local gradient alone

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_measure_of_gradient line 17

Source documentation

The scalar Bochner measure needs no amplitude assumption on the Poisson function. Local transport supplies that bound on an interior ball.

theorem NoncollapsedRCD.local_poisson_measure_of_gradient {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2 ≤ n)
    (f : SobolevSpace (hausdorff n X) hX.quadratic) (c : ℝ)
    {p : X} {R b C : ℝ} (hR : 0 < R) (hRb : 3 * R < b)
    (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p b) f c)
    (L : ℝ≥0) (hL : ∀ᵐ x ∂(hausdorff n X).restrict (ball p b),
      localGamma (hausdorff n X) hX.quadratic f f x ≤ (L : ℝ) ^ 2)
    (χ : GoodLaplacianCutoff (hausdorff n X) hX.quadratic p (3 * R / 2) C)
    (κ : ℝ) (hK : -κ ≤ K) :
    ∃ (G : SobolevSpace (hausdorff n X) hX.quadratic) (σ : Measure X),
      ∃ hσ : IsFiniteMeasure σ,
      (∀ᵐ x ∂hausdorff n X, 0 ≤ SobolevSpace.toLp (hausdorff n X) hX.quadratic G x ∧
…

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

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_energy_measure line 50

Source documentation

The actual scalar Bochner measure exists on every interior ball of a constant-Laplacian function with locally bounded gradient. All analytic objects are constructed from the RCD condition.

theorem NoncollapsedRCD.local_poisson_energy_measure {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2 ≤ n)
    (f : SobolevSpace (hausdorff n X) hX.quadratic) (c : ℝ)
    {p : X} {R b : ℝ} (hR : 0 < R) (hRb : 3 * R < b)
    (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p b) f c)
    (L : ℝ≥0) (hL : ∀ᵐ x ∂(hausdorff n X).restrict (ball p b),
      localGamma (hausdorff n X) hX.quadratic f f x ≤ (L : ℝ) ^ 2)
    (κ : ℝ) (hK : -κ ≤ K) :
    ∃ (G : SobolevSpace (hausdorff n X) hX.quadratic) (σ : Measure X),
      ∃ hσ : IsFiniteMeasure σ,
      (∀ᵐ x ∂hausdorff n X, 0 ≤ SobolevSpace.toLp (hausdorff n X) hX.quadratic G x ∧
        SobolevSpace.toLp (hausdorff n X) hX.quadratic G x ≤ (L : ℝ) ^ 2) ∧
…