ScalarPoissonKernelLocalization.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

A variable-coefficient cutoff commutator loses only one derivative. Nested cutoffs let this estimate use regularity on a larger neighborhood.

theorem OAI.PositiveEinsteinFour.Geometry.scalar_multiplier_commute line 21
theorem OAI.PositiveEinsteinFour.Geometry.scalar_multiplier_real_smul line 27
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_second_product line 31
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_helmholtz line 47
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_first_term line 54
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_second_term line 62
def OAI.PositiveEinsteinFour.Geometry.scalarPerturbedCutoffCommutator line 73
Source documentation
The commutator with a cutoff, for the actual differential operator.
```
def scalarPerturbedCutoffCommutator (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S)
    (ψ : S) (u : T) : T :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarPerturbedCutoffCommutator_eq line 77
theorem OAI.PositiveEinsteinFour.Geometry.scalar_sobolev_sum line 91
Distinct definitions of this name: OAI/Geometry/EinsteinFour/ScalarPoissonKernelBootstrap.lean:107 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.scalar_sobolev_sum@path.
theorem OAI.PositiveEinsteinFour.Geometry.scalarPerturbedCutoffCommutator_memSobolev line 102
Source documentation
The full variable-coefficient cutoff commutator has differential order one.
```
theorem scalarPerturbedCutoffCommutator_memSobolev
    (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S) (ψ : S) (n : ℕ) (u : T)
    (hu : MemSobolev ((n + 1 : ℕ) : ℝ) 2 u) :
    MemSobolev (n : ℝ) 2 (scalarPerturbedCutoffCommutator a b ψ u) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.scalarPerturbedCutoffCommutator
def OAI.PositiveEinsteinFour.Geometry.ScalarCutoffNested line 128
Source documentation
The outer cutoff equals one near the support of the inner cutoff.
```
def ScalarCutoffNested (ψ χ : S) : Prop :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_nested_value line 131
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_nested_first_zero line 139
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_nested_second_zero line 151
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_nested_mul line 166
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_nested_first_mul line 171
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_nested_second_mul line 177
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_nested_derivative line 183
theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_nested_second_derivative line 190
theorem OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator_nested_cutoff line 201
Source documentation
Inner localization of the equation is unchanged by inserting an outer cutoff.
```
theorem scalarPerturbedOperator_nested_cutoff (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S)
    (ψ χ : S) (h : ScalarCutoffNested ψ χ) (u : T) :
    M ψ (scalarPerturbedOperator a b (M χ u)) = M ψ (scalarPerturbedOperator a b u) := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ScalarCutoffNested, OAI.PositiveEinsteinFour.Geometry.scalarPerturbedOperator

theorem OAI.PositiveEinsteinFour.Geometry.scalar_nested_cutoff_gain line 227

Source documentation

One nested-cutoff step gains one local Sobolev order.

theorem scalar_nested_cutoff_gain
    (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)
    (ψ χ : S) (hnest : ScalarCutoffNested ψ χ) (n : ℕ) (u : T)
    (hu : MemSobolev ((n + 1 : ℕ) : ℝ) 2 (M χ u))
    (hf : MemSobolev (n : ℝ) 2 (M ψ (scalarPerturbedOperator a b u))) :
    MemSobolev ((n + 2 : ℕ) : ℝ) 2 (M ψ u) := by
…

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