feat(Probability/Markov): stationary distributions for stochastic matrices

[dennj]

This PR proves that every row-stochastic matrix on a finite nonempty
state space has a stationary distribution in the standard simplex.

Main additions to Mathlib/Probability/Markov/Stationary.lean:

• IsStationary: A distribution μ is stationary for matrix P if μ ᵥ* P = μ
• cesaroAverage: Cesàro average of iterates of a vector under a matrix
• Matrix.rowStochastic.exists_stationary_distribution: existence theorem

The proof uses Cesàro averaging: start with uniform distribution, form
averages, extract convergent subsequence by compactness, show limit is
stationary via L¹ non-expansiveness.

Also adds vecMul_mem_stdSimplex to Stochastic.lean: multiplying a
probability vector by a row-stochastic matrix preserves simplex membership.

This is human-made PR with AI help in golfing proof and documenting the code.

[github-actions]

PR summary c7a9524911

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Probability.Markov.Stationary (new file)	2158

---

Declarations diff

+ IsStationary
+ IsStationary.pow
+ cesaroAverage
+ cesaroAverage_mem_stdSimplex
+ exists_stationary_distribution
+ nnnorm_vecMul_le
+ norm_cesaroAverage_vecMul_sub_le
+ vecMul_mem_stdSimplex

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.

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

[j-loreaux]

@dennj there is already an open PR for this #28708 (although your PR contains some material which is not present there). That PR author has indicated that @dupuisf is welcome to take it over. Can you please coordinate with Frédéric Dupuis to get #28708 finished? After we can work on getting any material left in this PR into Mathlib.

(And for future reference, please try to check if anyone is already working on a given project by searching on Zulip and GitHub so that we avoid duplication of effort and review.)

[j-loreaux]

actually, I didn't realize that PR was ready, and I just sent it to be merged. When that's done, you can merge master into this PR and then add anything you have that was missing from that one.

[dennj]

actually, I didn't realize that PR was ready, and I just sent it to be merged. When that's done, you can merge master into this PR and then add anything you have that was missing from that one.

Done, I rebased my changes on top of that PR.

-awaiting-author

[mathlib-merge-conflicts]

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

[dennj]

-awaiting-author

[riccardobrasca]

Not my area of expertise, so un-assigning me.

[dupuisf]

I left a few initial comments. Could you also disclose whether generative AI tools were used in preparing this PR, and if so, how exactly? Thanks.

[dupuisf]

Why is it k + 1 instead of simply k?

[dennj]

So that every k : N gives a valid average. With k + 1, k = 0 averages one term; with plain k, you'd get 0^-1 * 0 = 0 and need k >= 1 side conditions everywhere downstream

[grunweg]

Hello from triage! My impression is that this PR was generated with substantial help from LLM. Can you comment on this, please? Per our AI policy, if so, you are required to mention this in the PR description.

[dennj]

-awaiting-author

I applied the suggestions in the comments and did some golfing