ScalarPoissonKernelCommutator.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exact localization of the distributional Laplacian, and the loss of only one Sobolev order in its smooth-cutoff commutator.

def OAI.PositiveEinsteinFour.Geometry.scalarSchwartzCoordinateDerivative line 17
theorem OAI.PositiveEinsteinFour.Geometry.scalar_schwartz_sum_multiplier line 20
theorem OAI.PositiveEinsteinFour.Geometry.scalar_secondDerivative_multiplier line 31

theorem OAI.PositiveEinsteinFour.Geometry.scalar_laplacian_multiplier line 55

Source documentation

The actual distributional Laplacian product rule.

theorem scalar_laplacian_multiplier (a : 𝓢(V, ℂ)) (u : 𝓢'(V, ℂ)) :
    Δ (smulLeftCLM ℂ a u) = smulLeftCLM ℂ a (Δ u) +
      (2 : ℂ) • (∑ i : Fin 4, smulLeftCLM ℂ (scalarSchwartzCoordinateDerivative i a)
        (scalarCoordinateDerivative i u)) + smulLeftCLM ℂ (Δ a : 𝓢(V, ℂ)) u := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarSchwartzCoordinateDerivative, OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative

def OAI.PositiveEinsteinFour.Geometry.scalarLaplacianCommutator line 76
Source documentation
The part created by commuting a smooth cutoff with the Laplacian.
```
def scalarLaplacianCommutator (a : 𝓢(V, ℂ)) (u : 𝓢'(V, ℂ)) : 𝓢'(V, ℂ) :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacianCommutator_eq line 79
theorem OAI.PositiveEinsteinFour.Geometry.scalarLaplacianCommutator_memSobolev line 87
Source documentation
A cutoff commutator loses only one derivative, including the H1-to-L2 case.
```
theorem scalarLaplacianCommutator_memSobolev (n : ℕ) (a : 𝓢(V, ℂ))
    (u : 𝓢'(V, ℂ)) (hu : MemSobolev ((n + 1 : ℕ) : ℝ) 2 u) :
    MemSobolev (n : ℝ) 2 (scalarLaplacianCommutator a u) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarLaplacianCommutator

theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_laplacian_memSobolev line 108

Source documentation

Localizing the equation preserves the lower Sobolev order of its RHS.

theorem scalar_cutoff_laplacian_memSobolev (n : ℕ) (a : 𝓢(V, ℂ))
    (u : 𝓢'(V, ℂ)) (hu : MemSobolev ((n + 1 : ℕ) : ℝ) 2 u)
    (hΔ : MemSobolev (n : ℝ) 2 (Δ u)) :
    MemSobolev (n : ℝ) 2 (Δ (smulLeftCLM ℂ a u)) := by
…