Energy bounds for the heat orbit of an L² datum

The Gaussian convolution is an L² contraction, so the spatial L² norm of the heat orbit is bounded by that of the datum at every positive time. For the gradient, the energy inequality ∫₀^τ ‖∇h‖₂² ≤ ½‖a‖₂² holds for the smooth compactly supported approximants of a datum in J, and passes to the heat orbit of the datum by Fatou's lemma, since the gradients converge pointwise. These are the energy clauses of the heat orbit in prop:pv-local-solution.

theorem ESS.heatConvGrad_tendsto_of_eLpNorm {fs : ℕ → CKN.Foundation.Parabolic.Vec3 → ℝ} {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hfs : ∀ (n : ℕ), MeasureTheory.MemLp (fs n) 2 MeasureTheory.volume) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fs n - f) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) {t : ℝ} (ht : 0 < t) (j : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : Filter.Tendsto (fun (n : ℕ) => heatConvGrad t (fs n) j x) Filter.atTop (nhds (heatConvGrad t f j x))

Convolution with a kernel derivative is continuous in the datum for the L² norm, pointwise at each positive time.

theorem ESS.heatOrbit_slice_lintegral_le {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) {s : ℝ} (hs : 0 < s) : ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖heatOrbit a (x, s)‖ₑ ^ 2 ≤ ∑ i : Fin 3, MeasureTheory.eLpNorm (fun (y : CKN.Foundation.Parabolic.Vec3) => a y i) 2 MeasureTheory.volume ^ 2

The L² contraction of the heat flow on the heat orbit of an L² datum: at every positive time the spatial square integral is bounded by the sum of the squared L² norms of the components of the datum.

theorem ESS.heatConvVec3_grad_lintegral_le {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 < τ) : ∫⁻ (t : ℝ) in Set.Ioo 0 τ, ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, ‖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)

The time-integrated Dirichlet energy of the heat orbit of smooth compactly supported data is bounded by the initial energy.

theorem ESS.heatOrbit_energy_lintegral_lt_top {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsInJ a) {τ : ℝ} (hτ : 0 < τ) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), ‖heatOrbit a z‖ₑ ^ 2 + ‖fun (i j : Fin 3) => CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatOrbit a (y, z.2) i) j z.1‖ₑ ^ 2 < ⊤

(h3) The heat orbit of a datum in J has finite energy on every slab ℝ³ × (0, τ): the space-time integral of |h|² + |∇h|² is finite.