OAI/Combinatorics/ContingencyTables/Counting/CompanionObservableApplication.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Observable variance for the actual companion completion-count lifts

The original chain uses the literal factorial lift of h_j. Its proved omission and dual addition properties, with q=W², supply the paper's transversal and observable bounds on the actual disjoint covering slots.

  1. theorem OAI.ContingencyTables.CompanionObservableApplication.transversal_variance line 23
  2. theorem OAI.ContingencyTables.CompanionObservableApplication.observable_poincare line 54