The above-two trial coefficients satisfy recurrence, support, and row-sum assumptions.

noncomputable def V7.Stage4AboveTwoFinalTrial.weight (p eta : ℝ) (n : ℕ) : ScalarSeq

The terminal-plateau weight sequence used by the above-two trial.

Equations

• V7.Stage4AboveTwoFinalTrial.weight p eta n = V7.Stage4AboveTwoDualPhase.plateauU p eta n

noncomputable def V7.Stage4AboveTwoFinalTrial.increment (p eta : ℝ) (n : ℕ) : ScalarSeq

The increments of the above-two trial's weight sequence.

Equations

• V7.Stage4AboveTwoFinalTrial.increment p eta n = V7.Stage4AboveTwoDualPhase.plateauDw p eta n

noncomputable def V7.Stage4AboveTwoFinalTrial.alpha (p eta : ℝ) (n : ℕ) : ScalarMatrix

The subdiagonal matrix selecting weighted gradient increments in an above-two phase.

Equations

• V7.Stage4AboveTwoFinalTrial.alpha p eta n row i = if 0 < row ∧ row ≤ n then if i = row - 1 then V7.Stage4AboveTwoFinalTrial.increment p eta n (row - 1) else 0 else 0

noncomputable def V7.Stage4AboveTwoFinalTrial.coeffC (p eta : ℝ) (n : ℕ) : ScalarMatrix

The recursive coefficients expressing above-two primal iterates in mirror iterates.

Equations

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

noncomputable def V7.Stage4AboveTwoFinalTrial.coeffB (p eta : ℝ) (n : ℕ) : ScalarMatrix

The differences of successive above-two primal coefficient rows.

Equations

• V7.Stage4AboveTwoFinalTrial.coeffB p eta n 0 x✝ = if x✝ = 0 then -1 else 0
• V7.Stage4AboveTwoFinalTrial.coeffB p eta n k.succ x✝ = V7.Stage4AboveTwoFinalTrial.coeffC p eta n k x✝ - V7.Stage4AboveTwoFinalTrial.coeffC p eta n (k + 1) x✝

@[simp]

theorem V7.Stage4AboveTwoFinalTrial.weight_of_lt {p eta : ℝ} {n k : ℕ} (hk : k < n) : weight p eta n k = aboveGamma p eta n * (↑k + 1) ^ 2

@[simp]

theorem V7.Stage4AboveTwoFinalTrial.weight_at {p eta : ℝ} {n : ℕ} : weight p eta n n = aboveGamma p eta n * ↑n ^ 2

theorem V7.Stage4AboveTwoFinalTrial.increment_of_lt {p eta : ℝ} {n k : ℕ} : increment p eta n k = weight p eta n k - if k = 0 then 0 else weight p eta n (k - 1)

@[simp]

theorem V7.Stage4AboveTwoFinalTrial.increment_at {p eta : ℝ} {n : ℕ} (hn : 1 ≤ n) : increment p eta n n = 0

theorem V7.Stage4AboveTwoFinalTrial.gamma_pos {p eta : ℝ} {n : ℕ} (hp : 2 < p) (heta : 0 < eta) (hn : 1 ≤ n) : 0 < aboveGamma p eta n

theorem V7.Stage4AboveTwoFinalTrial.weight_pos {p eta : ℝ} {n k : ℕ} (hp : 2 < p) (heta : 0 < eta) (hn : 1 ≤ n) (hk : k ≤ n) : 0 < weight p eta n k

theorem V7.Stage4AboveTwoFinalTrial.weight_succ_relation {p eta : ℝ} {n k : ℕ} (hn : 1 ≤ n) (hk : k < n) : weight p eta n (k + 1) = weight p eta n k + increment p eta n (k + 1)

@[simp]

theorem V7.Stage4AboveTwoFinalTrial.alpha_row {p eta : ℝ} {n k i : ℕ} (hk : k < n) : alpha p eta n (k + 1) i = if i = k then increment p eta n k else 0

@[simp]

theorem V7.Stage4AboveTwoFinalTrial.coeffC_zero {p eta : ℝ} {n : ℕ} : coeffC p eta n 0 0 = 1

@[simp]

theorem V7.Stage4AboveTwoFinalTrial.coeffB_zero {p eta : ℝ} {n : ℕ} : coeffB p eta n 0 0 = -1

theorem V7.Stage4AboveTwoFinalTrial.coeffC_support (p eta : ℝ) (n k i : ℕ) : k < i → coeffC p eta n k i = 0

theorem V7.Stage4AboveTwoFinalTrial.coeffC_row_sum (p eta : ℝ) (n : ℕ) (hp : 2 < p) (heta : 0 < eta) (hn : 1 ≤ n) (k : ℕ) : k ≤ n → ∑ i ∈ Finset.range (k + 1), coeffC p eta n k i = 1

theorem V7.Stage4AboveTwoFinalTrial.coeffB_row_sum (p eta : ℝ) (n : ℕ) (hp : 2 < p) (heta : 0 < eta) (hn : 1 ≤ n) (k : ℕ) : k < n → ∑ i ∈ Finset.range (k + 2), coeffB p eta n (k + 1) i = 0

theorem V7.Stage4AboveTwoFinalTrial.coefficient_assumptions (p eta : ℝ) (n : ℕ) (hp : 2 < p) (heta : 0 < eta) (hn : 1 ≤ n) : AboveCoefficientAssumptions n (weight p eta n) (increment p eta n) (alpha p eta n) (coeffC p eta n) (coeffB p eta n)