English
If a bound C controls finite measurable sets in a subspace and the directed union of finite-measure sets behaves nicely, then the bound holds on the whole space.
Русский
Если ограничение C действует на все конечные измеримые множества в подпространстве и объединение таких множеств ведёт себя хорошо, то ограничение распространяется на всю пространство.
LaTeX
$$f(UNIV) ≤ C under directed finite-measure cover$$
Lean4
theorem univ_le_of_forall_fin_meas_le {μ : Measure α} (hm : m ≤ m0) [SigmaFinite (μ.trim hm)] (C : ℝ≥0∞)
{f : Set α → ℝ≥0∞} (hf : ∀ s, MeasurableSet[m] s → μ s ≠ ∞ → f s ≤ C)
(h_F_lim : ∀ S : ℕ → Set α, (∀ n, MeasurableSet[m] (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)) :
f univ ≤ C := by
let S := @spanningSets _ m (μ.trim hm) _
have hS_mono : Monotone S := @monotone_spanningSets _ m (μ.trim hm) _
have hS_meas : ∀ n, MeasurableSet[m] (S n) := @measurableSet_spanningSets _ m (μ.trim hm) _
rw [← @iUnion_spanningSets _ m (μ.trim hm)]
refine (h_F_lim S hS_meas hS_mono).trans ?_
refine iSup_le fun n => hf (S n) (hS_meas n) ?_
exact ((le_trim hm).trans_lt (@measure_spanningSets_lt_top _ m (μ.trim hm) _ n)).ne
