PrimeProductMultiplicity.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.primeProductFiber line 9
Source documentation
The ordered prime tuples of length k whose product is N.
```
def primeProductFiber (k N : ℕ) : Set (Fin k → ℕ) :=
…
```
theorem OAI.Problem337.prime_tuple_perm_factors line 12
theorem OAI.Problem337.primeProductFiber_finite line 21
theorem OAI.Problem337.primeProductFiber_ncard_le line 30
Source documentation
Unique factorization bounds each atom of an ordered prime product by k!.
```
theorem primeProductFiber_ncard_le (k N : ℕ) :
    (primeProductFiber k N).ncard ≤ k.factorial := by
…
```
Mentions: OAI.Problem337.primeProductFiber

theorem OAI.Problem337.prime_sample_product_count line 49

Source documentation

Restricting each coordinate to a finite prime sampling set preserves the atom bound.

theorem prime_sample_product_count (S : Finset ℕ)
    (hS : ∀ p ∈ S, Nat.Prime p) (k N : ℕ) :
    (Finset.univ.filter (fun p : Fin k → S => ∏ i, (p i : ℕ) = N)).card ≤
      k.factorial := by
…

theorem OAI.Problem337.prime_sample_product_atom line 70

Source documentation

The corresponding normalized counting measure bound.

theorem prime_sample_product_atom (S : Finset ℕ)
    (hS : ∀ p ∈ S, Nat.Prime p) (k N : ℕ) :
    ((Finset.univ.filter (fun p : Fin k → S => ∏ i, (p i : ℕ) = N)).card : ℝ) /
        (S.card : ℝ) ^ k ≤ (k.factorial : ℝ) / (S.card : ℝ) ^ k := by
…

theorem OAI.Problem337.prime_sample_residue_count line 78

Source documentation

Reduction modulo a modulus exceeding all attainable products does not merge atoms.

theorem prime_sample_residue_count (S : Finset ℕ)
    (hS : ∀ p ∈ S, Nat.Prime p) (k q a : ℕ)
    (hshort : ∀ p : Fin k → S, ∏ i, (p i : ℕ) < q) :
    (Finset.univ.filter (fun p : Fin k → S => (∏ i, (p i : ℕ)) % q = a)).card ≤
      k.factorial := by
…