OAI/Combinatorics/Sensitivity/Iterates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Repeated disjoint composition with explicit finite raw-coordinate types.

  1. abbrev OAI.Paper320.IterateCoord line 13
  2. instance OAI.Paper320.iterateCoordFintype line 17
  3. def OAI.Paper320.iterateCompose line 24
  4. theorem OAI.Paper320.iterateCompose_one line 29
  5. theorem OAI.Paper320.iterateCompose_zero line 33
  6. theorem OAI.Paper320.iterateCoord_card line 42
  7. theorem OAI.Paper320.sensitivity_iterateCompose_le line 50
  8. theorem OAI.Paper320.blockSensitivityAt_iterateCompose_zero line 64
  9. def OAI.Paper320.iterateFin line 91
  10. theorem OAI.Paper320.iterateFin_zero line 95
  11. theorem OAI.Paper320.sensitivity_iterateFin_le line 100
  12. theorem OAI.Paper320.blockSensitivityAt_iterateFin_zero line 105
  13. theorem OAI.Paper320.nonconstant_of_blockSensitivityAt_pos line 112
  14. theorem OAI.Paper320.iterateFin_nonconstant line 119