ScalarPoissonKernelBootstrap.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Integer-order elliptic bootstrap from the actual distributional commutator and the proved small-coefficient H2 regularity theorem.

theorem OAI.PositiveEinsteinFour.Geometry.scalar_derivative_fourier line 20
theorem OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative_commute line 29
Source documentation
Coordinate derivatives commute for every tempered distribution.
```
theorem scalarCoordinateDerivative_commute (i j : Fin 4) (u : 𝓢'(V, ℂ)) :
    scalarCoordinateDerivative i (scalarCoordinateDerivative j u) =
      scalarCoordinateDerivative j (scalarCoordinateDerivative i u) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarCoordinateDerivative
theorem OAI.PositiveEinsteinFour.Geometry.scalar_derivative_add line 44
theorem OAI.PositiveEinsteinFour.Geometry.scalar_derivative_sub line 49
theorem OAI.PositiveEinsteinFour.Geometry.scalar_derivative_real_smul line 54
theorem OAI.PositiveEinsteinFour.Geometry.scalar_derivative_sum line 58
theorem OAI.PositiveEinsteinFour.Geometry.scalar_derivative_laplacian line 62
theorem OAI.PositiveEinsteinFour.Geometry.scalar_derivative_helmholtz line 75

theorem OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator_derivative line 82

Source documentation

Exact first commutator of the variable-coefficient operator.

theorem scalarPerturbedOperator_derivative (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S)
    (k : Fin 4) (u : 𝓢'(V, ℂ)) :
    scalarCoordinateDerivative k (scalarPerturbedOperator a b u) =
      scalarPerturbedOperator a b (scalarCoordinateDerivative k u) +
        (∑ i : Fin 4, ∑ j : Fin 4, smulLeftCLM ℂ (D k (a i j))
          (scalarCoordinateDerivative i (scalarCoordinateDerivative j u))) +
        ∑ i : Fin 4, smulLeftCLM ℂ (D k (b i)) (scalarCoordinateDerivative i u) := by
…

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

theorem OAI.PositiveEinsteinFour.Geometry.scalar_sobolev_nat_step line 102
theorem OAI.PositiveEinsteinFour.Geometry.scalar_sobolev_sum line 107
Distinct definitions of this name: OAI/Geometry/EinsteinFour/ScalarPoissonKernelLocalization.lean:91 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.scalar_sobolev_sum@path.

theorem OAI.PositiveEinsteinFour.Geometry.scalar_small_elliptic_integer_regularity line 120

Source documentation

Every integer Sobolev order of the right-hand side gives two additional orders for the original L2 solution.

theorem scalar_small_elliptic_integer_regularity
    (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S) (δ : ℝ) (hδ : 0 ≤ δ)
    (ha : ∀ i j x, ‖a i j x‖ ≤ δ)
    (ha1 : ∀ i j k x, ‖D k (a i j) x‖ ≤ δ)
    (ha2 : ∀ i j k l x, ‖D k (D l (a i j)) x‖ ≤ δ)
    (hb : ∀ i x, ‖b i x‖ ≤ δ)
    (hb1 : ∀ i k x, ‖D k (b i) x‖ ≤ δ)
    (hsmall : (16 * (2 * Real.pi) ^ 2 + 36 * (2 * Real.pi) + 20) * δ < 1)
    (n : ℕ) (u f : 𝓢'(V, ℂ)) (hu : MemSobolev 0 2 u)
    (hf : MemSobolev (n : ℝ) 2 f) (heq : scalarPerturbedOperator a b u = f) :
    MemSobolev ((n + 2 : ℕ) : ℝ) 2 u := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator