English
If x,y have norms ≤ r and x ≠ y, and a,b>0 with a+b=1, then the convex combination has norm strictly less than r.
Русский
Если ||x|| ≤ r и ||y|| ≤ r, x ≠ y, и a,b>0 с a+b=1, то ||a x + b y|| < r.
LaTeX
$$$\|x\| \le r,\ \|y\| \le r,\ x \neq y,\ a>0,\ b>0,\ a+b=1 \Rightarrow \|a x + b y\| < r$$$
Lean4
/-- If `x` and `y` are two distinct vectors of norm at most `r`, then a convex combination of `x`
and `y` with positive coefficients has norm strictly less than `r`. -/
theorem norm_combo_lt_of_ne (hx : ‖x‖ ≤ r) (hy : ‖y‖ ≤ r) (hne : x ≠ y) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) :
‖a • x + b • y‖ < r :=
by
simp only [← mem_ball_zero_iff, ← mem_closedBall_zero_iff] at hx hy ⊢
exact combo_mem_ball_of_ne hx hy hne ha hb hab
