The energy estimate for smooth zero-initial heat solutions

For a smooth solution w of ∂ₜ w - Δ w = H with compact spatial support and zero initial value at t = a, pairing the equation with (1 - Δ)^m w gives

‖w(t)‖²_{H^m} + ∫_a^b ‖w‖²_{H^{m+1}} ≤ C ∫_a^b ‖H‖²_{H^{m-1}}

(lem:local-heat-gain, step #fourier-energy-estimate). At integer order this pairing is the sum of the L² energies of the spatial derivatives ∂^β w, |β| ≤ m. Each ∂^β w solves the heat equation with source ∂^β H, written in divergence form ∂_k(∂^{β'} H) when β = β' ++ [k] is nonempty, so that only m - 1 derivatives of H enter. The smooth energy bound smoothVorticityEnergyGronwall then applies to each derivative.

The constant depends on m and on an upper bound for b - a: the Young absorption controls only the gradient part of the H^{m+1} norm, and the remaining ‖w‖²_{H^m} term is handled by Grönwall's inequality.

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

The iterated spatial coordinate derivative of a space-time field along a word; the first letter is applied first.

Equations

• ESS.spaceTimeWord [] x✝ = x✝
• ESS.spaceTimeWord (j :: β) x✝ = ESS.spaceTimeWord β fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial x✝ j p

theorem ESS.spaceTimeWord_append (β : List (Fin 3)) (k : Fin 3) (W : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : spaceTimeWord (β ++ [k]) W = fun (p : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (spaceTimeWord β W) k p

The last letter of a word is the outermost derivative.

theorem ESS.contDiff_spaceTimeWord (β : List (Fin 3)) {W : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hW : ContDiff ℝ (↑⊤) W) : ContDiff ℝ (↑⊤) (spaceTimeWord β W)

Spatial word derivatives of a smooth space-time field are smooth.

theorem ESS.spaceTimeWord_slice (β : List (Fin 3)) (W : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (t : ℝ) : (fun (y : CKN.Foundation.Parabolic.Vec3) => spaceTimeWord β W (y, t)) = CKN.wordDeriv β fun (y : CKN.Foundation.Parabolic.Vec3) => W (y, t)

On a time slice, the space-time word derivative is the spatial word derivative of the slice.

theorem ESS.timePartial_spaceTimeWord (β : List (Fin 3)) {W : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hW : ContDiff ℝ (↑⊤) W) : (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.timePartial (spaceTimeWord β W) p) = spaceTimeWord β fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.timePartial W q

Time differentiation commutes with spatial word derivatives of smooth fields.

theorem ESS.spatialSecondPartial_spaceTimeWord (β : List (Fin 3)) (k : Fin 3) {W : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hW : ContDiff ℝ (↑⊤) W) : (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialSecondPartial (spaceTimeWord β W) k k p) = spaceTimeWord β fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialSecondPartial W k k q

The spatial second derivative ∂_k ∂_k commutes with spatial word derivatives of smooth fields.

theorem ESS.spatialPartial_sub_sum {A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {B : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hB : ∀ (k : Fin 3), ContDiff ℝ (↑⊤) (B k)) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => A q - ∑ k : Fin 3, B k q) j p = CKN.spatialPartial A j p - ∑ k : Fin 3, CKN.spatialPartial (B k) j p

Spatial differentiation of a difference of smooth fields.

theorem ESS.spaceTimeWord_sub_sum (β : List (Fin 3)) {A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {B : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hB : ∀ (k : Fin 3), ContDiff ℝ (↑⊤) (B k)) : (spaceTimeWord β fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => A q - ∑ k : Fin 3, B k q) = fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => spaceTimeWord β A p - ∑ k : Fin 3, spaceTimeWord β (B k) p

Spatial word derivatives are linear on smooth fields.

theorem ESS.spatialPartial_eq_zero_of_compl {K : Set CKN.Foundation.Parabolic.Vec3} (hK : IsCompact K) {V : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hV : ∀ x ∉ K, ∀ (t : ℝ), V (x, t) = 0) (j : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : x ∉ K → ∀ (t : ℝ), CKN.spatialPartial V j (x, t) = 0

Fields vanishing outside a compact spatial set keep this property under spatial differentiation.

theorem ESS.timePartial_eq_zero_of_compl {K : Set CKN.Foundation.Parabolic.Vec3} {V : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hV : ∀ x ∉ K, ∀ (t : ℝ), V (x, t) = 0) (x : CKN.Foundation.Parabolic.Vec3) : x ∉ K → ∀ (t : ℝ), CKN.timePartial V (x, t) = 0

Fields vanishing outside a compact spatial set keep this property under time differentiation.

theorem ESS.spaceTimeWord_eq_zero_of_compl {K : Set CKN.Foundation.Parabolic.Vec3} (hK : IsCompact K) (β : List (Fin 3)) {V : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hV : ∀ x ∉ K, ∀ (t : ℝ), V (x, t) = 0) (x : CKN.Foundation.Parabolic.Vec3) : x ∉ K → ∀ (t : ℝ), spaceTimeWord β V (x, t) = 0

Word derivatives of fields vanishing outside a compact spatial set vanish there too.

theorem ESS.spaceTimeWord_eq_zero_of_slice (β : List (Fin 3)) {V : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {a : ℝ} (hV : ∀ (x : CKN.Foundation.Parabolic.Vec3), V (x, a) = 0) (x : CKN.Foundation.Parabolic.Vec3) : spaceTimeWord β V (x, a) = 0

Word derivatives of a field vanishing on a time slice vanish on that slice.

theorem ESS.spatialPartial_const_zero (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 0) j p = 0

theorem ESS.timePartial_const_zero (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.timePartial (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 0) p = 0

theorem ESS.spatialSecondPartial_const_zero (j k : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialSecondPartial (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 0) j k p = 0

theorem ESS.scalarHeatEnergy_smooth {a b : ℝ} (hab : a ≤ b) {z g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {F : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hz : ContDiff ℝ (↑⊤) z) (hF : ∀ (j : Fin 3), ContDiff ℝ (↑⊤) (F j)) (hg : ContDiff ℝ (↑⊤) g) {K : Set CKN.Foundation.Parabolic.Vec3} (hK : IsCompact K) (hzero : ∀ x ∉ K, ∀ (t : ℝ), z (x, t) = 0 ∧ (∀ (j : Fin 3), F j (x, t) = 0) ∧ g (x, t) = 0) (heq : ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.timePartial z p - ∑ j : Fin 3, CKN.spatialSecondPartial z j j p = ∑ j : Fin 3, CKN.spatialPartial (F j) j p + g p) (hinit : ∀ (x : CKN.Foundation.Parabolic.Vec3), z (x, a) = 0) : have f := fun (s : ℝ) => (2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, F j (x, s) ^ 2) + ∫ (x : CKN.Foundation.Parabolic.Vec3), g (x, s) ^ 2; (∀ t ∈ Set.Icc a b, ∫ (x : CKN.Foundation.Parabolic.Vec3), z (x, t) ^ 2 ≤ Real.exp (b - a) * ∫ (s : ℝ) in a..b, f s) ∧ ∫ (t : ℝ) in a..b, ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, CKN.spatialPartial z j (x, t) ^ 2 ≤ (1 + (b - a) * Real.exp (b - a)) * ∫ (s : ℝ) in a..b, f s

The smooth energy bound for a scalar solution of ∂ₜ z - Δ z = Σ_j ∂_j F_j + g with compact spatial support and zero value at t = a.

theorem ESS.continuous_integral_sq_of_compl {V : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hV : Continuous V) {K : Set CKN.Foundation.Parabolic.Vec3} (hK : IsCompact K) (h0 : ∀ x ∉ K, ∀ (t : ℝ), V (x, t) = 0) : Continuous fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), V (x, s) ^ 2

The spatial L² energy of a continuous field vanishing outside a compact spatial set is continuous in time.

theorem ESS.sum_sobolevWords_succ_le (m : ℕ) (φ : List (Fin 3) → ℝ) (hφ : ∀ (α : List (Fin 3)), 0 ≤ φ α) : ∑ γ ∈ CKN.sobolevWords (m + 1), φ γ ≤ φ [] + ∑ β ∈ CKN.sobolevWords m, ∑ j : Fin 3, φ (β ++ [j])

Every word of length at most m + 1 is empty or a word of length at most m followed by one letter.

theorem ESS.localHeatGain_fourierEnergy (m : ℕ) (hm : m = 1 ∨ m = 2) {L : ℝ} (hL : 0 < L) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a b : ℝ) (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), a < b → b - a ≤ L → ContDiff ℝ (↑⊤) w → (∃ (K : Set CKN.Foundation.Parabolic.Vec3), IsCompact K ∧ ∀ x ∉ K, ∀ (t : ℝ), w (x, t) = 0) → (∀ (x : CKN.Foundation.Parabolic.Vec3), w (x, a) = 0) → ∀ t ∈ Set.Icc a b, ((CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (y : CKN.Foundation.Parabolic.Vec3) => w (y, t)) + ∫ (s : ℝ) in a..b, CKN.sobolevNormSqOn (m + 1) Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (y : CKN.Foundation.Parabolic.Vec3) => w (y, s)) ≤ C * ∫ (s : ℝ) in a..b, CKN.sobolevNormSqOn (m - 1) Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.timePartial w (y, s) - ∑ j : Fin 3, CKN.spatialSecondPartial w j j (y, s)

lem:local-heat-gain, step #fourier-energy-estimate, with the constant depending on m and on an upper bound L for b - a.