OAI/Combinatorics/ContingencyTables/Machines/ScheduledCountSemantics.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The scheduled executable numerator vector is the public sampler's law

  1. lemma OAI.ContingencyTables.SmallGraphProfiles.dyadic_trialDenom line 18
  2. lemma OAI.ContingencyTables.SmallGraphProfiles.scheduledTrialDenominator_dense line 30
  3. lemma OAI.ContingencyTables.SmallGraphProfiles.scheduledTrialDenominator_unit line 39
  4. lemma OAI.ContingencyTables.SmallGraphProfiles.scheduledTrialDenominator_pos line 45
  5. lemma OAI.ContingencyTables.SmallGraphProfiles.scheduledOuterInput_code line 49
  6. def OAI.ContingencyTables.SmallGraphProfiles.scheduledCountsLaw line 67

    Source documentation

    No extra table oracle: this is the integer law of the ordinary public branch.

    def scheduledCountsLaw (htotal : ∑ i,r i=∑ j,c j) (k : ℕ) :
    IntegerLaw (Table r c)
      ((scheduledTrialDenominator ((List.ofFn r,List.ofFn c),k))^(outerTrials d k)) :=
…

    Mentions: OAI.ContingencyTables.IntegerLaw, OAI.ContingencyTables.Table, OAI.ContingencyTables.outerTrials

  7. lemma OAI.ContingencyTables.SmallGraphProfiles.scheduledDraw_dense line 83
  8. lemma OAI.ContingencyTables.SmallGraphProfiles.scheduledDraw_unit line 95
  9. lemma OAI.ContingencyTables.SmallGraphProfiles.scheduledCountsLaw_law line 105
  10. lemma OAI.ContingencyTables.SmallGraphProfiles.scheduledCounts_actual line 122

    Source documentation

    Every literal vector entry equals the corresponding embedded table count, including zero at infeasible matrices in the original bounding box.

    lemma scheduledCounts_actual (htotal : ∑ i,r i=∑ j,c j) (k : ℕ) :
    scheduledCounts ((List.ofFn r,List.ofFn c),k)=
      List.ofFn (((scheduledCountsLaw r c htotal k).push (index r c le_rfl)).count) := by
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.scheduledCountsLaw