From 76e0493904547f1ec3221696d1490d84633833b9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 3 Jun 2023 23:58:04 +0900 Subject: [PATCH 1/7] Convexity of power function - definition of convex_function - lnorm and equivalence lemma - hoelder for sums - convexity of powR Co-authored-by: Alessandro Bruni --- CHANGELOG_UNRELEASED.md | 12 ++++ theories/convex.v | 4 ++ theories/exp.v | 58 ++++++++++++++++ theories/hoelder.v | 126 ++++++++++++++++++++++++++++++++++- theories/lebesgue_integral.v | 11 +++ 5 files changed, 210 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2f9f22edf..8b4ffa0a9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -69,6 +69,18 @@ - in `measure.v`: + definition `ess_sup`, lemma `ess_sup_ge0` +- in `convex.v`: + + definition `convex_function` + +- in `exp.v`: + + lemmas `ln_le0`, `ger_powR`, `ler1_powR`, `le1r_powR`, `ger1_powR`, + `ge1r_powR`, `ge1r_powRZ`, `le1r_powRZ` + +- in `hoelder.v`: + + lemmas `lnormE`, `hoelder2`, `convex_powR` + +- in `lebesgue_integral.v`: + + lemma `ge0_integral_count` - in `exp.v`: + lemma `gt0_ltr_powR` diff --git a/theories/convex.v b/theories/convex.v index 5eff17447..7b4047c6c 100644 --- a/theories/convex.v +++ b/theories/convex.v @@ -149,6 +149,10 @@ Proof. by []. Qed. End conv_realDomainType. +Definition convex_function (R : realType) (D : set R) (f : R -> R^o) := + forall (t : {i01 R}), {in D &, forall (x y : R^o), (f (x <| t |> y) <= f x <| t |> f y)%R}. +(* TODO: generalize to convTypes once we have ordered convTypes (mathcomp 2) *) + (* ref: http://www.math.wisc.edu/~nagel/convexity.pdf *) Section twice_derivable_convex. Context {R : realType}. diff --git a/theories/exp.v b/theories/exp.v index e5ac2a6c4..7f115e5ce 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -586,6 +586,12 @@ Proof. by move=> x_gt1; rewrite -ltr_expR expR0 lnK // qualifE (lt_trans _ x_gt1). Qed. +Lemma ln_le0 (x : R) : x <= 1 -> ln x <= 0. +Proof. +have [x0|x0 x1] := leP x 0; first by rewrite ln0. +by rewrite -ler_expR expR0 lnK. +Qed. + Lemma continuous_ln x : 0 < x -> {for x, continuous ln}. Proof. move=> x_gt0; rewrite -[x]lnK//. @@ -658,6 +664,12 @@ Qed. Lemma powR_eq0_eq0 x p : x `^ p = 0 -> x = 0. Proof. by move=> /eqP; rewrite powR_eq0 => /andP[/eqP]. Qed. +Lemma ger_powR a : 0 < a <= 1 -> {homo powR a : x y /~ y <= x}. +Proof. +move=> /andP [a0 a1] x y xy. +rewrite /powR gt_eqF// ler_expR ler_wnmul2r// ln_le0//. +Qed. + Lemma ler_powR a : 1 <= a -> {homo powR a : x y / x <= y}. Proof. move=> a1 x y xy. @@ -673,6 +685,34 @@ by move/expR_inj/mulfI => /(_ (negbT (gt_eqF r0))); apply: ln_inj; rewrite posrE lt_neqAle eq_sym (xneq0,yneq0). Qed. +Lemma ler1_powR a r : 1 <= a -> r <= 1 -> a >= a `^ r. +Proof. +move=> a1 r1. +rewrite -[in leRHS](@powRr1 a)//; last exact: (le_trans _ a1). +by rewrite ler_powR. +Qed. + +Lemma le1r_powR a r : 1 <= a -> 1 <= r -> a <= a `^ r. +Proof. +move=> a1 r1. +rewrite -[in leLHS](@powRr1 a)//; last exact: (le_trans _ a1). +by rewrite ler_powR. +Qed. + +Lemma ger1_powR a r : 0 < a <= 1 -> r <= 1 -> a <= a `^ r. +Proof. +move=> /andP [a0 a1] r1. +rewrite -[in leLHS](@powRr1 a)//; last by rewrite ltW. +by rewrite ger_powR// a0. +Qed. + +Lemma ge1r_powR a r : 0 < a <= 1 -> 1 <= r -> a >= a `^ r. +Proof. +move=> /andP [a0 a1] r1. +rewrite -[in leRHS](@powRr1 a)//; last by rewrite ltW. +by rewrite ger_powR// a0. +Qed. + Lemma ge0_ler_powR (r : R) : 0 <= r -> {in Num.nneg &, {homo powR ^~ r : x y / x <= y >-> x <= y}}. Proof. @@ -701,6 +741,24 @@ case: (ltgtP x 0) => // x0 _; case: (ltgtP y 0) => //= y0 _; do ? by rewrite lnM// mulrDr expRD. Qed. +Lemma ge1r_powRZ x y r : 0 < x <= 1 -> 0 <= y -> 1 <= r -> + (x * y) `^ r <= x * (y `^ r). +Proof. +move=> /andP [x0 x1] y0 r1. +rewrite powRM//; last exact: ltW. +rewrite ler_wpmul2r// ?powR_ge0//. +by rewrite ge1r_powR// x0. +Qed. + +Lemma le1r_powRZ x y r : x >= 1 -> 0 <= y -> 1 <= r -> + (x * y) `^ r >= x * (y `^ r). +Proof. +move=> x1 y0 r1. +rewrite powRM//; last by rewrite (le_trans _ x1). +rewrite ler_wpmul2r// ?powR_ge0//. +rewrite le1r_powR//. +Qed. + Lemma powRrM (x y z : R) : x `^ (y * z) = (x `^ y) `^ z. Proof. rewrite /powR mulf_eq0; have [_|xN0] := eqVneq x 0. diff --git a/theories/hoelder.v b/theories/hoelder.v index 2d262c10f..af8a19ee1 100644 --- a/theories/hoelder.v +++ b/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 *) @@ -89,6 +89,20 @@ Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core. Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f). +Section lnorm. +(* lnorm is just Lnorm applied to counting *) +Context d {T : measurableType d} {R : realType}. + +Local Notation "'N_ p [ f ]" := (Lnorm counting p f). + +Lemma lnormE p (f : R^nat) : (0 < p)%R -> 'N_p%:E [f] = (\sum_(k p0 /=; rewrite gt_eqF// ge0_integral_count// => k. +by rewrite lee_fin powR_ge0. +Qed. + +End lnorm. + Section hoelder. Context d {T : measurableType d} {R : realType}. Variable mu : {measure set T -> \bar R}. @@ -230,3 +244,113 @@ by rewrite 2!mule1 -EFinD pq. Qed. End hoelder. + +Section hoelder2. +Context (R : realType). +Local Open Scope ring_scope. + +Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) : 0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 -> + 0 < p -> 0 < q -> p^-1 + q^-1 = 1 -> + a1 * b1 + a2 * b2 <= (a1`^p + a2`^p) `^ (p^-1) * (b1`^q + b2`^q)`^(q^-1). +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 end. +have mf a b : measurable_fun setT (f a b). done. +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. + by move=> [//|] [//|n _]; rewrite /f /= mulr0 normr0 powR0. +rewrite 2!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 + by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF. +rewrite 2!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 + by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF. +rewrite 2!big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin. +rewrite -EFinM invr1 powRr1; last by rewrite addr_ge0. +rewrite lee_fin. +do 2 (rewrite ger0_norm; last by rewrite mulr_ge0). +by do 4 (rewrite ger0_norm; last by []). +Qed. + +End hoelder2. + +Section convex_powR. +Context (R : realType). +Local Open Scope ring_scope. + +Lemma lerBr (x y : R) : (0 <= y -> x - y <= x)%R. +Proof. +by move=> x0; rewrite ler_subl_addl ler_addr. +Qed. + +Lemma convex_powR p : 1 <= p -> + convex_function `[0, +oo[%classic (@powR R ^~ p). +Proof. +move=> p1 t x y. +rewrite !inE /= !in_itv /= !andbT=> x_ge0 y_ge0. +pose w1 := `1-(t%:inum). +pose w2 := t%:inum. +suff: (w1 *: (x : R^o) + w2 *: (y : R^o)) `^ p<= + (w1 *: (x `^ p : R^o) + w2 *: (y `^ p : R^o)) by []. +have [->|w10] := eqVneq w1 0. + rewrite scale0r add0r scale0r add0r. + have [->|w20] := eqVneq w2 0. + by rewrite !scale0r powR0// gt_eqF ?(lt_le_trans _ p1). + by rewrite ge1r_powRZ// /w2 lt_neqAle eq_sym w20 andTb; apply/andP. +have [->|w20] := eqVneq w2 0. + rewrite scale0r addr0 scale0r addr0. + by rewrite ge1r_powRZ// ?onem_le1// andbT lt_neqAle eq_sym onem_ge0// andbT. +have [->|pn1] := eqVneq p 1. + rewrite !powRr1// addr_ge0// mulr_ge0 /w1 /w2//onem_ge0//. +pose q := p / (p - 1). +have q1 : 1 <= q. + by rewrite /q ler_pdivl_mulr// ?mul1r ?lerBr// subr_gt0 lt_neqAle eq_sym pn1. +rewrite -(@powRr1 _ (w1 *: (x `^ p : R^o) + w2 *: (y `^ p : R^o))); last first. + by rewrite addr_ge0// mulr_ge0// ?powR_ge0// /w2 ?onem_ge0// ?itv_ge0. +have -> : 1 = p^-1 * p by rewrite mulVf// lt0r_neq0// (lt_le_trans _ p1). +rewrite powRrM gt0_ler_powR//. +- by rewrite (le_trans _ p1). +- by rewrite nnegrE addr_ge0// mulr_ge0/w2/w1 ?onem_ge0. +- by rewrite nnegrE 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; [|exact/implyP..]. + have -> : p^-1 + q^-1 = 1. + rewrite /q invf_div -{1}(mul1r (p^-1)) -mulrDl (addrC p) addrA subrr add0r mulfV//. + by rewrite lt0r_neq0// (lt_le_trans _ p1). + by rewrite /w2 !powRr1// onem_ge0. +apply: (@le_trans _ _ ((w1 *: (x `^ p : R^o) + w2 *: (y `^ p : R^o)) `^ (p^-1) * (w1+w2) `^ (q^-1)))%R. + pose a1 := w1 `^ (p^-1) * x. + pose a2 := w2 `^ (p^-1) * y. + pose b1 := w1 `^ (q^-1). + pose b2 := w2 `^ (q^-1). + have : a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p)`^(p^-1) * (b1 `^ q + b2 `^ q)`^(q^-1). + apply: hoelder2 => //. + - 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 _ p1). + - by rewrite (lt_le_trans _ q1). + - rewrite /q invf_div -{1}div1r -mulrDl addrC -addrA (addrC _ 1) subrr addr0 divff// gt_eqF//. + by rewrite (lt_le_trans _ p1)// orbT. + rewrite /a1/a2/b1/b2. + rewrite powRM ?powR_ge0// -powRrM mulVf; last by rewrite gt_eqF// (lt_le_trans _ p1). + rewrite powRr1 ?onem_ge0//. + rewrite powRM ?powR_ge0// -powRrM mulVf; last by rewrite gt_eqF// (lt_le_trans _ p1). + rewrite powRr1; last by rewrite /w2. + rewrite -(@powRrM _ _ _ q) mulVf ?powRr1 ?onem_ge0//; last first. + by rewrite gt_eqF// (lt_le_trans _ q1). + rewrite -(@powRrM _ _ _ q) mulVf ?powRr1 ?onem_ge0 /w2//; last first. + by rewrite gt_eqF// (lt_le_trans _ q1). + by rewrite mulrAC (mulrAC _ y) => /le_trans; exact. +rewrite le_eqVlt; apply/orP; left; apply/eqP. +by rewrite {2}/w1 {2}/w2 subrK powR1 mulr1. +Qed. + +End convex_powR. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index ff4ab41cf..20f853c4b 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3950,6 +3950,17 @@ rewrite (@integral_measure_series _ _ R (fun n => [the measure _ _ of \d_ n]) se - by apply: summable_integral_dirac => //; exact: summable_funepos. Qed. +Lemma ge0_integral_count (a : nat -> \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. + End integral_counting. Section subadditive_countable. From 7d6c6779080461c5ccdb547a1480d88c944fd8bb Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 21 Sep 2023 17:24:29 +0900 Subject: [PATCH 2/7] nitpicks --- CHANGELOG_UNRELEASED.md | 4 +- classical/mathcomp_extra.v | 4 ++ theories/exp.v | 32 +++------ theories/hoelder.v | 129 +++++++++++++++-------------------- theories/lebesgue_integral.v | 2 +- 5 files changed, 75 insertions(+), 96 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8b4ffa0a9..fc4ecff92 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -77,7 +77,7 @@ `ge1r_powR`, `ge1r_powRZ`, `le1r_powRZ` - in `hoelder.v`: - + lemmas `lnormE`, `hoelder2`, `convex_powR` + + lemmas `Lnorm_counting`, `hoelder2`, `convex_powR` - in `lebesgue_integral.v`: + lemma `ge0_integral_count` @@ -85,6 +85,8 @@ - in `exp.v`: + lemma `gt0_ltr_powR` + lemma `powR_injective` +- in `mathcomp_extra.v`: + + lemma `lerBr` ### Changed diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 607722b63..3a55a7813 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1438,3 +1438,7 @@ Proof. by move=> i0r Pi0 ?; apply: le_trans (le_bigmax_seq _ _ _). Qed. End bigmax_seq. Arguments le_bigmax_seq {d T} x {I r} i0 P. + +(* NB: PR 1079 to MathComp in progress *) +Lemma lerBr {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x. +Proof. by move=> y0; rewrite ler_subl_addl ler_addr. Qed. diff --git a/theories/exp.v b/theories/exp.v index 7f115e5ce..29d0656bf 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -666,8 +666,8 @@ Proof. by move=> /eqP; rewrite powR_eq0 => /andP[/eqP]. Qed. Lemma ger_powR a : 0 < a <= 1 -> {homo powR a : x y /~ y <= x}. Proof. -move=> /andP [a0 a1] x y xy. -rewrite /powR gt_eqF// ler_expR ler_wnmul2r// ln_le0//. +move=> /andP[a0 a1] x y xy. +by rewrite /powR gt_eqF// ler_expR ler_wnmul2r// ln_le0. Qed. Lemma ler_powR a : 1 <= a -> {homo powR a : x y / x <= y}. @@ -687,30 +687,24 @@ Qed. Lemma ler1_powR a r : 1 <= a -> r <= 1 -> a >= a `^ r. Proof. -move=> a1 r1. -rewrite -[in leRHS](@powRr1 a)//; last exact: (le_trans _ a1). -by rewrite ler_powR. +by move=> a1 r1; rewrite (le_trans (ler_powR _ r1)) ?powRr1// (le_trans _ a1). Qed. Lemma le1r_powR a r : 1 <= a -> 1 <= r -> a <= a `^ r. Proof. -move=> a1 r1. -rewrite -[in leLHS](@powRr1 a)//; last exact: (le_trans _ a1). -by rewrite ler_powR. +by move=> a1 r1; rewrite (le_trans _ (ler_powR _ r1)) ?powRr1// (le_trans _ a1). Qed. Lemma ger1_powR a r : 0 < a <= 1 -> r <= 1 -> a <= a `^ r. Proof. -move=> /andP [a0 a1] r1. -rewrite -[in leLHS](@powRr1 a)//; last by rewrite ltW. -by rewrite ger_powR// a0. +move=> /andP[a0 _a1] r1. +by rewrite (le_trans _ (ger_powR _ r1)) ?powRr1 ?a0// ltW. Qed. Lemma ge1r_powR a r : 0 < a <= 1 -> 1 <= r -> a >= a `^ r. Proof. -move=> /andP [a0 a1] r1. -rewrite -[in leRHS](@powRr1 a)//; last by rewrite ltW. -by rewrite ger_powR// a0. +move=> /andP[a0 a1] r1. +by rewrite (le_trans (ger_powR _ r1)) ?powRr1 ?a0// ltW. Qed. Lemma ge0_ler_powR (r : R) : 0 <= r -> @@ -744,19 +738,15 @@ Qed. Lemma ge1r_powRZ x y r : 0 < x <= 1 -> 0 <= y -> 1 <= r -> (x * y) `^ r <= x * (y `^ r). Proof. -move=> /andP [x0 x1] y0 r1. -rewrite powRM//; last exact: ltW. -rewrite ler_wpmul2r// ?powR_ge0//. -by rewrite ge1r_powR// x0. +move=> /andP[x0 x1] y0 r1. +by rewrite (powRM _ (ltW _))// ler_wpmul2r ?powR_ge0// ge1r_powR// x0. Qed. Lemma le1r_powRZ x y r : x >= 1 -> 0 <= y -> 1 <= r -> (x * y) `^ r >= x * (y `^ r). Proof. move=> x1 y0 r1. -rewrite powRM//; last by rewrite (le_trans _ x1). -rewrite ler_wpmul2r// ?powR_ge0//. -rewrite le1r_powR//. +by rewrite (powRM _ (le_trans _ x1))// ler_wpmul2r ?powR_ge0// le1r_powR// x0. Qed. Lemma powRrM (x y z : R) : x `^ (y * z) = (x `^ y) `^ z. diff --git a/theories/hoelder.v b/theories/hoelder.v index af8a19ee1..56964fc90 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -4,7 +4,8 @@ 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 convex itv. +Require Import esum measure lebesgue_measure lebesgue_integral numfun exp. +Require Import convex itv. (******************************************************************************) (* Hoelder's Inequality *) @@ -71,8 +72,8 @@ 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 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). Proof. move=> r0 mf/=; rewrite (gt_eqF r0) => /poweR_eq0_eq0 fp. apply/ae_eq_integral_abs => //=. @@ -95,7 +96,8 @@ Context d {T : measurableType d} {R : realType}. Local Notation "'N_ p [ f ]" := (Lnorm counting p f). -Lemma lnormE p (f : R^nat) : (0 < p)%R -> 'N_p%:E [f] = (\sum_(k + 'N_p%:E [f] = (\sum_(k p0 /=; rewrite gt_eqF// ge0_integral_count// => k. by rewrite lee_fin powR_ge0. @@ -246,32 +248,32 @@ Qed. End hoelder. Section hoelder2. -Context (R : realType). +Context {R : realType}. Local Open Scope ring_scope. -Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) : 0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 -> +Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) : + 0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 -> 0 < p -> 0 < q -> p^-1 + q^-1 = 1 -> a1 * b1 + a2 * b2 <= (a1`^p + a2`^p) `^ (p^-1) * (b1`^q + b2`^q)`^(q^-1). 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 end. -have mf a b : measurable_fun setT (f a b). done. -have := @hoelder _ _ _ counting (f a1 a2) (f b1 b2) p q (mf a1 a2) (mf b1 b2) p0 q0 pq. -rewrite !lnormE//. +pose f a b n : R := match n with 0%nat => a | 1%nat => b | _ => 0 end. +have mf a b : measurable_fun setT (f a b) by []. +have := hoelder counting (mf a1 a2) (mf b1 b2) p0 q0 pq. +rewrite !Lnorm_counting//. rewrite (nneseries_split 2); last by move=> k; rewrite lee_fin powR_ge0. rewrite ereal_series_cond eseries0 ?adde0; last first. by move=> [//|] [//|n _]; rewrite /f /= mulr0 normr0 powR0. -rewrite 2!big_ord_recr /= big_ord0 add0e powRr1 ?normr_ge0// powRr1 ?normr_ge0//. +rewrite 2!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 +rewrite ereal_series_cond eseries0 ?adde0; last first. by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF. rewrite 2!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 +rewrite ereal_series_cond eseries0 ?adde0; last first. by move=> [//|] [//|n _]; rewrite /f /= normr0 powR0// gt_eqF. rewrite 2!big_ord_recr /= big_ord0 add0e -EFinD poweR_EFin. rewrite -EFinM invr1 powRr1; last by rewrite addr_ge0. -rewrite lee_fin. do 2 (rewrite ger0_norm; last by rewrite mulr_ge0). by do 4 (rewrite ger0_norm; last by []). Qed. @@ -279,77 +281,58 @@ Qed. End hoelder2. Section convex_powR. -Context (R : realType). +Context {R : realType}. Local Open Scope ring_scope. -Lemma lerBr (x y : R) : (0 <= y -> x - y <= x)%R. -Proof. -by move=> x0; rewrite ler_subl_addl ler_addr. -Qed. - Lemma convex_powR p : 1 <= p -> convex_function `[0, +oo[%classic (@powR R ^~ p). Proof. -move=> p1 t x y. -rewrite !inE /= !in_itv /= !andbT=> x_ge0 y_ge0. -pose w1 := `1-(t%:inum). -pose w2 := t%:inum. -suff: (w1 *: (x : R^o) + w2 *: (y : R^o)) `^ p<= - (w1 *: (x `^ p : R^o) + w2 *: (y `^ p : R^o)) by []. +move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0. +have p0 : 0 < p by rewrite (lt_le_trans _ p1). +rewrite !convRE; set w1 := `1-(t%:inum); set w2 := t%:inum. have [->|w10] := eqVneq w1 0. - rewrite scale0r add0r scale0r add0r. - have [->|w20] := eqVneq w2 0. - by rewrite !scale0r powR0// gt_eqF ?(lt_le_trans _ p1). - by rewrite ge1r_powRZ// /w2 lt_neqAle eq_sym w20 andTb; apply/andP. + rewrite !mul0r !add0r; have [->|w20] := eqVneq w2 0. + by rewrite !mul0r powR0// gt_eqF. + by rewrite ge1r_powRZ// /w2 lt_neqAle eq_sym w20/=; apply/andP. have [->|w20] := eqVneq w2 0. - rewrite scale0r addr0 scale0r addr0. - by rewrite ge1r_powRZ// ?onem_le1// andbT lt_neqAle eq_sym onem_ge0// andbT. -have [->|pn1] := eqVneq p 1. - rewrite !powRr1// addr_ge0// mulr_ge0 /w1 /w2//onem_ge0//. + rewrite !mul0r !addr0 ge1r_powRZ// onem_le1// andbT. + by rewrite lt_neqAle eq_sym onem_ge0// andbT. +have [->|p_neq1] := eqVneq p 1. + by rewrite !powRr1// addr_ge0// mulr_ge0// /w2 ?onem_ge0. +have {p1 p_neq1}p1 : 1 < p by rewrite lt_neqAle eq_sym p_neq1. pose q := p / (p - 1). -have q1 : 1 <= q. - by rewrite /q ler_pdivl_mulr// ?mul1r ?lerBr// subr_gt0 lt_neqAle eq_sym pn1. -rewrite -(@powRr1 _ (w1 *: (x `^ p : R^o) + w2 *: (y `^ p : R^o))); last first. - by rewrite addr_ge0// mulr_ge0// ?powR_ge0// /w2 ?onem_ge0// ?itv_ge0. -have -> : 1 = p^-1 * p by rewrite mulVf// lt0r_neq0// (lt_le_trans _ p1). -rewrite powRrM gt0_ler_powR//. -- by rewrite (le_trans _ p1). -- by rewrite nnegrE addr_ge0// mulr_ge0/w2/w1 ?onem_ge0. +have q1 : 1 <= q by rewrite /q ler_pdivl_mulr// ?mul1r ?lerBr// subr_gt0. +have q0 : 0 < q by rewrite (lt_le_trans _ q1). +have pq1 : p^-1 + q^-1 = 1. + rewrite /q invf_div -{1}(div1r p) -mulrDl addrCA subrr addr0. + by rewrite mulfV// gt_eqF. +rewrite -(@powRr1 _ (w1 * x `^ p + w2 * y `^ p)); last first. + by rewrite addr_ge0// mulr_ge0// ?powR_ge0// /w2 ?onem_ge0// itv_ge0. +have -> : 1 = p^-1 * p by rewrite mulVf ?gt_eqF. +rewrite powRrM (gt0_ler_powR (le_trans _ (ltW p1)))//. +- by rewrite nnegrE addr_ge0// mulr_ge0 /w2 ?onem_ge0. - by rewrite nnegrE 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; [|exact/implyP..]. - have -> : p^-1 + q^-1 = 1. - rewrite /q invf_div -{1}(mul1r (p^-1)) -mulrDl (addrC p) addrA subrr add0r mulfV//. - by rewrite lt0r_neq0// (lt_le_trans _ p1). - by rewrite /w2 !powRr1// onem_ge0. -apply: (@le_trans _ _ ((w1 *: (x `^ p : R^o) + w2 *: (y `^ p : R^o)) `^ (p^-1) * (w1+w2) `^ (q^-1)))%R. - pose a1 := w1 `^ (p^-1) * x. - pose a2 := w2 `^ (p^-1) * y. - pose b1 := w1 `^ (q^-1). - pose b2 := w2 `^ (q^-1). - have : a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p)`^(p^-1) * (b1 `^ q + b2 `^ q)`^(q^-1). +have -> : w1 * x + w2 * y = w1 `^ (p^-1) * w1 `^ (q^-1) * x + + w2 `^ (p^-1) * w2 `^ (q^-1) * y. + rewrite -!powRD pq1; [|exact/implyP..]. + by rewrite !powRr1// /w2 ?onem_ge0. +apply: (@le_trans _ _ ((w1 * x `^ p + w2 * y `^ p) `^ (p^-1) * + (w1 + w2) `^ q^-1)). + pose a1 := w1 `^ p^-1 * x. pose a2 := w2 `^ p^-1 * y. + pose b1 := w1 `^ q^-1. pose b2 := w2 `^ q^-1. + have : a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p) `^ p^-1 * + (b1 `^ q + b2 `^ q) `^ q^-1. apply: hoelder2 => //. - - 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 _ p1). - - by rewrite (lt_le_trans _ q1). - - rewrite /q invf_div -{1}div1r -mulrDl addrC -addrA (addrC _ 1) subrr addr0 divff// gt_eqF//. - by rewrite (lt_le_trans _ p1)// orbT. - rewrite /a1/a2/b1/b2. - rewrite powRM ?powR_ge0// -powRrM mulVf; last by rewrite gt_eqF// (lt_le_trans _ p1). - rewrite powRr1 ?onem_ge0//. - rewrite powRM ?powR_ge0// -powRrM mulVf; last by rewrite gt_eqF// (lt_le_trans _ p1). + - by rewrite mulr_ge0// powR_ge0. + - by rewrite mulr_ge0// powR_ge0. + - by rewrite powR_ge0. + - by rewrite powR_ge0. + rewrite /a1 /a2 /b1 /b2 powRM ?powR_ge0// -powRrM mulVf ?gt_eqF//. + rewrite powRr1 ?onem_ge0// powRM ?powR_ge0// -powRrM mulVf ?gt_eqF//. rewrite powRr1; last by rewrite /w2. - rewrite -(@powRrM _ _ _ q) mulVf ?powRr1 ?onem_ge0//; last first. - by rewrite gt_eqF// (lt_le_trans _ q1). - rewrite -(@powRrM _ _ _ q) mulVf ?powRr1 ?onem_ge0 /w2//; last first. - by rewrite gt_eqF// (lt_le_trans _ q1). + rewrite -(@powRrM _ _ _ q) mulVf ?gt_eqF// powRr1 ?onem_ge0//. + rewrite -(@powRrM _ _ _ q) mulVf ?gt_eqF// powRr1; last by rewrite /w2. by rewrite mulrAC (mulrAC _ y) => /le_trans; exact. -rewrite le_eqVlt; apply/orP; left; apply/eqP. by rewrite {2}/w1 {2}/w2 subrK powR1 mulr1. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 20f853c4b..8eaa1ba7c 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3945,7 +3945,7 @@ transitivity (\int[mseries (fun n => [the measure _ _ of \d_ n]) O]_t a t). rewrite (@integral_measure_series _ _ R (fun n => [the measure _ _ of \d_ n]) setT)//=. - by apply: eq_eseriesr=> i _; rewrite integral_dirac//= indicE mem_set// mul1e. - move=> n; apply/integrableP; split=> [//|]. - by rewrite integral_dirac//= indicE mem_set// mul1e; exact: (summable_pinfty sa). + by rewrite integral_dirac//= indicE mem_set// mul1e (summable_pinfty sa). - by apply: summable_integral_dirac => //; exact: summable_funeneg. - by apply: summable_integral_dirac => //; exact: summable_funepos. Qed. From bb25d1237d3336e61671c9829522ed7beac2d74e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 21 Sep 2023 17:27:31 +0900 Subject: [PATCH 3/7] nitpick --- theories/hoelder.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 56964fc90..1d380fff7 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -254,7 +254,8 @@ Local Open Scope ring_scope. Lemma hoelder2 (a1 a2 b1 b2 : R) (p q : R) : 0 <= a1 -> 0 <= a2 -> 0 <= b1 -> 0 <= b2 -> 0 < p -> 0 < q -> p^-1 + q^-1 = 1 -> - a1 * b1 + a2 * b2 <= (a1`^p + a2`^p) `^ (p^-1) * (b1`^q + b2`^q)`^(q^-1). + a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p) `^ p^-1 * + (b1 `^ q + b2 `^ q) `^ q^-1. Proof. move=> a10 a20 b10 b20 p0 q0 pq. pose f a b n : R := match n with 0%nat => a | 1%nat => b | _ => 0 end. From a3d443d568dc76c0b0c7bf5dd7ef66db7e279f5a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 27 Sep 2023 19:27:58 +0900 Subject: [PATCH 4/7] fix --- CHANGELOG_UNRELEASED.md | 2 +- classical/mathcomp_extra.v | 2 +- theories/hoelder.v | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fc4ecff92..3aacf7fb5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -86,7 +86,7 @@ + lemma `gt0_ltr_powR` + lemma `powR_injective` - in `mathcomp_extra.v`: - + lemma `lerBr` + + lemma `gerBl` ### Changed diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 3a55a7813..c2ead7e4a 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1440,5 +1440,5 @@ End bigmax_seq. Arguments le_bigmax_seq {d T} x {I r} i0 P. (* NB: PR 1079 to MathComp in progress *) -Lemma lerBr {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x. +Lemma gerBl {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x. Proof. by move=> y0; rewrite ler_subl_addl ler_addr. Qed. diff --git a/theories/hoelder.v b/theories/hoelder.v index 1d380fff7..56fb52353 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -300,9 +300,9 @@ have [->|w20] := eqVneq w2 0. by rewrite lt_neqAle eq_sym onem_ge0// andbT. have [->|p_neq1] := eqVneq p 1. by rewrite !powRr1// addr_ge0// mulr_ge0// /w2 ?onem_ge0. -have {p1 p_neq1}p1 : 1 < p by rewrite lt_neqAle eq_sym p_neq1. +have {p_neq1} {}p1 : 1 < p by rewrite lt_neqAle eq_sym p_neq1. pose q := p / (p - 1). -have q1 : 1 <= q by rewrite /q ler_pdivl_mulr// ?mul1r ?lerBr// subr_gt0. +have q1 : 1 <= q by rewrite /q ler_pdivl_mulr// ?mul1r ?gerBl// subr_gt0. have q0 : 0 < q by rewrite (lt_le_trans _ q1). have pq1 : p^-1 + q^-1 = 1. rewrite /q invf_div -{1}(div1r p) -mulrDl addrCA subrr addr0. From 54baf86c1f9ef62d31cce2b72a189fabd0269240 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 28 Sep 2023 00:52:29 +0900 Subject: [PATCH 5/7] for Coq 8.14 --- theories/hoelder.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 56fb52353..fa55a9d68 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -94,7 +94,7 @@ Section lnorm. (* lnorm is just Lnorm applied to counting *) Context d {T : measurableType d} {R : realType}. -Local Notation "'N_ p [ f ]" := (Lnorm counting p f). +Local Notation "'N_ p [ f ]" := (Lnorm [the measure _ _ of counting] p f). Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R -> 'N_p%:E [f] = (\sum_(k a10 a20 b10 b20 p0 q0 pq. pose f a b n : R := match n with 0%nat => a | 1%nat => b | _ => 0 end. have mf a b : measurable_fun setT (f a b) by []. -have := hoelder counting (mf a1 a2) (mf b1 b2) p0 q0 pq. +have := hoelder [the measure _ _ of counting] (mf a1 a2) (mf b1 b2) p0 q0 pq. rewrite !Lnorm_counting//. rewrite (nneseries_split 2); last by move=> k; rewrite lee_fin powR_ge0. rewrite ereal_series_cond eseries0 ?adde0; last first. From f6762913d131daa88872ecd47db4904b32965c74 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sun, 1 Oct 2023 13:57:31 +0200 Subject: [PATCH 6/7] Shortened proof --- theories/hoelder.v | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index fa55a9d68..025f87297 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -323,16 +323,8 @@ apply: (@le_trans _ _ ((w1 * x `^ p + w2 * y `^ p) `^ (p^-1) * pose b1 := w1 `^ q^-1. pose b2 := w2 `^ q^-1. have : a1 * b1 + a2 * b2 <= (a1 `^ p + a2 `^ p) `^ p^-1 * (b1 `^ q + b2 `^ q) `^ q^-1. - apply: hoelder2 => //. - - by rewrite mulr_ge0// powR_ge0. - - by rewrite mulr_ge0// powR_ge0. - - by rewrite powR_ge0. - - by rewrite powR_ge0. - rewrite /a1 /a2 /b1 /b2 powRM ?powR_ge0// -powRrM mulVf ?gt_eqF//. - rewrite powRr1 ?onem_ge0// powRM ?powR_ge0// -powRrM mulVf ?gt_eqF//. - rewrite powRr1; last by rewrite /w2. - rewrite -(@powRrM _ _ _ q) mulVf ?gt_eqF// powRr1 ?onem_ge0//. - rewrite -(@powRrM _ _ _ q) mulVf ?gt_eqF// powRr1; last by rewrite /w2. + by apply: hoelder2 => //; rewrite ?mulr_ge0 ?powR_ge0. + rewrite ?powRM ?powR_ge0 -?powRrM ?mulVf ?powRr1 ?gt_eqF ?onem_ge0/w2//. by rewrite mulrAC (mulrAC _ y) => /le_trans; exact. by rewrite {2}/w1 {2}/w2 subrK powR1 mulr1. Qed. From ed13992aba97aa85e936c7a0b31576465c68a50d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 2 Oct 2023 17:00:28 +0900 Subject: [PATCH 7/7] fix --- theories/hoelder.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 025f87297..bf5c85465 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -310,7 +310,7 @@ have pq1 : p^-1 + q^-1 = 1. rewrite -(@powRr1 _ (w1 * x `^ p + w2 * y `^ p)); last first. by rewrite addr_ge0// mulr_ge0// ?powR_ge0// /w2 ?onem_ge0// itv_ge0. have -> : 1 = p^-1 * p by rewrite mulVf ?gt_eqF. -rewrite powRrM (gt0_ler_powR (le_trans _ (ltW p1)))//. +rewrite powRrM (ge0_ler_powR (le_trans _ (ltW p1)))//. - by rewrite nnegrE addr_ge0// mulr_ge0 /w2 ?onem_ge0. - by rewrite nnegrE powR_ge0. have -> : w1 * x + w2 * y = w1 `^ (p^-1) * w1 `^ (q^-1) * x +