EuclideanHarmonicWideExtension.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A compact extension with fixed room around the half ball

theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.wide_compact_extension line 16

Source documentation

A C² compact extension equal to the harmonic model on the three-quarter ball; this leaves fixed room for a mean kernel around every half-ball point.

theorem EuclideanHarmonicModel.wide_compact_extension {n : ℕ} {S : ℝ}
    (w : EuclideanHarmonicModel n S) (hS : 0 < S) :
    ∃ F : Euclidean n → ℝ, ContDiff ℝ 2 F ∧ HasCompactSupport F ∧
      tsupport F ⊆ closedBall 0 (7*S/8) ∧
      (∀ x ∈ ball (0 : Euclidean n) (3*S/4), F x = w.value x) ∧
      (∀ x, |F x| ≤ |w.value x|) ∧
      HarmonicOnNhd F (ball 0 (3*S/4)) := by
…

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