Minkowski's inequality and accessory lemmas

Co-authored-by: @affeldt-aist

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

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.

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.
+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.