LocalizedPoissonAverages.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Interior spatial control from the localized weak Poisson equation

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.localized_poisson_average_bound line 19

Source documentation

The annular source contributes linearly in time, while the bounded source contributes its integrable square-root heat singularity.

theorem NoncollapsedRCD.localized_poisson_average_bound {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular] (hn : 2 ≤ n)
    {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker)
    (hg : HasCoordinateHeatBounds (hausdorff n X) ker) :
    ∃ J : ℝ, 0 < J ∧ ∀ (p : X) (R T : ℝ), 0 < R → -1 ≤ K*R^2 →
      0 < T → T ≤ 1 → T ≤ R^2 →
      ∀ (u : SobolevSpace (hausdorff n X) hX.quadratic)
        (b e : Lp ℝ 2 (hausdorff n X)),
      IsWeakLaplacian (hausdorff n X) hX.quadratic u (b+e) →
      ∀ (C D : ℝ≥0),
      (∀ᵐ x ∂hausdorff n X, |SobolevSpace.toLp _ _ u x| ≤ C) →
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.HasCoordinateHeatBounds, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsWeakLaplacian, OAI.RegularPointCoordinates.SobolevSpace.toLp