English
The smoothingFun μ is power-multiplicative: for any x, m, hm, smoothingFun μ x^m ^ m = smoothingFun μ x ^ m under the given conditions.
Русский
Сглаженная функция μ является степенно-производной по отношению к умножению: smoothingFun μ x^m ^{m} = smoothingFun μ x^{m}.
LaTeX
$$IsPowMul (smoothingFun μ)$$
Lean4
/-- If `μ 1 ≤ 1` and `μ` is nonarchimedean, then `smoothingFun μ` is
power-multiplicative. -/
theorem isPowMul_smoothingFun (hμ1 : μ 1 ≤ 1) : IsPowMul (smoothingFun μ) :=
by
intro x m hm
have hlim : Tendsto (fun n => smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x)) :=
Tendsto.comp (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)
(tendsto_atTop_atTop_of_monotone (fun n k hnk ↦ mul_le_mul_left' hnk m) (fun n ↦ ⟨n, le_mul_of_one_le_left' hm⟩))
apply tendsto_nhds_unique _ (Tendsto.pow hlim m)
have h_eq (n : ℕ) : smoothingSeminormSeq μ x (m * n) ^ m = smoothingSeminormSeq μ (x ^ m) n :=
by
have hm' : (m : ℝ) ≠ 0 := cast_ne_zero.mpr (_root_.ne_of_gt (lt_of_lt_of_le zero_lt_one hm))
simp only [smoothingSeminormSeq]
rw [pow_mul, ← rpow_natCast, ← rpow_mul (apply_nonneg μ _), cast_mul, ← one_div_mul_one_div, mul_comm (1 / (m : ℝ)),
mul_assoc, one_div_mul_cancel hm', mul_one]
simpa [h_eq] using tendsto_smoothingFun_of_map_one_le_one μ hμ1 _
