extract lemma, test notation (cont'd)

CHANGELOG_UNRELEASED.md

@@ -26,70 +26,17 @@
 - in `lebesgue_measure.v`:
   + lemma `closed_measurable`
 
-- in file `lebesgue_measure.v`,
-  + new lemmas `lebesgue_nearly_bounded`, and `lebesgue_regularity_inner`.
-- in file `measure.v`,
-  + new lemmas `measureU0`, `nonincreasing_cvg_mu`, and `epsilon_trick0`.
-- in file `real_interval.v`,
-  + new lemma `bigcup_itvT`.
-- in file `topology.v`,
-  + new lemma `uniform_nbhsT`.
-
-- in file `topology.v`,
-  + new definition `set_nbhs`.
-  + new lemmas `filterI_iter_sub`, `filterI_iterE`, `finI_fromI`, 
-    `filterI_iter_finI`, `smallest_filter_finI`, and `set_nbhsP`.
-
-- in file `lebesgue_measure.v`,
-  + new lemmas `pointwise_almost_uniform`, and 
-    `ae_pointwise_almost_uniform`.
 
-- in `exp.v`:
-  + lemmas `powRrM`, `gt0_ler_powR`,
-    `gt0_powR`, `norm_powR`, `lt0_norm_powR`,
-    `powRB`
-  + lemmas `poweRrM`, `poweRAC`, `gt0_poweR`,
-    `poweR_eqy`, `eqy_poweR`, `poweRD`, `poweRB`
-
-- in `mathcomp_extra.v`:
-  + definition `min_fun`, notation `\min`
-- in `classical_sets.v`:
-  + lemmas `set_predC`, `preimage_true`, `preimage_false`
-- in `lebesgue_measure.v`:
-  + lemmas `measurable_fun_ltr`, `measurable_minr`
-- in file `lebesgue_integral.v`,
-  + new lemmas `lusin_simple`, and `measurable_almost_continuous`.
-- in file `measure.v`,
-  + new lemmas `finite_card_sum`, and `measureU2`.
-
-- in `topology.v`:
-  + lemma `bigsetU_compact`
-
-- in `exp.v`:
-  + notation `` e `^?(r +? s) ``
-  + lemmas `expR_eq0`, `powRN`
-  + definition `poweRD_def`
-  + lemmas `poweRD_defE`, `poweRB_defE`, `add_neq0_poweRD_def`,
-    `add_neq0_poweRB_def`, `nneg_neq0_poweRD_def`, `nneg_neq0_poweRB_def`
-  + lemmas `powR_eq0`, `poweR_eq0`
-- in file `lebesgue_integral.v`,
-  + new lemma `approximation_sfun_integrable`.
-
-- in `classical_sets.v`:
-  + lemmas `properW`, `properxx`
-
-- in `classical_sets.v`:
-  + lemma `Zorn_bigcup`
 - in `lebesgue_measure.v`:
   + lemma `measurable_mulrr`
 
 - in `constructive_ereal.v`:
   + lemma `eqe_pdivr_mull`
 
 - in `lebesgue_integral.v`:
-  + definition `L_norm`, notation `'N[mu]_p[f]`
-  + lemmas `L_norm_ge0`, `eq_L_norm`
-  + lemmas `hoelder`
+  + definition `Lnorm`, notations `'N[mu]_p[f]`, `` `| f |_p ``
+  + lemmas `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0`
+  + lemma `hoelder`
 
 ### Changed
 

theories/lebesgue_integral.v

@@ -46,7 +46,7 @@ Require Import esum measure lebesgue_measure numfun exp itv.
 (*                           measure over T1, and m1 is a sigma finite        *)
 (*                           measure over T2                                  *)
 (*           'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1             *)
-(*                          The corresponding definition is L_norm            *)
+(*                          The corresponding definition is Lnorm.            *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -5355,39 +5355,69 @@ Qed.
 End sfinite_fubini.
 Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.
 
-Section L_norm.
-Context d (T : measurableType d) (R : realType)
-  (mu : {measure set T -> \bar R}).
+(* NB: move at the top of the file? *)
+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 "'`|' F '|_' p"
+  (at level 0, F at level 99, format "'[' '`|' F '|_' p ']'").
+
+Declare Scope Lnorm_scope.
+
+Section Lnorm.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
 Local Open Scope ereal_scope.
+Implicit Types (p : R) (f g : T -> R).
+
+Definition Lnorm p f := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1.
+
+Local Notation "`| f |_ p" := (Lnorm p f).
 
-Definition L_norm (p : R) (f : T -> R) : \bar R :=
-  (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1.
+Lemma Lnorm1 p f : `| f |_1 = \int[mu]_x `|f x|%:E.
+Proof.
+rewrite /Lnorm invr1// poweRe1//; last first.
+  by apply: integral_ge0 => t _; rewrite powRr1.
+by apply: eq_integral => t _; rewrite powRr1.
+Qed.
 
-Local Notation "'N_ p [ f ]" := (L_norm p f).
+Lemma Lnorm_ge0 p f : 0 <= `| f |_p. Proof. exact: poweR_ge0. Qed.
 
-Lemma L_norm_ge0 (p : R) (f : T -> R) : (0 <= 'N_p[f])%E.
-Proof. by rewrite /L_norm poweR_ge0. Qed.
+Lemma eq_Lnorm p f g : f =1 g -> `|f|_p = `|g|_p.
+Proof. by move=> fg; congr Lnorm; exact/funext. Qed.
 
-Lemma eq_L_norm (p : R) (f g : T -> R) : f =1 g -> 'N_p[f] = 'N_p[g].
-Proof. by move=> fg; congr L_norm; exact/funext. Qed.
+Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> `| f |_p = 0 ->
+  ae_eq mu [set: T] (fun x : T => (`|f x| `^ p)%:E) (cst 0).
+Proof.
+move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=.
+  apply: measurableT_comp => //.
+  apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //.
+  exact: measurableT_comp.
+under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//.
+by apply/fp/integral_ge0 => t _; rewrite lee_fin; exact: powR_ge0.
+Qed.
 
-End L_norm.
+End Lnorm.
 #[global]
-Hint Extern 0 (0 <= L_norm _ _ _) => solve [apply: L_norm_ge0] : core.
+Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core.
 
-Notation "'N[ mu ]_ p [ f ]" := (L_norm mu p f).
+Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
 
 Section hoelder.
-Context d (T : measurableType d) (R : realType).
+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 : T -> R) p :
+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.
 
-Let integrable_powR (f : T -> R) p : (0 < p)%R ->
-  measurable_fun setT f -> 'N[mu]_p[f] != +oo ->
+Local Notation "`| f |_ p" := (Lnorm mu p f).
+
+Let integrable_powR f p : (0 < p)%R ->
+  measurable_fun [set: T] f -> `| f |_p != +oo ->
   mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E).
 Proof.
 move=> p0 mf foo; apply/integrableP; split.
@@ -5399,65 +5429,55 @@ apply/eqP; congr (_ `^ _); apply/eq_integral.
 by move=> x _; rewrite gee0_abs // ?lee_fin ?powR_ge0.
 Qed.
 
