diff --git a/theories/exp.v b/theories/exp.v
index 2ac84ae6cb..e27115c5c9 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -954,8 +954,8 @@ move=> r0 x y.
 case: x => //= [x xint| _ _].
 - case: y => //= [y yint xy| _ _].
   - rewrite !lee_fin gt0_ler_powR//.
-    by move: xint; rewrite !in_itv /= andbT lee_fin => /andP [x0 _].
-    by move: yint; rewrite !in_itv /= andbT lee_fin => /andP [y0 _].
+    by move: xint; rewrite !in_itv /= leey andbT lee_fin.
+    by move: yint; rewrite !in_itv /= leey andbT lee_fin.
   - by case: eqP => [->|]; rewrite ?powRr0 ?leey.
 - by rewrite leye_eq => /eqP ->.
 Qed.
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 09b04fd56d..ae6503daff 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -346,22 +346,17 @@ Local Open Scope convex_scope.
 
 Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
 
-Let minkowski_half (f g : T -> R) (p : R) x : (1 < p)%R ->
+Let minkowski_half (f g : T -> R) (p : R) x : (1 <= p)%R ->
   (`| 2^-1 * f x + 2^-1 * g x | `^ p <= 2^-1 * `| f x | `^ p + 2^-1 * `| g x | `^ p)%R.
 Proof.
 move=> p1.
 apply: (@le_trans _ _ ((2^-1 * `| f x | + 2^-1 * `| g x |) `^ p))%R.
-  apply: gt0_ler_powR.
-  - by rewrite le_eqVlt; apply/orP; right; apply: (@lt_trans _ _ 1%R) => //.
-  - by rewrite in_itv/= andbT.
-  - by rewrite in_itv/= andbT.
-  - have -> : (2^-1 * `|f x| + 2^-1 * `|g x| = `|2^-1 * f x| + `|2^-1 * g x|)%R.
-      by rewrite !normrM !(@ger0_norm _ (2^-1)).
-    exact: ler_norm_add.
+  apply: ge0_ler_powR; rewrite ?nnegrE ?(le_trans _ p1)//.
+  by rewrite -[in leRHS](@ger0_norm _ (2^-1))// -!normrM; exact: ler_norm_add.
 rewrite {1 3}(_ : 2^-1 = 1 - 2^-1 :> R)%R; last by rewrite {2}(splitr 1) div1r addrK.
 have K : ((2^-1 : R) \in `[0, 1])%R.
   by rewrite in_itv//= invr_ge0 ler0n/= invf_le1// ler1n.
-apply (@convex_powR _ _ (ltW p1) (@Itv.mk _ `[0, 1] 2^-1 K)%R (`|f x|)%R (`|g x|)%R);
+apply (@convex_powR _ _ p1 (@Itv.mk _ `[0, 1] 2^-1 K)%R (`|f x|)%R (`|g x|)%R);
   by rewrite inE /= in_itv /= normr_ge0.
 Qed.
 
@@ -371,7 +366,7 @@ Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed.
 
 Let minkowski_lty (f g : T -> R) (p : R) :
   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.
+  (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 h x : (`| f x + g x | `^ p <= 2 `^ (p - 1) * (`| f x | `^ p  + `| g x | `^ p))%R.
@@ -381,12 +376,12 @@ have h x : (`| f x + g x | `^ p <= 2 `^ (p - 1) * (`| f x | `^ p  + `| g x | `^
   rewrite !powRM// !mulrA -powR_inv1//.
   rewrite -powRD; last by apply /implyP => _.
   by rewrite (addrC _ p) -mulrDr.
-rewrite /Lnorm gt_eqF ?(lt_trans _ p1)// poweR_lty//.
+rewrite /Lnorm gt_eqF ?(lt_le_trans _ p1)// poweR_lty//.
 apply: (@le_lt_trans _ _ (\int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p)%R)%:E)).
   apply: ge0_le_integral => //=.
-  - by move=> t _; rewrite lee_fin// powR_ge0.
-  - apply/EFin_measurable_fun/measurableT_comp_powR.
-    by apply: measurableT_comp => //; exact: measurable_funD.
+  - by move=> t _; rewrite lee_fin powR_ge0.
+  - by apply/EFin_measurable_fun/measurableT_comp_powR;
+      apply: measurableT_comp => //; exact: measurable_funD.
   - by move=> t _; rewrite lee_fin// mulr_ge0// ?addr_ge0 ?powR_ge0.
   - by apply/EFin_measurable_fun/measurable_funM => //; apply/measurable_funD => //;
       apply: measurableT_comp_powR => //; apply: measurableT_comp.
@@ -407,26 +402,35 @@ rewrite ge0_integralD//; last 4 first.
   - by apply/EFin_measurable_fun;
       apply: measurableT_comp_powR => //; apply: measurableT_comp.
 rewrite lte_add_pinfty//.
-- rewrite /= gt_eqF ?(lt_trans _ p1)// in Nfoo.
+- rewrite /= gt_eqF ?(lt_le_trans _ p1)// in Nfoo.
   apply: lty_poweRy Nfoo.
-  by rewrite invr_neq0// gt_eqF// (le_lt_trans _ p1).
-- rewrite /= gt_eqF ?(lt_trans _ p1)// in Ngoo.
+  by rewrite invr_neq0// gt_eqF// (lt_le_trans _ p1).
+- rewrite /= gt_eqF ?(lt_le_trans _ p1)// in Ngoo.
   apply: lty_poweRy Ngoo.
-  by rewrite invr_neq0// gt_eqF// (le_lt_trans _ p1).
+  by rewrite invr_neq0// gt_eqF// (lt_le_trans _ p1).
 Qed.
 
 Lemma minkowski (f g : T -> R) (p : R) :
   measurable_fun setT f -> measurable_fun setT g ->
-  (1 < p)%R ->
+  (1 <= p)%R ->
   'N_p%:E[(f \+ g)%R] <= 'N_p%:E[f] + 'N_p%:E[g].
 Proof.
-move=> mf mg p1.
+move=> mf mg.
+rewrite le_eqVlt => /orP [/eqP <-|p1].
+  rewrite !Lnorm1.
+  apply: (le_trans (y:=\int[mu]_x ((`|f x|)%:E + (`|g x|)%:E))).
+  apply: ge0_le_integral => //.
+  - by repeat apply: measurableT_comp => //; apply: measurable_funD.
+  - apply: measurableT_comp => //.
+    by apply: measurable_funD; apply: measurableT_comp.
+  - by move=> x _; rewrite lee_fin ler_norm_add.
+  by rewrite le_eqVlt ge0_integralD ?eqxx//; repeat apply: measurableT_comp => //.  
 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 apply: minkowski_lty => //; rewrite ltey; [exact: Nfoo|exact: Ngoo].
+  by apply: minkowski_lty => //; rewrite ?ltW// ltey; [exact: Nfoo|exact: Ngoo].
 have pm10 : (p - 1 != 0)%R.
   by rewrite gt_eqF// subr_gt0.
 have p0 : (0 < p)%R.