feat(probability/independence): Kolmogorov's 0-1 law

[RemyDegenne]

We prove that any event in the tail σ-algebra of an independent sequence of sub-σ-algebras has probability 0 or 1.

---

• [x] depends on: #16759

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#16759~~ By Dependent Issues (🤖). Happy coding!

[kex-y]

I think this looks good!

maintainer merge

[github-actions[bot]]

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

[ocfnash]

bors merge

[ocfnash]

Oh! I think this PR needs a merge from master: we changed the order of arguments in filter.limsup (and filter.liminf) yesterday in #16819

bors r-

bors d+

[bors[bot]]

:v: RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bors[bot]]

Canceled.

[RemyDegenne]

bors r+

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests