OAI/NumberTheory/Ostmann/Construction/RepeatedTupleEntropy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The broad-prime normalization cancels the repeated-tuple entropy

  1. theorem OAI.Ostmann.eventual_repeated_tuple_entropy line 11

    Source documentation

    There are two copies of the m broad positions and a fixed number of cell roles. The L^(-2m) in their actual prior removes the m log m cost.

    theorem eventual_repeated_tuple_entropy (r : ℕ) (z : ℝ) (hz : 0 < z) :
    ∀ᶠ m : ℕ in atTop, ∀ L : ℝ, 0 < L → (m : ℝ) ≤ z * L →
      ((2 * (m + r) : ℕ) : ℝ) ^ (2 * (m + r)) / L ^ (2 * m) ≤
        Real.exp ((2 * Real.log (4 * z) + 1) * m) := by
…