OAI/NumberTheory/Ostmann/Tree/BadArrangementCount.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Counting bad permutations through their actual overlap components

  1. def OAI.Ostmann.BadBulkArrangement line 12
  2. theorem OAI.Ostmann.badBulkArrangement_witness line 15
  3. theorem OAI.Ostmann.card_badBulkArrangement_le line 45
  4. theorem OAI.Ostmann.badBulkArrangement_count_bound line 59

    Source documentation

    The arrangement count used in Section 9. The prefactor depends only on the number of leaves r; all m-dependence is explicit.

    theorem badBulkArrangement_count_bound {r m : ℕ} (hr : 1 ≤ r) (hm : 0 < m) :
    (Fintype.card {e : Equiv.Perm (Fin r × Fin m) // BadBulkArrangement e} : ℝ) ≤
      ((r + 1) * r ^ (2 * r) : ℕ) * (m.factorial : ℝ) ^ r *
        Real.exp ((m : ℝ) * r * (Real.log r + 1) / 4) := by
…

    Mentions: OAI.Ostmann.BadBulkArrangement