The critical L⁵ bound for smooth heat data

For smooth compactly supported data the regularized profile g_η = (|h|² + η²)^{3/4} - η^{3/2} satisfies, by the entropy identity, sup_t ‖g_η(t)‖₂² + ∫∫ |∇g_η|² ≤ C ∫ E_η(b). The Gagliardo–Nirenberg inequality eq:gn-ten-thirds of the CKN manuscript at each time then bounds ∫∫ g_η^{10/3}, and Fatou's lemma as η → 0 gives the estimate eq:pv-heat-l5 of lem:pv-heat-critical for smooth compact data.

theorem ESS.h1_tenThirds_lintegral_le (H : CKN.H1Function Set.univ) : ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖H.toFun x‖ₑ ^ (10 / 3) ≤ CKN.gagliardoNirenbergSobolevConstant ^ 2 * (MeasureTheory.eLpNorm H.toFun 2 MeasureTheory.volume ^ 2) ^ (2 / 3) * MeasureTheory.eLpNorm (fun (x : CKN.Vec 3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (H.grad x)) 2 MeasureTheory.volume ^ 2

The Gagliardo–Nirenberg inequality eq:gn-ten-thirds of the CKN manuscript in power form for a whole-space H¹ function.

theorem ESS.heatRegG_nonneg {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) : 0 ≤ heatRegG η v

The regularized critical profile is nonnegative.

theorem ESS.heatRegG_tenThirds_slice {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), ‖heatRegG η (heatConvVec3 t b x)‖ₑ ^ (10 / 3) ≤ CKN.gagliardoNirenbergSobolevConstant ^ 2 * ENNReal.ofReal (27 * ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (b x)) ^ (2 / 3) * ENNReal.ofReal (9 / 2 * ∑ 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)

One time slice of the regularized profile: the Gagliardo–Nirenberg inequality combined with the entropy bound and the pointwise gradient bound.

theorem ESS.heatRegG_tenThirds_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 < τ) (hη : 0 < η) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), ‖heatRegG η (heatOrbit b z)‖ₑ ^ (10 / 3) ≤ CKN.gagliardoNirenbergSobolevConstant ^ 2 * ENNReal.ofReal (27 * ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (b x)) ^ (2 / 3) * ENNReal.ofReal (9 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (b x))

The space-time L^{10/3} integral of the regularized profile over ℝ³ × (0, τ) is bounded by its initial entropy, uniformly in τ.

theorem ESS.ofReal_integral_euclidean_cube_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) : ENNReal.ofReal (∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (b x) ^ 3) ≤ ENNReal.ofReal (√3 ^ 3) * MeasureTheory.eLpNorm b 3 MeasureTheory.volume ^ 3

The cubic Euclidean integral of smooth compact data is bounded by the cube of its L³ norm, up to the norm-comparison constant.

theorem ESS.heatOrbit_five_lintegral_smooth {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 < τ) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (heatOrbit b z)) ^ 5 ≤ CKN.gagliardoNirenbergSobolevConstant ^ 2 * ENNReal.ofReal (27 * (1 / 3 * ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (b x) ^ 3)) ^ (2 / 3) * ENNReal.ofReal (9 / 2 * (1 / 3 * ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (b x) ^ 3))

Fatou's lemma as the regularization vanishes: the space-time quintic integral of a smooth compact heat orbit is bounded by the limit of the regularized bounds.

theorem ESS.heatOrbit_five_smooth : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), (∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) → (∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) → ∀ (τ : ℝ), 0 < τ → MeasureTheory.eLpNorm (heatOrbit b) 5 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm b 3 MeasureTheory.volume

The critical estimate eq:pv-heat-l5 for smooth compact data: ‖S(·)b‖_{L⁵(Q_τ)} ≤ C‖b‖₃ with C independent of τ.