ThreePrimeIntegralCount.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.ThreePrimeContinuousFourier.primeFrequencies line 11
Source documentation
Positive prime frequencies up to the integer under representation.
```
def primeFrequencies (u : ℕ) : Finset ℕ := (Finset.Icc 1 u).filter Nat.Prime
```
def OAI.Problem337.ThreePrimeContinuousFourier.primePhaseSum line 14
Source documentation
The unweighted positive-sign prime exponential sum.
```
def primePhaseSum (u : ℕ) (x : ℝ) : ℂ :=
…
```
lemma OAI.Problem337.ThreePrimeContinuousFourier.prime_triples_eq_filter line 17
theorem OAI.Problem337.ThreePrimeContinuousFourier.prime_triple_integral line 27
Source documentation
The exact prime-triple count is a continuous cubic Fourier coefficient. This does not estimate the integral or assert a prime-distribution result.
```
theorem prime_triple_integral (u : ℕ) :
    (∫ x in (0 : ℝ)..1, primePhaseSum u x ^ 3 * phase (-(u : ℤ)) x) =
      ((supplyPrimeTriples u).card : ℂ) := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousFourier.primePhaseSum, OAI.Problem337.ThreePrimeContinuousFourier.phase, OAI.Problem337.supplyPrimeTriples