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

[mzinkevi]

The goal here is to prove that the expectation of a product of an finite number of independent random variables equals the production of the expectations.

See https://github.com/leanprover-community/mathlib/tree/mzinkevi_independent_finite_alt

---

[RemyDegenne]

You requested a review from me and I am happy to help on this, but note that I am not a maintainer and cannot approve the PR for merge.
I'll look at the code more thoroughly later but here are a few preliminary comments:

• please use set notation t ∈ generate_pi_system g instead of generate_pi_system g t. Even though set M is the same as M → Prop, we hide that and prefer usual set notation for readability.
• please put begin on a new line.
• you could add a lemma subset_generate_pi_system_self, proving that s ⊆ generate_pi_system s.
• you could add a lemma generate_pi_system_mono, proving that if s ⊆ t then generate_pi_system s ⊆ generate_pi_system t.
• g is a strange notation for a set of sets. It looks fine to me for a function g : β → set (set α), but unusual for g : set (set α). Maybe use S or T?

Aside from the review, I feel that we should make sure to coordinate our efforts. I am also currently adding results about independence and we should make sure that we don't do the same things twice. I have a series of PRs coming towards Kolmogorov's 0-1 law (see the independence branch, where it is complete but needs modifications before PR).
Also I see that on your mzinkevi_independent_finite_alt branch, you redefined indep_set in order to have indep_set s t μ ↔ indep_sets {s} {t} μ by definition. I saw on your other PR that you could use that equivalence, so I made PR #6242, in which I am using the current definition of indep_set to prove it, as well as indep_set s t μ ↔ μ (s ∩ t) = μ s * μ t.
And thanks for working on probability theory for mathlib!

[RemyDegenne]

Here are several minor comments, mostly about style, with suggestions to shorten the proofs.
I did not look at the two long proofs at the end yet.

[bryangingechen]

You requested a review from me and I am happy to help on this, but note that I am not a maintainer and cannot approve the PR for merge.

@RemyDegenne: I think I speak for all the maintainers when I say that we are very grateful when contributors help with reviews. Thank you!

[mzinkevi]

@RemyDegenne, thanks for the detailed review!

The reason I added you was because I am less concerned about the syntax and more because you wrote the proofs in independence. Since this PR is heading towards:

https://github.com/leanprover-community/mathlib/tree/mzinkevi_independent_finite_alt

I wanted to make sure we were on the same page. I'll add a second reviewer.

-Marty

[mzinkevi]

I added fpvandoorn as an "assignee". Maybe next time I will flip them.

[RemyDegenne]

You can see that continuous integration is failing due to the linter. If you click on details, it tells you that your definition generate_pi_system needs a docstring. All definitions need a docstring. Here is the way you add one:

/-- Docstring text here -/
inductive generate_pi_system ...

You can write #lint in your file to check that all lemmas/definitions above that point verify the linting checks (remove it before you commit).

As I suggested in my first comment, I feel like the basic API around generate_pi_system needs two or three more lemmas. Currently you have generate_pi_system_subset proving generate_pi_system g ⊆ t for a pi-system t such that g ⊆ t, and generate_pi_system_eq proving generate_pi_system g = g for a pi-system g. I would expand that to include more comparisons of g and generate_pi_system g:

lemma subset_generate_pi_system_self {α} (g : set (set α)) : g ⊆ generate_pi_system g :=
λ s, generate_pi_system.base

lemma generate_pi_system_subset_self {α} {g : set (set α)} (h_g : is_pi_system g) :
  generate_pi_system g ⊆ g :=
 begin
  intros x h,
  induction h with s h_s s u h_gen_s h_gen_u h_nonempty h_s h_u,
  { exact h_s, },
  { exact h_g _ _ h_s h_u h_nonempty, },
end

lemma generate_pi_system_eq {α} {g : set (set α)} (h_pi : is_pi_system g) :
  generate_pi_system g = g :=
set.subset.antisymm (generate_pi_system_subset_self h_pi) (subset_generate_pi_system_self g)

lemma generate_pi_system_mono {α} {S T : set (set α)} (hST : S ⊆ T) :
  generate_pi_system S ⊆ generate_pi_system T :=
begin
  intros t ht,
  induction ht with s h_s s u h_gen_s h_gen_u h_nonempty h_s h_u,
  { exact generate_pi_system.base (set.mem_of_subset_of_mem hST h_s),},
  { exact is_pi_system_generate_pi_system T _ _ h_s h_u h_nonempty, },
end

lemma generate_pi_system_subset {α} {g t : set (set α)} (h_t : is_pi_system t)
  (h_sub : g ⊆ t) : generate_pi_system g ⊆ t :=
set.subset.trans (generate_pi_system_mono h_sub) (generate_pi_system_subset_self h_t)

At that point, I am not sure generate_pi_system_subset is still a useful lemma, since it is only mono + subset_self.

[RemyDegenne]

A few minor changes about spacing.

[mzinkevi]

Okay, I have given a more thorough review of your comments. I renamed the algorithms.

We should start a separate thread discussing the high level goals here.

The indep_set we should discuss: I wanted you to be aware, and we should definitely coordinate. I am pushing towards Chernoff's inequalities, so we shouldn't have too much of a collision.

A question I have right now (and it is a question more than an answer) is whether measurable functions and measurable sets (and random variables and events) should be types. I am not sure if the default answer is yes or no. It is certainly prettier with them as types, but there are also an additional layer of theorems and definitions. A key question in my mind is what formulation makes it easier to automate theorems. It feels like the key goal is developing tactics and patterns proving:

1. Independence (of sets and functions (and spaces?))
2. Measurability (of sets and functions)
3. Equality of events (usually as identical sets)
4. Two random variables are identical

But again, let's discuss.

-Marty

[RemyDegenne]

I finally had a look at the last lemma.

[bryangingechen]

@mzinkevi I noticed that you put the following reply in the commit message:

Thank you! These changes are helpful in understanding the style. I haven't quite figured out the style as to line breaks, but I'll try to implement this pattern moving forward.
I have seen suffices, but I haven't used it yet. I'll look through my next PR to see where I can use it.

It's better to reply in the comments here since the commit messages aren't copied here and so are easily missed.

[sgouezel]

Thanks a lot for this! Since you are expanding nicely on what there is on pi systems in the file measurable_space.lean, I wonder if it wouldn't make sense to move all there is on this notion (and on dynkin systems) to the file you are creating, to get something more self-contained and easier to locate.

By the way, you are importing measure_space, but I guess it would suffice to import measurable_space for everything to make sense (and you don't need to open measure_theory as there is no measure in your file).

[mzinkevi]

Okay, I have refactored it as sgouezel requested. I added some comments on attribution.

[sgouezel]

Thanks for the refactor! I have pushed a few more detailed docstrings. This looks good to me, but I'd be happy to have a last look from @fpvandoorn or @RemyDegenne on this.

[RemyDegenne]

It looks good to me.

[sgouezel]

Thanks for checking!
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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