Heat Critical Smooth

A continuous function with sixth-order polynomial decay is integrable on the whole space, as used in lem:pv-heat-critical.

theorem ESS.heat_integrable_of_decay_six {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : Continuous f) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), |f x| ≤ C / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 6) : MeasureTheory.Integrable f MeasureTheory.volume

A continuous function with sixth-order polynomial decay is integrable on the whole space, as used in lem:pv-heat-critical.

theorem ESS.integral_scalar_spatialLaplacian_ibp {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfg : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * CKN.spatialDeriv g j x) MeasureTheory.volume) (hfg' : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.spatialDeriv g j y) j x) MeasureTheory.volume) (hf'g : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialDeriv f j x * CKN.spatialDeriv g j x) MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), f x * CKN.spatialLaplacian g x = -∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv f j x * CKN.spatialDeriv g j x

Whole-space integration by parts against the spatial Laplacian for smooth functions with integrable products, as used in lem:pv-heat-critical.

theorem ESS.heatConvVec3_firstDeriv_uniform_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) : ∃ (D : ℝ), 0 ≤ D ∧ ∀ {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| ≤ D / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 3

First spatial derivatives of a smooth compact vector heat orbit have cubic decay uniformly in positive time.

theorem ESS.heatConvVec3_fderiv_basis_apply {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 j : Fin 3) : (fderiv ℝ (heatConvVec3 t b) x) (CKN.basisVec j) i = CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x

The vector-valued heat derivative agrees componentwise with CKN's spatial derivative, as used in lem:pv-heat-critical.

noncomputable def ESS.heatSpatialDerivativeInput (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (j : Fin 3) : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3

The coordinate spatial derivative of the vector field supplied to heat convolution.

Equations

• ESS.heatSpatialDerivativeInput b j x i = CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => b y i) j x

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

Diagonal second spatial derivatives of a smooth compact vector heat orbit have cubic decay uniformly in positive time.

theorem ESS.heatRegTest_heatConv_dissipation_integrable {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 < η) : (∀ (i j : Fin 3), MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegTest η (heatConvVec3 t b y) i) j x * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x) MeasureTheory.volume) ∧ MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegTest η (heatConvVec3 t b y) i) j x * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x) MeasureTheory.volume

The spatial entropy-dissipation density of a smooth heat orbit is integrable, as used in lem:pv-heat-critical.

theorem ESS.heatRegEnergy_integral_derivative_eq_neg_gradient {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 < η) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, heatRegTest η (heatConvVec3 t b x) i * CKN.Foundation.Heat.heatConv t (CKN.spatialLaplacian fun (y : CKN.Foundation.Parabolic.Vec3) => b y i) x = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegTest η (heatConvVec3 t b y) i) j x * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x

Spatial integration by parts expresses the entropy derivative pairing as minus the nonnegative dissipation in lem:pv-heat-critical.

theorem ESS.heatRegEnergy_integral_antitoneOn {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 < η) : AntitoneOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (heatConvVec3 t b x)) (Set.Ioi 0)

The regularized entropy integral decreases on positive times, as used in lem:pv-heat-critical.

theorem ESS.heatRegEnergy_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) (η : ℝ) (hη : 0 < η) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (heatConvVec3 t b x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (b x)))

The regularized entropy integrals converge to their initial value as time decreases to zero, as used in lem:pv-heat-critical.

theorem ESS.heatRegEnergy_integral_le_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) {t η : ℝ} (ht : 0 < t) (hη : 0 < η) : ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (heatConvVec3 t b x) ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (b x)

The regularized entropy of a smooth heat orbit is bounded by its initial entropy; this is the time-integrated form used in lem:pv-heat-critical.