Hoelder's inequality (math-comp#942)

* tentative proof of Hoelder's inequality

* tentative def of ess sup

* fix case p = 0 of Lnorm

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

CHANGELOG_UNRELEASED.md

@@ -40,6 +40,17 @@
   + new definition `regular_space`.
   + new lemma `ent_closure`.
 
+- 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`
@@ -52,6 +63,12 @@
 
 - in `constructive_ereal.v`:
   + lemma `bigmaxe_fin_num`
+- in `ereal.v`:
+  + lemmas `uboundT`, `supremumsT`, `supremumT`, `ereal_supT`, `range_oppe`,
+    `ereal_infT`
+
+- in `measure.v`:
+  + definition `ess_sup`, lemma `ess_sup_ge0`
 
 ### Changed
 

_CoqProject

@@ -37,6 +37,7 @@ theories/derive.v
 theories/measure.v
 theories/numfun.v
 theories/lebesgue_integral.v
+theories/hoelder.v
 theories/probability.v
 theories/summability.v
 theories/signed.v

theories/Make

@@ -28,6 +28,7 @@ derive.v
 measure.v
 numfun.v
 lebesgue_integral.v
+hoelder.v
 probability.v
 summability.v
 signed.v

theories/constructive_ereal.v

@@ -3139,6 +3139,14 @@ Qed.
 Lemma lee_ndivr_mulr r x y : (r < 0)%R -> (y * r^-1%:E <= x) = (x * r%:E <= y).
 Proof. by move=> r0; rewrite muleC lee_ndivr_mull// muleC. Qed.
 
+Lemma eqe_pdivr_mull r x y : (r != 0)%R ->
+  ((r^-1)%:E * y == x) = (y == r%:E * x).
+Proof.
+rewrite neq_lt => /orP[|] r0.
+- by rewrite eq_le lee_ndivr_mull// lee_ndivl_mull// -eq_le.
+- by rewrite eq_le lee_pdivr_mull// lee_pdivl_mull// -eq_le.
+Qed.
+
 End realFieldType_lemmas.
 
 Module DualAddTheoryRealField.

theories/ereal.v

@@ -127,6 +127,9 @@ Section ERealArithTh_numDomainType.
 Context {R : numDomainType}.
 Implicit Types (x y z : \bar R) (r : R).
 
+Lemma range_oppe : range -%E = [set: \bar R]%classic.
+Proof. by apply/seteqP; split => [//|x] _; exists (- x); rewrite ?oppeK. Qed.
+
 Lemma oppe_subset (A B : set (\bar R)) :
   ((A `<=` B) <-> (-%E @` A `<=` -%E @` B))%classic.
 Proof.
@@ -336,11 +339,19 @@ Export ConstructiveDualAddTheory.
 Export DualAddTheoryNumDomain.
 End DualAddTheory.
 
+Canonical ereal_pointed (R : numDomainType) := PointedType (extended R) 0%E.
+
 Section ereal_supremum.
 Variable R : realFieldType.
 Local Open Scope classical_set_scope.
 Implicit Types (S : set (\bar R)) (x y : \bar R).
 
+Lemma uboundT : ubound [set: \bar R] = [set +oo].
+Proof.
+apply/seteqP; split => /= [x Tx|x -> ?]; last by rewrite leey.
+by apply/eqP; rewrite eq_le leey /= Tx.
+Qed.
+
 Lemma ereal_ub_pinfty S : ubound S +oo.
 Proof. by apply/ubP=> x _; rewrite leey. Qed.
 
@@ -352,9 +363,21 @@ right; rewrite predeqE => y; split => [/Snoo|->{y}].
 by have := Snoo _ Sx; rewrite leeNy_eq => /eqP <-.
 Qed.
 
+Lemma supremumsT : supremums [set: \bar R] = [set +oo].
+Proof.
+rewrite /supremums uboundT.
+by apply/seteqP; split=> [x []//|x -> /=]; split => // y ->.
+Qed.
+
 Lemma ereal_supremums_set0_ninfty : supremums (@set0 (\bar R)) -oo.
 Proof. by split; [exact/ubP | apply/lbP=> y _; rewrite leNye]. Qed.
 
+Lemma supremumT : supremum -oo [set: \bar R] = +oo.
+Proof.
+rewrite /supremum (negbTE setT0) supremumsT.
+by case: xgetP => // /(_ +oo)/= /eqP; rewrite eqxx.
+Qed.
+
 Lemma supremum_pinfty S x0 : S +oo -> supremum x0 S = +oo.
 Proof.
 move=> Spoo; rewrite /supremum ifF; last by apply/eqP => S0; rewrite S0 in Spoo.
@@ -372,11 +395,17 @@ Definition ereal_inf S := - ereal_sup (-%E @` S).
 
 Lemma ereal_sup0 : ereal_sup set0 = -oo. Proof. exact: supremum0. Qed.
 
