OAI/NumberTheory/EgyptianFractions/GeometricRandomResidues.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.RandomProducts.eventually_common_geometric_random_residues line 15

   Source documentation

   The middle-level small-residue and every-terminal-numerator guarantees hold for one common family of actual labelled prime samples. The onset is uniform in the prime pool and no Fourier hypothesis remains.

   theorem eventually_common_geometric_random_residues (D : ℝ) (hD : 1 ≤ D) :
       ∀ᶠ S : ℝ in atTop, ∀ P : Finset ℕ,
         (∀ p ∈ P, Nat.Prime p) →
         (∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101) →
         S ^ 99 ≤ (P.card : ℝ) →
         ∃ (f : Fin 1000 → ((Fin (blockLength S) × Bool) → P))
           (exceptional : ℕ → Finset ℕ),
           (∀ j ∈ middleTests D S, exceptional j ⊆ middleLevel D S j ∧
             ((exceptional j).card : ℝ) ≤
               cutoff D S j * Real.exp (-(blockLength S : ℝ) / 1000) ∧
             ∀ u ∈ middleLevel D S j, u ∉ exceptional j →
               (Real.exp (-(blockLength S : ℝ) / 10000) / 2) *
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.RandomProducts.blockLength

2. theorem OAI.Problem337.RandomProducts.eventually_common_geometric_random_fractional_residues line 76

   Source documentation

   The middle-level small-residue and every-terminal-numerator guarantees hold for one common family of actual labelled prime samples. The onset is uniform in the prime pool and no Fourier hypothesis remains.

   theorem eventually_common_geometric_random_fractional_residues (D : ℝ) (hD : 1 ≤ D) :
       ∀ᶠ S : ℝ in atTop, ∀ P : Finset ℕ,
         (∀ p ∈ P, Nat.Prime p) →
         (∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101) →
         S ^ 99 ≤ (P.card : ℝ) →
         ∃ (f : Fin 1000 → ((Fin (blockLength S) × Bool) → P))
           (exceptional : ℕ → Finset ℕ),
           (∀ j ∈ middleTests D S, exceptional j ⊆ middleLevel D S j ∧
             ((exceptional j).card : ℝ) ≤
               cutoff D S j * Real.exp (-(blockLength S : ℝ) / 1000) ∧
             ∀ u ∈ middleLevel D S j, u ∉ exceptional j →
               (Real.exp (-(blockLength S : ℝ) / 10000) / 2) *
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.RandomProducts.blockLength