OAI/NumberTheory/Ostmann/Construction/FactorialExponential.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary exponential factorial bounds used in arrangement ratios

  1. theorem OAI.Ostmann.factorial_exp_lower line 11
  2. theorem OAI.Ostmann.factorial_exp_upper line 22
  3. theorem OAI.Ostmann.block_factorial_ratio line 30

    Source documentation

    Normalization of r independent blocks against all permutations of rm slots produces the entropy gain -rm log r.

    theorem block_factorial_ratio {r m : ℕ} (hr : 1 ≤ r) (hm : 1 ≤ m) :
    (m.factorial : ℝ) ^ r / ((r * m).factorial : ℝ) ≤
      Real.exp ((r : ℝ) * m * (1 - Real.log r)) := by
…