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

[affeldt-aist]

analysis/theories/convex.v

Lines 144 to 164 in f129011

	Hypothesis cvg_left : (f @ b^'-) --> f b.
	Hypothesis cvg_right : (f @ a^'+) --> f a.
	Let L x := f a + factor a b x * (f b - f a).
	Let LE x : a < b -> L x = factor b a x * f a + factor a b x * f b.
	Proof.
	move=> ab; rewrite /L -(@onem_factor _ a) ?lt_eqF// /onem mulrBl mul1r.
	by rewrite -addrA -mulrN -mulrDr (addrC (f b)).
	Qed.
	Let convexf_ptP : a < b -> (forall x, a <= x <= b -> 0 <= L x - f x) ->
	forall t, f (a <| t |> b) <= f a <| t |> f b.
	Proof.
	move=> ab h t; set x := a <| t |> b; have /h : a <= x <= b.
	by rewrite -(conv1 a b) -{1}(conv0 a b) /x !le_line_path//= itv_ge0/=.
	rewrite subr_ge0 => /le_trans; apply.
	by rewrite LE// /x line_pathK ?lt_eqF// convC line_pathK ?gt_eqF.
	Qed.
	Hypothesis HDf : {in `]a, b[, forall x, derivable f x 1}.

This implements "continuity up the endpoints", approach 1.

Other approaches could have been (I am here reproducing contents from the conversion of now merged PR #873):

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.