OAI/NumberTheory/EgyptianFractions/DeterministicSubsetResidues.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.eventually_deterministic_subset_residues line 14

   Source documentation

   High-level residue distribution for the canonical deterministic prime block. The exact binary index set and all cardinality and size conditions are discharged, so this is ready for the common-denominator construction.

   theorem eventually_deterministic_subset_residues (D : ℝ) (hD : 255 ≤ D) :
       ∀ᶠ S : ℝ in atTop, ∀ (m : ℕ) (X : ℝ) (C : ℕ),
         S / (2 * Real.log S) ≤ (m : ℝ) → (m : ℝ) ≤ S / Real.log S →
         Real.exp S ≤ X → X ≤ Real.exp (D * S / 4) →
         Real.exp (D * S) ≤ (C : ℝ) → (C : ℝ) ≤ Real.exp (2 * D * S) →
         ∀ p : Fin m → ℕ, (∀ j, (p j).Prime) → Function.Injective p →
           (∀ j, (p j : ℝ) ≤ S ^ (101 : ℕ)) →
           ∃ E : Finset ℕ,
             E ⊆ Finset.Icc (⌊Real.exp (-(m : ℝ) / 10000) * X⌋₊ + 1) ⌊X⌋₊ ∧
             (E.card : ℝ) ≤ X * Real.exp (-(m : ℝ) / 1000) ∧
             ∀ u ∈ Finset.Icc (⌊Real.exp (-(m : ℝ) / 10000) * X⌋₊ + 1) ⌊X⌋₊,
               u ∉ E →
   …

   Mentions: OAI.Problem337.D