tentative proof of Radon-Nikodym #818

affeldt-aist · 2023-01-03T14:10:05Z

Motivation for this change

~~based on PR #777 (it seems that I cannot change the base of this PR because 777 is coming from a git repo that is not MathComp-Analysis, that's why the two commits from 777 appear again here)~~

~~this PR changes the definition of measure_ge0 by adding a measurable hypothesis which is not unreasonable but might be avoided @CohenCyril~~ (problem solved)

~~This PR actually duplicates a few lemmas from PR #914 that should be removed before merging.~~ DONE

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 · 2023-05-23T04:41:28Z

ping @zstone1 (the remaining errors in the CI are not from this PR)

zstone1 · 2023-05-25T16:12:08Z

Sorry for the delay, I expect to have some time for a review this weekend.

zstone1

It seems like a pretty faithful formalization of the textbook proof. I'm happy with the overall structure, and putting all these one-time use definitions into a module is a good idea for sure. I found one moderate simplification regarding fRN + eps. Basically shuffling the int fRN x + eps to int fRN x + int eps before the integrableP saves some headache. There are probably a few other similar proof improvements in the proof of radon_nikodym_finite, but I didn't find any trivial ones.

zstone1 · 2023-05-28T17:18:26Z

theories/charge.v

+  + apply/integrableP; split.
+      suff: measurable_fun setT (fun x => fRN x + epsRN%:num%:E).
+        exact: measurable_funS.
+      by apply: emeasurable_funD => //; exact: measurable_fun_fRN.
+    apply: (@le_lt_trans _ _ (\int[mu]_(x in \bigcup_k H k) `|fRN x| +
+       \int[mu]_(x in \bigcup_k H k)`| epsRN%:num%:E |)).
+      rewrite -(integralD mUH); last 2 first.
+        * apply: integrable_abse; apply/integrableP; split.
+            exact: measurable_funS measurable_fun_fRN.
+          rewrite (le_lt_trans _ int_fRN_lty)// subset_integral//.
+          by apply: measurableT_comp => //; exact: measurable_fun_fRN.
+        * apply: integrable_abse; apply/integrableP; split => //.
+          by rewrite integral_cst//= lte_mul_pinfty// ltey_eq fin_num_measure.
+      apply: ge0_le_integral => //.
+      * apply: measurableT_comp => //; apply: emeasurable_funD => //.
+        exact: measurable_funS measurable_fun_fRN.
+      * apply: emeasurable_funD => //; apply: measurableT_comp => //.
+        exact: measurable_funS measurable_fun_fRN.
+      * by move=> x _; exact: lee_abs_add.
+    apply: lte_add_pinfty.
+      rewrite (le_lt_trans _ int_fRN_lty)// subset_integral//.
+      by apply: measurableT_comp => //; exact: measurable_fun_fRN.
+    by rewrite integral_cst//= lte_mul_pinfty// ltey_eq fin_num_measure.


Suggested change

+ apply/integrableP; split.

suff: measurable_fun setT (fun x => fRN x + epsRN%:num%:E).

exact: measurable_funS.

by apply: emeasurable_funD => //; exact: measurable_fun_fRN.

apply: (@le_lt_trans _ _ (\int[mu]_(x in \bigcup_k H k) `|fRN x| +

\int[mu]_(x in \bigcup_k H k)`| epsRN%:num%:E |)).

rewrite -(integralD mUH); last 2 first.

* apply: integrable_abse; apply/integrableP; split.

exact: measurable_funS measurable_fun_fRN.

rewrite (le_lt_trans _ int_fRN_lty)// subset_integral//.

by apply: measurableT_comp => //; exact: measurable_fun_fRN.

* apply: integrable_abse; apply/integrableP; split => //.

by rewrite integral_cst//= lte_mul_pinfty// ltey_eq fin_num_measure.

apply: ge0_le_integral => //.

* apply: measurableT_comp => //; apply: emeasurable_funD => //.

exact: measurable_funS measurable_fun_fRN.

* apply: emeasurable_funD => //; apply: measurableT_comp => //.

exact: measurable_funS measurable_fun_fRN.

* by move=> x _; exact: lee_abs_add.

apply: lte_add_pinfty.

rewrite (le_lt_trans _ int_fRN_lty)// subset_integral//.

