English
Let K be a division ring equipped with a valuation v: K → Γ₀ and let γ ∈ Γ₀ˣ. For x,y ∈ K with y ≠ 0, if v(x − y) < min( γ · (v(y))², v(y) ), then v(x⁻¹ − y⁻¹) < γ.
Русский
Пусть K — деление кольцо с валюацией v: K → Γ₀ и γ ∈ Γ₀ˣ. Пусть x, y ∈ K, y ≠ 0. Если v(x − y) < min( γ · (v(y))², v(y) ), то v(x⁻¹ − y⁻¹) < γ.
LaTeX
$$$\forall x,y \in K\,\forall γ \in Γ_0^{\times},\ y \neq 0\;\Rightarrow\; v(x-y) < \min\big( γ \cdot (v(y) \cdot v(y)), v(y) \big) \Rightarrow v(x^{-1}-y^{-1}) < γ$$$
Lean4
theorem inversion_estimate {x y : K} {γ : Γ₀ˣ} (y_ne : y ≠ 0) (h : v (x - y) < min (γ * (v y * v y)) (v y)) :
v (x⁻¹ - y⁻¹) < γ :=
by
have hyp1 : v (x - y) < γ * (v y * v y) := lt_of_lt_of_le h (min_le_left _ _)
have hyp1' : v (x - y) * (v y * v y)⁻¹ < γ := mul_inv_lt_of_lt_mul₀ hyp1
have hyp2 : v (x - y) < v y := lt_of_lt_of_le h (min_le_right _ _)
have key : v x = v y := Valuation.map_eq_of_sub_lt v hyp2
have x_ne : x ≠ 0 := by
intro h
apply y_ne
rw [h, v.map_zero] at key
exact v.zero_iff.1 key.symm
have decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹ := by
rw [mul_sub_left_distrib, sub_mul, mul_assoc, show y * y⁻¹ = 1 from mul_inv_cancel₀ y_ne,
show x⁻¹ * x = 1 from inv_mul_cancel₀ x_ne, mul_one, one_mul]
calc
v (x⁻¹ - y⁻¹) = v (x⁻¹ * (y - x) * y⁻¹) := by rw [decomp]
_ = v x⁻¹ * (v <| y - x) * v y⁻¹ := by repeat' rw [Valuation.map_mul]
_ = (v x)⁻¹ * (v <| y - x) * (v y)⁻¹ := by rw [map_inv₀, map_inv₀]
_ = (v <| y - x) * (v y * v y)⁻¹ := by rw [mul_assoc, mul_comm, key, mul_assoc, mul_inv_rev]
_ = (v <| y - x) * (v y * v y)⁻¹ := rfl
_ = (v <| x - y) * (v y * v y)⁻¹ := by rw [Valuation.map_sub_swap]
_ < γ := hyp1'
