British flag theorem

This file proves the British flag theorem: for a rectangle a b c d and any point p, the sum of the squares of the distances from p to the opposite corners a and c equals the sum of the squares of the distances from p to b and d. The point p need not lie in the plane of the rectangle.

The rectangle is expressed as a (possibly degenerate) parallelogram, in the form that the diagonals a c and b d have the same midpoint, with a right angle at a. A generalization to an arbitrary parallelogram, with a correction term involving the cosine of the angle at a, is proved along the way.

Main results

• EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_of_angle_eq_pi_div_two: the British flag theorem.
• EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two: the if-and-only-if form: among parallelograms, the conclusion of the British flag theorem characterizes rectangles.

References

• https://en.wikipedia.org/wiki/British_flag_theorem

theorem InnerProductGeometry.norm_sq_add_norm_sub_add_sq_eq_norm_sub_sq_add_norm_sub_sq_add_two_mul_inner {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x u v : V) : ‖x‖ ^ 2 + ‖x - (u + v)‖ ^ 2 = ‖x - u‖ ^ 2 + ‖x - v‖ ^ 2 + 2 * inner ℝ u v

The identity underlying the British flag theorem, for the parallelogram with vertices 0, u, u + v and v and any point x, vector form.

theorem InnerProductGeometry.norm_sq_add_norm_sub_add_sq_eq_norm_sub_sq_add_norm_sub_sq_iff_inner_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x u v : V) : ‖x‖ ^ 2 + ‖x - (u + v)‖ ^ 2 = ‖x - u‖ ^ 2 + ‖x - v‖ ^ 2 ↔ inner ℝ u v = 0

British flag theorem, if-and-only-if vector form.

theorem EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_add_two_mul_inner {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c d : P} (h : midpoint ℝ a c = midpoint ℝ b d) (p : P) : dist p a ^ 2 + dist p c ^ 2 = dist p b ^ 2 + dist p d ^ 2 + 2 * inner ℝ (b -ᵥ a) (d -ᵥ a)

The British flag identity for a parallelogram, with the correction term written as an inner product.

theorem EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_add_two_mul_dist_mul_dist_mul_cos_angle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c d : P} (h : midpoint ℝ a c = midpoint ℝ b d) (p : P) : dist p a ^ 2 + dist p c ^ 2 = dist p b ^ 2 + dist p d ^ 2 + 2 * dist b a * dist d a * Real.cos (angle b a d)

The British flag theorem generalized to parallelograms, with a correction term of twice the product of the sides at a and the cosine of the angle at a.

theorem EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c d : P} (h : midpoint ℝ a c = midpoint ℝ b d) (p : P) : dist p a ^ 2 + dist p c ^ 2 = dist p b ^ 2 + dist p d ^ 2 ↔ angle b a d = Real.pi / 2

British flag theorem, if-and-only-if form: for a parallelogram a b c d and any point p, the British flag identity holds if and only if the angle at a is a right angle.

theorem EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_of_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c d : P} (h : midpoint ℝ a c = midpoint ℝ b d) (ha : angle b a d = Real.pi / 2) (p : P) : dist p a ^ 2 + dist p c ^ 2 = dist p b ^ 2 + dist p d ^ 2

British flag theorem: for a rectangle a b c d and any point p (not necessarily in the plane of the rectangle), the sum of the squares of the distances from p to the opposite corners a and c equals the sum of the squares of the distances from p to b and d.