Reverted notation to 'N_p[f]

theories/hoelder.v

@@ -4,7 +4,7 @@ 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 .
 Require Import signed reals ereal topology normedtype sequences real_interval.
-Require Import esum measure lebesgue_measure lebesgue_integral numfun exp.
+Require Import esum measure lebesgue_measure lebesgue_integral numfun exp convex itv.
 
 (******************************************************************************)
 (*                         Hoelder's Inequality                               *)
@@ -220,10 +220,7 @@ Section lnorm.
 Context (R : realType).
 Local Open Scope ereal_scope.
 
-Definition lnorm (p : R) (f : R^nat) : \bar R :=
-  (\sum_(x <oo) (`|f x| `^ p)%:E) `^ p^-1.
-
-Local Notation "`| f |~ p" := (lnorm p f).
+Local Notation "'N_ p [ f ]" := 'N[counting]_p[f].
 
 Lemma ge0_integral_count (a : nat -> \bar R) : (forall k, 0 <= a k) ->
   \int[counting]_t (a t) = \sum_(k <oo) (a k).
@@ -236,9 +233,9 @@ rewrite (@ge0_integral_measure_series _ _ R (fun n => [the measure _ _ of \d_ n]
 by apply: eq_eseriesr=> i _; rewrite integral_dirac//= indicE mem_set// mul1e.
 Qed.
 
-Lemma Lnorm_lnorm_eq p (f : R^nat) : 'N[counting]_p [f] = `| f |~p.
+Lemma lnormE p (f : R^nat) : 'N_p [f] = (\sum_(k <oo) (`| f k | `^ p)%:E) `^ p^-1.
 Proof.
-rewrite /lnorm -ge0_integral_count// => k.
+rewrite /Lnorm ge0_integral_count// => k.
 by rewrite lee_fin powR_ge0.
 Qed.
 
@@ -247,60 +244,23 @@ Proof.
 rewrite /poweR. case:x => //. case: ifPn => //.
 Qed.
 
-Lemma not_summable_lnorm_ifty p (f : R^nat) : (0 < p)%R ->
-  ~summable [set: nat] (fun t : nat => (`|f t| `^ p)%:E) -> `| f |~p = +oo%E.
-Proof.
-rewrite /summable /lnorm=>p0.
-rewrite ltNge leye_eq => /negP /negPn /eqP.
-rewrite nneseries_esum; last first.
-  move=> n _; rewrite lee_fin powR_ge0//.
-rewrite -fun_true.
-under eq_esum => i _ do rewrite gee0_abs ?lee_fin ?powR_ge0//.
-by move=> ->; rewrite poweRyr// gt_eqF// invr_gt0.
-Qed.
-
-Lemma lnorm_ifty_not_summable p (f : R^nat) : (0 < p)%R ->
-  lnorm p f = +oo%E -> ~summable [set: nat] (fun t : nat => (`|f t| `^ p)%:E).
-Proof.
-rewrite /summable /lnorm=>p0 /poweRyr_inv.
-under eq_esum => i _ do rewrite gee0_abs ?lee_fin ?powR_ge0//.
-rewrite nneseries_esum; last first.
-  move=> n _; rewrite lee_fin powR_ge0//.
-rewrite -fun_true => ->//.
-Qed.
-
-Lemma lnorm_ge0 (p : R) (f : R^nat) : (0 <= `| f |~p)%E.
-Proof.
-rewrite /lnorm poweR_ge0//.
-Qed.
-
 End lnorm.
 
-Declare Scope lnorm_scope.
-Notation "`| f |~ p" := (lnorm p f) : lnorm_scope.
-
 Section hoelder_sums.
 Context (R : realType).
 Local Open Scope ereal_scope.
-Local Open Scope lnorm_scope.
 
-Lemma hoelder_sums (f g : R^nat) (p q : R) :
-  measurable_fun setT f -> measurable_fun setT g ->
-  (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
-  `| (f \* g)%R |~(1) <= `| f |~p * `| g |~q.
-Proof.
-move=> mf mg p0 q0 pq; rewrite -!Lnorm_lnorm_eq hoelder//.
-Qed.
+Local Notation "'N_ p [ f ]" := 'N[counting]_p[f].
 
-Lemma hoelder_sum2 (a1 a2 b1 b2 : R) (p q : R) : (0 <= a1)%R -> (0 <= a2)%R -> (0 <= b1)%R -> (0 <= b2)%R ->
+Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) : (0 <= a1)%R -> (0 <= a2)%R -> (0 <= b1)%R -> (0 <= b2)%R ->
   (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
   (a1 * b1 + a2 * b2 <= (a1`^p + a2`^p) `^ (p^-1) * (b1`^q + b2`^q)`^(q^-1))%R.
 Proof.
 move=> a10 a20 b10 b20 p0 q0 pq.
 pose f := fun a b n => match n with 0%nat => a | 1%nat => b | _ => 0%R:R end.
 have mf a b : measurable_fun setT (f a b). done.
-have := @hoelder_sums (f a1 a2) (f b1 b2) p q (mf a1 a2) (mf b1 b2) p0 q0 pq.
-rewrite /lnorm.
+have := @hoelder _ _ _ counting (f a1 a2) (f b1 b2) p q (mf a1 a2) (mf b1 b2) p0 q0 pq.
+rewrite !lnormE.
 rewrite (nneseries_split 2); last by move=> k; rewrite lee_fin powR_ge0.
 rewrite ereal_series_cond eseries0 ?adde0; last first.
   case=>//; case=>// n n2; rewrite /f /= mulr0 normr0 powR0//.
@@ -332,7 +292,7 @@ Variable mu : {measure set T -> \bar R}.
 Local Open Scope ereal_scope.
 Local Open Scope convex_scope.
 
-Local Notation "`| f |~ p" := (Lnorm mu p f).
+Local Notation "'N_ p [ f ]" := 'N[counting]_p[f].
 
 Lemma ln_le0 (x : R) : (x <= 1 -> ln x <= 0)%R.
 Proof.
@@ -358,6 +318,8 @@ rewrite ger_powR//.
 apply/andP; split=>//.
 Qed.
 
+Local Open Scope convex_scope.
+
 Lemma convex_powR (t : {i01 R}) (x y : R^o) p : (1 <= p)%R ->
   (0 <= x)%R -> (0 <= y)%R ->
   ((x <| t |> y) `^ p <= (x `^ p : R^o) <| t |> y `^ p)%R.
@@ -402,7 +364,7 @@ apply: (le_trans (y:=(w1 *: (x `^ p : R^o) + w2 *: (y `^ p : R^o)) `^ (p^-1) * (
   pose b1 := (w1 `^ (q^-1))%R.
   pose b2 := (w2 `^ (q^-1))%R.
   have : (a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p)`^(p^-1) * (b1 `^ q + b2 `^ q)`^(q^-1))%R.
-    apply hoelder_sum2 => //.
+    apply hoelder2 => //.
     - by rewrite /a1 mulr_ge0// powR_ge0.
     - by rewrite /a2 mulr_ge0// powR_ge0.
     - by rewrite /b1 powR_ge0.