[Merged by Bors] - feat(MeasureTheory/Measure/TypeClass/NoAtoms): add `exists_accPt_of_noAtoms` by tdwag123 · Pull Request #32851 · leanprover-community/mathlib4

tdwag123 · 2025-12-13T19:51:16Z

feat(MeasureTheory/Measure/TypeClass/NoAtoms): Added a theorem that states If a set has positive measure under an atomless measure, then it has an accumulation point.

Added a lemma in (Topology/DiscreteSubset): If a subset of a topological space has no accumulation points,
then it carries the discrete topology.

Theorem added: exists_accPt_of_pos_hausdorffMeasure
Lemma added: discreteTopology_of_noAccPts

Harmonic's Aristotle gave the initial version of the proofs. I did substantial work shortening the proof from 40 lines and refactoring it into another Lemma.

Special thanks to @plp127 and @CoolRmal for the useful feedback in the PR process.

Co-authored-by: @Aristotle-Harmonic

Added a theorem that states if a set has positive s-dimensional Hausdorff measure, then it has an accumulation point, along with necessary proofs.

feat(MeasureTheory/Measure/Hausdorff) ∀ 𝑠 > 0, ∀ 𝐸 ⊂ 𝑅^𝑛, 𝐻^𝑠 (𝐸)>0 ⇒ ∃ 𝑥 ∈ 𝑅^𝑛 , 𝑥 is an accumulation point of 𝑃(𝐸).

github-actions · 2025-12-13T19:52:27Z

PR summary 17e9ef1cfc

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ discreteTopology_of_noAccPts
+ exists_accPt_of_noAtoms

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

github-actions · 2025-12-13T19:52:38Z

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

I removed the simp using simp? to find the appropriate simp only statement

Refactor the theorem to use a more general type for the set and include separability condition. I tried to take into account the suggestions, but I may have missed some. The theorem needed some bigger reworking after the generalization

generalization and change of location Added a theorem to show that if a set has positive measure under an atomless measure, then it has an accumulation point.

+ found a simplification

Added lemma for discrete topology based on no accumulation points.

Introduce lemma for discrete topology with no AccPts

plp127 · 2025-12-21T15:23:33Z

Can you update the PR title and description?

Removed lemma about discrete topology for sets with no accumulation points.

Moved out of the partial ordering section, factored some variables out the `exists_accPt_of_noAtoms ` theorem

added section wrappers around the theorem to prevent issues with `μ : Measure α` versus the partial measure `α`

Refactor the `exists_accPt_of_noAtoms` theorem for clarity and structure. -Removed the section for the theorem -Changed the assumptions to make them weaker -Changed where the open statements are Still to be done: See if I can refactor and make the assumptions even weaker.

Changed the assumptions for `exists_accPt_of_noAtoms` from [EPseudometricSpace] to [TopologicalSpace X]

Used filters to shorten, as suggested byPatrickMassot Co-authored-by: Patrick Massot <[email protected]>

tdwag123 · 2026-01-29T04:36:14Z

-awaiting-author

sgouezel · 2026-01-29T12:11:26Z

bors r+
Thanks!

@plp127

