OAI/NumberTheory/EgyptianFractions/PrimeGcdHits.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.prime_gcd_eq_hit_gcd line 9

   Source documentation

   Only prime sample values which divide the modulus contribute to the gcd. The index set, unlike a set of prime values, retains repeated samples.

   theorem prime_gcd_eq_hit_gcd {ι : Type*} (s : Finset ι) (p : ι → ℕ) (u : ℕ)
       (hp : ∀ i ∈ s, Nat.Prime (p i)) :
       Nat.gcd (∏ i ∈ s, p i) u =
         Nat.gcd (∏ i ∈ s with p i ∣ u, p i) u := by
   …

2. theorem OAI.Problem337.prime_gcd_dvd_hit_product line 22
3. theorem OAI.Problem337.prime_gcd_le_hit_product line 29
4. theorem OAI.Problem337.prime_gcd_le_pow_hit_count line 36
5. theorem OAI.Problem337.prime_gcd_le_real_pow_hit_count line 49

   Source documentation

   Real-valued sample bounds are convenient when the sampling interval is specified by a real asymptotic parameter.

   theorem prime_gcd_le_real_pow_hit_count {ι : Type*} (s : Finset ι) (p : ι → ℕ)
       (u : ℕ) (B : ℝ) (hp : ∀ i ∈ s, Nat.Prime (p i))
       (hB : ∀ i ∈ s, (p i : ℝ) ≤ B) :
       (Nat.gcd (∏ i ∈ s, p i) u : ℝ) ≤
         B ^ (s.filter (fun i => p i ∣ u)).card := by
   …

6. theorem OAI.Problem337.hit_count_large_of_gcd_large line 68

   Source documentation

   A large gcd forces many hits, counted with their sample multiplicities.

   theorem hit_count_large_of_gcd_large {ι : Type*} (s : Finset ι) (p : ι → ℕ)
       (u : ℕ) {B x : ℝ} (hp : ∀ i ∈ s, Nat.Prime (p i))
       (hB : ∀ i ∈ s, (p i : ℝ) ≤ B) (hB1 : 1 < B) (hx : 0 < x)
       (hlarge : x < (Nat.gcd (∏ i ∈ s, p i) u : ℝ)) :
       Real.log x / Real.log B < ((s.filter (fun i => p i ∣ u)).card : ℝ) := by
   …