English
In a normed ring with summable geometric series, if t is sufficiently small (‖t‖ < ‖x⁻¹‖⁻¹), then x+t is a unit. The construction provides an explicit Units structure for x+t.
Русский
В нормированном кольце с суммируемым геометрическим рядом, если t достаточно мал (‖t‖ < ‖x⁻¹‖⁻¹), то x+t является единицей; конструируется явная структура Units для x+t.
LaTeX
$$$\text{If } x \in R^{\times},\; \|t\| < \|x^{-1}\|^{-1} \Rightarrow x+t \in R^{\times}.$$$
Lean4
/-- In a normed ring with summable geometric series, a perturbation of a unit `x` by an
element `t` of distance less than `‖x⁻¹‖⁻¹` from `x` is a unit.
Here we construct its `Units` structure. -/
@[simps! val]
def add (x : Rˣ) (t : R) (h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹) : Rˣ :=
Units.copy
(x *
Units.oneSub (-((x⁻¹).1 * t))
(by
nontriviality R using zero_lt_one
have hpos : 0 < ‖(↑x⁻¹ : R)‖ := Units.norm_pos x⁻¹
calc
‖-(↑x⁻¹ * t)‖ = ‖↑x⁻¹ * t‖ := by rw [norm_neg]
_ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖ := (norm_mul_le (x⁻¹).1 _)
_ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ := by nlinarith only [h, hpos]
_ = 1 := mul_inv_cancel₀ (ne_of_gt hpos)))
(x + t) (by simp [mul_add]) _ rfl
