Slice estimates for the regularized critical test

At each time the Gagliardo–Nirenberg inequality applied to the regularized critical profile heatRegG η (Z) bounds its L^{10/3} norm by the regularized entropy and the entropy dissipation; over a time window the regularized critical inequality bounds both by Y = ∫∫ |Z| |g|². These are the two inputs of the critical estimate in lem:pv-stokes.

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

A continuous function on Vec3 bounded by C (1 + |x|)^{-6} is integrable.

theorem ESS.heatRegTest_dissipation_ge {η : ℝ} (hη : 0 < η) (v a : CKN.Foundation.Parabolic.Vec3) : (heatRegSq η v ^ (1 / 2) - η) * ∑ i : Fin 3, a i ^ 2 ≤ ∑ i : Fin 3, (fderiv ℝ (heatRegTest η) v) a i * a i

The entropy dissipation of the regularized critical test dominates the weighted squared gradient.

theorem ESS.response_sq_decay {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ∀ (i j : Fin 3), ContDiff ℝ (↑⊤) (g i j)) (hgc : ∀ (i j : Fin 3), HasCompactSupport (g i j)) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (responseVec g p) ≤ M ∧ ∑ i : Fin 3, responseVec g p i ^ 2 ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm p.1) ^ 6

The squared response q = ∑ Z_i² has a (1 + |x|)^{-6} bound, uniformly in time.

theorem ESS.response_critical_window_bounds {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ∀ (i j : Fin 3), ContDiff ℝ (↑⊤) (g i j)) (hgc : ∀ (i j : Fin 3), HasCompactSupport (g i j)) (hgpos : ∀ (i j : Fin 3), tsupport (g i j) ⊆ {p : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < p.2}) {η : ℝ} (hη : 0 < η) {τ : ℝ} (hτ : 0 ≤ τ) : (∀ t ∈ Set.Icc 0 τ, ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (responseVec g (x, t)) ≤ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (responseVec g p) * ∑ i : Fin 3, ∑ j : Fin 3, g i j p ^ 2 ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))) ∧ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ j : Fin 3, ∑ i : Fin 3, (fderiv ℝ (heatRegTest η) (responseVec g p)) (responseGrad g j p) i * responseGrad g j p i ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ)) ≤ 2 * ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (responseVec g p) * ∑ i : Fin 3, ∑ j : Fin 3, g i j p ^ 2 ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))

Over a time window the regularized entropy at every time and the dissipation are bounded by Y = ∫∫ |Z| |g|².

theorem ESS.response_critical_slice_gn {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ∀ (i j : Fin 3), ContDiff ℝ (↑⊤) (g i j)) (hgc : ∀ (i j : Fin 3), HasCompactSupport (g i j)) {η : ℝ} (hη : 0 < η) (t : ℝ) : ∫ (x : CKN.Foundation.Parabolic.Vec3), |heatRegG η (responseVec g (x, t))| ^ (10 / 3) ≤ CKN.gagliardoNirenbergSobolevConstant.toReal ^ 2 * (27 * ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (responseVec g (x, t))) ^ (2 / 3) * (9 / 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, ∑ i : Fin 3, (fderiv ℝ (heatRegTest η) (responseVec g (x, t))) (responseGrad g j (x, t)) i * responseGrad g j (x, t) i)

At each time, the Gagliardo–Nirenberg inequality for the regularized critical profile: its L^{10/3} norm is controlled by the regularized entropy and the entropy dissipation.