Stage 9: generic Euclidean telescoping algebra

These lemmas contain no OGM-G certificate assumption. They expose the recursively generated auxiliary p sequence and the exact polarization used by the finite-data identity.

noncomputable def O3.stage9WeightedGradient {d : ℕ} (delta : ℕ → ℝ) (g : ℕ → Vec d) (k : ℕ) : Vec d

The sum of gradients before index k, weighted by the certificate increments.

Equations

• O3.stage9WeightedGradient delta g k = ∑ j ∈ Finset.range k, delta j • g j

theorem O3.pairing_finset_sum_left {d : ℕ} {α : Type u_1} (s : Finset α) (f : α → Vec d) (x : Vec d) : pairing (∑ i ∈ s, f i) x = ∑ i ∈ s, pairing (f i) x

theorem O3.pairing_sub_left {d : ℕ} (x y z : Vec d) : pairing (x - y) z = pairing x z - pairing y z

theorem O3.pairing_neg_right' {d : ℕ} (x y : Vec d) : pairing x (-y) = -pairing x y

theorem O3.stage9WeightedGradient_succ {d : ℕ} (delta : ℕ → ℝ) (g : ℕ → Vec d) (k : ℕ) : stage9WeightedGradient delta g (k + 1) = stage9WeightedGradient delta g k + delta k • g k

theorem O3.stage9_pairing_summation_by_parts {d : ℕ} (delta : ℕ → ℝ) (g v : ℕ → Vec d) (n : ℕ) : ∑ i ∈ Finset.range n, delta i * pairing (g i) (v n - v i) = ∑ k ∈ Finset.range n, pairing (stage9WeightedGradient delta g (k + 1)) (v (k + 1) - v k)

Discrete summation by parts for the second pairing sum in the frozen certificate.

noncomputable def O3.stage9P {d : ℕ} (theta : ℕ → ℝ) (g : ℕ → Vec d) : ℕ → Vec d

The auxiliary sequence from the frozen OGM-G certificate.

Equations

• O3.stage9P theta g 0 = 0
• O3.stage9P theta g k.succ = (1 - 1 / theta k) • O3.stage9P theta g k + (1 / theta k) • g k

@[simp]

theorem O3.stage9P_zero {d : ℕ} (theta : ℕ → ℝ) (g : ℕ → Vec d) : stage9P theta g 0 = 0

@[simp]

theorem O3.stage9P_succ {d : ℕ} (theta : ℕ → ℝ) (g : ℕ → Vec d) (k : ℕ) : stage9P theta g (k + 1) = (1 - 1 / theta k) • stage9P theta g k + (1 / theta k) • g k

theorem O3.stage9P_one {d : ℕ} {theta : ℕ → ℝ} {g : ℕ → Vec d} : stage9P theta g 1 = (1 / theta 0) • g 0

theorem O3.stage9P_gradient_eq {d : ℕ} {theta : ℕ → ℝ} {g : ℕ → Vec d} {k : ℕ} (hθ : theta k ≠ 0) : g k = theta k • stage9P theta g (k + 1) - (theta k - 1) • stage9P theta g k

Rearranged auxiliary recurrence, with every division justified.

theorem O3.stage9P_endpoint {d : ℕ} {theta : ℕ → ℝ} {g : ℕ → Vec d} {n : ℕ} (hθn : theta n = 1) : stage9P theta g (n + 1) = g n

Since theta_n=1, the source endpoint is genuinely p_(n+1)=g_n.

theorem O3.lpNorm_two_sq_eq_pairing {d : ℕ} (x : Vec d) : lpNorm 2 x ^ 2 = pairing x x

Literal lpNorm 2 squared is the coordinate pairing with itself.

theorem O3.pairing_sub_add_self {d : ℕ} (x y : Vec d) : pairing (x - y) (x + y) = lpNorm 2 x ^ 2 - lpNorm 2 y ^ 2

Exact Euclidean polarization, still in the project's literal norm.

theorem O3.stage9P_quadratic_step {d : ℕ} {theta : ℕ → ℝ} {g : ℕ → Vec d} {k : ℕ} (hθ : theta k ≠ 0) : theta k * pairing (stage9P theta g k - g k) (stage9P theta g k + stage9P theta g (k + 1)) = theta k ^ 2 * (lpNorm 2 (stage9P theta g k) ^ 2 - lpNorm 2 (stage9P theta g (k + 1)) ^ 2)

The auxiliary recurrence converts the mixed product to a difference of squares with the exact theta_k^2 coefficient.

theorem O3.stage9_delta_gradient_sum {d : ℕ} (N : ℕ) (theta kappa delta : ℕ → ℝ) (g : ℕ → Vec d) (hθ : ∀ (k : ℕ), theta k ≠ 0) (hδ : ∀ k < N, delta k = kappa (k + 1) / theta k) (hκ : ∀ k < N, kappa k = kappa (k + 1) * (1 - 1 / theta k)) (k : ℕ) : k ≤ N → ∑ j ∈ Finset.range k, delta j • g j = kappa k • stage9P theta g k

The partial weighted gradient sum equals kappa_k p_k whenever the two exact scalar coefficient recurrences hold.