diff --git a/.nix/config.nix b/.nix/config.nix
index 25a13ce7a..3431ddf46 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -50,12 +50,16 @@ in
   ## will be created per bundle
   bundles."8.19".coqPackages = common-bundle // {
     coq.override.version = "8.19";
-    mathcomp.override.version = "2.2.0";
+    mathcomp.override.version = "master";
+    mathcomp-bigenough.override.version = "master";
+    mathcomp-finmap.override.version = "master";
   };
 
   bundles."8.20".coqPackages = common-bundle // {
     coq.override.version = "8.20";
-    mathcomp.override.version = "2.2.0";
+    mathcomp.override.version = "master";
+    mathcomp-bigenough.override.version = "master";
+    mathcomp-finmap.override.version = "master";
     ssprove.job = false;
   };
 
diff --git a/_CoqProject b/_CoqProject
index 713f59627..5735b84f1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -94,3 +94,4 @@ theories/pi_irrational.v
 theories/showcase/summability.v
 analysis_stdlib/Rstruct_topology.v
 analysis_stdlib/showcase/uniform_bigO.v
+theories/lspace.v
diff --git a/theories/charge.v b/theories/charge.v
index 64323cb44..433f5b492 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -1867,7 +1867,7 @@ have nuf A : d.-measurable A -> nu A = \int[mu]_(x in A) f x.
 move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //.
 - exact/measurable_funTS.
 - exact/measurable_funTS.
