Leray Limit Tail Limit #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.lerayLimit_lintegral_bound_of_compactExhaustion
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{μ : MeasureTheory.Measure α}
(S : Set α)
(K : ℕ → Set α)
(hK : MeasureTheory.AECover (μ.restrict S) Filter.atTop K)
(F : ℕ → α → E)
(G : α → E)
(B : ENNReal)
(hFbound : ∀ (m n : ℕ), ∫⁻ (x : α) in K m, ‖F n x‖ₑ ^ 2 ∂μ.restrict S ≤ B)
(htransfer :
∀ (m : ℕ),
(∀ (n : ℕ), ∫⁻ (x : α) in K m, ‖F n x‖ₑ ^ 2 ∂μ.restrict S ≤ B) → ∫⁻ (x : α) in K m, ‖G x‖ₑ ^ 2 ∂μ.restrict S ≤ B)
(hG : AEMeasurable G (μ.restrict S))
:
A uniform bound on an exhaustion passes to a measurable limit when the bound is lower semicontinuous on each member of that exhaustion.