English
If ‖x‖ = ‖y‖ = 1, then ‖x − y‖ lies between (2/π)·angle x y and angle x y.
Русский
Если ‖x‖ = ‖y‖ = 1, то ‖x − y‖ лежит между (2/π)·angle x y и angle x y.
LaTeX
$$$$\|x - y\| \in \left[ \frac{2}{\pi} \angle x y, \angle x y \right], \quad \|x\| = 1, \|y\| = 1.$$$$
Lean4
/-- Chord-length is a multiple of arc-length up to constants. -/
theorem norm_sub_mem_Icc_angle (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y) :=
by
wlog h : y = 1
· have := @this (x / y) 1 (by simp only [norm_div, hx, hy, div_one]) norm_one rfl
rwa [angle_div_left_eq_angle_mul_right, div_sub_one, norm_div, hy, div_one, one_mul] at this
rintro rfl
simp at hy
subst y
rw [norm_eq_one_iff'] at hx
obtain ⟨θ, hθ, rfl⟩ := hx
rw [angle_exp_one, exp_mul_I, add_sub_right_comm, (toIocMod_eq_self _).2]
· norm_cast
rw [norm_add_mul_I]
refine ⟨Real.le_sqrt_of_sq_le ?_, ?_⟩
· rw [mul_pow, ← abs_pow, abs_sq]
calc
_ = 2 * (1 - (1 - 2 / π ^ 2 * θ ^ 2)) := by ring
_ ≤ 2 * (1 - θ.cos) := by gcongr; exact Real.cos_le_one_sub_mul_cos_sq <| abs_le.2 <| Ioc_subset_Icc_self hθ
_ = _ := by linear_combination -θ.cos_sq_add_sin_sq
· rw [Real.sqrt_le_left (by positivity), ← abs_pow, abs_sq]
calc
_ = 2 * (1 - θ.cos) := by linear_combination θ.cos_sq_add_sin_sq
_ ≤ 2 * (1 - (1 - θ ^ 2 / 2)) := by gcongr; exact Real.one_sub_sq_div_two_le_cos
_ = _ := by ring
· convert hθ
ring
