OAI/Combinatorics/Sensitivity/Or.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Balancing the zero and one sensitivities by an OR of disjoint copies.

  1. def OAI.Paper320.orBits line 14
  2. theorem OAI.Paper320.orBits_eq_true line 16
  3. theorem OAI.Paper320.orBits_eq_false line 19
  4. theorem OAI.Paper320.orBits_zero line 22
  5. theorem OAI.Paper320.orBits_flip_of_witness line 25
  6. def OAI.Paper320.orCopies line 32
  7. theorem OAI.Paper320.orCopies_zero line 34
  8. theorem OAI.Paper320.sensitivity_orCopies_le line 40
  9. theorem OAI.Paper320.card_le_blockSensitivityAt_orBits_zero line 73
  10. theorem OAI.Paper320.blockSensitivityAt_orCopies_zero line 85