α : Type u_2
E : Type u_1
F : Type ?u.964234
𝕜 : Type ?u.964237
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
⊢ ENNReal.ofReal ‖∫ (a : α), f a ∂μ‖ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
α : Type u_2
E : Type u_1
F : Type ?u.964234
𝕜 : Type ?u.964237
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 ∂μ‖₊ ≤ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ
simp_rw [← ofReal_norm_eq_coe_nnnorm]
case h
α : Type u_2
E : Type u_1
F : Type ?u.964234
𝕜 : Type ?u.964237
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‖ ∂μ)
α : Type u_2
E : Type u_1
F : Type ?u.964234
𝕜 : Type ?u.964237
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
⊢ ENNReal.ofReal ‖∫ (a : α), f a ∂μ‖ ≤ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
apply ENNReal.ofReal_le_of_le_toReal
no goals
case h
α : Type u_2
E : Type u_1
F : Type ?u.964234
𝕜 : Type ?u.964237
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‖ ∂μ)
exact norm_integral_le_lintegral_norm f