OAI/Combinatorics/ParityLifts/RaceBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ParityWL.Complexity.race_budget_numeric line 7
2. lemma OAI.ParityWL.Complexity.race_machine_numeric line 22
3. lemma OAI.ParityWL.Complexity.raceDecision_bound line 43

   Source documentation

   One fixed finite machine enumerates all parameter pairs and bounded simulations. The exponent and multiplier do not depend on the pair which eventually halts.

   lemma raceDecision_bound (M : Machine) : ∃ A : ℝ, 0<A ∧ ∃ d : ℕ, 0<d ∧
       ∀ bs : List Bool, ∀ P : Bool → Prop,
       (∀ j : ℕ, 0<j → ∀ k : ℕ, 4 ≤ k → ∃ s b, Emits M (trialInput j k bs) s b ∧ P b) →
       ∀ j k s : ℕ, 0<j → 4 ≤ k → ∀ b : Bool, Emits M (trialInput j k bs) s b →
       ∃ t a, Emits (raceCode M).decision bs t a ∧ P a ∧
         (t : ℝ) ≤ A*(s+j+k+bs.length+2 : ℝ)^d := by
   …

   Mentions: OAI.ParityWL.Complexity.Machine, OAI.ParityWL.Complexity.Emits, OAI.ParityWL.Complexity.trialInput, OAI.ParityWL.Complexity.raceCode