+Lemma ereal_supT : ereal_sup [set: \bar R] = +oo.
+Proof. by rewrite /ereal_sup/= supremumT. Qed.
+
 Lemma ereal_sup1 x : ereal_sup [set x] = x. Proof. exact: supremum1. Qed.
 
 Lemma ereal_inf0 : ereal_inf set0 = +oo.
 Proof. by rewrite /ereal_inf image_set0 ereal_sup0. Qed.
 
+Lemma ereal_infT : ereal_inf [set: \bar R] = -oo.
+Proof. by rewrite /ereal_inf range_oppe/= ereal_supT. Qed.
+
 Lemma ereal_inf1 x : ereal_inf [set x] = x.
 Proof. by rewrite /ereal_inf image_set1 ereal_sup1 oppeK. Qed.
 
@@ -533,8 +562,6 @@ Qed.
 
 End ereal_supremum_realType.
 
-Canonical ereal_pointed (R : numDomainType) := PointedType (extended R) 0%E.
-
 Lemma restrict_abse T (R : numDomainType) (f : T -> \bar R) (D : set T) :
   (abse \o f) \_ D = abse \o (f \_ D).
 Proof.

theories/hoelder.v

@@ -0,0 +1,232 @@
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+From HB Require Import structures.
+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.
+
+(******************************************************************************)
+(*                         Hoelder's Inequality                               *)
+(*                                                                            *)
+(* This file provides Hoelder's inequality.                                   *)
+(*                                                                            *)
+(*           'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1             *)
+(*                          The corresponding definition is Lnorm.            *)
+(*                                                                            *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+Import numFieldTopology.Exports.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Reserved Notation "'N[ mu ]_ p [ F ]"
+  (at level 5, F at level 36, mu at level 10,
+  format "'[' ''N[' mu ]_ p '/  ' [ F ] ']'").
+(* for use as a local notation when the measure is in context: *)
+Reserved Notation "'N_ p [ F ]"
+  (at level 5, F at level 36, format "'[' ''N_' p '/  ' [ F ] ']'").
+
+Declare Scope Lnorm_scope.
+
+Local Open Scope ereal_scope.
+
+Section Lnorm.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Local Open Scope ereal_scope.
+Implicit Types (p : \bar R) (f g : T -> R) (r : R).
+
+Definition Lnorm p f :=
+  match p with
+  | p%:E => if p == 0%R then
+              mu (f @^-1` (setT `\ 0%R))
+            else
+              (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1
+  | +oo => if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0
+  | -oo => 0
+  end.
+
+Local Notation "'N_ p [ f ]" := (Lnorm p f).
+
+Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E.
+Proof.
+rewrite /Lnorm oner_eq0 invr1// poweRe1//.
+  by apply: eq_integral => t _; rewrite powRr1.
+by apply: integral_ge0 => t _; rewrite powRr1.
+Qed.
+
+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 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).
+Proof.
+move=> r0 mf/=; rewrite (gt_eqF r0) => /poweR_eq0_eq0 fp.
+apply/ae_eq_integral_abs => //=.
+  apply: measurableT_comp => //.
+  apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //.
+  exact: measurableT_comp.
+under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//.
+by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0.
+Qed.
+
+End Lnorm.
+#[global]
+Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core.
+
+Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f).
+
+Section hoelder.
+Context d {T : measurableType d} {R : realType}.
+Variable mu : {measure set T -> \bar R}.
+Local Open Scope ereal_scope.
+Implicit Types (p q : R) (f g : T -> R).
+
+Let measurableT_comp_powR f p :
+  measurable_fun [set: T] f -> measurable_fun setT (fun x => f x `^ p)%R.
+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 ->
+  measurable_fun [set: T] f -> 'N_p%:E[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) <-.
+rewrite /= (gt_eqF p0); apply/eqP; congr (_ `^ _).
+by apply/eq_integral => t _; rewrite ger0_norm// powR_ge0.
+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 ->
+  'N_p%:E[f] = 0 -> 'N_1[(f \* g)%R]  <= 'N_p%:E[f] * 'N_q%:E[g].
+Proof.
+move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//.
+rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0.
+- apply: measurableT_comp => //; apply: measurableT_comp => //.
+  exact: measurable_funM.
+- have := Lnorm_eq0_eq0 p0 mf f0.
+  apply: filterS => x /(_ I) /= [] /powR_eq0_eq0 + _.
+  by rewrite normrM => ->; rewrite mul0r.
+Qed.
+
+Let normalized p f x := `|f x| / fine 'N_p%:E[f].
+
+Let normalized_ge0 p f x : (0 <= normalized p f x)%R.
+Proof. by rewrite /normalized divr_ge0// fine_ge0// Lnorm_ge0. Qed.
+
+Let measurable_normalized p f : measurable_fun [set: T] f ->
+  measurable_fun [set: T] (normalized p f).
+Proof. by move=> mf; apply: measurable_funM => //; exact: measurableT_comp. Qed.
+
+Let integral_normalized f p : (0 < p)%R -> 0 < 'N_p%:E[f] ->
+  mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E) ->
+  \int[mu]_x (normalized p f x `^ p)%:E = 1.
+Proof.
+move=> p0 fpos ifp.
+transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p%:E[f] `^ p))%:E).
+  apply: eq_integral => t _.
+  rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0.
+  rewrite -[in LHS]powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0.
+  by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0.
+have fp0 : 0 < \int[mu]_x (`|f x| `^ p)%:E.
+  rewrite /= (gt_eqF p0) in fpos.
+  apply: gt0_poweR fpos; rewrite ?invr_gt0//.
+  by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0.
+rewrite /Lnorm (gt_eqF p0) -poweRrM mulVf ?lt0r_neq0// poweRe1//; last exact: ltW.
+under eq_integral do rewrite EFinM muleC.
+have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo.
+  move/integrableP: ifp => -[_].
+  by under eq_integral do rewrite gee0_abs// ?lee_fin ?powR_ge0//.
+rewrite integralZl//; apply/eqP; rewrite eqe_pdivr_mull ?mule1.
+- by rewrite fineK// ge0_fin_numE// ltW.
+- by rewrite gt_eqF// fine_gt0// foo andbT.
+Qed.
+
+Lemma hoelder f g p q : measurable_fun setT f -> measurable_fun setT g ->
+  (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R ->
+ 'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g].
+Proof.
+move=> mf mg p0 q0 pq.
+have [f0|f0] := eqVneq 'N_p%:E[f] 0%E; first exact: hoelder0.
+have [g0|g0] := eqVneq 'N_q%:E[g] 0%E.
+  rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC.
+  by under eq_Lnorm do rewrite /= mulrC.
+have {f0}fpos : 0 < 'N_p%:E[f] by rewrite lt_neqAle eq_sym f0// Lnorm_ge0.
+have {g0}gpos : 0 < 'N_q%:E[g] by rewrite lt_neqAle eq_sym g0// Lnorm_ge0.
+have [foo|foo] := eqVneq 'N_p%:E[f] +oo%E; first by rewrite foo gt0_mulye ?leey.
+have [goo|goo] := eqVneq 'N_q%:E[g] +oo%E; first by rewrite goo gt0_muley ?leey.
+pose F := normalized p f; pose G := normalized q g.
+rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]); last first.
+  rewrite !Lnorm1.
+  under [in RHS]eq_integral.
+    move=> x _.
+    rewrite /F /G /= /normalized (mulrC `|f x|)%R mulrA -(mulrA (_^-1)).
+    rewrite (mulrC (_^-1)) -mulrA ger0_norm; last first.
+      by rewrite mulr_ge0// divr_ge0 ?(fine_ge0, Lnorm_ge0, invr_ge0).
+    by 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//Lnorm_ge0.
+  rewrite -muleA muleC muleA EFinM muleCA 2!muleA.
+  rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e; last first.
+    rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
+    by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// fpos/= ltey.
+  rewrite (_ : 'N_q%:E[g] * _ = 1) ?mul1e// muleC.
+  rewrite -[X in _ * X]fineK; last by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
+  by rewrite -EFinM mulVr ?unitfE ?gt_eqF// fine_gt0// gpos/= ltey.
+rewrite -(mul1e ('N_p%:E[f] * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//.
+rewrite [leRHS](_ : _ = \int[mu]_x (F x `^ p / p + G x `^ q / q)%:E).
+  rewrite Lnorm1 ae_ge0_le_integral //.
+  - apply: measurableT_comp => //; apply: measurableT_comp => //.
+    by apply: measurable_funM => //; exact: measurable_normalized.
+  - 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_normalized.
+  apply/aeW => x _; rewrite lee_fin ger0_norm ?conjugate_powR ?normalized_ge0//.
+  by rewrite mulr_ge0// normalized_ge0.
+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_normalized.
+- 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_normalized.
+under eq_integral do rewrite EFinM.
+rewrite {1}ge0_integralZl//; last 3 first.
+- apply: measurableT_comp => //.
+  by apply: measurableT_comp_powR => //; exact: measurable_normalized.
+- 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_normalized.
+- by move=> x _; rewrite lee_fin powR_ge0.
+- by rewrite lee_fin invr_ge0 ltW.
+rewrite integral_normalized//; last exact: integrable_powR.
+rewrite integral_normalized//; last exact: integrable_powR.
+by rewrite 2!mule1 -EFinD pq.
+Qed.
+
+End hoelder.

theories/lebesgue_measure.v

@@ -1503,6 +1503,12 @@ apply: measurable_funTS => /=.
 by apply: continuous_measurable_fun; exact: mulrl_continuous.
 Qed.
 
+Lemma measurable_mulrr D (k : R) : measurable_fun D (fun x => x * k).
+Proof.
+apply: measurable_funTS => /=.
+by apply: continuous_measurable_fun; exact: mulrr_continuous.
+Qed.
+
 Lemma measurable_exprn D n : measurable_fun D (fun x => x ^+ n).
 Proof.
 apply measurable_funTS => /=.