α : Type u_2
E : Type ?u.1049026
F : Type ?u.1049029
𝕜 : Type ?u.1049032
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 α
X : Type ?u.1051723
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
G : Type u_1
inst✝ : NormedAddCommGroup G
f : α → G
hf : AEStronglyMeasurable f μ
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ENNReal.toReal (∫⁻ (x : α), ↑‖f x‖₊ ∂μ)

α : Type u_2
E : Type ?u.1049026
F : Type ?u.1049029
𝕜 : Type ?u.1049032
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 α
X : Type ?u.1051723
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
G : Type u_1
inst✝ : NormedAddCommGroup G
f : α → G
hf : AEStronglyMeasurable f μ
⊢ 0 ≤ᵐ[μ] fun x => ‖f x‖
α : Type u_2
E : Type ?u.1049026
F : Type ?u.1049029
𝕜 : Type ?u.1049032
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 α
X : Type ?u.1051723
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
G : Type u_1
inst✝ : NormedAddCommGroup G
f : α → G
hf : AEStronglyMeasurable f μ
⊢ (∫ (x : α), ‖f x‖ ∂μ) = ENNReal.toReal (∫⁻ (x : α), ↑‖f x‖₊ ∂μ)
rw [integral_eq_lintegral_of_nonneg_ae _ hf.norm]
no goals
α : Type u_2
E : Type ?u.1049026
F : Type ?u.1049029
𝕜 : Type ?u.1049032
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 α
X : Type ?u.1051723
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
G : Type u_1
inst✝ : NormedAddCommGroup G
f : α → G
hf : AEStronglyMeasurable f μ
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ENNReal.toReal (∫⁻ (x : α), ↑‖f x‖₊ ∂μ)
simp_rw [ofReal_norm_eq_coe_nnnorm]
α : Type u_2
E : Type ?u.1049026
F : Type ?u.1049029
𝕜 : Type ?u.1049032
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 α
X : Type ?u.1051723
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
G : Type u_1
inst✝ : NormedAddCommGroup G
f : α → G
hf : AEStronglyMeasurable f μ
⊢ ∀ (a : α), OfNat.ofNat 0 a ≤ (fun x => ‖f x‖) a
α : Type u_2
E : Type ?u.1049026
F : Type ?u.1049029
𝕜 : Type ?u.1049032
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 α
X : Type ?u.1051723
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
G : Type u_1
inst✝ : NormedAddCommGroup G
f : α → G
hf : AEStronglyMeasurable f μ
⊢ 0 ≤ᵐ[μ] fun x => ‖f x‖
refine' ae_of_all _ _
no goals
α : Type u_2
E : Type ?u.1049026
F : Type ?u.1049029
𝕜 : Type ?u.1049032
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 α
X : Type ?u.1051723
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
G : Type u_1
inst✝ : NormedAddCommGroup G
f : α → G
hf : AEStronglyMeasurable f μ
⊢ ∀ (a : α), OfNat.ofNat 0 a ≤ (fun x => ‖f x‖) a
simp_rw [Pi.zero_apply, norm_nonneg, imp_true_iff]