OAI/NumberTheory/Ostmann/Tree/BadArrangementFraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exponentially small proportion of bad bulk arrangements

  1. theorem OAI.Ostmann.badBulkArrangement_fraction_bound line 12
  2. theorem OAI.Ostmann.card_bulkPerm line 36

    Source documentation

    The total number of labeled arrangements is (rm)!, including when different slots happen to contain the same prime value.

    theorem card_bulkPerm (r m : ℕ) :
    Fintype.card (Equiv.Perm (Fin r × Fin m)) = (r * m).factorial := by
…