Ceva's theorem.

This file proves various versions of Ceva's theorem.

References

• https://en.wikipedia.org/wiki/Ceva%27s_theorem

theorem AffineIndependent.exists_affineCombination_eq_smul_eq {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {p : ι → P} (hp : AffineIndependent k p) {s : Set ι} (hs : s.Nonempty) {fs : ↑s → Finset ι} {w : ↑s → ι → k} (hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1) {p' : P} (hp' : ∀ (i : ↑s), p' ∈ affineSpan k {p ↑i, (Finset.affineCombination k (fs i) p) (w i)}) : ∃ (w' : ι → k) (fs' : Finset ι), ∑ j ∈ fs', w' j = 1 ∧ (Finset.affineCombination k fs' p) w' = p' ∧ ∀ (i : ↑s), ∃ (r : k), ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑fs' \ {↑i}).indicator w' j

A version of Ceva's theorem for an arbitrary indexed affinely independent family of points: consider some lines, each through one of the points and an affine combination of the points, and suppose they concur at p'; then p' is an affine combination of the points with weights proportional to those in the respective affine combinations.

theorem AffineIndependent.exists_affineCombination_eq_smul_eq_of_fintype {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Fintype ι] {p : ι → P} (hp : AffineIndependent k p) {s : Set ι} (hs : s.Nonempty) {w : ↑s → ι → k} (hw : ∀ (i : ↑s), ∑ j : ι, w i j = 1) {p' : P} (hp' : ∀ (i : ↑s), p' ∈ affineSpan k {p ↑i, (Finset.affineCombination k Finset.univ p) (w i)}) : ∃ (w' : ι → k), ∑ j : ι, w' j = 1 ∧ (Finset.affineCombination k Finset.univ p) w' = p' ∧ ∀ (i : ↑s), ∃ (r : k), ∀ (j : ι), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j

A version of Ceva's theorem for a finite indexed affinely independent family of points: consider some lines, each through one of the points and an affine combination of the points, and suppose they concur at p'; then p' is an affine combination of the points with weights proportional to those in the respective affine combinations.

theorem Affine.Triangle.prod_eq_prod_one_sub_of_mem_line_point_lineMap {k : Type u_1} {V : Type u_2} {P : Type u_3} [CommRing k] [NoZeroDivisors k] [AddCommGroup V] [Module k V] [AddTorsor V P] {t : Triangle k P} {r : Fin 3 → k} {p' : P} (hp' : ∀ (i : Fin 3), p' ∈ affineSpan k {t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)}) : ∏ i : Fin 3, r i = ∏ i : Fin 3, (1 - r i)

Ceva's theorem for a triangle, expressed in terms of multiplying weights.

theorem Affine.Triangle.prod_div_one_sub_eq_one_of_mem_line_point_lineMap {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [AddCommGroup V] [Module k V] [AddTorsor V P] {t : Triangle k P} {r : Fin 3 → k} (hr0 : ∀ (i : Fin 3), r i ≠ 0) {p' : P} (hp' : ∀ (i : Fin 3), p' ∈ affineSpan k {t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)}) : ∏ i : Fin 3, r i / (1 - r i) = 1

Ceva's theorem for a triangle, expressed using division.