OAI/Combinatorics/ContingencyTables/Sampling/PhysicalRetryTail.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.PhysicalRetryTail.live line 14
2. lemma OAI.ContingencyTables.PhysicalRetryTail.mean_mono line 16
3. lemma OAI.ContingencyTables.PhysicalRetryTail.mean_const line 23
4. lemma OAI.ContingencyTables.PhysicalRetryTail.live_nonnegative line 29
5. lemma OAI.ContingencyTables.PhysicalRetryTail.live_le_one line 30
6. lemma OAI.ContingencyTables.PhysicalRetryTail.experiment_mean_add line 32
7. lemma OAI.ContingencyTables.PhysicalRetryTail.halted_mean line 39
8. lemma OAI.ContingencyTables.PhysicalRetryTail.future_live_le line 48
9. def OAI.ContingencyTables.PhysicalRetryTail.tail line 56
10. lemma OAI.ContingencyTables.PhysicalRetryTail.tail_nonnegative line 59
11. lemma OAI.ContingencyTables.PhysicalRetryTail.tail_antitone line 65
12. lemma OAI.ContingencyTables.PhysicalRetryTail.padded_halted_result line 74
13. theorem OAI.ContingencyTables.PhysicalRetryTail.tail_le_failure line 92

    Source documentation

    All successful prefix executions have halted by the prefix cost. This implication is enough even though the failed endpoint is still live.

    theorem tail_le_failure (M : Table Γ Q) (out : Option B → Cfg Γ Q) (c : Cfg Γ Q)
        (p : Experiment (Option B)) (hp : Implements M out c p)
        (hhalt : ∀ b,(out (some b)).state=none) (n : ℕ) (hn : p.cost≤n) :
        tail M c n≤(p.mean (fun b => if b=none then 1 else 0):ℚ) := by
    …

    Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.PhysicalRetryTail.tail