OAI/Combinatorics/ContingencyTables/Rooted/RootedEstimatorWordSemantics.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.RootedEstimatorWordProgram.Banks line 14
2. def OAI.ContingencyTables.RootedEstimatorWordProgram.wordEquiv line 17
3. def OAI.ContingencyTables.RootedEstimatorWordProgram.input line 21
4. def OAI.ContingencyTables.RootedEstimatorWordProgram.encodeBanks line 24
5. def OAI.ContingencyTables.RootedEstimatorWordProgram.recodeBanks line 32
6. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.encodeBanks_recode line 36
7. def OAI.ContingencyTables.RootedEstimatorWordProgram.bankInput line 46
8. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.ratioBlock_input line 50
9. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.ratioBlocks_input line 65
10. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.correctionBlock_input line 80
11. theorem OAI.ContingencyTables.RootedEstimatorWordProgram.prepare_input line 106

    Source documentation

    Every input bit belongs to exactly one prescribed sample word. The positivity conditions merely ensure that complete-word parsing retains all scheduled sample rows.

    theorem prepare_input (c : Context) (markers : List Bool×List Bool)
        (hs : 0 < c.2.1.2) (hr : 0 < ratioWidth c) (ht : 0 < correctionWidth c)
        (bits : Fin (wordWidth c) → Bool) :
        prepare (input c markers bits)=bankInput c markers (wordEquiv c bits) := by
    …

    Mentions: OAI.ContingencyTables.RootedEstimatorWordProgram.prepare, OAI.ContingencyTables.RootedEstimatorWordProgram.input, OAI.ContingencyTables.RootedEstimatorWordProgram.bankInput, OAI.ContingencyTables.RootedEstimatorWordProgram.wordEquiv