case pos
α : Type u_1
E : Type ?u.645570
F : Type ?u.645573
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 μ
c : G
hs : MeasurableSet s
hμs : ↑↑μ s ≠ 0
hp : p ≠ 0
hp_top : p = ⊤
⊢ snorm (Set.indicator s fun x => c) p μ = ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)

case neg
α : Type u_1
E : Type ?u.645570
F : Type ?u.645573
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 μ
c : G
hs : MeasurableSet s
hμs : ↑↑μ s ≠ 0
hp : p ≠ 0
hp_top : ¬p = ⊤
⊢ snorm (Set.indicator s fun x => c) p μ = ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
α : Type u_1
E : Type ?u.645570
F : Type ?u.645573
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 μ
c : G
hs : MeasurableSet s
hμs : ↑↑μ s ≠ 0
hp : p ≠ 0
⊢ snorm (Set.indicator s fun x => c) p μ = ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
by_cases hp_top : p = ∞
no goals
case pos
α : Type u_1
E : Type ?u.645570
F : Type ?u.645573
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 μ
c : G
hs : MeasurableSet s
hμs : ↑↑μ s ≠ 0
hp : p ≠ 0
hp_top : p = ⊤
⊢ snorm (Set.indicator s fun x => c) p μ = ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
simp [hp_top, snormEssSup_indicator_const_eq s c hμs]
no goals
case neg
α : Type u_1
E : Type ?u.645570
F : Type ?u.645573
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 μ
c : G
hs : MeasurableSet s
hμs : ↑↑μ s ≠ 0
hp : p ≠ 0
hp_top : ¬p = ⊤
⊢ snorm (Set.indicator s fun x => c) p μ = ↑‖c‖₊ * ↑↑μ s ^ (1 / ENNReal.toReal p)
exact snorm_indicator_const hs hp hp_top