α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
h_and : f ≤ᵐ[Measure.restrict μ t] 0 ∧ 0 ≤ᵐ[Measure.restrict μ t] f
⊢ f =ᵐ[Measure.restrict μ t] 0

case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
⊢ f ≤ᵐ[Measure.restrict μ t] 0 ∧ 0 ≤ᵐ[Measure.restrict μ t] f
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
⊢ f =ᵐ[Measure.restrict μ t] 0
suffices h_and : f ≤ᵐ[μ.restrict t] 0 ∧ 0 ≤ᵐ[μ.restrict t] f
case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
⊢ f ≤ᵐ[Measure.restrict μ t] 0 ∧ 0 ≤ᵐ[Measure.restrict μ t] f
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
h_and : f ≤ᵐ[Measure.restrict μ t] 0 ∧ 0 ≤ᵐ[Measure.restrict μ t] f
⊢ f =ᵐ[Measure.restrict μ t] 0

case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
⊢ f ≤ᵐ[Measure.restrict μ t] 0 ∧ 0 ≤ᵐ[Measure.restrict μ t] f
exact h_and.1.mp (h_and.2.mono fun x hx1 hx2 => le_antisymm hx2 hx1)
case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
⊢ f ≤ᵐ[Measure.restrict μ t] 0
case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
⊢ f ≤ᵐ[Measure.restrict μ t] 0 ∧ 0 ≤ᵐ[Measure.restrict μ t] f
refine'
  ⟨_,
    ae_nonneg_restrict_of_forall_set_integral_nonneg hf_int_finite
      (fun s hs hμs => (hf_zero s hs hμs).symm.le) ht hμt⟩
case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
h_neg : 0 ≤ᵐ[Measure.restrict μ t] -f
⊢ f ≤ᵐ[Measure.restrict μ t] 0

case h_neg
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
⊢ 0 ≤ᵐ[Measure.restrict μ t] -f
case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
⊢ f ≤ᵐ[Measure.restrict μ t] 0
suffices h_neg : 0 ≤ᵐ[μ.restrict t] -f
case h_neg
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, (-f) x ∂μ
case h_neg
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
⊢ 0 ≤ᵐ[Measure.restrict μ t] -f
refine'
  ae_nonneg_restrict_of_forall_set_integral_nonneg (fun s hs hμs => (hf_int_finite s hs hμs).neg)
    (fun s hs hμs => _) ht hμt
case h_neg
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, -f x ∂μ
case h_neg
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, (-f) x ∂μ
simp_rw [Pi.neg_apply]
case h_neg
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ (∫ (a : α) in s, f a ∂μ) ≤ 0
case h_neg
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ 0 ≤ ∫ (x : α) in s, -f x ∂μ
rw [integral_neg, neg_nonneg]
no goals
case h_neg
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s✝ t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ (∫ (a : α) in s, f a ∂μ) ≤ 0
exact (hf_zero s hs hμs).le
case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
h_neg : 0 ≤ᵐ[Measure.restrict μ t] -f
x : α
hx : OfNat.ofNat 0 x ≤ (-f) x
⊢ f x ≤ OfNat.ofNat 0 x
case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
h_neg : 0 ≤ᵐ[Measure.restrict μ t] -f
⊢ f ≤ᵐ[Measure.restrict μ t] 0
refine' h_neg.mono fun x hx => _
case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
h_neg : 0 ≤ᵐ[Measure.restrict μ t] -f
x : α
hx : OfNat.ofNat 0 x ≤ -f x
⊢ f x ≤ OfNat.ofNat 0 x
case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
h_neg : 0 ≤ᵐ[Measure.restrict μ t] -f
x : α
hx : OfNat.ofNat 0 x ≤ (-f) x
⊢ f x ≤ OfNat.ofNat 0 x
rw [Pi.neg_apply] at hx
no goals
case h_and
α : Type u_1
E : Type ?u.89319
m m0 : MeasurableSpace α
μ : Measure α
s t✝ : Set α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : ℝ≥0∞
f✝ f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → IntegrableOn f s
hf_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s < ⊤ → (∫ (x : α) in s, f x ∂μ) = 0
t : Set α
ht : MeasurableSet t
hμt : ↑↑μ t ≠ ⊤
h_neg : 0 ≤ᵐ[Measure.restrict μ t] -f
x : α
hx : OfNat.ofNat 0 x ≤ -f x
⊢ f x ≤ OfNat.ofNat 0 x
simpa using hx