The total local trial cost is bounded by the endpoint costs of the realized controller path.
theorem
V7.Stage2Resume.pathGeometricSumsR1
{eps G Ma R : ℝ}
(heps : 0 < eps)
(hG : 0 < G)
(hMa : 0 < Ma)
(hR : 0 ≤ R)
(S : ℕ)
(lastRadius : ℕ → ℕ)
:
have Ms := fun (s : ℕ) => 2 ^ s * Ma;
have Dsj := fun (s j : ℕ) => 2 ^ j * G / Ms s;
have kappa := fun (s j : ℕ) => Ms s * Dsj s j / eps;
∀ (a : ℝ),
0 < a →
(∀ s ≤ S, ∑ j ∈ Finset.range (lastRadius s + 1), kappa s j ^ a ≤ kappa s (lastRadius s) ^ a / (1 - 2 ^ (-a))) ∧ ∑ s ∈ Finset.range (S + 1), (Ms s * R / eps) ^ a ≤ (Ms S * R / eps) ^ a / (1 - 2 ^ (-a))
The two source-level sums, proved independently over the realized radius prefix of each epoch and over the realized scale prefix.