OAI/Combinatorics/ParityLifts/UniformBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ParityWL.Complexity.uniform_reduction line 9

   Source documentation

   A single parameter-oblivious finite machine meets every positive rate. Its input polynomial degree is also fixed before choosing the rate.

   theorem uniform_reduction (c : Convention) (i : Implementation) (M : Machine) (f g : ℕ → ℝ)
       (hlim : Filter.Tendsto (fun k : ℕ => g k/k) Filter.atTop (nhds 0))
       (hM : UniformWLBound M c i f g) :
       ∃ d : ℕ, ∀ ε : ℝ, 0<ε → ∃ C : ℝ, 0<C ∧
         SATTimeBound (raceCode (trialCode c M).decision).decision
           (fun N L => C*(L+1 : ℝ)^d*2^(ε*N)) := by
   …

   Mentions: OAI.ParityWL.Convention, OAI.ParityWL.Complexity.Implementation, OAI.ParityWL.Complexity.Machine, OAI.ParityWL.Complexity.UniformWLBound, OAI.ParityWL.Complexity.SATTimeBound, OAI.ParityWL.Complexity.raceCode, OAI.ParityWL.Complexity.trialCode