From 5e6647b1041b0e3e3bb869bcdbf04b7f9fde7e16 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 8 Aug 2023 14:44:43 +0900 Subject: [PATCH] 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 | 80 ++--------- theories/convex.v | 4 + theories/exp.v | 56 ++++++++ theories/hoelder.v | 125 ++++++++++++++++- theories/lebesgue_integral.v | 257 ++--------------------------------- 5 files changed, 208 insertions(+), 314 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 51d5c39056..8efbde13ec 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -22,74 +22,6 @@ - in `exp.v`: + lemmas `concave_ln`, `conjugate_powR` - + lemma `concave_ln` -- in `lebesgue_measure.v`: - + lemma `closed_measurable` - -- in file `lebesgue_measure.v`, - + new lemmas `lebesgue_nearly_bounded`, and `lebesgue_regularity_inner`. -- in file `measure.v`, - + new lemmas `measureU0`, `nonincreasing_cvg_mu`, and `epsilon_trick0`. -- in file `real_interval.v`, - + new lemma `bigcup_itvT`. -- in file `topology.v`, - + new lemma `uniform_nbhsT`. - -- in file `topology.v`, - + new definition `set_nbhs`. - + new lemmas `filterI_iter_sub`, `filterI_iterE`, `finI_fromI`, - `filterI_iter_finI`, `smallest_filter_finI`, and `set_nbhsP`. - -- in file `lebesgue_measure.v`, - + new lemmas `pointwise_almost_uniform`, and - `ae_pointwise_almost_uniform`. - -- in `exp.v`: - + lemmas `powRrM`, `gt0_ler_powR`, - `gt0_powR`, `norm_powR`, `lt0_norm_powR`, - `powRB` - + lemmas `poweRrM`, `poweRAC`, `gt0_poweR`, - `poweR_eqy`, `eqy_poweR`, `poweRD`, `poweRB` - -- in `mathcomp_extra.v`: - + definition `min_fun`, notation `\min` -- in `classical_sets.v`: - + lemmas `set_predC`, `preimage_true`, `preimage_false` -- in `lebesgue_measure.v`: - + lemmas `measurable_fun_ltr`, `measurable_minr` -- in file `lebesgue_integral.v`, - + new lemmas `lusin_simple`, and `measurable_almost_continuous`. -- in file `measure.v`, - + new lemmas `finite_card_sum`, and `measureU2`. - -- in `topology.v`: - + lemma `bigsetU_compact` - -- in `exp.v`: - + notation `` e `^?(r +? s) `` - + lemmas `expR_eq0`, `powRN` - + definition `poweRD_def` - + lemmas `poweRD_defE`, `poweRB_defE`, `add_neq0_poweRD_def`, - `add_neq0_poweRB_def`, `nneg_neq0_poweRD_def`, `nneg_neq0_poweRB_def` - + lemmas `powR_eq0`, `poweR_eq0` -- in file `lebesgue_integral.v`, - + new lemma `approximation_sfun_integrable`. - -- in `classical_sets.v`: - + lemmas `properW`, `properxx` - -- in `classical_sets.v`: - + lemma `Zorn_bigcup` -- in `lebesgue_measure.v`: - + lemma `measurable_mulrr` - -- in `constructive_ereal.v`: - + lemma `eqe_pdivr_mull` - -- in `lebesgue_integral.v`: - + definition `L_norm`, notation `'N[mu]_p[f]` - + lemmas `L_norm_ge0`, `eq_L_norm` - + lemmas `hoelder` - in file `lebesgue_integral.v`, + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and @@ -137,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 2d262c10fa..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 *) @@ -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,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 7ed33ae19c..20f853c4bb 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.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 numfun exp itv. +Require Import esum measure lebesgue_measure numfun. (******************************************************************************) (* Lebesgue Integral *) @@ -45,8 +45,6 @@ Require Import esum measure lebesgue_measure numfun exp itv. (* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *) (* measure over T1, and m1 is a sigma finite *) (* measure over T2 *) -(* 'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 *) -(* The corresponding definition is L_norm *) (* *) (******************************************************************************) @@ -69,13 +67,6 @@ Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable"). Reserved Notation "m1 '\x' m2" (at level 40, m2 at next level). Reserved Notation "m1 '\x^' m2" (at level 40, m2 at next level). -Reserved Notation "'N[ mu ]_ p [ F ]" - (at level 5, F at level 36, mu at level 10, - format "'[' ''N[' mu ]_ p '/ ' [ F ] ']'"). -Reserved Notation "''N_' p [ F ]" (* for use as a local notation *) - (at level 5, F at level 36, - format "'[' ''N_' p '/ ' [ F ] ']'"). - #[global] Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. @@ -3959,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. @@ -5630,238 +5632,3 @@ by rewrite ritv //= -EFinM lee_fin mulrC. Unshelve. all: by end_near. Qed. End lebesgue_differentiation. - -Section L_norm. -Context d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R}). -Local Open Scope ereal_scope. - -Definition L_norm (p : R) (f : T -> R) : \bar R := - (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1. - -Local Notation "'N_ p [ f ]" := (L_norm p f). - -Lemma L_norm_ge0 (p : R) (f : T -> R) : (0 <= 'N_p[f])%E. -Proof. by rewrite /L_norm poweR_ge0. Qed. - -Lemma eq_L_norm (p : R) (f g : T -> R) : f =1 g -> 'N_p[f] = 'N_p[g]. -Proof. by move=> fg; congr L_norm; exact/funext. Qed. - -End L_norm. -#[global] -Hint Extern 0 (0 <= L_norm _ _ _) => solve [apply: L_norm_ge0] : core. - -Notation "'N[ mu ]_ p [ f ]" := (L_norm mu p f). - -Section hoelder. -Context d (T : measurableType d) (R : realType). -Variable mu : {measure set T -> \bar R}. -Local Open Scope ereal_scope. - -Let measurableT_comp_powR (f : T -> R) p : - measurable_fun setT f -> measurable_fun setT (fun x => f x `^ p)%R. -Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed. - -Let integrable_powR (f : T -> R) p : (0 < p)%R -> - measurable_fun setT f -> 'N[mu]_p[f] != +oo -> - mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E). -Proof. -move=> p0 mf foo; apply/integrableP; split. - apply: measurableT_comp => //; apply: measurableT_comp_powR. - exact: measurableT_comp. -rewrite ltey; apply: contra foo. -move=> /eqP/(@eqy_poweR _ _ p^-1); rewrite invr_gt0 => /(_ p0) <-. -apply/eqP; congr (_ `^ _); apply/eq_integral. -by move=> x _; rewrite gee0_abs // ?lee_fin ?powR_ge0. -Qed. - -Local Notation "'N_ p [ f ]" := (L_norm mu p f). - -Let hoelder0 (f g : T -> R) (p q : R) : - measurable_fun setT f -> measurable_fun setT g -> - (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R -> - 'N[mu]_p[f] = 0 -> - 'N[mu]_1 [(f \* g)%R] <= 'N[mu]_p [f] * 'N[mu]_q [g]. -Proof. -move=> mf mg p0 q0 pq f0; rewrite f0 mul0e. -suff: 'N_1 [(f \* g)%R] = 0%E by move=> ->. -move: f0; rewrite /L_norm; move/poweR_eq0_eq0. -rewrite /= invr1 poweRe1// => [fp|]; last first. - by apply: integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. -have {fp}f0 : ae_eq mu setT (fun x => (`|f x| `^ p)%:E) (cst 0). - apply/ae_eq_integral_abs => //=. - - apply: measurableT_comp => //; apply: measurableT_comp_powR. - exact: measurableT_comp. - - under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//. - by apply/fp/integral_ge0 => t _; rewrite lee_fin; exact: powR_ge0. -rewrite (ae_eq_integral (cst 0)%E) => [|//||//|]. -- by rewrite integral0. -- apply: measurableT_comp => //; apply: measurableT_comp_powR => //. - by apply: measurableT_comp => //; exact: measurable_funM. -- apply: filterS f0 => x /(_ I) /= [] /powR_eq0_eq0 fp0 _. - by rewrite powRr1// normrM fp0 mul0r. -Qed. - -Let normed p f x := `|f x| / fine 'N_p[f]. - -Let normed_ge0 p f x : (0 <= normed p f x)%R. -Proof. by rewrite /normed divr_ge0// fine_ge0// L_norm_ge0. Qed. - -Let measurable_normed p f : measurable_fun setT f -> - measurable_fun setT (normed p f). -Proof. -move=> mf; rewrite (_ : normed _ _ = *%R (fine ('N[mu]_p[f]))^-1 \o normr \o f). - by apply: measurableT_comp => //; exact: measurableT_comp. -by apply/funext => x /=; rewrite mulrC. -Qed. - -Let normed_expR p f x : (0 < p)%R -> - let F := normed p f in F x != 0%R -> expR (ln (F x `^ p) / p) = F x. -Proof. -move=> p0 F Fx0. -rewrite ln_powR// mulrAC divff// ?gt_eqF// mul1r. -by rewrite lnK// posrE lt_neqAle normed_ge0 eq_sym Fx0. -Qed. - -Let integral_normed f p : (0 < p)%R -> 0 < 'N_p[f] -> - mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E) -> - \int[mu]_x (normed p f x `^ p)%:E = 1. -Proof. -move=> p0 fpos ifp. -transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p[f] `^ p))%:E). - apply: eq_integral => t _. - rewrite powRM//; last by rewrite invr_ge0 fine_ge0// L_norm_ge0. - rewrite -powR_inv1; last by rewrite fine_ge0 // L_norm_ge0. - by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0. -rewrite /L_norm -poweRrM mulVf ?lt0r_neq0// poweRe1; last first. - by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. -under eq_integral do rewrite EFinM muleC. -rewrite integralZl//; apply/eqP; rewrite eqe_pdivr_mull ?mule1; last first. - rewrite gt_eqF// fine_gt0//; apply/andP; split. - apply: gt0_poweR fpos; rewrite ?invr_gt0//. - by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0. - move/integrableP: ifp => -[_]. - under eq_integral. - move=> x _; rewrite gee0_abs//; last by rewrite lee_fin powR_ge0. - over. - by []. -rewrite fineK// ge0_fin_numE//; last first. - by rewrite integral_ge0// => x _; rewrite lee_fin// powR_ge0. -move/integrableP: ifp => -[_]. -under eq_integral. - move=> x _; rewrite gee0_abs//; last by rewrite lee_fin powR_ge0. - over. -by []. -Qed. - -Lemma hoelder (f g : T -> R) (p q : R) : - measurable_fun setT f -> measurable_fun setT g -> - (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R -> - 'N[mu]_1 [(f \* g)%R] <= 'N[mu]_p [f] * 'N[mu]_q [g]. -Proof. -move=> mf mg p0 q0 pq. -have [f0|f0] := eqVneq 'N_p[f] 0%E; first exact: hoelder0. -have [g0|g0] := eqVneq 'N_q[g] 0%E. - rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC. - by under eq_L_norm do rewrite /= mulrC. -have {f0}fpos : 0 < 'N_p[f] by rewrite lt_neqAle eq_sym f0//= L_norm_ge0. -have {g0}gpos : 0 < 'N_q[g] by rewrite lt_neqAle eq_sym g0//= L_norm_ge0. -have [foo|foo] := eqVneq 'N_p[f] +oo%E; first by rewrite foo gt0_mulye ?leey. -have [goo|goo] := eqVneq 'N_q[g] +oo%E; first by rewrite goo gt0_muley ?leey. -pose F := normed p f. -pose G := normed q g. -have exp_convex x : (F x * G x <= F x `^ p / p + G x `^ q / q)%R. - have [Fx0|Fx0] := eqVneq (F x) 0%R. - by rewrite Fx0 mul0r powR0 ?gt_eqF// mul0r add0r divr_ge0 ?powR_ge0 ?ltW. - have {}Fx0 : (0 < F x)%R. - by rewrite lt_neqAle eq_sym Fx0 divr_ge0// fine_ge0// L_norm_ge0. - have [Gx0|Gx0] := eqVneq (G x) 0%R. - by rewrite Gx0 mulr0 powR0 ?gt_eqF// mul0r addr0 divr_ge0 ?powR_ge0 ?ltW. - have {}Gx0 : (0 < G x)%R. - by rewrite lt_neqAle eq_sym Gx0/= divr_ge0// fine_ge0// L_norm_ge0. - pose s x := ln ((F x) `^ p). - pose t x := ln ((G x) `^ q). - have : (expR (p^-1 * s x + q^-1 * t x) <= - p^-1 * expR (s x) + q^-1 * expR (t x))%R. - have -> : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK. - have K : (q^-1 \in `[0, 1])%R. - by rewrite in_itv/= invr_ge0 (ltW q0)/= -pq ler_paddl// invr_ge0 ltW. - exact: (convex_expR (@Itv.mk _ `[0, 1] q^-1 K)%R). - rewrite expRD (mulrC _ (s x)) normed_expR ?gt_eqF// -/(F x). - rewrite (mulrC _ (t x)) normed_expR ?gt_eqF// -/(G x) => /le_trans; apply. - rewrite /s /t [X in (_ * X + _)%R](@lnK _ (F x `^ p)%R); last first. - by rewrite posrE powR_gt0. - rewrite (@lnK _ (G x `^ q)%R); last by rewrite posrE powR_gt0. - by rewrite mulrC (mulrC _ q^-1). -have -> : 'N_1[(f \* g)%R] = 'N_1[(F \* G)%R] * 'N_p[f] * 'N_q[g]. - rewrite {1}/L_norm; under eq_integral => x _ do rewrite powRr1//. - rewrite invr1 poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin. - rewrite {1}/L_norm. - under [in RHS]eq_integral. - move=> x _. - rewrite /F /G /= /normed (mulrC `|f x|)%R mulrA -(mulrA (_^-1)). - rewrite (mulrC (_^-1)) -mulrA ger0_norm; last first. - by rewrite mulr_ge0// divr_ge0 ?(fine_ge0,L_norm_ge0,invr_ge0). - rewrite powRr1; last first. - by rewrite mulr_ge0// divr_ge0 ?(fine_ge0,L_norm_ge0,invr_ge0). - rewrite mulrC -normrM EFinM. - over. - rewrite /= ge0_integralZl//; last 2 first. - - apply: measurableT_comp => //; apply: measurableT_comp => //. - exact: measurable_funM. - - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// L_norm_ge0. - rewrite -muleA muleC invr1 poweRe1; last first. - rewrite mule_ge0//. - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// L_norm_ge0. - by apply integral_ge0 => x _; rewrite lee_fin. - rewrite muleA EFinM. - rewrite muleCA 2!muleA (_ : _ * 'N_p[f] = 1) ?mul1e; last first. - apply/eqP; rewrite eqe_pdivr_mull ?mule1; last first. - by rewrite gt_eqF// fine_gt0// fpos/= ltey. - by rewrite fineK// ?ge0_fin_numE ?ltey// L_norm_ge0. - rewrite (_ : 'N_q[g] * _ = 1) ?mul1e// muleC. - apply/eqP; rewrite eqe_pdivr_mull ?mule1; last first. - by rewrite gt_eqF// fine_gt0// gpos/= ltey. - by rewrite fineK// ?ge0_fin_numE ?ltey// L_norm_ge0. -rewrite -(mul1e ('N_p[f] * _)) -muleA lee_pmul ?mule_ge0 ?L_norm_ge0//. -apply: (@le_trans _ _ (\int[mu]_x (F x `^ p / p + G x `^ q / q)%:E)). - rewrite /L_norm invr1 poweRe1; last first. - by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. - apply: ae_ge0_le_integral => //. - - by move=> x _; exact: powR_ge0. - - apply: measurableT_comp => //; apply: measurableT_comp_powR => //. - apply: measurableT_comp => //. - by apply: measurable_funM => //; exact: measurable_normed. - - by move=> x _; rewrite lee_fin addr_ge0// divr_ge0// ?powR_ge0// ltW. - - by apply: measurableT_comp => //; apply: measurable_funD => //; - apply: measurable_funM => //; apply: measurableT_comp_powR => //; - exact: measurable_normed. - apply/aeW => x _. - by rewrite lee_fin powRr1// ger0_norm ?exp_convex// mulr_ge0// normed_ge0. -rewrite le_eqVlt; apply/orP; left; apply/eqP. -under eq_integral do rewrite EFinD mulrC (mulrC _ (_^-1)). -rewrite ge0_integralD//; last 4 first. -- by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW. -- apply: measurableT_comp => //; apply: measurableT_comp => //. - by apply: measurableT_comp_powR => //; exact: measurable_normed. -- by move=> x _; rewrite lee_fin mulr_ge0// ?invr_ge0 ?powR_ge0// ltW. -- apply: measurableT_comp => //; apply: measurableT_comp => //. - by apply: measurableT_comp_powR => //; exact: measurable_normed. -under eq_integral do rewrite EFinM. -rewrite {1}ge0_integralZl//; last 3 first. -- apply: measurableT_comp => //. - by apply: measurableT_comp_powR => //; exact: measurable_normed. -- by move=> x _; rewrite lee_fin powR_ge0. -- by rewrite lee_fin invr_ge0 ltW. -under [X in (_ + X)%E]eq_integral => x _ do rewrite EFinM. -rewrite ge0_integralZl//; last 3 first. -- apply: measurableT_comp => //. - by apply: measurableT_comp_powR => //; exact: measurable_normed. -- by move=> x _; rewrite lee_fin powR_ge0. -- by rewrite lee_fin invr_ge0 ltW. -rewrite integral_normed//; last exact: integrable_powR. -rewrite integral_normed//; last exact: integrable_powR. -by rewrite 2!mule1 -EFinD pq. -Qed. - -End hoelder.