OAI/NumberTheory/Ostmann/Construction/ConstituentFinalCostData.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual final pair counts at the linear constituent-size scale

  1. def OAI.Ostmann.constituentFinalCountRate line 11

    Source documentation

    This single constant bounds both the prime-test count and the quadratic pairwise-coprimality count of the literal final histories.

    noncomputable def constituentFinalCountRate (N n : ℕ) (s : ℝ) : ℝ :=
…
  2. theorem OAI.Ostmann.constituentFinalCountRate_nonneg line 14
  3. theorem OAI.Ostmann.constituent_final_linear_counts line 19