ι : Type ?u.20041361
𝕜 : Type ?u.20041364
E : Type ?u.20041367
F : Type ?u.20041370
A : Type ?u.20041373
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[Measure.restrict μ (Ioc a b)] g
hlt : ↑↑(Measure.restrict μ (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 < ↑↑(Measure.restrict μ (Ioc a b)) (support fun x => g x - f x)

case hf
ι : Type ?u.20041361
𝕜 : Type ?u.20041364
E : Type ?u.20041367
F : Type ?u.20041370
A : Type ?u.20041373
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[Measure.restrict μ (Ioc a b)] g
hlt : ↑↑(Measure.restrict μ (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 ≤ᵐ[Measure.restrict μ (Ioc a b)] fun x => g x - f x

case hfi
ι : Type ?u.20041361
𝕜 : Type ?u.20041364
E : Type ?u.20041367
F : Type ?u.20041370
A : Type ?u.20041373
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[Measure.restrict μ (Ioc a b)] g
hlt : ↑↑(Measure.restrict μ (Ioc a b)) {x | f x < g x} ≠ 0
⊢ Integrable fun x => g x - f x
ι : Type ?u.20041361
𝕜 : Type ?u.20041364
E : Type ?u.20041367
F : Type ?u.20041370
A : Type ?u.20041373
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[Measure.restrict μ (Ioc a b)] g
hlt : ↑↑(Measure.restrict μ (Ioc a b)) {x | f x < g x} ≠ 0
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) < ∫ (x : ℝ) in a..b, g x ∂μ
rw [← sub_pos, ← integral_sub hgi hfi, integral_of_le hab,
  MeasureTheory.integral_pos_iff_support_of_nonneg_ae]
no goals
case hf
ι : Type ?u.20041361
𝕜 : Type ?u.20041364
E : Type ?u.20041367
F : Type ?u.20041370
A : Type ?u.20041373
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[Measure.restrict μ (Ioc a b)] g
hlt : ↑↑(Measure.restrict μ (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 ≤ᵐ[Measure.restrict μ (Ioc a b)] fun x => g x - f x

case hfi
ι : Type ?u.20041361
𝕜 : Type ?u.20041364
E : Type ?u.20041367
F : Type ?u.20041370
A : Type ?u.20041373
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[Measure.restrict μ (Ioc a b)] g
hlt : ↑↑(Measure.restrict μ (Ioc a b)) {x | f x < g x} ≠ 0
⊢ Integrable fun x => g x - f x
exacts [hle.mono fun x => sub_nonneg.2, hgi.1.sub hfi.1]
ι : Type ?u.20041361
𝕜 : Type ?u.20041364
E : Type ?u.20041367
F : Type ?u.20041370
A : Type ?u.20041373
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[Measure.restrict μ (Ioc a b)] g
hlt : ↑↑(Measure.restrict μ (Ioc a b)) {x | f x < g x} ≠ 0
⊢ {x | f x < g x} ⊆ support fun x => g x - f x
ι : Type ?u.20041361
𝕜 : Type ?u.20041364
E : Type ?u.20041367
F : Type ?u.20041370
A : Type ?u.20041373
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[Measure.restrict μ (Ioc a b)] g
hlt : ↑↑(Measure.restrict μ (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 < ↑↑(Measure.restrict μ (Ioc a b)) (support fun x => g x - f x)
refine' pos_iff_ne_zero.2 (mt (measure_mono_null _) hlt)
no goals
ι : Type ?u.20041361
𝕜 : Type ?u.20041364
E : Type ?u.20041367
F : Type ?u.20041370
A : Type ?u.20041373
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[Measure.restrict μ (Ioc a b)] g
hlt : ↑↑(Measure.restrict μ (Ioc a b)) {x | f x < g x} ≠ 0
⊢ {x | f x < g x} ⊆ support fun x => g x - f x
exact fun x hx => (sub_pos.2 hx.out).ne'