Blowup Riesz Time Local

Pressure reconstruction and convergence bounds for the rescaled sequence.

theorem ESS.blowup_rieszPressureSpaceTime_time_indicator_ae (F : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (J : Set ℝ) (hJ : MeasurableSet J) : let S := Set.univ ×ˢ J; let G := fun (i j : Fin 3) => S.indicator (F i j); have hG := ⋯; S.indicator (CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_time_indicator_ae._proof_1 F hF) =ᵐ[MeasureTheory.volume] S.indicator (CKN.Leray.rieszPressureSpaceTime (3 / 2) blowup_rieszPressureSpaceTime_time_indicator_ae._proof_1 G hG)

Restricting a tensor to a measurable time set does not change its Riesz pressure on that set, as a space-time almost-everywhere identity.