Convex exp#873

Merged

affeldt-aist merged 22 commits intomath-comp:masterfrom

affeldt-aist:convex_exp

Apr 20, 2023

Commits on Apr 20, 2023

Introduce conves

yoshihiro503
and
affeldt-aist
committed
proof of second_drivative_convexf_pt

yoshihiro503
authored and
affeldt-aist
committed
proof of second_derivative_convex_pt

yoshihiro503
authored and
affeldt-aist
committed
proof of some lemmas

yoshihiro503
authored and
affeldt-aist
committed
prove Admitted lemmas

yoshihiro503
authored and
affeldt-aist
committed
introduce convex space with `{i01 R}`
affeldt-aist
committed
upd wrt last itv.v
affeldt-aist
committed
add to _CoqProject
affeldt-aist
committed
start solution 1 by zachary
affeldt-aist
committed
complete solution 1 by zachary

committed
minor cleaning
affeldt-aist
committed
minor generalization
affeldt-aist
committed
Update theories/convex.v

affeldt-aist
and
zstone1
committed
Update theories/convex.v

affeldt-aist
and
zstone1
committed
Update theories/convex.v

affeldt-aist
and
zstone1
committed
complete changelog and address comments
affeldt-aist
committed
expR convex
affeldt-aist
committed
fix makefile
affeldt-aist
committed
fix
affeldt-aist
committed
fix
affeldt-aist
committed
fix
affeldt-aist
committed
so that it compiles with mathcomp 1.14
affeldt-aist
committed