CutoffPoissonRepresentative.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Constructing the local representative of an actual Poisson solution

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.cutoff_poisson_representative line 19

Source documentation

Localizing the equation and integrating its actual two source terms constructs a Lipschitz representative without a gradient premise on f.

theorem NoncollapsedRCD.cutoff_poisson_representative {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 C : ℝ), 0 < R → -1 ≤ K*R^2 →
      0 < T → T ≤ 1 → T ≤ R^2 → 0 ≤ C →
      ∀ (Ω : Set X) (f : SobolevSpace (hausdorff n X) hX.quadratic) (c : ℝ),
      IsConstantLaplacianOn (hausdorff n X) hX.quadratic Ω f c →
      ∀ (A : ℝ≥0), (∀ᵐ x ∂hausdorff n X, |SobolevSpace.toLp _ _ f x| ≤ A) →
      ∀ χ : GoodLaplacianCutoff (hausdorff n X) hX.quadratic p R C,
      closedBall p (2*R) ⊆ Ω →
…

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