EuclideanHarmonicCompactExtension.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Compact extensions of local Euclidean harmonic functions

theorem OAI.RegularPointCoordinates.contDiff_mul_of_tsupport_subset line 16

Source documentation

A smooth cutoff supported inside the differentiability region produces a global smooth product, even when the original function is only local.

theorem contDiff_mul_of_tsupport_subset {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {Ω : Set E} (hΩ : IsOpen Ω) {f χ : E → ℝ} {k : ℕ∞ω}
    (hf : ContDiffOn ℝ k f Ω) (hχ : ContDiff ℝ k χ) (hs : tsupport χ ⊆ Ω) :
    ContDiff ℝ k (fun x => χ x*f x) := by
…

theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.compact_extension line 31

Source documentation

A normalized local harmonic model has a global compact C² extension which agrees on the half ball and never increases its pointwise magnitude.

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

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

theorem OAI.RegularPointCoordinates.laplacian_eq_zero_of_notMem_tsupport line 76
Source documentation
The distributional Laplacian has no support outside the original function's support.
```
theorem laplacian_eq_zero_of_notMem_tsupport {n : ℕ} (g : Euclidean n → ℝ)
    {x : Euclidean n} (hx : x ∉ tsupport g) : (Δ g) x = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.Euclidean
theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.integral_mul_laplacian_eq_zero line 84
Source documentation
Classical harmonicity implies the exact zero compact-test pairing needed for local smoothing.
```
theorem EuclideanHarmonicModel.integral_mul_laplacian_eq_zero {n : ℕ} {S : ℝ}
    (w : EuclideanHarmonicModel n S) (hS : 0 < S) {g : Euclidean n → ℝ}
    (hg : ContDiff ℝ 2 g) (hgs : HasCompactSupport g)
    (hs : tsupport g ⊆ ball 0 (S/2)) :
    (∫ x, w.value x*(Δ g) x) = 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.EuclideanHarmonicModel, OAI.RegularPointCoordinates.Euclidean