Changes
2 changed files (+128/-0)
-
Marden.lean (new)
-
@@ -0,0 +1,15 @@import Mathlib variable (a b c : ℂ) def complexCollinear := ((a - b) / (b - c)).im = 0 -- Root of 3x^2-2(a+b+c)x+(ab+bc+ac) noncomputable def derivPosRoot := (a + b + c + ((a + b + c) ^ 2 - 3 * (a * b + b * c + a * c)) ^ (1 / 2 : ℂ)) / 3 noncomputable def derivNegRoot := (a + b + c - ((a + b + c) ^ 2 - 3 * (a * b + b * c + a * c)) ^ (1 / 2 : ℂ)) / 3 noncomputable def distSum (z : ℂ) := ‖derivPosRoot a b c - z‖ + ‖derivNegRoot a b c - z‖ theorem marden (h : ¬complexCollinear a b c) : ∃ d, distSum (z := a / 2 + b / 2) = d ∧ distSum (z := b / 2 + c / 2) = d ∧ distSum (z := a / 2 + c / 2) = d := by sorry
-
-
MardenAristotle.lean (new)
-
@@ -0,0 +1,113 @@/- This file was edited by Aristotle. Lean version: leanprover/lean4:v4.24.0 Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7 This project request had uuid: 4cdeee76-7bdc-4cbc-8d02-4ea24e853538 The following was proved by Aristotle: - theorem marden (h : ¬complexCollinear a b c) : ∃ d, distSum (z -/ import Mathlib variable (a b c : ℂ) def complexCollinear := ((a - b) / (b - c)).im = 0 -- Root of 3x^2-2(a+b+c)x+(ab+bc+ac) noncomputable def derivPosRoot := (a + b + c + ((a + b + c) ^ 2 - 3 * (a * b + b * c + a * c)) ^ (1 / 2 : ℂ)) / 3 noncomputable def derivNegRoot := (a + b + c - ((a + b + c) ^ 2 - 3 * (a * b + b * c + a * c)) ^ (1 / 2 : ℂ)) / 3 noncomputable def distSum (z : ℂ) := ‖derivPosRoot a b c - z‖ + ‖derivNegRoot a b c - z‖ noncomputable section AristotleLemmas /- Algebraic identity for Marden's theorem proof. -/ theorem marden_square_identity (a b c : ℂ) : (2 * c - a - b) ^ 2 - 4 * ((a + b + c) ^ 2 - 3 * (a * b + b * c + a * c)) = -3 * (a - b) ^ 2 := by ring /- Symmetry of the algebraic expression involved in Marden's theorem. -/ lemma marden_norm_symmetry (a b c : ℂ) : Complex.normSq (a + b - 2 * c) + 3 * Complex.normSq (a - b) = Complex.normSq (b + c - 2 * a) + 3 * Complex.normSq (b - c) := by simpa [ Complex.normSq ] using by ring; /- Identity for the square of the sum of distances from x to y and -y. -/ lemma norm_add_norm_sub_sq (x y : ℂ) : (‖x + y‖ + ‖x - y‖) ^ 2 = 2 * (‖x‖ ^ 2 + ‖y‖ ^ 2) + 2 * ‖x ^ 2 - y ^ 2‖ := by -- Expanding the left-hand side using the parallelogram law: have h_lhs : (‖x + y‖ + ‖x - y‖) ^ 2 = ‖x + y‖ ^ 2 + 2 * ‖x + y‖ * ‖x - y‖ + ‖x - y‖ ^ 2 := by ring; norm_num [ Complex.normSq, Complex.sq_norm ] at * ; ring_nf at * ; aesop; rw [ show x ^ 2 - y ^ 2 = ( x + y ) * ( x - y ) by ring, norm_mul ] ; ring; /- The sum of distances from the roots of the derivative to the midpoint of AB equals the sum of distances to the midpoint of BC. -/ lemma marden_distSum_eq (a b c : ℂ) : distSum a b c ((a + b) / 2) = distSum a b c ((b + c) / 2) := by -- Let $z_1, z_2$ be the roots `derivPosRoot a b c` and `derivNegRoot a b c`. set z1 := derivPosRoot a b c set z2 := derivNegRoot a b c; -- Let $m = (a+b)/2$ and $m' = (b+c)/2$. set m : ℂ := (a + b) / 2 set m' : ℂ := (b + c) / 2; -- We want to compute $S = |z_1 - m| + |z_2 - m|$. -- By `norm_add_norm_sub_sq`, $S^2 = 2(|x|^2 + |y|^2) + 2|x^2 - y^2|$, where $x = \frac{z_1+z_2}{2} - m$ and $y = \frac{z_1-z_2}{2}$. let x := (z1 + z2) / 2 - m let y := (z1 - z2) / 2 have hx : x = (2 * c - a - b) / 6 := by unfold x z1 z2 m; ring; unfold derivPosRoot derivNegRoot; ring; have hy : y ^ 2 = ((a + b + c) ^ 2 - 3 * (a * b + b * c + a * c)) / 9 := by -- By definition of $y$, we know that $y^2 = \left(\frac{z_1 - z_2}{2}\right)^2$. simp [y, derivPosRoot, derivNegRoot] field_simp ring; rw [ show z1 = ( a + b + c + ( ( a + b + c ) ^ 2 - 3 * ( a * b + b * c + a * c ) ) ^ ( 1 / 2 : ℂ ) ) / 3 by rfl, show z2 = ( a + b + c - ( ( a + b + c ) ^ 2 - 3 * ( a * b + b * c + a * c ) ) ^ ( 1 / 2 : ℂ ) ) / 3 by rfl ] ; ring ; norm_num [ ← Complex.cpow_nat_mul ] ; ring; have hxy : x ^ 2 - y ^ 2 = - (a - b) ^ 2 / 12 := by rw [ hx, hy ] ; ring have h_norm_sq : ‖z1 - m‖ + ‖z2 - m‖ = Real.sqrt (2 * (‖x‖ ^ 2 + ‖y‖ ^ 2) + 2 * ‖x ^ 2 - y ^ 2‖) := by have h_norm_sq : (‖z1 - m‖ + ‖z2 - m‖) ^ 2 = 2 * (‖x‖ ^ 2 + ‖y‖ ^ 2) + 2 * ‖x ^ 2 - y ^ 2‖ := by convert norm_add_norm_sub_sq ( x ) ( y ) using 1 ; ring; rw [ show x + y = z1 - m by ring, show x - y = -m + z2 by ring ]; rw [ ← h_norm_sq, Real.sqrt_sq ( add_nonneg ( norm_nonneg _ ) ( norm_nonneg _ ) ) ]; -- Similarly, let $x' = \frac{z_1+z_2}{2} - m'$ and $y' = \frac{z_1-z_2}{2}$. let x' := (z1 + z2) / 2 - m' let y' := (z1 - z2) / 2 have hx' : x' = (2 * a - b - c) / 6 := by grind have hy' : y' ^ 2 = ((a + b + c) ^ 2 - 3 * (a * b + b * c + a * c)) / 9 := by exact hy have hxy' : x' ^ 2 - y' ^ 2 = - (b - c) ^ 2 / 12 := by rw [ hx', hy' ] ; ring have h_norm_sq' : ‖z1 - m'‖ + ‖z2 - m'‖ = Real.sqrt (2 * (‖x'‖ ^ 2 + ‖y'‖ ^ 2) + 2 * ‖x' ^ 2 - y' ^ 2‖) := by rw [ ← norm_add_norm_sub_sq ]; rw [ Real.sqrt_sq ( by positivity ) ] ; ring!; -- By `marden_norm_symmetry`, the term $|2c-a-b|^2 + 3|a-b|^2$ is equal to $|2a-b-c|^2 + 3|b-c|^2$, which corresponds to the expression for $m' = (b+c)/2$. have h_symm : ‖x‖ ^ 2 + ‖y‖ ^ 2 + ‖x ^ 2 - y ^ 2‖ = ‖x'‖ ^ 2 + ‖y'‖ ^ 2 + ‖x' ^ 2 - y' ^ 2‖ := by aesop; norm_num [ Complex.normSq, Complex.sq_norm ] at * ; ring_nf at * ; aesop; norm_num [ Complex.normSq, Complex.sq_norm ] ; ring; convert h_norm_sq.trans ( congr_arg Real.sqrt <| show 2 * ( ‖x‖ ^ 2 + ‖y‖ ^ 2 ) + 2 * ‖x ^ 2 - y ^ 2‖ = 2 * ( ‖x'‖ ^ 2 + ‖y'‖ ^ 2 ) + 2 * ‖x' ^ 2 - y' ^ 2‖ by linear_combination' h_symm * 2 ) using 1 end AristotleLemmas theorem marden (h : ¬complexCollinear a b c) : ∃ d, distSum (z := a / 2 + b / 2) = d ∧ distSum (z := b / 2 + c / 2) = d ∧ distSum (z := a / 2 + c / 2) = d := by refine' ⟨ _, rfl, _, _ ⟩; · -- By definition of marden_distSum_eq, we have: funext a b c; exact (by convert marden_distSum_eq a b c |> Eq.symm using 1 ; ring; ring); · funext a b c; exact (by convert marden_distSum_eq b a c |> Eq.symm using 1 <;> ring!; · unfold distSum; ring; unfold derivPosRoot derivNegRoot; ring; · unfold distSum; unfold derivPosRoot derivNegRoot; ring;)
-