English
Under suitable hypotheses, smoothingFun μ (x y) = smoothingFun μ x · smoothingFun μ y.
Русский
При подходящих гипотезах сглаженная функция μ умножается по аргументу: smoothingFun μ (x y) = smoothingFun μ x · smoothingFun μ y.
LaTeX
$$$smoothingFun \; μ (x y) = smoothingFun \; μ x \cdot smoothingFun \; μ y$$$
Lean4
/-- If `μ 1 ≤ 1`, and `x` is multiplicative for `μ`, then it is multiplicative for
`smoothingFun`. -/
theorem smoothingFun_of_map_mul_eq_mul (hμ1 : μ 1 ≤ 1) {x : R} (hx : ∀ y : R, μ (x * y) = μ x * μ y) (y : R) :
smoothingFun μ (x * y) = smoothingFun μ x * smoothingFun μ y :=
by
have hlim : Tendsto (fun n => μ x * smoothingSeminormSeq μ y n) atTop (𝓝 (smoothingFun μ x * smoothingFun μ y)) :=
by
rw [smoothingFun_apply_of_map_mul_eq_mul μ hμ1 hx]
exact Tendsto.const_mul _ (tendsto_smoothingFun_of_map_one_le_one μ hμ1 y)
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 (x * y)) hlim
simp only [EventuallyEq, eventually_atTop, ge_iff_le]
use 1
intro n hn1
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (_root_.ne_of_gt (lt_of_lt_of_le zero_lt_one hn1))
simp only [smoothingSeminormSeq]
rw [mul_pow, pow_mul_apply_eq_pow_mul μ hx, mul_rpow (pow_nonneg (apply_nonneg μ _) _) (apply_nonneg μ _), ←
rpow_natCast, ← rpow_mul (apply_nonneg μ _), mul_one_div_cancel hn0, rpow_one]
