OAI/Combinatorics/Sensitivity/Tower.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

An indexed tower of the literal recursive construction and its common blocks.

  1. def OAI.Paper320.TowerCoordinates line 12
  2. instance OAI.Paper320.towerCoordinatesFintype line 16
  3. def OAI.Paper320.TowerBlockIndex line 23
  4. instance OAI.Paper320.towerBlockIndexFintype line 27
  5. def OAI.Paper320.towerFamily line 34
  6. def OAI.Paper320.towerBlocks line 40
  7. def OAI.Paper320.baseExtension line 46

    Source documentation

    Extend a prescribed initial family to unused index counts without adding assumptions.

    def baseExtension {I : Type} (D : ℕ) (F : Fin D → (I → Bool) → Bool)
    (h : ℕ) (q : Fin h) (x : I → Bool) : Bool :=
…
  8. theorem OAI.Paper320.baseExtension_same line 50
  9. theorem OAI.Paper320.tower_coordinates_card line 55
  10. theorem OAI.Paper320.tower_block_index_card line 66
  11. theorem OAI.Paper320.towerBlocks_card line 77
  12. theorem OAI.Paper320.towerBlocks_nonempty line 89
  13. theorem OAI.Paper320.towerBlocks_pairwise line 96
  14. theorem OAI.Paper320.towerFamily_nested line 103
  15. theorem OAI.Paper320.towerFamily_zero line 118
  16. theorem OAI.Paper320.towerFamily_blocks line 133