OAI/NumberTheory/Ostmann/Tree/CellGroupExponentialCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact cell-list pigeonhole costs only a fixed exponential in m

  1. theorem OAI.Ostmann.eventual_cell_group_cost line 11
  2. theorem OAI.Ostmann.cell_group_endpoint_rate line 58

    Source documentation

    The endpoint count after fixing all cell lists keeps an explicit exponential rate, with no dependence on the number of fixed labels in it.

    theorem cell_group_endpoint_rate (e s : ℕ) (F X A B m : ℝ)
    (hcount : (e : ℝ) ≤ F * s) (hF : F ≤ Real.exp (B * m))
    (he : Real.sqrt X * Real.exp (-A * m) ≤ e) :
    Real.sqrt X * Real.exp (-(A + B) * m) ≤ s := by
…