-- exact: ae_eq_subset ff'.
+- exact: (@ae_eq_subset _ _ _ _ mu setT A f f' (@subsetT _ A)).
 Qed.
 
 End radon_nikodym_sigma_finite.
@@ -2093,6 +2093,10 @@ move=> mE; apply: integral_ae_eq => //.
   by rewrite -Radon_Nikodym_SigmaFinite.f_integral.
 Qed.
 
+(* TODO: move back to measure.v, current version incompatible *)
+Lemma ae_eq_mul2l (f g h : T -> \bar R) D : f = g %[ae mu in D] -> (h \* f) = (h \* g) %[ae mu in D].
+Proof. by apply: filterS => x /= /[apply] ->. Qed.
+
 Lemma Radon_Nikodym_change_of_variables f E : measurable E ->
     nu.-integrable E f ->
   \int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) =
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 5b5b020f8..55e0a73fc 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -10,10 +10,10 @@ From mathcomp Require Import numfun exp convex itv.
 (**md**************************************************************************)
 (* # Hoelder's Inequality                                                     *)
 (*                                                                            *)
-(* This file provides Hoelder's inequality.                                   *)
+(* This file provides Hoelder's inequality and its consequences, most notably *)
+(* Minkowski's inequality and the convexity of the power function.            *)
 (* ```                                                                        *)
-(*           'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1             *)
-(*                          The corresponding definition is Lnorm.            *)
+(*           'N[mu]_p[f] == the p-norm of f with measure mu                   *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -40,7 +40,7 @@ HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType}
     (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) :=
   match p with
   | p%:E => (if p == 0%R then
-              mu (f @^-1` (setT `\ 0%R))
+              (mu (f @^-1` (setT `\ 0%R))) `^ p^-1
             else
               (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1)%E
   | +oo%E => (if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0)%E
@@ -57,6 +57,20 @@ Implicit Types (p : \bar R) (f g : T -> R) (r : R).
 
 Local Notation "'N_ p [ f ]" := (Lnorm mu p f).
 
+Lemma Lnorm0 p : 1 <= p -> 'N_p[cst 0%R] = 0.
+Proof.
+rewrite unlock /Lnorm.
+case: p => [r||//].
+- rewrite lee_fin => r1.
+  have r0: r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1).
+  rewrite gt_eqF ?(lt_le_trans _ r1)//.
+  under eq_integral => x _ do rewrite /= normr0 powR0//.
+  by rewrite integral0 poweR0r// invr_neq0.
+case: ifPn => //mu0 _.
+rewrite (_ : normr \o _ = 0%R); last by apply: funext => x/=; rewrite normr0.
+exact: ess_sup_cst.
+Qed.
+
 Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E.
 Proof.
 rewrite unlock oner_eq0 invr1// poweRe1//.
@@ -74,16 +88,36 @@ 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).
+Lemma Lnorm_eq0_eq0 (f : T -> R) p :
+  measurable_fun setT f -> (0 < p)%E -> 'N_p[f] = 0 -> f = 0%R %[ae mu].
 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.
+rewrite unlock /Lnorm => mf.
+case: p => [r r0||].
+- case: ifPn => _.
+    rewrite preimage_setI preimage_setT setTI -preimage_setC.
+    move=> /poweR_eq0_eq0 /negligibleP.
+    move/(_ (measurableC _)); rewrite -[X in d.-measurable X]setTI.
+    move/(_ (mf _ _ _)).
+    by case=> // A [mA muA0 fA]; exists A; split => // x/= ?; exact: fA.
+  move=> /poweR_eq0_eq0.
+  move=> /(_ (integral_ge0 _ _)) h.
+  have: (\int[mu]_x (`|f x| `^ r)%:E)%E = 0 by apply: h => x _; rewrite lee_fin powR_ge0.
+  under eq_integral => x _ do rewrite -[_%:E]gee0_abs ?lee_fin ?powR_ge0//.
+  have mp: measurable_fun [set: T] (fun x : T => (`|f x| `^ r)%:E).
+    apply: measurableT_comp => //.
+    apply (measurableT_comp (measurable_powR _)) => //.
+    exact: measurableT_comp.
+  move/(ae_eq_integral_abs _ measurableT mp).
+  apply: filterS => x/= /[apply].
+  by case=> /powR_eq0_eq0 /eqP; rewrite normr_eq0 => /eqP.
+- case: ifPn => [mu0 _|].
+    exact: ess_sup_eq0.
+  rewrite ltNge => /negbNE mu0 _ _.
+  suffices mueq0: mu setT = 0 by exact: ae_eq0.
+  move: mu0 (measure_ge0 mu setT) => mu0 mu1.
+  suffices: (mu setT <= 0 <= mu setT)%E by move/le_anti.
+  by rewrite mu0 mu1.
+by [].
 Qed.
 
 Lemma powR_Lnorm f r : r != 0%R ->
@@ -93,9 +127,39 @@ move=> r0; rewrite unlock (negbTE r0) -poweRrM mulVf// poweRe1//.
 by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0.
 Qed.
 
+Lemma oppr_Lnorm f p :
+  'N_p[\- f]%R = 'N_p[f].
+Proof.
+rewrite unlock /Lnorm.
+case: p => /= [r||//].
+  case: eqP => _. congr ((mu _) `^ _).
+    rewrite !preimage_setI.
+    congr (_ `&` _).
+    rewrite -!preimage_setC.
+    congr (~` _).
+    rewrite /preimage.
+    apply: funext => x/=.
+    rewrite -{1}oppr0.
+    apply: propext. split; last by move=> ->.
+    by move/oppr_inj.
+  by under eq_integral => x _ do rewrite normrN.
+rewrite compA (_ : normr \o -%R = normr)//.
+apply: funext => x/=; exact: normrN.
+Qed.
+
+Lemma Lnorm_cst1 r : ('N_r%:E[cst 1%R] = (mu setT)`^(r^-1)).
+Proof.
+rewrite unlock /Lnorm.
+case: ifPn => [_|].
+  by rewrite preimage_cst ifT// inE/=; split => //; apply/eqP; rewrite oner_neq0.
+under eq_integral => x _ do rewrite normr1 powR1 (_ : 1 = cst 1 x)%R// -indicT.
+by rewrite integral_indic// setTI.
+Qed.
+
 End Lnorm_properties.
 
 #[global]
+
 Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core.
 
 Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
@@ -144,11 +208,12 @@ 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.
+rewrite -lte_fin.
 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.
+- apply: filterS (Lnorm_eq0_eq0 mf p0 f0) => x /(_ I)[] + _.
+  by rewrite normrM => ->; rewrite normr0 mul0r.
 Qed.
 
 Let normalized p f x := `|f x| / fine 'N_p%:E[f].
@@ -502,4 +567,20 @@ congr (_ * _); rewrite poweRN.
 - by rewrite -powR_Lnorm ?gt_eqF// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0.
 Qed.
 
+Lemma minkowski' f g p :
+  measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R ->
+  'N_p%:E[f] <= 'N_p%:E[f \+ g] + 'N_p%:E[g].
+Proof.
+move=> mf mg p1.
+rewrite (_ : f = ((f \+ g) \+ (-%R \o g))%R); last first.
+  by apply: funext => x /=; rewrite -addrA subrr addr0.
+rewrite [X in _ <= 'N__[X] + _](_ : ((f \+ g \- g) \+ g)%R = (f \+ g)%R); last first.
+  by apply: funext => x /=; rewrite -addrA [X in _ + _ + X]addrC subrr addr0.
+rewrite (_ : 'N__[g] = 'N_p%:E[-%R \o g]); last first.
+  by rewrite oppr_Lnorm.
+apply: minkowski => //.
+  apply: measurable_funD => //.
+apply: measurableT_comp => //.
+Qed.
+
 End minkowski.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 8a966ebcb..091e4d1cd 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -272,6 +272,8 @@ Lemma mfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed.
 Lemma mfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed.
 Lemma mfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed.
 Lemma mfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed.
+Lemma mfunMn f n : (f *+ n) = (fun x => f x *+ n) :> (_ -> _).
+Proof. by apply/funext=> x; elim: n => //= n; rewrite !mulrS !mfunD /= => ->. Qed.
 Lemma mfun_sum I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) :
   (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
 Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
@@ -285,6 +287,7 @@ HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g).
 HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f).
 HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g).
 HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g).
+(* TODO: fix this: HB.instance Definition _ f (n : nat) := MeasurableFun.copy (fun x => f x *+ n) (f *+ n). *)
 
 Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D.
 
@@ -3726,11 +3729,9 @@ Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType)
         (mu : {measure set T -> \bar R}).
 
-Local Notation ae_eq := (ae_eq mu).
-
 Let ae_eq_integral_abs_bounded (D : set T) (mD : measurable D) (f : T -> \bar R)
     M : measurable_fun D f -> (forall x, D x -> `|f x| <= M%:E) ->
-  ae_eq D f (cst 0) -> \int[mu]_(x in D) `|f x|%E  = 0.
+  (\forall x \ae mu, D x -> f x = 0) -> \int[mu]_(x in D) `|f x|%E  = 0.
 Proof.
 move=> mf fM [N [mA mN0 Df0N]].
 pose Df_neq0 := D `&` [set x | f x != 0].
@@ -3759,7 +3760,8 @@ by rewrite mule0 -eq_le => /eqP.
 Qed.
 
 Lemma ae_eq_integral_abs (D : set T) (mD : measurable D) (f : T -> \bar R) :
-  measurable_fun D f -> \int[mu]_(x in D) `|f x| = 0 <-> ae_eq D f (cst 0).
+    measurable_fun D f ->
+  \int[mu]_(x in D) `|f x| = 0 <-> (\forall x \ae mu, D x -> f x = 0).
 Proof.
 move=> mf; split=> [iDf0|Df0].
   exists (D `&` [set x | f x != 0]); split;
@@ -3813,7 +3815,7 @@ transitivity (limn (fun n => \int[mu]_(x in D) (f_ n x) )).
     have [ftm|ftm] := leP `|f t|%E m%:R%:E.
       by rewrite lexx /= (le_trans ftm)// lee_fin ler_nat.
     by rewrite (ltW ftm) /= lee_fin ler_nat.
-have ae_eq_f_ n : ae_eq D (f_ n) (cst 0).
+have ae_eq_f_ n : (f_ n) = (cst 0) %[ae mu in D].
   case: Df0 => N [mN muN0 DfN].
   exists N; split => // t /= /not_implyP[Dt fnt0].
   apply: DfN => /=; apply/not_implyP; split => //.
@@ -3922,7 +3924,7 @@ Qed.
 Lemma ge0_ae_eq_integral (D : set T) (f g : T -> \bar R) :
   measurable D -> measurable_fun D f -> measurable_fun D g ->
   (forall x, D x -> 0 <= f x) -> (forall x, D x -> 0 <= g x) ->
-  ae_eq D f g -> \int[mu]_(x in D) (f x) = \int[mu]_(x in D) (g x).
+  f = g %[ae mu in D] -> \int[mu]_(x in D) (f x) = \int[mu]_(x in D) (g x).
 Proof.
 move=> mD mf mg f0 g0 [N [mN N0 subN]].
 rewrite integralEpatch// [RHS]integralEpatch//.
@@ -3940,7 +3942,7 @@ Qed.
 
 Lemma ae_eq_integral (D : set T) (g f : T -> \bar R) :
   measurable D -> measurable_fun D f -> measurable_fun D g ->
-  ae_eq D f g -> integral mu D f = integral mu D g.
+  f = g %[ae mu in D] -> integral mu D f = integral mu D g.
 Proof.
 move=> mD mf mg /ae_eq_funeposneg[Dfgp Dfgn].
 rewrite integralE// [in RHS]integralE//; congr (_ - _).
diff --git a/theories/lspace.v b/theories/lspace.v
new file mode 100644
index 000000000..60a3b887c
--- /dev/null
+++ b/theories/lspace.v
@@ -0,0 +1,460 @@
+(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
+From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssralg ssrnum ssrint interval finmap.
+From mathcomp Require Import boolp reals ereal.
+From HB Require Import structures.
+From mathcomp Require Import classical_sets signed functions topology normedtype cardinality.
+From mathcomp Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral.
+From mathcomp Require Import exp hoelder.
+
+(******************************************************************************)
+(*                                                                            *)
+(*         LfunType mu p == type of measurable functions f such that the      *)
+(*                          integral of |f| ^ p is finite                     *)
+(*            LType mu p == type of the elements of the Lp space              *)
+(*          mu.-Lspace p == Lp space                                          *)
+(*                                                                            *)
+(******************************************************************************)
+
+Reserved Notation "mu .-Lspace p" (at level 4, format "mu .-Lspace  p").
+
+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.
+
+Definition finite_norm d (T : measurableType d) (R : realType)
+    (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) :=
+  ('N[ mu ]_p [ f ] < +oo)%E.
+
+HB.mixin Record isLfun d (T : measurableType d) (R : realType)
+    (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) (f : T -> R)
+  of @MeasurableFun d _ T R f := {
+  lfuny : finite_norm mu p f
+}.
+
+#[short(type=LfunType)]
+HB.structure Definition Lfun d (T : measurableType d) (R : realType)
+    (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) :=
+  {f of @MeasurableFun d _ T R f & isLfun d T R mu p p1 f}.
+
+Arguments lfuny {d} {T} {R} {mu} {p} _.
+#[global] Hint Resolve lfuny : core.
+#[global] Hint Extern 0 (@LfunType _ _ _ _ _) =>
+  solve [apply: lfuny] : core.
+
+Section Lfun_canonical.
+Context d (T : measurableType d) (R : realType).
+Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E).
+
+HB.instance Definition _ := gen_eqMixin (LfunType mu p1).
+HB.instance Definition _ := gen_choiceMixin (LfunType mu p1).
+
+End Lfun_canonical.
+
+Section Lequiv.
+Context d (T : measurableType d) (R : realType).
+Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E).
+
+Definition Lequiv (f g : LfunType mu p1) := `[< f = g %[ae mu] >].
+
+Let Lequiv_refl : reflexive Lequiv.
+Proof.
+by move=> f; exact/asboolP/(filterS _ (ae_eq_refl mu setT (EFin \o f))).
+Qed.
+
+Let Lequiv_sym : symmetric Lequiv.
+Proof.
+by move=> f g; apply/idP/idP => /asboolP h; apply/asboolP/ae_eq_sym.
+Qed.
+
+Let Lequiv_trans : transitive Lequiv.
+Proof.
+by move=> f g h /asboolP gf /asboolP fh; apply/asboolP/(ae_eq_trans gf fh).
+Qed.
+
+Canonical Lequiv_canonical :=
+  EquivRel Lequiv Lequiv_refl Lequiv_sym Lequiv_trans.
+
+Local Open Scope quotient_scope.
+
+Definition LspaceType := {eq_quot Lequiv}.
+Canonical LspaceType_quotType := [the quotType _ of LspaceType].
+Canonical LspaceType_eqType := [the eqType of LspaceType].
+Canonical LspaceType_choiceType := [the choiceType of LspaceType].
+Canonical LspaceType_eqQuotType := [the eqQuotType Lequiv of LspaceType].
+
+Lemma LequivP (f g : LfunType mu p1) :
+  reflect (f = g %[ae mu]) (f == g %[mod LspaceType]).
+Proof. by apply/(iffP idP); rewrite eqmodE// => /asboolP. Qed.
+
+Record LType := MemLType { Lfun_class : LspaceType }.
+Coercion LfunType_of_LType (f : LType) : LfunType mu p1 :=
+  repr (Lfun_class f).
+
+End Lequiv.
+
+Section Lspace.
+Context d (T : measurableType d) (R : realType).
+Variable mu : {measure set T -> \bar R}.
+
+Definition Lspace p (p1 : (1 <= p)%E) := [set: LType mu p1].
+Arguments Lspace : clear implicits.
+
+Lemma LType1_integrable (f : LType mu (@lexx _ _ 1%E)) : mu.-integrable setT (EFin \o f).
+Proof.
+apply/integrableP; split; first exact/EFin_measurable_fun.
+have := lfuny _ f.
+rewrite /finite_norm unlock /Lnorm ifF ?oner_eq0// invr1 poweRe1; last first.
+  by apply integral_ge0 => x _; rewrite lee_fin powRr1//.
+by under eq_integral => i _ do rewrite powRr1//.
+Qed.
+
+Let le12 : (1 <= 2%:E :> \bar R)%E.
+rewrite lee_fin.
+rewrite (ler_nat _ 1 2).
+by [].
+Qed.
+
+Lemma LType2_integrable_sqr (f : LType mu le12) :
+  mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)).
+Proof.
+apply/integrableP; split.
+  exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f).
+rewrite (@lty_poweRy _ _ (2^-1))//.
+rewrite (le_lt_trans _ (lfuny _ f))//.
+rewrite unlock /Lnorm ifF ?gt_eqF//.
+rewrite gt0_ler_poweR//.
+- by rewrite in_itv/= integral_ge0// leey.
+- rewrite in_itv/= leey integral_ge0// => x _.
+  by rewrite lee_fin powR_ge0.
+rewrite ge0_le_integral//.
+- apply: measurableT_comp => //.
+  exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f).
+- by move=> x _; rewrite lee_fin powR_ge0.
+- exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R)/measurableT_comp.
+- by move=> t _/=; rewrite lee_fin normrX powR_mulrn.
+Qed.
+
+End Lspace.
+Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope.
+
+(* move to hoelder.v *)
+Section conjugate.
+Context d (T : measurableType d) (R : realType).
+Variables (mu : {measure set T -> \bar R}) (p : \bar R).
+Hypothesis (p1 : (1 <= p)%E).
+
+Local Open Scope classical_set_scope.
+Local Open Scope ereal_scope.
+
+Definition conjugate :=
+  match p with
+  | r%:E => [get q : R | r^-1 + q^-1 = 1]%:E
+  | +oo  => 1
+  | -oo  => 0
+  end.
+
+Lemma conjugateE :
+  conjugate = if p is r%:E then (r * (r-1)^-1)%:E
+              else if p == +oo then 1 else 0.
+Proof.
+rewrite /conjugate.
+move: p1.
+case: p => [r|//=|//].
+rewrite lee_fin => r1.
+have r0 : r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1).
+congr (_%:E).
+apply: get_unique.
+  by rewrite invf_div mulrBl divff// mul1r addrCA subrr addr0.
+move=> /= y h0.
+suffices -> : y = (1 - r^-1)^-1.
+  by rewrite -(mul1r r^-1) -{1}(divff r0) -mulrBl invf_div.
+by rewrite -h0 -addrAC subrr add0r invrK.
+Qed.
+
+End conjugate.
+
+
+Section lfun_pred.
+Context d (T : measurableType d) (R : realType).
+Variables (mu : {measure set T -> \bar R}) (p : \bar R).
+
+Definition finlfun : {pred _ -> _} := mem [set f | finite_norm mu p f].
+Definition lfun : {pred _ -> _} := [predI @mfun _ _ T R & finlfun].
+Definition lfun_key : pred_key lfun. Proof. exact. Qed.
+Canonical lfun_keyed := KeyedPred lfun_key.
+Lemma sub_lfun_mfun : {subset lfun <= mfun}. Proof. by move=> x /andP[]. Qed.
+Lemma sub_lfun_finlfun : {subset lfun <= finlfun}. Proof. by move=> x /andP[]. Qed.
+End lfun_pred.
+
+
+Lemma minkowskie :
+forall [d : measure_display] [T : measurableType d] [R : realType] 
+  (mu : measure T R) [f g : T -> R] [p : \bar R],
+measurable_fun [set: T] f ->
+measurable_fun [set: T] g ->
+(1 <= p)%E -> ('N[mu]_p[(f \+ g)%R] <= 'N[mu]_p[f] + 'N[mu]_p[g])%E.
+(* TODO: Jairo is working on this *)
+Admitted.
+
+
+Section lfun.
+Context d (T : measurableType d) (R : realType).
+Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E).
+
+Notation lfun := (@lfun _ T R mu p).
+Section Sub.
+Context (f : T -> R) (fP : f \in lfun).
+Definition lfun_Sub1_subproof :=
+  @isMeasurableFun.Build d _ T R f (set_mem (sub_lfun_mfun fP)).
+#[local] HB.instance Definition _ := lfun_Sub1_subproof.
+Definition lfun_Sub2_subproof :=
+  @isLfun.Build d T R mu p p1 f (set_mem (sub_lfun_finlfun fP)).
+
+Import HBSimple.
+
+#[local] HB.instance Definition _ := lfun_Sub2_subproof.
+Definition lfun_Sub : LfunType mu p1 := f.
+End Sub.
+
+Lemma lfun_rect (K : LfunType mu p1 -> Type) :
+  (forall f (Pf : f \in lfun), K (lfun_Sub Pf)) -> forall u, K u.
+Proof.
+move=> Ksub [f [[Pf1] [Pf2]]].
+have Pf : f \in lfun by apply/andP; rewrite ?inE.
+have -> : Pf1 = set_mem (sub_lfun_mfun Pf) by [].
+have -> : Pf2 = set_mem (sub_lfun_finlfun Pf) by [].
+exact: Ksub.
+Qed.
+
+Lemma lfun_valP f (Pf : f \in lfun) : lfun_Sub Pf = f :> (_ -> _).
+Proof. by []. Qed.
+
+HB.instance Definition _ := isSub.Build _ _ (LfunType mu p1) lfun_rect lfun_valP.
+
+Lemma lfuneqP (f g : LfunType mu p1) : f = g <-> f =1 g.
+Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
+
+HB.instance Definition _ := [Choice of LfunType mu p1 by <:].
+
+Import numFieldNormedType.Exports.
+
+Lemma lfuny0 : finite_norm mu p (cst 0).
+Proof. by rewrite /finite_norm Lnorm0. Qed.
+
+HB.instance Definition _ := @isLfun.Build d T R mu p p1 (cst 0) lfuny0.
+
+Lemma mfunP (f : {mfun T >-> R}) : (f : T -> R) \in mfun.
+Proof. exact: valP. Qed.
+
+Lemma lfunP (f : LfunType mu p1) : (f : T -> R) \in lfun.
+Proof. exact: valP. Qed.
+
+Lemma mfun_scaler_closed : scaler_closed (@mfun _ _ T R).
+Proof. move=> a/= f; rewrite !inE; exact: measurable_funM. Qed.
+
+HB.instance Definition _ := GRing.isScaleClosed.Build _ _ (@mfun _ _ T R)
+  mfun_scaler_closed.
+HB.instance Definition _ := [SubZmodule_isSubLmodule of {mfun T >-> R} by <:].
+
+Lemma LnormZ (f : LfunType mu p1) a :
+  ('N[mu]_p[a \*: f] = `|a|%:E * 'N[mu]_p[f])%E.
+Proof.
+rewrite unlock /Lnorm.
+move: p p1 f.
+case=> //[r r1 f|].
+  rewrite gt_eqF ?(lt_le_trans ltr01)//.
+  under eq_integral => x _/= do rewrite -mulr_algl scaler1 normrM powRM ?EFinM//.
+  rewrite integralZl//; last first.
+    apply /integrableP; split.
+      apply: measurableT_comp => //.
+      rewrite (_ : (fun x : T => `|f x| `^ r) = (@powR R)^~ r \o normr \o f)//.
+      by repeat apply: measurableT_comp => //.
+    apply: (@lty_poweRy _ _ r^-1).
+      by rewrite gt_eqF// invr_gt0 ?(lt_le_trans ltr01).
+    have -> : ((\int[mu]_x `|(`|f x| `^ r)%:E|) `^ r^-1 = 'N[mu]_r%:E[f])%E.
+      rewrite unlock /Lnorm gt_eqF ?(lt_le_trans ltr01)//.
+      by under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//.
+    exact: (lfuny r1 f).
+  rewrite poweRM ?integral_ge0=> //[||x _]; rewrite ?lee_fin ?powR_ge0//.
+  by rewrite poweR_EFin -powRrM mulfV ?gt_eqF ?(lt_le_trans ltr01)// powRr1.
+move=> p0 f.
+case: ifP => mu0.
+  rewrite (_ : normr \o a \*: f = (`|a|) \*: (normr \o f)); last first.
+    by apply: funext => x/=; rewrite normrZ.
+  rewrite ess_supM//.
+  by near=> x=> /=.
+by rewrite mule0.
+Unshelve. end_near.
+Qed.
+
+Lemma lfun_submod_closed : submod_closed (lfun).
+Proof.
+split.
+  rewrite -[0]/(cst 0). exact: lfunP.
+move=> a/= f g fP gP.
+rewrite -[f]lfun_valP -[g]lfun_valP.
+move: (lfun_Sub _) (lfun_Sub _) => {fP} f {gP} g.
+rewrite !inE rpredD ?rpredZ ?mfunP//=.
+apply: mem_set => /=.
+rewrite /finite_norm.
+apply: (le_lt_trans (minkowskie _ _ _ _)) => //=.
+  suff: a *: (g : T -> R) \in mfun by exact: set_mem.
+  by rewrite rpredZ//; exact: mfunP.
+rewrite lte_add_pinfty//; last exact: lfuny.
+by rewrite LnormZ lte_mul_pinfty//; exact: lfuny.
+Qed.
+
+HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ lfun
+  lfun_submod_closed.
+HB.instance Definition _ := [SubChoice_isSubLmodule of LfunType mu p1 by <:].
+
+End lfun.
+
+
+Section Lspace_norm.
+Context d (T : measurableType d) (R : realType).
+Variable mu : {measure set T -> \bar R}.
+Variable (p : \bar R) (p1 : (1 <= p)%E).
+
+(* 0 - + should come with proofs that they are in LfunType mu p *)
+
+Notation ty := (LfunType mu p1).
+Definition nm f := fine ('N[mu]_p[f]).
+
+Lemma finite_norm_fine (f : ty) : (nm f)%:E = 'N[mu]_p[f].
+Proof. 
+by rewrite /nm fineK// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=; exact: lfuny.
+Qed.
+
+Lemma ler_Lnorm_add (f g : ty) :
+  nm (f + g) <= nm f + nm g.
+Proof. by rewrite -lee_fin EFinD !finite_norm_fine minkowskie. Qed.
+
+Lemma natmulfctE (U : pointedType) (K : ringType) (f : U -> K) n :
+  f *+ n = (fun x => f x *+ n).
+Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed.
+
+Lemma LnormN (f : ty) : nm (\-f) = nm f.
+Proof. by rewrite /nm oppr_Lnorm. Qed.
+
+Lemma enatmul_ninfty (n : nat) : (-oo *+ n.+1 = -oo :> \bar R)%E \/ (-oo *+ n.+1 = +oo :> \bar R)%E.
+Proof. by elim: n => //=[|n []->]; rewrite ?addNye; left. Qed.
+
+Lemma Lnorm_natmul (f : ty) k : nm (f *+ k) = nm f *+ k.
+Proof.
+apply/EFin_inj; rewrite finite_norm_fine -scaler_nat LnormZ normr_nat.
+by rewrite -[in RHS]mulr_natl EFinM finite_norm_fine.
+Qed.
+
+
+HB.about Num.Zmodule_isSemiNormed.Build.
+
+(* TODO : fix the definition *)
+HB.instance Definition _ :=
+  @Num.Zmodule_isSemiNormed.Build R (LfunType mu p1)
+     nm ler_Lnorm_add Lnorm_natmul LnormN.
+
+(* todo: add equivalent of mx_normZ and HB instance *)
+
+Lemma nm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu].
+Proof.
+rewrite /nm=> /eqP; rewrite -eqe=> /eqP; rewrite finite_norm_fine=> /Lnorm_eq0_eq0.
+by apply; rewrite ?(lt_le_trans _ p1).
+Qed.
+
+
+End Lspace_norm.
+
+Section Lspace_inclusion.
+Context d (T : measurableType d) (R : realType).
+Variable mu : {measure set T -> \bar R}.
+
+(* the following lemma is not needed, but looks useful, should we include it anyways? *)
+Lemma mul_lte_pinfty (x y : \bar R) : (x \is a fin_num -> 0 < x -> x * y < +oo -> y < +oo)%E.
+Proof. rewrite fin_numE => /andP[/eqP xNoo /eqP xoo].
+move: x xNoo xoo.
+case => // r _ _ rgt0.
+rewrite /mule.
+case: y => //[r0 ?|].
+  by rewrite ltry.
+case: ifP => //. by move: rgt0 => /[swap] /eqP -> /eqP; rewrite ltxx.
+case: ifP => //. by rewrite rgt0.
+Qed.
+
+Local Open Scope ereal_scope.
+
+Lemma measure_is_zero : mu [set: T] = 0%E -> mu = mzero.
+Admitted.
+
+Lemma Lspace_inclusion (p q : \bar R) :
+  forall (p1 : 1 <= p) (q1 : 1 <= q),
+    mu [set: T] < +oo -> p < q -> forall (f : {mfun T >-> R}), finite_norm mu q f -> finite_norm mu p f.
+Proof.
+have := measure_ge0 mu [set: T]; rewrite le_eqVlt => /orP[/eqP mu0 p1 q1 _ _ f _|mu_pos].
+  rewrite /finite_norm unlock /Lnorm.
+  move: p p1; case=> //; last by rewrite -mu0 ltxx.
+  move=> r r1; rewrite gt_eqF ?(lt_le_trans ltr01)//.
+  rewrite measure_is_zero// integral_measure_zero.
+  by rewrite poweR0r// gt_eqF// invr_gt0 (lt_le_trans ltr01).
+move: p q.
+case=> //[p|]; case=> //[q|] p1 q1; last first.
+  have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01).
+  move=> muoo _ f.
+  rewrite /finite_norm unlock /Lnorm mu_pos gt_eqF// => supf_lty.
+  rewrite poweR_lty// integral_fune_lt_pinfty => //.
+  apply: measurable_bounded_integrable => //.
+    rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)%R//.
+    apply: measurableT_comp => //=.
+    exact: measurableT_comp.
+  rewrite boundedE.
+  near=> A=> x/= _.
+  rewrite norm_powR// normr_id normr1 mulr1.
+  admit.
+move=> mu_fin pleq f ffin.
+have:= ffin; rewrite /finite_norm.
+have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01).
+have q0 : (0 < q)%R by rewrite ?(lt_le_trans ltr01).
+have qinv0 : q^-1 != 0%R by rewrite invr_neq0// gt_eqF.
+pose r := q/p.
+pose r' := (1 - r^-1)^-1.
+have := (@hoelder _ _ _ mu (fun x => `|f x| `^ p) (cst 1)%R r r')%R.
+rewrite (_ : (_ \* cst 1)%R = (fun x : T => `|f x| `^ p))%R -?fctM ?mulr1//.
+rewrite Lnorm_cst1 unlock /Lnorm invr1.
+rewrite !ifF; last 4 first.
+- by apply/eqP => p0'; rewrite p0' ltxx in p0.
+- by apply/eqP => q0'; rewrite q0' ltxx in q0.
+- by rewrite /r gt_eqF// divr_gt0// (lt_le_trans ltr01).
+- exact/negP/negP.
+under [X in X `^ 1 <= _] eq_integral => x _ do
+  rewrite powRr1// norm_powR// normrE.
+under [X in X`^ r^-1 * mu _ `^_]eq_integral => x _ do
+  rewrite /r norm_powR normrE ?powR_ge0// -powRrM mulrCA mulfV ?mulr1// ?gt_eqF//.
+rewrite [X in X <= _]poweRe1; last
+  by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0.
+move=> h1 /lty_poweRy h2.
+apply: poweR_lty.
+apply: le_lt_trans.
+  apply: h1.
+  - rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)%R//.
+    apply: measurableT_comp => //=.
+    exact: measurableT_comp => //=.
+  - exact: measurable_cst.
+  - rewrite/r divr_gt0//.
+  - rewrite /r' invr_gt0 subr_gt0 invf_lt1 ?(lt_trans ltr01)//;
+    by rewrite /r ltr_pdivlMr// mul1r.
+  - by rewrite /r' /r invf_div invrK addrCA subrr addr0.
+rewrite muleC lte_mul_pinfty ?fin_numElt?poweR_ge0//.
+  by rewrite (lt_le_trans _ (poweR_ge0 _ _)) ?poweR_lty.
+rewrite poweR_lty// (lty_poweRy qinv0)//.
+have:= ffin; rewrite /finite_norm unlock/Lnorm ifF//.
+by apply/eqP => q0'; rewrite q0' ltxx in q0.
+Admitted.
+
+End Lspace_inclusion.
diff --git a/theories/measure.v b/theories/measure.v
index 013b1a804..11178680d 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -4044,7 +4044,8 @@ Qed.
 Section ae.
 
 Definition almost_everywhere d (T : semiRingOfSetsType d) (R : realFieldType)
-  (mu : set T -> \bar R) (P : T -> Prop) := mu.-negligible (~` [set x | P x]).
+    (mu : set T -> \bar R) : set_system T :=
+  fun P => mu.-negligible (~` [set x | P x]).
 
 Let almost_everywhereT d (T : semiRingOfSetsType d) (R : realFieldType)
     (mu : {content set T -> \bar R}) : almost_everywhere mu setT.
@@ -4063,16 +4064,14 @@ Proof.
 by rewrite /almost_everywhere => mA mB; rewrite setCI; exact: negligibleU.
 Qed.
 
-#[global]
-Instance ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType)
+Definition ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType)
   (mu : {measure set T -> \bar R}) : Filter (almost_everywhere mu).
 Proof.
 by split; [exact: almost_everywhereT|exact: almost_everywhereI|
   exact: almost_everywhereS].
 Qed.
 
-#[global]
-Instance ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d}
+Definition ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d}
     (R : realFieldType) (mu : {measure set T -> \bar R}) :
   mu [set: T] > 0 -> ProperFilter (almost_everywhere mu).
 Proof.
