Heat Entropy H1

The regularized entropy profile of smooth heat data is in whole-space H¹.

noncomputable def ESS.heatRegGCompH1 {η : ℝ} (hη : 0 < η) {h : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hh : ContDiff ℝ (↑⊤) h) (hmem : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => h x i) 2 MeasureTheory.volume) (hderiv : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ h x) (CKN.basisVec j) i) 2 MeasureTheory.volume) {M : ℝ} (hM : 0 ≤ M) (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (h x) ≤ M) : CKN.H1Function Set.univ

The H1 function obtained by composing a smooth finite-energy field with the entropy map.

Equations

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

noncomputable def ESS.heatRegGHeatConvH1 {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) (hη : 0 < η) : CKN.H1Function Set.univ

The regularized entropy profile of smooth heat data is in whole-space H¹.

Equations

• ESS.heatRegGHeatConvH1 hb hbc ht hη = ESS.heatRegGCompH1 hη ⋯ ⋯ ⋯ ⋯ ⋯

theorem ESS.heatConvVec3_norm_decay {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) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ {t : ℝ}, 0 < t → ∀ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (heatConvVec3 t b x) ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 3

Smooth compact vector data have uniform positive-time spatial decay.

theorem ESS.heatConvVec3_spatialDeriv_decay_constants {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) : ∃ (C : Fin 3 → Fin 3 → ℝ), (∀ (i j : Fin 3), 0 ≤ C i j) ∧ ∀ {t : ℝ}, 0 < t → ∀ (x : CKN.Foundation.Parabolic.Vec3) (i j : Fin 3), |CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x| ≤ C i j / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 3

First spatial derivatives of smooth compact heat data have polynomial decay.

theorem ESS.heat_decay_six_integrable (C : ℝ) (hC : 0 ≤ C) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => C / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 6) MeasureTheory.volume

Polynomial decay of order six gives an integrable whole-space majorant.