OAI/Combinatorics/Sensitivity/Basic.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Finite Boolean flips and the exact maximum/witness interfaces for sensitivity.

  1. theorem OAI.Paper320.flip_empty line 14
  2. theorem OAI.Paper320.flip_singleton_self line 18
  3. theorem OAI.Paper320.flip_singleton_other line 22
  4. theorem OAI.Paper320.flip_flip line 26
  5. theorem OAI.Paper320.flip_insert line 30
  6. theorem OAI.Paper320.flip_prod_same line 38
  7. theorem OAI.Paper320.flip_prod_other line 43
  8. theorem OAI.Paper320.flip_false line 48
  9. theorem OAI.Paper320.flip_differences line 56
  10. theorem OAI.Paper320.sensitivityAt_le_card line 61
  11. theorem OAI.Paper320.sensitivityAt_le_sensitivity line 65
  12. theorem OAI.Paper320.sensitivity_le line 69
  13. theorem OAI.Paper320.sensitivityAt_eq_zero_iff line 73
  14. theorem OAI.Paper320.sensitivityAt_pos line 77
  15. theorem OAI.Paper320.exists_sensitivityAt_eq line 81
  16. theorem OAI.Paper320.blockSensitivityAt_le_blockSensitivity line 87
  17. theorem OAI.Paper320.blockSensitivity_le line 91
  18. theorem OAI.Paper320.le_blockSensitivityAt line 95
  19. theorem OAI.Paper320.blockSensitivityAt_le line 109
  20. theorem OAI.Paper320.exists_blockSensitivityAt_family line 120
  21. theorem OAI.Paper320.le_blockSensitivityAt_of_family line 137
  22. theorem OAI.Paper320.eq_of_singleton_invariant line 160
  23. theorem OAI.Paper320.sensitivity_pos_of_nonconstant line 168