@@ -4085,83 +4084,135 @@ End ae.
 
 #[global] Hint Extern 0 (Filter (almost_everywhere _)) =>
   (apply: ae_filter_ringOfSetsType) : typeclass_instances.
+#[global] Hint Extern 0 (Filter (nbhs (almost_everywhere _))) =>
+  (apply: ae_filter_ringOfSetsType) : typeclass_instances.
 
 #[global] Hint Extern 0 (ProperFilter (almost_everywhere _)) =>
   (apply: ae_properfilter_algebraOfSetsType) : typeclass_instances.
+#[global] Hint Extern 0 (ProperFilter (nbhs (almost_everywhere _))) =>
+  (apply: ae_properfilter_algebraOfSetsType) : typeclass_instances.
 
-Definition almost_everywhere_notation d (T : semiRingOfSetsType d)
-    (R : realFieldType) (mu : set T -> \bar R) (P : T -> Prop)
-  & (phantom Prop (forall x, P x)) := almost_everywhere mu P.
-Notation "{ 'ae' m , P }" :=
-  (almost_everywhere_notation m (inPhantom P)) : type_scope.
-
-Lemma aeW {d} {T : semiRingOfSetsType d} {R : realFieldType}
+Notation "{ 'ae' m , P }" := {near almost_everywhere m, P} : type_scope.
+Notation "\forall x \ae mu , P" := (\forall x \near almost_everywhere mu, P)
+  (format "\forall  x  \ae  mu ,  P",
+  x name, P at level 200, at level 200): type_scope.
+Definition ae_eq d (T : semiRingOfSetsType d) (R : realType) (mu : {measure set T -> \bar R})
+  (V : T -> Type) D (f g : forall x, V x) := (\forall x \ae mu, D x -> f x = g x).
+Notation "f = g %[ae mu 'in' D ]" := (\forall x \ae mu, D x -> f x = g x)
+  (format "f  =  g  '%[ae'  mu  'in'  D ]", g at next level, D at level 200, at level 70).
+Notation "f = g %[ae mu ]" := (f = g %[ae mu in setT ])
+  (format "f  =  g  '%[ae'  mu ]", g at next level, at level 70).
+
+Lemma aeW {d} {T : ringOfSetsType d} {R : realFieldType}
     (mu : {measure set _ -> \bar R}) (P : T -> Prop) :
-  (forall x, P x) -> {ae mu, forall x, P x}.
+  (forall x, P x) -> \forall x \ae mu, P x.
 Proof.
 move=> aP; have -> : P = setT by rewrite predeqE => t; split.
 by apply/negligibleP; [rewrite setCT|rewrite setCT measure0].
 Qed.
 
+Require Import -(notations) Setoid.
+
+Declare Scope signature_scope.
+Delimit Scope signature_scope with signature.
+Import -(notations) Morphisms.
+Module ProperNotations.
+
+  Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
+
+  Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
+
+  Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
+
+End ProperNotations.
+Import ProperNotations.
+
+Arguments Proper {A}%_type R%_signature m.
+Arguments respectful {A B}%_type (R R')%_signature _ _.
+
+Instance ae_eq_equiv d (T : ringOfSetsType d) R mu V D: Equivalence (@ae_eq d T R mu V D).
+Proof.
+split.
+- by move=> f; near=> x.
+- by move=> f g eqfg; near=> x => Dx; rewrite (near eqfg).
+- by move=> f g h eqfg eqgh; near=> x => Dx; rewrite (near eqfg) ?(near eqgh).
+Unshelve. all: by end_near. Qed.
+
+
+
 Section ae_eq.
-Local Open Scope ereal_scope.
+Local Open Scope ring_scope.
 Context d (T : sigmaRingType d) (R : realType).
+Implicit Types (U V : Type) (W : nzRingType).
 Variables (mu : {measure set T -> \bar R}) (D : set T).
-Implicit Types f g h i : T -> \bar R.
-
-Definition ae_eq f g := {ae mu, forall x, D x -> f x = g x}.
+Local Notation ae_eq := (ae_eq mu D).
 
-Lemma ae_eq0 f g : measurable D -> mu D = 0 -> ae_eq f g.
+Lemma ae_eq0 U (f g : T -> U) : measurable D -> mu D = 0 -> f = g %[ae mu in D].
 Proof. by move=> mD D0; exists D; split => // t/= /not_implyP[]. Qed.
 
-Lemma ae_eq_comp (j : \bar R -> \bar R) f g :
+Instance comp_ae_eq U V (j : T -> U -> V) : Proper (ae_eq ==> ae_eq) (fun f x => j x (f x)).
+Proof. by move=> f g; apply: filterS => x /[apply] /= ->. Qed.
+
+Instance comp_ae_eq2 U U' V (j : T -> U -> U' -> V) : Proper (ae_eq ==> ae_eq ==> ae_eq) (fun f g x => j x (f x) (g x)).
+Proof. by move=> f f' + g g'; apply: filterS2 => x + + Dx => -> // ->. Qed.
+
+Instance comp_ae_eq2' U U' V (j : U -> U' -> V) : Proper (ae_eq ==> ae_eq ==> ae_eq) (fun f g x => j (f x) (g x)).
+Proof. by move=> f f' + g g'; apply: filterS2 => x + + Dx => -> // ->. Qed.
+
+Instance sub_ae_eq2 : Proper (ae_eq ==> ae_eq ==> ae_eq) (@GRing.sub_fun T R).
+Proof. exact: (@comp_ae_eq2' _ _  R (fun x y => x - y)). Qed.
+
+Lemma ae_eq_refl U (f : T -> U) : ae_eq f f. Proof. exact/aeW. Qed.
+Hint Resolve ae_eq_refl : core.
+
+Lemma ae_eq_comp U V (j : U -> V) f g :
   ae_eq f g -> ae_eq (j \o f) (j \o g).
-Proof. by apply: filterS => x /[apply] /= ->. Qed.
+Proof. by move->. Qed.
 
-Lemma ae_eq_funeposneg f g : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-.
-Proof.
-split=> [fg|[]].
-  split; apply: filterS fg => x /[apply].
-    by rewrite !funeposE => ->.
-  by rewrite !funenegE => ->.
-apply: filterS2 => x + + Dx => /(_ Dx) fg /(_ Dx) gf.
-by rewrite (funeposneg f) (funeposneg g) fg gf.
-Qed.
+Lemma ae_eq_comp2 U V (j : T -> U -> V) f g :
+  ae_eq f g -> ae_eq (fun x => j x (f x)) (fun x => j x (g x)).
+Proof. by apply: filterS => x /[swap] + ->. Qed.
 
-Lemma ae_eq_refl f : ae_eq f f. Proof. exact/aeW. Qed.
+Lemma ae_eq_funeposneg (f g : T -> \bar R) :
+  ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-.
+Proof.
+split=> [fg|[pfg nfg]].
+  by split; near=> x => Dx; rewrite !(funeposE,funenegE) (near fg).
+by near=> x => Dx; rewrite (funeposneg f) (funeposneg g) ?(near pfg, near nfg).
+Unshelve. all: by end_near. Qed.
 
-Lemma ae_eq_sym f g : ae_eq f g -> ae_eq g f.
-Proof. by apply: filterS => x + Dx => /(_ Dx). Qed.
+Lemma ae_eq_sym U (f g : T -> U) : ae_eq f g -> ae_eq g f.
+Proof. by symmetry. Qed.
 
-Lemma ae_eq_trans f g h : ae_eq f g -> ae_eq g h -> ae_eq f h.
-Proof. by apply: filterS2 => x + + Dx => /(_ Dx) ->; exact. Qed.
+Lemma ae_eq_trans U (f g h : T -> U) : ae_eq f g -> ae_eq g h -> ae_eq f h.
+Proof. by apply transitivity. Qed.
 
-Lemma ae_eq_sub f g h i : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i).
-Proof. by apply: filterS2 => x + + Dx => /(_ Dx) -> /(_ Dx) ->. Qed.
+Lemma ae_eq_sub W (f g h i : T -> W) : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i).
+Proof. by apply: filterS2 => x + + Dx => /= /(_ Dx) -> /(_ Dx) ->. Qed.
 
