OAI/Combinatorics/ContingencyTables/Machines/FiniteWordRationalLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.FiniteWordExecution.machine_rational_event line 15

   Source documentation

   An event verified on the rational value survives literal output and finite-word compilation, without requiring a decoding oracle.

   theorem machine_rational_event (N : TreeTyped.Realizer n) (F : TreeTyped.Realizer f)
       (as : List Symbol) (ha : ∀ a∈as,a≠0)
       (hout : ∀ bs,∀ a∈f (as,bs),a≠6 ∧ a≠7)
       (draw : Bits (n as) → ℚ) (hf : ∀ bits,f (as,List.ofFn bits)=encodeRat (draw bits))
       (P : ℚ → Prop) (t : ℕ) (ht : machineTime N F as≤t) :
       average (fun bits : Bits (n as) => if P (draw bits) then 1 else 0) ≤
         ((Finset.univ.filter (fun bits : Bits t =>
           ∃ q : ℚ,Outputs (machine N F) as bits q ∧ P q)).card:ℚ)/(2:ℚ)^t := by
   …

   Mentions: OAI.ContingencyTables.FiniteWordExecution.machineTime, OAI.ContingencyTables.FiniteWordExecution.machine

2. theorem OAI.ContingencyTables.FiniteWordExecution.machine_rational_all line 47

   Source documentation

   All finite source words have a rational output satisfying P, so the compiled machine has that property on every random tape.

   theorem machine_rational_all (N : TreeTyped.Realizer n) (F : TreeTyped.Realizer f)
       (as : List Symbol) (ha : ∀ a∈as,a≠0)
       (hout : ∀ bs,∀ a∈f (as,bs),a≠6 ∧ a≠7)
       (draw : Bits (n as) → ℚ) (hf : ∀ bits,f (as,List.ofFn bits)=encodeRat (draw bits))
       (P : ℚ → Prop) (hP : ∀ bits,P (draw bits))
       (t : ℕ) (ht : machineTime N F as≤t) :
       ∀ bits : Bits t,∃ q : ℚ,Outputs (machine N F) as bits q ∧ P q := by
   …

   Mentions: OAI.ContingencyTables.FiniteWordExecution.machineTime, OAI.ContingencyTables.FiniteWordExecution.machine