TruncatedMellin.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual truncated Mellin integral

The Fourier approximation to the dyadic indicator is inserted into a finite arithmetic polynomial. The height is 2πξ, in accordance with Mathlib's Fourier convention. The multiplier vanishes for |ξ| ≥ T.

def OAI.CubicFirstMoment.dyadicFourierMultiplier line 21
def OAI.CubicFirstMoment.truncatedMellinWeight line 24
lemma OAI.CubicFirstMoment.continuous_dyadicFourierMultiplier line 28
lemma OAI.CubicFirstMoment.continuous_truncatedMellinWeight line 32
lemma OAI.CubicFirstMoment.truncatedMellinWeight_zero line 37
lemma OAI.CubicFirstMoment.truncatedMellinWeight_compact line 45
lemma OAI.CubicFirstMoment.integrable_truncatedMellinWeight_twist line 55
lemma OAI.CubicFirstMoment.smoothLogInterval_eq_mellin line 62
theorem OAI.CubicFirstMoment.smoothed_polynomial_eq_mellin line 82
Source documentation
An exact integral representation, using the same cutoff for every coefficient. Hence the height shifts are common across character rows.
```
theorem smoothed_polynomial_eq_mellin (N : Finset Eisenstein) (v : Eisenstein → ℂ)
    {X T : ℝ} (hX : 0 < X) (hT : 0 < T) (hN : ∀ n ∈ N, n ≠ 0) :
    (∑ n ∈ N, v n * smoothLogInterval T (norm n/X)) =
      ∫ ξ : ℝ, truncatedMellinWeight X T ξ *
        (∑ n ∈ N, v n * normTwist (2*Real.pi*ξ) n) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.smoothLogInterval, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.truncatedMellinWeight, OAI.CubicFirstMoment.normTwist