The L⁴ bound for the smooth forced heat response #
The energy estimate and the Gagliardo–Nirenberg inequality give
∫∫ |Z|^{10/3} ≤ C (∫∫ |g|²)^{5/3}; interpolating with the critical L⁵
bound gives ∫∫ |Z|⁴ ≤ C (∫∫ |g|²) (∫∫ |g|^{5/2})^{4/5}, the smooth-data form
of eq:pv-stokes-l4 in lem:pv-stokes.
theorem
ESS.response_tenThirds_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 ≤ τ)
:
MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, |responseVec g p i| ^ (10 / 3))
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))) ∧ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3,
|responseVec g p i| ^ (10 / 3) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ)) ≤ CKN.gagliardoNirenbergSobolevConstant.toReal ^ 2 * (∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3,
∑ j : Fin 3, g i j p ^ 2 ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))) ^ (5 / 3)
The space-time L^{10/3} bound of the smooth forced heat response in terms
of the space-time L² norm of the tensor.
The absolute constant of the smooth-data L⁴ estimate.
Equations
- ESS.responseL4Constant = (3 ^ (2 / 3) * CKN.gagliardoNirenbergSobolevConstant.toReal ^ 2) ^ (3 / 5) * ESS.criticalResponseConstant ^ (2 / 5)
Instances For
theorem
ESS.response_L4_estimate
{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 ≤ τ)
:
∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), (∑ i : Fin 3, responseVec g p i ^ 2) ^ 2 ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ)) ≤ (responseL4Constant * ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ 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 × ℝ), (∑ i : Fin 3, ∑ j : Fin 3, g i j p ^ 2) ^ (5 / 4) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))) ^ (4 / 5)
The L⁴ estimate for the smooth forced heat response:
∫∫ |Z|⁴ ≤ C (∫∫ |g|²) (∫∫ |g|^{5/2})^{4/5} with an absolute constant C.