-Lemma ae_eq_mul2r f g h : ae_eq f g -> ae_eq (f \* h) (g \* h).
-Proof. by apply: filterS => x /[apply] ->. Qed.
+Lemma ae_eq_mul2r W (f g h : T -> W) : ae_eq f g -> ae_eq (f \* h) (g \* h).
+Proof. by move=>/(ae_eq_comp2 (fun x y => y * h x)). Qed.
 
-Lemma ae_eq_mul2l f g h : ae_eq f g -> ae_eq (h \* f) (h \* g).
-Proof. by apply: filterS => x /[apply] ->. Qed.
+Lemma ae_eq_mul2l W (f g h : T -> W) : ae_eq f g -> ae_eq (h \* f) (h \* g).
+Proof. by move=>/(ae_eq_comp2 (fun x y => h x * y)). Qed.
 
-Lemma ae_eq_mul1l f g : ae_eq f (cst 1) -> ae_eq g (g \* f).
-Proof. by apply: filterS => x /[apply] ->; rewrite mule1. Qed.
+Lemma ae_eq_mul1l W (f g : T -> W) : ae_eq f (cst 1) -> ae_eq g (g \* f).
+Proof. by apply: filterS => x /= /[apply] ->; rewrite mulr1. Qed.
 
-Lemma ae_eq_abse f g : ae_eq f g -> ae_eq (abse \o f) (abse \o g).
+Lemma ae_eq_abse (f g : T -> \bar R) : ae_eq f g -> ae_eq (abse \o f) (abse \o g).
 Proof. by apply: filterS => x /[apply] /= ->. Qed.
 
 End ae_eq.
 
 Section ae_eq_lemmas.
