α : Type u_1
E : Type ?u.631037
F : Type ?u.631040
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs : MeasurableSet s✝
c : E
f✝ : α → E
hf : AEStronglyMeasurable f✝ μ
s : Set α
f : α → G
x : α
⊢ (fun x => ↑‖Set.indicator s f x‖₊) x ≤ (fun x => ↑‖f x‖₊) x
α : Type u_1
E : Type ?u.631037
F : Type ?u.631040
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs : MeasurableSet s✝
c : E
f✝ : α → E
hf : AEStronglyMeasurable f✝ μ
s : Set α
f : α → G
⊢ snormEssSup (Set.indicator s f) μ ≤ snormEssSup f μ
refine' essSup_mono_ae (eventually_of_forall fun x => _)
α : Type u_1
E : Type ?u.631037
F : Type ?u.631040
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs : MeasurableSet s✝
c : E
f✝ : α → E
hf : AEStronglyMeasurable f✝ μ
s : Set α
f : α → G
x : α
⊢ Set.indicator s (fun a => ‖f a‖₊) x ≤ ‖f x‖₊
α : Type u_1
E : Type ?u.631037
F : Type ?u.631040
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs : MeasurableSet s✝
c : E
f✝ : α → E
hf : AEStronglyMeasurable f✝ μ
s : Set α
f : α → G
x : α
⊢ (fun x => ↑‖Set.indicator s f x‖₊) x ≤ (fun x => ↑‖f x‖₊) x
rw [ENNReal.coe_le_coe, nnnorm_indicator_eq_indicator_nnnorm]
no goals
α : Type u_1
E : Type ?u.631037
F : Type ?u.631040
G : Type u_2
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s✝ : Set α
hs : MeasurableSet s✝
c : E
f✝ : α → E
hf : AEStronglyMeasurable f✝ μ
s : Set α
f : α → G
x : α
⊢ Set.indicator s (fun a => ‖f a‖₊) x ≤ ‖f x‖₊
exact Set.indicator_le_self s _ x