SharpHeightIntegral.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The concrete sharp-cutoff smoothing in the manuscript's height variable. The Fourier convention contributes the explicit Jacobian 1 / (2π). All finite sums below retain their original coefficients and support.

def OAI.CubicFirstMoment.cutoffHeightMultiplier line 15
lemma OAI.CubicFirstMoment.cutoffHeightMultiplier_integrable line 19
lemma OAI.CubicFirstMoment.cutoffHeightMultiplier_zero line 27
lemma OAI.CubicFirstMoment.smoothLogInterval_eq_height line 36

theorem OAI.CubicFirstMoment.finite_smooth_interval_height line 62

Source documentation

The smoothed finite arithmetic sum is the actual norm-twisted polynomial integrated against the compact height multiplier.

theorem finite_smooth_interval_height (P : Finset Eisenstein) (c : Eisenstein → ℂ)
    {X T : ℝ} (hX : 0 < X) (hT : 0 < T)
    (hP : ∀ p ∈ P, p ≠ 0) :
    (∑ p ∈ P, c p*smoothLogInterval T (norm p/X)) =
      ((2*Real.pi : ℝ) : ℂ)⁻¹ * ∫ t : ℝ,
        (cutoffHeightMultiplier T t * Complex.exp ((-Real.log X*t : ℝ)*Complex.I)) *
          ∑ p ∈ P, c p*normTwist t p := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.smoothLogInterval, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cutoffHeightMultiplier, OAI.CubicFirstMoment.normTwist

theorem OAI.CubicFirstMoment.prime_sharp_interval_height line 85

Source documentation

Exact sharp prime interval decomposition, with the endpoint error bound and no assumption about the prime sum itself.

theorem prime_sharp_interval_height (P : Finset Eisenstein)
    (hP : ∀ p ∈ P, primaryPrime p) (c : Eisenstein → ℂ)
    {X T : ℝ} (hX : 0 < X) (hT : 0 < T) :
    (∑ p ∈ P, c p*(intervalStep X (2*X) (norm p) : ℂ)) =
      ((2*Real.pi : ℝ) : ℂ)⁻¹ * (∫ t : ℝ,
        (cutoffHeightMultiplier T t * Complex.exp ((-Real.log X*t : ℝ)*Complex.I)) *
          ∑ p ∈ P, c p*normTwist t p) +
      ∑ p ∈ P, c p*sharpIntervalError X T (norm p) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.intervalStep, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cutoffHeightMultiplier, OAI.CubicFirstMoment.normTwist, OAI.CubicFirstMoment.sharpIntervalError