OAI/NumberTheory/EgyptianFractions/RandomGcdBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.RandomProducts.large_gcd_probability_le_exp line 12

   Source documentation

   A concrete large-gcd probability estimate for uniform samples from a prime set. This retains all sample multiplicities, and uses only finite counting.

   theorem large_gcd_probability_le_exp (P : Finset ℕ) (t u : ℕ) (S V : ℝ)
       (hP : P.Nonempty) (hS : 1 < S) (hV : 0 ≤ V)
       (hprime : ∀ p ∈ P, Nat.Prime p)
       (hmax : ∀ p ∈ P, (p : ℝ) ≤ S ^ 101)
       (ht : (t : ℝ) ≤ S) (hhits : ((P.filter (fun p => p ∣ u)).card : ℝ) ≤ S)
       (hsize : S ^ 99 ≤ (P.card : ℝ)) :
       (((sampleWords P t).filter (fun f =>
         Real.exp ((2 / 25 : ℝ) * V) < (Nat.gcd (∏ i, f i) u : ℝ))).card : ℝ) /
           (P.card : ℝ) ^ t ≤ Real.exp (-V / 20) := by
   …

   Mentions: OAI.Problem337.RandomProducts.sampleWords

2. theorem OAI.Problem337.RandomProducts.large_frequency_gcd_probability_le_exp line 59

   Source documentation

   The same estimate permits a small fixed frequency factor in the gcd.

   theorem large_frequency_gcd_probability_le_exp (P : Finset ℕ) (t u l : ℕ) (S V : ℝ)
       (hP : P.Nonempty) (hS : 1 < S) (hV : 0 ≤ V)
       (hprime : ∀ p ∈ P, Nat.Prime p)
       (hmax : ∀ p ∈ P, (p : ℝ) ≤ S ^ 101)
       (ht : (t : ℝ) ≤ S) (hhits : ((P.filter (fun p => p ∣ u)).card : ℝ) ≤ S)
       (hsize : S ^ 99 ≤ (P.card : ℝ)) (hl : 0 < l)
       (hlbound : (l : ℝ) ≤ Real.exp (V / 200)) :
       (((sampleWords P t).filter (fun f =>
         Real.exp (V / 10) < (Nat.gcd (l * ∏ i, f i) u : ℝ))).card : ℝ) /
           (P.card : ℝ) ^ t ≤ Real.exp (-V / 20) := by
   …

   Mentions: OAI.Problem337.RandomProducts.sampleWords

3. theorem OAI.Problem337.RandomProducts.small_reduced_modulus_probability_le line 107

   Source documentation

   Reduced moduli below exp (0.9 V) form an exponentially small set of samples. This is the random-gcd estimate used before applying bilinear Fourier cancellation.

   theorem small_reduced_modulus_probability_le (P : Finset ℕ) (t u l : ℕ) (S V : ℝ)
       (hP : P.Nonempty) (hS : 1 < S) (hV : 0 ≤ V) (huexp : (u : ℝ) = Real.exp V)
       (hprime : ∀ p ∈ P, Nat.Prime p)
       (hmax : ∀ p ∈ P, (p : ℝ) ≤ S ^ 101)
       (ht : (t : ℝ) ≤ S) (hhits : ((P.filter (fun p => p ∣ u)).card : ℝ) ≤ S)
       (hsize : S ^ 99 ≤ (P.card : ℝ)) (hl : 0 < l)
       (hlbound : (l : ℝ) ≤ Real.exp (V / 200)) :
       (((sampleWords P t).filter (fun f =>
         ((u / Nat.gcd (l * ∏ i, f i) u : ℕ) : ℝ) < Real.exp (9 * V / 10))).card : ℝ) /
           (P.card : ℝ) ^ t ≤ Real.exp (-V / 20) := by
   …

   Mentions: OAI.Problem337.RandomProducts.sampleWords

4. theorem OAI.Problem337.RandomProducts.random_gcd_exception_bound line 151

   Source documentation

   The random-gcd bound with exactly the prime sampling scale used in the manuscript. No asymptotic number-theory result is hidden: existence and cardinality of the prime set are explicit hypotheses, while the entire exceptional-event estimate is proved.

   theorem random_gcd_exception_bound (P : Finset ℕ) (t u l : ℕ) (S V : ℝ)
       (hP : P.Nonempty) (hS : 2 ≤ S) (hV : 0 ≤ V) (hVS : V ≤ S)
       (huexp : (u : ℝ) = Real.exp V) (hprime : ∀ p ∈ P, Nat.Prime p)
       (hinterval : ∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ 2 * S ^ 100)
       (ht : (t : ℝ) ≤ S) (hsize : S ^ 99 ≤ (P.card : ℝ)) (hl : 0 < l)
       (hlbound : (l : ℝ) ≤ Real.exp (V / 200)) :
       (((sampleWords P t).filter (fun f =>
         ((u / Nat.gcd (l * ∏ i, f i) u : ℕ) : ℝ) < Real.exp (9 * V / 10))).card : ℝ) /
           (P.card : ℝ) ^ t ≤ Real.exp (-V / 20) := by
   …

   Mentions: OAI.Problem337.RandomProducts.sampleWords

5. theorem OAI.Problem337.RandomProducts.random_gcd_exception_bound_wide line 192

   Source documentation

   The random-gcd bound with exactly the prime sampling scale used in the manuscript. No asymptotic number-theory result is hidden: existence and cardinality of the prime set are explicit hypotheses, while the entire exceptional-event estimate is proved.

   theorem random_gcd_exception_bound_wide (P : Finset ℕ) (t u l : ℕ) (S V : ℝ)
       (hP : P.Nonempty) (hS : 2 ≤ S) (hV : 0 ≤ V) (hVS : V ≤ S)
       (huexp : (u : ℝ) = Real.exp V) (hprime : ∀ p ∈ P, Nat.Prime p)
       (hinterval : ∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101)
       (ht : (t : ℝ) ≤ S) (hsize : S ^ 99 ≤ (P.card : ℝ)) (hl : 0 < l)
       (hlbound : (l : ℝ) ≤ Real.exp (V / 200)) :
       (((sampleWords P t).filter (fun f =>
         ((u / Nat.gcd (l * ∏ i, f i) u : ℕ) : ℝ) < Real.exp (9 * V / 10))).card : ℝ) /
           (P.card : ℝ) ^ t ≤ Real.exp (-V / 20) := by
   …

   Mentions: OAI.Problem337.RandomProducts.sampleWords