tendsto_smoothingFun_comp — Mathlib

English

If hμ1 and ψ is increasing, then the sequence μ(x^{ψ n})^{1/ψ n} tends to smoothingFun x, i.e., Tendsto of the composed map to smoothingFun.

Русский

Если hμ1 и ψ возрастает, то последовательность μ(x^{ψ n})^{1/ψ n} сходится к smoothingFun x.

LaTeX

$$$\lim_{n\to\infty} μ(x^{\psi(n)})^{1/\psi(n)} = smoothingFun μ x$$$

Lean4

theorem tendsto_smoothingFun_comp (hμ1 : μ 1 ≤ 1) (x : R) {ψ : ℕ → ℕ} (hψ_mono : StrictMono ψ) :
    Tendsto (fun n : ℕ => μ (x ^ ψ n) ^ (1 / ψ n : ℝ)) atTop (𝓝 (smoothingFun μ x)) :=
  have hψ_lim' : Tendsto ψ atTop atTop := StrictMono.tendsto_atTop hψ_mono
  (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x).comp hψ_lim'

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