Space-time Sobolev families and multiplication by smooth cutoffs

On a set V ⊆ ℝ³ × ℝ, a family B of square-integrable fields indexed by derivative words, with B (α ++ [j]) the distributional spatial derivative ∂_j B α on V, describes a field in L²_t H^n_x. Multiplication by a smooth field ζ whose spatial derivatives are all bounded maps such a family to the Leibniz family stLeibniz α (spaceTimeWord · ζ) B of the product. This is the cutoff step in the proof of lem:local-heat-gain.

def ESS.IsSpaceTimeWeakPartial (V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)) (j : Fin 3) (f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : Prop

g is the distributional j-th spatial derivative of f on V.

Equations

• One or more equations did not get rendered due to their size.

structure ESS.IsSpaceTimeFamily (n : ℕ) (V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)) (B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : Prop

A space-time derivative family through order n on V.

• memL2 (α : List (Fin 3)) : α.length ≤ n → MeasureTheory.MemLp (B α) 2 (MeasureTheory.volume.restrict V)
• weak (α : List (Fin 3)) (j : Fin 3) : α.length < n → IsSpaceTimeWeakPartial V j (B α) (B (α ++ [j]))

def ESS.stLeibniz : List (Fin 3) → (List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) → (List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The Leibniz family of a product of two space-time families; the first letter of the word is applied first.

Equations

• One or more equations did not get rendered due to their size.
• ESS.stLeibniz [] x✝¹ x✝ = fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => x✝¹ [] p * x✝ [] p

theorem ESS.memLp_two_restrict_of_test {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : Continuous φ) (hφc : HasCompactSupport φ) (V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)) : MeasureTheory.MemLp φ 2 (MeasureTheory.volume.restrict V)

A space-time test function is square integrable on every restriction.

theorem ESS.IsSpaceTimeWeakPartial.smooth_mul {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {j : Fin 3} {f g ζ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsSpaceTimeWeakPartial V j f g) (hζ : ContDiff ℝ (↑⊤) ζ) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict V)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict V)) : IsSpaceTimeWeakPartial V j (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => ζ p * f p) fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial ζ j p * f p + ζ p * g p

The first-order Leibniz rule for a distributional spatial derivative and a smooth factor.

theorem ESS.IsSpaceTimeWeakPartial.add {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {j : Fin 3} {f₁ g₁ f₂ g₂ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h₁ : IsSpaceTimeWeakPartial V j f₁ g₁) (h₂ : IsSpaceTimeWeakPartial V j f₂ g₂) (hf₁ : MeasureTheory.MemLp f₁ 2 (MeasureTheory.volume.restrict V)) (hf₂ : MeasureTheory.MemLp f₂ 2 (MeasureTheory.volume.restrict V)) (hg₁ : MeasureTheory.MemLp g₁ 2 (MeasureTheory.volume.restrict V)) (hg₂ : MeasureTheory.MemLp g₂ 2 (MeasureTheory.volume.restrict V)) : IsSpaceTimeWeakPartial V j (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => f₁ p + f₂ p) fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => g₁ p + g₂ p

The sum rule for distributional spatial derivatives.

theorem ESS.sobolevWords_zero : CKN.sobolevWords 0 = {[]}

theorem ESS.sobolevWords_mono {k n : ℕ} (hkn : k ≤ n) : CKN.sobolevWords k ⊆ CKN.sobolevWords n

theorem ESS.sum_sobolevWords_cons_le (k : ℕ) (j : Fin 3) (φ : List (Fin 3) → ℝ) (hφ : ∀ (α : List (Fin 3)), 0 ≤ φ α) : ∑ γ ∈ CKN.sobolevWords k, φ (j :: γ) ≤ ∑ γ ∈ CKN.sobolevWords (k + 1), φ γ

Sums over words of length at most k, shifted by a first letter, are bounded by sums over words of length at most k + 1.

theorem ESS.stLeibniz_abs_le (α : List (Fin 3)) (A B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (L : ℝ) (hA : ∀ (γ : List (Fin 3)), γ.length ≤ α.length → ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |A γ p| ≤ L) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : |stLeibniz α A B p| ≤ 2 ^ α.length * L * ∑ γ ∈ CKN.sobolevWords α.length, |B γ p|

The pointwise bound for a Leibniz family with a bounded first factor.

theorem ESS.stLeibniz_aestronglyMeasurable (α : List (Fin 3)) (A B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) {μ : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hA : ∀ (γ : List (Fin 3)), γ.length ≤ α.length → MeasureTheory.AEStronglyMeasurable (A γ) μ) (hB : ∀ (γ : List (Fin 3)), γ.length ≤ α.length → MeasureTheory.AEStronglyMeasurable (B γ) μ) : MeasureTheory.AEStronglyMeasurable (stLeibniz α A B) μ

Leibniz families of almost everywhere strongly measurable families are almost everywhere strongly measurable.

theorem ESS.stLeibniz_memLp (α : List (Fin 3)) {A B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (L : ℝ) (hAb : ∀ (γ : List (Fin 3)), γ.length ≤ α.length → ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |A γ p| ≤ L) (hAm : ∀ (γ : List (Fin 3)), γ.length ≤ α.length → MeasureTheory.AEStronglyMeasurable (A γ) (MeasureTheory.volume.restrict V)) (hB : ∀ (γ : List (Fin 3)), γ.length ≤ α.length → MeasureTheory.MemLp (B γ) 2 (MeasureTheory.volume.restrict V)) : MeasureTheory.MemLp (stLeibniz α A B) 2 (MeasureTheory.volume.restrict V)

Leibniz families with a bounded measurable first factor and a square integrable second factor are square integrable.

theorem ESS.exists_uniform_wordBound {ζ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hζb : ∀ (γ : List (Fin 3)), ∃ (L : ℝ), ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |spaceTimeWord γ ζ p| ≤ L) (k : ℕ) : ∃ (L : ℝ), ∀ (γ : List (Fin 3)), γ.length ≤ k → ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |spaceTimeWord γ ζ p| ≤ L

Bounds for each spatial word derivative give a uniform bound through any finite order.

theorem ESS.IsSpaceTimeFamily.smooth_mul {n : ℕ} {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hB : IsSpaceTimeFamily n V B) {ζ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζb : ∀ (γ : List (Fin 3)), ∃ (L : ℝ), ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |spaceTimeWord γ ζ p| ≤ L) : IsSpaceTimeFamily n V fun (α : List (Fin 3)) => stLeibniz α (fun (γ : List (Fin 3)) => spaceTimeWord γ ζ) B

Multiplication by a smooth field with bounded spatial derivatives maps a space-time derivative family to the Leibniz family of the product.

theorem ESS.stLeibniz_normSq_le (n : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)) (A B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (L : ℝ), (∀ (γ : List (Fin 3)), γ.length ≤ n → ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |A γ p| ≤ L) → (∀ (γ : List (Fin 3)), γ.length ≤ n → MeasureTheory.AEStronglyMeasurable (A γ) (MeasureTheory.volume.restrict V)) → (∀ (γ : List (Fin 3)), γ.length ≤ n → MeasureTheory.MemLp (B γ) 2 (MeasureTheory.volume.restrict V)) → ∑ α ∈ CKN.sobolevWords n, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in V, stLeibniz α A B p ^ 2 ≤ C * L ^ 2 * ∑ α ∈ CKN.sobolevWords n, ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in V, B α p ^ 2

The squared L²_t H^n_x norm of a Leibniz family is bounded by the squared norm of the second factor times the square of a bound for the first.