ScalarPoissonKernelHelmholtz.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The normalized constant-coefficient Helmholtz operator gains two Sobolev orders. This is an identity of actual tempered-distribution operators, deduced from the Fourier multiplier definition of the Bessel potential.

theorem OAI.PositiveEinsteinFour.Geometry.scalar_fourierMultiplier_add line 19
Distinct definitions of this name: OAI/Geometry/EinsteinFour/ScalarPoissonKernelDerivative.lean:79 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.scalar_fourierMultiplier_add@path.
theorem OAI.PositiveEinsteinFour.Geometry.scalar_bessel_two_add line 26
def OAI.PositiveEinsteinFour.Geometry.normalizedScalarHelmholtz line 41
Source documentation
The normalization follows the Fourier convention used by Mathlib: J² = 1 - (2π)⁻² Δ.
```
def normalizedScalarHelmholtz (u : 𝓢'(E, ℂ)) : 𝓢'(E, ℂ) :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.normalizedScalarHelmholtz_eq_bessel line 44
theorem OAI.PositiveEinsteinFour.Geometry.normalizedScalarHelmholtz_memSobolev_iff line 55
Source documentation
No regularity is assumed for u: regularity of its normalized Helmholtz image is equivalent to two additional Sobolev orders of u.
```
theorem normalizedScalarHelmholtz_memSobolev_iff {s : ℝ} {p : ℝ≥0∞}
    [Fact (1 ≤ p)] (u : 𝓢'(E, ℂ)) :
    MemSobolev s p (normalizedScalarHelmholtz u) ↔ MemSobolev (s + 2) p u := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.normalizedScalarHelmholtz
theorem OAI.PositiveEinsteinFour.Geometry.normalizedScalarHelmholtz_gain_two line 60
theorem OAI.PositiveEinsteinFour.Geometry.scalar_laplacian_gain_two line 67
Source documentation
Distributional control of both u and its actual Laplacian gains two orders, with no elliptic regularity premise.
```
theorem scalar_laplacian_gain_two {s : ℝ} {p : ℝ≥0∞} [Fact (1 ≤ p)]
    {u : 𝓢'(E, ℂ)} (hu : MemSobolev s p u) (hΔ : MemSobolev s p (Δ u)) :
    MemSobolev (s + 2) p u := by
…
```