FiniteWordTableLaw.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Identifying public table probabilities with finite-word masses

theorem OAI.ContingencyTables.FiniteWordExecution.machine_tableMass line 18

Source documentation

Exact finite-word compilation preserves each table's probability, including the quotient of the public output tape by trailing blanks.

theorem machine_tableMass (N : TreeTyped.Realizer n) (F : TreeTyped.Realizer f)
    (as : List MatchingFPRAS.Symbol) (ha : ∀ a∈as,a≠0)
    (hout : ∀ bs,∀ a∈f (as,bs),a≠6 ∧ a≠7)
    {m j L : ℕ} {r : Fin m → ℕ} {c : Fin j → ℕ}
    (hL : n as=L) (draw : Bits L → Table r c)
    (hf : ∀ bits,f (as,List.ofFn bits)=encodeMatrix (draw bits).val)
    (t : ℕ) (ht : machineTime N F as≤t) (X : Table r c) :
    tableMass (machine N F) as t X.val=
      ((mapLaw (uniformLaw (α := Bits L)) draw).mass X:ℝ) := by
…

Mentions: OAI.MatchingFPRAS.Symbol, OAI.ContingencyTables.Table, OAI.ContingencyTables.FiniteWordExecution.machineTime, OAI.ContingencyTables.FiniteWordExecution.machine