OAI/NumberTheory/EgyptianFractions/RandomProductFourier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.sum_fiber_card_mul line 11

   Source documentation

   Regroup a finite sum by the fibers of a map, with explicit fiber cardinalities.

   lemma sum_fiber_card_mul {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq κ]
       (f : ι → κ) (g : κ → ℂ) :
       (∑ r : κ, ((Finset.univ.filter (fun a : ι => f a = r)).card : ℂ) * g r) =
         ∑ a : ι, g (f a) := by
   …

2. lemma OAI.Problem337.primeProductModMass_average line 30

   Source documentation

   The mass function of a prime product is the pushforward of uniform counting.

   lemma primeProductModMass_average (P : Finset ℕ) (s q : ℕ) [NeZero q]
       (g : ZMod q → ℂ) :
       (∑ r : ZMod q, (primeProductModMass P s q r : ℂ) * g r) =
         (∑ a : Fin s → ↥P, g ((∏ i, (a i : ℕ)) : ZMod q)) / (P.card : ℂ)^s := by
   …

   Mentions: OAI.Problem337.primeProductModMass

3. lemma OAI.Problem337.primeProductModMass_double_average line 39

   Source documentation

   Two independent prime products correspond to the product of their residue masses.

   lemma primeProductModMass_double_average (P : Finset ℕ) (s q : ℕ) [NeZero q]
       (g : ZMod q → ZMod q → ℂ) :
       (∑ x : ZMod q, ∑ y : ZMod q,
         (primeProductModMass P s q x : ℂ) *
           (primeProductModMass P s q y : ℂ) * g x y) =
         (∑ a : Fin s → ↥P, ∑ b : Fin s → ↥P,
           g ((∏ i, (a i : ℕ)) : ZMod q) ((∏ i, (b i : ℕ)) : ZMod q)) /
             ((P.card : ℂ)^s)^2 := by
   …

   Mentions: OAI.Problem337.primeProductModMass

4. theorem OAI.Problem337.prime_product_bilinear_average_bound line 55

   Source documentation

   Exponential cancellation for two independent uniform prime products whenever all attainable integer products are smaller than the modulus. Repetitions among sampled primes are permitted.

   theorem prime_product_bilinear_average_bound
       (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (hne : P.Nonempty)
       (s q : ℕ) [NeZero q]
       (hsmall : ∀ a : Fin s → ↥P, (∏ i, (a i : ℕ)) < q)
       (c : (ZMod q)ˣ) :
       ‖(∑ a : Fin s → ↥P, ∑ b : Fin s → ↥P,
         ZMod.stdAddChar ((c : ZMod q) * ((∏ i, (a i : ℕ)) : ZMod q) *
           ((∏ i, (b i : ℕ)) : ZMod q))) / ((P.card : ℂ)^s)^2‖ ≤
         Real.sqrt (q : ℝ) * ((s.factorial : ℝ) / (P.card : ℝ)^s) := by
   …