The critical estimate for the smooth forced heat response #
Integrating the slice Gagliardo–Nirenberg estimate in time, letting the
regularization vanish, and applying Hölder's inequality to
Y = ∫∫ |Z| |g|² gives
∫∫ |Z|⁵ ≤ C (∫∫ |g|^{5/2})², sup_t ∫ |Z(t)|³ ≤ C (∫∫ |g|^{5/2})^{6/5},
the smooth-data form of eq:pv-stokes-l5 in lem:pv-stokes, with an absolute
constant C.
The absolute constant 9 κ² 27^{2/3} of the critical estimate, with κ the
real Sobolev constant.
Equations
- ESS.criticalGNConstant = 9 * CKN.gagliardoNirenbergSobolevConstant.toReal ^ 2 * 27 ^ (2 / 3)
Instances For
theorem
ESS.response_critical_profile_window_le
{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 ≤ τ)
:
∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |heatRegG η (responseVec g p)| ^ (10 / 3) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ)) ≤ criticalGNConstant * (∫ (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 τ))) ^ (5 / 3)
The regularized critical profile, integrated over a time window, is bounded
by C Y^{5/3} with Y = ∫∫ |Z| |g|².