OAI/Combinatorics/ContingencyTables/Transport/FiniteObservableTransport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact transport of finite experiments with rational outputs

Output values need not form a finite type. Equality against every real observable is preserved by deterministic postprocessing and by the independent arrays used in the counting estimator.

  1. def OAI.ContingencyTables.FiniteObservableTransport.SameLaw line 21
  2. lemma OAI.ContingencyTables.FiniteObservableTransport.SameLaw.map line 24
  3. lemma OAI.ContingencyTables.FiniteObservableTransport.SameLaw.prod line 29
  4. lemma OAI.ContingencyTables.FiniteObservableTransport.SameLaw.independent line 41
  5. lemma OAI.ContingencyTables.FiniteObservableTransport.indexed line 47