Documentation

LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.Main

The completed runtime satisfies the parameter-free main rate in all exponent regimes.

source
noncomputable def V7.Stage8Main.universalMainConstant :
ℝ

The universal constant combining initialization, anchor search, and Euclidean trial costs.

Equations
Instances For
    source
    theorem V7.Stage8Main.universalMainConstant_pos :
    0 < universalMainConstant
    source
    theorem V7.Stage8Main.universalMainConstant_one :
    1 ≤ universalMainConstant
    source
    theorem V7.Stage8Main.universalMainConstant_anchor :
    1 + O3.anchorLogConstant ≤ universalMainConstant
    source
    noncomputable def V7.Stage8Main.regimeMainConstant (p : ℝ) (hp : 1 < p) :
    ℝ

    The exponent-dependent constant combining anchor and non-Euclidean trial costs.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem V7.Stage8Main.regimeMainConstant_pos (p : ℝ) (hp : 1 < p) :
      0 < regimeMainConstant p hp
      source
      theorem V7.Stage8Main.regimeMainConstant_one_below (p : ℝ) (hp : 1 < p) (hp2 : p < 2) :
      1 ≤ regimeMainConstant p hp
      source
      theorem V7.Stage8Main.regimeMainConstant_anchor_below (p : ℝ) (hp : 1 < p) (hp2 : p < 2) :
      1 + O3.anchorLogConstant ≤ regimeMainConstant p hp
      source
      theorem V7.Stage8Main.regimeMainConstant_one_above (p : ℝ) (hp : 1 < p) (hp2 : 2 < p) :
      1 ≤ regimeMainConstant p hp
      source
      theorem V7.Stage8Main.regimeMainConstant_anchor_above (p : ℝ) (hp : 1 < p) (hp2 : 2 < p) :
      1 + O3.anchorLogConstant ≤ regimeMainConstant p hp
      source
      theorem V7.Stage8Main.main :
      MainStatement
      source
      theorem V7.main :
      MainStatement