ScalarPoissonKernelBesselEstimate.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Quantitative L2 realization of the normalized Helmholtz inverse and its first two coordinate derivatives. The constants retain Mathlib's 2π Fourier normalization.

theorem OAI.PositiveEinsteinFour.Geometry.scalar_norm_fourierInv line 20
def OAI.PositiveEinsteinFour.Geometry.scalarL2FourierMultiplier line 24
Source documentation
A bounded Fourier symbol acts continuously on the actual L2 space.
```
def scalarL2FourierMultiplier (a : Linf) : L2 →L[ℂ] L2 :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2FourierMultiplier_norm line 39
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2FourierMultiplier_distribution line 45
def OAI.PositiveEinsteinFour.Geometry.besselInverseSymbol line 54
def OAI.PositiveEinsteinFour.Geometry.besselFirstSymbol line 57
def OAI.PositiveEinsteinFour.Geometry.besselSecondSymbol line 60
theorem OAI.PositiveEinsteinFour.Geometry.besselInverseSymbol_temperate line 63
theorem OAI.PositiveEinsteinFour.Geometry.besselFirstSymbol_temperate line 67
theorem OAI.PositiveEinsteinFour.Geometry.besselSecondSymbol_temperate line 73
theorem OAI.PositiveEinsteinFour.Geometry.scalar_coordinate_abs_le line 79
theorem OAI.PositiveEinsteinFour.Geometry.besselInverseSymbol_bound line 84
theorem OAI.PositiveEinsteinFour.Geometry.besselFirstSymbol_bound line 89
theorem OAI.PositiveEinsteinFour.Geometry.besselSecondSymbol_bound line 97
theorem OAI.PositiveEinsteinFour.Geometry.scalar_symbol_memLp line 111
theorem OAI.PositiveEinsteinFour.Geometry.scalar_symbol_Linf_norm line 115
def OAI.PositiveEinsteinFour.Geometry.scalarBesselInverseL2 line 122
Source documentation
The actual L2 inverse of 1 - (2π)⁻² Δ.
```
def scalarBesselInverseL2 : L2 →L[ℂ] L2 :=
…
```
def OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL2 line 127
Source documentation
First distributional derivative of the normalized inverse, realized in L2.
```
def scalarBesselFirstL2 (i : Fin 4) : L2 →L[ℂ] L2 :=
…
```
def OAI.PositiveEinsteinFour.Geometry.scalarBesselSecondL2 line 132
Source documentation
Second distributional derivative of the normalized inverse, realized in L2.
```
def scalarBesselSecondL2 (i j : Fin 4) : L2 →L[ℂ] L2 :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselInverseL2_norm line 137
theorem OAI.PositiveEinsteinFour.Geometry.scalar_fourier_constant_norm line 142
theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_multiplier_contraction line 146
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL2_norm line 153
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselSecondL2_norm line 160
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselInverseL2_distribution line 167
theorem OAI.PositiveEinsteinFour.Geometry.scalar_derivative_multiplier line 174
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselInverseL2_symbol line 186
theorem OAI.PositiveEinsteinFour.Geometry.scalar_L2_smul_distribution line 191
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL2_symbol line 195
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselSecondL2_symbol line 202
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselFirstL2_distribution line 209
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselSecondL2_distribution line 221
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselInverseL2_helmholtz line 238
Source documentation
The L2 construction solves the actual normalized distributional equation.
```
theorem scalarBesselInverseL2_helmholtz (f : L2) :
    normalizedScalarHelmholtz (scalarBesselInverseL2 f : 𝓢'(V, ℂ)) = (f : 𝓢'(V, ℂ)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.normalizedScalarHelmholtz, OAI.PositiveEinsteinFour.Geometry.scalarBesselInverseL2
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselInverseL2_memSobolev line 245
Source documentation
The constructed inverse has two Sobolev derivatives.
```
theorem scalarBesselInverseL2_memSobolev (f : L2) :
    MemSobolev 2 2 (scalarBesselInverseL2 f : 𝓢'(V, ℂ)) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarBesselInverseL2