ScalarPoissonKernelLocalizationChain.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A finite chain of nested cutoffs upgrades local H1 control to every requested finite Sobolev order. Only the localized equation's right-hand side needs that order; the starting solution needs one derivative.

theorem OAI.PositiveEinsteinFour.Geometry.scalar_finite_cutoff_chain_gain line 25

Source documentation

n nested transitions upgrade an outer H1 cutoff to H^(n+1) at the innermost cutoff. The sequence outside the finite chain is irrelevant.

theorem scalar_finite_cutoff_chain_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)
    (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))) :
…

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

theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_family_all_orders line 58

Source documentation

A family of finite localizing chains gives all integer Sobolev orders for a fixed inner cutoff. This is the form used before Fourier inversion.

theorem scalar_cutoff_family_all_orders
    (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

theorem OAI.PositiveEinsteinFour.Geometry.scalar_cutoff_family_smooth_representative line 81

Source documentation

The regular representative is constructed by the Fourier Sobolev theorem, once the finite cutoff chains have been supplied.

theorem scalar_cutoff_family_smooth_representative
    (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