EuclideanHarmonicL1.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

L¹ mass of normalized compact harmonic extensions

theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.extension_l1_le line 16

Source documentation

The normalized L² bound controls the entire L¹ mass of any compact extension dominated by the model.

theorem EuclideanHarmonicModel.extension_l1_le {n : ℕ} {S : ℝ}
    (w : EuclideanHarmonicModel n S) (hS : 0 < S)
    {F : Euclidean n → ℝ} (hF : Continuous F) (hfs : HasCompactSupport F)
    (hs : tsupport F ⊆ ball 0 S) (hb : ∀ x, |F x| ≤ |w.value x|) :
    (∫ x, |F x|) ≤ volume.real (ball (0 : Euclidean n) S) := by
…

Mentions: OAI.RegularPointCoordinates.EuclideanHarmonicModel, OAI.RegularPointCoordinates.Euclidean