OAI/Combinatorics/ContingencyTables/Counting/CompanionChainValidator.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Polynomial validation of paired binary states

The bounded-profile arithmetic test specializes to width one. Thus the companion's state filter is a concrete list program on the two coordinates of every labelled pair.

  1. lemma OAI.ContingencyTables.CompanionChainValidator.single_iff_occupancy line 23
  2. lemma OAI.ContingencyTables.CompanionChainValidator.empty_iff_occupancy line 29
  3. lemma OAI.ContingencyTables.CompanionChainValidator.full_iff_occupancy line 35
  4. lemma OAI.ContingencyTables.CompanionChainValidator.plain_iff_occupancy line 40
  5. lemma OAI.ContingencyTables.CompanionChainValidator.defect_iff_occupancy line 49
  6. lemma OAI.ContingencyTables.CompanionChainValidator.chain_iff_occupancy line 72
  7. theorem OAI.ContingencyTables.CompanionChainValidator.paired_pattern_iff line 86

    Source documentation

    Width one is exactly the companion's labelled paired-state test.

    theorem paired_pattern_iff {m : ℕ} (e : Fin m ≃ P) (S : Set (P×Bool)) :
    patternTest ((List.ofFn (fun i => if (e i,false)∈S then 1 else 0),
      List.ofFn (fun i => if (e i,true)∈S then 1 else 0)),1)=true ↔ ChainState pairs S := by
…
  8. abbrev OAI.ContingencyTables.CompanionChainValidator.ValidatorInput line 107
  9. def OAI.ContingencyTables.CompanionChainValidator.pairFirstLookup line 109
  10. def OAI.ContingencyTables.CompanionChainValidator.pairSecondLookup line 112
  11. lemma OAI.ContingencyTables.CompanionChainValidator.polynomial_pairFirstLookup line 115
  12. lemma OAI.ContingencyTables.CompanionChainValidator.polynomial_pairSecondLookup line 119
  13. def OAI.ContingencyTables.CompanionChainValidator.pairedStateTest line 123
  14. def OAI.ContingencyTables.CompanionChainValidator.pairedStateTestRealizer line 127
  15. theorem OAI.ContingencyTables.CompanionChainValidator.polynomial_pairedStateTest line 132
  16. def OAI.ContingencyTables.CompanionChainValidator.labelEquiv line 143
  17. def OAI.ContingencyTables.CompanionChainValidator.pairCatalog line 146
  18. theorem OAI.ContingencyTables.CompanionChainValidator.pairedStateTest_encode line 152

    Source documentation

    This list program checks the literal companion state, with no feasibility oracle or whole-state enumeration.

    theorem pairedStateTest_encode (A : Instance I J) (S : Set (Labels A×Bool)) :
    pairedStateTest (pairCatalog A,encodeSet (coordinateEquiv A) S)=true ↔ ChainState pairs S := by
…

    Mentions: OAI.ContingencyTables.CompanionChainValidator.pairedStateTest, OAI.ContingencyTables.CompanionChainValidator.pairCatalog