[Merged by Bors] - feat(probability/independence): Independence of singletons#18506
[Merged by Bors] - feat(probability/independence): Independence of singletons#18506YaelDillies wants to merge 12 commits intomasterfrom
Conversation
| lemma comap_map_le : (m.map f).comap f ≤ m := (gc_comap_map f).l_u_le _ | ||
| lemma le_map_comap : m ≤ (m.comap g).map g := (gc_comap_map g).le_u_l _ | ||
|
|
||
| lemma comap_of_involutive {m' : measurable_space β} {g : β → β} (hg : involutive g) |
There was a problem hiding this comment.
This lemma immediately follows from 3 facts, 2 of them are not in mathlib yet. Could you add them, please?
-
measurable_embedding.comap_eq:comapof themeasurable_spaceinstance along ameasurable_embeddingis the corresponding instance; BTW,measurable_embedding fis equivalent tocomap f _ = _+measurable_set (range f). -
measurable_equiv.of_involutive: a measurable involutive map generates ameasurable_equiv; theto_equivprojection is given byequiv.perm.of_involutive; -
measurable_space.comap_comp- already in the library.
While you're at it, could you please add
-
measurable_equiv.map_eq
as well?
I'm not sure if we should use measurable_space in the names to make it clear that the lemmas are not about measure_theory.measure.map and measure_theory.measure.comap.
There was a problem hiding this comment.
I've added everything you mentioned here, but I couldn't prove measurable_embedding f ↔ comap f _ = _ ∧ measurable_set (range f). Instead I proved measurable_embedding f ↔ injective f ∧ comap f _ = _ ∧ measurable_set (range f).
|
Also, let's ask @RemyDegenne to review the part about |
|
Sorry, why has this been tagged as |
|
Are we good to go, now? |
| instance : measurable_space punit := ⊤ -- this also works for `unit` | ||
| instance : measurable_space bool := ⊤ | ||
| instance Prop.measurable_space : measurable_space Prop := ⊤ | ||
| instance {α} : measurable_space (set α) := ⊤ |
There was a problem hiding this comment.
Why this is the right instance for measurable_space (set α)? IMHO, any instance on set α that is not equal to the corresponding instance on α → Prop needs an explanation in the docstring.
There was a problem hiding this comment.
I thought I needed this instance but I'm not sure anymore. Let's see whether this PR compiles without it.
RemyDegenne
left a comment
There was a problem hiding this comment.
I am not sure that I agree that this is not too late but fine, let's proceed with this PR.
The changes to the independence file look good.
My only issue with this PR is the one raised by Yuri about the measurable space on set α: if there is a good reason for it not to be measurable_space.pi, it should be explained. If the case you care about is finite α, then measurable_space.pi is the same as top:
example [fintype α] : (measurable_space.pi : measurable_space (set α)) = ⊤ :=
begin
ext x,
simp only [measurable_space.measurable_set_top, iff_true],
refine measurable.set_of _,
exact measurable_of_countable _,
endApart from that, everything looks good.
|
Thanks! 🎉 |
Characterisation of independence in terms of measure distributing over finite intersections, and lemmas connecting the different concepts of independence. Also add supporting `measurable_space` and `set.preimage` lemmas
|
Build failed: |
|
bors merge |
Characterisation of independence in terms of measure distributing over finite intersections, and lemmas connecting the different concepts of independence. Also add supporting `measurable_space` and `set.preimage` lemmas
|
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Port a bit of leanprover-community/mathlib3#18506, but it's mostly handmade.
Port a bit of leanprover-community/mathlib3#18506, but it's mostly handmade. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
Port a bit of leanprover-community/mathlib3#18506, but it's mostly handmade. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
* commit '65a1391a0106c9204fe45bc73a039f056558cb83': (12443 commits)
feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (leanprover-community#18087)
feat(combinatorics/simple_graph): More clique lemmas (leanprover-community#19203)
feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (leanprover-community#16976)
move old README.md to OLD_README.md
doc: Add a warning mentioning Lean 4 to the readme (leanprover-community#19243)
feat(topology/metric_space): diameter of pointwise zero and addition (leanprover-community#19028)
feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (leanprover-community#18629)
feat(probability/independence): Independence of singletons (leanprover-community#18506)
feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (leanprover-community#18612)
feat(data/finset/lattice): `sup'`/`inf'` lemmas (leanprover-community#18989)
chore(order/liminf_limsup): Generalise and move lemmas (leanprover-community#18628)
feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (leanprover-community#17926)
feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (leanprover-community#11352)
feat(analysis/convex/proj_Icc): Extending convex functions (leanprover-community#18797)
feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (leanprover-community#17925)
feat(measure_theory/measure/haar_quotient): the Unfolding Trick (leanprover-community#18863)
feat(linear_algebra/orientation): add `orientation.reindex` (leanprover-community#19236)
feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (leanprover-community#17828)
feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (leanprover-community#15260)
feat(tactic/positivity): Extension for `ite` (leanprover-community#17650)
...
# Conflicts:
# README.md
Characterisation of independence in terms of measure distributing over finite intersections, and lemmas connecting the different concepts of independence.
Also add supporting
measurable_spaceandset.preimagelemmasMatch leanprover-community/mathlib4#2513