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

dirac measure #616

Merged
merged 1 commit into from
May 3, 2022
Merged

dirac measure #616

merged 1 commit into from
May 3, 2022

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Mar 28, 2022 •
edited
Loading

Motivation for this change

Tentative dirac measure.

TODO: doc and changelog DONE

TODO: change the statement of integral_dirac to

Lemma integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) :
  \int_ D (f x) 'd (\d_ a)[x] = (\1_D a)%:E * f a.

as part of PR #620

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
    (do not edit former entries, only append new ones, be careful:
    merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
  • added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@affeldt-aist affeldt-aist marked this pull request as draft March 28, 2022 10:15
@affeldt-aist affeldt-aist mentioned this pull request Mar 29, 2022
Merged
2 tasks
@affeldt-aist affeldt-aist marked this pull request as ready for review March 29, 2022 07:13
This was referenced Mar 29, 2022
Merged
Merged
@affeldt-aist affeldt-aist mentioned this pull request Apr 4, 2022
Merged
2 tasks
@affeldt-aist affeldt-aist force-pushed the dirac_measure branch 2 times, most recently from 50071b5 to 7aab4f1 Compare April 13, 2022 08:22
@affeldt-aist
Copy link
Member Author

Note that the presentation of the theory of this commit will certainly be changed by #646 but not the proof so it is still relevant to review it first.

1 similar comment
@affeldt-aist
Copy link
Member Author

Note that the presentation of the theory of this commit will certainly be changed by #646 but not the proof so it is still relevant to review it first.

proux01
proux01 reviewed May 2, 2022
View reviewed changes
Copy link
Collaborator

@proux01 proux01 left a comment

Choose a reason for hiding this comment

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

LGTM, sorry for those late reviews

theories/lebesgue_integral.v Outdated Show resolved Hide resolved
theories/lebesgue_integral.v Outdated Show resolved Hide resolved
theories/lebesgue_integral.v
Comment on lines +2381 to +2315
Lemma integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) :
D a -> \int_ D (f x) 'd (\d_ a)[x] = f a.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Couldn't this be generalized to something like?

\int_ D (f x) 'd (\d_ a)[x] = (\1_D a)%:E * f a.

Copy link
Member Author

Choose a reason for hiding this comment

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

This is a good idea but it might require lemmas that are part of PR #620.
Allow me to do it as part of PR #620 a bit later.

@proux01
Copy link
Collaborator

proux01 commented May 2, 2022

BTW, the dirac measure should probably be in measure.v rather than lebesgue_integral.v (it seems to be just a matter of requiring numfun to get \1_)

@affeldt-aist
Copy link
Member Author

LGTM, sorry for those late reviews

Definitely no problem. Thank you very much!

@proux01
Copy link
Collaborator

proux01 commented May 3, 2022

Updated CHANGELOG, will merge once CI is green.

@proux01 proux01 merged commit 77b5614 into master May 3, 2022
@proux01 proux01 deleted the dirac_measure branch May 3, 2022 13:49
CohenCyril
CohenCyril reviewed May 3, 2022
View reviewed changes
theories/measure.v
Arguments dirac {T} _ {R}.
Arguments dirac_measure {T} _ {R}.

Notation "\d_ a" := (dirac_measure a) : ring_scope.
Copy link
Member

Choose a reason for hiding this comment

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

I'm worried that this notation is bound to dirac_measure instead of dirac... it looks unstable to me.

CohenCyril
CohenCyril reviewed May 3, 2022
View reviewed changes
theories/measure.v
Arguments dirac {T} _ {R}.
Arguments dirac_measure {T} _ {R}.

Notation "\d_ a" := (dirac_measure a) : ring_scope.
Copy link
Member

Choose a reason for hiding this comment

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

I'm worried that this notation is bound to dirac_measure instead of dirac... it looks unstable to me.

Copy link
Member Author

Choose a reason for hiding this comment

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

Indeed. This is an oversight. This will anyway disappear once PR #646 is rebased.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CohenCyril CohenCyril CohenCyril left review comments

@proux01 proux01 proux01 left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@affeldt-aist @proux01 @CohenCyril