Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: port Geometry.Euclidean.Sphere.Ptolemy (#5037)
- Loading branch information
1 parent
d746104
commit 8663fc7
Showing
2 changed files
with
78 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,77 @@ | ||
/- | ||
Copyright (c) 2021 Manuel Candales. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Manuel Candales, Benjamin Davidson | ||
! This file was ported from Lean 3 source module geometry.euclidean.sphere.ptolemy | ||
! leanprover-community/mathlib commit 46b633fd842bef9469441c0209906f6dddd2b4f5 | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
-/ | ||
import Mathlib.Geometry.Euclidean.Sphere.Power | ||
import Mathlib.Geometry.Euclidean.Triangle | ||
|
||
/-! | ||
# Ptolemy's theorem | ||
This file proves Ptolemy's theorem on the lengths of the diagonals and sides of a cyclic | ||
quadrilateral. | ||
## Main theorems | ||
* `mul_dist_add_mul_dist_eq_mul_dist_of_cospherical`: Ptolemy’s Theorem (Freek No. 95). | ||
TODO: The current statement of Ptolemy’s theorem works around the lack of a "cyclic polygon" concept | ||
in mathlib, which is what the theorem statement would naturally use (or two such concepts, since | ||
both a strict version, where all vertices must be distinct, and a weak version, where consecutive | ||
vertices may be equal, would be useful; Ptolemy's theorem should then use the weak one). | ||
An API needs to be built around that concept, which would include: | ||
- strict cyclic implies weak cyclic, | ||
- weak cyclic and consecutive points distinct implies strict cyclic, | ||
- weak/strict cyclic implies weak/strict cyclic for any subsequence, | ||
- any three points on a sphere are weakly or strictly cyclic according to whether they are distinct, | ||
- any number of points on a sphere intersected with a two-dimensional affine subspace are cyclic in | ||
some order, | ||
- a list of points is cyclic if and only if its reversal is, | ||
- a list of points is cyclic if and only if any cyclic permutation is, while other permutations | ||
are not when the points are distinct, | ||
- a point P where the diagonals of a cyclic polygon cross exists (and is unique) with weak/strict | ||
betweenness depending on weak/strict cyclicity, | ||
- four points on a sphere with such a point P are cyclic in the appropriate order, | ||
and so on. | ||
-/ | ||
|
||
|
||
open Real | ||
|
||
open scoped EuclideanGeometry RealInnerProductSpace Real | ||
|
||
namespace EuclideanGeometry | ||
|
||
variable {V : Type _} [NormedAddCommGroup V] [InnerProductSpace ℝ V] | ||
|
||
variable {P : Type _} [MetricSpace P] [NormedAddTorsor V P] | ||
|
||
/-- **Ptolemy’s Theorem**. -/ | ||
theorem mul_dist_add_mul_dist_eq_mul_dist_of_cospherical {a b c d p : P} | ||
(h : Cospherical ({a, b, c, d} : Set P)) (hapc : ∠ a p c = π) (hbpd : ∠ b p d = π) : | ||
dist a b * dist c d + dist b c * dist d a = dist a c * dist b d := by | ||
have h' : Cospherical ({a, c, b, d} : Set P) := by rwa [Set.insert_comm c b {d}] | ||
have hmul := mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi h' hapc hbpd | ||
have hbp := left_dist_ne_zero_of_angle_eq_pi hbpd | ||
have h₁ : dist c d = dist c p / dist b p * dist a b := by | ||
rw [dist_mul_of_eq_angle_of_dist_mul b p a c p d, dist_comm a b] | ||
· rw [angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hbpd hapc, angle_comm] | ||
all_goals field_simp [mul_comm, hmul] | ||
have h₂ : dist d a = dist a p / dist b p * dist b c := by | ||
rw [dist_mul_of_eq_angle_of_dist_mul c p b d p a, dist_comm c b] | ||
· rwa [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi]; rwa [angle_comm] | ||
all_goals field_simp [mul_comm, hmul] | ||
have h₃ : dist d p = dist a p * dist c p / dist b p := by field_simp [mul_comm, hmul] | ||
have h₄ : ∀ x y : ℝ, x * (y * x) = x * x * y := fun x y => by rw [mul_left_comm, mul_comm] | ||
field_simp [h₁, h₂, dist_eq_add_dist_of_angle_eq_pi hbpd, h₃, hbp, dist_comm a b, h₄, ← sq, | ||
dist_sq_mul_dist_add_dist_sq_mul_dist b, hapc] | ||
#align euclidean_geometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical | ||
|
||
end EuclideanGeometry |