English
The seminormFromConst' hf1 hc hpm is power-multiplicative, i.e., (f(x^m))^n = f(x)^(mn) in the seminorm sense.
Русский
seminormFromConst' является степенно-мультипликативной: (f(x^m))^n = f(x)^{mn}.
LaTeX
$$IsPowMul (seminormFromConst' hf1 hc hpm)$$
Lean4
/-- The function `seminormFromConst' hf1 hc hpm` is power-multiplicative. -/
theorem seminormFromConst_isPowMul : IsPowMul (seminormFromConst' hf1 hc hpm) := fun x m hm ↦
by
simp only [seminormFromConst']
have hlim :
Tendsto (fun n ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop (𝓝 (seminormFromConst' hf1 hc hpm (x ^ m))) :=
by
apply
(seminormFromConst_isLimit hf1 hc hpm (x ^ m)).comp
(tendsto_atTop_atTop_of_monotone (fun _ _ hnk ↦ mul_le_mul_left' hnk m) _)
rintro n; use n; exact le_mul_of_one_le_left' hm
apply tendsto_nhds_unique hlim
convert (seminormFromConst_isLimit hf1 hc hpm x).pow m using 1
ext n
simp only [seminormFromConst_seq, div_pow, ← hpm _ hm, ← pow_mul, mul_pow, mul_comm m n]