-Context d (T : sigmaRingType d) (R : realType).
-Implicit Types mu : {measure set T -> \bar R}.
+Context d (T : sigmaRingType d) (R : realType) (U : Type).
+Implicit Types (mu : {measure set T -> \bar R}) (A : set T) (f g : T -> U).
 
 Lemma ae_eq_subset mu A B f g : B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g.
-Proof.
-move=> BA [N [mN N0 fg]]; exists N; split => //.
-by apply: subset_trans fg; apply: subsetC => z /= /[swap] /BA ? ->.
-Qed.
+Proof. by move=> BA; apply: filterS => x + /BA; apply. Qed.
 
 End ae_eq_lemmas.
 
@@ -5290,8 +5341,8 @@ End absolute_continuity.
 Notation "m1 `<< m2" := (measure_dominates m1 m2).
 
 Section absolute_continuity_lemmas.
-Context d (T : measurableType d) (R : realType).
-Implicit Types m : {measure set T -> \bar R}.
+Context d (T : measurableType d) (R : realType) (U : Type).
+Implicit Types (m : {measure set T -> \bar R}) (f g : T -> U).
 
 Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E ->
   m2 `<< m1 -> ae_eq m1 E f g -> ae_eq m2 E f g.
@@ -5315,4 +5366,49 @@ apply/negP => r0; apply/negP : rf; rewrite gt_eqF// (_ : _ @^-1` _ = setT)//.
 by apply/seteqP; split => // x _ /=; rewrite in_itv/= (lt_le_trans _ (f0 x)).
 Qed.
 
