MellinWindowSupport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The support and central plateau of the logarithmic smoothing kernel

lemma OAI.JointDickman.logarithmicWindowProfile_zero_of_outside line 11
lemma OAI.JointDickman.logarithmicWindowProfile_one_of_inside line 27

theorem OAI.JointDickman.mellinPacket_logarithmicWindow_support line 44

Source documentation

Enlarging the finite Dirichlet polynomial adds only zero kernel terms.

theorem mellinPacket_logarithmicWindow_support (f : ℕ → ℂ) {K N : ℕ} {η δ x : ℝ}
    (hη : 0 < η) (hηhalf : η < 1/2) (hδ : 0 < δ) (hx : 0 < x)
    (hK : K ≤ ⌊x⌋₊) (hN : ⌊x * Real.exp δ⌋₊ ≤ N) :
    mellinPacket (Ioc K N) f
      (normalizedSchwartzScale (logarithmicWindowProfile η hη hηhalf) δ hδ)
      (Real.log x + δ) =
    (∑ n ∈ Ioc ⌊x⌋₊ ⌊x * Real.exp δ⌋₊,
      (f n / (n : ℂ)) * logarithmicWindowProfile η hη hηhalf
        ((Real.log x + δ - Real.log (n : ℝ)) / δ)) / (δ : ℂ) := by
…

Mentions: OAI.JointDickman.mellinPacket, OAI.JointDickman.normalizedSchwartzScale, OAI.JointDickman.logarithmicWindowProfile