α : Type u_1
E : Type ?u.81134
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
t : Set α
hf : IntegrableOn f t
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : ↑↑(Measure.restrict μ t) s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, f x ∂Measure.restrict μ t
α : Type u_1
E : Type ?u.81134
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
t : Set α
hf : IntegrableOn f t
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
⊢ 0 ≤ᵐ[Measure.restrict μ t] f
refine' ae_nonneg_of_forall_set_integral_nonneg hf fun s hs h's => _
α : Type u_1
E : Type ?u.81134
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
t : Set α
hf : IntegrableOn f t
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : ↑↑(Measure.restrict μ t) s < ⊤
⊢ 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
α : Type u_1
E : Type ?u.81134
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
t : Set α
hf : IntegrableOn f t
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : ↑↑(Measure.restrict μ t) s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, f x ∂Measure.restrict μ t
simp_rw [Measure.restrict_restrict hs]
α : Type u_1
E : Type ?u.81134
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
t : Set α
hf : IntegrableOn f t
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : ↑↑(Measure.restrict μ t) s < ⊤
⊢ ↑↑μ (s ∩ t) < ⊤
α : Type u_1
E : Type ?u.81134
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
t : Set α
hf : IntegrableOn f t
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : ↑↑(Measure.restrict μ t) s < ⊤
⊢ 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
apply hf_zero s hs
no goals
α : Type u_1
E : Type ?u.81134
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
t : Set α
hf : IntegrableOn f t
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ (s ∩ t) < ⊤ → 0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
s : Set α
hs : MeasurableSet s
h's : ↑↑(Measure.restrict μ t) s < ⊤
⊢ ↑↑μ (s ∩ t) < ⊤
rwa [Measure.restrict_apply hs] at h's