From 72db09dc79f99c0ca85f9288eccbda07bc49a8b9 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Wed, 23 Aug 2023 14:37:10 +0200 Subject: [PATCH] Minkowski's inequality and accessory lemmas Co-authored-by: @affeldt-aist --- CHANGELOG_UNRELEASED.md | 6 ++ theories/exp.v | 36 ++++++++ theories/hoelder.v | 195 +++++++++++++++++++++++++++++++++++++++- 3 files changed, 236 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 43203f890f..10ad5fd3b5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -64,6 +64,12 @@ - in `lebesgue_integral.v`: + lemma `ge0_integral_count` +- in `exp.v`: + + lemmas `powRDm1`, `poweRN`, `poweR_lty`, `lty_powerRy`, `gt0_ler_poweR` + +- in `hoelder.v`: + + lemmas `Lnorm_powR_K`, `oneminvp`, `minkowski` + ### Changed - `mnormalize` moved from `kernel.v` to `measure.v` and generalized diff --git a/theories/exp.v b/theories/exp.v index 9643d6d909..8223933fbf 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -759,6 +759,16 @@ have [->|] := eqVneq r 0; first by rewrite mul1r add0r. by rewrite implybF mul0r => _ /negPf ->. Qed. +Lemma powRDm1 (x p : R) : 0 <= x -> 0 < p -> x * x `^ (p - 1) = x `^ p. +Proof. +move=> x0 p0. +have [->|xneq0] := eqVneq x 0. + by rewrite mul0r powR0// gt_eqF. +rewrite -{1}(@powRr1 x)// -powRD. + by rewrite addrCA subrr addr0. +by rewrite xneq0 implybT. +Qed. + Lemma powRN x r : x `^ (- r) = (x `^ r)^-1. Proof. have [r0|r0] := eqVneq r 0%R; first by rewrite r0 oppr0 powRr0 invr1. @@ -871,6 +881,9 @@ Proof. by move: x => [x'| |]//= x0; rewrite ?powRr1// (negbTE (oner_neq0 _)). Qed. +Lemma poweRN (x : \bar R) r : x \is a fin_num -> x `^ (- r) = (((fine x) `^ r)^-1)%:E. +Proof. case: x => // x xf. by rewrite poweR_EFin powRN. Qed. + Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0. Proof. by move=> r0 /=; rewrite (negbTE r0). Qed. @@ -880,6 +893,16 @@ Proof. by case: x => [x| |] //=; case: ifP. Qed. Lemma eqy_poweR x r : (0 < r)%R -> x = +oo -> x `^ r = +oo. Proof. by move: x => [| |]//= r0 _; rewrite gt_eqF. Qed. +Lemma poweR_lty (a : \bar R) (r : R) : a < +oo -> a `^ r < +oo. +Proof. +by move: a => [a| | _]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry. +Qed. + +Lemma lty_poweRy (a : \bar R) (r : R) : r != 0%R -> a `^ r < +oo -> a < +oo. +Proof. +by move=> r0; move: a => [a| | _]//=; rewrite ?ltry// (negbTE r0). +Qed. + Lemma poweR0r r : r != 0%R -> 0 `^ r = 0. Proof. by move=> r0; rewrite poweR_EFin powR0. Qed. @@ -913,6 +936,19 @@ Qed. Lemma poweR_eq0_eq0 x r : 0 <= x -> x `^ r = 0 -> x = 0. Proof. by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed. +Lemma gt0_ler_poweR (r : R) : (0 <= r)%R -> + {in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}. +Proof. +move=> r0 x y. +case: x => //= [x xint| _ _]. +- case: y => //= [y yint xy| _ _]. + - rewrite !lee_fin gt0_ler_powR//. + by move: xint; rewrite !in_itv /= andbT lee_fin => /andP [x0 _]. + by move: yint; rewrite !in_itv /= andbT lee_fin => /andP [y0 _]. + - by case: eqP => [->|]; rewrite ?powRr0 ?leey. +- by rewrite leye_eq => /eqP ->. +Qed. + Lemma poweRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r. Proof. have [->|rN0] := eqVneq r 0%R; first by rewrite !poweRe0 mule1. diff --git a/theories/hoelder.v b/theories/hoelder.v index 0a31c053e3..34636430e0 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -69,6 +69,13 @@ under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//. by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0. Qed. +Lemma Lnorm_powR_K f p : (p != 0%R) -> 'N_p[f] `^ p = \int[mu]_x (`| f x | `^ p)%:E. +Proof. +move=>p0. +rewrite /Lnorm -poweRrM mulVf//. +by rewrite poweRe1// integral_ge0// => x _; rewrite lee_fin// powR_ge0. +Qed. + End Lnorm. #[global] Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core. @@ -343,4 +350,190 @@ rewrite le_eqVlt; apply/orP; left; apply/eqP. by rewrite {2}/w1 {2}/w2 -addrA (addrC (- _)) subrr addr0 powR1 mulr1. Qed. -End convex_powR. \ No newline at end of file +End convex_powR. + +Section minkowski. +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 "'N_ p [ f ]" := (Lnorm mu p f). + +Let minkowski_half (f g : T -> R) (p : R) x : (1 < p)%R -> + (`| 2^-1 * f x + 2^-1 * g x | `^ p <= 2^-1 * `| f x | `^ p + 2^-1 * `| g x | `^ p)%R. +Proof. +move=> p1. +apply: (@le_trans _ _ ((2^-1 * `| f x | + 2^-1 * `| g x |) `^ p))%R. + apply: gt0_ler_powR. + - by rewrite le_eqVlt; apply/orP; right; apply: (@lt_trans _ _ 1%R) => //. + - by rewrite in_itv/= andbT. + - by rewrite in_itv/= andbT. + - have -> : (2^-1 * `|f x| + 2^-1 * `|g x| = `|2^-1 * f x| + `|2^-1 * g x|)%R. + by rewrite !normrM !(@ger0_norm _ (2^-1)). + exact: ler_norm_add. +rewrite {1 3}(_ : 2^-1 = 1 - 2^-1 :> R)%R; last by rewrite {2}(splitr 1) div1r addrK. +have K : ((2^-1 : R) \in `[0, 1])%R. + by rewrite in_itv//= invr_ge0 ler0n/= invf_le1// ler1n. +apply (@convex_powR _ _ (ltW p1) (@Itv.mk _ `[0, 1] 2^-1 K)%R (`|f x|)%R (`|g x|)%R); + by rewrite inE /= in_itv /= normr_ge0. +Qed. + +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 minkowski_lty (f g : T -> R) (p : R) : + measurable_fun setT f -> measurable_fun setT g -> + (1 < p)%R -> 'N_p[f] < +oo -> 'N_p[g] < +oo -> 'N_p[(f \+ g)%R] < +oo. +Proof. +move=> mf mg p1 Nfoo Ngoo. +have h x : (`| f x + g x | `^ p <= 2 `^ (p - 1) * (`| f x | `^ p + `| g x | `^ p))%R. + have := minkowski_half (fun x => 2 * f x)%R (fun x => 2 * g x)%R x p1. + rewrite mulrA mulVf// mul1r mulrA mulVf// mul1r !normrM (@ger0_norm _ 2)//. + move=> /le_trans; apply. + rewrite !powRM// !mulrA -powR_inv1//. + rewrite -powRD; last by apply /implyP => _. + by rewrite (addrC _ p) -mulrDr. +rewrite /Lnorm poweR_lty//. +apply: (@le_lt_trans _ _ (\int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p)%R)%:E)). + apply: ge0_le_integral => //=. + - by move=> t _; rewrite lee_fin// powR_ge0. + - apply/EFin_measurable_fun/measurableT_comp_powR. + by apply: measurableT_comp => //; exact: measurable_funD. + - by move=> t _; rewrite lee_fin// mulr_ge0// ?addr_ge0 ?powR_ge0. + - by apply/EFin_measurable_fun/measurable_funM => //; apply/measurable_funD => //; + apply: measurableT_comp_powR => //; apply: measurableT_comp. + - by move=> x _; rewrite lee_fin. +under eq_integral do rewrite EFinM. +rewrite ge0_integralM_EFin//; last 3 first. + - by move=> x _; rewrite lee_fin addr_ge0// powR_ge0. + - by apply/EFin_measurable_fun/measurable_funD => //; + apply: measurableT_comp_powR => //; apply: measurableT_comp. + - by rewrite powR_ge0. +rewrite lte_mul_pinfty ?lee_fin ?powR_ge0//. +under eq_integral do rewrite EFinD. +rewrite ge0_integralD//; last 4 first. + - by move=> x _; rewrite lee_fin powR_ge0. + - by apply/EFin_measurable_fun; + apply: measurableT_comp_powR => //; apply: measurableT_comp. + - by move=> x _; rewrite lee_fin powR_ge0. + - by apply/EFin_measurable_fun; + apply: measurableT_comp_powR => //; apply: measurableT_comp. +rewrite lte_add_pinfty//. +- apply: lty_poweRy Nfoo. + by rewrite invr_neq0// gt_eqF// (le_lt_trans _ p1). +- apply: lty_poweRy Ngoo. + by rewrite invr_neq0// gt_eqF// (le_lt_trans _ p1). +Qed. + +Lemma oneminvp (p : R) : (p != 0 -> 1 - p^-1 = (p-1)/p)%R. (* conjugate lemma? *) +Proof. +by move=> p0; rewrite mulrDl divff// mulN1r. +Qed. + +Lemma minkowski (f g : T -> R) (p : R) : + measurable_fun setT f -> measurable_fun setT g -> + (1 < p)%R -> + 'N_p[(f \+ g)%R] <= 'N_p[f] + 'N_p[g]. +Proof. +move=> mf mg p1. +have [->|Nfoo] := eqVneq 'N_p[f] +oo. + by rewrite addye ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)). +have [->|Ngoo] := eqVneq 'N_p[g] +oo. + by rewrite addey ?leey// -ltNye (lt_le_trans _ (Lnorm_ge0 _ _ _)). +have Nfgoo : 'N_p[(f \+ g)%R] < +oo. + by apply: minkowski_lty => //; rewrite ltey; [exact: Nfoo|exact: Ngoo]. +have pm10 : (p - 1 != 0)%R. + by rewrite gt_eqF// subr_gt0. +have p0 : (0 < p)%R. + by apply: (lt_trans _ p1). +have pneq0 : (p != 0)%R. + by rewrite neq_lt p0 orbT. +have : 'N_p[(f \+ g)%R] `^ p <= + ('N_p[f] + 'N_p[g]) * 'N_p[(f \+ g)%R] `^ p * ((fine 'N_p[(f \+ g)%R])^-1)%:E. + rewrite Lnorm_powR_K//. + under eq_integral => x _ do rewrite -powRDm1//. + apply: (@le_trans _ _ (\int[mu]_x ((`|f x| + `|g x|) * `|f x + g x| `^ (p - 1))%:E)). + apply: ge0_le_integral => //. + - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0. + - apply: measurableT_comp => //; apply: measurable_funM. + by apply: measurableT_comp => //; exact: measurable_funD. + apply: (measurableT_comp (f:=@powR R^~ (p-1)%R)) =>//. + by apply: measurableT_comp => //; exact: measurable_funD. + - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0. + - apply: measurableT_comp => //; apply: measurable_funM. + by apply: measurable_funD => //; exact: measurableT_comp. + apply: (measurableT_comp (f:=@powR R^~ (p-1)%R)) => //. + by apply: measurableT_comp => //; exact: measurable_funD. + - by move=> x _; rewrite lee_fin ler_wpmul2r// ?powR_ge0// ler_norm_add. + under eq_integral=> x _ do rewrite mulrDl EFinD. + rewrite ge0_integralD//; last 4 first. + - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0. + - apply: measurableT_comp => //; apply: measurable_funM. + exact: measurableT_comp. + apply: (measurableT_comp (f:=@powR R^~ (p-1)%R)) => //. + by apply: measurableT_comp => //; exact: measurable_funD. + - by move=> x _; rewrite lee_fin mulr_ge0// powR_ge0. + - apply: measurableT_comp => //; apply: measurable_funM. + exact: measurableT_comp. + apply: (measurableT_comp (f:=@powR R^~ (p-1)%R)) => //. + by apply: measurableT_comp => //; exact: measurable_funD. + apply: (@le_trans _ _ (('N_p[f] + 'N_p[g]) * + (\int[mu]_x (`|f x + g x| `^ p)%:E) `^ (1 - p^-1))). + rewrite muleDl; last 2 first. + - rewrite fin_numElt (@lt_le_trans _ _ 0) ?poweR_ge0// andTb poweR_lty//. + by rewrite (@lty_poweRy _ _ (p^-1))// invr_neq0// eq_sym neq_lt (@lt_trans _ _ 1)%R. + - by rewrite ge0_adde_def//= inE Lnorm_ge0. + rewrite lee_add//. + - apply: (@le_trans _ _ ('N_1[(f \* (@powR R ^~ (p - 1) \o normr \o (f \+ g)))%R])). + rewrite /Lnorm invr1 [leRHS]poweRe1/=; last first. + by apply: integral_ge0 => x _; rewrite lee_fin powRr1. + rewrite le_eqVlt; apply/orP; left; apply/eqP. + apply: eq_integral => x _; congr EFin. + by rewrite powRr1// -{1}(ger0_norm (powR_ge0 _ _)) -normrM. + apply: le_trans. + apply: (@hoelder _ _ _ _ _ _ p (p / (p - 1))) => //. + - by apply: (measurableT_comp (measurableT_comp _ _) (measurable_funD _ _)). + - by rewrite divr_gt0// subr_gt0. + - by rewrite invf_div -(oneminvp pneq0) addrCA subrr addr0. + rewrite le_eqVlt; apply/orP; left; apply/eqP; apply: congr2=>[//|]. + rewrite (oneminvp pneq0) -[in RHS]invf_div /Lnorm; apply: congr2 => [|//]. + by apply: eq_integral => x _; + rewrite norm_powR// normr_id -powRrM mulrC -mulrA (mulrC (_^-1)) divff ?mulr1. + - rewrite [leLHS](_ : _ = 'N_1[(g \* (fun x => `|f x + g x| `^ (p - 1)))%R]); last first. + under eq_integral=> x _ do rewrite -(normr_id (f x + g x))%R -norm_powR// -normrM. + by rewrite -(Lnorm1). + apply: le_trans. + apply: (@hoelder _ _ _ _ _ _ p ((1-p^-1)^-1)) => //. + - by apply: measurableT_comp_powR; apply: measurableT_comp => //; apply: measurable_funD => //. + - by rewrite invr_gt0 onem_gt0// invf_lt1. + - by rewrite invrK (addrC 1%R) addrA subrr add0r. + rewrite le_eqVlt; apply/orP; left; apply/eqP. + apply: congr1; rewrite /Lnorm invrK; apply: congr2=>[|//]. + by apply: eq_integral => x _; + rewrite ger0_norm ?powR_ge0// -powRrM oneminvp// invf_div mulrCA divff ?mulr1. + rewrite le_eqVlt; apply/orP; left; apply/eqP; rewrite -muleA; congr (_ * _). + under [X in X * _]eq_integral=> x _ do rewrite powRDm1 ?subr_gt0//. + rewrite poweRD; last by rewrite poweRD_defE gt_eqF ?implyFb// subr_gt0 invf_lt1//. + rewrite poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. + congr (_ * _); rewrite poweRN /Lnorm ?fine_poweR// fin_numElt (@lt_le_trans _ _ 0)// ?andTb. + by rewrite (lty_poweRy (invr_neq0 pneq0) Nfgoo)//. + by apply: integral_ge0=> x _; rewrite lee_fin powR_ge0. +have [-> _|Nfg0] := (eqVneq 'N_p[(f \+ g)%R] 0). + by rewrite adde_ge0 ?Lnorm_ge0. +rewrite lee_pdivl_mulr ?fine_gt0// ?Nfgoo ?andbT; last by + rewrite lt_neqAle Lnorm_ge0 andbT eq_sym. +rewrite -{1}(@fineK _ ('N_p[(f \+ g)%R] `^ p)); last by + rewrite fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (poweR_ge0 _ _))// andTb poweR_lty. +rewrite -(invrK (fine _)) lee_pdivr_mull; last by + rewrite invr_gt0 fine_gt0// poweR_lty// andbT lt_neqAle eq_sym poweR_eq0 poweR_ge0// andbT; + rewrite neq_lt (lt_trans _ p1)// orbT andbT. +rewrite muleC -muleA -{1}(@fineK _ ('N_p[(f \+ g)%R] `^ p)); last by + rewrite fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (poweR_ge0 _ _))// andTb poweR_lty. +rewrite -EFinM divff ?mule1; last by + rewrite neq_lt fine_gt0 ?orbT// lt_neqAle poweR_ge0 andbT eq_sym poweR_eq0 ?Lnorm_ge0// neq_lt (lt_trans _ p1)// orbT andbT Nfg0 andTb poweR_lty. +by rewrite ?fineK// fin_numElt (@lt_le_trans _ _ 0 -oo _ _ (Lnorm_ge0 _ _ _)). +Qed. + +End minkowski. \ No newline at end of file