ThreePrimeMangoldtIntegral.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.ThreePrimeContinuousFourier.mangoldtPhaseSum line 11
Source documentation
The actual positive-frequency Mangoldt polynomial on the unit circle.
```
def mangoldtPhaseSum (u : ℕ) (x : ℝ) : ℂ :=
…
```
lemma OAI.Problem337.ThreePrimeContinuousFourier.mangoldtPhaseSum_exp line 14
lemma OAI.Problem337.ThreePrimeContinuousFourier.mangoldtPhaseSum_continuous line 20
theorem OAI.Problem337.ThreePrimeContinuousFourier.mangoldt_triple_integral line 26
Source documentation
Exact continuous cubic extraction for the canonical positive-integer Mangoldt convolution. In particular no prime-distribution estimate is used.
```
theorem mangoldt_triple_integral (u : ℕ) :
    (∫ x in (0 : ℝ)..1, mangoldtPhaseSum u x ^ 3 * phase (-(u : ℤ)) x) =
      (mangoldtTripleSum u : ℂ) := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousFourier.mangoldtPhaseSum, OAI.Problem337.ThreePrimeContinuousFourier.phase, OAI.Problem337.mangoldtTripleSum
theorem OAI.Problem337.ThreePrimeContinuousFourier.mangoldt_cubic_intervalIntegrable line 49
Source documentation
The integral is a genuine integrable complex expression, not an appeal to the default value of the Bochner integral on a nonintegrable function.
```
theorem mangoldt_cubic_intervalIntegrable (u : ℕ) (a b : ℝ) :
    IntervalIntegrable
      (fun x => mangoldtPhaseSum u x ^ 3 * phase (-(u : ℤ)) x) MeasureTheory.volume a b := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousFourier.mangoldtPhaseSum, OAI.Problem337.ThreePrimeContinuousFourier.phase
theorem OAI.Problem337.ThreePrimeContinuousFourier.re_mangoldt_triple_integral line 56
Source documentation
Taking real parts recovers exactly the real arithmetic convolution.
```
theorem re_mangoldt_triple_integral (u : ℕ) :
    (∫ x in (0 : ℝ)..1, mangoldtPhaseSum u x ^ 3 * phase (-(u : ℤ)) x).re =
      mangoldtTripleSum u := by
…
```
Mentions: OAI.Problem337.ThreePrimeContinuousFourier.mangoldtPhaseSum, OAI.Problem337.ThreePrimeContinuousFourier.phase, OAI.Problem337.mangoldtTripleSum