Krein Milman for polytopes and FG cones

Polyhedral.lean

@@ -53,6 +53,7 @@ public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polyhedron.Lattice
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Basic
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Face
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Homogenization
+public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.KreinMilman
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Lattice
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Pointwise
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Basic
@@ -64,11 +65,11 @@ public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Lattice
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.WithTop
 public import Polyhedral.Mathlib.Geometry.Convex.Fun.Defs
 public import Polyhedral.Mathlib.Geometry.Convex.Fun.Dual
+public import Polyhedral.Mathlib.Geometry.Convex.Segment
 public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero
 public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.Closure
 public import Polyhedral.Mathlib.GroupTheory.GroupAction.SubMulActionWithZero.Nonneg
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
-public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Range
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.IsHomogenization
 public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Set

Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Finite/Face/KreinMilman.lean

@@ -1,19 +1,21 @@
 /-
-Copyright (c) 2025 Olivia Röhrig, Martin Winter. All rights reserved.
+Copyright (c) 2026 Moritz Firsching. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Olivia Röhrig, Martin Winter
+Authors: Moritz Firsching
 -/
 module
 
-public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.Face.Basic
+public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Homogenization
+public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.KreinMilman
 
 /-! In this file we prove the Krein-Milman theorem for FG cones: every finitely generated
 cone is spanned by its rays, that is, by the finite set of its 1-dimensional faces.
 
-TODO: aspects of the proof are rather cumbersome since the atoms of the face lattice are rays
-rather than points. We therefore intend to perform the proof on the polytope side and
-transfer it here using homogenization.
--/
+The theorem is derived from the Krein-Milman theorem for polytopes
+(`IsPolytope.krein_milman`): a salient FG cone admits a linear functional that is positive on
+all of its nonzero elements, the slice of the cone at weight one is a polytope, and the cone
+is the homogenization of that slice, so its rays are the homogenizations of the vertices of
+the slice. -/
 
 @[expose] public section
 
@@ -23,159 +25,21 @@ variable {R M : Type*}
 
 section Field
 
-variable [Field R] [LinearOrder R] [IsOrderedRing R]
+variable [Field R] [LinearOrder R] [IsStrictOrderedRing R]
 variable [AddCommGroup M] [Module R M]
 
