feat(Geometry/Convex): positivity extension for StdSimplex.weights

[YaelDillies]

Also add some Qq helper to Qq-match a type with Finsupp.

From the Polyhedra in Berlin workshop where people would have found it useful for positivity to close some goals.

Generated by Claude Opus in a few prompts worth of reviewl.

Assisted-by: Claude Opus 5

---

[github-actions]

PR summary f7e2f0fac3

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Finsupp.Defs	573	574	+1 (+0.17%)

Import changes for all files

Files

Import difference

77 files Mathlib.Algebra.BigOperators.Associated Mathlib.Algebra.BigOperators.Finsupp.Basic Mathlib.Algebra.BigOperators.Finsupp.Fin Mathlib.Algebra.Category.MonCat.Adjunctions Mathlib.Algebra.FreeAbelianGroup.Finsupp Mathlib.Algebra.FreeAbelianGroup.UniqueSums Mathlib.Algebra.FreeMonoid.UniqueProds Mathlib.Algebra.Group.Finsupp Mathlib.Algebra.Group.Subgroup.Finsupp Mathlib.Algebra.Group.Submonoid.Finsupp Mathlib.Algebra.Group.UniqueProds.Basic Mathlib.Algebra.GroupWithZero.Torsion Mathlib.Algebra.MonoidAlgebra.Cardinal Mathlib.Algebra.MonoidAlgebra.Defs Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Algebra.MonoidAlgebra.Lift Mathlib.Algebra.MonoidAlgebra.MapDomain Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors Mathlib.Algebra.MonoidAlgebra.Opposite Mathlib.Algebra.MonoidAlgebra.PointwiseSMul Mathlib.Algebra.Order.Antidiag.FinsuppEquiv Mathlib.Algebra.Order.Antidiag.Finsupp Mathlib.Algebra.Order.Floor.Div Mathlib.Algebra.Star.BigOperators Mathlib.Data.DFinsupp.Notation Mathlib.Data.DFinsupp.Small Mathlib.Data.Finset.Finsupp Mathlib.Data.Finsupp.AList Mathlib.Data.Finsupp.Antidiagonal Mathlib.Data.Finsupp.Basic Mathlib.Data.Finsupp.BigOperators Mathlib.Data.Finsupp.Defs Mathlib.Data.Finsupp.Ext Mathlib.Data.Finsupp.Fin Mathlib.Data.Finsupp.Fintype Mathlib.Data.Finsupp.Indicator Mathlib.Data.Finsupp.Interval Mathlib.Data.Finsupp.Lex Mathlib.Data.Finsupp.MonomialOrder Mathlib.Data.Finsupp.Multiset Mathlib.Data.Finsupp.NeLocus Mathlib.Data.Finsupp.Notation Mathlib.Data.Finsupp.Option Mathlib.Data.Finsupp.Order Mathlib.Data.Finsupp.PWO Mathlib.Data.Finsupp.Pointwise Mathlib.Data.Finsupp.Quotient Mathlib.Data.Finsupp.SMulWithZero Mathlib.Data.Finsupp.SMul Mathlib.Data.Finsupp.Sigma Mathlib.Data.Finsupp.Single Mathlib.Data.Finsupp.ToDFinsupp Mathlib.Data.Finsupp.WellFounded Mathlib.Data.List.ToFinsupp Mathlib.Data.Nat.Factorization.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.Data.Nat.Factorization.Divisors Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Nat.Factorization.LCM Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Factorization.Root Mathlib.Data.Sym.Sym2.Finsupp Mathlib.LinearAlgebra.Finsupp.Defs Mathlib.LinearAlgebra.Finsupp.SumProd Mathlib.Logic.Hydra Mathlib.NumberTheory.HeckeRing.Defs Mathlib.Order.Preorder.Finsupp Mathlib.RingTheory.HahnSeries.Addition Mathlib.RingTheory.HahnSeries.Basic Mathlib.RingTheory.UniqueFactorizationDomain.Basic Mathlib.RingTheory.UniqueFactorizationDomain.Finite Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative Mathlib.RingTheory.UniqueFactorizationDomain.Nat Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors Mathlib.SetTheory.Cardinal.Finsupp Mathlib.Testing.Plausible.Functions

1

---

Declarations diff (regex)

+ instantiateLevelMVarsQ
+ instantiateMVarsQ'
+ weights_pos

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit f7e2f0f).

• +6 new declarations
• −0 removed declarations

+Convexity.StdSimplex.weights_pos
+Mathlib.Meta.Positivity.evalStdSimplexWeights
+Mathlib.Meta.Positivity.evalStdSimplexWeightsApply
+Qq.instantiateLevelMVarsQ
+Qq.instantiateMVarsQ'
+Qq.matchFinsupp

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit f7e2f0fac3
Reference commit 97ac4d32b0

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).