renaming of `conv`

[affeldt-aist]

analysis/classical/set_interval.v

Line 340 in 0e392b5

Definition conv a b t : R := (1 - t) * a + t * b.

1. rename to line_path or affine_path

2. add

Definition wadd t a b : R := (1 - t) * a + t * b.

(this is different from the convention of infotheo)
where t is in R
but a t is a number between 0 and 1 in lemmas
for such numbers use the type {i01 _} provided by https://github.com/math-comp/analysis/blob/itv/theories/itv.v
this implies to change the definition of onem

3. add

Definition wavg t u a b : R := (t * a + u * b) / (t + u).

[t6s]

We could also try to incorporate a quaternary definition of the convex combination operator as in (Stone, 1949).

The factory for this structure would look like this:

HB.factory Record isConvexSpace (T : Type) := {
  convexspacechoiceclass : Choice.class_of T ;
  conv : Rpos -> Rpos -> T -> T -> T ;
  conv0 : forall p a b, conv p 0%:pr a b = a ;
  convmm : forall p a, conv p p a a = a ;
  convA : forall (p q r : prob) (a b c : T),
     conv (p+q) r (conv p q a b) c = conv (q+r) p (conv r q c b) a ;

  unscale lambda p q a b : conv (lambda*p) (lambda*q) a b = conv p q a b ;
}

The basic mixin of convex spaces would then have both ternary and quaternary operators and an equality axiom between the two.

(Should we further include the n-ary operator in the mixin?)

[affeldt-aist]

Partly addressed by #875