English
The map addEquiv 𝕜 A is antilipschitz with constant 2.
Русский
Отображение addEquiv 𝕜 A является антилипшицевым с константой 2.
LaTeX
$$$$\\text{AntilipschitzWith}(2,\\ addEquiv\\ 𝕜 A).$$$$
Lean4
theorem antilipschitzWith_addEquiv : AntilipschitzWith 2 (addEquiv 𝕜 A) :=
by
refine AddMonoidHomClass.antilipschitz_of_bound (addEquiv 𝕜 A) fun x => ?_
rw [norm_eq_sup, Prod.norm_def, NNReal.coe_two]
refine max_le ?_ ?_
· rw [mul_max_of_nonneg _ _ (zero_le_two : (0 : ℝ) ≤ 2)]
exact le_max_of_le_left ((le_add_of_nonneg_left (norm_nonneg _)).trans_eq (two_mul _).symm)
· nontriviality A
calc
‖algebraMap 𝕜 _ x.fst + mul 𝕜 A x.snd‖ ≤ ‖algebraMap 𝕜 _ x.fst‖ + ‖mul 𝕜 A x.snd‖ := norm_add_le _ _
_ = ‖x.fst‖ + ‖x.snd‖ := by
rw [norm_algebraMap', (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 A)).mp (isometry_mul 𝕜 A)]
_ ≤ _ := (add_le_add (le_max_left _ _) (le_max_right _ _)).trans_eq (two_mul _).symm
