isEquivalent_descFactorial — Mathlib

English

The derivative of qaryEntropy q is not continuous at p = 1.

Русский

Производная qaryEntropy q не непрерывна в p = 1.

LaTeX

$$¬ ContinuousAt (deriv (Real.qaryEntropy q)) 1$$

Lean4

/-- `n.descFactorial k` is asymptotically equivalent to `n^k`. -/
theorem isEquivalent_descFactorial (k : ℕ) :
    (fun (n : ℕ) ↦ (n.descFactorial k : ℝ)) ~[atTop] (fun (n : ℕ) ↦ (n ^ k : ℝ)) := by
  induction k with
  | zero => simpa using IsEquivalent.refl
  | succ k h =>
    simp_rw [descFactorial_succ, cast_mul, _root_.pow_succ']
    refine IsEquivalent.mul ?_ h
    have hz : ∀ᶠ (x : ℕ) in atTop, (x : ℝ) ≠ 0 := eventually_atTop.mpr ⟨1, fun n hn ↦ ne_of_gt (mod_cast hn)⟩
    rw [isEquivalent_iff_tendsto_one hz, ← tendsto_add_atTop_iff_nat k]
    simpa using tendsto_natCast_div_add_atTop (k : ℝ)

Похожие утверждения