The above-two trial's total query count obeys its regime-dependent rate.

noncomputable def V7.Stage4AboveTwoFinalTrial.trialConstant (p : ℝ) : ℝ

The exponent-dependent constant bounding the total queries of both above-two phases.

Equations

• V7.Stage4AboveTwoFinalTrial.trialConstant p = V7.aboveHp p ^ (p / (p + 2)) + V7.aboveJp p ^ (p / (p + 2)) + 2

theorem V7.Stage4AboveTwoFinalTrial.trialConstant_pos (p : ℝ) (hp : 2 < p) : 0 < trialConstant p

theorem V7.Stage4AboveTwoFinalTrial.calls_current_bound {d : ℕ} {eps : ℝ} {oracle : PairOracle d} {report : TrialReport d} {p M D : ℝ} {x0 : Point d} {m₁ m₂ : ℕ} (hp : 2 < p) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (hkappa : 1 ≤ M * D / eps) (hshape : FullShape p eps M D x0 oracle report m₁ m₂) : ↑report.calls ≤ trialConstant p * (M * D / eps) ^ (p / (p + 2))