feat(measure_theory): define Borel hierarchy and reprove cardinality bound on σ-algebras #17972

sterraf · 2022-12-17T20:11:32Z

I give an inductive definition of the Borel hierarchy (as suggested by Junyan Xu) and
I provide a basic API. This file serves as a refactor of measure_theory.card_measurable_space
since all the relevant results are proved using this engineering.
EDIT: The refactor is going to be part of a new PR as suggested during review.

There are self-contained changes to the set_theory folder that can be reviewed independently. ω₁ is now an ordinal (not an out, cf. measure_theory.card_measurable_space); for this I use the new function ordinal.initial. I prove a lemma using the cofinality of ω₁. I add a lemma on the cardinality of ordinal-indexed Unions.

…Union` I define `ω₁` as an ordinal (not as an `out`, cf. `measure_theory.card_measurable_space`). I prove a pair of lemmas using its cofinality. I add a lemma on the cardinality of ordinal-indexed `Union`s in preparation for material on the Borel hierarchy.

…ound on σ-algebras I give an inductive definition of the Borel hierarchy (as suggested by Junyan Xu) and I provide a basic API. This file serves as a refactor of `measure_theory.card_measurable_space` since all the relevant results are proved using this engineering.

sgouezel

First bunch of comments, mostly about the use of docstrings.

src/measure_theory/borel_hierarchy.lean

src/set_theory/cardinal/ordinal.lean

sgouezel · 2022-12-26T18:15:41Z

src/set_theory/ordinal/basic.lean

@@ -957,6 +957,13 @@ theorem ord_card_le (o : ordinal) : o.card.ord ≤ o := gc_ord_card.l_u_le _

 lemma lt_ord_succ_card (o : ordinal) : o < (succ o.card).ord := lt_ord.2 $ lt_succ _

+/--
+The converse of the following lemma is false (take, for instance `i = ω+1` and `κ = ℵ₀`).


The docstring is something which shows up as a tooltip when using the lemma. So it should explain the content of the lemma. Additional comments such that the fact that the converse is false are definitely useful, but the first goal is to explain the content of the lemma.

This file has already been reached by the tide. What would be the best course of action now? Either,

move the change to the point of first use (perhaps with a TODO sign to later fix it), therefore leaving this file unmodified; or

keep the edit as it stands, and when (if) the changes are approved, create a parallel PR to mathlib4?

This file has already been reached by the tide. What would be the best course of action now? Either,

move the change to the point of first use (perhaps with a TODO sign to later fix it), therefore leaving this file unmodified

I decided to go this way. I didn't put the TODO sign after all, but I keep a personal record for tidying things up later.

No need to mention previous history Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Saving space as suggested Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

In particular, an intro section defining the Borel hierarchy in detail.

src/measure_theory/borel_hierarchy.lean

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

sgouezel

Review on the first part of the code. I have a lot of minor comments, which is perfectly normal. Could you make sure that you also take these comments into account in the part of the code I haven't reviewed?

src/measure_theory/borel_hierarchy.lean

Correct spacing Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

≠ is the standard spelling Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/measure_theory/borel_hierarchy.lean

src/set_theory/cardinal/cofinality.lean

src/measure_theory/borel_hierarchy.lean

Singular namespaces. And spacing Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

- Simplifying closure of proofs. - Style.

vihdzp

Haven't reviewed the Borel hierarchy part yet.

src/set_theory/cardinal/ordinal.lean

src/set_theory/cardinal/cofinality.lean

Golfed proof Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>

…ing ordinal.basic

…er the tide now

semorrison · 2023-07-25T09:46:06Z

Closed per https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Freeze.20of.20mathlib3/near/378402889.

sterraf added 2 commits December 17, 2022 16:19

line too long

ef43db1

sterraf added the awaiting-review The author would like community review of the PR label Dec 17, 2022

sterraf requested a review from a team as a code owner December 17, 2022 20:52

sterraf assigned sterraf and unassigned sterraf Dec 17, 2022

fix line width and copyright statement

77a211d

sterraf changed the title ~~feat(set_theory): define ω₁ and prove lemma on cardinality of Union~~ feat(measure_theory): define Borel hierarchy and reprove cardinality bound on σ-algebras Dec 18, 2022

sgouezel reviewed Dec 26, 2022

View reviewed changes

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes t-order Order hierarchy and removed awaiting-review The author would like community review of the PR labels Dec 26, 2022

sterraf and others added 5 commits December 26, 2022 15:39

Update src/measure_theory/borel_hierarchy.lean

a064690

No need to mention previous history Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Update src/measure_theory/borel_hierarchy.lean

9458918

Saving space as suggested Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Update src/set_theory/cardinal/ordinal.lean

b5e9bf6

Saving space as suggested Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Changes to documentation suggested by S. Gouëzel.

28b7e8b

In particular, an intro section defining the Borel hierarchy in detail.

line too long

3571ea2

sterraf added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 26, 2022

sgouezel reviewed Dec 27, 2022

View reviewed changes

src/measure_theory/borel_hierarchy.lean Outdated Show resolved Hide resolved

src/measure_theory/borel_hierarchy.lean Outdated Show resolved Hide resolved

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 27, 2022

sterraf and others added 3 commits December 27, 2022 12:21

Update src/measure_theory/borel_hierarchy.lean

687247d

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Delete section on cardinality of sigma-algebras for later.

e41dfa7

More docstrings & minor code edits

fdfd1ef

sterraf added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes awaiting-review The author would like community review of the PR labels Dec 28, 2022

sgouezel reviewed Jan 7, 2023

View reviewed changes

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jan 7, 2023

sterraf and others added 2 commits January 7, 2023 11:07

Apply suggestions from code review

68b14e9

Correct spacing Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Update src/measure_theory/borel_hierarchy.lean

1d65106

≠ is the standard spelling Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

alreadydone reviewed Jan 7, 2023

View reviewed changes

sterraf and others added 4 commits January 7, 2023 17:36

Apply suggestions from code review

6b7993c

Singular namespaces. And spacing Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Suggested edits.

3b3e2ae

- Simplifying closure of proofs. - Style.

Moving to constructions dir

5f831da

Docstring, indentation

6b08306

sterraf added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 9, 2023

vihdzp reviewed Jan 20, 2023

View reviewed changes

sterraf and others added 2 commits January 26, 2023 12:39

Update src/set_theory/cardinal/ordinal.lean

cd3b013

Golfed proof Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>

Definition of initial ordinals; eliminating superfluous lemma; restor…

1f89414

…ing ordinal.basic

semorrison added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Mar 28, 2023

Putting changes back to ordinal.basic, since there are more files und…

b7089a4

…er the tide now

eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023

semorrison closed this Jul 25, 2023

sterraf mentioned this pull request Aug 6, 2023

[Merged by Bors] - feat(SetTheory): definition of initial ordinals, ω₁ as an ordinal, ordinal-indexed unions leanprover-community/mathlib4#6404

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(measure_theory): define Borel hierarchy and reprove cardinality bound on σ-algebras #17972

feat(measure_theory): define Borel hierarchy and reprove cardinality bound on σ-algebras #17972

sterraf commented Dec 17, 2022 •

edited

Loading

sgouezel left a comment

sgouezel Dec 26, 2022

sterraf Feb 27, 2023

sterraf Mar 18, 2023

sgouezel left a comment

vihdzp left a comment

semorrison commented Jul 25, 2023

feat(measure_theory): define Borel hierarchy and reprove cardinality bound on σ-algebras #17972

feat(measure_theory): define Borel hierarchy and reprove cardinality bound on σ-algebras #17972

Conversation

sterraf commented Dec 17, 2022 • edited Loading

sgouezel left a comment

Choose a reason for hiding this comment

sgouezel Dec 26, 2022

Choose a reason for hiding this comment

sterraf Feb 27, 2023

Choose a reason for hiding this comment

sterraf Mar 18, 2023

Choose a reason for hiding this comment

sgouezel left a comment

Choose a reason for hiding this comment

vihdzp left a comment

Choose a reason for hiding this comment

semorrison commented Jul 25, 2023

sterraf commented Dec 17, 2022 •

edited

Loading