ScalarPoissonKernelDerivative.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Integer Sobolev regularity in four dimensions is characterized by the four actual distributional coordinate derivatives.

def OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative line 18
Source documentation
The actual distributional derivative in one Euclidean coordinate.
```
def scalarCoordinateDerivative (i : Fin 4) (u : 𝓢'(V, ℂ)) : 𝓢'(V, ℂ) :=
…
```
def OAI.PositiveEinsteinFour.Geometry.scalarBesselReciprocal line 21
def OAI.PositiveEinsteinFour.Geometry.scalarBesselCoordinate line 24
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselReciprocal_temperate line 27
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselCoordinate_temperate line 32
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselReciprocal_bound line 38
theorem OAI.PositiveEinsteinFour.Geometry.scalarBesselCoordinate_bound line 44
theorem OAI.PositiveEinsteinFour.Geometry.scalarDerivative_fourierMultiplier line 71
theorem OAI.PositiveEinsteinFour.Geometry.scalar_fourierMultiplier_add line 79
Distinct definitions of this name: OAI/Geometry/EinsteinFour/ScalarPoissonKernelHelmholtz.lean:19 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.scalar_fourierMultiplier_add@path.
theorem OAI.PositiveEinsteinFour.Geometry.scalar_fourierMultiplier_sum line 86
theorem OAI.PositiveEinsteinFour.Geometry.scalarBessel_coordinate_term line 94
theorem OAI.PositiveEinsteinFour.Geometry.scalar_bessel_one_reconstruction line 115
Source documentation
An exact bounded-multiplier reconstruction of one Bessel derivative.
```
theorem scalar_bessel_one_reconstruction (u : 𝓢'(V, ℂ)) :
    besselPotential V ℂ 1 u =
      fourierMultiplierCLM ℂ scalarBesselReciprocal u +
        ∑ i : Fin 4, (2 * Real.pi * Complex.I)⁻¹ •
          fourierMultiplierCLM ℂ (scalarBesselCoordinate i) (scalarCoordinateDerivative i u) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarBesselReciprocal, OAI.PositiveEinsteinFour.Geometry.scalarBesselCoordinate, OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative
theorem OAI.PositiveEinsteinFour.Geometry.scalar_memSobolev_succ_iff line 148
Source documentation
Four coordinate derivatives characterize one additional Sobolev order.
```
theorem scalar_memSobolev_succ_iff (s : ℝ) (u : 𝓢'(V, ℂ)) :
    MemSobolev (s + 1) 2 u ↔
      MemSobolev s 2 u ∧ ∀ i : Fin 4, MemSobolev s 2 (scalarCoordinateDerivative i u) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative