case pos
α : Type u_2
E : Type u_1
F : Type ?u.960408
𝕜 : Type ?u.960411
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ)

case neg
α : Type u_2
E : Type u_1
F : Type ?u.960408
𝕜 : Type ?u.960411
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : ¬Integrable f
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ)
α : Type u_2
E : Type u_1
F : Type ?u.960408
𝕜 : Type ?u.960411
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : α → E
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ)
by_cases hf : Integrable f μ
case pos
α : Type u_2
E : Type u_1
F : Type ?u.960408
𝕜 : Type ?u.960411
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f
⊢ ‖L1.integral (Integrable.toL1 f hf)‖ ≤ ‖Integrable.toL1 f hf‖
case pos
α : Type u_2
E : Type u_1
F : Type ?u.960408
𝕜 : Type ?u.960411
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ)
rw [integral_eq f hf, ← Integrable.norm_toL1_eq_lintegral_norm f hf]
no goals
case pos
α : Type u_2
E : Type u_1
F : Type ?u.960408
𝕜 : Type ?u.960411
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f
⊢ ‖L1.integral (Integrable.toL1 f hf)‖ ≤ ‖Integrable.toL1 f hf‖
exact L1.norm_integral_le _
case neg
α : Type u_2
E : Type u_1
F : Type ?u.960408
𝕜 : Type ?u.960411
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : ¬Integrable f
⊢ 0 ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ)
case neg
α : Type u_2
E : Type u_1
F : Type ?u.960408
𝕜 : Type ?u.960411
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : ¬Integrable f
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ)
rw [integral_undef hf, norm_zero]
no goals
case neg
α : Type u_2
E : Type u_1
F : Type ?u.960408
𝕜 : Type ?u.960411
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : ¬Integrable f
⊢ 0 ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ)
exact toReal_nonneg