OAI/Combinatorics/ContingencyTables/Counting/CompanionPhaseWords.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionPhaseWords.observationBits line 19

   Source documentation

   Separate current-parameter and next-parameter oracle words are reserved at every observed state, including states at which they are unused.

   def observationBits (A : Instance I J) (C K j : ℕ) (xi : ℚ) : ℕ :=
   …

2. def OAI.ContingencyTables.CompanionPhaseWords.phaseBits line 22
3. def OAI.ContingencyTables.CompanionPhaseWords.phaseWordEquiv line 25
4. def OAI.ContingencyTables.CompanionPhaseWords.observedTerm line 31
5. def OAI.ContingencyTables.CompanionPhaseWords.observedRatio line 39
6. lemma OAI.ContingencyTables.CompanionPhaseWords.observedTerm_nonneg line 46
7. lemma OAI.ContingencyTables.CompanionPhaseWords.observedRatio_positive line 58
8. structure OAI.ContingencyTables.CompanionPhaseWords.Stored line 81
9. def OAI.ContingencyTables.CompanionPhaseWords.update line 85
10. theorem OAI.ContingencyTables.CompanionPhaseWords.update_positive line 97

    Source documentation

    A nonaborting update keeps every stored rational positive, even if all its weight calls were statistically inaccurate.

    theorem update_positive (A : Instance I J) (C : ℕ) (hC : 0 < C) (K j N : ℕ)
        (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
        (hj : j+1 ≤ rationalHeight A C) (xi : ℚ) (hx0 : 0 < xi) (hx1 : xi < 1)
        (v : Grid (I := Fin (dimension A)) K) (old next : Stored A)
    …

    Mentions: OAI.ContingencyTables.CompanionPhaseWords.Stored

11. lemma OAI.ContingencyTables.CompanionPhaseWords.update_multiplier_cast line 114