OAI/NumberTheory/Ostmann/Construction/FinalFactorialBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The factorial gain from the actual final reassignment family

  1. theorem OAI.Ostmann.final_reassignment_card_exp_lower line 12
  2. theorem OAI.Ostmann.final_diagonal_entropy_bound line 29

    Source documentation

    At fixed depth, the diagonal exponential cost is beaten by the factorial family as soon as its entropy margin is positive.

    theorem final_diagonal_entropy_bound (n m : ℕ) (a C : ℝ)
    (ha : a ≤ (n : ℝ) * Real.log 2 - 1 - C) :
    Real.exp (C * (2 ^ (n + 1) : ℝ) * m) /
        (Fintype.card (FinalParityReassignments n m) : ℝ) ≤
      Real.exp (-a * (2 ^ (n + 1) : ℝ) * m) := by
…

    Mentions: OAI.Ostmann.FinalParityReassignments