From bf0ab5ab8a3b23279150f5a75c5da62ec79330c0 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 14 Sep 2023 15:51:38 +0900 Subject: [PATCH] Hoelder's inequality (#942) * tentative proof of Hoelder's inequality * tentative def of ess sup * fix case p = 0 of Lnorm Co-authored-by: Alessandro Bruni --- CHANGELOG_UNRELEASED.md | 17 +++ _CoqProject | 1 + theories/Make | 1 + theories/constructive_ereal.v | 8 ++ theories/ereal.v | 31 ++++- theories/hoelder.v | 232 ++++++++++++++++++++++++++++++++++ theories/lebesgue_measure.v | 6 + theories/measure.v | 20 +++ 8 files changed, 314 insertions(+), 2 deletions(-) create mode 100644 theories/hoelder.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 604eb9d08..cc6e632c5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/_CoqProject b/_CoqProject index 194be550b..9521968f4 100644 --- a/_CoqProject +++ b/_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 diff --git a/theories/Make b/theories/Make index eb5a1f241..cd6285c45 100644 --- a/theories/Make +++ b/theories/Make @@ -28,6 +28,7 @@ derive.v measure.v numfun.v lebesgue_integral.v +hoelder.v probability.v summability.v signed.v diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 606f350d7..073d5ff52 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -3173,6 +3173,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. diff --git a/theories/ereal.v b/theories/ereal.v index 8821c1a86..fd01f2417 100644 --- a/theories/ereal.v +++ b/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. +HB.instance Definition _ (R : numDomainType) := isPointed.Build (\bar 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. -HB.instance Definition _ (R : numDomainType) := isPointed.Build (\bar 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. diff --git a/theories/hoelder.v b/theories/hoelder.v new file mode 100644 index 000000000..895f1eae8 --- /dev/null +++ b/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 [in RHS]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. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 4fbbd3ca3..80c22682c 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1508,6 +1508,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 => /=. diff --git a/theories/measure.v b/theories/measure.v index 18dd24966..d2108b7d4 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -228,6 +228,8 @@ From HB Require Import structures. (* measurableType's with resp. display d1 and d2 *) (* *) (* m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1 *) +(* ess_sup f == essential supremum of the function f : T -> R where T is a *) +(* measurableType and R is a realType *) (* *) (******************************************************************************) @@ -4347,3 +4349,21 @@ Proof. by move=> m12 m23 A mA /m23-/(_ mA) /m12; exact. Qed. End absolute_continuity. Notation "m1 `<< m2" := (measure_dominates m1 m2). + +Section essential_supremum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> R. + +Definition ess_sup f := + ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]). + +Lemma ess_sup_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R -> + 0 <= ess_sup f. +Proof. +move=> muT f0; apply: lb_ereal_inf => _ /= [r /eqP rf <-]; rewrite leNgt. +apply/negP => r0; apply/negP : rf; rewrite gt_eqF// (_ : _ @^-1` _ = setT)//. +by apply/seteqP; split => // x _ /=; rewrite in_itv/= (lt_le_trans _ (f0 x)). +Qed. + +End essential_supremum.