Transport of sums over the realized geometric visits into chronological report-call bounds.
theorem
V7.Stage2Resume.raggedGridListSum
(S : ℕ)
(lastRadius : ℕ → ℕ)
(f : ℕ → ℕ → ℝ)
:
(List.flatMap (fun (s : ℕ) => List.map (fun (j : ℕ) => f s j) (List.range (lastRadius s + 1)))
(List.range (S + 1))).sum = ∑ s ∈ Finset.range (S + 1), ∑ j ∈ Finset.range (lastRadius s + 1), f s j
theorem
V7.Stage2Resume.raggedVisitGridSum
(eps Ma G a : ℝ)
(S : ℕ)
(lastRadius : ℕ → ℕ)
:
(List.map (fun (visit : ControllerVisit) => (visit.M * visit.D / eps) ^ a)
(List.flatMap
(fun (s : ℕ) =>
List.map (fun (j : ℕ) => { M := 2 ^ s * Ma, D := 2 ^ j * G / (2 ^ s * Ma) }) (List.range (lastRadius s + 1)))
(List.range (S + 1)))).sum = ∑ s ∈ Finset.range (S + 1), ∑ j ∈ Finset.range (lastRadius s + 1), (2 ^ s * Ma * (2 ^ j * G / (2 ^ s * Ma)) / eps) ^ a
theorem
V7.Stage2Resume.actualReportCallsLeVisitSum
{d : ℕ}
{eps C a : ℝ}
(visits : List ControllerVisit)
(reports : List (TrialReport d))
(hlen : visits.length = reports.length)
(henvelope :
∀ i < reports.length,
∃ (visit : ControllerVisit) (report : TrialReport d),
VisitAt visits i visit ∧ ReportAt reports i report ∧ ↑report.calls ≤ C * (visit.M * visit.D / eps) ^ a)
: