PrimeProductFibers.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.prime_list_fiber_card_le line 9

Source documentation

Unique factorization bounds any fixed-product family of prime lists by permutations.

lemma prime_list_fiber_card_le (S : Finset (List ℕ)) (s N : ℕ)
    (hlen : ∀ l ∈ S, l.length = s)
    (hprime : ∀ l ∈ S, ∀ p ∈ l, Nat.Prime p)
    (hprod : ∀ l ∈ S, l.prod = N) : S.card ≤ s.factorial := by
…

lemma OAI.Problem337.prime_tuple_fiber_card_le line 27

Source documentation

A fixed product has at most s! ordered prime factorizations of length s.

lemma prime_tuple_fiber_card_le {s : ℕ} (S : Finset (Fin s → ℕ)) (N : ℕ)
    (hprime : ∀ a ∈ S, ∀ i, Nat.Prime (a i))
    (hprod : ∀ a ∈ S, (∏ i, a i) = N) : S.card ≤ s.factorial := by
…

theorem OAI.Problem337.prime_product_fiber_card line 46

Source documentation

The counting version of the prime-product atom bound, allowing repeated prime samples.

theorem prime_product_fiber_card (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (s N : ℕ) :
    (Finset.univ.filter (fun a : Fin s → ↥P => (∏ i, (a i : ℕ)) = N)).card ≤
      s.factorial := by
…

theorem OAI.Problem337.prime_product_mod_fiber_card line 68

Source documentation

Reducing products modulo a modulus larger than all products preserves the atom bound.

theorem prime_product_mod_fiber_card (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p)
    (s q : ℕ) (hsmall : ∀ a : Fin s → ↥P, (∏ i, (a i : ℕ)) < q) (r : ZMod q) :
    (Finset.univ.filter (fun a : Fin s → ↥P => ((∏ i, (a i : ℕ)) : ZMod q) = r)).card ≤
      s.factorial := by
…

def OAI.Problem337.primeProductModMass line 82
Source documentation
The probability mass of one residue for independent uniform prime samples.
```
def primeProductModMass (P : Finset ℕ) (s q : ℕ) (r : ZMod q) : ℝ :=
…
```
lemma OAI.Problem337.primeProductModMass_nonneg line 86
lemma OAI.Problem337.primeProductModMass_le line 91
lemma OAI.Problem337.sum_primeProductModMass line 98
lemma OAI.Problem337.sum_sq_le_atom_bound line 115

theorem OAI.Problem337.prime_product_mod_sum_sq_le line 126

Source documentation

The squared L² norm of a fresh product distribution is at most its factorial atom bound.

theorem prime_product_mod_sum_sq_le (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p)
    (hne : P.Nonempty) (s q : ℕ) [NeZero q]
    (hsmall : ∀ a : Fin s → ↥P, (∏ i, (a i : ℕ)) < q) :
    (∑ r : ZMod q, (primeProductModMass P s q r)^2) ≤
      (s.factorial : ℝ) / (P.card : ℝ)^s := by
…

Mentions: OAI.Problem337.primeProductModMass

lemma OAI.Problem337.factorial_ratio_le_rpow line 135

Source documentation

A convenient scale form of the factorial atom estimate.

lemma factorial_ratio_le_rpow (s : ℕ) (S K P : ℝ) (hS : 1 ≤ S)
    (hs : (s : ℝ) ≤ S) (hP : S^(K-1) ≤ P) :
    (s.factorial : ℝ) / P^s ≤ S^((2-K)*(s : ℝ)) := by
…

theorem OAI.Problem337.prime_product_mod_sum_sq_le_rpow line 160

Source documentation

Scale estimate used for the fresh-product distributions in the random-residue argument.

theorem prime_product_mod_sum_sq_le_rpow (P : Finset ℕ)
    (hP : ∀ p ∈ P, Nat.Prime p) (hne : P.Nonempty) (s q : ℕ) [NeZero q]
    (hsmall : ∀ a : Fin s → ↥P, (∏ i, (a i : ℕ)) < q)
    (S K : ℝ) (hS : 1 ≤ S) (hs : (s : ℝ) ≤ S) (hcard : S^(K-1) ≤ P.card) :
    (∑ r : ZMod q, (primeProductModMass P s q r)^2) ≤ S^((2-K)*(s : ℝ)) :=
…

Mentions: OAI.Problem337.primeProductModMass