-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(probability_theory/independence): prove equivalences for indep_set #6242
Conversation
I think a more principled approach to @[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 |
Thanks for the better approach. |
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
…mathlib into mzinkevi_pi_system
I changed the proof to use a much simpler approach, using the fact that All statements about |
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
bors r+ |
…et (#6242) 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`. Co-authored-by: mzinkevi <martinz@google.com> Co-authored-by: mzinkevi <41597957+mzinkevi@users.noreply.github.com>
Build failed (retrying...): |
…et (#6242) 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`. Co-authored-by: mzinkevi <martinz@google.com> Co-authored-by: mzinkevi <41597957+mzinkevi@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…et (#6242) 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`. Co-authored-by: mzinkevi <martinz@google.com> Co-authored-by: mzinkevi <41597957+mzinkevi@users.noreply.github.com>
Prove the following equivalences on
indep_set
, for measurable setss,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 obtainindep_set s t µ
fromindep_sets S T µ
ands ∈ S
,t ∈ T
.