OAI/Combinatorics/ContingencyTables/Sampling/PhysicalPrefixTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Future halting tails after a bounded stopping prefix

  1. lemma OAI.ContingencyTables.PhysicalPrefixTail.deterministic_mean line 13
  2. theorem OAI.ContingencyTables.PhysicalPrefixTail.after_prefix line 23

    Source documentation

    A prefix may end at different times on different tapes. After its worst-case budget, the future live probability is bounded by the average future live probability at its actual endpoints.

    theorem after_prefix (M : Table Γ Q) (out : A → Cfg Γ Q) (c : Cfg Γ Q)
    (p : Experiment A) (h : Implements M out c p) (S n : ℕ) (hS : p.cost≤S) :
    (experiment M (S+n) c).mean live≤
      p.mean (fun a => (experiment M n (out a)).mean live) := by
…

    Mentions: OAI.ContingencyTables.Table