HitCount.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.RandomProducts.sampleWords line 11
Source documentation
All words of a fixed length over a finite alphabet.
```
def sampleWords (P : Finset α) (t : ℕ) : Finset (Fin t → α) :=
…
```
def OAI.Problem337.RandomProducts.hitWords line 15
Source documentation
Words having at least k coordinates in the distinguished set.
```
def hitWords (P H : Finset α) (t k : ℕ) : Finset (Fin t → α) :=
…
```
def OAI.Problem337.RandomProducts.hitCylinder line 19
Source documentation
Words required to hit the distinguished set at each specified coordinate.
```
def hitCylinder (P H : Finset α) {t : ℕ} (T : Finset (Fin t)) : Finset (Fin t → α) :=
…
```
theorem OAI.Problem337.RandomProducts.card_hitCylinder line 23
theorem OAI.Problem337.RandomProducts.card_hitWords_le line 36
Source documentation
Elementary union bound over sets of k hit positions.
```
theorem card_hitWords_le (P H : Finset α) (t k : ℕ) :
    (hitWords P H t k).card ≤ t.choose k * H.card ^ k * P.card ^ (t - k) := by
…
```
Mentions: OAI.Problem337.RandomProducts.hitWords

theorem OAI.Problem337.RandomProducts.hit_probability_le line 69

Source documentation

Normalized finite counting bound for independent uniform samples.

theorem hit_probability_le (P H : Finset α) (t k : ℕ) (hP : P.Nonempty) :
    ((hitWords P H t k).card : ℝ) / (P.card : ℝ) ^ t ≤
      ((t : ℝ) * (H.card : ℝ) / (P.card : ℝ)) ^ k := by
…

Mentions: OAI.Problem337.RandomProducts.hitWords

theorem OAI.Problem337.RandomProducts.gcd_prod_dvd_hit_prod line 99
Source documentation
Prime factors not dividing the modulus do not contribute to the common divisor. The indexing retains multiplicities, as required for sampling with replacement.
```
theorem gcd_prod_dvd_hit_prod (s : Finset α) (p : α → ℕ) (u : ℕ)
    (hprime : ∀ i ∈ s, Nat.Prime (p i)) :
    Nat.gcd u (∏ i ∈ s, p i) ∣ ∏ i ∈ s, if p i ∣ u then p i else 1 := by
…
```

theorem OAI.Problem337.RandomProducts.gcd_prod_le_pow_hit_count line 119

Source documentation

A common-divisor bound in terms of the number of hit samples.

theorem gcd_prod_le_pow_hit_count (s : Finset α) (p : α → ℕ) (u B : ℕ)
    (hprime : ∀ i ∈ s, Nat.Prime (p i)) (hB : ∀ i ∈ s, p i ≤ B) :
    Nat.gcd u (∏ i ∈ s, p i) ≤ B ^ (s.filter (fun i => p i ∣ u)).card := by
…

theorem OAI.Problem337.RandomProducts.gcd_probability_le line 141

Source documentation

Uniform sampling estimate for a large gcd of a product of sampled primes. This is the combinatorial part of the random-gcd exceptional-event bound.

theorem gcd_probability_le (P : Finset ℕ) (t k u B : ℕ)
    (hP : P.Nonempty) (hprime : ∀ p ∈ P, Nat.Prime p)
    (hB : ∀ p ∈ P, p ≤ B) (hBone : 1 ≤ B) :
    (((sampleWords P t).filter (fun f =>
      B ^ (k - 1) < Nat.gcd u (∏ i, f i))).card : ℝ) / (P.card : ℝ) ^ t ≤
      ((t : ℝ) * ((P.filter (fun p => p ∣ u)).card : ℝ) / (P.card : ℝ)) ^ k := by
…

Mentions: OAI.Problem337.RandomProducts.sampleWords

theorem OAI.Problem337.RandomProducts.hit_probability_le_exp line 175

Source documentation

The numerical parameter choice for the exceptional gcd event in the random-products argument. The threshold hypothesis is the denominator-cleared form of k ≥ 0.08 * V / (101 * log S).

theorem hit_probability_le_exp (P H : Finset α) (t k : ℕ) (S V : ℝ)
    (hP : P.Nonempty) (hS : 1 < S) (hV : 0 ≤ V)
    (ht : (t : ℝ) ≤ S) (hH : (H.card : ℝ) ≤ S)
    (hsize : S ^ 99 ≤ (P.card : ℝ))
    (hk : 8 * V ≤ 10100 * (k : ℝ) * Real.log S) :
    ((hitWords P H t k).card : ℝ) / (P.card : ℝ) ^ t ≤ Real.exp (-V / 20) := by
…

Mentions: OAI.Problem337.RandomProducts.hitWords