sum_le_integral

theorem sum_le_integral {x₀ : ℝ} {f : ℝ → ℝ} {n : ℕ} (hf : AntitoneOn f (Ioc x₀ (x₀ + n)))    (hfi : IntegrableOn f (Icc x₀ (x₀ + n))) :    (∑ i ∈ Finset.range n, f (x₀ + ↑(i + 1))) ≤ ∫ x in x₀..x₀ + n, f x := by   cases n with simp only [Nat.cast_add, Nat.cast_one, CharP.cast_eq_zero, add_zero,      lt_self_iff_false, not_false_eq_true,    Ioc_eq_empty, Finset.range_zero, Nat.cast_add, Nat.cast_one, Finset.sum_empty,    intervalIntegral.integral_same, le_refl] at hf ⊢  | succ n =>  have : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1) := by    ext i ; by_cases hi : i = 0 <;> simp [hi] ; omega  simp only [this, Finset.singleton_union, Finset.mem_Ico, nonpos_iff_eq_zero, one_ne_zero,    lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true, and_true, not_false_eq_true,    Finset.sum_insert, CharP.cast_eq_zero, zero_add, ge_iff_le]   have l4 : IntervalIntegrable f volume x₀ (x₀ + 1) := by    apply IntegrableOn.intervalIntegrable    simp only [le_add_iff_nonneg_right, zero_le_one, uIcc_of_le]    apply hfi.mono_set    apply Icc_subset_Icc le_rfl    simp  have l5 x (hx : x ∈ Ioc x₀ (x₀ + 1)) : (fun x ↦ f (x₀ + 1)) x ≤ f x := by    rcases hx with ⟨hx1, hx2⟩    refine hf ⟨hx1, by linarith⟩ ⟨by linarith, by linarith⟩ hx2  have l6 : ∫ x in x₀..x₀ + 1, f (x₀ + 1) = f (x₀ + 1) := by simp   have l1 : f (x₀ + 1) ≤ ∫ x in x₀..x₀ + 1, f x := by    rw [← l6] ; apply intervalIntegral.integral_mono_ae_restrict (by linarith) (by simp) l4    apply eventually_of_mem _ l5    have : (Ioc x₀ (x₀ + 1))ᶜ ∩ Icc x₀ (x₀ + 1) = {x₀} := by simp [← sdiff_eq_compl_inter]    simp [ae, this]   have l2 : AntitoneOn (fun x ↦ f (x₀ + x)) (Icc 1 ↑(n + 1)) := by    intro u ⟨hu1, _⟩ v ⟨_, hv2⟩ huv ; push_cast at hv2    refine hf ⟨?_, ?_⟩ ⟨?_, ?_⟩ ?_ <;> linarith   have l3 := @AntitoneOn.sum_le_integral_Ico 1 (n + 1) (fun x => f (x₀ + x)) (by simp)    (by simpa using l2)   simp only [Nat.cast_add, Nat.cast_one, intervalIntegral.integral_comp_add_left] at l3  convert! _root_.add_le_add l1 l3   have := @intervalIntegral.integral_comp_mul_add ℝ _ _ 1 (n + 1) 1 f one_ne_zero x₀  rw [intervalIntegral.integral_add_adjacent_intervals]  · exact l4  · apply IntegrableOn.intervalIntegrable    simp only [add_le_add_iff_left, le_add_iff_nonneg_left, Nat.cast_nonneg, uIcc_of_le]    apply hfi.mono_set    apply Icc_subset_Icc    · linarith    · simp