ScalarPoissonKernelUniqueness.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The density step for distributional uniqueness. An invertible L2 extension of the transposed operator after Bessel regularization gives a dense Schwartz range, and hence a trivial L2 distributional kernel.

def OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselInverse line 20
Source documentation
The negative-two Bessel multiplier preserves the actual test space.
```
def scalarSchwartzBesselInverse (φ : 𝓢(V, ℂ)) : 𝓢(V, ℂ) :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselInverse_distribution line 24
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2_distribution_injective line 31
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselInverse_toLp line 36
def OAI.PositiveEinsteinFour.Geometry.scalarL2TestPairing line 45
Source documentation
The bilinear, rather than Hermitian, L2 pairing used by distributions.
```
def scalarL2TestPairing (u : L2) : L2 →L[ℂ] ℂ :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2TestPairing_schwartz line 48
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_denseRange_of_bessel_equiv line 59
Source documentation
Surjectivity on L2 after a Schwartz-preserving regularization implies density of the unregularized test-function range.
```
theorem scalarSchwartz_denseRange_of_bessel_equiv
    (T : 𝓢(V, ℂ) → 𝓢(V, ℂ)) (e : L2 ≃L[ℂ] L2)
    (hT : ∀ φ : 𝓢(V, ℂ), (T (scalarSchwartzBesselInverse φ)).toLp 2 = e (φ.toLp 2)) :
    DenseRange (fun φ : 𝓢(V, ℂ) => (T φ).toLp 2) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselInverse
theorem OAI.PositiveEinsteinFour.Geometry.scalarL2_eq_zero_of_pairing line 71
Source documentation
Nondegeneracy of the distributional L2 pairing.
```
theorem scalarL2_eq_zero_of_pairing (u : L2)
    (hzero : ∀ v : L2, scalarL2TestPairing u v = 0) : u = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarL2TestPairing

theorem OAI.PositiveEinsteinFour.Geometry.scalarL2_eq_zero_of_dense_tests line 86

Source documentation

A distribution represented by L2 is zero if it annihilates a dense L2 family of Schwartz test functions.

theorem scalarL2_eq_zero_of_dense_tests (u : L2) (T : 𝓢(V, ℂ) → 𝓢(V, ℂ))
    (hT : DenseRange (fun φ : 𝓢(V, ℂ) => (T φ).toLp 2))
    (hu : ∀ φ : 𝓢(V, ℂ), (u : 𝓢'(V, ℂ)) (T φ) = 0) : u = 0 := by
…

theorem OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator_kernel_of_transpose_equiv line 99
Source documentation
A transposed L2 isomorphism gives distributional uniqueness without regularity of the kernel element.
```
theorem scalarPerturbedOperator_kernel_of_transpose_equiv
    (a : Fin 4 → Fin 4 → 𝓢(V, ℂ)) (b : Fin 4 → 𝓢(V, ℂ))
    (e : L2 ≃L[ℂ] L2)
    (he : ∀ φ : 𝓢(V, ℂ),
      (scalarSchwartzTranspose a b (scalarSchwartzBesselInverse φ)).toLp 2 = e (φ.toLp 2))
    (u : L2) (hu : scalarPerturbedOperator a b (u : 𝓢'(V, ℂ)) = 0) : u = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarSchwartzTranspose, OAI.PositiveEinsteinFour.Geometry.scalarSchwartzBesselInverse, OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator