OAI/NumberTheory/EgyptianFractions/PrimePoolSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.eventually_residue_prime_vector line 13

   Source documentation

   Select the deterministic prime vector of length floor(S/log S) from the proved elementary prime pool.

   theorem eventually_residue_prime_vector :
       ∀ᶠ S : ℝ in atTop,
         ∃ p : Fin ⌊S / Real.log S⌋₊ → ℕ,
           Function.Injective p ∧
           (∀ i, Nat.Prime (p i) ∧ S ^ 100 < (p i : ℝ) ∧ (p i : ℝ) ≤ S ^ 101) ∧
           Function.Injective (ResidueConstruction.subsetEntry p) ∧
           (Finset.univ.image (ResidueConstruction.subsetEntry p)).card = 2 ^ ⌊S / Real.log S⌋₊ := by
   …

   Mentions: OAI.Problem337.ResidueConstruction.subsetEntry