…oAtoms` (#32851) feat(MeasureTheory/Measure/TypeClass/NoAtoms): Added a theorem that states If a set has positive measure under an atomless measure, then it has an accumulation point. Added a lemma in (Topology/DiscreteSubset): If a subset of a topological space has no accumulation points, then it carries the discrete topology. Theorem added: `exists_accPt_of_pos_hausdorffMeasure` Lemma added: `discreteTopology_of_noAccPts ` **Harmonic's Aristotle gave the initial version of the proofs.** I did substantial work shortening the proof from 40 lines and refactoring it into another Lemma. Special thanks to @plp127 and @CoolRmal for the useful feedback in the PR process. Co-authored-by: @Aristotle-Harmonic Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-01-29T13:00:34Z

This PR was included in a batch that was canceled, it will be automatically retried

@plp127

…oAtoms` (#32851) feat(MeasureTheory/Measure/TypeClass/NoAtoms): Added a theorem that states If a set has positive measure under an atomless measure, then it has an accumulation point. Added a lemma in (Topology/DiscreteSubset): If a subset of a topological space has no accumulation points, then it carries the discrete topology. Theorem added: `exists_accPt_of_pos_hausdorffMeasure` Lemma added: `discreteTopology_of_noAccPts ` **Harmonic's Aristotle gave the initial version of the proofs.** I did substantial work shortening the proof from 40 lines and refactoring it into another Lemma. Special thanks to @plp127 and @CoolRmal for the useful feedback in the PR process. Co-authored-by: @Aristotle-Harmonic Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-01-29T14:04:57Z

Pull request successfully merged into master.

Build succeeded:

@plp127

…oAtoms` (leanprover-community#32851) feat(MeasureTheory/Measure/TypeClass/NoAtoms): Added a theorem that states If a set has positive measure under an atomless measure, then it has an accumulation point. Added a lemma in (Topology/DiscreteSubset): If a subset of a topological space has no accumulation points, then it carries the discrete topology. Theorem added: `exists_accPt_of_pos_hausdorffMeasure` Lemma added: `discreteTopology_of_noAccPts ` **Harmonic's Aristotle gave the initial version of the proofs.** I did substantial work shortening the proof from 40 lines and refactoring it into another Lemma. Special thanks to @plp127 and @CoolRmal for the useful feedback in the PR process. Co-authored-by: @Aristotle-Harmonic Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

@plp127

…oAtoms` (leanprover-community#32851) feat(MeasureTheory/Measure/TypeClass/NoAtoms): Added a theorem that states If a set has positive measure under an atomless measure, then it has an accumulation point. Added a lemma in (Topology/DiscreteSubset): If a subset of a topological space has no accumulation points, then it carries the discrete topology. Theorem added: `exists_accPt_of_pos_hausdorffMeasure` Lemma added: `discreteTopology_of_noAccPts ` **Harmonic's Aristotle gave the initial version of the proofs.** I did substantial work shortening the proof from 40 lines and refactoring it into another Lemma. Special thanks to @plp127 and @CoolRmal for the useful feedback in the PR process. Co-authored-by: @Aristotle-Harmonic Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

tdwag123 added 2 commits December 13, 2025 01:37

feat(add theorem exists_accPt_of_pos_hausdorffMeasure)

967ac90

Added a theorem that states if a set has positive s-dimensional Hausdorff measure, then it has an accumulation point, along with necessary proofs.

Merge pull request #1 from tdwag123/tdwag123-patch-1

21d2882

feat(MeasureTheory/Measure/Hausdorff) ∀ 𝑠 > 0, ∀ 𝐸 ⊂ 𝑅^𝑛, 𝐻^𝑠 (𝐸)>0 ⇒ ∃ 𝑥 ∈ 𝑅^𝑛 , 𝑥 is an accumulation point of 𝑃(𝐸).

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Dec 13, 2025

[pre-commit.ci lite] apply automatic fixes

ca17e63

github-actions Bot added the t-measure-probability Measure theory / Probability theory label Dec 13, 2025

Merge branch 'master' into master

b4348d8

tdwag123 marked this pull request as draft December 13, 2025 20:13

tdwag123 and others added 2 commits December 13, 2025 12:17

Remove simp

25a26ec

I removed the simp using simp? to find the appropriate simp only statement

[pre-commit.ci lite] apply automatic fixes

aede9f0

tdwag123 marked this pull request as ready for review December 13, 2025 20:36

Merge branch 'master' into master

ef18f26

CoolRmal reviewed Dec 14, 2025

View reviewed changes

plp127 reviewed Dec 16, 2025

View reviewed changes

Comment thread Mathlib/MeasureTheory/Measure/Hausdorff.lean Outdated

leanprover-community-bot-assistant assigned urkud Dec 17, 2025

tdwag123 added 2 commits December 17, 2025 14:36

Add theorem for accumulation points in atomless measures,

e1a7b1c

generalization and change of location Added a theorem to show that if a set has positive measure under an atomless measure, then it has an accumulation point.

Revert

36faba8

tdwag123 commented Dec 18, 2025

View reviewed changes

Comment thread Mathlib/MeasureTheory/Measure/Hausdorff.lean

plp127 reviewed Dec 18, 2025

View reviewed changes

Comment thread Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated

Refactor exists_accPt_of_noAtoms theorem

23b186d

+ found a simplification

plp127 reviewed Dec 19, 2025

View reviewed changes

Comment thread Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated

tdwag123 added 2 commits December 18, 2025 21:52

Introduce lemma for discrete topology with no AccPts

06bb893

Added lemma for discrete topology based on no accumulation points.

Merge pull request #2 from tdwag123/tdwag123-patch-3

a117a01

Introduce lemma for discrete topology with no AccPts

tdwag123 requested a review from plp127 December 21, 2025 05:12

tdwag123 changed the title ~~feat(MeasureTheory/Measure/Hausdorff) add exists_accPt_of_pos_hausdorffMeasure~~ feat(MeasureTheory/Measure/TypeClass/NoAtoms) add exists_accPt_of_noAtoms Dec 21, 2025

tdwag123 added 2 commits December 25, 2025 15:32

Delete discreteTopology_of_noAccPts lemma

16a1c8b

Removed lemma about discrete topology for sets with no accumulation points.

Import DiscreteSubset in NoAtoms module

4489eed

tdwag123 added 2 commits December 27, 2025 17:52

Refactor exists_accPt_of_noAtoms theorem + move

4411990

Moved out of the partial ordering section, factored some variables out the `exists_accPt_of_noAtoms ` theorem

Section wrappers around theorem

85f1171

added section wrappers around the theorem to prevent issues with `μ : Measure α` versus the partial measure `α`

sgouezel reviewed Jan 2, 2026

View reviewed changes

Comment thread Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated

sgouezel reviewed Jan 2, 2026

View reviewed changes

Comment thread Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 2, 2026

tdwag123 and others added 4 commits January 7, 2026 23:54

Merge branch 'leanprover-community:master' into master

37fc38f

Weakens assumptions for exists_accPt_of_noAtoms

c480fd3

Changed the assumptions for `exists_accPt_of_noAtoms` from [EPseudometricSpace] to [TopologicalSpace X]

[pre-commit.ci lite] apply automatic fixes

3da4cc9

tdwag123 requested a review from sgouezel January 15, 2026 05:59

Merge branch 'master' into master

333c5e3

tdwag123 requested a review from CoolRmal January 19, 2026 05:31

tdwag123 changed the title ~~feat(MeasureTheory/Measure/TypeClass/NoAtoms) add exists_accPt_of_noAtoms~~ feat(MeasureTheory/Measure/TypeClass/NoAtoms): add exists_accPt_of_noAtoms Jan 22, 2026

Merge branch 'master' into master

fd9ec90

PatrickMassot reviewed Jan 22, 2026

View reviewed changes

Comment thread Mathlib/Topology/DiscreteSubset.lean Outdated

tdwag123 and others added 2 commits January 22, 2026 10:47

Refactored Mathlib/Topology/DiscreteSubset.lean

bb7be35

Used filters to shorten, as suggested byPatrickMassot Co-authored-by: Patrick Massot <[email protected]>

Merge branch 'master' into master

e1198d6

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 29, 2026

Merge branch 'master' into master

4cd9f39

ghost added the ready-to-merge This PR has been sent to bors. label Jan 29, 2026

mathlib-bors Bot changed the title ~~feat(MeasureTheory/Measure/TypeClass/NoAtoms): add exists_accPt_of_noAtoms~~ [Merged by Bors] - feat(MeasureTheory/Measure/TypeClass/NoAtoms): add exists_accPt_of_noAtoms Jan 29, 2026

mathlib-bors Bot closed this Jan 29, 2026

Uh oh!

Conversation

tdwag123 commented Dec 13, 2025 • edited by RemyDegenne Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Dec 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 17e9ef1cfc

Import changes for modified files

Declarations diff

Uh oh!

github-actions Bot commented Dec 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

✅ PR Title Formatted Correctly

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

plp127 commented Dec 21, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tdwag123 commented Jan 29, 2026

Uh oh!

sgouezel commented Jan 29, 2026

Uh oh!

mathlib-bors Bot commented Jan 29, 2026

Uh oh!

mathlib-bors Bot commented Jan 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

tdwag123 commented Dec 13, 2025 •

edited by RemyDegenne

Loading

github-actions Bot commented Dec 13, 2025 •

edited

Loading

github-actions Bot commented Dec 13, 2025 •

edited

Loading