case inl
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hab : a < b
⊢ (0 < ∫ (x : ℝ) in a..b, f x ∂μ) ↔ a < b ∧ 0 < ↑↑μ (support f ∩ Ioc a b)

case inr
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ (0 < ∫ (x : ℝ) in a..b, f x ∂μ) ↔ a < b ∧ 0 < ↑↑μ (support f ∩ Ioc a b)
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ι a b)] f
hfi : IntervalIntegrable f μ a b
⊢ (0 < ∫ (x : ℝ) in a..b, f x ∂μ) ↔ a < b ∧ 0 < ↑↑μ (support f ∩ Ioc a b)
cases' lt_or_le a b with hab hba
case inl
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc a b)] f
hfi : IntervalIntegrable f μ a b
hab : a < b
⊢ (0 < ∫ (x : ℝ) in a..b, f x ∂μ) ↔ a < b ∧ 0 < ↑↑μ (support f ∩ Ioc a b)
case inl
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hab : a < b
⊢ (0 < ∫ (x : ℝ) in a..b, f x ∂μ) ↔ a < b ∧ 0 < ↑↑μ (support f ∩ Ioc a b)
rw [uIoc_of_le hab.le] at hf
no goals
case inl
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc a b)] f
hfi : IntervalIntegrable f μ a b
hab : a < b
⊢ (0 < ∫ (x : ℝ) in a..b, f x ∂μ) ↔ a < b ∧ 0 < ↑↑μ (support f ∩ Ioc a b)
simp only [hab, true_and_iff, integral_of_le hab.le,
  set_integral_pos_iff_support_of_nonneg_ae hf hfi.1]
case inr
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) ≤ 0
case inr
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ (0 < ∫ (x : ℝ) in a..b, f x ∂μ) ↔ a < b ∧ 0 < ↑↑μ (support f ∩ Ioc a b)
suffices (∫ x in a..b, f x ∂μ) ≤ 0 by simp only [this.not_lt, hba.not_lt, false_and_iff]
case inr
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ
case inr
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) ≤ 0
rw [integral_of_ge hba, neg_nonpos]
case inr
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc b a)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ
case inr
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ
rw [uIoc_comm, uIoc_of_le hba] at hf
no goals
case inr
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc b a)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ
exact integral_nonneg_of_ae hf
no goals
ι : Type ?u.19569821
𝕜 : Type ?u.19569824
E : Type ?u.19569827
F : Type ?u.19569830
A : Type ?u.19569833
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
this : (∫ (x : ℝ) in a..b, f x ∂μ) ≤ 0
⊢ (0 < ∫ (x : ℝ) in a..b, f x ∂μ) ↔ a < b ∧ 0 < ↑↑μ (support f ∩ Ioc a b)
simp only [this.not_lt, hba.not_lt, false_and_iff]