α : Type u_2
E✝ : Type ?u.638627
F : Type ?u.638630
G : Type ?u.638633
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✝ μ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : α → E
x : α
⊢ ‖Set.indicator s f x‖ ≤ ‖f x‖
α : Type u_2
E✝ : Type ?u.638627
F : Type ?u.638630
G : Type ?u.638633
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✝ μ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : α → E
⊢ snorm (Set.indicator s f) p μ ≤ snorm f p μ
refine' snorm_mono_ae (eventually_of_forall fun x => _)
α : Type u_2
E✝ : Type ?u.638627
F : Type ?u.638630
G : Type ?u.638633
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✝ μ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : α → E
x : α
⊢ ‖Set.indicator s f x‖₊ ≤ ‖f x‖₊
α : Type u_2
E✝ : Type ?u.638627
F : Type ?u.638630
G : Type ?u.638633
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✝ μ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : α → E
x : α
⊢ ‖Set.indicator s f x‖ ≤ ‖f x‖
suffices ‖s.indicator f x‖₊ ≤ ‖f x‖₊ by exact NNReal.coe_mono this
α : Type u_2
E✝ : Type ?u.638627
F : Type ?u.638630
G : Type ?u.638633
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✝ μ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : α → E
x : α
⊢ Set.indicator s (fun a => ‖f a‖₊) x ≤ ‖f x‖₊
α : Type u_2
E✝ : Type ?u.638627
F : Type ?u.638630
G : Type ?u.638633
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✝ μ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : α → E
x : α
⊢ ‖Set.indicator s f x‖₊ ≤ ‖f x‖₊
rw [nnnorm_indicator_eq_indicator_nnnorm]
no goals
α : Type u_2
E✝ : Type ?u.638627
F : Type ?u.638630
G : Type ?u.638633
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✝ μ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : α → E
x : α
⊢ Set.indicator s (fun a => ‖f a‖₊) x ≤ ‖f x‖₊
exact s.indicator_le_self _ x
no goals
α : Type u_2
E✝ : Type ?u.638627
F : Type ?u.638630
G : Type ?u.638633
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✝ μ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : α → E
x : α
this : ‖Set.indicator s f x‖₊ ≤ ‖f x‖₊
⊢ ‖Set.indicator s f x‖ ≤ ‖f x‖
exact NNReal.coe_mono this