English
As above, a form of Stewart: sum of two squared legs equals product of BC with sum of square of AB and AC.
Русский
Как выше, форма Стюарта: сумма квадратов сторон равна произведению BC на сумму квадратов AB и AC.
LaTeX
$$$\operatorname{dist}(a,b)^2 + \operatorname{dist}(a,c)^2 = 2\left( \operatorname{dist}(a,\text{midpoint}(b,c))^2 + (\operatorname{dist}(b,c)/2)^2\right)$$$
Lean4
/-- **Apollonius's Theorem**. -/
theorem dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq (a b c : P) :
dist a b ^ 2 + dist a c ^ 2 = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2) :=
by
by_cases hbc : b = c
· simp [hbc, midpoint_self, dist_self, two_mul]
· let m := midpoint ℝ b c
have : dist b c ≠ 0 := (dist_pos.mpr hbc).ne'
have hm := dist_sq_mul_dist_add_dist_sq_mul_dist a b c m (angle_midpoint_eq_pi b c hbc)
simp only [m, dist_left_midpoint, dist_right_midpoint, Real.norm_two] at hm
calc
dist a b ^ 2 + dist a c ^ 2 =
2 / dist b c * (dist a b ^ 2 * ((2 : ℝ)⁻¹ * dist b c) + dist a c ^ 2 * (2⁻¹ * dist b c)) :=
by field_simp
_ = 2 * (dist a (midpoint ℝ b c) ^ 2 + (dist b c / 2) ^ 2) :=
by
rw [hm]
field_simp
