α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
⊢ (∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
⊢ ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
simp_rw [integral_congr_ae (show f =ᵐ[μ] fun x => ‖f x‖ by
    filter_upwards [f_nn]with x hx
    rw [Real.norm_eq_abs, abs_eq_self.mpr hx]),
  ofReal_integral_norm_eq_lintegral_nnnorm hfi, ← ofReal_norm_eq_coe_nnnorm]
case h
α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
⊢ (fun a => ENNReal.ofReal ‖f a‖) =ᵐ[μ] fun a => ENNReal.ofReal (f a)
α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
⊢ (∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
apply lintegral_congr_ae
case h
α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
x : α
hx : OfNat.ofNat 0 x ≤ f x
⊢ ENNReal.ofReal ‖f x‖ = ENNReal.ofReal (f x)
case h
α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
⊢ (fun a => ENNReal.ofReal ‖f a‖) =ᵐ[μ] fun a => ENNReal.ofReal (f a)
filter_upwards [f_nn]with x hx
no goals
case h
α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
x : α
hx : OfNat.ofNat 0 x ≤ f x
⊢ ENNReal.ofReal ‖f x‖ = ENNReal.ofReal (f x)
exact congr_arg ENNReal.ofReal (by rw [Real.norm_eq_abs, abs_eq_self.mpr hx])
case h
α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
x : α
hx : OfNat.ofNat 0 x ≤ f x
⊢ f x = ‖f x‖
α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
⊢ f =ᵐ[μ] fun x => ‖f x‖
filter_upwards [f_nn]with x hx
no goals
case h
α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
x : α
hx : OfNat.ofNat 0 x ≤ f x
⊢ f x = ‖f x‖
rw [Real.norm_eq_abs, abs_eq_self.mpr hx]
no goals
α : Type u_1
E : Type ?u.1079546
F : Type ?u.1079549
𝕜 : Type ?u.1079552
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.1082243
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hfi : Integrable f
f_nn : 0 ≤ᵐ[μ] f
x : α
hx : OfNat.ofNat 0 x ≤ f x
⊢ ‖f x‖ = f x
rw [Real.norm_eq_abs, abs_eq_self.mpr hx]