English
Let x ∈ R. Then for the constant-based seminorm, we have a multiplicativity in the argument: seminormFromConst'(hf1 hc hpm)(c x) = seminormFromConst'(hf1 hc hpm c) · seminormFromConst'(hf1 hc hpm x).
Русский
Пусть x ∈ R. Тогда константо-определённая семинормa удовлетворяет правилу умножения в аргументе: seminormFromConst'(hf1 hc hpm)(c x) = seminormFromConst'(hf1 hc hpm c) · seminormFromConst'(hf1 hc hpm x).
LaTeX
$$$\operatorname{seminormFromConst'}_{hf1,hc,hpm}(c x) = \operatorname{seminormFromConst'}_{hf1,hc,hpm}(c) \cdot \operatorname{seminormFromConst'}_{hf1,hc,hpm}(x)$$$
Lean4
/-- For every `x : R`, `seminormFromConst' hf1 hc hpm (c * x)` equals the product
`seminormFromConst' hf1 hc hpm c * SeminormFromConst' hf1 hc hpm x`. -/
theorem seminormFromConst_const_mul (x : R) :
seminormFromConst' hf1 hc hpm (c * x) = seminormFromConst' hf1 hc hpm c * seminormFromConst' hf1 hc hpm x :=
by
have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' hf1 hc hpm x)) :=
by
apply
(seminormFromConst_isLimit hf1 hc hpm x).comp
(tendsto_atTop_atTop_of_monotone (fun _ _ hnm ↦ add_le_add_right hnm 1) _)
rintro n; use n; omega
rw [seminormFromConst_apply_c hf1 hc hpm]
apply tendsto_nhds_unique (seminormFromConst_isLimit hf1 hc hpm (c * x))
have hterm : seminormFromConst_seq c f (c * x) = fun n ↦ f c * seminormFromConst_seq c f x (n + 1) :=
by
simp only [seminormFromConst_seq_def]
ext n
ring_nf
rw [mul_assoc _ (f c), mul_inv_cancel₀ hc, mul_one]
simpa [hterm] using tendsto_const_nhds.mul hlim
