Commit 2026-05-15 08:37 c5360fdb

View on Github →

feat(Geometry/Convex): indexed convex combinations (#37592) We introduce sConvexComb and the indexed version iConvexComb as the main API for ConvexSpace and prove lemmas around the new definitions. Rename convexComboPair to convexCombPair to match.

Estimated changes

Modified Mathlib/Analysis/Convex/MetricSpace.lean

deleted theorem ConvexSpace.ofConvex.coe_convexCombination

added theorem Convexity.ConvexSpace.ofConvex.coe_iConvexComb

added theorem Convexity.ConvexSpace.ofConvex.coe_sConvexComb

added theorem Convexity.continuous_convexCombPair'

added theorem Convexity.continuous_convexCombPair

added theorem Convexity.continuous_convexCombPair_of_isBounded

added theorem Convexity.dist_convexCombPair_convexCombPair

added theorem Convexity.dist_convexCombPair_convexCombPair_le

added theorem Convexity.dist_convexCombPair_left

added theorem Convexity.dist_convexCombPair_right

added theorem Convexity.dist_iConvexComb_le

added theorem Convexity.dist_iConvexComb_left_le

added theorem Convexity.dist_iConvexComb_right_le

added theorem Convexity.dist_left_convexCombPair

added theorem Convexity.dist_right_convexCombPair

added theorem Convexity.dist_sConvexComb_left_le

added theorem Convexity.dist_sConvexComb_right_le

added theorem Convexity.isAffineMap_coe

deleted theorem IsConvexMetricSpace.of_convex

deleted theorem continuous_convexComboPair'

deleted theorem continuous_convexComboPair

deleted theorem continuous_convexComboPair_of_isBounded

deleted theorem dist_convexCombination_left_le

deleted theorem dist_convexCombination_map_le

deleted theorem dist_convexCombination_right_le

deleted theorem dist_convexComboPair_convexComboPair

deleted theorem dist_convexComboPair_convexComboPair_le

deleted theorem dist_convexComboPair_left

deleted theorem dist_convexComboPair_right

deleted theorem dist_left_convexComboPair

deleted theorem dist_right_convexComboPair

Modified Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean

added theorem AddTorsor.convexCombPair_eq_lineMap

added def AddTorsor.convexCombination

added theorem AddTorsor.convexCombination_assoc

added theorem AddTorsor.convexCombination_single

added theorem AddTorsor.iConvexComb_eq_affineCombination

added theorem AddTorsor.sConvexComb_eq_affineCombination

added theorem Convexity.StdSimplex.isAffineMap_weights

added theorem Convexity.convexCombPair_eq_add

added theorem Convexity.iConvexComb_eq_sum

added theorem Convexity.sConvexComb_eq_sum

Modified Mathlib/Geometry/Convex/ConvexSpace/Defs.lean

added theorem Convexity.IsAffineMap.comp

added theorem Convexity.IsAffineMap.map_convexCombPair

added theorem Convexity.IsAffineMap.map_iConvexComb

added structure Convexity.IsAffineMap

added def Convexity.StdSimplex.duple

added theorem Convexity.StdSimplex.isAffineMap_map

added def Convexity.StdSimplex.join

added def Convexity.StdSimplex.map

added theorem Convexity.StdSimplex.map_comp

added theorem Convexity.StdSimplex.map_const

added theorem Convexity.StdSimplex.map_duple

added theorem Convexity.StdSimplex.map_id

added theorem Convexity.StdSimplex.map_map

added theorem Convexity.StdSimplex.map_sConvexComb

added theorem Convexity.StdSimplex.map_single

added theorem Convexity.StdSimplex.mk_single

added theorem Convexity.StdSimplex.nonempty

added def Convexity.StdSimplex.single

added theorem Convexity.StdSimplex.support_weights_eq_singleton

added theorem Convexity.StdSimplex.support_weights_nonempty

added theorem Convexity.StdSimplex.weights_convexCombPair

added theorem Convexity.StdSimplex.weights_iConvexComb

added theorem Convexity.StdSimplex.weights_inj

added theorem Convexity.StdSimplex.weights_ne_zero

added theorem Convexity.StdSimplex.weights_nonneg

added theorem Convexity.StdSimplex.weights_sConvexComb

added structure Convexity.StdSimplex

added def Convexity.convexCombPair

added theorem Convexity.convexCombPair_convexCombPair_assoc_left

added theorem Convexity.convexCombPair_convexCombPair_assoc_right

added theorem Convexity.convexCombPair_convexCombPair_left_eq_sConvexComb

added theorem Convexity.convexCombPair_convexCombPair_right_eq_sConvexComb

added theorem Convexity.convexCombPair_def

added theorem Convexity.convexCombPair_iConvexComb_iConvexComb

added theorem Convexity.convexCombPair_iConvexComb_left

added theorem Convexity.convexCombPair_iConvexComb_right

added theorem Convexity.convexCombPair_one

added theorem Convexity.convexCombPair_same

added theorem Convexity.convexCombPair_symm

added theorem Convexity.convexCombPair_zero

added def Convexity.iConvexComb

added theorem Convexity.iConvexComb_assoc''

added theorem Convexity.iConvexComb_assoc'

added theorem Convexity.iConvexComb_assoc

added theorem Convexity.iConvexComb_comm

added theorem Convexity.iConvexComb_congr

added theorem Convexity.iConvexComb_const

added theorem Convexity.iConvexComb_convexCombPair

added theorem Convexity.iConvexComb_convexCombPair_comm

added theorem Convexity.iConvexComb_convexCombPair_comm_left

added theorem Convexity.iConvexComb_convexCombPair_comm_right

added theorem Convexity.iConvexComb_id'

added theorem Convexity.iConvexComb_id

added theorem Convexity.iConvexComb_map

added theorem Convexity.iConvexComb_single

added theorem Convexity.isAffineMap_convexCombPair

added theorem Convexity.map_iConvexComb

added theorem Convexity.sConvexComb_convexCombPair

added theorem Convexity.sConvexComb_map

added theorem Convexity.sConvexComb_sConvexComb

deleted def StdSimplex.duple

deleted theorem StdSimplex.ext

deleted def StdSimplex.join

deleted def StdSimplex.map

deleted theorem StdSimplex.map_comp

deleted theorem StdSimplex.map_const

deleted theorem StdSimplex.map_duple

deleted theorem StdSimplex.map_id

deleted theorem StdSimplex.map_map

deleted theorem StdSimplex.map_single

deleted theorem StdSimplex.mk_single

deleted theorem StdSimplex.nonempty

deleted def StdSimplex.single

deleted structure StdSimplex

deleted def convexComboPair

deleted theorem convexComboPair_one

deleted theorem convexComboPair_same

deleted theorem convexComboPair_symm

deleted theorem convexComboPair_zero

Modified Mathlib/Topology/Subpath.lean

modified theorem Path.range_subpathAux

Modified Mathlib/Topology/UnitInterval.lean

added theorem Set.Icc.coe_convexComb

deleted theorem Set.Icc.coe_convexCombo

added theorem Set.Icc.continuous_convexComb

added theorem Set.Icc.continuous_convexComb_prod

deleted theorem Set.Icc.continuous_convexCombo

deleted theorem Set.Icc.continuous_convexCombo_prod

added def Set.Icc.convexComb

added theorem Set.Icc.convexComb_assoc'

added theorem Set.Icc.convexComb_assoc

added theorem Set.Icc.convexComb_eq

added theorem Set.Icc.convexComb_le

added theorem Set.Icc.convexComb_one

added theorem Set.Icc.convexComb_symm

added theorem Set.Icc.convexComb_zero

added theorem Set.Icc.convexComb_zero_one

deleted def Set.Icc.convexCombo

deleted theorem Set.Icc.convexCombo_assoc'

deleted theorem Set.Icc.convexCombo_assoc

deleted theorem Set.Icc.convexCombo_eq

deleted theorem Set.Icc.convexCombo_le

deleted theorem Set.Icc.convexCombo_one

deleted theorem Set.Icc.convexCombo_symm

deleted theorem Set.Icc.convexCombo_zero

deleted theorem Set.Icc.convexCombo_zero_one

added theorem Set.Icc.eq_convexComb

deleted theorem Set.Icc.eq_convexCombo

added theorem Set.Icc.le_convexComb

deleted theorem Set.Icc.le_convexCombo

Modified MathlibTest/grind/lint.lean