OAI/Combinatorics/ContingencyTables/Counting/CompanionMultiplierProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A binary rational program for each learned multiplier

The two observed frequencies have the same trajectory length, which cancels before division. Thus one multiplication by the ratio of the actual integer counts implements the exact rational update, including the zero-denominator behavior on unsuccessful histories.

  1. def OAI.ContingencyTables.CompanionMultiplierProgram.countRatio line 21
  2. def OAI.ContingencyTables.CompanionMultiplierProgram.countPlainRealizer line 24
  3. def OAI.ContingencyTables.CompanionMultiplierProgram.countRatioRealizer line 28
  4. lemma OAI.ContingencyTables.CompanionMultiplierProgram.polynomial_countRatio line 31
  5. abbrev OAI.ContingencyTables.CompanionMultiplierProgram.UpdateInput line 35
  6. def OAI.ContingencyTables.CompanionMultiplierProgram.updateCode line 37
  7. def OAI.ContingencyTables.CompanionMultiplierProgram.diagonalRealizer line 40
  8. lemma OAI.ContingencyTables.CompanionMultiplierProgram.polynomial_diagonal line 44
  9. def OAI.ContingencyTables.CompanionMultiplierProgram.updateCodeRealizer line 51
  10. theorem OAI.ContingencyTables.CompanionMultiplierProgram.polynomial_updateCode line 56
  11. lemma OAI.ContingencyTables.CompanionMultiplierProgram.updateCode_value line 63
  12. theorem OAI.ContingencyTables.CompanionMultiplierProgram.updateCode_learn line 81

    Source documentation

    This is the literal source multiplier update at a pair of actual labels, not a surrogate recurrence on unrelated rational values.

    theorem updateCode_learn (states : List (Set (Labels A×Bool)))
    (hlen : 0<states.length) (w : CompanionRationalUpdates.Pair A → CompanionRationalUpdates.Pair A → ℚ)
    (i j : Fin p) (hw : 0≤w (pair (g i)) (pair (g j))) :
    TreeFraction.val (updateCode (((orderedCatalog A g e,states.map (encodeSet e)),(i.val,j.val)),
      TreeFraction.repr (w (pair (g i)) (pair (g j)))))=
        rationalLearn pairs w states (pair (g i)) (pair (g j)) := by
…

    Mentions: OAI.ContingencyTables.CompanionRationalUpdates.Pair, OAI.ContingencyTables.CompanionMultiplierProgram.updateCode