[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i in Finset.range a, f (x₀ + ↑i)
[PROOFSTEP]
have hint : ∀ k : ℕ, k < a → IntervalIntegrable f volume (x₀ + k) (x₀ + (k + 1 : ℕ)) :=
  by
  intro k hk
  refine' (hf.mono _).intervalIntegrable
  rw [uIcc_of_le]
  · apply Icc_subset_Icc
    · simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
    · simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
  · simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
[PROOFSTEP]
intro k hk
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
[PROOFSTEP]
refine' (hf.mono _).intervalIntegrable
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ uIcc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
rw [uIcc_of_le]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ Icc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
apply Icc_subset_Icc
[GOAL]
case h₁
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ ≤ x₀ + ↑k
[PROOFSTEP]
simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
[GOAL]
case h₂
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ + ↑(k + 1) ≤ x₀ + ↑a
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ + ↑k ≤ x₀ + ↑(k + 1)
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i in Finset.range a, f (x₀ + ↑i)
[PROOFSTEP]
calc
  ∫ x in x₀..x₀ + a, f x = ∑ i in Finset.range a, ∫ x in x₀ + i..x₀ + (i + 1 : ℕ), f x :=
    by
    convert (intervalIntegral.sum_integral_adjacent_intervals hint).symm
    simp only [Nat.cast_zero, add_zero]
  _ ≤ ∑ i in Finset.range a, ∫ _ in x₀ + i..x₀ + (i + 1 : ℕ), f (x₀ + i) :=
    by
    apply Finset.sum_le_sum fun i hi => ?_
    have ia : i < a := Finset.mem_range.1 hi
    refine' intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => _
    apply hf _ _ hx.1
    ·
      simp only [ia.le, mem_Icc, le_add_iff_nonneg_right, Nat.cast_nonneg, add_le_add_iff_left, Nat.cast_le,
        and_self_iff]
    · refine' mem_Icc.2 ⟨le_trans (by simp) hx.1, le_trans hx.2 _⟩
      simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt ia]
  _ = ∑ i in Finset.range a, f (x₀ + i) := by simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x = ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x
[PROOFSTEP]
convert (intervalIntegral.sum_integral_adjacent_intervals hint).symm
[GOAL]
case h.e'_2.h.e'_5
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ x₀ = x₀ + ↑0
[PROOFSTEP]
simp only [Nat.cast_zero, add_zero]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x ≤
    ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i)
