1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 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;)