The quadratic heat energy for smooth compact data

For smooth compactly supported data the Gaussian heat orbit satisfies the energy identity d/dt ∫ |h|² = -2 ∫ |∇h|². Integrating it in time gives the energy bounds used for the L^{10/3} part of lem:pv-heat-critical.

theorem ESS.heatConvVec3_sq_integral_hasDerivAt {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, heatConvVec3 s b x i ^ 2) (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, 2 * heatConvVec3 t b x i * CKN.Foundation.Heat.heatConv t (CKN.spatialLaplacian fun (y : CKN.Foundation.Parabolic.Vec3) => b y i) x) t

The quadratic energy of a smooth compact vector heat orbit differentiates in time with the heat-equation derivative, as used in lem:pv-heat-critical.

theorem ESS.heatConvVec3_sq_integral_derivative_eq {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) {t : ℝ} (ht : 0 < t) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, 2 * heatConvVec3 t b x i * CKN.Foundation.Heat.heatConv t (CKN.spatialLaplacian fun (y : CKN.Foundation.Parabolic.Vec3) => b y i) x = -(2 * ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x ^ 2)

Spatial integration by parts identifies the quadratic energy derivative with minus twice the Dirichlet energy, as used in lem:pv-heat-critical.

theorem ESS.heatConvVec3_sq_integral_tendsto_initial {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, heatConvVec3 t b x i ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2))

The quadratic energy of a smooth compact vector heat orbit converges to its initial value as time decreases to zero.

theorem ESS.heatConvVec3_energy_bound {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) {τ : ℝ} (hτ : 0 < τ) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, heatConvVec3 τ b x i ^ 2 ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2 ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 τ, ENNReal.ofReal (2 * ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x ^ 2) ≤ ENNReal.ofReal (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, b x i ^ 2)

Time integration of the quadratic energy identity: the energy does not increase and twice the Dirichlet energy integrated over (0, τ) is bounded by the initial energy, as used in lem:pv-heat-critical.