ScalarPoissonKernelAdjoint.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The actual transpose of the localized second-order scalar operator. All coefficient and derivative operations here act on Schwartz functions; there is no assumed integration-by-parts or regularity identity.

def OAI.PositiveEinsteinFour.Geometry.scalarSchwartzHelmholtz line 20
Source documentation
The normalized constant-coefficient operator on test functions.
```
def scalarSchwartzHelmholtz (φ : 𝓢(V, ℂ)) : 𝓢(V, ℂ) :=
…
```
def OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator line 24
Source documentation
The actual variable-coefficient operator on tempered distributions.
```
def scalarPerturbedOperator (a : Fin 4 → Fin 4 → 𝓢(V, ℂ))
    (b : Fin 4 → 𝓢(V, ℂ)) (u : 𝓢'(V, ℂ)) : 𝓢'(V, ℂ) :=
…
```
def OAI.PositiveEinsteinFour.Geometry.scalarSchwartzTranspose line 32
Source documentation
The transpose includes the derivatives of the coefficients.
```
def scalarSchwartzTranspose (a : Fin 4 → Fin 4 → 𝓢(V, ℂ))
    (b : Fin 4 → 𝓢(V, ℂ)) (φ : 𝓢(V, ℂ)) : 𝓢(V, ℂ) :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzHelmholtz_transpose line 41
theorem OAI.PositiveEinsteinFour.Geometry.scalar_second_transpose line 45
theorem OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator_transpose line 54
Source documentation
The precise distributional transpose identity, including signs and the order reversal in the two derivative slots.
```
theorem scalarPerturbedOperator_transpose (a : Fin 4 → Fin 4 → 𝓢(V, ℂ))
    (b : Fin 4 → 𝓢(V, ℂ)) (u : 𝓢'(V, ℂ)) (φ : 𝓢(V, ℂ)) :
    scalarPerturbedOperator a b u φ = u (scalarSchwartzTranspose a b φ) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator, OAI.PositiveEinsteinFour.Geometry.scalarSchwartzTranspose

theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzCoordinateDerivative_product line 66

Source documentation

First-order product rule on the test-function space.

theorem scalarSchwartzCoordinateDerivative_product (a φ : 𝓢(V, ℂ)) (i : Fin 4) :
    scalarSchwartzCoordinateDerivative i (SchwartzMap.smulLeftCLM ℂ a φ) =
      SchwartzMap.smulLeftCLM ℂ (scalarSchwartzCoordinateDerivative i a) φ +
        SchwartzMap.smulLeftCLM ℂ a (scalarSchwartzCoordinateDerivative i φ) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarSchwartzCoordinateDerivative

theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartzCoordinateDerivative_second_product line 82

Source documentation

Expanding the two coefficient derivatives exhibits all lower-order terms.

theorem scalarSchwartzCoordinateDerivative_second_product
    (a φ : 𝓢(V, ℂ)) (i j : Fin 4) :
    scalarSchwartzCoordinateDerivative j (scalarSchwartzCoordinateDerivative i
      (SchwartzMap.smulLeftCLM ℂ a φ)) =
      SchwartzMap.smulLeftCLM ℂ a
        (scalarSchwartzCoordinateDerivative j (scalarSchwartzCoordinateDerivative i φ)) +
      SchwartzMap.smulLeftCLM ℂ (scalarSchwartzCoordinateDerivative i a)
        (scalarSchwartzCoordinateDerivative j φ) +
      SchwartzMap.smulLeftCLM ℂ (scalarSchwartzCoordinateDerivative j a)
        (scalarSchwartzCoordinateDerivative i φ) +
      SchwartzMap.smulLeftCLM ℂ
        (scalarSchwartzCoordinateDerivative j (scalarSchwartzCoordinateDerivative i a)) φ := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarSchwartzCoordinateDerivative