case intro.intro
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
⊢ 0 ≤ᵐ[μ] f
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ 0 ≤ᵐ[μ] f
rcases hf.1 with ⟨f', hf'_meas, hf_ae⟩
case intro.intro
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
hf'_integrable : Integrable f'
⊢ 0 ≤ᵐ[μ] f
case intro.intro
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
⊢ 0 ≤ᵐ[μ] f
have hf'_integrable : Integrable f' μ := Integrable.congr hf hf_ae
case intro.intro
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
hf'_integrable : Integrable f'
hf'_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f' x ∂μ
⊢ 0 ≤ᵐ[μ] f
case intro.intro
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
hf'_integrable : Integrable f'
⊢ 0 ≤ᵐ[μ] f
have hf'_zero : ∀ s, MeasurableSet s → μ s < ∞ → 0 ≤ ∫ x in s, f' x ∂μ := by
  intro s hs h's
  rw [set_integral_congr_ae hs (hf_ae.mono fun x hx _ => hx.symm)]
  exact hf_zero s hs h's
no goals
case intro.intro
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
hf'_integrable : Integrable f'
hf'_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f' x ∂μ
⊢ 0 ≤ᵐ[μ] f
exact
  (ae_nonneg_of_forall_set_integral_nonneg_of_stronglyMeasurable hf'_meas hf'_integrable
        hf'_zero).trans
    hf_ae.symm.le
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
hf'_integrable : Integrable f'
s : Set α
hs : MeasurableSet s
h's : ↑↑μ s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, f' x ∂μ
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
hf'_integrable : Integrable f'
⊢ ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f' x ∂μ
intro s hs h's
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
hf'_integrable : Integrable f'
s : Set α
hs : MeasurableSet s
h's : ↑↑μ s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
hf'_integrable : Integrable f'
s : Set α
hs : MeasurableSet s
h's : ↑↑μ s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, f' x ∂μ
rw [set_integral_congr_ae hs (hf_ae.mono fun x hx _ => hx.symm)]
no goals
α : Type u_1
E : Type ?u.77645
m m0 : MeasurableSpace α
μ : Measure α
s✝ t : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f : α → ℝ
hf : Integrable f
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
f' : α → ℝ
hf'_meas : StronglyMeasurable f'
hf_ae : f =ᵐ[μ] f'
hf'_integrable : Integrable f'
s : Set α
hs : MeasurableSet s
h's : ↑↑μ s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ
exact hf_zero s hs h's