Existence of Euler Line

Stream: Is there code for X?

[Kevin Buzzard]

How do we state the assertion that orthocenter, the circumcenter, and the centroid of a triangle all lie on a line, in Lean, using the approach which I attribute to Joseph Myers? I need to get started somehow so I thought I'd ask a concrete problem so I could start learning from there.

I am tiring of telling schoolchildren about natural numbers, I need a new talk.

[Joseph Myers]

We don't have an explicit definition of euler_line, but affine_span ℝ {s.circumcenter, (univ : finset (fin (n + 1))).centroid ℝ s.points} seems like a reasonable definition to go in geometry.euclidean.monge_point for the Euler line of a simplex. It should then be straightforward to prove that this really is a line (i.e., its direction has finrank equal to 1) if the circumcenter and centroid are different (e.g. using affine_independent_of_ne and finrank_vector_span_of_affine_independent; this would actually be a lemma for linear_algebra.affine_space.finite_dimensional about the finrank of the vector_span of any two different points in an affine space, not something specific to the Euclidean case).

The fact that the monge_point lies on the so-defined euler_line is more or less trivial from how we define monge_point and the definition of affine subspaces and basic lemmas about affine spans; the real work of proving the result you give is that the orthocenter (defined as the monge_point in the two-dimensional case) actually satisfies the properties expected for it (i.e. the lemmas orthocenter_mem_altitude and eq_orthocenter_of_forall_mem_altitude, but the main work is actually the computation in inner_monge_point_vsub_face_centroid_vsub, and much of the work there in turn is done by simp).

[Kevin Buzzard]

For the finrank 1 argument I seem to need vector_span ℝ (set.range ![X, Y]) = vector_span ℝ ↑(affine_span ℝ {X, Y})(with hypothesis X!=Y) (NB simp reduces this to vector_span ℝ {Y, X} = vector_span ℝ (span_points ℝ {X, Y})). Am working my way towards Monge points.

[Joseph Myers]

With more or better simp lemmas it should be possible to get simp to reduce that to vector_span ℝ {Y, X} = vector_span ℝ {X, Y}. There ought to be a simp lemma about the vector_span of the affine_span (deduced from affine_span_coe and direction_affine_span, for example). And the simp lemma coe_affine_span is suspect, really it ought to be the other way round on the principle that the bundled affine_span is normally the preferred representation and span_points should only be used when that specific description of the set of points is of interest.

[Kevin Buzzard]

Yes, Bhavik tamed it in the end at Xena last night (where I broke my pledge to do Lean 4 once a week and instead spent several hours trying to prove that angle at centre equals twice angle at circumference in Lean 3 :-) )