Convergence of the whole-space pressures

Strong local L³ convergence of velocities with uniformly bounded global L³ slices gives strong local L^(3/2) convergence of their whole-space Riesz pressures (prop:blowup-limit, pressure-limit step): the pressure of the tensor near a large ball converges by the L^(3/2) bound of the double Riesz transforms, and the pressure of the far tensor is uniformly small.

theorem ESS.blowupLimitAssemblyPressure_indicator_time_window (U : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) {A : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (J : Set ℝ) (hA : A ⊆ Set.univ ×ˢ J) (i j : Fin 3) : A.indicator ((Set.univ ×ˢ J).indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => U z i * U z j) = A.indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => U z i * U z j

Truncating a time-truncated tensor to a smaller set inside the time window is the truncation of the original tensor.

theorem ESS.blowupLimitAssemblyPressure_mass_to_eLpNorm {μ : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)} {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : Measurable f) {ε : ENNReal} (hmass : ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal |f z| ^ (3 / 2) ∂μ ≤ ε) : MeasureTheory.eLpNorm f (ENNReal.ofReal (3 / 2)) μ ≤ ε ^ (2 / 3)

The norm of a canonical pressure class restricted to a set is the L^(3/2) seminorm of the representative.

theorem ESS.blowupLimitAssemblyPressure_riesz_tendsto (vs : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (hvs : ∀ (k : ℕ), Measurable (vs k)) (U : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (hU : Measurable U) {a : ℝ} (ha : a < 0) {N : ENNReal} (hN : N < ⊤) (hslice : ∀ (k : ℕ), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a 0), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => vs k (x, t)) 3 MeasureTheory.volume ≤ N) (hUslice : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a 0), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t)) 3 MeasureTheory.volume ≤ N) (hconv : ∀ (L : ℝ), 0 < L → Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => vs k z - U z) 3 (MeasureTheory.volume.restrict (CKN.euclideanBall 0 L ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)) (hF : ∀ (k : ℕ) (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => vs k z i * vs k z j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp ((Set.univ ×ˢ Set.Ioo a 0).indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => U z i * U z j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) {R : ℝ} (hR : 0 < R) : Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Leray.rieszPressureSpaceTime (3 / 2) blowupLimitAssemblyPressure_riesz_tendsto._proof_1 (fun (i j : Fin 3) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => vs k z i * vs k z j) ⋯ z - CKN.Leray.rieszPressureSpaceTime (3 / 2) blowupLimitAssemblyPressure_riesz_tendsto._proof_1 (fun (i j : Fin 3) => (Set.univ ×ˢ Set.Ioo a 0).indicator fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => U z i * U z j) hG z) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (CKN.euclideanBall 0 R ×ˢ Set.Ioo a 0))) Filter.atTop (nhds 0)

Strong local convergence of pressures from strong local L³ convergence of velocities with uniform global L³ slice bounds on a past time window.