Skip to content

Instantly share code, notes, and snippets.

@kbuzzard
Created June 24, 2021 18:11
Show Gist options
  • Save kbuzzard/4ff9d7812efacd34433ee8ebe1190a46 to your computer and use it in GitHub Desktop.
Save kbuzzard/4ff9d7812efacd34433ee8ebe1190a46 to your computer and use it in GitHub Desktop.
triangle experiments
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment