PR summary a2d322044a

Import changes for modified files

No significant changes to the import graph

## 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>

./scripts/reporting/technical-debt-metrics.sh pr_summary

note: file Mathlib/Probability/Independence/Process.lean` was renamed to `Mathlib/Probability/Independence/Process/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

Is the definition using Fin easier to use in some cases? Should the Nat-indexed monotone sequence property be the main definition?

I wondered which one should be the definition. In the end I kept the Fin one because in my experience it is more common in textbooks etc., but my experience might be biased. As they both are equivalent, I decided to go with this one.

Also the only time I worked with the definition was to prove that a process with independent increments and Gaussian marginals was Gaussian, and I am not sure how the Nat version of the def could ease the proof. The main difficulty was to index a finset in the right order, but I would have had the same with a Nat version, to which I should have added a way to deal with integers larger than the cardinal of the finset.

But I guess @jvanwinden had a case where Nat was easier to deal with? I think maybe it was because they were dealing with an infinite sequence of increments, so I'd say the answer depends on what you are doing.

I agree with @EtienneC30 that the Fin version aligns closer with textbook definitions. On the other hand, I can offer two examples where the Nat version is nicer to work with:

• the (second) Borel-Cantelli lemma requires independence of infinitely many events. So whenever these events are formulated in terms of independent increments, the Nat version is natural. I experienced this when proving the law of the iterated logarithm
• the other advantage of Nat is that there are fewer types involved, which can sometimes reduce bookkeeping. The original proof of indepFun_sub_sub was significantly simplified by this

Taking all this into account, I am still undecided on which definition would be best suited for mathlib.

I am working on a PR to prove the lemma I mentioned above. I'll try to get rid of Fin and use Nat instead, and if it works I'll do the change. In any case this should be discussed in a docstring.

Ok in the end I stuck with Fin for the definition, especially because for the definition with Nat I should have added the EventuallyConst condition which would have made the definition too cluttered (or I should have added an extra lemma for that case). But I indicated clearly in the docstring that in some cases it was better to use Nat. Regarding Gaussian processes, I stuck with Fin in #36745 and it works actually quite nicely, I don't think the Nat version would have made it more convenient.

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Build