English
For any p with p ≠ 0 and any real x, the equality ‖(x : AddCircle p)‖ = |x| holds if and only if |x| ≤ |p|/2.
Русский
Пусть p ≠ 0 и y ∈ ℝ. Тогда выполняется равенство ‖(y : AddCircle p)‖ = |y| тогда и только тогда, когда |y| ≤ |p|/2.
LaTeX
$$$p \\neq 0 \\Rightarrow (\\| (x : \\mathrm{AddCircle}(p)) \\| = |x| \\iff |x| \\le \\dfrac{|p|}{2})$$$
Lean4
theorem norm_coe_eq_abs_iff {x : ℝ} (hp : p ≠ 0) : ‖(x : AddCircle p)‖ = |x| ↔ |x| ≤ |p| / 2 :=
by
refine ⟨fun hx => hx ▸ norm_le_half_period p hp, fun hx => ?_⟩
suffices ∀ p : ℝ, 0 < p → |x| ≤ p / 2 → ‖(x : AddCircle p)‖ = |x|
by
rcases hp.symm.lt_or_gt with (hp | hp)
· rw [abs_eq_self.mpr hp.le] at hx
exact this p hp hx
· rw [← norm_neg_period]
rw [abs_eq_neg_self.mpr hp.le] at hx
exact this (-p) (neg_pos.mpr hp) hx
clear hx
intro p hp hx
rcases eq_or_ne x (p / (2 : ℝ)) with (rfl | hx')
· simp [abs_div]
suffices round (p⁻¹ * x) = 0 by simp [norm_eq, this]
rw [round_eq_zero_iff]
obtain ⟨hx₁, hx₂⟩ := abs_le.mp hx
replace hx₂ := Ne.lt_of_le hx' hx₂
constructor
· rwa [le_inv_mul_iff₀ hp, mul_neg, ← mul_div_assoc, mul_one]
· rwa [inv_mul_lt_iff₀ hp, ← mul_div_assoc, mul_one]
