From d28f783091d324386ec3e06928ce5c727664c0b4 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Wed, 16 Aug 2023 14:21:16 +0200 Subject: [PATCH] - lnorms - hoelder for sums and specialization - convexity of powR --- theories/hoelder.v | 217 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 217 insertions(+) diff --git a/theories/hoelder.v b/theories/hoelder.v index 035917eb50..21eb1d5e1c 100644 --- a/theories/hoelder.v +++ b/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 \bar R) : (forall k, 0 <= a k) -> + \int[counting]_t (a t) = \sum_(k 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. \ No newline at end of file