Convexity of powR (math-comp#1011)

* Convexity of power function

- definition of convex_function
- lnorm and equivalence lemma
- hoelder for sums
- convexity of powR

Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -69,10 +69,24 @@
 
 - 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 `Lnorm_counting`, `hoelder2`, `convex_powR`
+
+- in `lebesgue_integral.v`:
+  + lemma `ge0_integral_count`
 
 - in `exp.v`:
   + lemma `gt0_ltr_powR`
   + lemma `powR_injective`
+- in `mathcomp_extra.v`:
+  + lemma `gerBl`
 
 ### Changed
 

classical/mathcomp_extra.v

@@ -891,3 +891,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 gerBl {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x.
+Proof. by move=> y0; rewrite ler_subl_addl ler_addr. Qed.

theories/convex.v

@@ -154,6 +154,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}.

theories/exp.v

@@ -592,6 +592,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//.
@@ -664,6 +670,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.
+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}.
 Proof.
 move=> a1 x y xy.
@@ -679,6 +691,28 @@ 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.
+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.
+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.
+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.
+by rewrite (le_trans (ger_powR _ r1)) ?powRr1 ?a0// ltW.
+Qed.
+
 Lemma ge0_ler_powR (r : R) : 0 <= r ->
   {in Num.nneg &, {homo powR ^~ r : x y / x <= y >-> x <= y}}.
 Proof.
@@ -707,6 +741,20 @@ 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.
+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.
+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.
 Proof.
 rewrite /powR mulf_eq0; have [_|xN0] := eqVneq x 0.

theories/hoelder.v

@@ -5,6 +5,7 @@ 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 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 => //=.
@@ -89,6 +90,21 @@ 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 [the measure _ _ of counting] p f).
+
+Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R ->
+  'N_p%:E [f] = (\sum_(k <oo) (`| f k | `^ p)%:E) `^ p^-1.
+Proof.
+move=> 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 +246,87 @@ 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 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 [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.
+  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 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 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.
+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 convex_powR p : 1 <= p ->
+  convex_function `[0, +oo[%classic (@powR R ^~ p).
+Proof.
+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 !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 !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 {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 ?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.
+  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 (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 +
+                            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.
+    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.
+
+End convex_powR.

theories/lebesgue_integral.v

@@ -4041,11 +4041,22 @@ 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.
 
+Lemma ge0_integral_count (a : nat -> \bar R) : (forall k, 0 <= a k) ->
+  \int[counting]_t (a t) = \sum_(k <oo) (a k).
+Proof.
+move=> 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.