-Local Notation "'N_ p [ f ]" := (L_norm mu p f).
-
-Let hoelder0 (f g : T -> R) (p q : R) :
-  measurable_fun setT f -> measurable_fun setT g ->
+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[mu]_p[f] = 0 ->
-  'N[mu]_1 [(f \* g)%R] <= 'N[mu]_p [f] * 'N[mu]_q [g].
+  `| f |_ p = 0 -> `| (f \* g)%R |_1  <= `| f |_p * `| g |_ q.
 Proof.
 move=> mf mg p0 q0 pq f0; rewrite f0 mul0e.
-suff: 'N_1 [(f \* g)%R] = 0%E by move=> ->.
-move: f0; rewrite /L_norm; move/poweR_eq0_eq0.
-rewrite /= invr1 poweRe1// => [fp|]; last first.
+suff: `| (f \* g)%R |_1 = 0 by move=> ->.
+rewrite /Lnorm /= invr1 poweRe1; last first.
   by apply: integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0.
-have {fp}f0 : ae_eq mu setT (fun x => (`|f x| `^ p)%:E) (cst 0).
-  apply/ae_eq_integral_abs => //=.
-  - apply: measurableT_comp => //; apply: measurableT_comp_powR.
-    exact: measurableT_comp.
-  - under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//.
-    by apply/fp/integral_ge0 => t _; rewrite lee_fin; exact: powR_ge0.
-rewrite (ae_eq_integral (cst 0)%E) => [|//||//|].
+rewrite (ae_eq_integral (cst 0)) => [|//||//|].
 - by rewrite integral0.
 - apply: measurableT_comp => //; apply: measurableT_comp_powR => //.
   by apply: measurableT_comp => //; exact: measurable_funM.
-- apply: filterS f0 => x /(_ I) /= [] /powR_eq0_eq0 fp0 _.
+- have : ae_eq mu setT (fun x => (`|f x| `^ p)%:E) (cst 0).
+    exact: Lnorm_eq0_eq0.
+  apply: filterS => x /(_ I) /= [] /powR_eq0_eq0 fp0 _.
   by rewrite powRr1// normrM fp0 mul0r.
 Qed.
 
-Let normed p f x := `|f x| / fine 'N_p[f].
+Let normed p f x := `|f x| / fine `|f|_p.
 
 Let normed_ge0 p f x : (0 <= normed p f x)%R.
