OAI/NumberTheory/EgyptianFractions/ThreePrimeFourier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.ThreePrimeFourier.weighted_triple_character_identity line 11

   Source documentation

   Exact Fourier extraction of a weighted ordered triple in a finite cyclic group. No primality or analytic estimate is needed.

   theorem weighted_triple_character_identity {q : ℕ} [NeZero q]
       {α : Type*} (s : Finset α) (f : α → ZMod q) (w : α → ℂ)
       (u : ZMod q) :
       (∑ r : ZMod q, (∑ a ∈ s, w a * ZMod.stdAddChar (f a * r)) ^ 3 *
         ZMod.stdAddChar (-u * r)) =
       (q : ℂ) * ∑ a ∈ s, ∑ b ∈ s, ∑ c ∈ s,
         if f a + f b + f c = u then w a * w b * w c else 0 := by
   …

2. theorem OAI.Problem337.ThreePrimeFourier.weighted_natural_triple_character_identity line 66

   Source documentation

   Choosing the cyclic modulus above every possible sum removes all modular aliasing. The resulting identity counts ordinary natural-number sums exactly.

   theorem weighted_natural_triple_character_identity {q : ℕ} [NeZero q]
       (s : Finset ℕ) (w : ℕ → ℂ) (u : ℕ)
       (hs : ∀ a ∈ s, a ≤ u) (hq : 3 * u < q) :
       (∑ r : ZMod q, (∑ a ∈ s, w a * ZMod.stdAddChar ((a : ZMod q) * r)) ^ 3 *
         ZMod.stdAddChar (-(u : ZMod q) * r)) =
       (q : ℂ) * ∑ a ∈ s, ∑ b ∈ s, ∑ c ∈ s,
         if a + b + c = u then w a * w b * w c else 0 := by
   …

3. theorem OAI.Problem337.ThreePrimeFourier.weighted_natural_triple_fourier line 95

   Source documentation

   Normalized inverse Fourier extraction for weighted ordinary triples.

   theorem weighted_natural_triple_fourier {q : ℕ} [NeZero q]
       (s : Finset ℕ) (w : ℕ → ℂ) (u : ℕ)
       (hs : ∀ a ∈ s, a ≤ u) (hq : 3 * u < q) :
       (∑ a ∈ s, ∑ b ∈ s, ∑ c ∈ s,
         if a + b + c = u then w a * w b * w c else 0) =
       (∑ r : ZMod q, (∑ a ∈ s, w a * ZMod.stdAddChar ((a : ZMod q) * r)) ^ 3 *
         ZMod.stdAddChar (-(u : ZMod q) * r)) / (q : ℂ) := by
   …

4. theorem OAI.Problem337.ThreePrimeFourier.supply_prime_triple_sum_eq_nested line 108

   Source documentation

   The existing ordered-prime-triple finset is exactly the filtered cube of the primes at most u. This identity also applies to arbitrary weights.

   theorem supply_prime_triple_sum_eq_nested (u : ℕ) (w : ℕ → ℂ) :
       (∑ t ∈ supplyPrimeTriples u, w t.1 * w t.2.1 * w t.2.2) =
       ∑ a ∈ (Finset.Icc 1 u).filter Nat.Prime,
         ∑ b ∈ (Finset.Icc 1 u).filter Nat.Prime,
           ∑ c ∈ (Finset.Icc 1 u).filter Nat.Prime,
             if a + b + c = u then w a * w b * w c else 0 := by
   …

   Mentions: OAI.Problem337.supplyPrimeTriples

5. theorem OAI.Problem337.ThreePrimeFourier.supply_prime_weighted_fourier line 127

   Source documentation

   Exact extraction of the log-weighted prime count that occurs in the three-prime lower bound. The modulus condition excludes all circular sums.

   theorem supply_prime_weighted_fourier {q : ℕ} [NeZero q]
       (u : ℕ) (hq : 3 * u < q) :
       (∑ t ∈ supplyPrimeTriples u,
         (Real.log (t.1 : ℝ) : ℂ) * (Real.log (t.2.1 : ℝ) : ℂ) *
           (Real.log (t.2.2 : ℝ) : ℂ)) =
       (∑ r : ZMod q,
         (∑ a ∈ (Finset.Icc 1 u).filter Nat.Prime,
           (Real.log (a : ℝ) : ℂ) * ZMod.stdAddChar ((a : ZMod q) * r)) ^ 3 *
             ZMod.stdAddChar (-(u : ZMod q) * r)) / (q : ℂ) := by
   …

   Mentions: OAI.Problem337.supplyPrimeTriples

6. theorem OAI.Problem337.ThreePrimeFourier.supply_prime_weighted_fourier_re line 142

   Source documentation

   Real-part version of the exact extraction formula.

   theorem supply_prime_weighted_fourier_re {q : ℕ} [NeZero q]
       (u : ℕ) (hq : 3 * u < q) :
       (∑ t ∈ supplyPrimeTriples u,
         Real.log (t.1 : ℝ) * Real.log (t.2.1 : ℝ) * Real.log (t.2.2 : ℝ)) =
       (∑ r : ZMod q,
         (∑ a ∈ (Finset.Icc 1 u).filter Nat.Prime,
           (Real.log (a : ℝ) : ℂ) * ZMod.stdAddChar ((a : ZMod q) * r)) ^ 3 *
             ZMod.stdAddChar (-(u : ZMod q) * r)).re / (q : ℝ) := by
   …

   Mentions: OAI.Problem337.supplyPrimeTriples

7. theorem OAI.Problem337.ThreePrimeFourier.major_minor_real_lower_bound line 156

   Source documentation

   Splitting frequencies into an arbitrary major set and its complement gives the standard lower bound by the major real part minus the minor norm.

   theorem major_minor_real_lower_bound {α : Type*} [Fintype α] [DecidableEq α]
       (s : Finset α) (F : α → ℂ) (Q : ℝ) (hQ : 0 < Q) :
       ((∑ r ∈ s, F r).re - ‖∑ r ∈ sᶜ, F r‖) / Q ≤
         (∑ r, F r).re / Q := by
   …

   Mentions: OAI.Problem337.F

8. theorem OAI.Problem337.ThreePrimeFourier.supply_prime_weighted_lower_of_major_minor line 170

   Source documentation

   A lower major-frequency bound and an upper minor-frequency norm bound imply a lower bound for the actual log-weighted ordered-prime-triple count. The genuinely analytic estimates remain explicit hypotheses.

   theorem supply_prime_weighted_lower_of_major_minor {q : ℕ} [NeZero q]
       (u : ℕ) (hq : 3 * u < q) (major : Finset (ZMod q))
       (A E : ℝ)
       (hmajor : A * (q : ℝ) ≤
         (∑ r ∈ major,
           (∑ a ∈ (Finset.Icc 1 u).filter Nat.Prime,
             (Real.log (a : ℝ) : ℂ) * ZMod.stdAddChar ((a : ZMod q) * r)) ^ 3 *
               ZMod.stdAddChar (-(u : ZMod q) * r)).re)
       (hminor : ‖∑ r ∈ majorᶜ,
           (∑ a ∈ (Finset.Icc 1 u).filter Nat.Prime,
             (Real.log (a : ℝ) : ℂ) * ZMod.stdAddChar ((a : ZMod q) * r)) ^ 3 *
               ZMod.stdAddChar (-(u : ZMod q) * r)‖ ≤ E * (q : ℝ)) :
   …