tendsto_smoothingFun_of_map_one_le_one

English

If hμ1 holds and ψ is strictly increasing, then the subsequence n ↦ μ(x^{ψ n})^{1/ψ n} converges to smoothingFun μ x.

Русский

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

LaTeX

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

Lean4

/-- If `μ 1 ≤ 1`, then `smoothingFun μ x` is the limit of `smoothingSeminormSeq μ x`
  as `n` tends to infinity. -/
theorem tendsto_smoothingFun_of_map_one_le_one (hμ1 : μ 1 ≤ 1) (x : R) :
    Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x)) :=
  by
  by_cases hx : μ x = 0
  · exact tendsto_smoothingFun_of_eq_zero μ hx
  · exact tendsto_smoothingFun_of_ne_zero μ hμ1 hx

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