MellinWindowError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform error of smoothing a hard logarithmic window

lemma OAI.JointDickman.logarithmicWindowProfile_bad_card line 11

Source documentation

Only integers in the two transition strips can see a nonconstant profile.

lemma logarithmicWindowProfile_bad_card {η δ x : ℝ}
    (hη : 0 < η) (hηhalf : η < 1/2) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hx : 0 < x) :
    (((Ioc ⌊x⌋₊ ⌊x * Real.exp δ⌋₊).filter fun n : ℕ =>
      logarithmicWindowProfile η hη hηhalf
        ((Real.log x + δ - Real.log (n : ℝ)) / δ) ≠ 1).card : ℝ) ≤
          8 * η * δ * x + 2 := by
…

Mentions: OAI.JointDickman.logarithmicWindowProfile

theorem OAI.JointDickman.logarithmicWindowAverage_mellinPacket_error line 41

Source documentation

The hard window differs from the smooth Mellin packet by an arbitrarily small fixed profile error and the explicit integer endpoint error.

theorem logarithmicWindowAverage_mellinPacket_error (f : ArithmeticFunction ℂ)
    (hf : ∀ n, ‖f n‖ ≤ 1) {K N : ℕ} {η δ x : ℝ}
    (hη : 0 < η) (hηhalf : η < 1/2) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hx : 0 < x)
    (hK : K ≤ ⌊x⌋₊) (hN : ⌊x * Real.exp δ⌋₊ ≤ N) :
    ‖logarithmicWindowAverage f δ (Real.log x) -
      mellinPacket (Ioc K N) f
        (normalizedSchwartzScale (logarithmicWindowProfile η hη hηhalf) δ hδ)
        (Real.log x + δ)‖ ≤ 16 * η + 4 / (δ * x) := by
…

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