From 9f078d888c76a6fd65c4315ab9715b355190d9b5 Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Fri, 16 Oct 2026 08:52:18 +0200 Subject: [PATCH 1/4] Bump mathlib --- Polyhedral.lean | 2 - .../Group/Pointwise/SetLike/Basic.lean | 2 +- .../Mathlib/Data/SetLike/IsConcrete.lean | 2 +- .../Geometry/Convex/Cone/Pointed/Basic.lean | 2 +- .../Convex/Cone/Pointed/DualClosed.lean | 2 +- .../Geometry/Convex/Cone/Pointed/Lineal.lean | 2 +- .../Geometry/Convex/Cone/Pointed/Rank.lean | 2 +- .../Convex/ConvexSpace/AffineSpace.lean | 7 -- .../Convex/ConvexSpace/Homogenization.lean | 1 - .../Convex/ConvexSpace/Set/Face/Basic.lean | 4 +- .../ConvexSpace/Set/Face/Homogenization.lean | 2 +- .../ConvexSpace/Set/Homogenization.lean | 2 +- .../Mathlib/Geometry/Convex/Fun/Defs.lean | 21 +++-- .../AffineSpace/AffineSubspace/Defs.lean | 77 ------------------- .../LinearAlgebra/AffineSpace/Dimension.lean | 28 ------- .../AffineSpace/Homogenization/Set.lean | 2 +- lake-manifest.json | 32 ++++---- lakefile.toml | 2 +- lean-toolchain | 2 +- 19 files changed, 44 insertions(+), 150 deletions(-) delete mode 100644 Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean delete mode 100644 Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Dimension.lean diff --git a/Polyhedral.lean b/Polyhedral.lean index 1b028e43..242f3273 100644 --- a/Polyhedral.lean +++ b/Polyhedral.lean @@ -68,10 +68,8 @@ 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.Defs public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Range public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Defs -public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Dimension public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.IsHomogenization public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.Set public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Lattice diff --git a/Polyhedral/Mathlib/Algebra/Group/Pointwise/SetLike/Basic.lean b/Polyhedral/Mathlib/Algebra/Group/Pointwise/SetLike/Basic.lean index 68738acf..457959b3 100644 --- a/Polyhedral/Mathlib/Algebra/Group/Pointwise/SetLike/Basic.lean +++ b/Polyhedral/Mathlib/Algebra/Group/Pointwise/SetLike/Basic.lean @@ -12,7 +12,7 @@ import Mathlib.Algebra.Group.Equiv.Basic import Mathlib.Algebra.Group.Prod import Mathlib.Algebra.Order.Monoid.Unbundled.Pow import Mathlib.Data.Set.NAry -import Mathlib.Data.SetLike.Basic +import Mathlib.Basic.SetLike.Basic import Mathlib.Algebra.Group.Defs /-! This files defines the pointwise operations on `SetLike` that are inherited from `Set`-/ diff --git a/Polyhedral/Mathlib/Data/SetLike/IsConcrete.lean b/Polyhedral/Mathlib/Data/SetLike/IsConcrete.lean index bbdcaa81..a1b3202f 100644 --- a/Polyhedral/Mathlib/Data/SetLike/IsConcrete.lean +++ b/Polyhedral/Mathlib/Data/SetLike/IsConcrete.lean @@ -5,7 +5,7 @@ Authors: Martin Winter -/ module -public import Mathlib.Data.SetLike.Basic +public import Mathlib.Basic.SetLike.Basic public import Mathlib.Order.CompleteLattice.Defs import Mathlib.Data.Set.Basic diff --git a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Basic.lean b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Basic.lean index 04c48d3c..e1666b5e 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Basic.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Basic.lean @@ -10,7 +10,7 @@ public import Polyhedral.Mathlib.Algebra.Module.Submodule.Basic public import Mathlib.Algebra.Order.Nonneg.Basic import Mathlib.RingTheory.LocalRing.Basic -import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs +import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs /-! This file proves basic facts about cones that are intended to go into Pointed/Basic. -/ diff --git a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/DualClosed.lean b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/DualClosed.lean index e7a6da68..24ba751d 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/DualClosed.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/DualClosed.lean @@ -215,7 +215,7 @@ lemma dual_eq_bot_iff_forall_eq_zero_or_exists_neg : lemma dual_dual_eq_top_iff_exists_ne_zero_forall_nonneg : dual p.flip (dual p C) ≠ ⊤ ↔ ∃ φ : N, p.flip φ ≠ 0 ∧ ∀ x ∈ C, 0 ≤ p x φ := by constructor <;> intro h - · obtain ⟨x, hx⟩ := SetLike.exists_not_mem_of_ne_top _ h + · obtain ⟨x, hx⟩ := SetLike.exists_notMem_of_ne_top _ h obtain ⟨φ, hxφ, hφ⟩ := farkas (dual_dualClosed _ _) hx use φ constructor diff --git a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Lineal.lean b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Lineal.lean index d19b0569..5a302100 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Lineal.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Lineal.lean @@ -148,7 +148,7 @@ lemma span_inf_of_codisjoint_lineal {S : Submodule R M} (hS : Codisjoint C.linea span R (C ⊓ S : PointedCone R M) = span R C ⊓ S := by nth_rw 2 [← C.inf_sup_lineal hS] rw [← coe_sup_submodule_span, Submodule.span_union, coe_ofSubmodule, Submodule.span_eq C.lineal] - rw [sup_inf_assoc_of_le C.lineal (Submodule.span_le.mpr fun _ hx ↦ hx.2)] + rw [sup_inf_assoc_of_le C.lineal (Submodule.span_le.mpr (by simp))] rw [Eq.comm, sup_eq_left] intro x hx apply Submodule.subset_span diff --git a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Rank.lean b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Rank.lean index 2f29405d..545cd488 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Rank.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Rank.lean @@ -7,7 +7,7 @@ module public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Lineal public import Polyhedral.Mathlib.Algebra.Module.Submodule.Dual.Field -public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Dimension +public import Mathlib.LinearAlgebra.AffineSpace.Dimension /-! ## Rank of Pointed Cones diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean index c263a792..4c7b3b09 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean @@ -35,13 +35,6 @@ variable [ConvexSpace R P₁] [IsAffineConvexSpace R V₁ P₁] variable [ConvexSpace R P₂] [IsAffineConvexSpace R V₂ P₂] variable (f : P₁ →ᵃ[R] P₂) --- PR #39437 -lemma isAffineMap : IsAffineMap R f where - map_sConvexComb s := by - rw [sConvexComb_eq_affineCombination, sConvexComb_map, iConvexComb_eq_affineCombination] - simpa only [Function.comp_id] using - map_affineCombination (s := s.weights.support) _root_.id s.weights s.total f - @[simp] lemma map_sConvexComb (w : StdSimplex R P₁) : f (sConvexComb w) = sConvexComb (w.map f) := f.isAffineMap.map_sConvexComb w diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean index 5ae1ad42..f769df9a 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Homogenization.lean @@ -79,7 +79,6 @@ variable (hom) in embedding of the set. -/ theorem image_hull_eq_convexHull_image {s : Set A} : ℋ.ofPoint '' Convexity.convexHull R s ⊆ hull R (ℋ.ofPoint '' s) := by - apply Set.image_subset_iff.mp rw [ℋ.ofPoint.isAffineMap.image_convexHull] simpa using (hull R _).isConvexSet.convexHull_subset_iff.mpr subset_hull diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Basic.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Basic.lean index 4f7f5062..9ba2a405 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Basic.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Basic.lean @@ -170,9 +170,7 @@ theorem isFaceOf_map_iff {f : M₁ → M₂} {F C : ConvexSet R M₁} (hhf : IsA rw [hf hzy] at hy use hy · intro hz - have hhz : f z ∈ (A.map hhf) := by - use z, hz - apply Set.mem_preimage.mp hhz + exact ⟨z, hz, rfl⟩ rw [h F, h C] at hh exact hh · intro h diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean index 1bc03668..a128565b 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Face/Homogenization.lean @@ -11,7 +11,7 @@ public import Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Set.Homogenization /-! This files proves results about faces of convex sets / cones and homogenization. -/ -@[expose] public section +@[expose] public noncomputable section namespace Affine.IsHomogenization diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean index 1e97a99d..7d1f138d 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean @@ -11,7 +11,7 @@ public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.Homogenization.IsHomo /-! This file defines homogenization of convex sets in affine spaces. -/ -@[expose] public section +@[expose] public noncomputable section open Convexity Pointwise Set PointedCone Submodule diff --git a/Polyhedral/Mathlib/Geometry/Convex/Fun/Defs.lean b/Polyhedral/Mathlib/Geometry/Convex/Fun/Defs.lean index d08cb00d..bdf6f2bd 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/Fun/Defs.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/Fun/Defs.lean @@ -98,15 +98,26 @@ lemma IsConvexFunOn.map_iConvexComb_le (hf : IsConvexFunOn R s f) {w : StdSimple grw [StdSimplex.weights_map, mapDomain_support] simpa [Set.subset_def] -@[to_dual (dont_translate := R) le_map_convexCombPair] -lemma IsConvexFunOn.map_convexCombPair_le (hf : IsConvexFunOn R s f) (hx : x ∈ s) (hy : y ∈ s) - {a b : R} {ha hb hab} : - f (convexCombPair a b ha hb hab x y) ≤ convexCombPair a b ha hb hab (f x) (f y) := by +omit [ConvexSpace R X] in +private lemma support_duple_subset (hx : x ∈ s) (hy : y ∈ s) {a b : R} {ha : 0 ≤ a} {hb : 0 ≤ b} + {hab : a + b = 1} : + ↑(StdSimplex.duple x y ha hb hab).weights.support ⊆ s := by classical - grw [convexCombPair, hf.map_sConvexComb_le, iConvexComb_duple] grw [StdSimplex.weights_duple, support_add, support_single_subset, support_single_subset] simp [Set.subset_def, *] +lemma IsConvexFunOn.map_convexCombPair_le (hf : IsConvexFunOn R s f) (hx : x ∈ s) (hy : y ∈ s) + {a b : R} {ha hb hab} : + f (convexCombPair a b ha hb hab x y) ≤ convexCombPair a b ha hb hab (f x) (f y) := by + rw [convexCombPair, ← iConvexComb_duple] + exact hf.map_sConvexComb_le (support_duple_subset hx hy) + +lemma IsConcaveFunOn.le_map_convexCombPair (hf : IsConcaveFunOn R s f) (hx : x ∈ s) (hy : y ∈ s) + {a b : R} {ha hb hab} : + convexCombPair a b ha hb hab (f x) (f y) ≤ f (convexCombPair a b ha hb hab x y) := by + rw [← iConvexComb_duple, convexCombPair] + exact hf.le_map_sConvexComb (support_duple_subset hx hy) + @[to_dual (attr := simp)] protected lemma IsConvexFunOn.empty : IsConvexFunOn R (∅ : Set X) f := by simp [IsConvexFunOn] diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean deleted file mode 100644 index 12ac350b..00000000 --- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean +++ /dev/null @@ -1,77 +0,0 @@ -/- -Copyright (c) 2026 Vlad Tsyrklevich. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Vlad Tsyrklevich --/ -module - -public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs - -/-! AffineSpace lemmas -/ - -@[expose] public section - -open Set -open scoped Pointwise - -namespace Submodule - -variable {k V : Type*} [Ring k] [AddCommGroup V] [Module k V] - -@[simp] -theorem coe_toAffineSubspace (p : Submodule k V) : (p.toAffineSubspace : Set V) = (p : Set V) := - rfl - -/-- Reinterprets a `p : AffineSubspace k V` that includes `0` as a `Submodule k V`. -/ -def ofAffineSubspace {p : AffineSubspace k V} (hp : 0 ∈ p) : Submodule k V where - carrier := p - add_mem' ha hb := by simpa using p.smul_vsub_vadd_mem' 1 ha hp hb - zero_mem' := by simpa - smul_mem' c x hx := by simpa using p.smul_vsub_vadd_mem' c hx hp hp - -@[simp] -theorem ofAffineSubspace_toAffineSubspace {p : AffineSubspace k V} (hp : 0 ∈ p) : - ↑(ofAffineSubspace hp) = p := rfl - -@[simp] -theorem toAffineSubspace_ofAffineSubspace {p : Submodule k V} : - ofAffineSubspace (mem_toAffineSubspace.mpr p.zero_mem) = p := rfl - -instance : CanLift (AffineSubspace k V) (Submodule k V) toAffineSubspace (0 ∈ ·) where - prf _ hp := ⟨ofAffineSubspace hp, ofAffineSubspace_toAffineSubspace hp⟩ - -end Submodule - -namespace AffineSubspace - -variable {k V : Type*} [Ring k] [AddCommGroup V] [Module k V] - -@[simp] -theorem toAffineSubspace_ne_bot (p : Submodule k V) : p.toAffineSubspace ≠ ⊥ := - (AffineSubspace.nonempty_iff_ne_bot _).mp ⟨0, p.zero_mem⟩ - -end AffineSubspace - -section AffineSpace' - -variable {k : Type*} {V : Type*} [Ring k] [AddCommGroup V] [Module k V] - --- TODO: Delete once mathlib PR #43582 lands -@[simp] -lemma affineSpan_insert_zero' (s : Set V) : - affineSpan k (insert 0 s) = Submodule.span k s := by - rw [AffineSubspace.ext_iff, ← Submodule.span_insert_zero] - refine affineSpan_subset_span.antisymm ?_ - rw [← vectorSpan_add_self, vectorSpan_def] - refine Subset.trans ?_ <| subset_add_left _ <| mem_insert .. - gcongr - exact subset_sub_left <| mem_insert .. - -theorem affineSpan_eq_span_iff_zero_mem {s : Set V} : - affineSpan k s = ↑(Submodule.span k s) ↔ 0 ∈ affineSpan k s := by - refine ⟨by simp +contextual, fun h ↦ ?_⟩ - rw [← affineSpan_insert_eq_affineSpan _ h, affineSpan_insert_zero'] - -alias ⟨_, affineSpan_eq_span_of_zero_mem⟩ := affineSpan_eq_span_iff_zero_mem - -end AffineSpace' diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Dimension.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Dimension.lean deleted file mode 100644 index 689d326d..00000000 --- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Dimension.lean +++ /dev/null @@ -1,28 +0,0 @@ -/- -Copyright (c) 2026 Vlad Tsyrklevich. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Vlad Tsyrklevich --/ -module - -public import Mathlib.LinearAlgebra.AffineSpace.Dimension -public import Polyhedral.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs - -/-! Dimension lemmas -/ - -@[expose] public section - -namespace AffineSubspace - -variable {R V : Type*} [Ring R] [AddCommGroup V] [Module R V] - -@[simp] -theorem dim_toAffineSubspace (s : Submodule R V) : s.toAffineSubspace.dim = Module.rank R s := by - rw [dim_eq_rank (toAffineSubspace_ne_bot _), Submodule.toAffineSubspace_direction] - -@[simp] -theorem finDim_toAffineSubspace (s : Submodule R V) : - s.toAffineSubspace.finDim = Module.finrank R s := by - rw [finDim_eq_finrank (toAffineSubspace_ne_bot _), Submodule.toAffineSubspace_direction] - -end AffineSubspace diff --git a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Set.lean b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Set.lean index 90544aac..211493cd 100644 --- a/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Set.lean +++ b/Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Homogenization/Set.lean @@ -17,7 +17,7 @@ import Mathlib.Algebra.Order.Nonneg.Field In particular, the homogenization is never empty. This enables to prove suitable order isomorphisms. -/ -@[expose] public section +@[expose] public noncomputable section namespace Affine.Set diff --git a/lake-manifest.json b/lake-manifest.json index aa8a271a..4810c658 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,11 @@ -{"version": "1.2.0", +{"version": "1.3.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ebec2b1d5b20a5ebf551798df78b13f2688a6e70", + "rev": "cfc55fc58714a59dc06e6e79edc6d1d95140d3c2", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d736b237948ab1bdf316407a575f0d3c7f6ba772", + "rev": "0e1ffe2e4ba5ecfdfaf15c65b8d3805dbb7134ae", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.35.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/PatrickMassot/checkdecls.git", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e50948299c4dc4a4c21b1c34b6a6a4fddc19f912", + "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "95e037bfdc31d3916ac615446847fb01960e2719", + "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f8e94c24111148c9ad1b866212a6e1a0fabb5e76", + "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4c70ac059693669e5756e32a7a94b57ee1e99dc5", + "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "75d936c7af167cc93fac0d31237682fc2204591d", + "rev": "4a174c490d8707121c4a9290800489f105d85e07", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "786b7acdca7eb4e9c76c5d1d5bd810e7e5c56334", + "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "167242e0621ba382fd6f7b2a7e932ce0811f9ab1", + "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,7 +105,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "0d36e6d34f6861ed37185646b2e5d7a9eff46281", + "rev": "4ed2f27ecf81792abc8ff848670ac4356d0c4794", "name": "leansqlite", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,17 +115,17 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "2842b9871b04862f944c032e34052cb9448ccb71", + "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.35.0-rc2", + "inputRev": "v4.35.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, "scope": "", - "rev": "1daff5db5b332b2aa094cecd6b6fea657ef9ced4", + "rev": "6e48acac3a91665fcdc4a20d50b7ce6b7b41711f", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -135,7 +135,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d73123f5b70ae67d3650bfea3b74faf4eaee2cfc", + "rev": "876b844aa52183cbcc0d82fdd4d1fc349f0dac34", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/lakefile.toml b/lakefile.toml index 4264471b..46589029 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -19,7 +19,7 @@ git = "https://github.com/PatrickMassot/checkdecls.git" [[require]] name = "«doc-gen4»" git = "https://github.com/leanprover/doc-gen4" -rev = "main" +rev = "v4.35.0" [[require]] name = "mathlib" diff --git a/lean-toolchain b/lean-toolchain index 15b914d9..a6aff065 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.35.0-rc2 \ No newline at end of file +leanprover/lean4:v4.35.0 From ab05c7e461a816d51354c946fb7d1a0467782c07 Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Fri, 16 Oct 2026 13:30:59 +0200 Subject: [PATCH 2/4] Yael review feedback --- .../Geometry/Convex/AffineMap/Module.lean | 20 +------------------ .../Geometry/Convex/Cone/Pointed/Rank.lean | 6 +++--- .../Convex/ConvexSpace/AffineSpace.lean | 20 ------------------- .../ConvexSpace/Set/Homogenization.lean | 2 +- Polyhedral/Mathlib/Geometry/Convex/Hull.lean | 2 +- Polyhedral/Mathlib/Geometry/Convex/Set.lean | 2 +- 6 files changed, 7 insertions(+), 45 deletions(-) diff --git a/Polyhedral/Mathlib/Geometry/Convex/AffineMap/Module.lean b/Polyhedral/Mathlib/Geometry/Convex/AffineMap/Module.lean index e4cc6984..0c7c5c50 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/AffineMap/Module.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/AffineMap/Module.lean @@ -8,28 +8,10 @@ public section open Convexity open scoped Pointwise -namespace LinearMap -variable {R M N : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] - [Module R M] [AddCommMonoid N] [Module R N] [ConvexSpace R M] [IsModuleConvexSpace R M] - [ConvexSpace R N] [IsModuleConvexSpace R N] (f : M →ₗ[R] N) - -alias isAffineMap := IsAffineMap.linearMap - -@[simp] lemma map_sConvexComb (w : StdSimplex R M) : - f (sConvexComb w) = sConvexComb (w.map f) := f.isAffineMap.map_sConvexComb w - -lemma isConvexSet_image {s : Set M} (hs : IsConvexSet R s) : IsConvexSet R (f '' s) := - hs.image f.isAffineMap - -lemma isConvexSet_range : IsConvexSet R (Set.range f) := by - rw [← Set.image_univ] - exact isConvexSet_image f .univ - -end LinearMap - namespace Convexity variable {R S M : Type*} +alias _root_.LinearMap.isAffineMap := IsAffineMap.linearMap section Semiring variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] diff --git a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Rank.lean b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Rank.lean index 545cd488..138fa578 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Rank.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/Cone/Pointed/Rank.lean @@ -1,13 +1,13 @@ /- -Copyright (c) 2025 Olivia Röhig, Kilian Rueß, Mrtin Winter. All rights reserved. +Copyright (c) 2025 Olivia Röhig, Kilian Rueß, Martin Winter. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Olivia Röhig, Kilian Rueß, Mrtin Winter +Authors: Olivia Röhig, Kilian Rueß, Martin Winter -/ module +public import Mathlib.LinearAlgebra.AffineSpace.Dimension public import Polyhedral.Mathlib.Geometry.Convex.Cone.Pointed.Lineal public import Polyhedral.Mathlib.Algebra.Module.Submodule.Dual.Field -public import Mathlib.LinearAlgebra.AffineSpace.Dimension /-! ## Rank of Pointed Cones diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean index 4c7b3b09..4c4338cb 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean @@ -26,26 +26,6 @@ public section open Convexity Finset AddTorsor open scoped Pointwise -namespace AffineMap -variable {R V₁ V₂ P₁ P₂ : Type*} -variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R] -variable [AddCommGroup V₁] [Module R V₁] [AddTorsor V₁ P₁] -variable [AddCommGroup V₂] [Module R V₂] [AddTorsor V₂ P₂] -variable [ConvexSpace R P₁] [IsAffineConvexSpace R V₁ P₁] -variable [ConvexSpace R P₂] [IsAffineConvexSpace R V₂ P₂] -variable (f : P₁ →ᵃ[R] P₂) - -@[simp] lemma map_sConvexComb (w : StdSimplex R P₁) : - f (sConvexComb w) = sConvexComb (w.map f) := f.isAffineMap.map_sConvexComb w - -lemma isConvexSet_image {s : Set P₁} (hs : IsConvexSet R s) : IsConvexSet R (f '' s) := - hs.image f.isAffineMap - -lemma isConvexSet_range : IsConvexSet R (Set.range f) := by - simpa using f.isConvexSet_image .univ - -end AffineMap - namespace Convexity variable {R V P I : Type*} variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R] diff --git a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean index 7d1f138d..2504afbb 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/ConvexSpace/Set/Homogenization.lean @@ -228,7 +228,7 @@ theorem homogenize_dehomogenize_of_le_positive {C : PointedCone R W} simpa [y', ℋ.ofPoint_range_eq_comap_weight_one] using inv_mul_cancel₀ (@hC y hyC hy0).ne.symm exact ⟨y', hy'C, hy'⟩ - · exact C.isConvexSet.inter ℋ.ofPoint.isConvexSet_range + · exact C.isConvexSet.inter (.range ℋ.ofPoint.isAffineMap) lemma homogenize_mono_iff {K₁ K₂ : ConvexSet R A} : K₁.homogenize ℋ ≤ K₂.homogenize ℋ ↔ K₁ ≤ K₂ where diff --git a/Polyhedral/Mathlib/Geometry/Convex/Hull.lean b/Polyhedral/Mathlib/Geometry/Convex/Hull.lean index ab996cbe..d33144a1 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/Hull.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/Hull.lean @@ -31,7 +31,7 @@ For finite `ι`, this can be interpreted as saying that a polytope is the image simplex under some affine map. -/ lemma convexHull_range (f : ι → X) : convexHull R (.range f) = .range (fun w : StdSimplex R ι ↦ iConvexComb w f) := by - refine (convexHull_min ?_ isAffineMap_iConvexComb.isConvexSet_range).antisymm ?_ + refine (convexHull_min ?_ (.range isAffineMap_iConvexComb)).antisymm ?_ · rintro _ ⟨i, rfl⟩ exact ⟨.single i, by simp⟩ · rintro _ ⟨w, rfl⟩ diff --git a/Polyhedral/Mathlib/Geometry/Convex/Set.lean b/Polyhedral/Mathlib/Geometry/Convex/Set.lean index e110cc5b..3ef6a3ac 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/Set.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/Set.lean @@ -10,7 +10,7 @@ variable {R X Y Z : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] [ConvexSpace R Y] [ConvexSpace R Z] {f : X → Y} {s : Set X} {t : Set Y} /-- The range of an affine map between convex spaces is convex. -/ -lemma IsAffineMap.isConvexSet_range (hf : IsAffineMap R f) : +lemma IsConvexSet.range (hf : IsAffineMap R f) : IsConvexSet R (.range f) := by simpa using IsConvexSet.univ.image hf protected lemma IsConvexSet.image2 {f : X → Y → Z} (hf : IsAffineMap R ↿f) From 1044a31bc72000f0a1988650a1f847fc62797b08 Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Fri, 16 Oct 2026 23:35:05 +0200 Subject: [PATCH 3/4] revert back to @[to_dual (dont_translate)] --- .../Mathlib/Geometry/Convex/Fun/Defs.lean | 27 ++++++------------- 1 file changed, 8 insertions(+), 19 deletions(-) diff --git a/Polyhedral/Mathlib/Geometry/Convex/Fun/Defs.lean b/Polyhedral/Mathlib/Geometry/Convex/Fun/Defs.lean index bdf6f2bd..527d0ebe 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/Fun/Defs.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/Fun/Defs.lean @@ -53,7 +53,7 @@ See `IsConvexFunOn.of_map_convexCombPair_le`. Under mild assumptions, convexity of the function `f` implies convexity of the set `s`. See `IsConvexFunOn.isConvexSet`. -/ -@[to_dual IsConcaveFunOn +@[to_dual (dont_translate := R) IsConcaveFunOn /-- A function `f : X → Y` from a convex space to an ordered convex space is concave on a set `s` if its hypograph `{(x, y) : X × Y | x ∈ s ∧ y ≤ f x}` is a convex set. @@ -64,7 +64,7 @@ Under mild assumptions, concavity of the function `f` implies convexity of the s See `IsConcaveFunOn.isConvexSet`. -/] def IsConvexFunOn : Prop := IsConvexSet R {(x, y) : X × Y | x ∈ s ∧ f x ≤ y} -@[to_dual] +@[to_dual (dont_translate := R)] lemma IsConvexFunOn.isConvexSet_epigraph (hf : IsConvexFunOn R s f) : IsConvexSet R {(x, y) : X × Y | x ∈ s ∧ f x ≤ y} := hf @@ -80,7 +80,7 @@ lemma IsConvexFunOn.isConvexSet (hf : IsConvexFunOn R s f) : IsConvexSet R s := grw [StdSimplex.weights_map, mapDomain_support]; simpa simpa [Function.comp_def] using (hf.isConvexSet_epigraph.sConvexComb_mem this).1 -@[to_dual le_map_sConvexComb] +@[to_dual (dont_translate := R) le_map_sConvexComb] lemma IsConvexFunOn.map_sConvexComb_le (hf : IsConvexFunOn R s f) {w : StdSimplex R X} (hw : ↑w.weights.support ⊆ s) : f w.sConvexComb ≤ w.iConvexComb f := by @@ -98,25 +98,14 @@ lemma IsConvexFunOn.map_iConvexComb_le (hf : IsConvexFunOn R s f) {w : StdSimple grw [StdSimplex.weights_map, mapDomain_support] simpa [Set.subset_def] -omit [ConvexSpace R X] in -private lemma support_duple_subset (hx : x ∈ s) (hy : y ∈ s) {a b : R} {ha : 0 ≤ a} {hb : 0 ≤ b} - {hab : a + b = 1} : - ↑(StdSimplex.duple x y ha hb hab).weights.support ⊆ s := by - classical - grw [StdSimplex.weights_duple, support_add, support_single_subset, support_single_subset] - simp [Set.subset_def, *] - +@[to_dual (dont_translate := R) le_map_convexCombPair] lemma IsConvexFunOn.map_convexCombPair_le (hf : IsConvexFunOn R s f) (hx : x ∈ s) (hy : y ∈ s) {a b : R} {ha hb hab} : f (convexCombPair a b ha hb hab x y) ≤ convexCombPair a b ha hb hab (f x) (f y) := by - rw [convexCombPair, ← iConvexComb_duple] - exact hf.map_sConvexComb_le (support_duple_subset hx hy) - -lemma IsConcaveFunOn.le_map_convexCombPair (hf : IsConcaveFunOn R s f) (hx : x ∈ s) (hy : y ∈ s) - {a b : R} {ha hb hab} : - convexCombPair a b ha hb hab (f x) (f y) ≤ f (convexCombPair a b ha hb hab x y) := by - rw [← iConvexComb_duple, convexCombPair] - exact hf.le_map_sConvexComb (support_duple_subset hx hy) + classical + grw [convexCombPair, hf.map_sConvexComb_le, iConvexComb_duple] + grw [StdSimplex.weights_duple, support_add, support_single_subset, support_single_subset] + simp [Set.subset_def, *] @[to_dual (attr := simp)] protected lemma IsConvexFunOn.empty : IsConvexFunOn R (∅ : Set X) f := by simp [IsConvexFunOn] From 6aa893b64fcb6202c5a4c895ab732c6d1c90174e Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Tue, 20 Oct 2026 17:24:23 +0200 Subject: [PATCH 4/4] Olivia review --- Polyhedral/Mathlib/Geometry/Convex/AffineMap/Module.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Polyhedral/Mathlib/Geometry/Convex/AffineMap/Module.lean b/Polyhedral/Mathlib/Geometry/Convex/AffineMap/Module.lean index 0c7c5c50..ff5a3bb8 100644 --- a/Polyhedral/Mathlib/Geometry/Convex/AffineMap/Module.lean +++ b/Polyhedral/Mathlib/Geometry/Convex/AffineMap/Module.lean @@ -11,8 +11,6 @@ open scoped Pointwise namespace Convexity variable {R S M : Type*} -alias _root_.LinearMap.isAffineMap := IsAffineMap.linearMap - section Semiring variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [ConvexSpace R M] [IsModuleConvexSpace R M] {K K₁ K₂ : Set M} @@ -22,7 +20,8 @@ protected lemma IsConvexSet.add (hK₁ : IsConvexSet R K₁) (hK₂ : IsConvexSe variable [DistribSMul S M] [SMulCommClass R S M] -lemma isAffineMap_smul (s : S) : IsAffineMap R fun x : M ↦ s • x := (s • LinearMap.id).isAffineMap +lemma isAffineMap_smul (s : S) : IsAffineMap R fun x : M ↦ s • x := + IsAffineMap.linearMap (s • LinearMap.id : M →ₗ[R] M) protected lemma IsConvexSet.smul (s : S) {K : Set M} (hK : IsConvexSet R K) : IsConvexSet R (s • K) := by rw [← Set.image_smul]; exact hK.image (isAffineMap_smul s) @@ -35,7 +34,7 @@ variable [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] protected lemma IsConvexSet.neg (hK : IsConvexSet R K) : IsConvexSet R (-K) := by rw [← Set.image_neg_eq_neg] - exact hK.image (LinearEquiv.neg R).toLinearMap.isAffineMap + exact hK.image (.linearMap (LinearEquiv.neg R).toLinearMap) @[simp] lemma isConvexSet_neg : IsConvexSet R (-K) ↔ IsConvexSet R K where mp h := by simpa using h.neg