-variable {C F F₁ F₂ : PointedCone R M}
-
-section opt
-
-/- The minimum of `f/g` on a cone. -/
-def opt (C : PointedCone R M) (f g : M →ₗ[R] R) : PointedCone R M where
-  carrier := {x ∈ C | ∀ y ∈ C, f x * g y ≤ f y * g x}
-  add_mem' := by
-    intro a b ha hb
-    simp only [Set.mem_ofPred_eq, map_add] at *
-    refine ⟨C.add_mem ha.1 hb.1, ?_⟩
-    intro y hy
-    rw [add_mul, mul_add]
-    exact add_le_add (ha.2 y hy) (hb.2 y hy)
-  zero_mem' := by simp only [Set.mem_ofPred_eq, zero_mem, map_zero, zero_mul, mul_zero, le_refl,
-     implies_true, and_self]
-  smul_mem' := by
-    intro a x hx
-    refine ⟨C.smul_mem a.2 hx.1, ?_⟩
-    intro y hy
-    by_cases! h : a ≤ 0
-    · simp [nonpos_iff_eq_zero.mp h]
-    simp only [LinearMap.map_smul_of_tower, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]
-    exact (smul_le_smul_iff_of_pos_left h).mpr <| hx.2 y hy
-
--- TODO: the proof was modified after features changed and needs golfing:
---  * `Salient.of_le_positive` was hacked in.
---  * `mem_positive'` was hacked in to recover the previous form of `hg`.
-lemma IsFaceOf.of_opt (C : PointedCone R M) (f g : M →ₗ[R] R) (hCg : C ≤ g.positive) :
-    (C.opt f g).IsFaceOf C := by
-  have hg : ∀ x ∈ C, 0 ≤ g x ∧ (g x = 0 → x = 0) := -- hacked in to recover `hg`
-    fun _ hx => g.mem_positive'.mp (hCg hx)
-  refine ⟨fun _ hx ↦ hx.1, ?_⟩
-  intro x y a hx hy ha ⟨h2, h⟩
-  by_cases! x_ne_0 : x = 0
-  · rw [x_ne_0]; exact zero_mem (C.opt f g)
-  by_cases! t_ne_0 : a • x + y = 0
-  · exfalso
-    have hC' := Salient.of_le_positive hCg
-    exact (smul_ne_zero (ne_of_gt ha) x_ne_0) <|
-      hC' (a • x) (C.smul_mem (le_of_lt ha) hx) y hy t_ne_0
-  refine ⟨hx, fun z hz ↦ ?_⟩
-  have : g x > 0 := lt_of_le_of_ne (hg _ hx).1 (fun h ↦ x_ne_0 <| (hg _ hx).2 (Eq.symm h))
-  have t1 := h x hx
-  have t2 := h y hy
-  have t4 := (mul_le_mul_iff_of_pos_left this).mpr <| (h z hz)
-  simp only [map_add, map_smul, smul_eq_mul] at t1 t2 t4
-  have local_lemma : ∀ {a b c d e : R}, e > 0 → a ≤ b → c ≤ d → e * a + c = e * b + d → a = b :=
-    fun _ _ _ _ ↦ by nlinarith
-  have t3 : (a * f x + f y) * g x = f x * (a * g x + g y) := local_lemma ha t1 t2 (by ring)
-  have : a * g x + g y > 0 := by
-    simpa only [gt_iff_lt, map_add, map_smul, smul_eq_mul] using
-      lt_of_le_of_ne (hg _ h2).1 (fun h ↦ t_ne_0 <| (hg _ h2).2 (Eq.symm h))
-  apply (mul_le_mul_iff_of_pos_left this).mp
-  nth_rw 3 [mul_comm] at t3
-  rw [← mul_assoc, ← t3]
-  linarith
-
-lemma FG.exists_ne_zero_mem_opt (C : PointedCone R M) (hC : C.FG) (hC0 : C ≠ ⊥) (f g : M →ₗ[R] R)
-    (hCg : C ≤ g.positive) : ∃ x, x ≠ 0 ∧ x ∈ C.opt f g := by classical
-  have hg : ∀ x ∈ C, 0 ≤ g x ∧ (g x = 0 → x = 0) := -- hacked in to recover `hg`
-    fun _ hx => g.mem_positive'.mp (hCg hx)
-  obtain ⟨s, hs⟩ := hC
-  have hs0 : ∃ z ∈ s, z ≠ 0 := by
-    by_contra hs0
-    push Not at hs0
-    exact hC0 <| by rw [← hs]; exact Submodule.span_eq_bot.mpr hs0
-  have hg_pos : ∀ {z : M}, z ∈ C → z ≠ 0 → 0 < g z := by
-    intro z hz hz0
-    exact lt_of_le_of_ne (hg _ hz).1 (fun h ↦ hz0 <| (hg _ hz).2 (Eq.symm h))
-  let s0 : Finset M := s.filter fun z => z ≠ 0
-  have hs0_ne : s0.Nonempty := by
-    rcases hs0 with ⟨z, hzs, hz0⟩
-    exact ⟨z, by simp [s0, hzs, hz0]⟩
-  obtain ⟨x, hx0, hxmin⟩ := Finset.exists_min_image s0 (fun z => f z / g z) hs0_ne
-  have hxs : x ∈ s := (Finset.mem_filter.mp hx0).1
-  have hx_ne_0 : x ≠ 0 := (Finset.mem_filter.mp hx0).2
-  have hxC : x ∈ C := by rw [← hs]; exact subset_hull hxs
-  have hgx : 0 < g x := hg_pos hxC hx_ne_0
-  have hgen : ∀ z ∈ s, f x * g z ≤ f z * g x := by
-    intro z hzs
-    by_cases hz0 : z = 0
-    · simp [hz0]
-    have hzC : z ∈ C := by rw [← hs]; exact subset_hull hzs
-    have hgz : 0 < g z := hg_pos hzC hz0
-    have hz0' : z ∈ s0 := by simp [s0, hzs, hz0]
-    exact (div_le_div_iff₀ hgx hgz).1 (hxmin _ hz0')
-  refine ⟨x, hx_ne_0, ?_⟩
-  refine ⟨hxC, ?_⟩
-  intro y hy
-  rw [← hs] at hy
-  induction hy using Submodule.span_induction with
-  | mem z hz => exact hgen z hz
-  | zero =>
-      simp
-  | add y z _ _ hy hz =>
-      simpa [map_add, add_mul, mul_add] using add_le_add hy hz
-  | smul a y _ hy =>
-      have hy' := mul_le_mul_of_nonneg_left hy a.2
-      simp only [LinearMap.map_smul_of_tower, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
-        ge_iff_le]
-      exact hy'
-
-lemma FG.opt_neq_bot (C : PointedCone R M) (hC : C.FG) (hC0 : C ≠ ⊥) (f g : M →ₗ[R] R)
-     (hCg : C ≤ g.positive) : C.opt f g ≠ ⊥ := by
-  rcases FG.exists_ne_zero_mem_opt C hC hC0 f g hCg with ⟨x, hx0, hxopt⟩
-  exact fun hbot => hx0 <| by simpa [hbot] using hxopt
-
-end opt
+variable {C : PointedCone R M}
 
-/- For every ray `x` of the span of a set `s`, there is a member of `s` that also spans the ray. -/
-lemma IsFaceOf.hull_ray {s : Set M} {x : M} (hx : x ≠ 0)
-    (hspan : (R ∙₊ x).IsFaceOf (hull R s)) : ∃ y ∈ s, ∃ c : R, 0 < c ∧ y = c • x := by
-  have h := hspan.hull_inter_face_hull_inf_face
-  have ⟨y, hy, hy0⟩ : ∃ w ∈ s ∩ (R ∙₊ x), w ≠ 0 := by
-    by_contra H
-    absurd hx
-    push Not at H
-    simp only [← Set.mem_singleton_iff] at H
-    simpa [h] using Submodule.span_mono (R := {c : R // 0 ≤ c}) H
-  simp only [Set.mem_inter_iff, SetLike.mem_coe, Submodule.mem_span_singleton,
-    Subtype.exists] at hy
-  obtain ⟨hys, a, ha, rfl⟩ := hy
-  exact ⟨_, hys, a, lt_of_le_of_ne ha (fun h => hy0 (by simp [← h])), rfl⟩
+open Convexity Affine Affine.IsHomogenization
 
-open Module in
 /-- Krein-Milman theorem: every finitely generated cone is spanned by its rays, that is,
 by the finite set of its 1-dimensional faces. -/
 lemma FG.krein_milman (hfg : C.FG) (hsal : C.Salient) :
     ∃ s : Finset M, hull R s = C ∧ ∀ x ∈ s, (R ∙₊ x).IsFaceOf C := by
   classical
-  let ⟨s, hs⟩ := hfg
-  by_cases hs' : s = ∅
-  · exact ⟨∅, by simp [← hs, hs']⟩
-  by_contra! h
-  let t := s.filter fun x => (R ∙₊ x).IsFaceOf C
-  specialize h t
-  have hts : t ⊆ s := by simp [t]
-  have hst : ¬(s : Set M) ⊆ hull R (t : Set M) := by
-    by_contra h'
-    have h' := Submodule.span_mono (R := {c : R // 0 ≤ c}) h'
-    have h'' := Submodule.span_mono (R := {c : R // 0 ≤ c}) hts
-    simp only [Submodule.span_coe_eq_restrictScalars, Submodule.restrictScalars_self] at h'
-    rw [← le_antisymm h' h'', hs] at h
-    simp [t, and_assoc] at h
-  obtain ⟨x, hxs, hxt⟩ := Set.not_subset.mp hst
-  have hx : x ∈ C := by
-    rw [← hs]
-    exact subset_hull hxs
-  obtain ⟨f, hf, hf'⟩ := FG.farkas (Dual.eval R M) hxt
+  by_cases hbot : C = ⊥
+  · exact ⟨∅, by simp [hbot]⟩
+  -- a linear functional that is positive on all nonzero elements of `C`
   obtain ⟨g, hg, hgker⟩ := IsExposedFaceOf.lineal hfg
   have hker : C ⊓ g.ker = ⊥ := by
     rw [← hgker]
@@ -188,50 +52,31 @@ lemma FG.krein_milman (hfg : C.FG) (hsal : C.Salient) :
     have : y ∈ C ⊓ g.ker := ⟨hy, hgy⟩
     rw [hker] at this
     simpa using this
-  simp only [Dual.eval_apply] at hf hf'
-  let F := C.opt f g
-  have hF : F.IsFaceOf C := IsFaceOf.of_opt C f g hgC
-  have hC0 : C ≠ ⊥ := by
-    intro hC0
-    have : x = 0 := by simpa [hC0] using hx
-    exact hxt (by simp [this])
-  have hF' := opt_neq_bot C hfg hC0 f g hgC
-  have hFsal := Salient.of_le_salient hsal hF.le
-  obtain ⟨r, hr0, hrF⟩ := exists_ray (hF.fg hfg) hF' hFsal
-  have hr := IsFaceOf.trans hrF hF
-  rw [← hs] at hr
-  obtain ⟨w, hws, c, hc', h⟩ := hr.hull_ray hr0
-  simp only [SetLike.mem_coe] at hws
-  have hc0 := (ne_of_lt hc').symm
-  have hrw : r = c⁻¹ • w := by
-    subst h hs
-    simp [smul_smul, hc0]
-  rw [hrw] at hr
-  rw [hull_singleton_smul_eq (inv_pos.mpr hc')] at hr
-  have hwt : w ∈ t := by
-    simpa [Finset.mem_filter, t] using ⟨hws, hs ▸ hr⟩
-  have hwF : r ∈ F := by
-    have : r ∈ hull R {r} := by simp
-    exact hrF.le this
-  have hwF : w ∈ F := by
-    rw [h]
-    exact F.smul_mem (le_of_lt hc') hwF
-  simp only [opt, Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk, Set.mem_ofPred_eq,
-    F] at hwF
-  have hgw : 0 < g w := by
-    have hw0 : w ≠ 0 := by
-      rw [h]
-      exact smul_ne_zero hc0 hr0
-    by_contra! h
-    have hgw := g.mem_positive'.mp (hgC hwF.1)
-    have hgw' := le_antisymm hgw.1 h
-    have := hgw.2 hgw'.symm
-    absurd hxt
-    contradiction
-  have hwF := hwF.2 x hx
-  have : 0 ≤ f w * g x := mul_nonneg (hf' w hwt) (g.mem_positive'.mp (hgC hx)).1
-  have : f x * g w < 0 := mul_neg_of_neg_of_pos hf hgw
-  linarith
+  -- the weight-one slice of `C` is nonempty
+  obtain ⟨y, hyC, hy0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hbot
+  have hg : g ≠ 0 := fun h ↦ hy0 <| by simpa [h] using (LinearMap.mem_positive'.mp (hgC hyC)).2
+  -- choose the homogenization whose affine space is the weight-one plane
+  let ℋ := IsHomogenization.ofWeightNeZero hg
+  -- view `C` as the homogenization of its weight-one slice
+  let weightOnePlane := AffineSubspace.comap (g.toAffineMap) {1}
+  have : Nonempty weightOnePlane :=
+    Function.Surjective.nonempty (Set.restrictPreimage_surjective {1} (g.surjective_of_ne_zero hg))
+  let : ConvexSpace R weightOnePlane := .ofAddTorsor
+  let : ConvexSpace R M := .ofModule
+  have hCP : homogenize ℋ (dehomogenize ℋ C) = C :=
+    homogenize_dehomogenize_of_le_positive ((weight_ofWeightNeZero hg).symm ▸ hgC)
+  -- the slice is a polytope; apply the Krein-Milman theorem for polytopes
+  have hP : IsPolytope R (dehomogenize ℋ C : Set weightOnePlane) := by
+    rw [IsPolytope.iff_homogenize_fg (W := M), hCP]
+    · exact hfg
+    · exact dehomogenize_isConvexSet ℋ C
+  obtain ⟨s, hs, hface⟩ := IsPolytope.krein_milman hP
+  refine ⟨s.image ℋ.ofPoint, ?_, ?_⟩
+  · rw [Finset.coe_image, hull_image_ofPoint_eq_homogenize_convexHull, hs, hCP]
+  · intro x hx
+    obtain ⟨q, hq, rfl⟩ := Finset.mem_image.mp hx
+    have h := homogenize_isFaceOf ℋ (dehomogenize_isConvexSet ℋ C) (hface q hq)
+    rwa [homogenize_singleton, hCP] at h
 
 end Field
 

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Order.lean

@@ -115,7 +115,7 @@ lemma upperMass_eq_one_iff : w.upperMass x = 1 ↔ ∀ y, w.weights y ≠ 0 →
   refine ⟨fun h1 y hy ↦ ?_, fun hall ↦ ?_⟩
   · rw [h1] at h
     have hz := add_left_cancel (h.trans (add_zero 1).symm)
-    by_contra! hxy
+    by_contra hxy
     exact hy <| (Finset.sum_eq_zero_iff_of_nonneg fun _ _ ↦ w.weights_nonneg _).1 hz y <| by
       simp [hy, hxy]
   · rwa [Finset.sum_eq_zero fun y ↦ by simp +contextual [hall], add_zero] at h

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polyhedron/Lattice.lean

@@ -17,7 +17,7 @@ namespace Convexity
 open Convexity
 
 variable {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
-variable {V : Type*} [AddCommGroup V] [Module R V] -- [ConvexSpace R V] [IsModuleConvexSpace R V]
+variable {V : Type*} [AddCommGroup V] [Module R V]
 variable {A : Type*} [AddTorsor V A] [ConvexSpace R A]
 
 variable (R A) in
@@ -50,11 +50,6 @@ section IsModuleConvexSpace
 
 variable [ConvexSpace R V] [IsModuleConvexSpace R V] [IsAffineConvexSpace R V A]
 
-@[coe] def toConvexSet (P : Polyhedron R A) : ConvexSet R A :=
-  ⟨P, P.isPolyhedron.isConvexSet⟩
-
-instance : Coe (Polyhedron R A) (ConvexSet R A) := ⟨toConvexSet⟩
-
 end IsModuleConvexSpace
 
 /- # LE -/

Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Polytope/Face.lean

@@ -7,6 +7,7 @@ module
 
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Lattice
 public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Homogenization
+public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Face.Lattice
 
 import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Finite.Face.Grade
 import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Homogenization
@@ -18,28 +19,30 @@ public section
 
 variable {R V A : Type*}
 
-open Convexity ConvexSet Affine
+open Convexity IsConvexSet Affine
+
+namespace Convexity
 
 section Field
 
 variable [Field R] [LinearOrder R] [IsStrictOrderedRing R]
 variable [AddCommGroup V] [Module R V]
 variable [AddTorsor V A] [ConvexSpace R A] [IsAffineConvexSpace R V A]
 
-variable {C F : ConvexSet R A}
+variable {C F : Set A}
 
 include V in
 /-- Faces of polytopes are polytopes. -/
-theorem IsPolytope.face_isPolytope (hC : IsPolytope R (C : Set A)) (hF : IsFaceOf F C) :
+theorem IsPolytope.face_isPolytope (hC : IsPolytope R C) (hF : IsFaceOf R F C) :
     IsPolytope R (F : Set A) := by
   let : ConvexSpace R (Homogenization R A) := ConvexSpace.ofModule
-  have homF := (IsHomogenization.canonical R A).homogenize_isFaceOf hF
+  have homF := (IsHomogenization.canonical R A).homogenize_isFaceOf hC.isConvexSet hF
   have := PointedCone.IsFaceOf.fg (IsPolytope.homogenize_fg _ hC) homF
   convert FG.dehomogenize_isPolytope this (fun _ a b ↦ weight_pos_of_mem_homogenize a b)
-  simp [dehomogenize_homogenize]
+  rw [dehomogenize_homogenize _  hF.isConvexSet]
 
 include V in
-instance {P : Polytope R A} : CoeOut (Face (P : ConvexSet R A)) (Polytope R A) where
+instance {P : Polytope R A} : CoeOut (Face P.isPolytope.isConvexSet) (Polytope R A) where
   coe F := ⟨_, IsPolytope.face_isPolytope P.isPolytope F.isFaceOf⟩
 
 include V in
@@ -49,12 +52,14 @@ homogenization cones.
 This is private since it does not yet have the correct grading (off-by-one).
 -/
 private noncomputable instance Polytope.faceHomogenizationGradeOrder (P : Polytope R A) :
-    GradeOrder ℕ (Face (P : ConvexSet R A)) := by
+    GradeOrder ℕ (Face P.isPolytope.isConvexSet) := by
   let : ConvexSpace R (Homogenization R A) := ConvexSpace.ofModule
   let ℋ := IsHomogenization.canonical R A
-  have : (homogenize _ (P : ConvexSet R A)).FG := IsPolytope.homogenize_fg ℋ P.isPolytope
+  have : (homogenize _ P).FG := IsPolytope.homogenize_fg ℋ P.isPolytope
   let := PointedCone.FG.gradeOrder_finrank this
-  refine GradeOrder.liftRight _ (face_homogenizeIso ℋ P).strictMono ?_
+  refine GradeOrder.liftRight _ (face_homogenizeIso ℋ P.isPolytope.isConvexSet).strictMono ?_
   exact fun x y ↦ (apply_covBy_apply_iff _).mpr
 
 end Field
+
+end Convexity