-
Notifications
You must be signed in to change notification settings - Fork 44
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
Introduce convex function on real numbers #794
Conversation
2343aae
to
3889af7
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.
Nice results. I've made comments about a couple generalizations, one regarding annoying endpoint issues, the other regarding generalizing to vector space ranges. I care more about the endpoints one mostly because it's much harder to fix later. Happy to work with you on that if that'd be helpful.
(* ^^^ probability ^^^ *) | ||
|
||
Definition derivable_interval {R : numFieldType}(f : R -> R) (a b: R) := | ||
forall x, x \in `[a, b] -> derivable f x 1. |
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 definition misbehaves at the endpoints. In particular, it requires f
to be be "differentiable from the left at a
". That makes this definition rely on values of f
outside [a,b]
. One big consequence is characteristic functions like if x \in `[a,b] then 1 else 0
fails this definition, as its not derivable at a
or b
. For what it's worth, I had an analogous issue with realfun.v
, see #752 for how I addressed it there. You'll need something slightly different here, though.
I've seen textbooks take these approaches:
- Demanding "continuity up the endpoints" is one approach
forall x, x \in `]a, b[ -> derivable f x 1.
/\
cvg (at_right a f^`()) /\ cvg (at_right b f^`())
or some variation of this. However, this implies some continuity of the derivative, which is maybe not ideal.
2. We could change the derivative to use a different topology. One way to do that is add an analog to the {within `[a,b], continuous f}
notation of {within `[a,b], derivable f}
. This would take limits only on the subspace topology.
3. Similarly, but specialized to working in R
, it should be fine to define it like
forall x, x \in `]a, b[ -> derivable f x 1
/\
"differentiable from the right at b" /\ "differentiable from the left at a"
For some sensible notion of "left" and "right" derivative.
Section twice_derivable_convex. | ||
|
||
Variable R : realType. | ||
Variables (f : R -> R) (a b : R). |
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.
Where do we need the assumption that the range of f
is R
? If it's painless, generalizing to a vector space would be quite helpful for me. I'll need some stuff about convexity in both R
and R^n
for my work on space-filling curves, so I'm happy to have these results either way.
Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
d8ea758
to
2dad201
Compare
Co-authored-by: Reynald Affeldt reynald.affeldt@aist.go.jp
Motivation for this change
Things done/to do
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
)Automatic note to reviewers
Read this Checklist and put a milestone if possible.