ScalarPoissonKernelSourceChain.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The geometric equation has a smooth right-hand side for P - Id. These localization steps use that remainder and only H1 of the solution.

theorem OAI.PositiveEinsteinFour.Geometry.scalarCutoffNested_mul line 22
Source documentation
Inserting an outer cutoff does not change the inner localization.
```
theorem scalarCutoffNested_mul (ψ χ : S) (h : ScalarCutoffNested ψ χ) (u : T) :
    M ψ (M χ u) = M ψ u := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.ScalarCutoffNested

theorem OAI.PositiveEinsteinFour.Geometry.scalar_nested_cutoff_gain_of_remainder line 34

Source documentation

One local gain uses a regular remainder P u - u, not an assumption that P u is already regular to the target order.

theorem scalar_nested_cutoff_gain_of_remainder
    (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 - u))) :
    MemSobolev ((n + 2 : ℕ) : ℝ) 2 (M ψ u) := by
…

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

theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_cutoff_chain_gain_of_remainder line 59

Source documentation

Finite nested localization for the actual smooth remainder P u - u.

theorem scalar_finite_cutoff_chain_gain_of_remainder
    (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 : T) (n : ℕ) (ψ : ℕ → S)
    (hnest : ∀ k < n, ScalarCutoffNested (ψ k) (ψ (k + 1)))
    (hu : MemSobolev 1 2 (M (ψ n) u))
    (hf : ∀ k ≤ n, MemSobolev (n : ℝ) 2 (M (ψ k) (scalarPerturbedOperator a b u - u))) :
…

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

theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_family_all_orders_of_remainder line 92

Source documentation

The remainder-based finite chains yield every integer order for one fixed inner cutoff.

theorem scalar_cutoff_family_all_orders_of_remainder
    (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 : T) (φ : S)
    (hchain : ∀ n : ℕ, ∃ ψ : ℕ → S, ψ 0 = φ ∧
      (∀ k < n, ScalarCutoffNested (ψ k) (ψ (k + 1))) ∧
      MemSobolev 1 2 (M (ψ n) u) ∧
…

Mentions: OAI.PositiveEinsteinFour.Geometry.ScalarCutoffNested