Convex exp #873

affeldt-aist · 2023-03-13T17:16:07Z

Motivation for this change

This is a continuation of PR #794 (I have duplicated the PR because it looks like I cannot push commits to it).
On top of PR #794, it introduces convex spaces and use the type {i01 R} from the PR #869.

This PR introduce convexs spaces, show that lmodType form instances, and use them to show that a function with a non-negative second derivative is convex (like the exponential function @hoheinzollern).

closes #794

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-03-13T17:20:17Z

theories/convex.v

+Definition derivable_interval {R : numFieldType} (f : R -> R) (a b : R) :=
+  forall x, x \in `[a, b] -> derivable f x 1.


[NB: review comment by @zstone1 copied verbatim from PR #794]

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.

1. 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.

The last two commits implement this solution.
(Hopefully, we think that you wrote cvg (at_right a f^`()) but actually meant cvg (at_right a f).)
Is it in the right direction? @zstone1

affeldt-aist · 2023-03-13T17:21:46Z

theories/convex.v

+Section twice_derivable_convex.
+Context {R : realType}.
+Variables (f : R -> R^o) (a b : R^o).


[NB: review comment by @zstone1 copied verbatim from PR #794 ]

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.

Where do we need the assumption that the range of f is R?

We at least need to be able to compare to 0 but I maybe need to spend more time.

affeldt-aist · 2023-03-13T17:23:00Z

[NB: review comment by @zstone1 copied verbatim from PR https://github.com//pull/794 ]

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.

hoheinzollern · 2023-03-17T16:35:30Z

On top of being helpful for the exponential function, definitions about convexity are also necessary for the formalization of Hoelder's inequality and the special case of Cauchy Schwarz's inequality from PR #790.

zstone1

Much improved from before.

It looks like all the endpoint conditions all make sense. It should now work correctly for the indicator function on [0,1]
I generalized a few things to topologicalType.
Happy to see the generalization to convex spaces.

Other than the small generalizations, looks good to me.

theories/convex.v

affeldt-aist · 2023-04-10T04:18:06Z

Many thanks for the review!

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Co-authored-by: Alessandro Bruni <alessandro.bruni@gmail.com> Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>

Co-authored-by: zstone1 <zstonex@gmail.com>

* Introduce convex - introduce convex spaces - proof of second_derivative_convex_pt - using `{i01 R}` - expR convex Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp> Co-authored-by: Alessandro Bruni <alessandro.bruni@gmail.com> Co-authored-by: Takafumi Saikawa <tscompor@gmail.com> Co-authored-by: zstone1 <zstonex@gmail.com> Co-authored-by: Yoshihiro Imai <y.imai@aist.go.jp>

CohenCyril · 2023-08-17T08:25:01Z

theories/exp.v

+Lemma convex_expR (t : {i01 R}) (a b : R^o) : a <= b ->
+  expR (a <| t |> b) <= (expR a : R^o) <| t |> (expR b : R^o).


@affeldt-aist the multiplications of such lemmas call for a notion of convex function (or convex function on a given domain)

CohenCyril · 2023-08-17T08:26:32Z

theories/realfun.v

+(*   derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and       *)
+(*                                        continuous up to the boundary       *)


Unfortunately {in `]x, y[, forall x, derivable f x 1} does not mean f is derivable on `]x, y[ 🤷

affeldt-aist commented Mar 13, 2023

View reviewed changes

affeldt-aist mentioned this pull request Mar 13, 2023

Introduce convex function on real numbers #794

Closed

2 tasks

affeldt-aist changed the base branch from master to itv March 13, 2023 17:25

affeldt-aist added this to the 0.6.2 milestone Mar 13, 2023

affeldt-aist mentioned this pull request Mar 14, 2023

conv -> line_path #875

Merged

2 tasks

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

affeldt-aist changed the base branch from itv to master March 15, 2023 15:31

affeldt-aist force-pushed the convex_exp branch from 577b4ba to a540fbb Compare March 15, 2023 15:47

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 requested a review from zstone1 April 7, 2023 04:51

zstone1 approved these changes Apr 7, 2023

View reviewed changes

theories/convex.v Outdated Show resolved Hide resolved

theories/convex.v Outdated Show resolved Hide resolved

theories/convex.v Outdated Show resolved Hide resolved

theories/convex.v Outdated Show resolved Hide resolved

affeldt-aist force-pushed the convex_exp branch from 787c833 to d40b4ec Compare April 13, 2023 10:13

yoshihiro503 and others added 14 commits April 20, 2023 14:21

Introduce conves

4922657

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

proof of second_drivative_convexf_pt

c4d0655

proof of second_derivative_convex_pt

c5740a5

proof of some lemmas

4800c81

prove Admitted lemmas

e3c49de

introduce convex space with {i01 R}

19073d6

upd wrt last itv.v

5292705

add to _CoqProject

3ee73c6

start solution 1 by zachary

0234e48

complete solution 1 by zachary

4ab60d7

Co-authored-by: Alessandro Bruni <alessandro.bruni@gmail.com> Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>

minor cleaning

3731788

minor generalization

d8a3c48

Update theories/convex.v

c9cad66

Co-authored-by: zstone1 <zstonex@gmail.com>

Update theories/convex.v

796e84b

Co-authored-by: zstone1 <zstonex@gmail.com>

affeldt-aist and others added 3 commits April 20, 2023 14:21

Update theories/convex.v

3504ef2

Co-authored-by: zstone1 <zstonex@gmail.com>

complete changelog and address comments

055ad41

expR convex

4ac9f43

affeldt-aist force-pushed the convex_exp branch from d40b4ec to 4ac9f43 Compare April 20, 2023 05:26

affeldt-aist added 5 commits April 20, 2023 15:26

fix makefile

79349e6

fix

603ccf3

fix

e9b175f

fix

2348f94

so that it compiles with mathcomp 1.14

ad69e9b

affeldt-aist merged commit f129011 into math-comp:master Apr 20, 2023

affeldt-aist mentioned this pull request Apr 20, 2023

introduce {within [a, b], derivable f}` or/and "differentiable from the right/left at a/b" #904

Open

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 Apr 29, 2023

CohenCyril reviewed Aug 17, 2023

View reviewed changes

CohenCyril mentioned this pull request Oct 2, 2023

Wrong documentation? #1038

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Convex exp #873

Convex exp #873

affeldt-aist commented Mar 13, 2023 •

edited

Loading

affeldt-aist Mar 13, 2023

affeldt-aist Mar 29, 2023 •

edited

Loading

affeldt-aist Mar 13, 2023

affeldt-aist Apr 3, 2023

affeldt-aist commented Mar 13, 2023

hoheinzollern commented Mar 17, 2023

zstone1 left a comment

affeldt-aist commented Apr 10, 2023

CohenCyril Aug 17, 2023

CohenCyril Aug 17, 2023 •

edited

Loading

		Definition derivable_interval {R : numFieldType} (f : R -> R) (a b : R) :=
		forall x, x \in `[a, b] -> derivable f x 1.

		Lemma convex_expR (t : {i01 R}) (a b : R^o) : a <= b ->
		expR (a <\| t \|> b) <= (expR a : R^o) <\| t \|> (expR b : R^o).

		(* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *)
		(* continuous up to the boundary *)

Convex exp #873

Convex exp #873

Conversation

affeldt-aist commented Mar 13, 2023 • edited Loading

Motivation for this change

Things done/to do

Automatic note to reviewers

affeldt-aist Mar 13, 2023

Choose a reason for hiding this comment

affeldt-aist Mar 29, 2023 • edited Loading

Choose a reason for hiding this comment

affeldt-aist Mar 13, 2023

Choose a reason for hiding this comment

affeldt-aist Apr 3, 2023

Choose a reason for hiding this comment

affeldt-aist commented Mar 13, 2023

hoheinzollern commented Mar 17, 2023

zstone1 left a comment

Choose a reason for hiding this comment

affeldt-aist commented Apr 10, 2023

CohenCyril Aug 17, 2023

Choose a reason for hiding this comment

CohenCyril Aug 17, 2023 • edited Loading

Choose a reason for hiding this comment

affeldt-aist commented Mar 13, 2023 •

edited

Loading

affeldt-aist Mar 29, 2023 •

edited

Loading

CohenCyril Aug 17, 2023 •

edited

Loading