feat: set up API for ConvexSpace#37592
feat: set up API for ConvexSpace#37592erdOne wants to merge 13 commits intoleanprover-community:masterfrom
ConvexSpace#37592Conversation
github-actions
bot
added
the
large-import
PR summary 79463c8311Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.LinearAlgebra.ConvexSpace | 770 | 842 | +72 (+9.35%) |
| Mathlib.LinearAlgebra.ConvexSpace.AffineSpace | 1021 | 1005 | -16 (-1.57%) |
| Mathlib.Analysis.Convex.MetricSpace | 1475 | 1474 | -1 (-0.07%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.LinearAlgebra.ConvexSpace.AffineSpace |
-16 |
Mathlib.Analysis.Convex.MetricSpace |
-1 |
Mathlib.LinearAlgebra.ConvexSpace |
72 |
Declarations diff
+ ConvexSpace.IsMetricCompatible
+ ConvexSpace.IsMetricCompatible.of_convex
+ ConvexSpace.mk
+ ConvexSpace.ofConvex.coe_iConvexCombo
+ ConvexSpace.ofConvex.coe_sConvexCombo
+ IsAffineMap
+ IsAffineMap.comp
+ IsAffineMap.id
+ IsAffineMap.map_convexComboPair
+ IsAffineMap.map_iConvexCombo
+ StdSimplex.isAffineMap_map
+ StdSimplex.isAffineMap_weights
+ convexComboPair_convexComboPair_assoc_left
+ convexComboPair_convexComboPair_assoc_right
+ convexComboPair_convexComboPair_left_eq_sConvexCombo
+ convexComboPair_convexComboPair_right_eq_sConvexCombo
+ convexComboPair_def
+ convexComboPair_eq_add
+ convexComboPair_iConvexCombo_iConvexCombo
+ convexComboPair_iConvexCombo_left
+ convexComboPair_iConvexCombo_right
+ dist_iConvexCombo_le
+ dist_iConvexCombo_left_le
+ dist_iConvexCombo_right_le
+ dist_sConvexCombo_left_le
+ dist_sConvexCombo_right_le
+ iConvexCombo
+ iConvexCombo_comm
+ iConvexCombo_congr
+ iConvexCombo_const
+ iConvexCombo_convexComboPair
+ iConvexCombo_convexComboPair_comm
+ iConvexCombo_convexComboPair_comm_left
+ iConvexCombo_convexComboPair_comm_right
+ iConvexCombo_eq_affineCombination
+ iConvexCombo_eq_sum
+ iConvexCombo_iConvexCombo
+ iConvexCombo_id
+ iConvexCombo_id'
+ iConvexCombo_map
+ iConvexCombo_single
+ instance : ConvexSpace R (StdSimplex R I)
+ isAffineMap_coe
+ isAffineMap_convexComboPair
+ join_join
+ join_single
+ map_iConvexCombo
+ map_join
+ map_sConvexCombo
+ sConvexCombo_eq_affineCombination
+ sConvexCombo_eq_sum
+ sConvexCombo_sConvexCombo
+ weights_nonneg
+ weights_sConvexCombo
- ConvexSpace.ofConvex.coe_convexCombination
- IsConvexMetricSpace
- IsConvexMetricSpace.of_convex
- _root_.convexCombination_eq_sum
- dist_convexCombination_left_le
- dist_convexCombination_map_le
- dist_convexCombination_right_le
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Co-authored-by: Yaël Dillies <[email protected]>
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks! 🚀
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
mathlib-triage
bot
added
the
maintainer-merge
2 participants
We introduce
sConvexComboand the indexed versioniConvexComboas the main API forConvexSpaceand prove lemmas around the new definitions.