OAI/NumberTheory/Ostmann/Construction/BadMatchingHarmonicBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.factorial_harmonic_entropy line 11
2. theorem OAI.Ostmann.bad_separated_harmonic_bound line 32

   Source documentation

   This is the bad-part exponent before the transfer gap is subtracted. The only prefactor left is constant at fixed tree depth and nonbulk slots.

   theorem bad_separated_harmonic_bound {r m : ℕ} {N : Type*} [Fintype N]
       (hr : 1 ≤ r) (hm0 : 0 < m) (L z C : ℝ)
       (hL : 0 < L) (hz : 0 < z) (hm : (m : ℝ) ≤ z * L) :
       (Fintype.card {e : PartitionMatching (@sumSide (Fin r × Fin m) N)
         (@sumSide (Fin r × Fin m) N) // BadBulkArrangement (separatedMatchingLeft e)} : ℝ) *
         (L⁻¹) ^ (r * m) * Real.exp (C * (r * m : ℕ)) ≤
         (((r + 1) * r ^ (2 * r) : ℕ) : ℝ) * (Fintype.card N).factorial *
           Real.exp ((Real.log z + Real.log r / 4 + C + 1 / 4) * (r * m : ℕ)) := by
   …

   Mentions: OAI.Ostmann.PartitionMatching, OAI.Ostmann.sumSide, OAI.Ostmann.BadBulkArrangement, OAI.Ostmann.separatedMatchingLeft