case pos
α : Type u_1
E : Type ?u.633107
F : Type ?u.633110
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 α
c : G
hμ0 : μ = 0
⊢ snormEssSup (Set.indicator s fun x => c) μ ≤ ↑‖c‖₊

case neg
α : Type u_1
E : Type ?u.633107
F : Type ?u.633110
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 α
c : G
hμ0 : ¬μ = 0
⊢ snormEssSup (Set.indicator s fun x => c) μ ≤ ↑‖c‖₊
α : Type u_1
E : Type ?u.633107
F : Type ?u.633110
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 α
c : G
⊢ snormEssSup (Set.indicator s fun x => c) μ ≤ ↑‖c‖₊
by_cases hμ0 : μ = 0
case pos
α : Type u_1
E : Type ?u.633107
F : Type ?u.633110
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 α
c : G
hμ0 : μ = 0
⊢ 0 ≤ ↑‖c‖₊
case pos
α : Type u_1
E : Type ?u.633107
F : Type ?u.633110
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 α
c : G
hμ0 : μ = 0
⊢ snormEssSup (Set.indicator s fun x => c) μ ≤ ↑‖c‖₊
rw [hμ0, snormEssSup_measure_zero]
no goals
case pos
α : Type u_1
E : Type ?u.633107
F : Type ?u.633110
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 α
c : G
hμ0 : μ = 0
⊢ 0 ≤ ↑‖c‖₊
exact zero_le _
no goals
case neg
α : Type u_1
E : Type ?u.633107
F : Type ?u.633110
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 α
c : G
hμ0 : ¬μ = 0
⊢ snormEssSup (Set.indicator s fun x => c) μ ≤ ↑‖c‖₊
exact (snormEssSup_indicator_le s fun _ => c).trans (snormEssSup_const c hμ0).le