-Proof. by rewrite /normed divr_ge0// fine_ge0// L_norm_ge0. Qed.
+Proof. by rewrite /normed divr_ge0// fine_ge0// Lnorm_ge0. Qed.
 
 Let measurable_normed p f : measurable_fun setT f ->
   measurable_fun setT (normed p f).
 Proof.
-move=> mf; rewrite (_ : normed _ _ = *%R (fine ('N[mu]_p[f]))^-1 \o normr \o f).
+move=> mf; rewrite (_ : normed _ _ = *%R (fine (`|f|_p))^-1 \o normr \o f).
   by apply: measurableT_comp => //; exact: measurableT_comp.
 by apply/funext => x /=; rewrite mulrC.
 Qed.
 
 Let normed_expR p f x : (0 < p)%R ->
   let F := normed p f in F x != 0%R -> expR (ln (F x `^ p) / p) = F x.
 Proof.
-move=> p0 F Fx0.
-rewrite ln_powR// mulrAC divff// ?gt_eqF// mul1r.
+move=> p0 F Fx0; rewrite ln_powR// mulrAC divff// ?gt_eqF// mul1r.
 by rewrite lnK// posrE lt_neqAle normed_ge0 eq_sym Fx0.
 Qed.
 
-Let integral_normed f p : (0 < p)%R -> 0 < 'N_p[f] ->
+Let integral_normed f p : (0 < p)%R -> 0 < `|f|_p ->
   mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E) ->
   \int[mu]_x (normed p f x `^ p)%:E = 1.
 Proof.
 move=> p0 fpos ifp.
-transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p[f] `^ p))%:E).
+transitivity (\int[mu]_x (`|f x| `^ p / fine (`|f|_p `^ p))%:E).
   apply: eq_integral => t _.
-  rewrite powRM//; last by rewrite invr_ge0 fine_ge0// L_norm_ge0.
-  rewrite -powR_inv1; last by rewrite fine_ge0 // L_norm_ge0.
+  rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0.
+  rewrite -powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0.
   by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0.
-rewrite /L_norm -poweRrM mulVf ?lt0r_neq0// poweRe1; last first.
+rewrite /Lnorm -poweRrM mulVf ?lt0r_neq0// poweRe1; last first.
   by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0.
 under eq_integral do rewrite EFinM muleC.
 rewrite integralZl//; apply/eqP; rewrite eqe_pdivr_mull ?mule1; last first.
@@ -5478,78 +5498,83 @@ under eq_integral.
 by [].
 Qed.
 
-Lemma hoelder (f g : T -> R) (p q : R) :
-  measurable_fun setT f -> measurable_fun setT g ->
+Let normed_convex f g p q x : (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1)%R = 1%R ->
+ (normed p f x * normed q g x <=
+  normed p f x `^ p / p + normed q g x `^ q / q)%R.
+Proof.
+move=> p0 q0 pq; set F := normed p f; set G := normed q g.
+have [Fx0|Fx0] := eqVneq (F x) 0%R.
+  by rewrite Fx0 mul0r powR0 ?gt_eqF// mul0r add0r divr_ge0 ?powR_ge0 ?ltW.
+have {}Fx0 : (0 < F x)%R.
+  by rewrite lt_neqAle eq_sym Fx0 divr_ge0// fine_ge0// Lnorm_ge0.
+have [Gx0|Gx0] := eqVneq (G x) 0%R.
+  by rewrite Gx0 mulr0 powR0 ?gt_eqF// mul0r addr0 divr_ge0 ?powR_ge0 ?ltW.
+have {}Gx0 : (0 < G x)%R.
+  by rewrite lt_neqAle eq_sym Gx0/= divr_ge0// fine_ge0// Lnorm_ge0.
+pose s x := ln ((F x) `^ p).
+pose t x := ln ((G x) `^ q).
+have : (expR (p^-1 * s x + q^-1 * t x) <=
+        p^-1 * expR (s x) + q^-1 * expR (t x))%R.
+  have -> : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK.
+  have K : (q^-1 \in `[0, 1])%R.
+    by rewrite in_itv/= invr_ge0 (ltW q0)/= -pq ler_paddl// invr_ge0 ltW.
+  exact: (convex_expR (@Itv.mk _ `[0, 1] q^-1 K)%R).
+rewrite expRD (mulrC _ (s x)) normed_expR ?gt_eqF// -/(F x).
+rewrite (mulrC _ (t x)) normed_expR ?gt_eqF// -/(G x) => /le_trans; apply.
+rewrite /s /t [X in (_ * X + _)%R](@lnK _ (F x `^ p)%R); last first.
+  by rewrite posrE powR_gt0.
+rewrite (@lnK _ (G x `^ q)%R); last by rewrite posrE powR_gt0.
+by rewrite mulrC (mulrC _ q^-1).
+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[mu]_1 [(f \* g)%R] <= 'N[mu]_p [f] * 'N[mu]_q [g].
+ `| (f \* g)%R |_1 <= `| f |_p * `| g |_q.
 Proof.
 move=> mf mg p0 q0 pq.
-have [f0|f0] := eqVneq 'N_p[f] 0%E; first exact: hoelder0.
-have [g0|g0] := eqVneq 'N_q[g] 0%E.
+have [f0|f0] := eqVneq `|f|_p 0%E; first exact: hoelder0.
+have [g0|g0] := eqVneq `|g|_q 0%E.
   rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC.
-  by under eq_L_norm do rewrite /= mulrC.
-have {f0}fpos : 0 < 'N_p[f] by rewrite lt_neqAle eq_sym f0//= L_norm_ge0.
-have {g0}gpos : 0 < 'N_q[g] by rewrite lt_neqAle eq_sym g0//= L_norm_ge0.
-have [foo|foo] := eqVneq 'N_p[f] +oo%E; first by rewrite foo gt0_mulye ?leey.
-have [goo|goo] := eqVneq 'N_q[g] +oo%E; first by rewrite goo gt0_muley ?leey.
+  by under eq_Lnorm do rewrite /= mulrC.
+have {f0}fpos : 0 < `|f|_p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0.
+have {g0}gpos : 0 < `|g|_q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0.
+have [foo|foo] := eqVneq `|f|_p +oo%E; first by rewrite foo gt0_mulye ?leey.
+have [goo|goo] := eqVneq `|g|_q +oo%E; first by rewrite goo gt0_muley ?leey.
 pose F := normed p f.
 pose G := normed q g.
-have exp_convex x : (F x * G x <= F x `^ p / p + G x `^ q / q)%R.
-  have [Fx0|Fx0] := eqVneq (F x) 0%R.
-    by rewrite Fx0 mul0r powR0 ?gt_eqF// mul0r add0r divr_ge0 ?powR_ge0 ?ltW.
-  have {}Fx0 : (0 < F x)%R.
-    by rewrite lt_neqAle eq_sym Fx0 divr_ge0// fine_ge0// L_norm_ge0.
-  have [Gx0|Gx0] := eqVneq (G x) 0%R.
-    by rewrite Gx0 mulr0 powR0 ?gt_eqF// mul0r addr0 divr_ge0 ?powR_ge0 ?ltW.
-  have {}Gx0 : (0 < G x)%R.
-    by rewrite lt_neqAle eq_sym Gx0/= divr_ge0// fine_ge0// L_norm_ge0.
-  pose s x := ln ((F x) `^ p).
-  pose t x := ln ((G x) `^ q).
-  have : (expR (p^-1 * s x + q^-1 * t x) <=
-          p^-1 * expR (s x) + q^-1 * expR (t x))%R.
-    have -> : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK.
-    have K : (q^-1 \in `[0, 1])%R.
-      by rewrite in_itv/= invr_ge0 (ltW q0)/= -pq ler_paddl// invr_ge0 ltW.
-    exact: (convex_expR (@Itv.mk _ `[0, 1] q^-1 K)%R).
-  rewrite expRD (mulrC _ (s x)) normed_expR ?gt_eqF// -/(F x).
-  rewrite (mulrC _ (t x)) normed_expR ?gt_eqF// -/(G x) => /le_trans; apply.
-  rewrite /s /t [X in (_ * X + _)%R](@lnK _ (F x `^ p)%R); last first.
-    by rewrite posrE powR_gt0.
-  rewrite (@lnK _ (G x `^ q)%R); last by rewrite posrE powR_gt0.
-  by rewrite mulrC (mulrC _ q^-1).
-have -> : 'N_1[(f \* g)%R] = 'N_1[(F \* G)%R] * 'N_p[f] * 'N_q[g].
-  rewrite {1}/L_norm; under eq_integral => x _ do rewrite powRr1//.
+have -> : `| (f \* g)%R |_1 = `| (F \* G)%R |_1 * `| f |_p * `| g |_q.
+  rewrite {1}/Lnorm; under eq_integral => x _ do rewrite powRr1//.
   rewrite invr1 poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin.
-  rewrite {1}/L_norm.
+  rewrite {1}/Lnorm.
   under [in RHS]eq_integral.
     move=> x _.
     rewrite /F /G /= /normed (mulrC `|f x|)%R mulrA -(mulrA (_^-1)).
     rewrite (mulrC (_^-1)) -mulrA ger0_norm; last first.
-      by rewrite mulr_ge0// divr_ge0 ?(fine_ge0,L_norm_ge0,invr_ge0).
+      by rewrite mulr_ge0// divr_ge0 ?(fine_ge0, Lnorm_ge0, invr_ge0).
     rewrite powRr1; last first.
-      by rewrite mulr_ge0// divr_ge0 ?(fine_ge0,L_norm_ge0,invr_ge0).
+      by rewrite mulr_ge0// divr_ge0 ?(fine_ge0, Lnorm_ge0, invr_ge0).
     rewrite mulrC -normrM EFinM.
     over.
   rewrite /= ge0_integralZl//; last 2 first.
     - apply: measurableT_comp => //; apply: measurableT_comp => //.
       exact: measurable_funM.
-    - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// L_norm_ge0.
+    - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0.
   rewrite -muleA muleC invr1 poweRe1; last first.
     rewrite mule_ge0//.
-      by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// L_norm_ge0.
+      by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0.
     by apply integral_ge0 => x _; rewrite lee_fin.
   rewrite muleA EFinM.
-  rewrite muleCA 2!muleA (_ : _ * 'N_p[f] = 1) ?mul1e; last first.
+  rewrite muleCA 2!muleA (_ : _ * `|f|_p = 1) ?mul1e; last first.
     apply/eqP; rewrite eqe_pdivr_mull ?mule1; last first.
       by rewrite gt_eqF// fine_gt0// fpos/= ltey.
-    by rewrite fineK// ?ge0_fin_numE ?ltey// L_norm_ge0.
-  rewrite (_ : 'N_q[g] * _ = 1) ?mul1e// muleC.
+    by rewrite fineK// ?ge0_fin_numE ?ltey// Lnorm_ge0.
+  rewrite (_ : `|g|_q * _ = 1) ?mul1e// muleC.
   apply/eqP; rewrite eqe_pdivr_mull ?mule1; last first.
     by rewrite gt_eqF// fine_gt0// gpos/= ltey.
-  by rewrite fineK// ?ge0_fin_numE ?ltey// L_norm_ge0.
-rewrite -(mul1e ('N_p[f] * _)) -muleA lee_pmul ?mule_ge0 ?L_norm_ge0//.
+  by rewrite fineK// ?ge0_fin_numE ?ltey// Lnorm_ge0.
+rewrite -(mul1e (`|f|_p * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//.
 apply: (@le_trans _ _ (\int[mu]_x (F x `^ p / p + G x `^ q / q)%:E)).
-  rewrite /L_norm invr1 poweRe1; last first.
+  rewrite /Lnorm invr1 poweRe1; last first.
     by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0.
   apply: ae_ge0_le_integral => //.
   - by move=> x _; exact: powR_ge0.
@@ -5560,8 +5585,8 @@ apply: (@le_trans _ _ (\int[mu]_x (F x `^ p / p + G x `^ q / q)%:E)).
   - by apply: measurableT_comp => //; apply: measurable_funD => //;
        apply: measurable_funM => //; apply: measurableT_comp_powR => //;
        exact: measurable_normed.
-  apply/aeW => x _.
-  by rewrite lee_fin powRr1// ger0_norm ?exp_convex// mulr_ge0// normed_ge0.
+  apply/aeW => x _; rewrite lee_fin powRr1// ger0_norm ?normed_convex//.
+ by rewrite mulr_ge0// normed_ge0.
 rewrite le_eqVlt; apply/orP; left; apply/eqP.
 under eq_integral do rewrite EFinD mulrC (mulrC _ (_^-1)).
 rewrite ge0_integralD//; last 4 first.