case pos
α : Type u_1
E : Type u_2
F : Type ?u.691352
G : Type ?u.691355
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : ↑↑μ s ≠ 0
hp_top : p = ⊤
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * ENNReal.toReal (↑↑μ s) ^ (1 / ENNReal.toReal p)

case neg
α : Type u_1
E : Type u_2
F : Type ?u.691352
G : Type ?u.691355
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : ↑↑μ s ≠ 0
hp_top : ¬p = ⊤
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * ENNReal.toReal (↑↑μ s) ^ (1 / ENNReal.toReal p)
α : Type u_1
E : Type u_2
F : Type ?u.691352
G : Type ?u.691355
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : ↑↑μ s ≠ 0
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * ENNReal.toReal (↑↑μ s) ^ (1 / ENNReal.toReal p)
by_cases hp_top : p = ∞
case pos
α : Type u_1
E : Type u_2
F : Type ?u.691352
G : Type ?u.691355
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : ↑↑μ s ≠ 0
hp_top : p = ⊤
⊢ ‖indicatorConstLp ⊤ hs hμs c‖ = ‖c‖
case pos
α : Type u_1
E : Type u_2
F : Type ?u.691352
G : Type ?u.691355
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : ↑↑μ s ≠ 0
hp_top : p = ⊤
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * ENNReal.toReal (↑↑μ s) ^ (1 / ENNReal.toReal p)
rw [hp_top, ENNReal.top_toReal, _root_.div_zero, Real.rpow_zero, mul_one]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.691352
G : Type ?u.691355
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : ↑↑μ s ≠ 0
hp_top : p = ⊤
⊢ ‖indicatorConstLp ⊤ hs hμs c‖ = ‖c‖
exact norm_indicatorConstLp_top hμs_pos
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.691352
G : Type ?u.691355
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : ↑↑μ s ≠ 0
hp_top : ¬p = ⊤
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * ENNReal.toReal (↑↑μ s) ^ (1 / ENNReal.toReal p)
exact norm_indicatorConstLp hp_pos hp_top