Partition Telescoping and Uniform Small-Interval Bounds

This file implements the lemmas for removing the sorries in global_evaluation_from_partition in EVICore6.lean.

Main results

• find_fine_partition: Lemma P0 - Find a partition with step size < L
• partition_geometry_range: Lemma P1 - Partition points are in [0,r]
• partition_geometry_monotone: Lemma P1 - Partition is monotone with equal steps
• telescoping_identity: Lemma T1 - Telescoping sum identity
• per_segment_bound: Lemma U1 - Bound on each segment from uniform control
• sum_per_segment_bounds: Lemma S1 - Sum of per-segment bounds
• global_evaluation_via_partition: Main proposition - Global bound from partition

noncomputable def Frourio.partition_point (r : ℝ) (N i : ℕ) : ℝ

The i-th point of the equi-partition of [0,r] with N parts

Equations

• Frourio.partition_point r N i = ↑i * r / ↑N

noncomputable def Frourio.shifted_partition_point (s r : ℝ) (N i : ℕ) : ℝ

The shifted partition point S_i = s + t_i

Equations

• Frourio.shifted_partition_point s r N i = s + Frourio.partition_point r N i

theorem Frourio.find_fine_partition {r L : ℝ} (hr : 0 < r) (hL : 0 < L) : ∃ (N : ℕ), 0 < N ∧ r / ↑N < L

Lemma P0: Find a fine partition If r > 0 and L > 0, then there exists N ∈ ℕ, N ≥ 1, such that r/N < L.

theorem Frourio.partition_geometry_range (r : ℝ) (N : ℕ) (hN : 0 < N) (hr : 0 ≤ r) (i : ℕ) (hi : i ≤ N) : 0 ≤ partition_point r N i ∧ partition_point r N i ≤ r

Lemma P1 (Range): Partition points are in [0,r] For all i = 0,...,N, we have 0 ≤ t_i ≤ r.

theorem Frourio.partition_geometry_monotone (r : ℝ) (N : ℕ) (hr : 0 ≤ r) (i : ℕ) : partition_point r N i ≤ partition_point r N (i + 1) ∧ partition_point r N (i + 1) - partition_point r N i = r / ↑N

Lemma P1 (Monotone): Partition is monotone with equal steps For all i = 0,...,N-1, we have t_i ≤ t_{i+1} and t_{i+1} - t_i = r/N.

theorem Frourio.telescoping_identity (g : ℝ → ℝ) (s r : ℝ) (N : ℕ) (hN : 0 < N) : ∑ i ∈ Finset.range N, (g (shifted_partition_point s r N (i + 1)) - g (shifted_partition_point s r N i)) = g (s + r) - g s

Lemma T1: Telescoping identity For any function g : ℝ → ℝ and S_i := s + t_i, ∑{i=0}^{N-1} (g(S{i+1}) - g(S_i)) = g(S_N) - g(S_0) = g(s + r) - g(s).

theorem Frourio.per_segment_bound {φ : ℝ → ℝ} {s r ε L : ℝ} (h_control : ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → z - y < L → φ (s + z) - φ (s + y) ≤ ε * (z - y)) (N : ℕ) (hN : 0 < N) (hr : 0 < r) (hL : r / ↑N < L) (i : ℕ) (hi : i < N) : φ (shifted_partition_point s r N (i + 1)) - φ (shifted_partition_point s r N i) ≤ ε * (r / ↑N)

Lemma U1: Per-segment bound from uniform control Assume the uniform small-interval control on [0,r] with parameter L. If N ≥ 1 and r/N < L, then for all i = 0,...,N-1, φ(s + t_{i+1}) - φ(s + t_i) ≤ ε(t_{i+1} - t_i) = ε(r/N).

theorem Frourio.sum_per_segment_bounds {φ : ℝ → ℝ} {s r ε L : ℝ} (h_control : ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → z - y < L → φ (s + z) - φ (s + y) ≤ ε * (z - y)) (N : ℕ) (hN : 0 < N) (hr : 0 < r) (hL : r / ↑N < L) : ∑ i ∈ Finset.range N, (φ (shifted_partition_point s r N (i + 1)) - φ (shifted_partition_point s r N i)) ≤ ε * r

Lemma S1: Summing per-segment bounds Under the hypotheses of U1, ∑{i=0}^{N-1} (φ(s + t{i+1}) - φ(s + t_i)) ≤ ε ∑{i=0}^{N-1} (t{i+1} - t_i) = εr.

theorem Frourio.global_evaluation_via_partition {φ : ℝ → ℝ} {s r ε L : ℝ} (h_control : ∀ (y z : ℝ), y ∈ Set.Icc 0 r → z ∈ Set.Icc 0 r → y ≤ z → z - y < L → φ (s + z) - φ (s + y) ≤ ε * (z - y)) (hr : 0 < r) (hL : 0 < L) : φ (s + r) ≤ φ s + ε * r

Main Proposition: Global evaluation via partition Assume the uniform small-interval control on [0,r] with constant L > 0. Pick N ≥ 1 with r/N < L. Then φ(s + r) ≤ φ(s) + εr.