English
If x is multiplicative for f, then seminormFromConst' hf1 hc hpm x equals f x under suitable hypotheses; i.e., if ∀ y, f(xy) = f(x) f(y) then seminormFromConst' hf1 hc hpm x = f x.
Русский
Если x мультипликативно относительно f, то при подходящих гипотезах SeminormFromConst' hf1 hc hpm x = f x.
LaTeX
$$$(\forall y, f(xy)=f(x)f(y)) \Rightarrow \ seminomFromConst'(hf1,hc,hpm) x = f x$$$
Lean4
/-- If `x : R` is multiplicative for `f`, then `seminormFromConst' hf1 hc hpm x = f x`. -/
theorem seminormFromConst_apply_of_isMul {x : R} (hx : ∀ y : R, f (x * y) = f x * f y) :
seminormFromConst' hf1 hc hpm x = f x :=
have hlim : Tendsto (seminormFromConst_seq c f x) atTop (𝓝 (f x)) :=
by
have hseq : seminormFromConst_seq c f x = fun _n ↦ f x :=
by
ext n
by_cases hn : n = 0
· simp only [seminormFromConst_seq, hn, pow_zero, mul_one, div_one]
·
simp only [seminormFromConst_seq, hx (c ^ n), hpm _ (Nat.one_le_iff_ne_zero.mpr hn), mul_div_assoc,
div_self (pow_ne_zero n hc), mul_one]
rw [hseq]
exact tendsto_const_nhds
tendsto_nhds_unique (seminormFromConst_isLimit hf1 hc hpm x) hlim
