English
For any x: Fin 2 → ℤ with x ≠ 0, at least one of the squared normalized components is at least 1: 1 ≤ (x0/‖x‖)^2 or 1 ≤ (x1/‖x‖)^2.
Русский
Для любого x ∈ ℤ^2 не нулевого веса хотя бы одна из нормированных компонент удовлетворяет 1 ≤ (x_i/‖x‖)^2.
LaTeX
$$$1 \\le \\left( \\dfrac{x_0}{\\|x\\|} \\right)^2 \\ \\lor\\ 1 \\le \\left( \\dfrac{x_1}{\\|x\\|} \\right)^2,$ где $x = (x_0,x_1) \\neq 0$$$
Lean4
theorem div_max_sq_ge_one (x : Fin 2 → ℤ) (hx : x ≠ 0) : 1 ≤ (x 0 / ‖x‖) ^ 2 ∨ 1 ≤ (x 1 / ‖x‖) ^ 2 :=
by
refine (max_choice (x 0).natAbs (x 1).natAbs).imp (fun H0 ↦ ?_) (fun H1 ↦ ?_)
· have : x 0 ≠ 0 := by rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
simp only [norm_eq_max_natAbs, H0, Int.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq, OfNat.ofNat_ne_zero,
not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self, le_refl]
· have : x 1 ≠ 0 := by rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
simp only [norm_eq_max_natAbs, H1, Int.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq, OfNat.ofNat_ne_zero,
not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self, le_refl]
