English
If μ(x) = 0, then smoothingSeminormSeq μ x tends to smoothingFun μ x as n → ∞; in particular the infimum is 0.
Русский
Если μ(x) = 0, то smoothingSeminormSeq μ x сходится к smoothingFun μ x при n → ∞; в частности, инфимум равен нулю.
LaTeX
$$$\lim_{n\to\infty} μ(x^n)^{1/n} = smoothingFun μ x$ when μ(x) = 0$$
Lean4
/-- If `μ x = 0`, then `smoothingFun μ x` is the limit of `smoothingSeminormSeq μ x`. -/
theorem tendsto_smoothingFun_of_eq_zero {x : R} (hx : μ x = 0) :
Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x)) :=
by
have h0 (n : ℕ) (hn : 1 ≤ n) : μ (x ^ n) ^ (1 / (n : ℝ)) = 0 :=
by
have hμn : μ (x ^ n) = 0 := by
apply le_antisymm _ (apply_nonneg μ _)
rw [← zero_pow (pos_iff_ne_zero.mp hn), ← hx]
exact map_pow_le_pow _ x (one_le_iff_ne_zero.mp hn)
rw [hμn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]
have hL0 : (iInf fun n : PNat => μ (x ^ (n : ℕ)) ^ (1 / (n : ℝ))) = 0 :=
le_antisymm (ciInf_le_of_le (smoothingSeminormSeq_bddBelow μ x) (1 : PNat) (le_of_eq (h0 1 (le_refl _))))
(le_ciInf fun n => rpow_nonneg (apply_nonneg μ _) _)
simpa only [hL0] using tendsto_atTop_of_eventually_const h0
