Positive constants and endpoint estimates for geometric trial amortization.

theorem V7.Stage2Resume.epochScale_pos {Ma : ℝ} (hMa : 0 < Ma) (s : ℕ) : 0 < 2 ^ s * Ma

The R1 premise is the load-bearing source of positivity for every epoch scale.

theorem V7.Stage2Resume.epochRadius_pos {G Ma : ℝ} (hG : 0 < G) (hMa : 0 < Ma) (s j : ℕ) : 0 < 2 ^ j * G / (2 ^ s * Ma)

theorem V7.Stage2Resume.epochKappa_pos {eps G Ma : ℝ} (heps : 0 < eps) (hG : 0 < G) (hMa : 0 < Ma) (s j : ℕ) : 0 < 2 ^ s * Ma * (2 ^ j * G / (2 ^ s * Ma)) / eps

theorem V7.Stage2Resume.acceptedRadius_pos {G Ma Da : ℝ} (hG : 0 < G) (hMa : 0 < Ma) (hDa : Da = G / Ma) : 0 < Da

theorem V7.Stage2Resume.localCostExponent_le_one {p : ℝ} (_hp : 1 < p) : localCostExponent p ≤ 1

theorem V7.Stage2Resume.localCostExponent_eq_half_of_le_two {p : ℝ} (hp : p ≤ 2) : localCostExponent p = 1 / 2

theorem V7.Stage2Resume.localCostExponent_eq_above {p : ℝ} (hp : 2 < p) : localCostExponent p = p / (p + 2)

noncomputable def V7.Stage2Resume.amortizationConstant (a : ℝ) : ℝ

The constant bounding the sum of costs along the realized geometric controller path.

Equations

• V7.Stage2Resume.amortizationConstant a = 1 + 4 / (1 - 2 ^ (-a)) ^ 2

theorem V7.Stage2Resume.amortizationConstant_pos {a : ℝ} (ha : 0 < a) : 0 < amortizationConstant a

theorem V7.Stage2Resume.endpointCoefficient_le_constant {a : ℝ} (ha : 0 < a) (hale : a ≤ 1) : (2 ^ a / (1 - 2 ^ (-a))) ^ 2 ≤ amortizationConstant a