OAI/Combinatorics/ContingencyTables/Counting/ComputedCountingParameters.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Counting schedules computed from the original bounded margins

The capacity-bit sum is formed after the executed endpoint translation. All remaining dimensions, precisions, cutoffs and phase counts use the proved rational/natural formulas. No numeric schedule hypothesis is left to an external caller.

  1. def OAI.ContingencyTables.ComputedCountingParameters.dimensionAllowance line 23
  2. def OAI.ContingencyTables.ComputedCountingParameters.capacityBits line 25
  3. def OAI.ContingencyTables.ComputedCountingParameters.coefficient line 28
  4. def OAI.ContingencyTables.ComputedCountingParameters.binCount line 33
  5. def OAI.ContingencyTables.ComputedCountingParameters.cutoff line 37
  6. def OAI.ContingencyTables.ComputedCountingParameters.phases line 41
  7. lemma OAI.ContingencyTables.ComputedCountingParameters.coefficient_pos line 45
  8. lemma OAI.ContingencyTables.ComputedCountingParameters.binCount_pos line 50
  9. lemma OAI.ContingencyTables.ComputedCountingParameters.cutoff_two line 57
  10. def OAI.ContingencyTables.ComputedCountingParameters.data line 64
  11. lemma OAI.ContingencyTables.ComputedCountingParameters.data_dimension line 71
  12. lemma OAI.ContingencyTables.ComputedCountingParameters.data_capacityBits line 76
  13. lemma OAI.ContingencyTables.ComputedCountingParameters.binCount_cast line 81
  14. lemma OAI.ContingencyTables.ComputedCountingParameters.cutoff_eq line 88
  15. lemma OAI.ContingencyTables.ComputedCountingParameters.phases_final line 94
  16. lemma OAI.ContingencyTables.ComputedCountingParameters.phases_height line 102
  17. def OAI.ContingencyTables.ComputedCountingParameters.start line 110

    Source documentation

    The canonical zero grid point is valid even when there are no free coordinates; its construction does not search the geometric state space.

    def start (hEK : PublishedEdmondsKarp.EdmondsKarp1972Theorem1)
    (r : Fin m→ℕ) (c : Fin n→ℕ) (b : Fin m→Fin n→ℕ)
    (hne : ∃ X,TableTightening.Feasible r c b X) (epsilon : ℚ) (he : 0<epsilon) :
    Grid (I:=Fin (dimension (data hEK r c b hne epsilon he))) (binCount r c b epsilon) :=
…

    Mentions: OAI.ContingencyTables.PublishedEdmondsKarp.EdmondsKarp1972Theorem1, OAI.ContingencyTables.TableTightening.Feasible, OAI.ContingencyTables.ComputedCountingParameters.data, OAI.ContingencyTables.ComputedCountingParameters.binCount

  18. def OAI.ContingencyTables.ComputedCountingParameters.settings line 116