English
If hμ1 and μ is powMul, then smoothingFun μ x = μ x for all x when the pow-multiplicative condition holds.
Русский
Если hμ1 и μ обладает powMul, тогда smoothingFun μ x = μ x для всех x при соблюдении условия powMul.
LaTeX
$$smoothingFun μ x = μ x$$
Lean4
/-- If `μ 1 ≤ 1` and `∀ (1 ≤ n), μ (x ^ n) = μ x ^ n`, then `smoothingFun μ x = μ x`. -/
theorem smoothingFun_of_powMul (hμ1 : μ 1 ≤ 1) {x : R} (hx : ∀ (n : ℕ) (_hn : 1 ≤ n), μ (x ^ n) = μ x ^ n) :
smoothingFun μ x = μ x :=
by
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x) tendsto_const_nhds
simp only [EventuallyEq, eventually_atTop, ge_iff_le]
use 1
intro n hn
simp only [smoothingSeminormSeq]
have hn0 : (n : ℝ) ≠ 0 := cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)
rw [hx n hn, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
