Ceva's theorem

Author: YaelDillies

LeanCamCombi/Ceva.lean

@@ -0,0 +1,69 @@
+import Mathlib
+import LeanCamCombi.Mathlib.Analysis.Convex.Combination
+import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.Combination
+
+open AffineMap Finset
+
+variable {ι 𝕜 V : Type*} [DecidableEq ι] [LinearOrderedField 𝕜] [AddCommGroup V] [Module 𝕜 V]
+  {s t : Finset ι} {w : ι → 𝕜} {x y : ι → V} {i : ι}
+
+-- /-- **Ceva's theorem** for affine combinations. -/
+-- theorem ceva_affineComb [Nontrivial 𝕜] (hy : ∀ i ∈ s, y i ∈ affineSpan 𝕜 (x '' (s \ {i})))
+--     (hs : s.Nonempty) :
+--     (∃ z, ∃ c : ι → 𝕜, ∀ i ∈ s, lineMap (y i) (x i) (c i) = z) ↔
+--       ∃ w : ι → 𝕜, ∑ i ∈ s, w i = 1 ∧ ∀ i ∈ s, w i ≠ 1 → (s \ {i}).centerMass w x = y i where
+--   mp := by
+--     rintro ⟨z, c, hz⟩
+--     obtain ⟨i, hi⟩ := hs
+--     norm_cast at hy
+--     obtain ⟨w, hw₁, hyi⟩ := mem_affineSpan_image.1 <| hy i hi
+--     refine ⟨Pi.single i (c i) + (1 - c i) • Function.update w i 0, fun j hj ↦ ?_, ?_, ?_⟩
+--     · sorry
+
+--     -- choose hc₀ hc₁ hz using hz
+--     sorry
+--   mpr := by
+--     rintro ⟨w, hw₁, hwxy⟩
+--     refine ⟨s.centerMass w x, w, fun i hi ↦ ?_⟩
+--     rw [← hwxy, lineMap_centerMass_sdiff_singleton_of_ne_one hi (hw₀ _ hi) hw₁]
+
+/-- **Ceva's theorem** for convex combinations. -/
+theorem ceva_convexComb (hy : ∀ i ∈ s, y i ∈ convexHull 𝕜 (x '' (s \ {i})))
+    (hs : s.Nontrivial) :
+    (∃ z, ∃ c : ι → 𝕜, ∀ i ∈ s, 0 ≤ c i ∧ c i ≤ 1 ∧ lineMap (y i) (x i) (c i) = z) ↔
+      ∃ w : ι → 𝕜,
+        (∀ i ∈ s, 0 ≤ w i) ∧ ∑ i ∈ s, w i = 1 ∧ ∀ i ∈ s, (s \ {i}).centerMass w x = y i where
+  mp := by
+    rintro ⟨z, c, hz⟩
+    choose hc₀ hc₁ hz using hz
+    by_cases hc : ∀ i ∈ s, c i = 1
+    · refine ⟨fun _ ↦ (#s)⁻¹, by simp, by simp [hs.nonempty.card_ne_zero], fun i hi ↦ ?_⟩
+      simp only [centerMass, sum_const, nsmul_eq_mul, mul_inv_rev, inv_inv, ← smul_sum, ← mul_smul,
+        mul_right_comm, ne_eq, Nat.cast_eq_zero, hs.nonempty.card_ne_zero, not_false_eq_true,
+        mul_inv_cancel₀, one_mul]
+      sorry
+      -- obtain ⟨j, hj, hji⟩ := hs.exists_ne i
+    push_neg at hc
+    obtain ⟨i, hi, hci⟩ := hc
+    norm_cast at hy
+    obtain ⟨w, hw₀, hw₁, hyi⟩ := mem_convexHull_image.1 <| hy i hi
+    refine ⟨Pi.single i (c i) + (1 - c i) • Function.update w i 0, fun j hj ↦
+      add_nonneg (Pi.single_nonneg (α := fun _ ↦ 𝕜).2 (hc₀ _ hi) _) <|
+      mul_nonneg (sub_nonneg.2 <| hc₁ _ hi) ?_, ?_, fun j hj ↦ ?_⟩
+    · obtain rfl | hji := eq_or_ne j i
+      · simp
+      · simpa [hji] using hw₀ _ (by simp [*])
+    · simp [sum_add_distrib, hi, ← mul_sum, sum_update_of_mem, ← sum_erase_eq_sub, hw₁]
+    obtain rfl | hij := eq_or_ne i j
+    · rwa [centerMass_congr (w := (1 - c i) • w) (sdiff_singleton_eq_erase ..) _ fun _ _ ↦ rfl,
+        centerMass_smul_left]
+      exact sub_ne_zero.2 hci.symm
+      aesop
+    have := (hz i hi).trans (hz j hj).symm
+    simp [centerMass, sum_add_distrib]
+    sorry
+  mpr := by
+    rintro ⟨w, hw₀, hw₁, hwxy⟩
+    refine ⟨s.centerMass w x, w, fun i hi ↦ ⟨hw₀ _ hi, hw₁ ▸ single_le_sum hw₀ hi, ?_⟩⟩
+    rw [← hwxy _ hi, lineMap_centerMass_sdiff_singleton_of_nonneg hi _ hw₁]
+    exact fun j hj ↦ hw₀ _ <| sdiff_subset hj

LeanCamCombi/Mathlib/Analysis/Convex/Combination.lean

@@ -0,0 +1,114 @@
+import Mathlib.Analysis.Convex.Combination
+
+open AffineMap Finset
+
+section oldVars
+variable {ι R E : Type*} [LinearOrderedField R] [AddCommGroup E] [Module R E] {s : Finset ι}
+  {f : ι → E} {x : E}
+
+lemma mem_convexHull_image :
+    x ∈ convexHull R (f '' s) ↔
+      ∃ w : ι → R, (∀ i ∈ s, 0 ≤ w i) ∧ ∑ i ∈ s, w i = 1 ∧ s.centerMass w f = x where
+  mp hp := by
+    classical
+    rw [← Subtype.range_val (s := s.toSet), ← Set.range_comp,
+      convexHull_range_eq_exists_affineCombination] at hp
+    obtain ⟨t, w, hw₀, hw₁, rfl⟩ := hp
+    refine ⟨fun i ↦ if hi : i ∈ Subtype.val '' (t : Set s.toSet) then w ⟨i, by aesop⟩ else 0,
+      by aesop, ?_⟩
+    · simp [Finset.sum_dite]
+      sorry
+  mpr := by
+    rintro ⟨w, hw₀, hw₁, rfl⟩; exact s.centerMass_mem_convexHull hw₀ (by simp [hw₁]) (by aesop)
+
+end oldVars
+
+variable {ι 𝕜 V : Type*} [LinearOrderedField 𝕜] [AddCommGroup V] [Module 𝕜 V]
+  {s t : Finset ι} {v w : ι → 𝕜} {x y : ι → V} {i : ι}
+
+lemma centerMass_congr (hst : s = t) (hvw : ∀ i ∈ t, v i = w i) (hxy : ∀ i ∈ t, x i = y i) :
+    s.centerMass v x = t.centerMass w y := by
+  unfold centerMass; rw [sum_congr hst hvw, sum_congr hst fun i hi ↦ by rw [hvw i hi, hxy i hi]]
+
+variable [DecidableEq ι]
+
+lemma centerMass_union (hst : Disjoint s t) (hs : (∀ i ∈ s, w i = 0) ∨ ∑ i ∈ s, w i ≠ 0)
+    (ht : (∀ i ∈ t, w i = 0) ∨ ∑ i ∈ t, w i ≠ 0) (hw₁ : ∑ i ∈ s ∪ t, w i = 1) :
+    (s ∪ t).centerMass w x =
+      (∑ i ∈ s, w i) • s.centerMass w x + (∑ i ∈ t, w i) • t.centerMass w x := by
+  obtain hs | hs := hs
+  · simp only [sum_union hst, sum_eq_zero hs, zero_add] at hw₁
+    simp only [centerMass, sum_union hst, sum_eq_zero hs, hw₁, zero_add, inv_one, smul_add,
+      one_smul, inv_zero, zero_smul, smul_zero, add_left_eq_self]
+    exact sum_eq_zero fun i hi ↦ by simp [hs _ hi]
+  obtain ht | ht := ht
+  · simp only [sum_union hst, sum_eq_zero ht, add_zero] at hw₁
+    simp only [centerMass, sum_union hst, hw₁, sum_eq_zero ht, add_zero, inv_one, smul_add,
+      one_smul, inv_zero, zero_smul, smul_zero, add_right_eq_self]
+    exact sum_eq_zero fun i hi ↦ by simp [ht _ hi]
+  · simp [centerMass, hs, ht, hst, sum_union, hw₁]
+
+lemma centerMass_union_of_ne_zero (hst : Disjoint s t) (hs : ∑ i ∈ s, w i ≠ 0)
+    (ht : ∑ i ∈ t, w i ≠ 0) (hw₁ : ∑ i ∈ s ∪ t, w i = 1) :
+    (s ∪ t).centerMass w x =
+      (∑ i ∈ s, w i) • s.centerMass w x + (∑ i ∈ t, w i) • t.centerMass w x :=
+  centerMass_union hst (.inr hs) (.inr ht) hw₁
+
+lemma centerMass_union_of_nonneg (hst : Disjoint s t) (hw₀ : ∀ i ∈ s ∪ t, 0 ≤ w i)
+    (hw₁ : ∑ i ∈ s ∪ t, w i = 1) :
+    (s ∪ t).centerMass w x =
+      (∑ i ∈ s, w i) • s.centerMass w x + (∑ i ∈ t, w i) • t.centerMass w x := by
+  refine centerMass_union hst ?_ ?_ hw₁
+  · rw [← sum_eq_zero_iff_of_nonneg fun j hj ↦ hw₀ _ <| subset_union_left hj]
+    exact em _
+  · rw [← sum_eq_zero_iff_of_nonneg fun j hj ↦ hw₀ _ <| subset_union_right hj]
+    exact em _
+
+lemma lineMap_centerMass_centerMass (hst : Disjoint s t)
+    (hs : (∀ i ∈ s, w i = 0) ∨ ∑ i ∈ s, w i ≠ 0) (ht : (∀ i ∈ t, w i = 0) ∨ ∑ i ∈ t, w i ≠ 0)
+    (hw₁ : ∑ i ∈ s ∪ t, w i = 1) :
+    lineMap (s.centerMass w x) (t.centerMass w x) (∑ i ∈ t, w i) = (s ∪ t).centerMass w x := by
+  rw [lineMap_apply_module, ← hw₁, sum_union hst, add_sub_cancel_right,
+    centerMass_union hst hs ht hw₁]
+
+lemma lineMap_centerMass_centerMass_of_ne_zero (hst : Disjoint s t) (hs : ∑ i ∈ s, w i ≠ 0)
+    (ht : ∑ i ∈ t, w i ≠ 0) (hw₁ : ∑ i ∈ s ∪ t, w i = 1) :
+    lineMap (s.centerMass w x) (t.centerMass w x) (∑ i ∈ t, w i) = (s ∪ t).centerMass w x :=
+  lineMap_centerMass_centerMass hst (.inr hs) (.inr ht) hw₁
+
+lemma lineMap_centerMass_centerMass_of_nonneg (hst : Disjoint s t) (hw₀ : ∀ i ∈ s ∪ t, 0 ≤ w i)
+    (hw₁ : ∑ i ∈ s ∪ t, w i = 1) :
+    lineMap (s.centerMass w x) (t.centerMass w x) (∑ i ∈ t, w i) = (s ∪ t).centerMass w x := by
+  rw [lineMap_apply_module, ← hw₁, sum_union hst, add_sub_cancel_right,
+    centerMass_union_of_nonneg hst hw₀ hw₁]
+
+lemma lineMap_centerMass_sdiff (hi : i ∈ s) (hi₀ : w i ≠ 0) (hi₁ : w i ≠ 1)
+    (hw₁ : ∑ i ∈ s, w i = 1) :
+    lineMap ((s \ {i}).centerMass w x) (x i) (w i) = s.centerMass w x := by
+  rw [← centerMass_singleton i x hi₀, ← sum_singleton w i,
+    lineMap_centerMass_centerMass] <;>
+    simp [*, union_eq_left.2, sub_eq_zero, eq_comm (b := w _)]
+
+lemma centerMass_sdiff_of_weight_eq_zero (hi : i ∈ s) (hi₀ : w i = 0) :
+    (s \ {i}).centerMass w x = s.centerMass w x := by
+  simp [hi₀, sum_sdiff_eq_sub (singleton_subset_iff.2 hi), centerMass]
+
+lemma lineMap_centerMass_sdiff_singleton_of_ne_one (hi : i ∈ s) (hi₁ : w i ≠ 1)
+    (hw₁ : ∑ j ∈ s, w j = 1) :
+    lineMap ((s \ {i}).centerMass w x) (x i) (w i) = s.centerMass w x := by
+  obtain hi₀ | hi₀ := eq_or_ne (w i) 0
+  · simp [centerMass_sdiff_of_weight_eq_zero hi, hi₀]
+  · rw [← centerMass_singleton i x hi₀, ← sum_singleton w i, lineMap_centerMass_centerMass] <;>
+      simp [*, union_eq_left.2, sub_eq_zero, eq_comm (b := w _)]
+
+lemma lineMap_centerMass_sdiff_singleton_of_nonneg (hi : i ∈ s) (hw₀ : ∀ j ∈ s \ {i}, 0 ≤ w j)
+    (hw₁ : ∑ j ∈ s, w j = 1) :
+    lineMap ((s \ {i}).centerMass w x) (x i) (w i) = s.centerMass w x := by
+  obtain hi₁ | hi₁ := eq_or_ne (w i) 1
+  · rw [← centerMass_singleton i x (w := w) (by simp [hi₁]), ← sum_singleton w i,
+      lineMap_centerMass_centerMass]
+    rotate_left 2
+    · rw [← sum_eq_zero_iff_of_nonneg hw₀]
+      exact em _
+    all_goals simp [*, union_eq_left.2, sub_eq_zero, eq_comm (b := w _)]
+  · exact lineMap_centerMass_sdiff_singleton_of_ne_one hi hi₁ hw₁

LeanCamCombi/Mathlib/LinearAlgebra/AffineSpace/Combination.lean

@@ -0,0 +1,48 @@
+import Mathlib.LinearAlgebra.AffineSpace.Combination
+
+variable {ι k V P : Type*} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P]
+    {p₀ : P} {p : ι → P} {w : ι → k} {s : Finset ι} {t : Set P}
+
+-- TODO: Replace
+lemma weightedVSub_mem_vectorSpan' (h : ∑ i ∈ s, w i = 0) (hp : ∀ i ∈ s, p i ∈ t) :
+    s.weightedVSub p w ∈ vectorSpan k t := by
+  obtain rfl | ⟨i, hi⟩ := s.eq_empty_or_nonempty
+  · simp
+  rw [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero s w p h (p i)]
+  simp
+  exact sum_mem fun j hj ↦ Submodule.smul_mem _ _ <| vsub_mem_vectorSpan _ (hp _ hj) (hp _ hi)
+
+-- TODO: Replace
+lemma affineCombination_mem_affineSpan' [Nontrivial k] (h : ∑ i ∈ s, w i = 1)
+    (hp : ∀ i ∈ s, p i ∈ t) : s.affineCombination k p w ∈ affineSpan k t := by
+  classical
+  have hnz : ∑ i ∈ s, w i ≠ 0 := h.symm ▸ one_ne_zero
+  have hn : s.Nonempty := Finset.nonempty_of_sum_ne_zero hnz
+  cases' hn with i1 hi1
+  let w1 : ι → k := Function.update (Function.const ι 0) i1 1
+  have hw1 : ∑ i ∈ s, w1 i = 1 := by
+    simp only [w1, Function.const_zero, Finset.sum_update_of_mem hi1, Pi.zero_apply,
+        Finset.sum_const_zero, add_zero]
+  have hw1s : s.affineCombination k p w1 = p i1 :=
+    s.affineCombination_of_eq_one_of_eq_zero w1 p hi1 (Function.update_self ..) fun _ _ hne =>
+      Function.update_of_ne hne ..
+  have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k t).direction := by
+    rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
+    apply weightedVSub_mem_vectorSpan' _ hp
+    simp [Pi.sub_apply, h, hw1]
+  rw [← vsub_vadd (s.affineCombination k p w) (p i1)]
+  exact AffineSubspace.vadd_mem_of_mem_direction hv (mem_affineSpan k <| hp _ hi1)
+
+lemma mem_affineSpan_image [Nontrivial k] :
+    p₀ ∈ affineSpan k (p '' s) ↔
+      ∃ w : ι → k, ∑ i ∈ s, w i = 1 ∧ p₀ = s.affineCombination k p w where
+  mp hp := by
+    classical
+    rw [← Subtype.range_val (s := s.toSet), ← Set.range_comp] at hp
+    obtain ⟨w, hw, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp
+    refine ⟨fun i ↦ if hi : i ∈ s then w ⟨i, hi⟩ else 0, ?_, ?_⟩
+    simp [Finset.sum_dite]
+    convert hw using 1
+    sorry
+    sorry
+  mpr := by rintro ⟨w, hw₁, rfl⟩; exact affineCombination_mem_affineSpan' hw₁ (by aesop)