OAI/Combinatorics/Sensitivity/Construction.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The initial family, recursively constructed predicates, and final OR.

  1. def OAI.Paper320.constructionBase line 16
  2. abbrev OAI.Paper320.ConstructionCoordinates line 18
  3. def OAI.Paper320.terminalPredicate line 21
  4. theorem OAI.Paper320.construction_base_nested line 25
  5. theorem OAI.Paper320.construction_base_zero line 29
  6. theorem OAI.Paper320.construction_base_blocks line 34
  7. theorem OAI.Paper320.terminalPredicate_zero line 41
  8. theorem OAI.Paper320.terminalPredicate_blocks line 47
  9. theorem OAI.Paper320.terminalPredicate_blockSensitivity line 56
  10. theorem OAI.Paper320.construction_profiles line 67
  11. theorem OAI.Paper320.terminalPredicate_sensitivityAt line 89
  12. def OAI.Paper320.finalBoolean line 103
  13. theorem OAI.Paper320.finalBoolean_zero line 107
  14. theorem OAI.Paper320.finalBoolean_sensitivity line 112
  15. theorem OAI.Paper320.finalBoolean_blockSensitivity line 121
  16. def OAI.Paper320.constructionDimension line 133
  17. theorem OAI.Paper320.final_coordinates_card line 136
  18. def OAI.Paper320.finalWitness line 142
  19. theorem OAI.Paper320.finalWitness_zero line 146
  20. theorem OAI.Paper320.finalWitness_sensitivity line 150
  21. theorem OAI.Paper320.finalWitness_blockSensitivity line 157
  22. theorem OAI.Paper320.constructionDimension_pos line 163