triangle experiments

gistfile1.txt

import geometry.euclidean.monge_point

-- let's look at the definition of the monge point of a simplex.

/-
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`).
-/
#print affine.simplex.monge_point
#check @affine.simplex.monge_point
/-
affine.simplex.monge_point :
  Π {V : Type u_1} {P : Type u_2} [_inst_1 : inner_product_space ℝ V] [_inst_2 : metric_space P]
  [_inst_3 : normed_add_torsor V P] {n : ℕ}, affine.simplex ℝ P n → P
-/

universes u v

variables {V : Type u} {𝔼 : Type v} [inner_product_space ℝ V] [metric_space 𝔼]
  [normed_add_torsor V 𝔼] {n : ℕ}

include V

open finset

/-- the Euler line of a simplex -/
noncomputable def euler_line (s : affine.simplex ℝ 𝔼 n): affine_subspace ℝ 𝔼 := 
affine_span ℝ {s.circumcenter, (univ : finset (fin (n + 1))).centroid ℝ s.points}

open affine_subspace

open finite_dimensional

/-
(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).
   -/

#check span_points

theorem linear_algebra.affine_space.finite_dimensional.finrank_vector_span_pair_eq_one
  {X Y : 𝔼} (h : X ≠ Y) : 
  finrank ℝ (direction (affine_span ℝ {X, Y} : affine_subspace ℝ 𝔼)) = 1 :=
begin
  have h2 := affine_independent_of_ne ℝ h,
  have h4 : fintype.card (fin 2) = 2 := by simp,
  have h3 := finrank_vector_span_of_affine_independent h2 h4,
  rw ←h3,
  delta direction,
  suffices : vector_span ℝ (set.range ![X, Y]) = vector_span ℝ ↑(affine_span ℝ {X, Y}),
    rw this,
  simp,
  apply le_antisymm,
  { apply vector_span_mono,
    convert subset_span_points _ _ using 2,
    ext, simp, tauto!,
  },
  rw vector_span_def,
  rw vector_span_def,
  rw submodule.span_le,
  intros x hx,
  
--  library_search,
end

theorem euler_line.finrank_eq_one (s : affine.simplex ℝ 𝔼 n)
  (hs : s.circumcenter ≠ (univ : finset (fin (n + 1))).centroid ℝ s.points) : 
  finrank ℝ (direction (euler_line s)) = 1 :=
begin
  exact linear_algebra.affine_space.finite_dimensional.finrank_vector_span_pair_eq_one hs,
end

#check finite_dimensional.finrank
--variable (s : affine.simplex ℝ P 2) -- three affine-independent points.