ThreePrimeFourierReduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.ThreePrimeFourier.primeFourierSum line 13
Source documentation
The ordinary positive-sign prime exponential sum, at the zero-padded cyclic modulus 3*u+1.
```
def primeFourierSum (u : ℕ) (r : ZMod (3 * u + 1)) : ℂ :=
…
```
def OAI.Problem337.ThreePrimeFourier.primeFourierIntegrand line 18
Source documentation
The cubic integrand extracting the ordered prime triples of sum u.
```
def primeFourierIntegrand (u : ℕ) (r : ZMod (3 * u + 1)) : ℂ :=
…
```
theorem OAI.Problem337.ThreePrimeFourier.weightedSupplyPrimeTriples_eq_fourier line 22
Source documentation
The canonical weighted count is exactly the real inverse Fourier sum.
```
theorem weightedSupplyPrimeTriples_eq_fourier (u : ℕ) :
    weightedSupplyPrimeTriples u =
      (∑ r, primeFourierIntegrand u r).re / (3 * u + 1 : ℕ) := by
…
```
Mentions: OAI.Problem337.weightedSupplyPrimeTriples, OAI.Problem337.ThreePrimeFourier.primeFourierIntegrand

theorem OAI.Problem337.ThreePrimeFourier.quantitativeThreePrimeLowerBound_of_major_minor line 30

Source documentation

The remaining quantitative three-prime assertion follows from explicit major-frequency main terms and minor-frequency errors for the actual prime exponential sums. This theorem does not assert either analytic estimate.

theorem quantitativeThreePrimeLowerBound_of_major_minor
    (major : (u : ℕ) → Finset (ZMod (3 * u + 1)))
    (c : ℝ) (hc : 0 < c)
    (hmajor : ∀ᶠ u : ℕ in atTop, Odd u →
      (2 * c * (u : ℝ) ^ 2) * (3 * u + 1 : ℕ) ≤
        (∑ r ∈ major u, primeFourierIntegrand u r).re)
    (hminor : ∀ᶠ u : ℕ in atTop, Odd u →
      ‖∑ r ∈ (major u)ᶜ, primeFourierIntegrand u r‖ ≤
        (c * (u : ℝ) ^ 2) * (3 * u + 1 : ℕ)) :
    QuantitativeThreePrimeLowerBound := by
…

Mentions: OAI.Problem337.ThreePrimeFourier.primeFourierIntegrand, OAI.Problem337.QuantitativeThreePrimeLowerBound