English
If hm is a trimming of σ-algebras m ≤ m0, then limsup of f with respect to ae μ trimmed equals limsup with ae μ, for measurable f.
Русский
Если hm — обрезание σ-алгебр m ≤ m0, то limsup f по ae μ, обрезанному hm, равен limsup f по ae μ для измеримой f.
LaTeX
$$limsup f (ae (μ.trim hm)) = limsup f (ae μ)$$
Lean4
theorem limsup_trim (hm : m ≤ m0) {f : α → ℝ≥0∞} (hf : Measurable[m] f) : limsup f (ae (μ.trim hm)) = limsup f (ae μ) :=
by
simp_rw [limsup_eq]
suffices h_set_eq : {a : ℝ≥0∞ | ∀ᵐ n ∂μ.trim hm, f n ≤ a} = {a : ℝ≥0∞ | ∀ᵐ n ∂μ, f n ≤ a} by rw [h_set_eq]
ext1 a
suffices h_meas_eq : μ {x | ¬f x ≤ a} = μ.trim hm {x | ¬f x ≤ a} by simp_rw [Set.mem_setOf_eq, ae_iff, h_meas_eq]
refine (trim_measurableSet_eq hm ?_).symm
exact (measurableSet_le hf measurable_const).compl
