[Merged by Bors] - feat(measure_theory/independence): define independence of sets of sets, measurable spaces, sets, functions

[RemyDegenne]

This first PR about independence contains definitions, a few lemmas about independence of unions/intersections of sets of sets, and a proof that two measurable spaces are independent iff generating pi-systems are independent (included in this PR to demonstrate usability of the definitions).

---

The plan is to follow with the content of the file independence.lean on the independence branch:

• proof of the pi-system lemma for a family of measurable spaces instead of just two,
• Kolmogorov's 0-1 law.

[hrmacbeth]

Great to see a new area start to be filled out! Could you update docs/undergrad.yaml with each PR, so this PR knocks off the first few items on the "Probability" list, etc?

[eric-wieser]

If you're feeling ambitious you could also introduce notation for independence. As a contrived demo:

def indep { A : Type*} (μ : ℕ) (a b : A) : Prop := sorry
def Indep { A B : Type*} (μ : ℕ) (f : B → A) : Prop := sorry

-- assuming the "indepedent" (⫫) of probability is suitable here: 
infix ` ⫫ `:50 := indep _
notation a ` ⫫[` μ `] ` b :50 := indep μ a b

notation `⫫ `:65 := indep
notation `⫫` binders `, ` r:(scoped:67 f, Indep _ f) := r
notation `⫫[` μ `]` binders `, ` r:(scoped:67 f, Indep μ f) := r

variables {A B : Type*} (a b : A) (f : B → A) (μ : ℕ) -- obviously mu should be a measure, I'm lazy

#check a ⫫[μ] b
#check a ⫫ b

#check (⫫ i, f i)
#check (⫫[μ] i, f i)

[sgouezel]

I think the math structure is good. I have a problem with the terminology in many docstrings, coming from the fact that "measurable space" means a space with a sigma-algebra in maths, and a sigma-algebra on an already given space in Lean. You could avoid the ambiguity by replacing "measurable space" with "measurable space structure" in many docstrings, to indicate that you are not introducing a new space, only a new measurable structure.

[sgouezel]

I have pushed minor changes:

• some docstring clarification
• use dot notation where possible
• put everything in a namespace probability_theory (there are enough notions of independence in mathematics that we shouldn't preempt it in the root namespace)
• Move the file to a new folder probability_theory
• Remove a useless assumption of finite measure in an ext lemma.

I have checked what you've done, and I am very happy with it. You should my changes before this can be merged, though!

bors d+

[bors]

✌️ 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.

[eric-wieser]

@sgouezel, do you have any thoughts on my notation suggestion in #5848 (comment)?

[sgouezel]

It's a nice suggestion. However, in most probability theory papers this kind of notation is not used, and independence is spellt out explicitly. So I would say it's good to have it but I am not sure it should become the normal form to express independence in mathlib. In any case, it can wait for a later PR unless Rémy wants to add it now.

[eric-wieser]

Waiting for a later PR is probably a good idea anyway

[RemyDegenne]

I will not add the notation to this PR, and to be honest I am not completely sure about its utility. The indep names are already short enough that I don't see a huge benefit in introducing new notation. But that might be entirely due to the habit I have of not using notation for independence in my own work (except for "i.i.d.", which should probably be introduced at some point).

[RemyDegenne]

bors r+

[sgouezel]

Yes, I expect that iid will be a very useful (and very much used) definition

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Canceled.

[RemyDegenne]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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