Having Problems on Proving Integral Using Riemann Sum

Stream: general

[Li Haonan]

Question
Use $ε-N$ definition for limits to define the most basic version of Riemann integral on $[0, 1]$, which is $I(f):=\lim_{n\to\infty}\sum_{i=1}^{n}f(\frac{i}{n})\cdot\frac{1}{n}$, then show that the integration of $f(x) = x$ on $[0, 1]$ equals $\frac{1}{2}$

Existing code

import Mathlib.Algebra.Field.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

open BigOperators Nat Finset

/-
Define the Riemann sum for f(x) = x over [0,1] with n partitions:
S_n = (1/n) * Σ (i=0 to n-1) (i/n)
-/
noncomputable def riemann_sum (n : ℕ) : ℝ :=
  (1 / n) * ∑ i ∈ range n, (i : ℝ) / n

/-
Simplify the Riemann sum to closed form (n+1)/(2n):
1. Expand the definition of riemann_sum
2. Distribute the (1/n) multiplication
3. Simplify each term to i/n²
4. Compute sum of i from 0 to n-1 = n(n-1)/2
5. Final algebraic simplification
-/
lemma riemann_sum_closed_form (n : ℕ) (hn : n ≠ 0) :
    riemann_sum n = (n - 1) / (2 * n) := by
  unfold riemann_sum  -- Expand the definition
  rw [mul_sum]  -- Distribute multiplication over sum
  -- Simplify (1/n)*(i/n) = i/n² for each term
  simp_rw [div_mul_div_comm 1 ↑n ↑i ↑n, one_mul]
  -- Compute sum of i from 0 to n-1 = n(n-1)/2
  rw [sum_range_id]
  -- Final algebraic simplification:
  -- n(n-1)/2n² = (n-1)/2n → (n+1)/2n when adjusted
  have n_ne_zero : (n : ℝ) ≠ 0 := by exact_mod_cast hn
  field_simp [n_ne_zero]  -- Clear denominators
  ring  -- Finish with ring algebra

/-
ε-N proof that lim_{n→∞} S_n = 1/2:
1. Take arbitrary ε > 0
2. Choose N = max(1, ⌈1/(2ε)⌉)
3. For n ≥ N, show |S_n - 1/2| < ε
-/
theorem riemann_limit : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |riemann_sum n - 1/2| < ε := by
  intro ε hε  -- Take arbitrary ε > 0
  -- Choose N = max(1, ⌈1/(2ε)⌉) to ensure:
  -- (1) N ≥ 1 (so n ≠ 0)
  -- (2) N ≥ 1/(2ε) (to bound the error)
  let N := max 1 ⌈1 / (2 * ε)⌉₊
  use N  -- This N will work for our proof
  intro n hn  -- Take any n ≥ N
  -- First show n ≥ 1 (from first component of max)
  have n_ge_1 : n ≥ 1 := by
    apply le_trans (le_max_left 1 ⌈1 / (2 * ε)⌉₊) hn
  -- And n ≥ ⌈1/(2ε)⌉ (from second component)
  have n_ge_ceil : n ≥ ⌈1 / (2 * ε)⌉₊ := by
    apply le_trans (le_max_right 1 ⌈1 / (2 * ε)⌉₊) hn
  -- Since n ≥ 1, we know n ≠ 0
  have n_pos : n ≠ 0 := by linarith
  -- Simplify |S_n - 1/2| using closed form
  rw [riemann_sum_closed_form n n_pos,
      add_div ↑n 1 (2*↑n),
      ← one_mul,
      mul_div_mul_right_eq_div 1 2 ↑n,
      add_sub_right_comm (1/2) (1/(2*↑n)) (1/2),
      sub_self,
      abs_of_pos (by positivity)]
  -- Now need to show 1/(2n) < ε
  -- Since n ≥ ⌈1/(2ε)⌉, we have n > 1/(2ε)
  have : n > 1 / (2 * ε) := by
    refine lt_of_lt_of_le ?_ (Nat.le_ceil (1 / (2 * ε)))
    exact (le_max_right _ _).trans_lt hn
  -- Which implies 1/(2n) < ε
  rwa [lt_div_iff (by positivity), mul_comm] at this

/-
Final claim that the integral equals 1/2:
1. Proves existence of limit I=1/2
2. Shows it satisfies the ε-δ condition
-/
example : ∃ (I : ℝ), ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |riemann_sum n - I| < ε ∧ I = 1/2 := by
  use 1/2  -- The integral value is 1/2
  intro ε hε  -- For any ε > 0
  -- Get the N from our limit theorem
  obtain ⟨N, hN⟩ := riemann_limit ε hε
  -- Package the result with proof that I=1/2
  exact ⟨N, λ n hn ↦ ⟨hN n hn, rfl⟩⟩

Doubt
Not sure why simp_rw [div_mul_div_comm 1 ↑n ↑i ↑n] and rw[add_div ↑n 1 (2*↑n)] does not work. Can anyone help me to correct it or advise me how to fix it? Greatly appreciate your help!

[Aaron Liu]

i is a bound variable, and is not available in the context. Either replace it with a placeholder (underscore) or use conv.

[Patrick Massot]

When you write div_mul_div_comm 1 ↑n ↑i ↑n, Lean has no way to understand which coercion you mean by ↑ in ↑n. You can write (n : ℝ).

[Patrick Massot]

When you want to work under a summation sign you indeed don’t have access to the summation variable which is bound by the sum. If you don’t know the conv incantation you can type conv? then Shift-click in the tactic state on the expression inside the sum. It will make a create conv suggestion link. Clicking on the link will give you access to the summation body. In your case this should be good enough.

[Patrick Massot]

In general it’s not good enough because this looses the summation set information. For this you can state in a have the sum equality that you want and then start the proof by apply sum_congr.