[PROOFSTEP]
apply Finset.sum_le_sum fun i hi => ?_
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i)
[PROOFSTEP]
have ia : i < a := Finset.mem_range.1 hi
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i)
[PROOFSTEP]
refine' intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => _
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
⊢ x₀ + ↑i ≤ x₀ + ↑(i + 1)
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
⊢ IntervalIntegrable (fun x => f (x₀ + ↑i)) volume (x₀ + ↑i) (x₀ + ↑(i + 1))
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ f x ≤ f (x₀ + ↑i)
[PROOFSTEP]
apply hf _ _ hx.1
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ + ↑i ∈ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
simp only [ia.le, mem_Icc, le_add_iff_nonneg_right, Nat.cast_nonneg, add_le_add_iff_left, Nat.cast_le, and_self_iff]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x ∈ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
refine' mem_Icc.2 ⟨le_trans (by simp) hx.1, le_trans hx.2 _⟩
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ ≤ x₀ + ↑i
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ + ↑(i + 1) ≤ x₀ + ↑a
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt ia]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i) = ∑ i in Finset.range a, f (x₀ + ↑i)
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ x in Finset.Ico a b, f ↑x
[PROOFSTEP]
rw [(Nat.sub_add_cancel hab).symm, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x ≤ ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
conv =>
  congr
  congr
  ·skip
  ·skip
  rw [add_comm]
  ·skip
  ·skip
  congr
  congr
  rw [← zero_add a]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x ≤ ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
  congr
  congr
  ·skip
  ·skip
  rw [add_comm]
  ·skip
  ·skip
  congr
  congr
  rw [← zero_add a]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x ≤ ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
  congr
  congr
  ·skip
  ·skip
  rw [add_comm]
  ·skip
  ·skip
  congr
  congr
  rw [← zero_add a]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x ≤ ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
congr
[GOAL]
case a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
congr
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f x
case a.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑(b - a) + ↑a
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
·skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f x
[PROOFSTEP]
skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f x
[PROOFSTEP]
skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f x
[PROOFSTEP]
skip
[GOAL]
case a.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑(b - a) + ↑a
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
·skip
[GOAL]
case a.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a
[PROOFSTEP]
skip
[GOAL]
case a.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a
[PROOFSTEP]
skip
[GOAL]
case a.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a
[PROOFSTEP]
skip
[GOAL]
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑(b - a) + ↑a
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
rw [add_comm]
[GOAL]
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a + ↑(b - a)
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
·skip
[GOAL]
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a + ↑(b - a)
[PROOFSTEP]
skip
[GOAL]
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a + ↑(b - a)
[PROOFSTEP]
skip
[GOAL]
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a + ↑(b - a)
[PROOFSTEP]
skip
[GOAL]
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
·skip
[GOAL]
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
[PROOFSTEP]
skip
[GOAL]
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
[PROOFSTEP]
skip
[GOAL]
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
[PROOFSTEP]
skip
[GOAL]
case a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
congr
[GOAL]
case a.s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.Ico a (b - a + a)
case a.f x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | fun x => f ↑x
[PROOFSTEP]
congr
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| a
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
case a.f x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | fun x => f ↑x
[PROOFSTEP]
rw [← zero_add a]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.Ico (0 + a) (b - a + a), f ↑x
[PROOFSTEP]
rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.range (b - a), f ↑(a + x)
[PROOFSTEP]
conv =>
  rhs
  congr
  ·skip
  ext
  rw [Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.range (b - a), f ↑(a + x)
[PROOFSTEP]
  rhs
  congr
  ·skip
  ext
  rw [Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.range (b - a), f ↑(a + x)
[PROOFSTEP]
  rhs
  congr
  ·skip
  ext
  rw [Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.range (b - a), f ↑(a + x)
[PROOFSTEP]
rhs
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.range (b - a), f ↑(a + x)
[PROOFSTEP]
congr
[GOAL]
case s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.range (b - a)
case f x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | fun x => f ↑(a + x)
[PROOFSTEP]
·skip
[GOAL]
case s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.range (b - a)
[PROOFSTEP]
skip
[GOAL]
case s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.range (b - a)
[PROOFSTEP]
skip
[GOAL]
case s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.range (b - a)
[PROOFSTEP]
skip
[GOAL]
case f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f ↑(a + x)
[PROOFSTEP]
ext
[GOAL]
case f.h
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
x✝ : ℕ
| f ↑(a + x✝)
[PROOFSTEP]
rw [Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.range (b - a), f (↑a + ↑x)
[PROOFSTEP]
apply AntitoneOn.integral_le_sum
[GOAL]
case hf
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ AntitoneOn (fun x => f x) (Icc (↑a) (↑a + ↑(b - a)))
[PROOFSTEP]
simp only [hf, hab, Nat.cast_sub, add_sub_cancel'_right]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i in Finset.range a, f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
[PROOFSTEP]
have hint : ∀ k : ℕ, k < a → IntervalIntegrable f volume (x₀ + k) (x₀ + (k + 1 : ℕ)) :=
  by
  intro k hk
  refine' (hf.mono _).intervalIntegrable
  rw [uIcc_of_le]
  · apply Icc_subset_Icc
    · simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
    · simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
  · simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
[PROOFSTEP]
intro k hk
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
[PROOFSTEP]
refine' (hf.mono _).intervalIntegrable
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ uIcc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
rw [uIcc_of_le]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ Icc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
apply Icc_subset_Icc
[GOAL]
case h₁
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ ≤ x₀ + ↑k
[PROOFSTEP]
simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
[GOAL]
case h₂
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ + ↑(k + 1) ≤ x₀ + ↑a
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ + ↑k ≤ x₀ + ↑(k + 1)
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
[PROOFSTEP]
calc
  (∑ i in Finset.range a, f (x₀ + (i + 1 : ℕ))) =
      ∑ i in Finset.range a, ∫ _ in x₀ + i..x₀ + (i + 1 : ℕ), f (x₀ + (i + 1 : ℕ)) :=
    by simp
  _ ≤ ∑ i in Finset.range a, ∫ x in x₀ + i..x₀ + (i + 1 : ℕ), f x :=
    by
    apply Finset.sum_le_sum fun i hi => ?_
    have ia : i + 1 ≤ a := Finset.mem_range.1 hi
    refine' intervalIntegral.integral_mono_on (by simp) (by simp) (hint _ ia) fun x hx => _
    apply hf _ _ hx.2
    · refine' mem_Icc.2 ⟨le_trans ((le_add_iff_nonneg_right _).2 (Nat.cast_nonneg _)) hx.1, le_trans hx.2 _⟩
      simp only [Nat.cast_le, add_le_add_iff_left, ia]
    · refine' mem_Icc.2 ⟨(le_add_iff_nonneg_right _).2 (Nat.cast_nonneg _), _⟩
      simp only [add_le_add_iff_left, Nat.cast_le, ia]
  _ = ∫ x in x₀..x₀ + a, f x :=
    by
    convert intervalIntegral.sum_integral_adjacent_intervals hint
    simp only [Nat.cast_zero, add_zero]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, f (x₀ + ↑(i + 1)) =
    ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1))
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤
    ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x
[PROOFSTEP]
apply Finset.sum_le_sum fun i hi => ?_
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x
[PROOFSTEP]
have ia : i + 1 ≤ a := Finset.mem_range.1 hi
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x
[PROOFSTEP]
refine' intervalIntegral.integral_mono_on (by simp) (by simp) (hint _ ia) fun x hx => _
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
⊢ x₀ + ↑i ≤ x₀ + ↑(i + 1)
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
⊢ IntervalIntegrable (fun x => f (x₀ + ↑(i + 1))) volume (x₀ + ↑i) (x₀ + ↑(i + 1))
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ f (x₀ + ↑(i + 1)) ≤ f x
[PROOFSTEP]
apply hf _ _ hx.2
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x ∈ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
refine' mem_Icc.2 ⟨le_trans ((le_add_iff_nonneg_right _).2 (Nat.cast_nonneg _)) hx.1, le_trans hx.2 _⟩
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ + ↑(i + 1) ≤ x₀ + ↑a
[PROOFSTEP]
simp only [Nat.cast_le, add_le_add_iff_left, ia]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ + ↑(i + 1) ∈ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
refine' mem_Icc.2 ⟨(le_add_iff_nonneg_right _).2 (Nat.cast_nonneg _), _⟩
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ + ↑(i + 1) ≤ x₀ + ↑a
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, ia]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x = ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
[PROOFSTEP]
convert intervalIntegral.sum_integral_adjacent_intervals hint
[GOAL]
case h.e'_3.h.e'_5
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ x₀ = x₀ + ↑0
[PROOFSTEP]
simp only [Nat.cast_zero, add_zero]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i in Finset.Ico a b, f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, f x
[PROOFSTEP]
rw [(Nat.sub_add_cancel hab).symm, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i in Finset.Ico a (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
conv =>
  congr
  congr
  congr
  rw [← zero_add a]
  ·skip
  ·skip
  ·skip
  rw [add_comm]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ i in Finset.Ico a (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
  congr
  congr
  congr
  rw [← zero_add a]
  ·skip
  ·skip
  ·skip
  rw [add_comm]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ i in Finset.Ico a (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
  congr
  congr
  congr
  rw [← zero_add a]
  ·skip
  ·skip
  ·skip
  rw [add_comm]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ i in Finset.Ico a (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
congr
[GOAL]
case a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ i in Finset.Ico a (b - a + a), f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
congr
[GOAL]
case a.s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.Ico a (b - a + a)
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
congr
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| a
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
rw [← zero_add a]
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| 0 + a
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
·skip
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| 0 + a
[PROOFSTEP]
skip
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| 0 + a
[PROOFSTEP]
skip
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| 0 + a
[PROOFSTEP]
skip
[GOAL]
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
·skip
[GOAL]
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
[PROOFSTEP]
skip
[GOAL]
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
[PROOFSTEP]
skip
[GOAL]
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
[PROOFSTEP]
skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
·skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
[PROOFSTEP]
skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
[PROOFSTEP]
skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
[PROOFSTEP]
skip
[GOAL]
case a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
rw [add_comm]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i in Finset.Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x in Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
conv =>
  lhs
  congr
  congr
  ·skip
  ext
  rw [add_assoc, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
  lhs
  congr
  congr
  ·skip
  ext
  rw [add_assoc, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
  lhs
  congr
  congr
  ·skip
  ext
  rw [add_assoc, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
lhs
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.range (b - a), f ↑(a + x + 1)
[PROOFSTEP]
congr
[GOAL]
case s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.range (b - a)
case f x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | fun x => f ↑(a + x + 1)
[PROOFSTEP]
congr
[GOAL]
case s.n
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a
case f x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | fun x => f ↑(a + x + 1)
[PROOFSTEP]
·skip
[GOAL]
case s.n
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a
[PROOFSTEP]
skip
[GOAL]
case s.n
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a
[PROOFSTEP]
skip
[GOAL]
case s.n
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a
[PROOFSTEP]
skip
[GOAL]
case f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f ↑(a + x + 1)
[PROOFSTEP]
ext
[GOAL]
case f.h
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
x✝ : ℕ
| f ↑(a + x✝ + 1)
[PROOFSTEP]
rw [add_assoc, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x in Finset.range (b - a), f (↑a + ↑(x + 1)) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
apply AntitoneOn.sum_le_integral
[GOAL]
case hf
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ AntitoneOn f (Icc (↑a) (↑a + ↑(b - a)))
[PROOFSTEP]
simp only [hf, hab, Nat.cast_sub, add_sub_cancel'_right]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i in Finset.range a, f (x₀ + ↑i) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
[PROOFSTEP]
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, -f x ≤ ∑ x in Finset.range a, -f (x₀ + ↑x)
[PROOFSTEP]
exact hf.neg.integral_le_sum
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∑ x in Finset.Ico a b, f ↑x ≤ ∫ (x : ℝ) in ↑a..↑b, f x
[PROOFSTEP]
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, -f x ≤ ∑ x in Finset.Ico a b, -f ↑x
[PROOFSTEP]
exact hf.neg.integral_le_sum_Ico hab
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i in Finset.range a, f (x₀ + ↑(i + 1))
[PROOFSTEP]
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ x in Finset.range a, -f (x₀ + ↑(x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, -f x
[PROOFSTEP]
exact hf.neg.sum_le_integral
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ i in Finset.Ico a b, f ↑(i + 1)
[PROOFSTEP]
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∑ x in Finset.Ico a b, -f ↑(x + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, -f x
[PROOFSTEP]
exact hf.neg.sum_le_integral_Ico hab
