Source indexedlemma · leanprover/lean4:v4.32.0

tendsto_rpow_atTop_nhds_zero_of_norm_gt_one

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:352 to 363

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "tendsto-rpow-atTop-nhds-zero-of-norm-gt-one")
  (statement := /-- Let $x>1$. Then $$\lim_{\sigma\to-\infty}x^\sigma=0.$$ -/)
  (proof := /-- Standard. -/)
  (latexEnv := "lemma")]
lemma tendsto_rpow_atTop_nhds_zero_of_norm_gt_one {x : ℝ} (x_gt_one : 1 < x) (C : ℝ) :
    Tendsto (fun (σ : ℝ) ↦ x ^ σ * C) atBot (𝓝 0)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "tendsto-rpow-atTop-nhds-zero-of-norm-gt-one")  (statement := /-- Let $x>1$. Then $$\lim_{\sigma\to-\infty}x^\sigma=0.$$ -/)  (proof := /-- Standard. -/)  (latexEnv := "lemma")]lemma tendsto_rpow_atTop_nhds_zero_of_norm_gt_one {x : ℝ} (x_gt_one : 1 < x) (C : ℝ) :    Tendsto (fun (σ : ℝ) ↦ x ^ σ * C) atBot (𝓝 0) := by  have := (zero_lt_one.trans x_gt_one)  have h := tendsto_rpow_atTop_nhds_zero_of_norm_lt_one (inv_pos.mpr this)    (inv_lt_one_of_one_lt₀ x_gt_one) C  convert (h.comp tendsto_neg_atBot_atTop) using 1  ext; simp only [this.le, inv_rpow, Function.comp_apply, rpow_neg, inv_inv]