case pos
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
hfm : AEStronglyMeasurable f μ
⊢ (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), g a ∂μ

case neg
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
hfm : ¬AEStronglyMeasurable f μ
⊢ (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), g a ∂μ
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
⊢ (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), g a ∂μ
by_cases hfm : AEStronglyMeasurable f μ
case pos
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
hfm : AEStronglyMeasurable f μ
⊢ HasFiniteIntegral fun a => f a
case pos
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
hfm : AEStronglyMeasurable f μ
⊢ (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), g a ∂μ
refine' integral_mono_ae ⟨hfm, _⟩ hgi h
case pos
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf✝ : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
hfm : AEStronglyMeasurable f μ
x : α
hf : OfNat.ofNat 0 x ≤ f x
hfg : f x ≤ g x
⊢ ‖f x‖ ≤ ‖g x‖
case pos
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
hfm : AEStronglyMeasurable f μ
⊢ HasFiniteIntegral fun a => f a
refine' hgi.hasFiniteIntegral.mono <| h.mp <| hf.mono fun x hf hfg => _
no goals
case pos
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf✝ : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
hfm : AEStronglyMeasurable f μ
x : α
hf : OfNat.ofNat 0 x ≤ f x
hfg : f x ≤ g x
⊢ ‖f x‖ ≤ ‖g x‖
simpa [abs_of_nonneg hf, abs_of_nonneg (le_trans hf hfg)]
case neg
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
hfm : ¬AEStronglyMeasurable f μ
⊢ 0 ≤ ∫ (a : α), g a ∂μ
case neg
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
hfm : ¬AEStronglyMeasurable f μ
⊢ (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), g a ∂μ
rw [integral_non_aestronglyMeasurable hfm]
no goals
case neg
α : Type u_1
E : Type ?u.1228980
F : Type ?u.1228983
𝕜 : Type ?u.1228986
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.1231677
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f g : α → ℝ
hf : 0 ≤ᵐ[μ] f
hgi : Integrable g
h : f ≤ᵐ[μ] g
hfm : ¬AEStronglyMeasurable f μ
⊢ 0 ≤ ∫ (a : α), g a ∂μ
exact integral_nonneg_of_ae (hf.trans h)