PrimeHits.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.gcd_prod_dvd_prod_gcd line 9

Source documentation

A gcd of a product divides the product of the individual gcds.

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

theorem OAI.Problem337.gcd_prime_product_dvd_hits line 24

Source documentation

Only prime samples that divide the modulus contribute to its gcd with the sampled product, even when sampled values repeat.

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

theorem OAI.Problem337.gcd_prime_product_le_pow_hits line 40

Source documentation

Bounded sampled primes give a power bound in the number of hits.

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

theorem OAI.Problem337.gcd_frequency_prime_product_le line 54

Source documentation

The extra frequency factor costs at most its full size.

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

theorem OAI.Problem337.prime_divisor_population_pow_le line 71
Source documentation
A set of distinct prime divisors, all at least L, has size bounded by the logarithm of the modulus. This bounds the population of hit values.
```
theorem prime_divisor_population_pow_le (P : Finset ℕ) (u L : ℕ)
    (hu : 0 < u) (hp : ∀ p ∈ P, p.Prime) (hL : ∀ p ∈ P, L ≤ p) :
    L ^ (P.filter (fun p => p ∣ u)).card ≤ u := by
…
```

theorem OAI.Problem337.prime_divisor_population_log_le line 89

Source documentation

Real logarithmic version of the prime hit population estimate.

theorem prime_divisor_population_log_le (P : Finset ℕ) (u L : ℕ)
    (hu : 0 < u) (hL1 : 1 < L)
    (hp : ∀ p ∈ P, p.Prime) (hL : ∀ p ∈ P, L ≤ p) :
    ((P.filter (fun p => p ∣ u)).card : ℝ) ≤
      Real.log (u : ℝ) / Real.log (L : ℝ) := by
…