English
Let f : X → E be monotone on a measurable set s, and suppose s has a least element a and a greatest element b (i.e., a and b bound s from below and above). Then f is essentially bounded on s with respect to the restricted measure μ|_s; equivalently, f ∈ L∞(μ|_s).
Русский
Пусть f: X → E монотонна на измеримом множестве s и существует наименьший элемент a и наибольший элемент b в s; тогда f ограничена почти surely на s относительно меры μ, то есть f ∈ L∞(μ|_s).
LaTeX
$$$f \in L^{\\infty}(\\mu\\restriction s)$$$
Lean4
theorem memLp_top (hmono : MonotoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (h's : MeasurableSet s) :
MemLp f ∞ (μ.restrict s) := by
borelize E
have hbelow : BddBelow (f '' s) := ⟨f a, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono ha.1 hy (ha.2 hy)⟩
have habove : BddAbove (f '' s) := ⟨f b, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono hy hb.1 (hb.2 hy)⟩
have : IsBounded (f '' s) := Metric.isBounded_of_bddAbove_of_bddBelow habove hbelow
rcases isBounded_iff_forall_norm_le.mp this with ⟨C, hC⟩
have A : MemLp (fun _ => C) ⊤ (μ.restrict s) := memLp_top_const _
apply MemLp.mono A (aemeasurable_restrict_of_monotoneOn h's hmono).aestronglyMeasurable
apply (ae_restrict_iff' h's).mpr
apply ae_of_all _ fun y hy ↦ ?_
exact (hC _ (mem_image_of_mem f hy)).trans (le_abs_self _)