+Lemma ess_sup_cst r : (0 < mu setT)%E -> (ess_sup (cst r) = r%:E)%E.
+Proof.
+rewrite /ess_sup => mu0.
+under eq_set do rewrite preimage_cst/=.
+rewrite ereal_inf_EFin.
+- congr (_%:E).
+  rewrite [X in inf X](_ : _ = `[r, +oo[%classic); last first.
+    apply/seteqP; split => /=x/=.
+      case: ifPn => [_|]; first by move: mu0=> /[swap] ->; rewrite ltNge lexx.
+      by rewrite set_itvE notin_setE/= ltNge in_itv andbT/= => /negP /negPn.
+    rewrite in_itv/= => /andP[x0 _].
+    by rewrite ifF// set_itvE; apply/negP; rewrite in_setE/= ltNge => /negP.
+  by rewrite inf_itv.
+- exists r => x/=; case: ifPn => [_|].
+    by move: mu0 => /[swap] ->; rewrite ltNge lexx.
+  by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE.
+by exists r => /=; rewrite ifF//; rewrite set_itvE;
+  rewrite memNset //=; apply/negP; rewrite -real_leNgt ?num_real.
+Qed.
+
+Lemma ess_sup_ger f (r : R) : (forall x, f x <= r)%R -> (ess_sup f <= r%:E).
+Proof.
+move=> fr.
+rewrite /ess_sup.
+apply: ereal_inf_le.
+apply/exists2P.
+exists r%:E => /=; split => //.
+apply/exists2P.
+exists r; split => //.
+rewrite preimage_itvoy.
+suffices -> : [set x | r < f x]%R = set0 by [].
+apply/seteqP; split => x //=.
+rewrite lt_neqAle => /andP[rneqfx rlefx].
+move: (fr x) => fxler.
+have: (f x <= r <= f x)%R by rewrite rlefx fxler.
+by move/le_anti; move: rneqfx => /[swap] -> /eqP.
+Qed.
+
+Lemma ess_sup_eq0 f : ess_sup (normr \o f) = 0 -> f = 0%R %[ae mu].
+Admitted.
+
+Lemma ess_supM (f : T -> R) (a : R) : (0 <= a)%R -> (\forall x \ae mu, 0 <= f x)%R ->
+  (ess_sup (cst a \* f)%R = a%:E * ess_sup f)%E.
+Admitted.
+
 End essential_supremum.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 5008548ff..a7ab17e11 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -252,17 +252,27 @@ by rewrite opprK.
 Qed.
 
 HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T
-    of Num.NormedZmodule R T & PseudoPointedMetric R T := {
+    of Num.SemiNormedZmodule R T & PseudoPointedMetric R T := {
   pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |)
 }.
 
+(* HB.factory Record NormedZmod_PseudoMetric_eq (R : numDomainType) T *)
+(*     of Num.SemiNormedZmodule R T & PseudoPointedMetric R T := { *)
+(*   pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |) *)
+(* }. *)
+
+#[short(type="pseudoMetricSemiNormedZmodType")]
+HB.structure Definition PseudoMetricSemiNormedZmod (R : numDomainType) :=
+  {T of Num.SemiNormedZmodule R T & PseudoMetric R T
+   & NormedZmod_PseudoMetric_eq R T & isPointed T}.
+
 #[short(type="pseudoMetricNormedZmodType")]
 HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) :=
   {T of Num.NormedZmodule R T & PseudoMetric R T
    & NormedZmod_PseudoMetric_eq R T & isPointed T}.
 
 Section pseudoMetricnormedzmodule_lemmas.
-Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}.
+Context {K : numDomainType} {V : pseudoMetricSemiNormedZmodType K}.
 
 Local Notation ball_norm := (ball_ (@normr K V)).
 
@@ -807,21 +817,27 @@ Proof. by rewrite cvgeryP cvgrnyP. Qed.
 (** Modules with a norm depending on a numDomain*)
 
 HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V
-    of PseudoMetricNormedZmod K V & Tvs K V := {
+    of PseudoMetricSemiNormedZmod K V & Tvs K V := {
   normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
+#[short(type="semiNormedModType")]
+HB.structure Definition SemiNormedModule (K : numDomainType) :=
+  {T of PseudoMetricSemiNormedZmod K T & Tvs K T
+   & PseudoMetricNormedZmod_Tvs_isNormedModule K T}.
+
+
 #[short(type="normedModType")]
 HB.structure Definition NormedModule (K : numDomainType) :=
   {T of PseudoMetricNormedZmod K T & Tvs K T
    & PseudoMetricNormedZmod_Tvs_isNormedModule K T}.
 
-HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V
-    of PseudoMetricNormedZmod K V & GRing.Lmodule K V := {
+HB.factory Record PseudoMetricSemiNormedZmod_Lmodule_isSemiNormedModule (K : numFieldType) V
+    of PseudoMetricSemiNormedZmod K V & GRing.Lmodule K V := {
  normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
-HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V.
+HB.builders Context K V of PseudoMetricSemiNormedZmod_Lmodule_isSemiNormedModule K V.
 
 (* NB: These lemmas are done later with more machinery. They should
    be simplified once normedtype is split, and the present section can
@@ -859,7 +875,9 @@ rewrite [leRHS](_ : _ = M^-1 * (M *  M)); last first.
   by rewrite mulrA mulVf ?mul1r// gt_eqF.
 rewrite [leLHS](_ : _ = M^-1 * (M * (`|x| + `|x|) + `|e| / 2)); last first.
   by rewrite mulrDr mulrA mulVf ?mul1r ?gt_eqF// mulrC addrA.
-by rewrite ler_wpM2l ?invr_ge0// ?ltW// -ltrBrDl -mulrBr ltr_pM// ltrBrDl.
+rewrite ler_wpM2l ?invr_ge0// ?ltW// -ltrBrDl -mulrBr ltr_pM// ltrBrDl.
+near: M; apply: nbhs_pinfty_gt.
+rewrite !realD// normr_real//.
 Unshelve. all: by end_near. Qed.
 
 Lemma locally_convex :
@@ -2444,7 +2462,7 @@ by rewrite !num_max bE dE maxr_pMr.
 Qed.
 
 HB.instance Definition _ :=
-  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m.+1, n.+1)
+  PseudoMetricSemiNormedZmod_Lmodule_isSemiNormedModule.Build K 'M[K]_(m.+1, n.+1)
     mx_normZ.
 
 End matrix_NormedModule.