English
For any x ∈ ℝ, the norm of x in AddCircle p is the distance to the nearest integer multiple of p, i.e., ‖(x : AddCircle p)‖ = |x − round(p⁻¹ x) p|.
Русский
Для любого x ∈ ℝ норма x в AddCircle p равна расстоянию до ближайшего кратного p, т. е. ‖(x : AddCircle p)‖ = |x − round(p⁻¹ x) p|.
LaTeX
$$$$\\| (x : \\mathrm{AddCircle}(p)) \\| = | x - \\operatorname{round}(p^{-1} x) \\cdot p |.$$$$
Lean4
theorem norm_eq {x : ℝ} : ‖(x : AddCircle p)‖ = |x - round (p⁻¹ * x) * p| :=
by
suffices ∀ x : ℝ, ‖(x : AddCircle (1 : ℝ))‖ = |x - round x|
by
rcases eq_or_ne p 0 with (rfl | hp)
· simp
have hx := norm_coe_mul p x p⁻¹
rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx
rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]
clear! x p
intro x
simp only [le_antisymm_iff, le_norm_iff, Real.norm_eq_abs]
refine ⟨le_of_forall_le fun r hr ↦ ?_, ?_⟩
· rw [abs_sub_round_eq_min, le_inf_iff]
rw [le_norm_iff] at hr
constructor
· simpa [abs_of_nonneg] using hr (fract x)
· simpa [abs_sub_comm (fract x)] using hr (fract x - 1) (by simp)
·
simpa [zmultiples, QuotientAddGroup.eq, zsmul_eq_mul, mul_one, mem_mk, mem_range, and_imp, forall_exists_index,
eq_neg_add_iff_add_eq, ← eq_sub_iff_add_eq, forall_swap (α := ℕ)] using round_le _
