OAI/NumberTheory/Ostmann/Construction/CommonAnchorCells.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixing the two anchor-cell indices per depth before the target words

  1. theorem OAI.Ostmann.common_bounded_anchor_cells line 9
  2. theorem OAI.Ostmann.anchor_cell_cost line 45

    Source documentation

    The anchor pigeonhole has an absolute exponential rate when its fixed number of slots is below the bulk scale.

    theorem anchor_cell_cost (k B : ℕ) (C L z m : ℝ)
    (hC : 0 ≤ C) (hL : 0 ≤ L) (hsize : (2 * k : ℕ) ≤ z)
    (hB : (B + 1 : ℕ) ≤ Real.exp (C * L)) (hm : z * L ≤ 2 * m) :
    (((B + 1) ^ (2 * k) : ℕ) : ℝ) ≤ Real.exp (2 * C * m) := by
…