OAI/Combinatorics/Sensitivity/Composition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Disjoint Boolean composition, with each child retaining its own raw coordinates.

  1. def OAI.Paper320.compose line 14
  2. theorem OAI.Paper320.compose_flip_sensitive_iff line 18
  3. theorem OAI.Paper320.compose_zero line 45
  4. theorem OAI.Paper320.compose_flip_product_zero line 50
  5. theorem OAI.Paper320.sensitivityAt_compose line 75
  6. theorem OAI.Paper320.sensitivity_compose_le line 91
  7. theorem OAI.Paper320.blockSensitivityAt_compose_zero_le line 106