case pos
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ (∫ (a : α), f a ∂μ) = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)

case neg
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f
⊢ (∫ (a : α), f a ∂μ) = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
⊢ (∫ (a : α), f a ∂μ) = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
by_cases hfi : Integrable f μ
case pos
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
case pos
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ (∫ (a : α), f a ∂μ) = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
rw [integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi]
no goals
case pos
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
h_min : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = 0
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) =
    ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
rw [h_min, zero_toReal, _root_.sub_zero]
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ (fun a => ENNReal.ofReal (-f a)) =ᵐ[μ] 0

α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ AEMeasurable fun a => ENNReal.ofReal (-f a)
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ) = 0
rw [lintegral_eq_zero_iff']
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ f x → (fun a => ENNReal.ofReal (-f a)) x = OfNat.ofNat 0 x
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ (fun a => ENNReal.ofReal (-f a)) =ᵐ[μ] 0
refine' hf.mono _
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ ∀ (x : α), 0 ≤ f x → ENNReal.ofReal (-f x) = 0
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ ∀ (x : α), OfNat.ofNat 0 x ≤ f x → (fun a => ENNReal.ofReal (-f a)) x = OfNat.ofNat 0 x
simp only [Pi.zero_apply]
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
a : α
h : 0 ≤ f a
⊢ ENNReal.ofReal (-f a) = 0
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ ∀ (x : α), 0 ≤ f x → ENNReal.ofReal (-f x) = 0
intro a h
no goals
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
a : α
h : 0 ≤ f a
⊢ ENNReal.ofReal (-f a) = 0
simp only [h, neg_nonpos, ofReal_eq_zero]
no goals
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f
⊢ AEMeasurable fun a => ENNReal.ofReal (-f a)
exact measurable_ofReal.comp_aemeasurable hfm.aemeasurable.neg
case neg
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f
⊢ 0 = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
case neg
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f
⊢ (∫ (a : α), f a ∂μ) = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
rw [integral_undef hfi]
case neg
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
⊢ 0 = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
case neg
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f
⊢ 0 = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
simp_rw [Integrable, hfm, hasFiniteIntegral_iff_norm, lt_top_iff_ne_top, Ne.def, true_and_iff,
  Classical.not_not] at hfi
case neg
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
this : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
⊢ 0 = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
case neg
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
⊢ 0 = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
have : (∫⁻ a : α, ENNReal.ofReal (f a) ∂μ) = ∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ := by
  refine' lintegral_congr_ae (hf.mono fun a h => _)
  dsimp only
  rw [Real.norm_eq_abs, abs_of_nonneg h]
case neg
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
this : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
⊢ 0 = ENNReal.toReal ⊤
case neg
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
this : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
⊢ 0 = ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ)
rw [this, hfi]
no goals
case neg
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
this : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
⊢ 0 = ENNReal.toReal ⊤
rfl
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
a : α
h : OfNat.ofNat 0 a ≤ f a
⊢ (fun a => ENNReal.ofReal (f a)) a = (fun a => ENNReal.ofReal ‖f a‖) a
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ) = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
refine' lintegral_congr_ae (hf.mono fun a h => _)
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
a : α
h : OfNat.ofNat 0 a ≤ f a
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal ‖f a‖
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
a : α
h : OfNat.ofNat 0 a ≤ f a
⊢ (fun a => ENNReal.ofReal (f a)) a = (fun a => ENNReal.ofReal ‖f a‖) a
dsimp only
no goals
α : Type u_1
E : Type ?u.1043260
F : Type ?u.1043263
𝕜 : Type ?u.1043266
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.1045957
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ) = ⊤
a : α
h : OfNat.ofNat 0 a ≤ f a
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal ‖f a‖
rw [Real.norm_eq_abs, abs_of_nonneg h]