α : Type u_1
E : Type ?u.1069837
F : Type ?u.1069840
𝕜 : Type ?u.1069843
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.1072534
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
hfi : Integrable fun x => ↑(f x)
⊢ (∫⁻ (a : α), ↑(f a) ∂μ) = ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : α), ↑(f a) ∂μ))
α : Type u_1
E : Type ?u.1069837
F : Type ?u.1069840
𝕜 : Type ?u.1069843
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.1072534
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
hfi : Integrable fun x => ↑(f x)
⊢ (∫⁻ (a : α), ↑(f a) ∂μ) = ENNReal.ofReal (∫ (a : α), ↑(f a) ∂μ)
simp_rw [integral_eq_lintegral_of_nonneg_ae (eventually_of_forall fun x => (f x).coe_nonneg)
    hfi.aestronglyMeasurable, ← ENNReal.coe_nnreal_eq]
α : Type u_1
E : Type ?u.1069837
F : Type ?u.1069840
𝕜 : Type ?u.1069843
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.1072534
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
hfi : Integrable fun x => ↑(f x)
⊢ (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
α : Type u_1
E : Type ?u.1069837
F : Type ?u.1069840
𝕜 : Type ?u.1069843
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.1072534
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
hfi : Integrable fun x => ↑(f x)
⊢ (∫⁻ (a : α), ↑(f a) ∂μ) = ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : α), ↑(f a) ∂μ))
rw [ENNReal.ofReal_toReal]
α : Type u_1
E : Type ?u.1069837
F : Type ?u.1069840
𝕜 : Type ?u.1069843
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.1072534
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
hfi : Integrable fun x => ↑(f x)
⊢ (∫⁻ (a : α), ↑(f a) ∂μ) < ⊤
α : Type u_1
E : Type ?u.1069837
F : Type ?u.1069840
𝕜 : Type ?u.1069843
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.1072534
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
hfi : Integrable fun x => ↑(f x)
⊢ (∫⁻ (a : α), ↑(f a) ∂μ) ≠ ⊤
rw [← lt_top_iff_ne_top]
case a
α : Type u_1
E : Type ?u.1069837
F : Type ?u.1069840
𝕜 : Type ?u.1069843
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.1072534
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
hfi : Integrable fun x => ↑(f x)
⊢ (∫⁻ (a : α), ↑(f a) ∂μ) < ⊤ ↔ HasFiniteIntegral fun x => ↑(f x)
α : Type u_1
E : Type ?u.1069837
F : Type ?u.1069840
𝕜 : Type ?u.1069843
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.1072534
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
hfi : Integrable fun x => ↑(f x)
⊢ (∫⁻ (a : α), ↑(f a) ∂μ) < ⊤
convert hfi.hasFiniteIntegral
no goals
case a
α : Type u_1
E : Type ?u.1069837
F : Type ?u.1069840
𝕜 : Type ?u.1069843
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.1072534
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ≥0
hfi : Integrable fun x => ↑(f x)
⊢ (∫⁻ (a : α), ↑(f a) ∂μ) < ⊤ ↔ HasFiniteIntegral fun x => ↑(f x)
simp_rw [HasFiniteIntegral, NNReal.nnnorm_eq]