Source indexedlemma · leanprover/lean4:v4.32.0

limitOfConstant

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:293 to 311

Source documentation

TODO : Move to general section

Exact Lean statement

@[blueprint
  (title := "limitOfConstant")
  (statement := /--
  Let $a:\R\to\C$ be a function, and let $\sigma>0$ be a real number. Suppose that, for all
  $\sigma, \sigma'>0$, we have $a(\sigma')=a(\sigma)$, and that
  $\lim_{\sigma\to\infty}a(\sigma)=0$. Then $a(\sigma)=0$.
  -/)
  (latexEnv := "lemma")]
lemma limitOfConstant {a : ℝ → ℂ} {σ : ℝ} (σpos : 0 < σ)
    (ha : ∀ (σ' : ℝ) (σ'' : ℝ) (_ : 0 < σ') (_ : 0 < σ''), a σ' = a σ'')
    (ha' : Tendsto a atTop (𝓝 0)) : a σ = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "limitOfConstant")  (statement := /--  Let $a:\R\to\C$ be a function, and let $\sigma>0$ be a real number. Suppose that, for all  $\sigma, \sigma'>0$, we have $a(\sigma')=a(\sigma)$, and that  $\lim_{\sigma\to\infty}a(\sigma)=0$. Then $a(\sigma)=0$.  -/)  (latexEnv := "lemma")]lemma limitOfConstant {a : ℝ → ℂ} {σ : ℝ} (σpos : 0 < σ)    (ha : ∀ (σ' : ℝ) (σ'' : ℝ) (_ : 0 < σ') (_ : 0 < σ''), a σ' = a σ'')    (ha' : Tendsto a atTop (𝓝 0)) : a σ = 0 := by  /--  \begin{align*}  \lim_{\sigma'\to\infty}a(\sigma) &= \lim_{\sigma'\to\infty}a(\sigma') \\  &= 0  \end{align*}  -/  have := eventuallyEq_of_mem (mem_atTop σ) fun σ' h ↦ ha σ' σ (σpos.trans_le h) σpos  exact tendsto_const_nhds_iff.mp (ha'.congr' this)