Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.tendsto_boundary_sine_terms

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2489 to 2507

Mathematical statement

Exact Lean statement

lemma tendsto_boundary_sine_terms {a b : ℝ} (ha0 : 0 ≤ a) (hb0 : 0 ≤ b)
    (ha : ¬ ∃ k : ℤ, a = k) (hb : ¬ ∃ k : ℤ, b = k) (s : ℂ) :
    Tendsto
      (fun N : ℕ ↦
        (b : ℂ) ^ (-s) *
            ((∑ n ∈ range N,
              Real.sin (2 * Real.pi * (n + 1) * b) /
                (Real.pi * (n + 1 : ℝ))) : ℂ) -
          (a : ℂ) ^ (-s) *
            ((∑ n ∈ range N,
              Real.sin (2 * Real.pi * (n + 1) * a) /
                (Real.pi * (n + 1 : ℝ))) : ℂ))
      atTop (𝓝 ((a : ℂ) ^ (-s) * B1 a - (b : ℂ) ^ (-s) * B1 b))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tendsto_boundary_sine_terms {a b : ℝ} (ha0 : 0 ≤ a) (hb0 : 0 ≤ b)    (ha : ¬ ∃ k : ℤ, a = k) (hb : ¬ ∃ k : ℤ, b = k) (s : ℂ) :    Tendsto      (fun N : ℕ ↦        (b : ℂ) ^ (-s) *            ((∑ n ∈ range N,              Real.sin (2 * Real.pi * (n + 1) * b) /                (Real.pi * (n + 1 : ℝ))) : ℂ) -          (a : ℂ) ^ (-s) *            ((∑ n ∈ range N,              Real.sin (2 * Real.pi * (n + 1) * a) /                (Real.pi * (n + 1 : ℝ))) : ℂ))      atTop (𝓝 ((a : ℂ) ^ (-s) * B1 a - (b : ℂ) ^ (-s) * B1 b)) := by  have hb_tendsto :=    (tendsto_sine_over_pi_series_neg_B1 hb0 hb).ofReal.const_mul ((b : ℂ) ^ (-s))  have ha_tendsto :=    (tendsto_sine_over_pi_series_neg_B1 ha0 ha).ofReal.const_mul ((a : ℂ) ^ (-s))  simpa [Complex.ofReal_neg, sub_eq_add_neg, add_comm, add_left_comm, add_assoc,    mul_comm, mul_left_comm, mul_assoc] using hb_tendsto.sub ha_tendsto