-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem MonotoneOn.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)

Proof state:
case intro
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (fun x => C) ⊤ (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ ‖C‖

Tactic:
apply ae_of_all _ fun y hy ↦ ?_

Result:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (fun x => C) ⊤ (μ.restrict s)
y : X
hy : y ∈ s
⊢ ‖f y‖ ≤ ‖C‖

Proof state:
case intro
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (fun x => C) ⊤ (μ.restrict s)
⊢ MemLp f ⊤ (μ.restrict s)

Tactic:
apply MemLp.mono A (aemeasurable_restrict_of_monotoneOn h's hmono).aestronglyMeasurable

Result:
case intro
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (fun x => C) ⊤ (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ ‖C‖

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
C : ℝ
hC : ∀ x ∈ f '' s, ‖x‖ ≤ C
A : MemLp (fun x => C) ⊤ (μ.restrict s)
y : X
hy : y ∈ s
⊢ ‖f y‖ ≤ ‖C‖

Tactic:
exact (hC _ (mem_image_of_mem f hy)).trans (le_abs_self _)

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
⊢ MemLp f ⊤ (μ.restrict s)

Tactic:
have : IsBounded (f '' s) := Metric.isBounded_of_bddAbove_of_bddBelow habove hbelow

Result:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
habove : BddAbove (f '' s)
this : IsBounded (f '' s)
⊢ MemLp f ⊤ (μ.restrict s)

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MemLp f ⊤ (μ.restrict s)

Tactic:
have hbelow : BddBelow (f '' s) := ⟨f a, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono ha.1 hy (ha.2 hy)⟩

Result:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hbelow : BddBelow (f '' s)
⊢ MemLp f ⊤ (μ.restrict s)