Theorem: tendsto_rpow_atTop_nhds_zero_of_norm_gt_one (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x : ℝ
x_gt_one : 1 < x
C : ℝ
⊢ Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
Tactic:
have := (zero_lt_one.trans x_gt_one)
State after:
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
⊢ Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)

State before:
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
⊢ Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
Tactic:
have h := tendsto_rpow_atTop_nhds_zero_of_norm_lt_one (inv_pos.mpr this) (inv_lt_one x_gt_one) C
State after:
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
⊢ Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)

State before:
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
⊢ Tendsto (fun σ => x ^ σ * C) atBot (𝓝 0)
Tactic:
convert (h.comp tendsto_neg_atBot_atTop) using 1
State after:
case h.e'_3
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
⊢ (fun σ => x ^ σ * C) = (fun σ => x⁻¹ ^ σ * C) ∘ Neg.neg

State before:
case h.e'_3
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
⊢ (fun σ => x ^ σ * C) = (fun σ => x⁻¹ ^ σ * C) ∘ Neg.neg
Tactic:
ext
State after:
case h.e'_3.h
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
x✝ : ℝ
⊢ x ^ x✝ * C = ((fun σ => x⁻¹ ^ σ * C) ∘ Neg.neg) x✝

State before:
case h.e'_3.h
x : ℝ
x_gt_one : 1 < x
C : ℝ
this : 0 < x
h : Tendsto (fun σ => x⁻¹ ^ σ * C) atTop (𝓝 0)
x✝ : ℝ
⊢ x ^ x✝ * C = ((fun σ => x⁻¹ ^ σ * C) ∘ Neg.neg) x✝
Tactic:
simp only [this.le, inv_rpow, Function.comp_apply, rpow_neg, inv_inv]
State after:
no goals