Missing theory for Hoelder conjugates

[hoheinzollern]

This would much improve the presentation of Minkowski's inequality and therefore PR #1000

Here is a draft by @affeldt-aist

Section hoelder_conjugate.
Context {R : realType}.
Local Open Scope ereal_scope.

Definition hoelder_conj (p : \bar R) :=
  match p with
  | +oo => 1
  | -oo => 1
  | r%:E => if r == 1%R then +oo else if r == 0%:R then 1 else (`1-(r^-1))^-1%:E
  end.

Local Notation "p ^*" := (hoelder_conj p).

Lemma hoelder_conj1 : 1^* = +oo.
Proof.
by rewrite /hoelder_conj eqxx.
Qed.

Lemma hoelder_conj_gt1 (p : \bar R) : 1 <= p -> 1 <= p^*.
Proof.
move: p => [r/=||]//; case: ifPn => [_ _|r1]; first by rewrite leey.
rewrite le_eqVlt eq_sym eqe (negbTE r1)/= lte_fin => {}r1.
rewrite gt_eqF ?(lt_trans _ r1)// onemV ?gt_eqF ?(lt_trans _ r1)//.
rewrite lee_fin invf_ge1; last first.
  by rewrite divr_gt0// ?subr_gt0// (le_lt_trans _ r1).
by rewrite lter_pdivrMr// ?(le_lt_trans _ r1)// mul1r ler_subl_addr ler_addl.
Qed.

Let inve (x : \bar R) :=
  match x with
  | +oo%E => 0
  | -oo%E => 0
  | r%:E => r^-1%:E
  end.

Local Notation "x ^-1" := (inve x) : ereal_scope.

Lemma hoelder_conjP (p : \bar R) : p^-1 + p^*^-1 = 1.
Proof.
move: p => [r| |]/=; [|by rewrite add0e invr1..].
case: ifPn => [/eqP -> /=|r1]; first by rewrite adde0 invr1.
case: ifPn => [/eqP -> /=|r0]; first by rewrite invr0 invr1 add0e.
rewrite onemV//= invrK -EFinD -{1}(mul1r (r^-1)%R) -mulrDl.
by rewrite addrCA subrr addr0 divff.
Qed.

End hoelder_conjugate.