[Merged by Bors] - feat: Independence of singletons

[YaelDillies]

Port a bit of leanprover-community/mathlib#18506, but it's mostly handmade.

---

• depends on: [Merged by Bors] - feat: Sigma-algebra generated by a singleton #2513

Rémy, I tried understanding your new independence API but I still feel like I'm butchering your file.

From LeanCamCombi

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: Sigma-algebra generated by a singleton #2513
  By Dependent Issues (🤖). Happy coding!

[RemyDegenne]

I will review this more thoroughly in the next two days, but right now I can say that it looks like many results could be generalized to independence with respect to a kernel and a measure (like most results about independence). For example, we could have, in Independence/Kernel.lean,

theorem iIndepSets_singleton_iff {s : ι → Set Ω} {_mΩ : MeasurableSpace Ω}
    {κ : kernel α Ω} {μ : Measure α} :
    iIndepSets (fun i ↦ {s i}) κ μ ↔
      ∀ S : Finset ι, ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, s i) = ∏ i in S, κ a (s i) := by

I actually wrote a few of those results for #6098 because I wanted to deduce the conditional independence version. That was before I remembered that you had similar lemmas for independence.

If you don't want to generalize the various lemmas yourself, I can do it and push to this PR. Feel free to take from #6098 if you want to do it (I don't think everything is in there, but the example above is).

As for butchering "my" file, no worries: I think the API is far from perfect and I would love it if someone else could help put some order to it.

[YaelDillies]

I had a similar thought about generalizing the results to kernels, but I wasn't sure enough to do it without your advice.

I don't know anything about kernels, so i will have to do some reading.

[RemyDegenne]

Sorry, I wrote that I would come back to review more, but the conclusion is simply that this should be generalized and I should have marked it awaiting-author. @YaelDillies, do you mind if I do it and push to this branch?

[YaelDillies]

Please do! If you don't have time to do it, I can do it myself tonight, since I've now understood what kernels were.

[RemyDegenne]

I've generalized everything to kernel independence. Now we need another reviewer. @JasonKYi perhaps?

[JasonKYi]

Can you resolve the merge conflict?

[JasonKYi]

Looks good!
maintainer merge

[github-actions]

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

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style