OAI/Combinatorics/ContingencyTables/Counting/CompanionEvaluatedWeightProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The executed multiplier times labelled weight

Both factors are computed from the supplied current state. The matrix lookup and the oracle consume no hidden finite-state enumeration.

  1. abbrev OAI.ContingencyTables.CompanionEvaluatedWeightProgram.Frame line 18
  2. abbrev OAI.ContingencyTables.CompanionEvaluatedWeightProgram.Input line 19
  3. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.multiplierInput line 21
  4. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.multiplierInputRealizer line 23
  5. lemma OAI.ContingencyTables.CompanionEvaluatedWeightProgram.polynomial_multiplierInput line 27
  6. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.multiplier line 32
  7. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.multiplierRealizer line 34
  8. lemma OAI.ContingencyTables.CompanionEvaluatedWeightProgram.polynomial_multiplier line 37
  9. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.weightInput line 40
  10. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.weightInputRealizer line 41
  11. lemma OAI.ContingencyTables.CompanionEvaluatedWeightProgram.polynomial_weightInput line 43
  12. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.weight line 49
  13. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.weightRealizer line 50
  14. lemma OAI.ContingencyTables.CompanionEvaluatedWeightProgram.polynomial_weight line 53
  15. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.output line 58
  16. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.outputRealizer line 59
  17. lemma OAI.ContingencyTables.CompanionEvaluatedWeightProgram.polynomial_output line 62
  18. abbrev OAI.ContingencyTables.CompanionEvaluatedWeightProgram.LabelIndex line 75
  19. def OAI.ContingencyTables.CompanionEvaluatedWeightProgram.sourceWeights line 78
  20. lemma OAI.ContingencyTables.CompanionEvaluatedWeightProgram.multiplier_code line 82
  21. theorem OAI.ContingencyTables.CompanionEvaluatedWeightProgram.sameLaw_evaluated line 93

    Source documentation

    Arbitrary observables of the executed weighted query agree with the proved mathematical oracle, including outcomes on its failure event.

    theorem sameLaw_evaluated (A : Instance (Fin m) (Fin n)) (C K j : ℕ)
    (hC : 0 < C) (hj : j ≤ rationalHeight A C) (hK : 1 ≤ K)
    (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=CompanionOracleDensity.binWidth A C)
    (xi : ℚ) (hxi : 0 < xi) (z : View A → ℕ)
    (v : Grid (I := Fin (RootedCatalogGrid.freeCount A)) K) (degree depth : List Bool)
…

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.RootedCatalogGrid.freeCount