ScalarPoissonKernelLocalRegularity.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Small-coefficient regularity applies to an existing L2 distributional solution: construct an H2 solution, then identify the two using the actual formal-transpose uniqueness theorem.

theorem OAI.PositiveEinsteinFour.Geometry.scalar_coordinate_sub line 21
theorem OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator_sub line 26
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_Linf_bound line 34

theorem OAI.PositiveEinsteinFour.Geometry.scalar_small_elliptic_gain_two line 43

Source documentation

This is regularity of the given solution, not only existence of a new regular solution. All smallness assumptions concern the actual coefficient functions and their first two derivatives.

theorem scalar_small_elliptic_gain_two
    (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)
    (u f : L2) (hu : scalarPerturbedOperator a b (u : 𝓢'(V, ℂ)) = (f : 𝓢'(V, ℂ))) :
    MemSobolev 2 2 (u : 𝓢'(V, ℂ)) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator