OAI/Combinatorics/ContingencyTables/Rooted/RootedPhaseWords.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fresh selected-root oracle words and actual rational phase updates

  1. def OAI.ContingencyTables.RootedPhaseWords.observedTerm line 19
  2. def OAI.ContingencyTables.RootedPhaseWords.observedRatio line 27
  3. lemma OAI.ContingencyTables.RootedPhaseWords.observedTerm_nonneg line 34
  4. lemma OAI.ContingencyTables.RootedPhaseWords.observedRatio_positive line 46
  5. def OAI.ContingencyTables.RootedPhaseWords.update line 69
  6. theorem OAI.ContingencyTables.RootedPhaseWords.update_positive line 81

    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) (R : RootedCompletion.Selection A.T) (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.RootedCompletion.Selection

  7. lemma OAI.ContingencyTables.RootedPhaseWords.update_multiplier_cast line 98