feat(LinearAlgebra/ConvexSpace): StdSimplex bind operation

[TBUGTB]

Define the monadic bind operation for StdSimplex and add basic API lemmas. This operation is needed for formalising the Komlós lemma used in the construction of Stochastic Integrals (cf. this PR in the brownian-motion project).

---

• depends on: [Merged by Bors] - feat(Geometry/Convex): indexed convex combinations #37592

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 5b5173e00f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ bind
+ bind_const
+ bind_single
+ sum_map
+ support_subset_support_bind
+ weights_bind

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.

---

No changes to technical debt.

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.sh 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).

[TBUGTB]

-awaiting-author

[EtienneC30]

Can you resolve the conversations when you applied a suggestion please? This makes the page easier to read.

[EtienneC30]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

[RemyDegenne]

bors r+

[YaelDillies]

Please instead use iConvexCombo once #37592 is merged

[YaelDillies]

bors r-

[mathlib-bors]

Canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat(Geometry/Convex): indexed convex combinations #37592
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[YaelDillies]

Sorry, I thought #37592 would be merged within a few days... At any rate, I am claiming that iConvexCombo from that PR replaces StdSimplex.bind from this one, so IMO you can close this on and adapt brownian-motion to use iConvexCombo instead.

[TBUGTB]

okay, thanks for letting me know