Skip to content

[Merged by Bors] - feat: Properties of the Integral of MulExpNegMulSq#19781

Closed
JakobStiefel wants to merge 68 commits intomasterfrom
Stiefel_MulExpNegMulSq
Closed

[Merged by Bors] - feat: Properties of the Integral of MulExpNegMulSq#19781
JakobStiefel wants to merge 68 commits intomasterfrom
Stiefel_MulExpNegMulSq

Conversation

@JakobStiefel
Copy link
Copy Markdown
Collaborator

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

Show convergence properties of the Integral of MulExpNegMulSq wrt finite measures, important for the proof of separation of finite measures by subalgebras of functions

Open in Gitpod

@JakobStiefel JakobStiefel added t-analysis Analysis (normed *, calculus) t-measure-probability Measure theory / Probability theory labels 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
Copy link
Copy Markdown

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

PR summary 32eb8d71a0

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral (new file) 2136

Declarations diff

+ abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt
+ abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure
+ dist_integral_mulExpNegMulSq_comp_le
+ dist_triangle8
+ exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints
+ ext_of_forall_integral_eq
+ integrable_mulExpNegMulSq_comp
+ integrable_mulExpNegMulSq_comp_restrict_of_isCompact
+ integral_mulExpNegMulSq_comp_eq
+ norm_integral_sub_setIntegral_le
+ tendsto_integral_filter_of_norm_le_const
+ tendsto_integral_mulExpNegMulSq_comp
+ tendsto_integral_mul_one_plus_inv_smul_sq_pow

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
Closed
Closed
Closed
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 7, 2024
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Dec 8, 2024

The file Mathlib/Analysis/SpecialFunctions/MulExpNegSq.lean that you are introducing contains a bunch of results, in many directions and with a log of imports. It would probably be a good idea to have one basic file containing just the basic properties of the function (without any measure theory, say), and another file devoted to its properties wrt integration.

Do you think you could do such a split, and extract a PR just devoted to the first file, i.e., basic properties of the function? This would be easier and quicker to review -- in general, aiming for PRs of less than 200 lines if possible is a good idea, as reviewers will be more inclined to review it.

@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 8, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 10, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Feb 10, 2025

This PR/issue depends on:

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 10, 2025
@JakobStiefel JakobStiefel removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 11, 2025
RemyDegenne
RemyDegenne reviewed Feb 13, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@RemyDegenne RemyDegenne left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here are a bunch of comments about style.

RemyDegenne
RemyDegenne reviewed Feb 13, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@RemyDegenne RemyDegenne left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't have much to say about the mathematical content of the PR, which looks good. But here is another round of comments, again mostly about style and names.

@RemyDegenne RemyDegenne added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 13, 2025
@JakobStiefel JakobStiefel removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 13, 2025
RemyDegenne
RemyDegenne approved these changes Feb 14, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@RemyDegenne RemyDegenne left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 14, 2025

✌️ JakobStiefel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 14, 2025
@JakobStiefel
Copy link
Copy Markdown
Collaborator Author

JakobStiefel commented Feb 14, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Feb 14, 2025
@JakobStiefel
feat: Properties of the Integral of MulExpNegMulSq (#19781)
0efc5f6 
Show convergence properties of the Integral of `MulExpNegMulSq` wrt finite measures, important for the proof of separation of finite measures by subalgebras of functions
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 14, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Properties of the Integral of MulExpNegMulSq [Merged by Bors] - feat: Properties of the Integral of MulExpNegMulSq Feb 14, 2025
@mathlib-bors mathlib-bors bot closed this Feb 14, 2025
@mathlib-bors mathlib-bors bot deleted the Stiefel_MulExpNegMulSq branch February 14, 2025 11:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@RemyDegenne RemyDegenne RemyDegenne approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus) t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@JakobStiefel @sgouezel @mathlib4-dependent-issues-bot @RemyDegenne @leanprover-community-bot-assistant