[Merged by Bors] - feat: separation of FiniteMeasure by StarSubalgebra#19782
[Merged by Bors] - feat: separation of FiniteMeasure by StarSubalgebra#19782JakobStiefel wants to merge 101 commits intomasterfrom
FiniteMeasure by StarSubalgebra#19782Conversation
PR summary 210c7a1ce9Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.MeasureTheory.Measure.HasOuterApproxClosed | 1602 | 1991 | +389 (+24.28%) |
Import changes for all files
| Files | Import difference |
|---|---|
5 filesMathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Topology.ContinuousMap.ZeroAtInfty |
1 |
Mathlib.MeasureTheory.Measure.HasOuterApproxClosed |
389 |
Mathlib.Analysis.RCLike.BoundedContinuous (new file) |
1561 |
Mathlib.MeasureTheory.Measure.FiniteMeasureExt (new file) |
2212 |
Declarations diff
+ AlgHom.compLeftContinuousBounded
+ _root_.MonoidHom.compLeftContinuousBounded
+ _root_.RingHom.compLeftContinuousBounded
+ coe_toContinuousMapStarₐ
+ coe_toContinuousMapₐ
+ comp_apply
+ ext_of_forall_integral_eq_of_IsFiniteMeasure
+ ext_of_forall_mem_subalgebra_integral_eq_of_polish
+ ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable
+ instMulOneClass
+ lipschitzWith_ofReal
+ restrict_toContinuousMap_eq_toContinuousMapStar_restrict
+ toContinuousMapStarₐ
+ toContinuousMapₐ
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.
Increase in tech debt: (relative, absolute) = (1.00, 0.04)
| Current number | Change | Type |
|---|---|---|
| 25 | 1 | large files |
Current commit 210c7a1ce9
Reference commit 67019e0bbf
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
FiniteMeasaure by StarSubalgebraFiniteMeasure by StarSubalgebra
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
RemyDegenne
left a comment
There was a problem hiding this comment.
The new approach looks nice!
|
I merged master to fix the conflict introduced by the two PRs about |
|
I fixed it: some statement or file probably moved on master and was not imported anymore. I added an import and that fixed the issue. |
RemyDegenne
left a comment
There was a problem hiding this comment.
Thanks, this is great!
You can merge after resolving a few very minor things.
bors d+
|
✌️ JakobStiefel can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
A `StarSubalgebra` of bounded continuous functions separates finite measures if it separates points. Important result in probability Co-authored-by: Remy Degenne <remydegenne@gmail.com> Co-authored-by: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
FiniteMeasure by StarSubalgebraFiniteMeasure by StarSubalgebra
A `StarSubalgebra` of bounded continuous functions separates finite measures if it separates points. Important result in probability Co-authored-by: Remy Degenne <remydegenne@gmail.com> Co-authored-by: JakobStiefel <73285902+JakobStiefel@users.noreply.github.com>
A
StarSubalgebraof bounded continuous functions separates finite measures if it separates points. Important result in probabilityMulExpNegMulSq#19781MulExpNegMulSq#20604