fixing hoelder.v after rebase

Author: hoheinzollern

theories/hoelder.v

@@ -43,7 +43,7 @@ HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType}
               mu (f @^-1` (setT `\ 0%R))
             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
+  | +oo%E => (if mu [set: T] > 0 then ess_supr mu (normr \o f) else 0)%E
   | -oo%E => 0%E
   end.
 Canonical locked_Lnorm := Unlockable Lnorm.unlock.
@@ -68,7 +68,7 @@ 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/=.
+by case: ifPn => // /ess_sup_ger; apply => t/=.
 Qed.
 
 Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g].

theories/measure.v

@@ -5413,21 +5413,3 @@ Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E ->
 Proof. by move=> mE m21 [A [mA A0 ?]]; exists A; split => //; exact: m21. Qed.
 
 End absolute_continuity_lemmas.
-
-Section essential_supremum.
-Context d {T : semiRingOfSetsType d} {R : realType}.
-Variable mu : {measure set T -> \bar R}.
-Implicit Types f : T -> R.
-
-Definition ess_sup f :=
-  ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]).
-
-Lemma ess_sup_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R ->
-  0 <= ess_sup f.
-Proof.
-move=> muT f0; apply: lb_ereal_inf => _ /= [r /eqP rf <-]; rewrite leNgt.
-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.
-
-End essential_supremum.