Bounds for the pressure limit #
Uniform slice and space-time L³ bounds for the blow-up velocities and their
limit, and the bookkeeping between L^(3/2) classes and seminorms used in
the pressure-limit step of prop:blowup-limit.
theorem
ESS.blowupLimitAssemblyPressure_rieszPressure_congr_ae
{F G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
(hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
(h : ∀ (i j : Fin 3), F i j =ᵐ[MeasureTheory.volume] G i j)
:
The canonical Riesz pressure depends only on the almost-everywhere class of its tensor.
theorem
ESS.blowupLimitAssemblyPressure_eLpNorm_sub_tendsto
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
[Fact (1 ≤ p)]
{f : ℕ → α → ℝ}
{g : α → ℝ}
(hf : ∀ (k : ℕ), MeasureTheory.MemLp (f k) p μ)
(hg : MeasureTheory.MemLp g p μ)
(h :
Filter.Tendsto (fun (k : ℕ) => MeasureTheory.MemLp.toLp (f k) ⋯) Filter.atTop (nhds (MeasureTheory.MemLp.toLp g hg)))
:
Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => f k x - g x) p μ) Filter.atTop (nhds 0)
Convergence of L^p classes is convergence of the L^p seminorm of the differences.
theorem
ESS.blowupLimitAssemblyPressure_velocity_slice_bound
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Mᵤ : ENNReal)
(hsourceU :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => goodPointDomain.indicator u (x, s))
MeasureTheory.volume ∧ MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (goodPointDomain.indicator u (x, s)))
3 MeasureTheory.volume ≤ Mᵤ)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ r : ℝ)
(hr : 0 < r)
:
∀ᵐ (t : ℝ), MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (blowupVelocity x₀ t₀ r u (x, t)))
3 MeasureTheory.volume ≤ Mᵤ
The zero-extended rescaled velocities have uniformly bounded global L³ slices at almost every time.
theorem
ESS.blowupLimitAssemblyPressure_memLp_three_of_slices
{w : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3}
(hw : Measurable w)
{I : Set ℝ}
{N : ENNReal}
(hslice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => w (x, t)) 3 MeasureTheory.volume ≤ N)
(S : Set CKN.Foundation.Parabolic.Vec3)
:
MeasureTheory.eLpNorm w 3 (MeasureTheory.volume.restrict (S ×ˢ I)) ≤ (MeasureTheory.volume I * N ^ 3) ^ (1 / 3)
A measurable space-time field whose slices are uniformly bounded in L³ on a finite time interval is in L³ on every product set with that time interval, with a uniform bound.