- lnorms

- hoelder for sums and specialization
- convexity of powR

theories/hoelder.v

@@ -194,3 +194,220 @@ by rewrite 2!mule1 -EFinD pq.
 Qed.
 
 End hoelder.
+
+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).
+
+Lemma ge0_integral_count (a : nat -> \bar R) : (forall k, 0 <= a k) ->
+  \int[counting]_t (a t) = \sum_(k <oo) (a k).
+Proof.
+move=> sa.
+transitivity (\int[mseries (fun n => [the measure _ _ of \d_ n]) O]_t a t).
+  congr (integral _ _ _); apply/funext => A.
+  by rewrite /= counting_dirac.
+rewrite (@ge0_integral_measure_series _ _ R (fun n => [the measure _ _ of \d_ n]) setT)//=.
+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.
+Proof.
+rewrite /lnorm -ge0_integral_count// => k.
+by rewrite lee_fin powR_ge0.
+Qed.
+
+Lemma poweRyr_inv (p : R) (x : \bar R) : x `^ p = +oo -> x = +oo.
+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.
+
+Lemma hoelder_sum2 (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.
+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//.
+rewrite big_ord_recr /= big_ord_recr /= big_ord0 add0e powRr1 ?normr_ge0// powRr1 ?normr_ge0//.
+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 /= normr0 powR0//; case: eqP=>// p0'; move: p0; rewrite p0' ltxx//.
+rewrite big_ord_recr /= big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin.
+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 /= normr0 powR0//; case: eqP=>// q0'; move: q0; rewrite q0' ltxx//.
+rewrite big_ord_recr /= big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin.
+rewrite -EFinM invr1 powRr1; last by rewrite addr_ge0.
+rewrite lee_fin.
+rewrite ger0_norm; last by rewrite mulr_ge0.
+rewrite ger0_norm; last by rewrite mulr_ge0.
+rewrite ger0_norm; last by [].
+rewrite ger0_norm; last by [].
+rewrite ger0_norm; last by [].
+rewrite ger0_norm; last by [].
+by [].
+Qed.
+
+End hoelder_sums.
+
+Section convex_powR.
+Context d (T : measurableType d) (R : realType).
+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).
+
+Lemma ln_le0 (x : R) : (x <= 1 -> ln x <= 0)%R.
+Proof.
+have [x0|x0 x1] := leP x 0%R.
+  by rewrite ln0.
+by rewrite -ler_expR expR0 lnK.
+Qed.
+
+Lemma ger_powR (a : R) : (0 < a <= 1 -> {homo powR a : x y /~ y <= x})%R.
+Proof.
+move=> /andP [a0 a1] x y xy.
+rewrite /powR gt_eqF// ler_expR ler_wnmul2r// ln_le0//.
+Qed.
+
+Lemma powR_scale (x y : R) r : (0 < x <= 1 -> 0 <= y -> 1 <= r -> (x * y) `^ r <= x * (y `^ r))%R.
+Proof.
+move=> /andP [x0 x1] y0 r1.
+have x0' : (0 <= x)%R by rewrite le_eqVlt; apply/orP; right.
+rewrite powRM//.
+rewrite ler_wpmul2r// ?powR_ge0//.
+rewrite -[in leRHS](@powRr1 _ x)//.
+rewrite ger_powR//.
+apply/andP; split=>//.
+Qed.
+
+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.
+Proof.
+move=> p1 x_ge0 y_ge0.
+pose w1 := `1-(t%:inum).
+pose w2 := t%:inum.
+suff: ((w1 *: x + w2 *: y) `^ p<=
+       (w1 *: (x `^ p : R^o) + w2 *: (y `^ p : R^o)))%R by [].
+have [->|w10] := eqVneq w1 0%R.
+  rewrite scale0r add0r scale0r add0r.
+  have [->|w20] := eqVneq w2 0%R.
+    by rewrite !scale0r powR0// gt_eqF ?(lt_le_trans _ p1).
+  by rewrite powR_scale// /w2 lt_neqAle eq_sym w20 andTb; apply/andP.
+have [->|w20] := eqVneq w2 0%R.
+  rewrite scale0r addr0 scale0r addr0.
+  by rewrite powR_scale// ?onem_le1// andbT lt_neqAle eq_sym onem_ge0// andbT.
+have [->|pn1] := eqVneq p 1%R.
+  rewrite !powRr1// addr_ge0// mulr_ge0 /w1 /w2//onem_ge0//.
+pose q := p / (p - 1).
+have q1 : (1 <= q)%R.
+  rewrite /q ler_pdivl_mulr ?mul1r ?ler_subl_addr ?ler_addl// subr_gt0 lt_neqAle p1 eq_sym pn1//.
+rewrite -(@powRr1 _ (w1 *: (x `^ p : R^o) + w2 *: (y `^ p : R^o)))%R; last first.
+  rewrite addr_ge0// mulr_ge0// ?powR_ge0// /w2 ?onem_ge0// ?itv_ge0.
+have -> : (1 = p^-1 * p)%R.
+  by rewrite mulVf//; apply: lt0r_neq0; rewrite (lt_le_trans _ p1).
+rewrite powRrM gt0_ler_powR//.
+- by rewrite (@le_trans _ _ 1)%R.
+- by rewrite in_itv/= andbT addr_ge0// mulr_ge0/w2/w1 ?onem_ge0.
+- by rewrite in_itv/= andbT powR_ge0.
+have -> : (w1 *: (x : R^o) + w2 *: (y : R^o) = w1 `^ (p^-1) * w1 `^ (q^-1) *: (x : R^o) + w2 `^ (p^-1) * w2 `^ (q^-1) *: (y : R^o))%R.
+  rewrite -!powRD; last 2 first.
+  - by apply /implyP=>_.
+  - by apply /implyP=>_.
+  have -> : (p^-1 + q^-1 = 1)%R.
+    rewrite /q invf_div -{1}(mul1r (p^-1)) -mulrDl (addrC p) addrA subrr add0r mulfV//.
+    by apply lt0r_neq0; rewrite (lt_le_trans _ p1).
+  rewrite !powRr1 /w2/w1// onem_ge0//.
+apply: (le_trans (y:=(w1 *: (x `^ p : R^o) + w2 *: (y `^ p : R^o)) `^ (p^-1) * (w1+w2) `^ (q^-1)))%R.
+  pose a1 := (w1 `^ (p^-1) * x)%R.
+  pose a2 := (w2 `^ (p^-1) * y)%R.
+  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 => //.
+    - by rewrite /a1 mulr_ge0// powR_ge0.
+    - by rewrite /a2 mulr_ge0// powR_ge0.
+    - by rewrite /b1 powR_ge0.
+    - by rewrite /b2 powR_ge0.
+    - by rewrite (@lt_le_trans _ _ (1)%R).
+    - by rewrite (@lt_le_trans _ _ (1)%R).
+    - rewrite /q invf_div -{1}div1r -mulrDl addrC -addrA (addrC _ 1%R) subrr addr0 divff// neq_lt.
+      by rewrite (@lt_le_trans _ _ 1%R _ p)// orbT.
+  rewrite /a1/a2/b1/b2.
+  rewrite powRM ?powR_ge0// -powRrM mulVf; last first.
+    by rewrite neq_lt (@lt_le_trans _ _ 1 0 p)%R ?orbT.
+  rewrite powRr1 ?onem_ge0//.
+  rewrite powRM ?powR_ge0// -powRrM mulVf; last first.
+    by rewrite neq_lt (@lt_le_trans _ _ 1 0 p)%R ?orbT.
+  rewrite powRr1; last by rewrite /w2.
+  rewrite -(@powRrM _ _ _ q) mulVf ?powRr1 ?onem_ge0//; last first.
+    rewrite neq_lt (@lt_le_trans _ _ 1 0 q)%R// ?orbT//.
+  rewrite -(@powRrM _ _ _ q) mulVf ?powRr1 ?onem_ge0 /w2//; last first.
+    rewrite neq_lt (@lt_le_trans _ _ 1 0 q)%R// ?orbT//.
+  rewrite mulrAC.
+  rewrite (mulrAC _ y).
+  move=> /le_trans.
+  apply.
+  by [].
+rewrite le_eqVlt; apply/orP; left; apply/eqP.
+rewrite {2}/w1 {2}/w2 -addrA (addrC (- _)%R) subrr addr0 powR1 mulr1//.
+Qed.
+
+End convex_powR.