renaming of `conv`

[affeldt-aist]

https://github.com/math-comp/analysis/blob/0e392b5d36dd33e7e054a9a481bf9f4b17a90ed0/classical/set_interval.v#L340

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

[affeldt-aist]

Note that during this meeting https://github.com/math-comp/analysis/wiki/2026-06-26-Meeting it was decided to use the convention t a * (1 - t) * b so that we can port quickly material from infotheo (https://github.com/affeldt-aist/infotheo)