diff --git a/theories/ehoelder.v b/theories/ehoelder.v
new file mode 100644
index 000000000..8f738ea17
--- /dev/null
+++ b/theories/ehoelder.v
@@ -0,0 +1,251 @@
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
+From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
+From mathcomp Require Import cardinality fsbigop signed reals ereal.
+From mathcomp Require Import topology normedtype sequences real_interval.
+From mathcomp Require Import esum measure lebesgue_measure lebesgue_integral.
+From mathcomp Require Import numfun exp convex itv.
+
+(**md**************************************************************************)
+(* # Hoelder's Inequality                                                     *)
+(*                                                                            *)
+(* This file provides Hoelder's inequality.                                   *)
+(* ```                                                                        *)
+(*           'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1             *)
+(*                          The corresponding definition is Lnorm.            *)
+(* ```                                                                        *)
+(*                                                                            *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+Import numFieldTopology.Exports.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+Local Open Scope ereal_scope.
+
+Reserved Notation "'N[ mu ]_ p [ F ]"
+  (at level 5, F at level 36, mu at level 10,
+  format "'[' ''N[' mu ]_ p '/  ' [ F ] ']'").
+(* for use as a local notation when the measure is in context: *)
+Reserved Notation "'N_ p [ F ]"
+  (at level 5, F at level 36, format "'[' ''N_' p '/  ' [ F ] ']'").
+
+
+Section extended_essential_supremum.
+  Local Open Scope classical_set_scope.
+  Local Open Scope ring_scope.
+  Local Open Scope ereal_scope.
+  Context d {T : semiRingOfSetsType d} {R : realType}.
+  Variable mu : {measure set T -> \bar R}.
+  Implicit Types (f : T -> \bar R).
+
+  Definition ess_supe f :=
+    ereal_inf ([set r | mu ([set x | r < f x]%E) = 0]%E). (* '[r, +oo] ? *)
+
+  Definition ess_infe f := - ess_supe (\- f). 
+
+
+  Lemma ess_supe_ge0 f : 0 < mu setT -> (forall t, 0%E <= f t) ->
+    0 <= ess_supe f.
+  Proof. 
+    move=> H H0. apply: lb_ereal_inf. move => r /= /eqP H1.
+    case r eqn:H2; 
+    rewrite ?le0y // leNgt; 
+    apply/negP => r0; apply/negP : H1; 
+    rewrite -preimage_itv_o_infty gt_eqF// (_ : f @^-1` _ = setT)//= 
+    ?setIidr //=; apply/seteqP; split => // x _ /=; 
+    rewrite in_itv/= (lt_le_trans _ (H0 x)) //= leey //.  
+  Qed.
+  Lemma ess_infe_le0 f : 0 < mu setT -> (forall t, f t <= 0) -> ess_infe f <= 0.
+  Proof.
+    move => H H0. rewrite /ess_infe oppe_le0. 
+    apply : ess_supe_ge0. rewrite //=. move => t.  
+    rewrite oppe_ge0 //.
+    Qed.
+
+  Lemma ess_infe_ge0 f : 0 < mu setT -> (forall t, 0%E <= f t) ->
+    0 <= ess_infe f.
+Proof. 
+  move => H H0. 
+  rewrite /ess_infe oppe_ge0 /ess_supe. 
+  apply ereal_inf_le.
+  rewrite exists2E.
+  exists 0. split; rewrite //=.
+  have H1 : [set x | 0%R < - f x] = set0.
+  - apply eq_set => x. 
+    have H1 := H0 x.
+    rewrite -falseE oppe_gt0.
+    rewrite leNgt in H1; apply negbTE in H1.
+    rewrite H1 //=.
+  by rewrite H1.
+Qed.
+
+(*
+Lemma aku (S : set (\bar R)) : S != set0 -> 
+- ereal_sup S = ereal_sup (-%E @` S).
+Proof.
+  move => H. rewrite /ereal_sup / supremum. rewrite (negPf H).
+  have H0 := negP H.
+  case: ifPn => H1.
+  - have H2 := (image_set0_set0 (eqP H1)).
+    move : H1; by rewrite H2 (image_set0 -%E) -{1}H2.
+    Check @xgetPex (\bar R) -oo (supremums S).
+  -
+Qed.  
+*)
+
+
+
+End extended_essential_supremum.
+
+Declare Scope Lnorme_scope.
+
+(*
+Definition ifpoweR {R : realType} (x : \bar R) r := 
+  if x is x'%:E 
+  then (x' `^ r)%:E 
+  else 
+    if x is +oo then 
+      if r == 0%R then 1 else +oo
+    else 
+      if r == 0%R then 1 else 0%R.
+
+Lemma poweR_ifpoweR {R : realType} : @poweR R = ifpoweR.
+Proof.
+  by apply funext => x; case : x => [r| //= | //=].
+Qed.
+*)
+
+
+Definition lne {R : realType} (x : \bar R) :=
+  match x with
+  | x'%:E => (ln x')%:E
+  | +oo => +oo
+  | -oo => 0
+  end.
+
+Definition geo_mean {d} {T : measurableType d} {R : realType} (P : probability T R) (g : T -> \bar R) := 
+expeR (\int[P]_x (lne (g x)))%E.
+
+HB.lock Definition Lnorme {d} {T : measurableType d} {R : realType} (P : probability T R) 
+(p : \bar R) (f : T -> \bar R) :=
+  match p with
+  | p%:E => (if p == 0%R then
+              geo_mean P f
+            else
+              (\int[P]_x (`|f x| `^ p)) `^ p^-1)%E
+  | +oo%E => (if P [set: T] > 0 then ess_supe P (abse \o f) else 0)%E
+  | -oo%E => (if P [set: T] > 0 then ess_infe P (abse \o f) else 0)%E
+  end.
+Canonical locked_Lnorme := Unlockable Lnorme.unlock.
+Arguments Lnorme {d T R} P p f.
+
+Section Lnorme_properties.
+  Context d {T : measurableType d} {R : realType}.
+  Variable P : probability T R.
+  Local Open Scope ereal_scope.
+  Implicit Types (p : \bar R) (f g : T -> \bar R) (r : R).
+
+  Local Notation "'Ne_ p [ f ]" := (Lnorme P p f).
+
+  Lemma Lnorm1 f : 'Ne_1[f] = \int[P]_x `|f x|.
+  Proof. 
+    rewrite unlock oner_eq0 invr1// poweRe1//.
+    - by apply : eq_integral => t _; rewrite poweRe1.
+    - by apply : integral_ge0 => t _; rewrite  poweRe1.
+  Qed.
+  
+  Lemma Lnorme_ge0 p f : 0 <= 'Ne_p[f].
+  Proof. 
+    rewrite unlock. move : p => [r/=|/=|//].
+    - case: ifPn => // _; 
+      rewrite ?/geo_mean ?expeR_ge0 ?poweR_ge0//.
+    - case: ifPn => H //; rewrite ess_supe_ge0 //;
+      move => t; rewrite compE //=.
+    - case: ifPn => H //; rewrite ess_infe_ge0 //.
+      move => t; rewrite compE //=.
+  Qed.
+
+  Lemma eq_Lnorme p f g : f =1 g -> 'Ne_p[f] = 'Ne_p[g].
+  Proof.
+    move => H; congr Lnorme; exact /funext.
+  Qed.
+
+  Lemma measurable_poweR r :
+  measurable_fun [set: \bar R] (@poweR R ^~ r).
+  Proof.
+  move => _ /= B H.
+  rewrite setIidr; last first. 
+    apply subsetT.
+  Print poweR.
+  rewrite [X in measurable X]
+  (_ : (poweR^~ r @^-1` B) = 
+  if (r == 0%R) then (
+    if 1 \in B then [set : \bar R] else set0 ) 
+  else
+  (B `&` [set +oo]) `|` (if 0 \in B then [set -oo] else set0) `|`
+  EFin @` (
+    @powR R ^~ r @^-1` (fine @` (B `\` [set -oo; +oo]))
+          )
+  ); last first. 
+  case (r == 0%R) eqn:H0; apply/seteqP; 
+  split => [a //= H1 //= | a //= H1 //=].
+  - (*r == 0*)
+  move : H1; rewrite (eqP H0) //= => H1. 
+  -- split => //=; apply poweRe0.
+  -- destruct H1 as [H1 H2]; apply H1.
+  - (*r != 0*)
+  -- (*B <= B*)
+     move : H1; rewrite /poweR H0 => H1.
+     case a as [s| | ].
+  --- (*a = s %:E*) 
+      right. 
+      exists s; last first => //=. 
+      exists (s%:E `^ r); last first =>  //=.
+      split => //=. rewrite not_orE //=.
+  --- (*a = +oo*)
+      repeat left; split => //=; rewrite not_orE //=.
+  --- (*a = -oo*)
+      left. right. case : ifPn => //=. move => H2.
+      rewrite notin_setE in H2. contradiction.
+  -- (*B <= A*)
+  --- case H1.
+  ---- case.
+  ----- move => H2. destruct H2 as [H2 H3]. 
+       by move : H2; rewrite H3 //= H0.
+  ----- case : ifPn => //=. move => H2 H3.
+       rewrite H3 //= H0. by rewrite in_setE in H2.
+  ---- move => H2. destruct H2 as [b [c [H2 H3]] H4].
+       rewrite not_orE in H3. destruct H3 as [H3 H6].
+       case c as [s | | ]. 
+  ----- move : H5 H2 => //= => H5. 
+        by rewrite H5 -H4 poweR_EFin.
+  ----- contradiction.
+  ----- contradiction.
+  
+       
+
+    
+  Qed.
+
+
+
+  Lemma Lnorme_eq0_eq0 r f : 
+  (0 < r)%R -> 
+  measurable_fun setT f ->
+  'Ne_r%:E[f] = 0 -> 
+  ae_eq P [set: T] (fun t => (`|f t| `^ r)) (cst 0).
+  Proof.
+    move => H H0. rewrite unlock (gt_eqF H) => /poweR_eq0_eq0 H1.
+    apply/ae_eq_integral_abs => //=.
+      Search (poweR).
+      apply: (@measurableT_comp _ _ _ _ _ _ (@poweR R ^~ r)) => //=.
+
+
+
+End Lnorme_properties.
\ No newline at end of file
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 346c0cb48..340a34966 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -48,458 +48,459 @@ HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType}
   end.
 Canonical locked_Lnorm := Unlockable Lnorm.unlock.
 Arguments Lnorm {d T R} mu p f.
+    
 
 Section Lnorm_properties.
-Context d {T : measurableType d} {R : realType}.
-Variable mu : {measure set T -> \bar R}.
-Local Open Scope ereal_scope.
-Implicit Types (p : \bar R) (f g : T -> R) (r : R).
-
-Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
-
-Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E.
-Proof.
-rewrite unlock oner_eq0 invr1// poweRe1//.
-  by apply: eq_integral => t _; rewrite powRr1.
-by apply: integral_ge0 => t _; rewrite powRr1.
-Qed.
-
-Lemma Lnorm_ge0 p f : 0 <= 'N_p[f].
-Proof.
-rewrite unlock; move: p => [r/=|/=|//].
-  by case: ifPn => // r0; exact: poweR_ge0.
-by case: ifPn => // /ess_sup_ge0; apply => t/=.
-Qed.
-
-Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g].
-Proof. by move=> fg; congr Lnorm; exact/funext. Qed.
-
-Lemma Lnorm_eq0_eq0 r f : (0 < r)%R -> measurable_fun setT f ->
-  'N_r%:E[f] = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ r)%:E) (cst 0).
-Proof.
-move=> r0 mf; rewrite unlock (gt_eqF r0) => /poweR_eq0_eq0 fp.
-apply/ae_eq_integral_abs => //=.
-  apply: measurableT_comp => //.
-  apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //.
-  exact: measurableT_comp.
-under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//.
-by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0.
-Qed.
-
-Lemma powR_Lnorm f r : r != 0%R ->
-  'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E.
-Proof.
-move=> r0; rewrite unlock (negbTE r0) -poweRrM mulVf// poweRe1//.
-by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0.
-Qed.
-
-End Lnorm_properties.
-
-#[global]
-Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core.
-
-Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
-
-Section lnorm.
-(* l-norm is just L-norm applied to counting *)
-Context d {T : measurableType d} {R : realType}.
-Local Open Scope ereal_scope.
-Local Notation "'N_ p [ f ]" := (Lnorm [the measure _ _ of counting] p f).
-
-Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R ->
-  'N_p%:E [f] = (\sum_(k <oo) (`| f k | `^ p)%:E) `^ p^-1.
-Proof.
-move=> p0; rewrite unlock gt_eqF// ge0_integral_count// => k.
-by rewrite lee_fin powR_ge0.
-Qed.
-
-End lnorm.
-
-Section hoelder.
-Context d {T : measurableType d} {R : realType}.
-Variable mu : {measure set T -> \bar R}.
-Local Open Scope ereal_scope.
-Implicit Types (p q : R) (f g : T -> R).
-
-Let measurableT_comp_powR f p :
-  measurable_fun [set: T] f -> measurable_fun setT (fun x => f x `^ p)%R.
-Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.
-
-Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
-
-Let integrable_powR f p : (0 < p)%R ->
-    measurable_fun [set: T] f -> 'N_p%:E[f] != +oo ->
-  mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E).
-Proof.
-move=> p0 mf foo; apply/integrableP; split.
-  apply: measurableT_comp => //; apply: measurableT_comp_powR.
-  exact: measurableT_comp.
-rewrite ltey; apply: contra foo.
-move=> /eqP/(@eqy_poweR _ _ p^-1); rewrite invr_gt0 => /(_ p0) <-.
-rewrite unlock (gt_eqF p0); apply/eqP; congr (_ `^ _).
-by apply/eq_integral => t _; rewrite [RHS]gee0_abs// lee_fin powR_ge0.
-Qed.
-
-Let hoelder0 f g p q : measurable_fun setT f -> measurable_fun setT g ->
-    (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
-  'N_p%:E[f] = 0 -> 'N_1[(f \* g)%R]  <= 'N_p%:E[f] * 'N_q%:E[g].
-Proof.
-move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//.
-rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0.
-- by do 2 apply: measurableT_comp => //; exact: measurable_funM.
-- apply: filterS (Lnorm_eq0_eq0 p0 mf f0) => x /(_ I)[] /powR_eq0_eq0 + _.
-  by rewrite normrM => ->; rewrite mul0r.
-Qed.
-
-Let normalized p f x := `|f x| / fine 'N_p%:E[f].
-
-Let normalized_ge0 p f x : (0 <= normalized p f x)%R.
-Proof. by rewrite /normalized divr_ge0// fine_ge0// Lnorm_ge0. Qed.
-
-Let measurable_normalized p f : measurable_fun [set: T] f ->
-  measurable_fun [set: T] (normalized p f).
-Proof. by move=> mf; apply: measurable_funM => //; exact: measurableT_comp. Qed.
-
-Let integral_normalized f p : (0 < p)%R -> 0 < 'N_p%:E[f] ->
-    mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E) ->
-  \int[mu]_x (normalized p f x `^ p)%:E = 1.
-Proof.
-move=> p0 fpos ifp.
-transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p%:E[f] `^ p))%:E).
-  apply: eq_integral => t _.
-  rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0.
-  rewrite -[in LHS]powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0.
-  by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0.
-have fp0 : 0 < \int[mu]_x (`|f x| `^ p)%:E.
-  rewrite unlock (gt_eqF p0) in fpos.
-  apply: gt0_poweR fpos; rewrite ?invr_gt0//.
-  by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0.
-rewrite unlock (gt_eqF p0) -poweRrM mulVf ?(gt_eqF p0)// (poweRe1 (ltW fp0))//.
-under eq_integral do rewrite EFinM muleC.
-have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo.
-  move/integrableP: ifp => -[_].
-  by under eq_integral do rewrite gee0_abs// ?lee_fin ?powR_ge0//.
-rewrite integralZl//; apply/eqP; rewrite eqe_pdivrMl ?mule1.
-- by rewrite fineK// gt0_fin_numE.
-- by rewrite gt_eqF// fine_gt0// foo andbT.
-Qed.
-
-Lemma hoelder f g p q : measurable_fun setT f -> measurable_fun setT g ->
-    (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
- 'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g].
-Proof.
-move=> mf mg p0 q0 pq.
-have [f0|f0] := eqVneq 'N_p%:E[f] 0%E; first exact: hoelder0.
-have [g0|g0] := eqVneq 'N_q%:E[g] 0%E.
-  rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC.
-  by under eq_Lnorm do rewrite /= mulrC.
-have {f0}fpos : 0 < 'N_p%:E[f] by rewrite lt0e f0 Lnorm_ge0.
-have {g0}gpos : 0 < 'N_q%:E[g] by rewrite lt0e g0 Lnorm_ge0.
-have [foo|foo] := eqVneq 'N_p%:E[f] +oo%E; first by rewrite foo gt0_mulye ?leey.
-have [goo|goo] := eqVneq 'N_q%:E[g] +oo%E; first by rewrite goo gt0_muley ?leey.
-pose F := normalized p f; pose G := normalized q g.
-rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first.
-  rewrite !Lnorm1; under [in RHS]eq_integral.
-    move=> x _; rewrite /F /G /normalized/=.
-    rewrite ger0_norm; last by rewrite mulr_ge0 ?divr_ge0 ?fine_ge0 ?Lnorm_ge0.
-    by rewrite mulrACA -normrM EFinM; over.
-  rewrite ge0_integralZr//; last 2 first.
-    - by do 2 apply: measurableT_comp => //; exact: measurable_funM.
-    - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0.
-  rewrite -!muleA [X in _ * X](_ : _ = 1) ?mule1// EFinM muleACA.
-  rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e; last first.
+  Context d {T : measurableType d} {R : realType}.
+  Variable mu : {measure set T -> \bar R}.
+  Local Open Scope ereal_scope.
+  Implicit Types (p : \bar R) (f g : T -> R) (r : R).
+
+  Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
+
+  Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E.
+  Proof.
+  rewrite unlock oner_eq0 invr1// poweRe1//.
+    by apply: eq_integral => t _; rewrite powRr1.
+  by apply: integral_ge0 => t _; rewrite powRr1.
+  Qed.
+
+  Lemma Lnorm_ge0 p f : 0 <= 'N_p[f].
+  Proof.
+  rewrite unlock; move: p => [r/=|/=|//].
+    by case: ifPn => // r0; exact: poweR_ge0.
+  by case: ifPn => // /ess_sup_ge0; apply => t/=.
+  Qed.
+
+  Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g].
+  Proof. by move=> fg; congr Lnorm; exact/funext. Qed.
+
+  Lemma Lnorm_eq0_eq0 r f : (0 < r)%R -> measurable_fun setT f ->
+    'N_r%:E[f] = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ r)%:E) (cst 0).
+  Proof.
+  move=> r0 mf; rewrite unlock (gt_eqF r0) => /poweR_eq0_eq0 fp.
+  apply/ae_eq_integral_abs => //=.
+    apply: measurableT_comp => //.
+    apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //.
+    exact: measurableT_comp.
+  under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//.
+  by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0.
+  Qed.
+
+  Lemma powR_Lnorm f r : r != 0%R ->
+    'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E.
+  Proof.
+  move=> r0; rewrite unlock (negbTE r0) -poweRrM mulVf// poweRe1//.
+  by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0.
+  Qed.
+
+  End Lnorm_properties.
+
+  #[global]
+  Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core.
+
+  Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
+
+  Section lnorm.
+  (* l-norm is just L-norm applied to counting *)
+  Context d {T : measurableType d} {R : realType}.
+  Local Open Scope ereal_scope.
+  Local Notation "'N_ p [ f ]" := (Lnorm [the measure _ _ of counting] p f).
+
+  Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R ->
+    'N_p%:E [f] = (\sum_(k <oo) (`| f k | `^ p)%:E) `^ p^-1.
+  Proof.
+  move=> p0; rewrite unlock gt_eqF// ge0_integral_count// => k.
+  by rewrite lee_fin powR_ge0.
+  Qed.
+
+  End lnorm.
+
+  Section hoelder.
+  Context d {T : measurableType d} {R : realType}.
+  Variable mu : {measure set T -> \bar R}.
+  Local Open Scope ereal_scope.
+  Implicit Types (p q : R) (f g : T -> R).
+
+  Let measurableT_comp_powR f p :
+    measurable_fun [set: T] f -> measurable_fun setT (fun x => f x `^ p)%R.
+  Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.
+
+  Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
+
+  Let integrable_powR f p : (0 < p)%R ->
+      measurable_fun [set: T] f -> 'N_p%:E[f] != +oo ->
+    mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E).
+  Proof.
+  move=> p0 mf foo; apply/integrableP; split.
+    apply: measurableT_comp => //; apply: measurableT_comp_powR.
+    exact: measurableT_comp.
+  rewrite ltey; apply: contra foo.
+  move=> /eqP/(@eqy_poweR _ _ p^-1); rewrite invr_gt0 => /(_ p0) <-.
+  rewrite unlock (gt_eqF p0); apply/eqP; congr (_ `^ _).
+  by apply/eq_integral => t _; rewrite [RHS]gee0_abs// lee_fin powR_ge0.
+  Qed.
+
+  Let hoelder0 f g p q : measurable_fun setT f -> measurable_fun setT g ->
+      (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
+    'N_p%:E[f] = 0 -> 'N_1[(f \* g)%R]  <= 'N_p%:E[f] * 'N_q%:E[g].
+  Proof.
+  move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//.
+  rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0.
+  - by do 2 apply: measurableT_comp => //; exact: measurable_funM.
+  - apply: filterS (Lnorm_eq0_eq0 p0 mf f0) => x /(_ I)[] /powR_eq0_eq0 + _.
+    by rewrite normrM => ->; rewrite mul0r.
+  Qed.
+
+  Let normalized p f x := `|f x| / fine 'N_p%:E[f].
+
+  Let normalized_ge0 p f x : (0 <= normalized p f x)%R.
+  Proof. by rewrite /normalized divr_ge0// fine_ge0// Lnorm_ge0. Qed.
+
+  Let measurable_normalized p f : measurable_fun [set: T] f ->
+    measurable_fun [set: T] (normalized p f).
+  Proof. by move=> mf; apply: measurable_funM => //; exact: measurableT_comp. Qed.
+
+  Let integral_normalized f p : (0 < p)%R -> 0 < 'N_p%:E[f] ->
+      mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E) ->
+    \int[mu]_x (normalized p f x `^ p)%:E = 1.
+  Proof.
+  move=> p0 fpos ifp.
+  transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p%:E[f] `^ p))%:E).
+    apply: eq_integral => t _.
+    rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0.
+    rewrite -[in LHS]powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0.
+    by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0.
+  have fp0 : 0 < \int[mu]_x (`|f x| `^ p)%:E.
+    rewrite unlock (gt_eqF p0) in fpos.
+    apply: gt0_poweR fpos; rewrite ?invr_gt0//.
+    by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0.
+  rewrite unlock (gt_eqF p0) -poweRrM mulVf ?(gt_eqF p0)// (poweRe1 (ltW fp0))//.
+  under eq_integral do rewrite EFinM muleC.
+  have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo.
+    move/integrableP: ifp => -[_].
+    by under eq_integral do rewrite gee0_abs// ?lee_fin ?powR_ge0//.
+  rewrite integralZl//; apply/eqP; rewrite eqe_pdivrMl ?mule1.
+  - by rewrite fineK// gt0_fin_numE.
+  - by rewrite gt_eqF// fine_gt0// foo andbT.
+  Qed.
+
+  Lemma hoelder f g p q : measurable_fun setT f -> measurable_fun setT g ->
+      (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
+  'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g].
+  Proof.
+  move=> mf mg p0 q0 pq.
+  have [f0|f0] := eqVneq 'N_p%:E[f] 0%E; first exact: hoelder0.
+  have [g0|g0] := eqVneq 'N_q%:E[g] 0%E.
+    rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC.
+    by under eq_Lnorm do rewrite /= mulrC.
+  have {f0}fpos : 0 < 'N_p%:E[f] by rewrite lt0e f0 Lnorm_ge0.
+  have {g0}gpos : 0 < 'N_q%:E[g] by rewrite lt0e g0 Lnorm_ge0.
+  have [foo|foo] := eqVneq 'N_p%:E[f] +oo%E; first by rewrite foo gt0_mulye ?leey.
+  have [goo|goo] := eqVneq 'N_q%:E[g] +oo%E; first by rewrite goo gt0_muley ?leey.
+  pose F := normalized p f; pose G := normalized q g.
+  rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first.
+    rewrite !Lnorm1; under [in RHS]eq_integral.
+      move=> x _; rewrite /F /G /normalized/=.
+      rewrite ger0_norm; last by rewrite mulr_ge0 ?divr_ge0 ?fine_ge0 ?Lnorm_ge0.
+      by rewrite mulrACA -normrM EFinM; over.
+    rewrite ge0_integralZr//; last 2 first.
+      - by do 2 apply: measurableT_comp => //; exact: measurable_funM.
+      - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0.
+    rewrite -!muleA [X in _ * X](_ : _ = 1) ?mule1// EFinM muleACA.
+    rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e; last first.
+      rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
+      by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// fpos/= ltey.
     rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
-    by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// fpos/= ltey.
-  rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
-  by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// gpos/= ltey.
-rewrite -(mul1e ('N_p%:E[f] * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//.
-rewrite [leRHS](_ : _ = \int[mu]_x (F x `^ p / p + G x `^ q / q)%:E).
-  rewrite Lnorm1 ae_ge0_le_integral //.
-  - do 2 apply: measurableT_comp => //.
-    by apply: measurable_funM => //; exact: measurable_normalized.
-  - by move=> x _; rewrite lee_fin addr_ge0// divr_ge0// ?powR_ge0// ltW.
-  - by apply: measurableT_comp => //; apply: measurable_funD => //;
-       apply: measurable_funM => //; apply: measurableT_comp_powR => //;
-       exact: measurable_normalized.
-  apply/aeW => x _; rewrite lee_fin ger0_norm ?conjugate_powR ?normalized_ge0//.
-  by rewrite mulr_ge0// normalized_ge0.
-under eq_integral do rewrite EFinD.
-rewrite ge0_integralD//; last 4 first.
-- by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW.
-- apply: measurableT_comp => //; apply: measurable_funM => //.
-  by apply: measurableT_comp_powR => //; exact: measurable_normalized.
-- by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW.
-- apply: measurableT_comp => //; apply: measurable_funM => //.
-  by apply: measurableT_comp_powR => //; exact: measurable_normalized.
-under eq_integral do rewrite EFinM.
-rewrite [X in X + _]ge0_integralZr//; last 3 first.
-- apply: measurableT_comp => //.
-  by apply: measurableT_comp_powR => //; exact: measurable_normalized.
-- by move=> x _; rewrite lee_fin powR_ge0.
-- by rewrite lee_fin invr_ge0 ltW.
-under [X in _ + X]eq_integral => x _ do rewrite EFinM.
-rewrite ge0_integralZr//; last 3 first.
-- apply: measurableT_comp => //.
-  by apply: measurableT_comp_powR => //; exact: measurable_normalized.
-- by move=> x _; rewrite lee_fin powR_ge0.
-- by rewrite lee_fin invr_ge0 ltW.
-rewrite integral_normalized//; last exact: integrable_powR.
-rewrite integral_normalized//; last exact: integrable_powR.
-by rewrite 2!mul1e -EFinD pq.
-Qed.
-
-End hoelder.
-
-Section hoelder2.
-Context {R : realType}.
-Local Open Scope ring_scope.
-
-Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) :
-  0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 ->
-  0 < p -> 0 < q -> p^-1 + q^-1 = 1 ->
-  a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p) `^ p^-1 *
-                       (b1 `^ q + b2 `^ q) `^ q^-1.
-Proof.
-move=> a10 a20 b10 b20 p0 q0 pq.
-pose f a b n : R := match n with 0%nat => a | 1%nat => b | _ => 0 end.
-have mf a b : measurable_fun setT (f a b) by [].
-have := hoelder [the measure _ _ of counting] (mf a1 a2) (mf b1 b2) p0 q0 pq.
-rewrite !Lnorm_counting//.
-rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0.
-rewrite add0n ereal_series_cond eseries0 ?adde0; last first.
-  by move=> [//|] [//|n _]; rewrite /f /= mulr0 normr0 powR0.
-rewrite big_mkord 2!big_ord_recr/= big_ord0 add0e.
-rewrite powRr1 ?normr_ge0 ?powRr1 ?normr_ge0//.
-rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0.
-rewrite ereal_series_cond eseries0 ?adde0; last first.
-  by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF.
-rewrite big_mkord 2!big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin.
-rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0.
-rewrite ereal_series_cond eseries0 ?adde0; last first.
-  by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF.
-rewrite big_mkord 2!big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin.
-rewrite -EFinM invr1 powRr1; last by rewrite addr_ge0.
-do 2 (rewrite ger0_norm; last by rewrite mulr_ge0).
-by do 4 (rewrite ger0_norm; last by []).
-Qed.
-
-End hoelder2.
-
-Section convex_powR.
-Context {R : realType}.
-Local Open Scope ring_scope.
-
-Lemma convex_powR p : 1 <= p ->
-  convex_function `[0, +oo[%classic (@powR R ^~ p).
-Proof.
-move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0.
-have p0 : 0 < p by rewrite (lt_le_trans _ p1).
-rewrite !convRE; set w1 := `1-(t%:inum); set w2 := t%:inum.
-have [->|w10] := eqVneq w1 0.
-  rewrite !mul0r !add0r; have [->|w20] := eqVneq w2 0.
-    by rewrite !mul0r powR0// gt_eqF.
-  by rewrite ge1r_powRZ// /w2 lt_neqAle eq_sym w20/=; apply/andP.
-have [->|w20] := eqVneq w2 0.
-  by rewrite !mul0r !addr0 ge1r_powRZ// onem_le1// andbT lt0r w10 onem_ge0.
-have [->|p_neq1] := eqVneq p 1.
-  by rewrite !powRr1// addr_ge0// mulr_ge0// /w2 ?onem_ge0.
-have {p_neq1} {}p1 : 1 < p by rewrite lt_neqAle eq_sym p_neq1.
-pose q := p / (p - 1).
-have q1 : 1 <= q by rewrite /q ler_pdivlMr// ?mul1r ?gerBl// subr_gt0.
-have q0 : 0 < q by rewrite (lt_le_trans _ q1).
-have pq1 : p^-1 + q^-1 = 1.
-  rewrite /q invf_div -{1}(div1r p) -mulrDl addrCA subrr addr0.
-  by rewrite mulfV// gt_eqF.
-rewrite -(@powRr1 _ (w1 * x `^ p + w2 * y `^ p)); last first.
-  by rewrite addr_ge0// mulr_ge0// ?powR_ge0// /w2 ?onem_ge0// itv_ge0.
-have -> : 1 = p^-1 * p by rewrite mulVf ?gt_eqF.
-rewrite powRrM (ge0_ler_powR (le_trans _ (ltW p1)))//.
-- by rewrite nnegrE addr_ge0// mulr_ge0 /w2 ?onem_ge0.
-- by rewrite nnegrE powR_ge0.
-have -> : w1 * x + w2 * y = w1 `^ (p^-1) * w1 `^ (q^-1) * x +
-                            w2 `^ (p^-1) * w2 `^ (q^-1) * y.
-  rewrite -!powRD pq1; [|exact/implyP..].
-  by rewrite !powRr1// /w2 ?onem_ge0.
-apply: (@le_trans _ _ ((w1 * x `^ p + w2 * y `^ p) `^ (p^-1) *
-                       (w1 + w2) `^ q^-1)).
-  pose a1 := w1 `^ p^-1 * x. pose a2 := w2 `^ p^-1 * y.
-  pose b1 := w1 `^ q^-1. pose b2 := w2 `^ q^-1.
-  have : a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p) `^ p^-1 *
-                              (b1 `^ q + b2 `^ q) `^ q^-1.
-    by apply: hoelder2 => //; rewrite ?mulr_ge0 ?powR_ge0.
-  rewrite ?powRM ?powR_ge0 -?powRrM ?mulVf ?powRr1 ?gt_eqF ?onem_ge0/w2//.
-  by rewrite mulrAC (mulrAC _ y) => /le_trans; exact.
-by rewrite {2}/w1 {2}/w2 subrK powR1 mulr1.
-Qed.
-
-End convex_powR.
-
-Section minkowski.
-Context d (T : measurableType d) (R : realType).
-Variable mu : {measure set T -> \bar R}.
-Implicit Types (f g : T -> R) (p : R).
-
-Let convex_powR_abs_half f g p x : 1 <= p ->
-  `| 2^-1 * f x + 2^-1 * g x | `^ p <=
-   2^-1 * `| f x | `^ p + 2^-1 * `| g x | `^ p.
-Proof.
-move=> p1; rewrite (@le_trans _ _ ((2^-1 * `| f x | + 2^-1 * `| g x |) `^ p))//.
-  rewrite ge0_ler_powR ?nnegrE ?(le_trans _ p1)//.
-  by rewrite (le_trans (ler_normD _ _))// 2!normrM ger0_norm.
-rewrite {1 3}(_ : 2^-1 = 1 - 2^-1); last by rewrite {2}(splitr 1) div1r addrK.
-rewrite (@convex_powR _ _ p1 (@Itv.mk _ _ _ _)) ?inE/= ?in_itv/= ?normr_ge0//.
-by rewrite /Itv.itv_cond/= in_itv/= invr_ge0 ler0n invf_le1 ?ler1n.
-Qed.
-
-Let measurableT_comp_powR f p :
-  measurable_fun setT f -> measurable_fun setT (fun x => f x `^ p)%R.
-Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.
-
-Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
-Local Open Scope ereal_scope.
-
-Let minkowski1 f g p : measurable_fun setT f -> measurable_fun setT g ->
-  'N_1[(f \+ g)%R] <= 'N_1[f] + 'N_1[g].
-Proof.
-move=> mf mg.
-rewrite !Lnorm1 -ge0_integralD//; [|by do 2 apply: measurableT_comp..].
-rewrite ge0_le_integral//.
-- by do 2 apply: measurableT_comp => //; exact: measurable_funD.
-- by move=> x _; rewrite lee_fin.
-- by apply/measurableT_comp/measurable_funD; exact/measurableT_comp.
-- by move=> x _; rewrite lee_fin ler_normD.
-Qed.
-
-Let minkowski_lty f g p :
-  measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R ->
-  'N_p%:E[f] < +oo -> 'N_p%:E[g] < +oo -> 'N_p%:E[(f \+ g)%R] < +oo.
-Proof.
-move=> mf mg p1 Nfoo Ngoo.
-have p0 : p != 0%R by rewrite gt_eqF// (lt_le_trans _ p1).
-have h x : (`| f x + g x | `^ p <=
-            2 `^ (p - 1) * (`| f x | `^ p + `| g x | `^ p))%R.
-  have := convex_powR_abs_half (fun x => 2 * f x)%R (fun x => 2 * g x)%R x p1.
-  rewrite !normrM (@ger0_norm _ 2)// !mulrA mulVf// !mul1r => /le_trans; apply.
-  rewrite !powRM// !mulrA -powR_inv1// -powRD ?pnatr_eq0 ?implybT//.
-  by rewrite (addrC _ p) -mulrDr.
-rewrite unlock (gt_eqF (lt_le_trans _ p1))// poweR_lty//.
-pose x := \int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p))%:E.
-apply: (@le_lt_trans _ _ x).
-  rewrite ge0_le_integral//=.
-  - by move=> t _; rewrite lee_fin// powR_ge0.
-  - apply/measurable_EFinP/measurableT_comp_powR/measurableT_comp => //.
-    exact: measurable_funD.
-  - by move=> t _; rewrite lee_fin mulr_ge0 ?addr_ge0 ?powR_ge0.
-  - by apply/measurable_EFinP/measurable_funM/measurable_funD => //;
-      exact/measurableT_comp_powR/measurableT_comp.
-  - by move=> ? _; rewrite lee_fin.
-rewrite {}/x; under eq_integral do rewrite EFinM.
-rewrite ge0_integralZl_EFin ?powR_ge0//; last 2 first.
-  - by move=> x _; rewrite lee_fin addr_ge0// powR_ge0.
-  - by apply/measurable_EFinP/measurable_funD => //;
-      exact/measurableT_comp_powR/measurableT_comp.
-rewrite lte_mul_pinfty ?lee_fin ?powR_ge0//.
-under eq_integral do rewrite EFinD.
-rewrite ge0_integralD//; last 4 first.
+    by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// gpos/= ltey.
+  rewrite -(mul1e ('N_p%:E[f] * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//.
+  rewrite [leRHS](_ : _ = \int[mu]_x (F x `^ p / p + G x `^ q / q)%:E).
+    rewrite Lnorm1 ae_ge0_le_integral //.
+    - do 2 apply: measurableT_comp => //.
+      by apply: measurable_funM => //; exact: measurable_normalized.
+    - by move=> x _; rewrite lee_fin addr_ge0// divr_ge0// ?powR_ge0// ltW.
+    - by apply: measurableT_comp => //; apply: measurable_funD => //;
+        apply: measurable_funM => //; apply: measurableT_comp_powR => //;
+        exact: measurable_normalized.
+    apply/aeW => x _; rewrite lee_fin ger0_norm ?conjugate_powR ?normalized_ge0//.
+    by rewrite mulr_ge0// normalized_ge0.
+  under eq_integral do rewrite EFinD.
+  rewrite ge0_integralD//; last 4 first.
+  - by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW.
+  - apply: measurableT_comp => //; apply: measurable_funM => //.
+    by apply: measurableT_comp_powR => //; exact: measurable_normalized.
+  - by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW.
+  - apply: measurableT_comp => //; apply: measurable_funM => //.
+    by apply: measurableT_comp_powR => //; exact: measurable_normalized.
+  under eq_integral do rewrite EFinM.
+  rewrite [X in X + _]ge0_integralZr//; last 3 first.
+  - apply: measurableT_comp => //.
+    by apply: measurableT_comp_powR => //; exact: measurable_normalized.
   - by move=> x _; rewrite lee_fin powR_ge0.
-  - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp.
+  - by rewrite lee_fin invr_ge0 ltW.
+  under [X in _ + X]eq_integral => x _ do rewrite EFinM.
+  rewrite ge0_integralZr//; last 3 first.
+  - apply: measurableT_comp => //.
+    by apply: measurableT_comp_powR => //; exact: measurable_normalized.
   - by move=> x _; rewrite lee_fin powR_ge0.
-  - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp.
-by rewrite lte_add_pinfty// -powR_Lnorm ?(gt_eqF (lt_trans _ p1))// poweR_lty.
-Qed.
-
-Lemma minkowski f g p :
-  measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R ->
-  'N_p%:E[(f \+ g)%R] <= 'N_p%:E[f] + 'N_p%:E[g].
-Proof.
-move=> mf mg; rewrite le_eqVlt => /predU1P[<-|p1]; first exact: minkowski1.
-have [->|Nfoo] := eqVneq 'N_p%:E[f] +oo.
-  by rewrite addye ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)).
-have [->|Ngoo] := eqVneq 'N_p%:E[g] +oo.
-  by rewrite addey ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)).
-have Nfgoo : 'N_p%:E[(f \+ g)%R] < +oo.
-  by rewrite minkowski_lty// ?ltW// ltey; [exact: Nfoo|exact: Ngoo].
-suff : 'N_p%:E[(f \+ g)%R] `^ p <= ('N_p%:E[f] + 'N_p%:E[g]) *
-    'N_p%:E[(f \+ g)%R] `^ p * (fine 'N_p%:E[(f \+ g)%R])^-1%:E.
-  have [-> _|Nfg0] := eqVneq 'N_p%:E[(f \+ g)%R] 0.
-    by rewrite adde_ge0 ?Lnorm_ge0.
-  rewrite lee_pdivlMr ?fine_gt0// ?lt0e ?Nfg0 ?Lnorm_ge0//.
-  rewrite -{1}(@fineK _ ('N_p%:E[(f \+ g)%R] `^ p)); last first.
-    by rewrite fin_num_poweR// ge0_fin_numE// Lnorm_ge0.
-  rewrite -(invrK (fine _)) lee_pdivrMl; last first.
-    rewrite invr_gt0 fine_gt0// (poweR_lty _ Nfgoo) andbT poweR_gt0//.
-    by rewrite lt0e Nfg0 Lnorm_ge0.
-  rewrite fineK ?ge0_fin_numE ?Lnorm_ge0// => /le_trans; apply.
-  rewrite lee_pdivrMl; last first.
-    by rewrite fine_gt0// poweR_lty// andbT poweR_gt0// lt0e Nfg0 Lnorm_ge0.
-  by rewrite fineK// 1?muleC// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0.
-have p0 : (0 < p)%R by exact: (lt_trans _ p1).
-rewrite powR_Lnorm ?gt_eqF//.
-under eq_integral => x _ do rewrite -mulr_powRB1//.
-apply: (@le_trans _ _
-    (\int[mu]_x ((`|f x| + `|g x|) * `|f x + g x| `^ (p - 1))%:E)).
+  - by rewrite lee_fin invr_ge0 ltW.
+  rewrite integral_normalized//; last exact: integrable_powR.
+  rewrite integral_normalized//; last exact: integrable_powR.
+  by rewrite 2!mul1e -EFinD pq.
+  Qed.
+
+  End hoelder.
+
+  Section hoelder2.
+  Context {R : realType}.
+  Local Open Scope ring_scope.
+
+  Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) :
+    0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 ->
+    0 < p -> 0 < q -> p^-1 + q^-1 = 1 ->
+    a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p) `^ p^-1 *
+                        (b1 `^ q + b2 `^ q) `^ q^-1.
+  Proof.
+  move=> a10 a20 b10 b20 p0 q0 pq.
+  pose f a b n : R := match n with 0%nat => a | 1%nat => b | _ => 0 end.
+  have mf a b : measurable_fun setT (f a b) by [].
+  have := hoelder [the measure _ _ of counting] (mf a1 a2) (mf b1 b2) p0 q0 pq.
+  rewrite !Lnorm_counting//.
+  rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0.
+  rewrite add0n ereal_series_cond eseries0 ?adde0; last first.
+    by move=> [//|] [//|n _]; rewrite /f /= mulr0 normr0 powR0.
+  rewrite big_mkord 2!big_ord_recr/= big_ord0 add0e.
+  rewrite powRr1 ?normr_ge0 ?powRr1 ?normr_ge0//.
+  rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0.
+  rewrite ereal_series_cond eseries0 ?adde0; last first.
+    by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF.
+  rewrite big_mkord 2!big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin.
+  rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0.
+  rewrite ereal_series_cond eseries0 ?adde0; last first.
+    by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF.
+  rewrite big_mkord 2!big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin.
+  rewrite -EFinM invr1 powRr1; last by rewrite addr_ge0.
+  do 2 (rewrite ger0_norm; last by rewrite mulr_ge0).
+  by do 4 (rewrite ger0_norm; last by []).
+  Qed.
+
+  End hoelder2.
+
+  Section convex_powR.
+  Context {R : realType}.
+  Local Open Scope ring_scope.
+
+  Lemma convex_powR p : 1 <= p ->
+    convex_function `[0, +oo[%classic (@powR R ^~ p).
+  Proof.
+  move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0.
+  have p0 : 0 < p by rewrite (lt_le_trans _ p1).
+  rewrite !convRE; set w1 := `1-(t%:inum); set w2 := t%:inum.
+  have [->|w10] := eqVneq w1 0.
+    rewrite !mul0r !add0r; have [->|w20] := eqVneq w2 0.
+      by rewrite !mul0r powR0// gt_eqF.
+    by rewrite ge1r_powRZ// /w2 lt_neqAle eq_sym w20/=; apply/andP.
+  have [->|w20] := eqVneq w2 0.
+    by rewrite !mul0r !addr0 ge1r_powRZ// onem_le1// andbT lt0r w10 onem_ge0.
+  have [->|p_neq1] := eqVneq p 1.
+    by rewrite !powRr1// addr_ge0// mulr_ge0// /w2 ?onem_ge0.
+  have {p_neq1} {}p1 : 1 < p by rewrite lt_neqAle eq_sym p_neq1.
+  pose q := p / (p - 1).
+  have q1 : 1 <= q by rewrite /q ler_pdivlMr// ?mul1r ?gerBl// subr_gt0.
+  have q0 : 0 < q by rewrite (lt_le_trans _ q1).
+  have pq1 : p^-1 + q^-1 = 1.
+    rewrite /q invf_div -{1}(div1r p) -mulrDl addrCA subrr addr0.
+    by rewrite mulfV// gt_eqF.
+  rewrite -(@powRr1 _ (w1 * x `^ p + w2 * y `^ p)); last first.
+    by rewrite addr_ge0// mulr_ge0// ?powR_ge0// /w2 ?onem_ge0// itv_ge0.
+  have -> : 1 = p^-1 * p by rewrite mulVf ?gt_eqF.
+  rewrite powRrM (ge0_ler_powR (le_trans _ (ltW p1)))//.
+  - by rewrite nnegrE addr_ge0// mulr_ge0 /w2 ?onem_ge0.
+  - by rewrite nnegrE powR_ge0.
+  have -> : w1 * x + w2 * y = w1 `^ (p^-1) * w1 `^ (q^-1) * x +
+                              w2 `^ (p^-1) * w2 `^ (q^-1) * y.
+    rewrite -!powRD pq1; [|exact/implyP..].
+    by rewrite !powRr1// /w2 ?onem_ge0.
+  apply: (@le_trans _ _ ((w1 * x `^ p + w2 * y `^ p) `^ (p^-1) *
+                        (w1 + w2) `^ q^-1)).
+    pose a1 := w1 `^ p^-1 * x. pose a2 := w2 `^ p^-1 * y.
+    pose b1 := w1 `^ q^-1. pose b2 := w2 `^ q^-1.
+    have : a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p) `^ p^-1 *
+                                (b1 `^ q + b2 `^ q) `^ q^-1.
+      by apply: hoelder2 => //; rewrite ?mulr_ge0 ?powR_ge0.
+    rewrite ?powRM ?powR_ge0 -?powRrM ?mulVf ?powRr1 ?gt_eqF ?onem_ge0/w2//.
+    by rewrite mulrAC (mulrAC _ y) => /le_trans; exact.
+  by rewrite {2}/w1 {2}/w2 subrK powR1 mulr1.
+  Qed.
+
+  End convex_powR.
+
+  Section minkowski.
+  Context d (T : measurableType d) (R : realType).
+  Variable mu : {measure set T -> \bar R}.
+  Implicit Types (f g : T -> R) (p : R).
+
+  Let convex_powR_abs_half f g p x : 1 <= p ->
+    `| 2^-1 * f x + 2^-1 * g x | `^ p <=
+    2^-1 * `| f x | `^ p + 2^-1 * `| g x | `^ p.
+  Proof.
+  move=> p1; rewrite (@le_trans _ _ ((2^-1 * `| f x | + 2^-1 * `| g x |) `^ p))//.
+    rewrite ge0_ler_powR ?nnegrE ?(le_trans _ p1)//.
+    by rewrite (le_trans (ler_normD _ _))// 2!normrM ger0_norm.
+  rewrite {1 3}(_ : 2^-1 = 1 - 2^-1); last by rewrite {2}(splitr 1) div1r addrK.
+  rewrite (@convex_powR _ _ p1 (@Itv.mk _ _ _ _)) ?inE/= ?in_itv/= ?normr_ge0//.
+  by rewrite /Itv.itv_cond/= in_itv/= invr_ge0 ler0n invf_le1 ?ler1n.
+  Qed.
+
+  Let measurableT_comp_powR f p :
+    measurable_fun setT f -> measurable_fun setT (fun x => f x `^ p)%R.
+  Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.
+
+  Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
+  Local Open Scope ereal_scope.
+
+  Let minkowski1 f g p : measurable_fun setT f -> measurable_fun setT g ->
+    'N_1[(f \+ g)%R] <= 'N_1[f] + 'N_1[g].
+  Proof.
+  move=> mf mg.
+  rewrite !Lnorm1 -ge0_integralD//; [|by do 2 apply: measurableT_comp..].
   rewrite ge0_le_integral//.
-  - by move=> ? _; rewrite lee_fin mulr_ge0// powR_ge0.
-  - apply: measurableT_comp => //; apply: measurable_funM.
-      exact/measurableT_comp/measurable_funD.
-    exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
-  - by move=> ? _; rewrite lee_fin mulr_ge0// powR_ge0.
-  - apply/measurableT_comp => //; apply: measurable_funM.
-      by apply/measurable_funD => //; exact: measurableT_comp.
-    exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
-  - by move=> ? _; rewrite lee_fin ler_wpM2r// ?powR_ge0// ler_normD.
-under eq_integral=> ? _ do rewrite mulrDl EFinD.
-rewrite ge0_integralD//; last 4 first.
-  - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0.
-  - apply: measurableT_comp => //; apply: measurable_funM.
-      exact: measurableT_comp.
-    exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
-  - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0.
-  - apply: measurableT_comp => //; apply: measurable_funM.
-      exact: measurableT_comp.
-    exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
-rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) *
-    (\int[mu]_x (`|f x + g x| `^ p)%:E) `^ `1-(p^-1)).
-  rewrite muleDl; last 2 first.
-    - rewrite fin_num_poweR// -powR_Lnorm ?gt_eqF// fin_num_poweR//.
-      by rewrite ge0_fin_numE ?Lnorm_ge0.
-    - by rewrite ge0_adde_def// inE Lnorm_ge0.
-  apply: leeD.
-  - pose h := (@powR R ^~ (p - 1) \o normr \o (f \+ g))%R; pose i := (f \* h)%R.
-    rewrite [leLHS](_ : _ = 'N_1[i]%R); last first.
-      rewrite Lnorm1; apply: eq_integral => x _.
-      by rewrite normrM (ger0_norm (powR_ge0 _ _)).
-    rewrite [X in _ * X](_ : _ = 'N_(p / (p - 1))%:E[h]); last first.
-      rewrite unlock mulf_eq0 gt_eqF//= invr_eq0 subr_eq0 (gt_eqF p1).
-      rewrite onemV ?gt_eqF// invf_div; apply: congr2; last by [].
-      apply: eq_integral => x _; congr EFin.
-      rewrite norm_powR// normr_id -powRrM mulrCA divff ?mulr1//.
-      by rewrite subr_eq0 gt_eqF.
-    apply: (@hoelder _ _ _ _ _ _ p (p / (p - 1))) => //.
-    + exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
-    + by rewrite divr_gt0// subr_gt0.
-    + by rewrite invf_div -onemV ?gt_eqF// addrCA subrr addr0.
-  - pose h := (fun x => `|f x + g x| `^ (p - 1))%R; pose i := (g \* h)%R.
-    rewrite [leLHS](_ : _ = 'N_1[i]); last first.
-      rewrite Lnorm1; apply: eq_integral => x _ .
-      by rewrite normrM norm_powR// normr_id.
-    rewrite [X in _ * X](_ : _ = 'N_((1 - p^-1)^-1)%:E[h])//; last first.
-      rewrite unlock invrK invr_eq0 subr_eq0 eq_sym invr_eq1 (gt_eqF p1).
-      apply: congr2; last by [].
-      apply: eq_integral => x _; congr EFin.
-      rewrite -/(onem p^-1) onemV ?gt_eqF// norm_powR// normr_id -powRrM.
-      by rewrite invf_div mulrCA divff ?subr_eq0 ?gt_eqF// ?mulr1.
-    apply: (le_trans (@hoelder _ _ _ _ _ _ p (1 - p^-1)^-1 _ _ _ _ _)) => //.
-    + exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
-    + by rewrite invr_gt0 onem_gt0// invf_lt1.
-    + by rewrite invrK addrCA subrr addr0.
-rewrite -muleA; congr (_ * _).
-under [X in X * _]eq_integral=> x _ do rewrite mulr_powRB1 ?subr_gt0//.
-rewrite poweRD; last by rewrite poweRD_defE gt_eqF ?implyFb// subr_gt0 invf_lt1.
-rewrite poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0.
-congr (_ * _); rewrite poweRN.
-- by rewrite unlock gt_eqF// fine_poweR.
-- by rewrite -powR_Lnorm ?gt_eqF// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0.
-Qed.
+  - by do 2 apply: measurableT_comp => //; exact: measurable_funD.
+  - by move=> x _; rewrite lee_fin.
+  - by apply/measurableT_comp/measurable_funD; exact/measurableT_comp.
+  - by move=> x _; rewrite lee_fin ler_normD.
+  Qed.
+
+  Let minkowski_lty f g p :
+    measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R ->
+    'N_p%:E[f] < +oo -> 'N_p%:E[g] < +oo -> 'N_p%:E[(f \+ g)%R] < +oo.
+  Proof.
+  move=> mf mg p1 Nfoo Ngoo.
+  have p0 : p != 0%R by rewrite gt_eqF// (lt_le_trans _ p1).
+  have h x : (`| f x + g x | `^ p <=
+              2 `^ (p - 1) * (`| f x | `^ p + `| g x | `^ p))%R.
+    have := convex_powR_abs_half (fun x => 2 * f x)%R (fun x => 2 * g x)%R x p1.
+    rewrite !normrM (@ger0_norm _ 2)// !mulrA mulVf// !mul1r => /le_trans; apply.
+    rewrite !powRM// !mulrA -powR_inv1// -powRD ?pnatr_eq0 ?implybT//.
+    by rewrite (addrC _ p) -mulrDr.
+  rewrite unlock (gt_eqF (lt_le_trans _ p1))// poweR_lty//.
+  pose x := \int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p))%:E.
+  apply: (@le_lt_trans _ _ x).
+    rewrite ge0_le_integral//=.
+    - by move=> t _; rewrite lee_fin// powR_ge0.
+    - apply/measurable_EFinP/measurableT_comp_powR/measurableT_comp => //.
+      exact: measurable_funD.
+    - by move=> t _; rewrite lee_fin mulr_ge0 ?addr_ge0 ?powR_ge0.
+    - by apply/measurable_EFinP/measurable_funM/measurable_funD => //;
+        exact/measurableT_comp_powR/measurableT_comp.
+    - by move=> ? _; rewrite lee_fin.
+  rewrite {}/x; under eq_integral do rewrite EFinM.
+  rewrite ge0_integralZl_EFin ?powR_ge0//; last 2 first.
+    - by move=> x _; rewrite lee_fin addr_ge0// powR_ge0.
+    - by apply/measurable_EFinP/measurable_funD => //;
+        exact/measurableT_comp_powR/measurableT_comp.
+  rewrite lte_mul_pinfty ?lee_fin ?powR_ge0//.
+  under eq_integral do rewrite EFinD.
+  rewrite ge0_integralD//; last 4 first.
+    - by move=> x _; rewrite lee_fin powR_ge0.
+    - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp.
+    - by move=> x _; rewrite lee_fin powR_ge0.
+    - exact/measurable_EFinP/measurableT_comp_powR/measurableT_comp.
+  by rewrite lte_add_pinfty// -powR_Lnorm ?(gt_eqF (lt_trans _ p1))// poweR_lty.
+  Qed.
+
+  Lemma minkowski f g p :
+    measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R ->
+    'N_p%:E[(f \+ g)%R] <= 'N_p%:E[f] + 'N_p%:E[g].
+  Proof.
+  move=> mf mg; rewrite le_eqVlt => /predU1P[<-|p1]; first exact: minkowski1.
+  have [->|Nfoo] := eqVneq 'N_p%:E[f] +oo.
+    by rewrite addye ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)).
+  have [->|Ngoo] := eqVneq 'N_p%:E[g] +oo.
+    by rewrite addey ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)).
+  have Nfgoo : 'N_p%:E[(f \+ g)%R] < +oo.
+    by rewrite minkowski_lty// ?ltW// ltey; [exact: Nfoo|exact: Ngoo].
+  suff : 'N_p%:E[(f \+ g)%R] `^ p <= ('N_p%:E[f] + 'N_p%:E[g]) *
+      'N_p%:E[(f \+ g)%R] `^ p * (fine 'N_p%:E[(f \+ g)%R])^-1%:E.
+    have [-> _|Nfg0] := eqVneq 'N_p%:E[(f \+ g)%R] 0.
+      by rewrite adde_ge0 ?Lnorm_ge0.
+    rewrite lee_pdivlMr ?fine_gt0// ?lt0e ?Nfg0 ?Lnorm_ge0//.
+    rewrite -{1}(@fineK _ ('N_p%:E[(f \+ g)%R] `^ p)); last first.
+      by rewrite fin_num_poweR// ge0_fin_numE// Lnorm_ge0.
+    rewrite -(invrK (fine _)) lee_pdivrMl; last first.
+      rewrite invr_gt0 fine_gt0// (poweR_lty _ Nfgoo) andbT poweR_gt0//.
+      by rewrite lt0e Nfg0 Lnorm_ge0.
+    rewrite fineK ?ge0_fin_numE ?Lnorm_ge0// => /le_trans; apply.
+    rewrite lee_pdivrMl; last first.
+      by rewrite fine_gt0// poweR_lty// andbT poweR_gt0// lt0e Nfg0 Lnorm_ge0.
+    by rewrite fineK// 1?muleC// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0.
+  have p0 : (0 < p)%R by exact: (lt_trans _ p1).
+  rewrite powR_Lnorm ?gt_eqF//.
+  under eq_integral => x _ do rewrite -mulr_powRB1//.
+  apply: (@le_trans _ _
+      (\int[mu]_x ((`|f x| + `|g x|) * `|f x + g x| `^ (p - 1))%:E)).
+    rewrite ge0_le_integral//.
+    - by move=> ? _; rewrite lee_fin mulr_ge0// powR_ge0.
+    - apply: measurableT_comp => //; apply: measurable_funM.
+        exact/measurableT_comp/measurable_funD.
+      exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
+    - by move=> ? _; rewrite lee_fin mulr_ge0// powR_ge0.
+    - apply/measurableT_comp => //; apply: measurable_funM.
+        by apply/measurable_funD => //; exact: measurableT_comp.
+      exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
+    - by move=> ? _; rewrite lee_fin ler_wpM2r// ?powR_ge0// ler_normD.
+  under eq_integral=> ? _ do rewrite mulrDl EFinD.
+  rewrite ge0_integralD//; last 4 first.
+    - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0.
+    - apply: measurableT_comp => //; apply: measurable_funM.
+        exact: measurableT_comp.
+      exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
+    - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0.
+    - apply: measurableT_comp => //; apply: measurable_funM.
+        exact: measurableT_comp.
+      exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
+  rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) *
+      (\int[mu]_x (`|f x + g x| `^ p)%:E) `^ `1-(p^-1)).
+    rewrite muleDl; last 2 first.
+      - rewrite fin_num_poweR// -powR_Lnorm ?gt_eqF// fin_num_poweR//.
+        by rewrite ge0_fin_numE ?Lnorm_ge0.
+      - by rewrite ge0_adde_def// inE Lnorm_ge0.
+    apply: leeD.
+    - pose h := (@powR R ^~ (p - 1) \o normr \o (f \+ g))%R; pose i := (f \* h)%R.
+      rewrite [leLHS](_ : _ = 'N_1[i]%R); last first.
+        rewrite Lnorm1; apply: eq_integral => x _.
+        by rewrite normrM (ger0_norm (powR_ge0 _ _)).
+      rewrite [X in _ * X](_ : _ = 'N_(p / (p - 1))%:E[h]); last first.
+        rewrite unlock mulf_eq0 gt_eqF//= invr_eq0 subr_eq0 (gt_eqF p1).
+        rewrite onemV ?gt_eqF// invf_div; apply: congr2; last by [].
+        apply: eq_integral => x _; congr EFin.
+        rewrite norm_powR// normr_id -powRrM mulrCA divff ?mulr1//.
+        by rewrite subr_eq0 gt_eqF.
+      apply: (@hoelder _ _ _ _ _ _ p (p / (p - 1))) => //.
+      + exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
+      + by rewrite divr_gt0// subr_gt0.
+      + by rewrite invf_div -onemV ?gt_eqF// addrCA subrr addr0.
+    - pose h := (fun x => `|f x + g x| `^ (p - 1))%R; pose i := (g \* h)%R.
+      rewrite [leLHS](_ : _ = 'N_1[i]); last first.
+        rewrite Lnorm1; apply: eq_integral => x _ .
+        by rewrite normrM norm_powR// normr_id.
+      rewrite [X in _ * X](_ : _ = 'N_((1 - p^-1)^-1)%:E[h])//; last first.
+        rewrite unlock invrK invr_eq0 subr_eq0 eq_sym invr_eq1 (gt_eqF p1).
+        apply: congr2; last by [].
+        apply: eq_integral => x _; congr EFin.
+        rewrite -/(onem p^-1) onemV ?gt_eqF// norm_powR// normr_id -powRrM.
+        by rewrite invf_div mulrCA divff ?subr_eq0 ?gt_eqF// ?mulr1.
+      apply: (le_trans (@hoelder _ _ _ _ _ _ p (1 - p^-1)^-1 _ _ _ _ _)) => //.
+      + exact/measurableT_comp_powR/measurableT_comp/measurable_funD.
+      + by rewrite invr_gt0 onem_gt0// invf_lt1.
+      + by rewrite invrK addrCA subrr addr0.
+  rewrite -muleA; congr (_ * _).
+  under [X in X * _]eq_integral=> x _ do rewrite mulr_powRB1 ?subr_gt0//.
+  rewrite poweRD; last by rewrite poweRD_defE gt_eqF ?implyFb// subr_gt0 invf_lt1.
+  rewrite poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0.
+  congr (_ * _); rewrite poweRN.
+  - by rewrite unlock gt_eqF// fine_poweR.
+  - by rewrite -powR_Lnorm ?gt_eqF// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0.
+  Qed.
 
 End minkowski.