Documentation

LeanPool.EscauriazaSereginSverak.PartV.ForcedHeatCriticalFinal

The critical L⁵ and L^∞ L³ bounds for the smooth forced heat response #

Letting the regularization vanish in the window estimates and applying Hölder's inequality to Y = ∫∫ |Z| |g|² gives, with B = ∫∫ |g|^{5/2},

∫∫ |Z|⁵ ≤ C B² and ∫ |Z(t)|³ ≤ C B^{6/5} for 0 ≤ t ≤ τ,

the smooth-data form of eq:pv-stokes-l5 in lem:pv-stokes, with an absolute constant C.

source
theorem ESS.response_rpow_five_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 ^ 2) ^ (5 / 2)) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))) ∧ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), (∑ i : Fin 3, responseVec g p i ^ 2) ^ (5 / 2) ∂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 space-time L⁵ integral of the response is bounded by C Y^{5/3}.

source
theorem ESS.response_rpow_three_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 ≤ τ) {t : ℝ} (ht : t ∈ Set.Icc 0 τ) :
∫ (x : CKN.Foundation.Parabolic.Vec3), (∑ i : Fin 3, responseVec g (x, t) i ^ 2) ^ (3 / 2) ≤ 3 * ∫ (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 τ))

For every time in the window, the spatial L³ integral of the response is bounded by 3 Y.

source
theorem ESS.response_forcing_holder {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 × ℝ), 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 × ℝ), (∑ i : Fin 3, responseVec g p i ^ 2) ^ (5 / 2) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ))) ^ (1 / 5) * (∫ (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)

Hölder's inequality for Y = ∫∫ |Z| |g|² with exponents 5 and 5/4.

source
noncomputable def ESS.criticalResponseConstant :
ℝ

The absolute constant of the smooth-data critical estimate.

Equations
Instances For
    source
    theorem ESS.criticalResponseConstant_nonneg :
    0 ≤ criticalResponseConstant
    source
    theorem ESS.response_critical_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) ^ (5 / 2) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 τ)) ≤ criticalResponseConstant * (∫ (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 τ))) ^ 2 ∧ ∀ t ∈ Set.Icc 0 τ, ∫ (x : CKN.Foundation.Parabolic.Vec3), (∑ i : Fin 3, responseVec g (x, t) i ^ 2) ^ (3 / 2) ≤ criticalResponseConstant * (∫ (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 τ))) ^ (6 / 5)

    The critical estimate for the smooth forced heat response: with B = ∫∫_{(0,τ]} |g|^{5/2}, ∫∫_{(0,τ]} |Z|⁵ ≤ C B² and ∫ |Z(t)|³ ≤ C B^{6/5} for 0 ≤ t ≤ τ, with an absolute constant C.