case pos
α : Type u_1
β : Type u_2
γ : Type ?u.835159
δ : Type ?u.835162
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : p = 0
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.835159
δ : Type ?u.835162
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : ¬p = 0
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
α : Type u_1
β : Type u_2
γ : Type ?u.835159
δ : Type ?u.835162
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
by_cases h_zero : p = 0
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.835159
δ : Type ?u.835162
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : ¬p = 0
h_top : p = ⊤
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.835159
δ : Type ?u.835162
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : ¬p = 0
h_top : ¬p = ⊤
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.835159
δ : Type ?u.835162
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : ¬p = 0
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
by_cases h_top : p = ∞
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.835159
δ : Type ?u.835162
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : ¬p = 0
h_top : ¬p = ⊤
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
exact hf.integrable_norm_rpow h_zero h_top
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.835159
δ : Type ?u.835162
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : p = 0
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
simp [h_zero, integrable_const]
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.835159
δ : Type ?u.835162
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : Memℒp f p
h_zero : ¬p = 0
h_top : p = ⊤
⊢ Integrable fun x => ‖f x‖ ^ ENNReal.toReal p
simp [h_top, integrable_const]