diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index dd30e31d60..8efbde13ec 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -51,17 +51,6 @@ + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0` + lemma `hoelder` -- in `lebesgue_measure.v`: - + lemma `measurable_mulrr` - -- in `constructive_ereal.v`: - + lemma `eqe_pdivr_mull` - -- new file `hoelder.v`: - + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]` - + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0` - + lemma `hoelder` - - in file `lebesgue_integral.v`, + new lemmas `simple_bounded`, `measurable_bounded_integrable`, `compact_finite_measure`, `approximation_continuous_integrable` @@ -80,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` ### Changed diff --git a/theories/convex.v b/theories/convex.v index 5eff17447a..7b4047c6c0 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 b21b553f90..5110b27bec 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,12 +664,46 @@ 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. by rewrite /powR gt_eqF ?(lt_le_trans _ a1)// ler_expR ler_wpmul2r ?ln_ge0. 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 gt0_ler_powR (r : R) : 0 <= r -> {in `[0, +oo[ &, {homo powR ^~ r : x y / x <= y >-> x <= y}}. Proof. @@ -684,6 +724,22 @@ 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 12f5e600b0..07f97e4abe 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 *) @@ -61,27 +61,18 @@ rewrite /Lnorm oner_eq0 invr1// poweRe1//. by apply: integral_ge0 => t _; rewrite powRr1. Qed. -<<<<<<< HEAD Lemma Lnorm_ge0 p f : 0 <= 'N_p[f]. Proof. move: p => [r/=|/=|//]. by case: ifPn => // r0; exact: poweR_ge0. by case: ifPn => // /ess_sup_ge0; apply => t/=. Qed. -======= -Lemma Lnorm_ge0 p f : 0 <= 'N_p[f]. Proof. exact: poweR_ge0. Qed. ->>>>>>> eb049178 (going back to the N notation) Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g]. Proof. by move=> fg; congr Lnorm; exact/funext. Qed. -<<<<<<< HEAD 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 p f : measurable_fun setT f -> 'N_p[f] = 0 -> - ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0). ->>>>>>> eb049178 (going back to the N notation) Proof. move=> r0 mf/=; rewrite (gt_eqF r0) => /poweR_eq0_eq0 fp. apply/ae_eq_integral_abs => //=. @@ -98,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}. @@ -111,11 +116,7 @@ Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed. Local Notation "'N_ p [ f ]" := (Lnorm mu p f). Let integrable_powR f p : (0 < p)%R -> -<<<<<<< HEAD measurable_fun [set: T] f -> 'N_p%:E[f] != +oo -> -======= - measurable_fun [set: T] f -> 'N_p[f] != +oo -> ->>>>>>> eb049178 (going back to the N notation) mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E). Proof. move=> p0 mf foo; apply/integrableP; split. @@ -129,11 +130,7 @@ Qed. Let hoelder0 f g p q : measurable_fun setT f -> measurable_fun setT g -> (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R -> -<<<<<<< HEAD 'N_p%:E[f] = 0 -> 'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g]. -======= - 'N_p[f] = 0 -> 'N_1[(f \* g)%R] <= 'N_p[f] * 'N_q[g]. ->>>>>>> eb049178 (going back to the N notation) Proof. move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//. rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0. @@ -247,3 +244,112 @@ 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 lerBlDl 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 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; [|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. \ No newline at end of file diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index ff4ab41cf4..20f853c4bb 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.