ThreePrimeLocalFourier.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.threePrimeLocalFactor_eq_cubic line 11
Source documentation
The normalized actual local solution count agrees with the zero frequency plus the normalized cubic nonzero-frequency sum.
```
theorem threePrimeLocalFactor_eq_cubic (p u : ℕ) [Fact p.Prime] :
    (threePrimeLocalFactor p (u : ZMod p) : ℂ) =
      1 + ThreePrimeLocalFactor.cubicPrimeCoefficient p u := by
…
```
Mentions: OAI.Problem337.threePrimeLocalFactor, OAI.Problem337.ThreePrimeLocalFactor.cubicPrimeCoefficient
theorem OAI.Problem337.threePrimeLocalTriples_card_fourier line 20
Source documentation
An unnormalized finite Fourier identity for literal local unit triples. All normalizing constants are checked against the combinatorial count.
```
theorem threePrimeLocalTriples_card_fourier (p u : ℕ) [Fact p.Prime] :
    (p : ℂ) * (threePrimeLocalTriples p (u : ZMod p)).card =
      ((p : ℂ) - 1) ^ 3 *
        (1 + ThreePrimeLocalFactor.cubicPrimeCoefficient p u) := by
…
```
Mentions: OAI.Problem337.threePrimeLocalTriples, OAI.Problem337.ThreePrimeLocalFactor.cubicPrimeCoefficient
theorem OAI.Problem337.threePrimeCubicCoefficient_im line 34
Source documentation
The cubic prime-frequency contribution is real, as follows from its independently counted local-density interpretation.
```
theorem threePrimeCubicCoefficient_im (p u : ℕ) [Fact p.Prime] :
    (ThreePrimeLocalFactor.cubicPrimeCoefficient p u).im = 0 := by
…
```
Mentions: OAI.Problem337.ThreePrimeLocalFactor.cubicPrimeCoefficient