Blowup Compactness Boundary #
Compactness of the rescaled fields in the endpoint regularity argument.
theorem
ESS.blowup_tendstoInMeasure_of_local_exhaustion
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[PseudoEMetricSpace E]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(S : ℕ → Set α)
(hSm : ∀ (n : ℕ), MeasurableSet (S n))
(hSmono : Monotone S)
(hcover : μ (⋃ (n : ℕ), S n)ᶜ = 0)
(f : ℕ → α → E)
(g : α → E)
(hlocal : ∀ (n : ℕ), MeasureTheory.TendstoInMeasure (μ.restrict (S n)) f Filter.atTop g)
:
On a finite-measure cylinder, convergence in measure on every member of an increasing measurable exhaustion gives convergence in measure globally.
theorem
ESS.blowup_tendstoInMeasure_to_time_zero
{E : Type u_1}
[PseudoEMetricSpace E]
(A : Set CKN.Foundation.Parabolic.Vec3)
(hA : MeasurableSet A)
(hAfin : MeasureTheory.volume A < ⊤)
(a : ℝ)
(f : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → E)
(g : CKN.Foundation.Parabolic.Vec3 × ℝ → E)
(hlocal :
∀ b < 0,
MeasureTheory.TendstoInMeasure ((MeasureTheory.volume.prod MeasureTheory.volume).restrict (A ×ˢ Set.Ioo a b)) f
Filter.atTop g)
:
Convergence in measure on every finite past subcylinder extends to the open cylinder ending at time zero.
theorem
ESS.blowup_tendstoInMeasure_to_time_zero_of_local_Ltwo
(A : Set CKN.Foundation.Parabolic.Vec3)
(hA : MeasurableSet A)
(hAfin : MeasureTheory.volume A < ⊤)
(a : ℝ)
(f : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3)
(g : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3)
(hlocal :
∀ b < 0,
Filter.Tendsto
(fun (k : ℕ) =>
MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f k z - g z) 2
((MeasureTheory.volume.prod MeasureTheory.volume).restrict (A ×ˢ Set.Ioo a b)))
Filter.atTop (nhds 0))
:
Strong local L² convergence below time zero implies convergence in
measure on the full bounded open past cylinder.