English
If hμ1 and hx: μ(xy) = μ x μ y, then smoothingFun μ (x y) = smoothingFun μ x · smoothingFun μ y.
Русский
Если hμ1 и hx: μ(xy) = μ x μ y, то smoothingFun μ (xy) = smoothingFun μ x · smoothingFun μ y.
LaTeX
$$$smoothingFun μ (x y) = smoothingFun μ x \cdot smoothingFun μ y$$$
Lean4
/-- If `μ 1 ≤ 1` and `∀ y : R, μ (x * y) = μ x * μ y`, then `smoothingFun μ x = μ x`. -/
theorem smoothingFun_apply_of_map_mul_eq_mul (hμ1 : μ 1 ≤ 1) {x : R} (hx : ∀ y : R, μ (x * y) = μ x * μ y) :
smoothingFun μ x = μ x :=
by
apply tendsto_nhds_unique_of_eventuallyEq (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x) tendsto_const_nhds
simp only [EventuallyEq, eventually_atTop, ge_iff_le]
use 1
intro n hn
simp only [smoothingSeminormSeq]
by_cases hx0 : μ x = 0
· have hxn : μ (x ^ n) = 0 := by
apply le_antisymm _ (apply_nonneg μ _)
apply le_trans (map_pow_le_pow μ x (one_le_iff_ne_zero.mp hn))
rw [hx0, zero_pow (pos_iff_ne_zero.mp hn)]
rw [hx0, hxn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]
· have h1 : μ 1 = 1 := by rw [← mul_right_inj' hx0, ← hx 1, mul_one, mul_one]
have hn0 : (n : ℝ) ≠ 0 := cast_ne_zero.mpr (_root_.ne_of_gt (lt_of_lt_of_le zero_lt_one hn))
rw [← mul_one (x ^ n), pow_mul_apply_eq_pow_mul μ hx, ← rpow_natCast, h1, mul_one, ← rpow_mul (apply_nonneg μ _),
mul_one_div_cancel hn0, rpow_one]
