Documentation

LeanPool.ParameterFreeGradient.V7.Proofs.Stage8Main.LocalDispatch

Stage 8: current local-trial runtime dispatch #

The selectors in this file are made before a positive instance is supplied. They depend only on public runtime data and the cached exact observation.

source
noncomputable def V7.Stage8Main.belowTrialFor {d : ℕ} (p : ℝ) (hp : 1 < p) (hp2 : p < 2) (eps M D : ℝ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (x0 : Point d) (cached : CachedPair d) :
LocalTrial d

A below-two local trial selected from the proved existence theorem.

Equations
Instances For
    source
    theorem V7.Stage8Main.belowTrialFor_spec {d : ℕ} (p : ℝ) (hp : 1 < p) (hp2 : p < 2) (eps M D : ℝ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (x0 : Point d) (cached : CachedPair d) (inst : PositiveInstance p d x0) :
    cached.observation = O3.PairOracle.observe inst.oracle x0 → eps < lpNorm (conjugateExponent p) (inst.oracle.gradient x0) → D ≥ lpNorm (conjugateExponent p) (inst.oracle.gradient x0) / M → ∃ (report : TrialReport d) (w : BelowTrialWitness p d), (belowTrialFor p hp hp2 eps M D heps hM hD x0 cached).Executes M D cached inst.oracle report ∧ TrialCertificate eps p M D inst.L inst.R cached inst.oracle report ∧ BelowTrialOperationalContract p eps M D x0 cached inst.oracle report w ∧ ↑report.calls ≤ 4 * √(M * D / ((p - 1) * eps)) + 2 ∧ ↑report.calls ≤ (4 / √(p - 1) + 2) * √(M * D / eps)
    source
    noncomputable def V7.Stage8Main.euclideanConstant :
    ℝ

    The universal query-bound constant selected for the Euclidean local trial.

    Equations
    Instances For
      source
      theorem V7.Stage8Main.euclideanConstant_pos :
      0 < euclideanConstant
      source
      noncomputable def V7.Stage8Main.euclideanM {d : ℕ} (eps M D : ℝ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (x0 : Point d) (cached : CachedPair d) :
      ℕ

      The selected horizon of the Euclidean gap-reduction phase.

      Equations
      Instances For
        source
        noncomputable def V7.Stage8Main.euclideanN {d : ℕ} (eps M D : ℝ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (x0 : Point d) (cached : CachedPair d) :
        ℕ

        The selected horizon of the Euclidean OGM-G phase.

        Equations
        Instances For
          source
          noncomputable def V7.Stage8Main.euclideanTrialFor {d : ℕ} (eps M D : ℝ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (x0 : Point d) (cached : CachedPair d) :
          LocalTrial d

          A Euclidean local trial selected with its certified two-phase horizons.

          Equations
          Instances For
            source
            theorem V7.Stage8Main.euclideanTrialFor_spec {d : ℕ} (eps M D : ℝ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (x0 : Point d) (cached : CachedPair d) :
            euclideanM eps M D heps hM hD x0 cached = ⌈2 * √(M * D / eps)⌉₊ ∧ euclideanN eps M D heps hM hD x0 cached = euclideanM eps M D heps hM hD x0 cached ∧ ∀ (inst : PositiveInstance 2 d x0), cached.observation = O3.PairOracle.observe inst.oracle x0 → eps < lpNorm 2 (inst.oracle.gradient x0) → D ≥ lpNorm 2 (inst.oracle.gradient x0) / M → ∃ (report : TrialReport d) (phaseA : EuclideanGapData d (euclideanM eps M D heps hM hD x0 cached)) (phaseB : OGMGData d (euclideanN eps M D heps hM hD x0 cached)), (euclideanTrialFor eps M D heps hM hD x0 cached).Executes M D cached inst.oracle report ∧ TrialCertificate eps 2 M D inst.L inst.R cached inst.oracle report ∧ EuclideanTrialOperationalContract x0 M D inst report phaseA phaseB ∧ report.calls ≤ 2 * euclideanM eps M D heps hM hD x0 cached + euclideanN eps M D heps hM hD x0 cached + 1 ∧ ↑report.calls ≤ euclideanConstant * √(M * D / eps)
            source
            noncomputable def V7.Stage8Main.aboveConstant (p : ℝ) (hp : 2 < p) :
            ℝ

            The exponent-dependent query-bound constant for an above-two local trial.

            Equations
            Instances For
              source
              theorem V7.Stage8Main.aboveConstant_pos (p : ℝ) (hp : 2 < p) :
              0 < aboveConstant p hp
              source
              noncomputable def V7.Stage8Main.aboveTrialFor {d : ℕ} (p : ℝ) (hp : 2 < p) (eps M D : ℝ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (x0 : Point d) (cached : CachedPair d) :
              LocalTrial d

              An above-two local trial selected from the proved existence theorem.

              Equations
              Instances For
                source
                theorem V7.Stage8Main.aboveTrialFor_spec {d : ℕ} (p : ℝ) (hp : 2 < p) (eps M D : ℝ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (x0 : Point d) (cached : CachedPair d) (inst : PositiveInstance p d x0) :
                cached.observation = O3.PairOracle.observe inst.oracle x0 → eps < lpNorm (conjugateExponent p) (inst.oracle.gradient x0) → D ≥ lpNorm (conjugateExponent p) (inst.oracle.gradient x0) / M → ∃ (report : TrialReport d) (w : AboveTrialWitness p d), (aboveTrialFor p hp eps M D heps hM hD x0 cached).Executes M D cached inst.oracle report ∧ TrialCertificate eps p M D inst.L inst.R cached inst.oracle report ∧ AboveTrialOperationalContract p eps M D x0 cached inst.oracle report w ∧ ↑report.calls ≤ aboveConstant p hp * (M * D / eps) ^ (p / (p + 2))