by apply: measurableT_comp => //; exact: measurable_fun_fRN.

by rewrite integral_cst//= lte_mul_pinfty// ltey_eq fin_num_measure.

+ apply: integrableD => //.

(apply: integrableS; first exact: measurableT) => //; apply /integrableP.

by split; [exact: measurable_fun_fRN | exact: int_fRN_lty].

apply/integrableP; split; rewrite // integral_cst // lte_mul_pinfty //.

by rewrite ltey_eq fin_num_measure.

Oh! Thanks. I committed your suggestion after a rebase: 0a13408

There are probably a few other similar proof improvements in the proof of radon_nikodym_finite, but I didn't find any trivial ones.

I still have to take some time to look for more simplifications.

CohenCyril

Really nice. Just two small remarks (in addition to @zstone1's).

theories/measure.v

CohenCyril · 2023-05-29T13:57:35Z

theories/charge.v

+  exists2 f : T -> \bar R, mu.-integrable [set: T] f &
+    forall E, measurable E -> nu E = \int[mu]_(x in E) f x.


Should we extract this existential and have a function Randon_Nikodym mu nu that is mu.-integrable and such that:

forall E, measurable E -> nu E = \int[mu]_(x in E) Radon_Nikodym mu nu x.

?

That would indeed look better. Here is a first try: 04dfc2c

Indeed it looks better...
I guess the code would be slightly shorter if you used the same Theorem Radon_Nikodym as before (renaming it) but extracted the witness out of it, rather than having both a long definition and proof for extracting the existential.

Co-authored-by: IshiguroYoshihiro

Co-authored-by: Zachary Stone <[email protected]>

CohenCyril · 2023-06-07T08:34:26Z

CHANGELOG_UNRELEASED.md

+  + definitions `jordan_neg`, `jordan_pos`
+  + lemmas `jordan_decomp`, `jordan_pos_dominates`, `jordan_neg_dominates`
+  + lemma `radon_nikodym_finite`
+  + definition `Radon_Nikodym`, notation `'d nu /d mu`


Where is the notation defined?
If you define it, which I think is nice, we must put it in a special scope because we might want the same kind of notation for partial derivatives someday.

Yes, I messed up with my commits, wait a minute.

- add notation Co-authored-by: IshiguroYoshihiro

CohenCyril

I'm fine with the changes. And root for merging.

(I involuntarily re-requested a review by @zstone1 but since he approved before I think we're good to merge?)

affeldt-aist · 2023-06-07T13:31:30Z

Thank for the careful reviews! @zstone1 @CohenCyril

* proof of Radon-Nikodym Co-authored-by: IshiguroYoshihiro Co-authored-by: Zachary Stone <[email protected]>

* tentative proof of Radon-Nikodym (#818) * proof of Radon-Nikodym Co-authored-by: IshiguroYoshihiro Co-authored-by: Zachary Stone <[email protected]> * fix for charge.v - added Monoid.isLaw instance for maxe --------- Co-authored-by: Zachary Stone <[email protected]>

* proof of Radon-Nikodym Co-authored-by: IshiguroYoshihiro Co-authored-by: Zachary Stone <[email protected]>

affeldt-aist force-pushed the radon_nikodym branch 2 times, most recently from 5ba0046 to 0d8a631 Compare February 6, 2023 03:02

affeldt-aist force-pushed the radon_nikodym branch 3 times, most recently from c4c5f80 to 038b28f Compare February 15, 2023 07:02

affeldt-aist force-pushed the radon_nikodym branch 2 times, most recently from 245e696 to ea73299 Compare February 17, 2023 05:07

affeldt-aist marked this pull request as ready for review February 17, 2023 05:09

affeldt-aist added this to the 0.6.2 milestone Feb 23, 2023

affeldt-aist force-pushed the radon_nikodym branch from ea73299 to 3a9883b Compare February 24, 2023 14:21

affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Mar 15, 2023

affeldt-aist force-pushed the radon_nikodym branch from 3a9883b to 87263bc Compare March 19, 2023 00:24

CohenCyril added the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Mar 27, 2023

affeldt-aist modified the milestones: 0.6.2, 0.6.3 Apr 10, 2023

affeldt-aist force-pushed the radon_nikodym branch 4 times, most recently from 9b1dc60 to 5d93a32 Compare April 27, 2023 16:54

affeldt-aist requested a review from zstone1 April 27, 2023 17:11

affeldt-aist force-pushed the radon_nikodym branch 3 times, most recently from 0b77ec7 to 4d1c934 Compare May 20, 2023 08:06

zstone1 approved these changes May 28, 2023

View reviewed changes

CohenCyril approved these changes May 29, 2023

View reviewed changes

affeldt-aist force-pushed the radon_nikodym branch from 3ee3745 to 04dfc2c Compare June 2, 2023 05:01

affeldt-aist added 2 commits June 7, 2023 17:20

tentative proof of Radon-Nikodym

0ad046b

Co-authored-by: IshiguroYoshihiro

clean, changelog

a9d77c8

affeldt-aist and others added 5 commits June 7, 2023 17:22

fix

efcd718

fix

0b4b884

fix

c71aa74

fix to compile with 8.14+1.14.0

520c047

simplification by Zachary

54ba33b

Co-authored-by: Zachary Stone <[email protected]>

affeldt-aist force-pushed the radon_nikodym branch from 04dfc2c to c02a98f Compare June 7, 2023 08:28

CohenCyril reviewed Jun 7, 2023

View reviewed changes

add a definition of RN derivative

405fd3a

- add notation Co-authored-by: IshiguroYoshihiro

affeldt-aist force-pushed the radon_nikodym branch from c02a98f to 405fd3a Compare June 7, 2023 08:40

affeldt-aist added 2 commits June 7, 2023 17:42

fix format

c6dfc9a

dominates -> measure_dominates

bdcce06

CohenCyril requested review from CohenCyril and zstone1 June 7, 2023 09:55

CohenCyril approved these changes Jun 7, 2023

View reviewed changes

for compilation with coq < 8.17

b4c611b

zstone1 approved these changes Jun 7, 2023

View reviewed changes

affeldt-aist merged commit 17eea58 into math-comp:master Jun 7, 2023

affeldt-aist added a commit to affeldt-aist/analysis that referenced this pull request Jun 8, 2023

tentative proof of Radon-Nikodym (math-comp#818)

ccf4a63

* proof of Radon-Nikodym Co-authored-by: IshiguroYoshihiro Co-authored-by: Zachary Stone <[email protected]>

proux01 removed the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Jun 8, 2023

IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this pull request Sep 7, 2023

tentative proof of Radon-Nikodym (math-comp#818)

791471f

* proof of Radon-Nikodym Co-authored-by: IshiguroYoshihiro Co-authored-by: Zachary Stone <[email protected]>

		exists2 f : T -> \bar R, mu.-integrable [set: T] f &
		forall E, measurable E -> nu E = \int[mu]_(x in E) f x.

tentative proof of Radon-Nikodym #818

tentative proof of Radon-Nikodym #818

Uh oh!

Conversation

affeldt-aist commented Jan 3, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Motivation for this change

Things done/to do

Automatic note to reviewers

Uh oh!

affeldt-aist commented May 23, 2023

Uh oh!

zstone1 commented May 25, 2023

Uh oh!

zstone1 left a comment

Choose a reason for hiding this comment

Uh oh!

zstone1 May 28, 2023

Choose a reason for hiding this comment

Uh oh!

affeldt-aist Jun 2, 2023

Choose a reason for hiding this comment

Uh oh!

affeldt-aist Jun 2, 2023

Choose a reason for hiding this comment

Uh oh!

CohenCyril left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

CohenCyril May 29, 2023

Choose a reason for hiding this comment

Uh oh!

affeldt-aist Jun 2, 2023

Choose a reason for hiding this comment

Uh oh!

CohenCyril Jun 5, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

CohenCyril Jun 7, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

affeldt-aist Jun 7, 2023

Choose a reason for hiding this comment

Uh oh!

CohenCyril left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

affeldt-aist commented Jun 7, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

affeldt-aist commented Jan 3, 2023 •

edited

Loading

CohenCyril left a comment •

edited

Loading

CohenCyril Jun 5, 2023 •

edited

Loading

CohenCyril Jun 7, 2023 •

edited

Loading

CohenCyril left a comment •

edited

Loading