Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: results on inner regularity of finite measures #19780

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat: results on inner regularity of finite measures #19780

wants to merge 19 commits into from
+324 −0

Conversation

JakobStiefel
Copy link
Collaborator

@JakobStiefel JakobStiefel commented Dec 7, 2024 •
edited
Loading

in a PseudoEMetricSpace and CompleteSpace with SecondCountableTopology, any finite measure is inner regular with respect to compact sets. In other words, finite measures are tight. Important result in probability

Open in Gitpod

@JakobStiefel JakobStiefel added the t-measure-probability Measure theory / Probability theory label Dec 7, 2024
@github-actions 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 7, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Dec 7, 2024 •
edited
Loading

PR summary 49b22c3003

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.MeasureTheory.Measure.RegularityCompacts (new file) 1368

Declarations diff

+ InnerRegularCompactLTTop_of_polishSpace
+ InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable
+ InnerRegular_of_polishSpace
+ InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable
+ PolishSpace.innerRegular_isCompact_isClosed_measurableSet
+ exists_isCompact_closure_measure_compl_lt
+ exists_measure_iInter_lt
+ innerRegularWRT_isCompact
+ innerRegularWRT_isCompact_closure
+ innerRegularWRT_isCompact_closure_iff
+ innerRegularWRT_isCompact_closure_of_univ
+ innerRegularWRT_isCompact_isClosed
+ innerRegularWRT_isCompact_isClosed_iff
+ innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure
+ innerRegularWRT_isCompact_isClosed_isOpen
+ innerRegularWRT_isCompact_isOpen
+ innerRegularWRT_of_exists_compl_lt
+ innerRegular_isCompact_isClosed_measurableSet_of_finite
+ interUnionBalls
+ isCompact_closure_interUnionBalls
+ tendsto_atTop_zero_iff_le_of_antitone
+ tendsto_atTop_zero_iff_lt_of_antitone
+ totallyBounded_interUnionBalls

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).

This was referenced Dec 7, 2024
Open
Open
Open
Open
@sgouezel
Copy link
Contributor

sgouezel commented Dec 8, 2024

The PR text is a little bit misleading, as it's not true in general that a finite measure is inner regular wrt compact sets in an emetric space: you need completeness and second countability assumptions (i.e., a polish space), right? Can you adjust the PR text, and the docstring in the file?

I'm also a little bit confused by the fact that the author of the PR is not mentioned as one of the authors of the main file. Can you explain what is going on here?

And thanks for PRing this, this is an important result that should definitely be in mathlib!

@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes label Dec 8, 2024
@JakobStiefel JakobStiefel changed the title feat: inner regularity of finite measures wrt compact sets feat: results on inner regularity of finite measures Dec 10, 2024
JakobStiefel and others added 3 commits December 10, 2024 12:08
@JakobStiefel
clarify docstring
8b770f0
@JakobStiefel @github-actions
remove blank space
c7917a8 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@JakobStiefel @github-actions
remove blank space
2fdf7e7 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@JakobStiefel
Copy link
Collaborator Author

I'm also a little bit confused by the fact that the author of the PR is not mentioned as one of the authors of the main file. Can you explain what is going on here?

The file is originally fom https://github.com/RemyDegenne/kolmogorov_extension4, which isn't a pull request yet. I copied the needed file with the permission of Peter Pfaffelhuber in order to proceed the work on separation of finite measures, #19782.

@JakobStiefel JakobStiefel removed the awaiting-author A reviewer has asked the author a question or requested changes label Dec 10, 2024
sgouezel
sgouezel reviewed Dec 11, 2024
View reviewed changes
Mathlib/MeasureTheory/Measure/MeasureSpace.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Measure/RegularityCompacts.lean Show resolved Hide resolved
@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes label Dec 11, 2024
@JakobStiefel JakobStiefel removed the awaiting-author A reviewer has asked the author a question or requested changes label Dec 18, 2024
@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes label Dec 18, 2024
@JakobStiefel JakobStiefel removed the awaiting-author A reviewer has asked the author a question or requested changes label Dec 18, 2024
@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 4, 2025
@JakobStiefel JakobStiefel removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 7, 2025
@sgouezel
Copy link
Contributor

sgouezel commented Jan 7, 2025

bors r+
Thanks!

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 7, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 7, 2025
@JakobStiefel
feat: results on inner regularity of finite measures (#19780)
3e203da 
in a `PseudoEMetricSpace` and `CompleteSpace` with `SecondCountableTopology`, any finite measure is inner regular with respect to compact sets. In other words, finite measures are tight. Important result in probability 



Co-authored-by: JakobStiefel <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 7, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: results on inner regularity of finite measures [Merged by Bors] - feat: results on inner regularity of finite measures Jan 7, 2025
@mathlib-bors mathlib-bors bot closed this Jan 7, 2025
@mathlib-bors mathlib-bors bot deleted the Stiefel_RegularityCompacts branch January 7, 2025 18:04
Julian added a commit that referenced this pull request Jan 8, 2025
@Julian
Merge remote-tracking branch 'origin/master' into emultiplicity-of-nat
53d4c08 
* origin/master: (642 commits)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  feat(Analysis/Analytic): lemmas about `smul` for power series (#19816)
  chore: don't import algebra in `Data.Multiset.Basic` (#19775)
  ...
Julian added a commit that referenced this pull request Jan 8, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
0ae6406 
* origin/master: (80 commits)
  chore(CategoryTheory): remove data produced by tactic block (#20565)
  feat: `|∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ` (#20540)
  feat: the Boolean subalgebra generated by the lattice generated by a set (#20440)
  feat: misc. lemmas about moments, tilted measures (#20150)
  chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556)
  feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373)
  feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377)
  chore: scope 'on' notation to Function (#20562)
  chore: disable docPrime linter (#20559)
  chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557)
  fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539)
  chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551)
  feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542)
  chore(Noetherian/Artinian): generalize to Semiring (#20534)
  chore: protect `Filter.nhds_{iInf,inf}` (#20530)
  chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511)
  chore: extract 3 new files out of MeasureSpace (#20509)
  feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326)
  doc(RingTheory/Flat): add reference to Lambek's paper (#20266)
  feat(NumberTheory/AbelSummation): add more results (#19942)
  chore(Multilinear/Basic): generalize the `SMul` instance (#20536)
  feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516)
  feat(ContDiff): add `iteratedFDeriv_comp` (#20472)
  feat(LowerUpperTopology): add lemmas (#20465)
  feat(ContDiff): weaken some assumptions (#20368)
  fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
  chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528)
  feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089)
  feat: results on inner regularity of finite measures (#19780)
  chore: to_additive various results on groups, group actions (#20547)
  feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466)
  chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553)
  perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524)
  fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529)
  chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535)
  feat(RingTheory): being unramified is a local property (#20323)
  chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439)
  feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970)
  chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521)
  feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255)
  chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235)
  chore: don't import algebra in `Data.Finset.Basic` (#19779)
  feat: initial segment commutes with `Iio` (#20503)
  chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215)
  chore: smile more often (#20436)
  chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416)
  feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007)
  doc: change "module homomorphism" to "linear map" (#20481)
  perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519)
  fix: do not keep only the first line of hints (#19756)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees
No one assigned
Labels
new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@JakobStiefel @sgouezel @leanprover-community-mathlib4-bot