[Merged by Bors] - feat(probability_theory/independence): prove equivalences for indep_set

[RemyDegenne]

Prove the following equivalences on indep_set, for measurable sets s,t and a probability measure µ :

• indep_set s t μ ↔ μ (s ∩ t) = μ s * μ t,
• indep_set s t μ ↔ indep_sets {s} {t} μ.

In indep_sets.indep_set_of_mem, we use those equivalences to obtain indep_set s t µ from indep_sets S T µ and s ∈ S, t ∈ T.

---

• depends on: [Merged by Bors] - feat(measure_theory/pi_system) lemmas for pi_system, useful for independence. #6353

[sgouezel]

I think a more principled approach to generate_from_set might make sense. Something like the following, maybe:

@[simp] lemma union_univ {s : set α} : s ∪ univ = univ := sorry

@[simp] lemma univ_union {s : set α} : univ ∪ s = univ := sorry

lemma generate_from_of_finite
  (S : set (set α)) (hcompl : ∀ s ∈ S, sᶜ ∈ S) (hempty : ∅ ∈ S) (hfin : finite S)
  (hun : ∀ s ∈ S, ∀ t ∈ S, s ∪ t ∈ S) :
  generate_measurable S = S :=
let m : measurable_space α :=
{ measurable_set' := S,
  measurable_set_empty := hempty,
  measurable_set_compl := hcompl,
  measurable_set_Union := sorry } in
le_antisymm (generate_from_le (λ t ht, ht) : generate_from S ≤ m)
  (λ t ht, measurable_set_generate_from ht)

lemma generate_from_set (s : set α) :
  generate_measurable ({∅, set.univ, s, sᶜ} : set (set α)) = ({∅, set.univ, s, sᶜ} : set (set α)) :=
generate_from_of_finite _ (by simp) (by simp) (by simp) (by simp)

Note that union_univ and univ_union have just been merged in master. So, there is only one sorry left (which is nontrivial, but probably more interesting than a case by case analysis).

[RemyDegenne]

Thanks for the better approach.
After experimenting a bit, I think this will be easier if we have lemmas about (finite) union-closed sets of sets. In fact, this is the third independent piece of code I have in which union-closed sets of sets appear and I need some of their properties. I will define sup-closed sets (and finsets) in a complete lattice and prove a bunch of lemmas on them before coming back to this PR.

[RemyDegenne]

I changed the proof to use a much simpler approach, using the fact that {s} is a pi-system, as done by @mzinkevi in #6466.

All statements about generate_from_set have been removed. I plan on doing two new related PRs: one with the properties of sup-closed sets I was talking about in my last comment (which will also be useful for the proof of the zero-one law), a second one with the generate_from_of_finite and generate_from_set lemmas discussed above.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(measure_theory/pi_system) lemmas for pi_system, useful for independence. #6353

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[sgouezel]

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

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