-
Notifications
You must be signed in to change notification settings - Fork 43
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.
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
Lebesgue Stieltjes measure #677
Conversation
95f619d
to
957048a
Compare
I've just checked out the lemma statements (not the proofs), and it looks pretty neat. The existing |
957048a
to
9981b71
Compare
9981b71
to
6f50236
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A few nitpicks and questions. The only meaningful change to consider would be explicitly building the Sogenfrey Line (in realfun.v
?) instead of the "right_continuous" predicate. It won't change the proofs much either way, so it's easy to deal with it later. Up to you.
41f1a00
to
5d39745
Compare
5d39745
to
c6b28dc
Compare
c6b28dc
to
3b5670a
Compare
db3e705
to
840e030
Compare
840e030
to
31bc05c
Compare
31bc05c
to
bad2809
Compare
a7fd96f
to
4b41e9a
Compare
4b41e9a
to
f47791d
Compare
f47791d
to
30c1217
Compare
30c1217
to
57e8084
Compare
(* x and y are real numbers *) | ||
(* R.-ocitv == display for ocitv_type R *) | ||
(* R.-ocitv.-measurable == semiring of sets of open-closed intervals *) | ||
(* hlength f A := f b - f a with the hull of the set of real *) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should not be called hlength anymore.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This has been renamed to wlength
for weight
(W
is sometimes used in the literature and this seems to correspond to the original idea by Stieltjes, though he may have been using H
at the time in fact).
The lemmas have been reworked a bit so that
the user can get along only with lemmas about lebesgue_measure
,
wlength
does not appear in proof scripts except in the proof of outer regularity
that exhibits wlength
on purpose as far as I can see @zstone1 .
- up to sigma_sub_additive (wip)
- fix intermediate lemma - use continuity hypo
Co-authored-by: [email protected] Co-authored-by: Takafumi Saikawa <[email protected]>
d5653a9
to
3915fa4
Compare
Wouah, CI green, thanks @proux01 |
For what? |
For the constant care to the infrastructure! |
* tentative definition of lebesgue stieltjes measure * cumulative function with HB * put lebesgue_measure proof in module --------- Co-authored-by: IshiguroYoshihiro <[email protected]> Co-authored-by: [email protected] Co-authored-by: Takafumi Saikawa <[email protected]>
* tentative definition of lebesgue stieltjes measure * cumulative function with HB * put lebesgue_measure proof in module --------- Co-authored-by: IshiguroYoshihiro <[email protected]> Co-authored-by: [email protected] Co-authored-by: Takafumi Saikawa <[email protected]>
Motivation for this change
This is an attempt at generalizing
lebesgue_mesure.v
.RFC, FYI @hoheinzollern @IshiguroYoshihiro
We have only replayed the first part so far and plan to work on proving more properties soon.
Co-authored-by: @t6s
Things done/to do
CHANGELOG_UNRELEASED.md
Automatic note to reviewers
Read this Checklist and put a milestone if possible.