LeanPool.ParameterFreeGradient.V7.Proofs.Stage3BelowTwoS3F.Coefficients

The explicit below-two coefficient matrices satisfy recurrence, support, and row-sum conditions.

source

noncomputable def V7.Stage3BelowTwoS3F.weight (n k : ℕ) :

ℝ

The quadratic below-two weights, constant at the terminal index and zero beyond it.

Equations

V7.Stage3BelowTwoS3F.weight n k = if k < n then (↑k + 1) ^ 2 / 4 else if k = n then ↑n ^ 2 / 4 else 0

Instances For

source

noncomputable def V7.Stage3BelowTwoS3F.increment (n k : ℕ) :

ℝ

The below-two weight increments, set to zero from the terminal index onward.

Equations

V7.Stage3BelowTwoS3F.increment n k = if k < n then V7.Stage3BelowTwoS3F.weight n k - if k = 0 then 0 else V7.Stage3BelowTwoS3F.weight n (k - 1) else 0

Instances For

source

noncomputable def V7.Stage3BelowTwoS3F.alpha (n : ℕ) :

ScalarMatrix

The subdiagonal coefficient matrix selecting each weighted gradient increment.

Equations

V7.Stage3BelowTwoS3F.alpha n row i = if 0 < row ∧ row ≤ n then if i = row - 1 then V7.Stage3BelowTwoS3F.increment n (row - 1) else 0 else 0

Instances For

source

noncomputable def V7.Stage3BelowTwoS3F.coeffC (n : ℕ) :

ScalarMatrix

The recursive coefficients expressing primal iterates as combinations of mirror iterates.

Equations

One or more equations did not get rendered due to their size.
V7.Stage3BelowTwoS3F.coeffC n 0 x✝ = if x✝ = 0 then 1 else 0

Instances For

source

noncomputable def V7.Stage3BelowTwoS3F.coeffB (n : ℕ) :

ScalarMatrix

The differences of successive primal coefficient rows, with the prescribed initial row.

Equations

V7.Stage3BelowTwoS3F.coeffB n 0 x✝ = if x✝ = 0 then -1 else 0
V7.Stage3BelowTwoS3F.coeffB n k.succ x✝ = V7.Stage3BelowTwoS3F.coeffC n k x✝ - V7.Stage3BelowTwoS3F.coeffC n (k + 1) x✝

Instances For

source

@[simp]

theorem V7.Stage3BelowTwoS3F.weight_of_lt {n k : ℕ} (hk : k < n) :

weight n k = (↑k + 1) ^ 2 / 4

source

@[simp]

theorem V7.Stage3BelowTwoS3F.weight_at {n : ℕ} :

weight n n = ↑n ^ 2 / 4

source

theorem V7.Stage3BelowTwoS3F.weight_pos {n k : ℕ} (hn : 1 ≤ n) (hk : k ≤ n) :

0 < weight n k

source

@[simp]

theorem V7.Stage3BelowTwoS3F.increment_of_lt {n k : ℕ} (hk : k < n) :

increment n k = weight n k - if k = 0 then 0 else weight n (k - 1)

source

@[simp]

theorem V7.Stage3BelowTwoS3F.increment_at {n : ℕ} :

increment n n = 0

source

theorem V7.Stage3BelowTwoS3F.increment_formula {n k : ℕ} (hk : k < n) :

increment n k = (2 * ↑k + 1) / 4

source

theorem V7.Stage3BelowTwoS3F.weight_sub_increment_sq {n k : ℕ} (hk : k < n) :

weight n k - increment n k ^ 2 = (4 * ↑k + 3) / 16

source

theorem V7.Stage3BelowTwoS3F.weight_succ_relation {n k : ℕ} (hk : k < n) :

weight n (k + 1) = weight n k + increment n (k + 1)

source

@[simp]

theorem V7.Stage3BelowTwoS3F.alpha_row {n k i : ℕ} (hk : k < n) :

alpha n (k + 1) i = if i = k then increment n k else 0

source

@[simp]

theorem V7.Stage3BelowTwoS3F.coeffC_zero {n : ℕ} :

coeffC n 0 0 = 1

source

@[simp]

theorem V7.Stage3BelowTwoS3F.coeffB_zero {n : ℕ} :

coeffB n 0 0 = -1

source

theorem V7.Stage3BelowTwoS3F.coeffC_support (n k i : ℕ) :

k < i → coeffC n k i = 0

source

theorem V7.Stage3BelowTwoS3F.coeffC_row_sum (n : ℕ) (hn : 1 ≤ n) (k : ℕ) :

k ≤ n → ∑ i ∈ Finset.range (k + 1), coeffC n k i = 1

source

theorem V7.Stage3BelowTwoS3F.coeffB_row_sum (n : ℕ) (hn : 1 ≤ n) (k : ℕ) :

k < n → ∑ i ∈ Finset.range (k + 2), coeffB n (k + 1) i = 0

source

theorem V7.Stage3BelowTwoS3F.coefficient_assumptions (n : ℕ) (hn : 1 ≤ n) :

BelowCoefficientAssumptions n (weight n) (increment n) (alpha n) (coeffC n) (coeffB n)