α : Type u_1
E : Type ?u.79505
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f g : α → ℝ
hf : Integrable f
hg : Integrable g
hf_le : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) ≤ ∫ (x : α) in s, g x ∂μ
⊢ 0 ≤ᵐ[μ] g - f
α : Type u_1
E : Type ?u.79505
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f g : α → ℝ
hf : Integrable f
hg : Integrable g
hf_le : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) ≤ ∫ (x : α) in s, g x ∂μ
⊢ f ≤ᵐ[μ] g
rw [← eventually_sub_nonneg]
α : Type u_1
E : Type ?u.79505
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f g : α → ℝ
hf : Integrable f
hg : Integrable g
hf_le : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, (g - f) x ∂μ
α : Type u_1
E : Type ?u.79505
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f g : α → ℝ
hf : Integrable f
hg : Integrable g
hf_le : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) ≤ ∫ (x : α) in s, g x ∂μ
⊢ 0 ≤ᵐ[μ] g - f
refine' ae_nonneg_of_forall_set_integral_nonneg (hg.sub hf) fun s hs => _
α : Type u_1
E : Type ?u.79505
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f g : α → ℝ
hf : Integrable f
hg : Integrable g
hf_le : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ s < ⊤ → (∫ (a : α) in s, f a ∂μ) ≤ ∫ (a : α) in s, g a ∂μ
α : Type u_1
E : Type ?u.79505
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f g : α → ℝ
hf : Integrable f
hg : Integrable g
hf_le : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, (g - f) x ∂μ
rw [integral_sub' hg.integrableOn hf.integrableOn, sub_nonneg]
no goals
α : Type u_1
E : Type ?u.79505
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f g : α → ℝ
hf : Integrable f
hg : Integrable g
hf_le : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ s < ⊤ → (∫ (a : α) in s, f a ∂μ) ≤ ∫ (a : α) in s, g a ∂μ
exact hf_le s hs