OAI/Combinatorics/ContingencyTables/Counting/CompanionRationalUpdates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Exact rational multiplier updates of the outer annealing run

  1. abbrev OAI.ContingencyTables.CompanionRationalUpdates.Pair line 18
  2. def OAI.ContingencyTables.CompanionRationalUpdates.initial line 20
  3. lemma OAI.ContingencyTables.CompanionRationalUpdates.initial_positive line 25
  4. lemma OAI.ContingencyTables.CompanionRationalUpdates.initial_cast line 29
  5. lemma OAI.ContingencyTables.CompanionRationalUpdates.initial_binary_bound line 36

    Source documentation

    The initializer has a uniform binary bound using only the polynomial small-cell scale, including values at pair arguments outside defect types.

    lemma initial_binary_bound (A : Instance I J) (p q : Pair A) :
    RatBound (initial A p q) (2^(A.W+4)) := by
…

    Mentions: OAI.ContingencyTables.CompanionRationalUpdates.Pair, OAI.ContingencyTables.CompanionRationalUpdates.initial

  6. def OAI.ContingencyTables.CompanionRationalUpdates.plainCount line 59
  7. def OAI.ContingencyTables.CompanionRationalUpdates.defectCount line 62
  8. lemma OAI.ContingencyTables.CompanionRationalUpdates.plainCount_le line 65
  9. lemma OAI.ContingencyTables.CompanionRationalUpdates.defectCount_le line 68
  10. lemma OAI.ContingencyTables.CompanionRationalUpdates.rationalLearn_counts line 71
  11. def OAI.ContingencyTables.CompanionRationalUpdates.CountsPositive line 83

    Source documentation

    Every decision to divide is preceded by the literal positive-count check used in the source algorithm.

    def CountsPositive (A : Instance I J) (l : List (Set (Labels A×Bool))) : Prop :=
…
  12. def OAI.ContingencyTables.CompanionRationalUpdates.checkedUpdate line 86
  13. lemma OAI.ContingencyTables.CompanionRationalUpdates.checkedUpdate_positive line 90
  14. def OAI.ContingencyTables.CompanionRationalUpdates.history line 107

    Source documentation

    The literal rational history is exactly the real history, including all unsuccessful histories.

    def history (A : Instance I J) (samples : ℕ → List (Set (Labels A×Bool))) :
    ℕ → Pair A → Pair A → ℚ
  | 0 => initial A
  | j+1 => rationalLearn pairs (history A samples j) (samples j)

    Mentions: OAI.ContingencyTables.CompanionRationalUpdates.Pair, OAI.ContingencyTables.CompanionRationalUpdates.initial

  15. lemma OAI.ContingencyTables.CompanionRationalUpdates.history_cast line 112
  16. theorem OAI.ContingencyTables.CompanionRationalUpdates.history_good line 126
  17. lemma OAI.ContingencyTables.CompanionRationalUpdates.history_positive line 137
  18. theorem OAI.ContingencyTables.CompanionRationalUpdates.history_binary_bound line 146

    Source documentation

    Every bounded observation history has polynomial-length rational multipliers, without a success or positivity assumption on that history.

    theorem history_binary_bound (A : Instance I J) (samples : ℕ → List (Set (Labels A×Bool)))
    (N j : ℕ) (hlen : ∀ a<j,(samples a).length ≤ N) (p q : Pair A) :
    RatBound (history A samples j p q) (2^(A.W+4+j*N)) := by
…

    Mentions: OAI.ContingencyTables.CompanionRationalUpdates.Pair, OAI.ContingencyTables.CompanionRationalUpdates.history