Regime-specific local trial costs combine with geometric path amortization.

noncomputable def V7.Stage8Main.amortUniversal : ℝ

A universal constant selected from the geometric trial amortization theorem.

Equations

• V7.Stage8Main.amortUniversal = Classical.choose V7.geometricTrialAmortization

theorem V7.Stage8Main.amortUniversal_pos : 0 < amortUniversal

noncomputable def V7.Stage8Main.amortFor (p : ℝ) (hp : 1 < p) : ℝ

The exponent-dependent constant selected from the geometric trial amortization theorem.

Equations

• V7.Stage8Main.amortFor p hp = Classical.choose ⋯

theorem V7.Stage8Main.amortFor_pos (p : ℝ) (hp : 1 < p) : 0 < amortFor p hp

noncomputable def V7.Stage8Main.selectedAmort (p : ℝ) (hp : 1 < p) : ℝ

The universal amortization constant at exponent two and the regime constant otherwise.

Equations

• V7.Stage8Main.selectedAmort p hp = if p = 2 then V7.Stage8Main.amortUniversal else V7.Stage8Main.amortFor p hp

theorem V7.Stage8Main.selectedAmort_pos (p : ℝ) (hp : 1 < p) : 0 < selectedAmort p hp

theorem V7.Stage8Main.runtimeCoefficient_pos {d : ℕ} (data : RuntimeData d) : 0 < runtimeCoefficient data

theorem V7.Stage8Main.reportCalls_bound {d : ℕ} (data : RuntimeData d) (inst : PositiveInstance data.input.p d data.input.x0) (hcached : data.cached.observation = O3.PairOracle.observe inst.oracle data.input.x0) (hlarge : data.input.eps < lpNorm (conjugateExponent data.input.p) (inst.oracle.gradient data.input.x0)) (hMaBound : data.Ma < 2 * inst.L) (hDaBound : data.G / data.Ma ≤ 2 * inst.R) {finish : RuntimeFinish d} (hinv : FinishInvariant data inst finish) : ↑(List.map (fun (report : TrialReport d) => report.calls) finish.reports).sum ≤ runtimeCoefficient data * selectedAmort data.input.p ⋯ * conditionBar inst data.input.eps ^ localCostExponent data.input.p