Local energy estimate for smooth solutions of the heat equation

For a smooth solution of ∂ₜ w - Δ w = div F on a cylinder B_R × (a, b), a space-time cutoff vanishing near the bottom of the cylinder gives the interior bound for the spatial L² norm of w at every later time up to the top and for the spatial gradient of w in L², in terms of the L² norms of w and F on the cylinder. This is the smooth estimate behind the energy levels of thm:vorticity-regularity.

theorem ESS.vorticityHeatSmooth_spatialPartial_eq {A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial A j p = (fderiv ℝ A p) (CKN.basisVec j, 0)

theorem ESS.vorticityHeatSmooth_timePartial_eq {A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.timePartial A p = (fderiv ℝ A p) (0, 1)

theorem ESS.vorticityHeatSmooth_spatialPartial_contDiff {A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (j : Fin 3) : ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial A j p

theorem ESS.vorticityHeatSmooth_timePartial_contDiff {A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) : ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.timePartial A p

theorem ESS.vorticityHeatSmooth_spatialPartial_mul {A B : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => A q * B q) j p = A p * CKN.spatialPartial B j p + B p * CKN.spatialPartial A j p

theorem ESS.vorticityHeatSmooth_timePartial_mul {A B : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.timePartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => A q * B q) p = A p * CKN.timePartial B p + B p * CKN.timePartial A p

theorem ESS.vorticityHeatSmooth_spatialPartial_add {A B : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => A q + B q) j p = CKN.spatialPartial A j p + CKN.spatialPartial B j p

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

theorem ESS.vorticityHeatSmooth_spatialPartial_const_mul {A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (c : ℝ) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => c * A q) j p = c * CKN.spatialPartial A j p

theorem ESS.vorticityHeatSmooth_residual {η w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {F : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hw : ContDiff ℝ (↑⊤) w) (hF : ∀ (j : Fin 3), ContDiff ℝ (↑⊤) (F j)) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.timePartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => η q * w q) p - ∑ j : Fin 3, CKN.spatialSecondPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => η q * w q) j j p - ∑ j : Fin 3, CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => η q * F j q - 2 * (w q * CKN.spatialPartial η j q)) j p = w p * (CKN.timePartial η p + ∑ j : Fin 3, CKN.spatialSecondPartial η j j p) - ∑ j : Fin 3, CKN.spatialPartial η j p * F j p + η p * (CKN.timePartial w p - ∑ j : Fin 3, CKN.spatialSecondPartial w j j p - ∑ j : Fin 3, CKN.spatialPartial (F j) j p)

The residual of the localized heat equation: the product η w solves the heat equation with the flux η F - 2 w ∇η, up to lower-order cutoff terms and η times the residual of w.

theorem ESS.vorticityHeatSmooth_vec3Ball_subset (x₀ : CKN.Foundation.Parabolic.Vec3) (R : ℝ) : CKN.Foundation.Parabolic.vec3Ball x₀ R ⊆ Metric.closedBall x₀ R

Euclidean balls lie in the closed coordinate balls of the same radius.

theorem ESS.vorticityHeatSmooth_integrableOn_box {h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : Continuous h) (x₀ : CKN.Foundation.Parabolic.Vec3) (R a b : ℝ) : MeasureTheory.IntegrableOn h (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b) MeasureTheory.volume

Continuous functions are integrable on bounded boxes.

theorem ESS.vorticityHeatSmooth_integrableOn_ball {h : CKN.Foundation.Parabolic.Vec3 → ℝ} (hh : Continuous h) (x₀ : CKN.Foundation.Parabolic.Vec3) (R : ℝ) : MeasureTheory.IntegrableOn h (CKN.Foundation.Parabolic.vec3Ball x₀ R) MeasureTheory.volume

Continuous functions are integrable on Euclidean balls.

theorem ESS.vorticityHeatSmooth_boxIntegral {S : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hh : MeasureTheory.IntegrableOn h (S ×ˢ I) MeasureTheory.volume) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in S ×ˢ I, h z = ∫ (s : ℝ) in I, ∫ (x : CKN.Foundation.Parabolic.Vec3) in S, h (x, s) ∧ MeasureTheory.IntegrableOn (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3) in S, h (x, s)) I MeasureTheory.volume

Fubini on a space-time box, with the time integral outside.

theorem ESS.vorticityHeatSmooth_slice {Q : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hQ : Continuous Q) {K : Set CKN.Foundation.Parabolic.Vec3} (hK : IsCompact K) (hzero : ∀ (x : CKN.Foundation.Parabolic.Vec3) (s : ℝ), x ∉ K → Q (x, s) = 0) : (∀ (s : ℝ), MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => Q (x, s)) MeasureTheory.volume) ∧ Continuous fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), Q (x, s)

A continuous function vanishing outside a compact spatial set has integrable spatial slices and a continuous spatial integral.

theorem ESS.vorticityHeatSmooth_spatialPartial_sep {G : CKN.Foundation.Parabolic.Vec3 → ℝ} (hG : Differentiable ℝ G) (c : ℝ → ℝ) (j : Fin 3) (q : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G p.1 * c p.2) j q = CKN.spatialDeriv G j q.1 * c q.2

Spatial derivative of a separated product G(x) c(t).

theorem ESS.vorticityHeatSmooth_timePartial_sep (G : CKN.Foundation.Parabolic.Vec3 → ℝ) {c : ℝ → ℝ} (hc : Differentiable ℝ c) (q : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.timePartial (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G p.1 * c p.2) q = G q.1 * deriv c q.2

Time derivative of a separated product G(x) c(t).

theorem ESS.vorticityHeatSmooth_notMem_tsupport {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ tsupport ψ) (j k : Fin 3) : ψ x = 0 ∧ CKN.spatialDeriv ψ j x = 0 ∧ CKN.spatialDeriv (CKN.spatialDeriv ψ j) k x = 0

Outside the topological support, a function and its first two coordinate derivatives vanish.

theorem ESS.vorticityHeatSmooth_pointwise {L η W T : ℝ} {S F : Fin 3 → ℝ} (hL : 0 ≤ L) (hη : |η| ≤ 1) (hS : ∀ (j : Fin 3), |S j| ≤ L) (hT : |T| ≤ 4 * L) : 2 * ∑ j : Fin 3, ∑ _i : Fin 3, (η * F j - 2 * (W * S j)) ^ 2 + ∑ _i : Fin 3, (W * T - ∑ j : Fin 3, S j * F j) ^ 2 ≤ (12 + 336 * L ^ 2) * (W ^ 2 + ∑ j : Fin 3, F j ^ 2)

The pointwise algebra of the localized energy: the localized flux and residual are controlled by the solution and its flux, given bounds for the cutoff and its derivatives.

theorem ESS.vorticityHeatSmooth_localEnergy {r R κ : ℝ} (hr : 0 < r) (hrR : r < R) (hκ : 0 < κ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (a b : ℝ) (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (F : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), a + κ ≤ b → b ≤ a + 1 → ContDiff ℝ (↑⊤) w → (∀ (j : Fin 3), ContDiff ℝ (↑⊤) (F j)) → (∀ z ∈ CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b, CKN.timePartial w z - ∑ j : Fin 3, CKN.spatialSecondPartial w j j z = ∑ j : Fin 3, CKN.spatialPartial (F j) j z) → (∀ t ∈ Set.Icc (a + κ) b, ∫ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x₀ r, w (x, t) ^ 2 ≤ C * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b, w z ^ 2 + ∑ j : Fin 3, F j z ^ 2) ∧ ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ Set.Ioo (a + κ) b, ∑ j : Fin 3, CKN.spatialPartial w j z ^ 2 ≤ C * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ioo a b, w z ^ 2 + ∑ j : Fin 3, F j z ^ 2

Local energy estimate for smooth solutions of ∂ₜ w - Δ w = div F on B_R(x₀) × (a, b): the spatial L² norm on the inner ball at every time from a + κ to the top, and the spatial gradient in L² on the inner cylinder, are bounded by the L² norms of w and F on the whole cylinder. The constant depends only on the radii and on κ (thm:vorticity-regularity).