Real-valued interpolation and the regularized critical profile

The Gagliardo–Nirenberg inequality of lem:u-ten-thirds of the CKN manuscript in real integral form for continuously differentiable functions, and the elementary bounds and limits of the regularized critical profile heatRegG η and entropy heatRegEnergy η as η → 0, as used in lem:pv-stokes.

theorem ESS.integral_rpow_tenThirds_le {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ 1 f) (h2 : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => f x ^ 2) MeasureTheory.volume) (hD : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ f x) (CKN.basisVec j) ^ 2) MeasureTheory.volume) (h103 : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => |f x| ^ (10 / 3)) MeasureTheory.volume) : ∫ (x : CKN.Foundation.Parabolic.Vec3), |f x| ^ (10 / 3) ≤ CKN.gagliardoNirenbergSobolevConstant.toReal ^ 2 * (∫ (x : CKN.Foundation.Parabolic.Vec3), f x ^ 2) ^ (2 / 3) * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, (fderiv ℝ f x) (CKN.basisVec j) ^ 2

The whole-space Gagliardo–Nirenberg inequality in real integral form: ∫ |f|^{10/3} ≤ K² (∫ f²)^{2/3} ∫ |∇f|², with K the real Sobolev constant of CKN.h1_gagliardoNirenberg_tenThirds.

theorem ESS.heatRegG_nonneg_le_rpow {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) : 0 ≤ heatRegG η v ∧ heatRegG η v ≤ (∑ i : Fin 3, v i ^ 2) ^ (3 / 4)

The regularized critical profile lies between 0 and (∑ v_i²)^{3/4}.

theorem ESS.heatRegG_tendsto_rpow (v : CKN.Foundation.Parabolic.Vec3) : Filter.Tendsto (fun (η : ℝ) => heatRegG η v) (nhdsWithin 0 (Set.Ioi 0)) (nhds ((∑ i : Fin 3, v i ^ 2) ^ (3 / 4)))

As the regularization vanishes, the regularized critical profile tends to (∑ v_i²)^{3/4} = |v|^{3/2}.

theorem ESS.heatRegEnergy_tendsto_rpow (v : CKN.Foundation.Parabolic.Vec3) : Filter.Tendsto (fun (η : ℝ) => heatRegEnergy η v) (nhdsWithin 0 (Set.Ioi 0)) (nhds (1 / 3 * (∑ i : Fin 3, v i ^ 2) ^ (3 / 2)))

As the regularization vanishes, the regularized entropy tends to ⅓ (∑ v_i²)^{3/2} = ⅓ |v|³.

theorem ESS.fderiv_scalar_comp_slice_apply {φ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hφ : Differentiable ℝ φ) {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hU : ∀ (k : Fin 3), Differentiable ℝ (U k)) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (v : CKN.Foundation.Parabolic.Vec3) : (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => φ fun (k : Fin 3) => U k (y, t)) x) v = (fderiv ℝ φ fun (k : Fin 3) => U k (x, t)) fun (k : Fin 3) => (fderiv ℝ (U k) (x, t)) (v, 0)

Chain rule for a scalar map applied to a time slice of a smooth vector field.

theorem ESS.window_prod_eq (τ : ℝ) : MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ)) = (MeasureTheory.volume.prod MeasureTheory.volume).restrict (Set.univ ×ˢ Set.Ioc 0 τ)

A time window as a restriction of the space-time product measure.

theorem ESS.window_integral_mono {F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {t₁ τ : ℝ} (ht₁ : t₁ ≤ τ) (hF : MeasureTheory.Integrable F (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ)))) (hF0 : ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 ≤ F p) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), F p ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 t₁)) ≤ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), F p ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))

Integrals of a nonnegative function over growing time windows increase.