Source-exact OGM-G theta and kappa coefficients

This file isolates the scalar coefficient arithmetic in TeX Lemma lem:ogmg. The representation is Nat-indexed because the certificate sums over i = 0, ..., n; every theorem that uses a source index records the appropriate boundary hypothesis explicitly.

noncomputable def O3.stage9Theta (n i : ℕ) : ℝ

The source OGM-G coefficient theta_i at horizon n. Index zero uses the special doubled radical, while positive indices use the ordinary backward tail ending in theta_n = 1.

Equations

• O3.stage9Theta n i = if i = 0 then O3.ogmgThetaZero n else O3.ogmgThetaTail (n - i)

@[simp]

theorem O3.stage9Theta_zero (n : ℕ) : stage9Theta n 0 = ogmgThetaZero n

theorem O3.stage9Theta_of_pos {n i : ℕ} (hi : 0 < i) : stage9Theta n i = ogmgThetaTail (n - i)

@[simp]

theorem O3.stage9Theta_endpoint {n : ℕ} (hn : 1 ≤ n) : stage9Theta n n = 1

theorem O3.thetaZeroStep_pos (t : ℝ) : 0 < thetaZeroStep t

theorem O3.thetaStep_gt_half (t : ℝ) : 1 / 2 < thetaStep t

theorem O3.thetaZeroStep_gt_half (t : ℝ) : 1 / 2 < thetaZeroStep t

theorem O3.stage9Theta_pos (n i : ℕ) : 0 < stage9Theta n i

theorem O3.stage9Theta_ne_zero (n i : ℕ) : stage9Theta n i ≠ 0

In particular every denominator theta_i used by OGM-G is positive.

theorem O3.stage9_two_mul_theta_sub_one_pos (n i : ℕ) : 0 < 2 * stage9Theta n i - 1

The other source denominator 2 theta_i - 1 is strictly positive.

theorem O3.stage9_two_mul_theta_sub_one_ne_zero (n i : ℕ) : 2 * stage9Theta n i - 1 ≠ 0

theorem O3.stage9Theta_ordinary_equation {n i : ℕ} (hi : 1 ≤ i) (hin : i < n) : stage9Theta n i ^ 2 - stage9Theta n i = stage9Theta n (i + 1) ^ 2

The ordinary backward equation, valid exactly at 1 <= i < n.

theorem O3.stage9Theta_special_equation {n : ℕ} (_hn : 1 ≤ n) : stage9Theta n 0 ^ 2 - stage9Theta n 0 = 2 * stage9Theta n 1 ^ 2

The source's special doubled first equation.

theorem O3.stage9Theta_succ_le {n i : ℕ} (hin : i < n) : stage9Theta n (i + 1) ≤ stage9Theta n i

Adjacent theta coefficients decrease with their source index.

noncomputable def O3.stage9Kappa (n i : ℕ) : ℝ

Source definition of kappa: the zeroth coefficient is one and every positive coefficient is theta_0^2 / (2 theta_i^2).

Equations

• O3.stage9Kappa n i = if i = 0 then 1 else O3.stage9Theta n 0 ^ 2 / (2 * O3.stage9Theta n i ^ 2)

@[simp]

theorem O3.stage9Kappa_zero (n : ℕ) : stage9Kappa n 0 = 1

theorem O3.stage9Kappa_of_pos {n i : ℕ} (hi : 0 < i) : stage9Kappa n i = stage9Theta n 0 ^ 2 / (2 * stage9Theta n i ^ 2)

theorem O3.stage9Kappa_nonneg (n i : ℕ) : 0 ≤ stage9Kappa n i

theorem O3.stage9Kappa_mul_theta_sq {n i : ℕ} (hi : 1 ≤ i) : stage9Kappa n i * stage9Theta n i ^ 2 = stage9Theta n 0 ^ 2 / 2

The constant product used at the quadratic telescoping endpoint.

theorem O3.stage9Kappa_zero_le_one {n : ℕ} (hn : 1 ≤ n) : stage9Kappa n 0 ≤ stage9Kappa n 1

The first increment is nonnegative; this is the step that uses the special identity theta_0^2 - theta_0 = 2 theta_1^2.

theorem O3.stage9Kappa_mono_succ {n i : ℕ} (hin : i < n) : stage9Kappa n i ≤ stage9Kappa n (i + 1)

kappa_i is nondecreasing on the entire source interval.

theorem O3.stage9Kappa_mono {n i j : ℕ} (hij : i ≤ j) (hjn : j ≤ n) : stage9Kappa n i ≤ stage9Kappa n j

Interval form of monotonicity, convenient for finite certificate sums.

noncomputable def O3.stage9Delta (n i : ℕ) : ℝ

The source increment delta_i = kappa_(i+1) - kappa_i.

Equations

• O3.stage9Delta n i = O3.stage9Kappa n (i + 1) - O3.stage9Kappa n i

theorem O3.stage9Delta_nonneg {n i : ℕ} (hin : i < n) : 0 ≤ stage9Delta n i

theorem O3.stage9Delta_eq_kappa_div_theta {n i : ℕ} (hin : i < n) : stage9Delta n i = stage9Kappa n (i + 1) / stage9Theta n i

Exact coefficient increment used in the p-sequence induction. The i=0 branch uses the special doubled theta equation, while positive indices use the ordinary equation.

theorem O3.stage9Kappa_eq_next_mul_one_sub_inv {n i : ℕ} (hin : i < n) : stage9Kappa n i = stage9Kappa n (i + 1) * (1 - 1 / stage9Theta n i)

Rearranged delta identity in precisely the form used to update the weighted-gradient partial sum.

theorem O3.stage9Theta_zero_lower {n : ℕ} (hn : 1 ≤ n) : (↑n + 1) / √2 ≤ stage9Theta n 0

The source endpoint lower bound, now exposed through the Nat-indexed coefficient representation used by Stage 9.