Source indexedlemma · leanprover/lean4:v4.32.0

limitOfConstantLeft

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:315 to 333

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "limitOfConstantLeft")
  (statement := /--
  Let $a:\R\to\C$ be a function, and let $\sigma<-3/2$ 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 limitOfConstantLeft {a : ℝ → ℂ} {σ : ℝ} (σlt : σ ≤ -3 / 2)
    (ha : ∀ (σ' : ℝ) (σ'' : ℝ) (_ : σ' ≤ -3 / 2) (_ : σ'' ≤ -3 / 2), a σ' = a σ'')
    (ha' : Tendsto a atBot (𝓝 0)) : a σ = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "limitOfConstantLeft")  (statement := /--  Let $a:\R\to\C$ be a function, and let $\sigma<-3/2$ 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 limitOfConstantLeft {a : ℝ → ℂ} {σ : ℝ} (σlt : σ ≤ -3 / 2)    (ha : ∀ (σ' : ℝ) (σ'' : ℝ) (_ : σ' ≤ -3 / 2) (_ : σ'' ≤ -3 / 2), a σ' = a σ'')    (ha' : Tendsto a atBot (𝓝 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_atBot (-3/2)) fun σ' h ↦ ha σ' σ h σlt  exact tendsto_const_nhds_iff.mp (ha'.congr' this)