feat(MeasureTheory/Measure/TypeClass/NoAtoms) add `exists_accPt_of_noAtoms` #32851

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 98379c78c5

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 Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

error: the PR title does not contain a colon

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

feat (feature)
fix (bug fix)
doc (documentation)
style (formatting, missing semicolons, ...)
refactor
test (when adding missing tests)
chore (maintain)
perf (performance improvement, optimization, ...)
ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

Data/Nat/Basic
Algebra/Group/Defs
Topology/Constructions

<subject> has the following constraints:

do not capitalize the first letter
no dot(.) at the end
use imperative, present tense: "change" not "changed" nor "changes"

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

Mathlib/MeasureTheory/Measure/Hausdorff.lean

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

Mathlib/MeasureTheory/Measure/Hausdorff.lean

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.

Mathlib/MeasureTheory/Measure/Hausdorff.lean

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean

+ found a simplification

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean

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.

CoolRmal

I think this is ready to be merged after some minor changes.

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean

sgouezel · 2025-12-27T21:13:53Z

Could you close the discussions for which you think they have been dealt with? It helps the reviewers to see what remains to be done.

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>

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 `α`

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean

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]

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

Mathlib/MeasureTheory/Measure/Hausdorff.lean Outdated Show resolved Hide resolved

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

Mathlib/MeasureTheory/Measure/Hausdorff.lean Show resolved Hide resolved

plp127 reviewed Dec 18, 2025

View reviewed changes

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated Show resolved Hide resolved

Refactor exists_accPt_of_noAtoms theorem

23b186d

+ found a simplification

plp127 reviewed Dec 19, 2025

View reviewed changes

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated Show resolved Hide resolved

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 requested a review from CoolRmal December 27, 2025 02:13

CoolRmal reviewed Dec 27, 2025

View reviewed changes

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated Show resolved Hide resolved

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated Show resolved Hide resolved

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated Show resolved Hide resolved

tdwag123 and others added 4 commits December 27, 2025 17:20

Remove redundant TopologicalSpace pt 1

6778dbf

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>

Remove redundant TopologicalSpace pt 2

701c85d

Co-authored-by: Yongxi (Aaron) Lin <97214596+CoolRmal@users.noreply.github.com>

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

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated Show resolved Hide resolved

sgouezel reviewed Jan 2, 2026

View reviewed changes

Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean Outdated Show resolved Hide resolved

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

feat(MeasureTheory/Measure/TypeClass/NoAtoms) add exists_accPt_of_noAtoms #32851

Are you sure you want to change the base?

feat(MeasureTheory/Measure/TypeClass/NoAtoms) add exists_accPt_of_noAtoms #32851

Uh oh!

Conversation

tdwag123 commented Dec 13, 2025 • edited 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 98379c78c5

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 Needs Formatting

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!

CoolRmal left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel commented Dec 27, 2025

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

feat(MeasureTheory/Measure/TypeClass/NoAtoms) add `exists_accPt_of_noAtoms` #32851

feat(MeasureTheory/Measure/TypeClass/NoAtoms) add `exists_accPt_of_noAtoms` #32851

tdwag123 commented Dec 13, 2025 •

edited

Loading

github-actions bot commented Dec 13, 2025 •

edited

Loading

github-actions bot commented Dec 13, 2025 •

edited

Loading