diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0252e99cf6..6633f90563 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -61,6 +61,17 @@ - in `classical_sets.v`: + lemmas `properW`, `properxx` +- in `lebesgue_measure.v`: + + lemma `measurable_mulrr` + +- in `constructive_ereal.v`: + + lemma `eqe_pdivr_mull` + +- in `lebesgue_integral.v`: + + definition `L_norm`, notation `'N[mu]_p[f]` + + lemmas `L_norm_ge0`, `eq_L_norm` + + lemmas `hoelder` + ### Changed - moved from `lebesgue_measure.v` to `real_interval.v`: diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 9bff255445..a646eda0e8 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -3103,6 +3103,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/lebesgue_integral.v b/theories/lebesgue_integral.v index 3d201b8912..2829d68e2f 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4,7 +4,7 @@ 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 numfun. +Require Import esum measure lebesgue_measure numfun exp itv. (******************************************************************************) (* Lebesgue Integral *) @@ -45,6 +45,8 @@ Require Import esum measure lebesgue_measure numfun. (* m1 \x^ m2 == product measure over T1 * T2, m2 is a measure *) (* measure over T1, and m1 is a sigma finite *) (* measure over T2 *) +(* 'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 *) +(* The corresponding definition is L_norm *) (* *) (******************************************************************************) @@ -67,6 +69,13 @@ Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable"). Reserved Notation "m1 '\x' m2" (at level 40, m2 at next level). Reserved Notation "m1 '\x^' m2" (at level 40, m2 at next level). +Reserved Notation "'N[ mu ]_ p [ F ]" + (at level 5, F at level 36, mu at level 10, + format "'[' ''N[' mu ]_ p '/ ' [ F ] ']'"). +Reserved Notation "''N_' p [ F ]" (* for use as a local notation *) + (at level 5, F at level 36, + format "'[' ''N_' p '/ ' [ F ] ']'"). + #[global] Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. @@ -5344,3 +5353,238 @@ Qed. End sfinite_fubini. Arguments sfinite_Fubini {d d' X Y R} m1 m2 f. + +Section L_norm. +Context d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}). +Local Open Scope ereal_scope. + +Definition L_norm (p : R) (f : T -> R) : \bar R := + (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1. + +Local Notation "'N_ p [ f ]" := (L_norm p f). + +Lemma L_norm_ge0 (p : R) (f : T -> R) : (0 <= 'N_p[f])%E. +Proof. by rewrite /L_norm poweR_ge0. Qed. + +Lemma eq_L_norm (p : R) (f g : T -> R) : f =1 g -> 'N_p[f] = 'N_p[g]. +Proof. by move=> fg; congr L_norm; exact/funext. Qed. + +End L_norm. +#[global] +Hint Extern 0 (0 <= L_norm _ _ _) => solve [apply: L_norm_ge0] : core. + +Notation "'N[ mu ]_ p [ f ]" := (L_norm mu p f). + +Section hoelder. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. +Local Open Scope ereal_scope. + +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 integrable_powR (f : T -> R) p : (0 < p)%R -> + measurable_fun setT f -> 'N[mu]_p[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) <-. +apply/eqP; congr (_ `^ _); apply/eq_integral. +by move=> x _; rewrite gee0_abs // ?lee_fin ?powR_ge0. +Qed. + +Local Notation "'N_ p [ f ]" := (L_norm mu p f). + +Let hoelder0 (f g : T -> R) (p q : R) : + measurable_fun setT f -> measurable_fun setT g -> + (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R -> + 'N[mu]_p[f] = 0 -> + 'N[mu]_1 [(f \* g)%R] <= 'N[mu]_p [f] * 'N[mu]_q [g]. +Proof. +move=> mf mg p0 q0 pq f0; rewrite f0 mul0e. +suff: 'N_1 [(f \* g)%R] = 0%E by move=> ->. +move: f0; rewrite /L_norm; move/poweR_eq0_eq0. +rewrite /= invr1 poweRe1// => [fp|]; last first. + by apply: integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. +have {fp}f0 : ae_eq mu setT (fun x => (`|f x| `^ p)%:E) (cst 0). + apply/ae_eq_integral_abs => //=. + - apply: measurableT_comp => //; apply: measurableT_comp_powR. + exact: measurableT_comp. + - under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//. + by apply/fp/integral_ge0 => t _; rewrite lee_fin; exact: powR_ge0. +rewrite (ae_eq_integral (cst 0)%E) => [|//||//|]. +- by rewrite integral0. +- apply: measurableT_comp => //; apply: measurableT_comp_powR => //. + by apply: measurableT_comp => //; exact: measurable_funM. +- apply: filterS f0 => x /(_ I) /= [] /powR_eq0_eq0 fp0 _. + by rewrite powRr1// normrM fp0 mul0r. +Qed. + +Let normed p f x := `|f x| / fine 'N_p[f]. + +Let normed_ge0 p f x : (0 <= normed p f x)%R. +Proof. by rewrite /normed divr_ge0// fine_ge0// L_norm_ge0. Qed. + +Let measurable_normed p f : measurable_fun setT f -> + measurable_fun setT (normed p f). +Proof. +move=> mf; rewrite (_ : normed _ _ = *%R (fine ('N[mu]_p[f]))^-1 \o normr \o f). + by apply: measurableT_comp => //; exact: measurableT_comp. +by apply/funext => x /=; rewrite mulrC. +Qed. + +Let normed_expR p f x : (0 < p)%R -> + let F := normed p f in F x != 0%R -> expR (ln (F x `^ p) / p) = F x. +Proof. +move=> p0 F Fx0. +rewrite ln_powR// mulrAC divff// ?gt_eqF// mul1r. +by rewrite lnK// posrE lt_neqAle normed_ge0 eq_sym Fx0. +Qed. + +Let integral_normed f p : (0 < p)%R -> 0 < 'N_p[f] -> + mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E) -> + \int[mu]_x (normed p f x `^ p)%:E = 1. +Proof. +move=> p0 fpos ifp. +transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p[f] `^ p))%:E). + apply: eq_integral => t _. + rewrite powRM//; last by rewrite invr_ge0 fine_ge0// L_norm_ge0. + rewrite -powR_inv1; last by rewrite fine_ge0 // L_norm_ge0. + by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0. +rewrite /L_norm -poweRrM mulVf ?lt0r_neq0// poweRe1; last first. + by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. +under eq_integral do rewrite EFinM muleC. +rewrite integralZl//; apply/eqP; rewrite eqe_pdivr_mull ?mule1; last first. + rewrite gt_eqF// fine_gt0//; apply/andP; split. + apply: gt0_poweR fpos; rewrite ?invr_gt0//. + by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0. + move/integrableP: ifp => -[_]. + under eq_integral. + move=> x _; rewrite gee0_abs//; last by rewrite lee_fin powR_ge0. + over. + by []. +rewrite fineK// ge0_fin_numE//; last first. + by rewrite integral_ge0// => x _; rewrite lee_fin// powR_ge0. +move/integrableP: ifp => -[_]. +under eq_integral. + move=> x _; rewrite gee0_abs//; last by rewrite lee_fin powR_ge0. + over. +by []. +Qed. + +Lemma hoelder (f g : T -> R) (p q : R) : + measurable_fun setT f -> measurable_fun setT g -> + (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R -> + 'N[mu]_1 [(f \* g)%R] <= 'N[mu]_p [f] * 'N[mu]_q [g]. +Proof. +move=> mf mg p0 q0 pq. +have [f0|f0] := eqVneq 'N_p[f] 0%E; first exact: hoelder0. +have [g0|g0] := eqVneq 'N_q[g] 0%E. + rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC. + by under eq_L_norm do rewrite /= mulrC. +have {f0}fpos : 0 < 'N_p[f] by rewrite lt_neqAle eq_sym f0//= L_norm_ge0. +have {g0}gpos : 0 < 'N_q[g] by rewrite lt_neqAle eq_sym g0//= L_norm_ge0. +have [foo|foo] := eqVneq 'N_p[f] +oo%E; first by rewrite foo gt0_mulye ?leey. +have [goo|goo] := eqVneq 'N_q[g] +oo%E; first by rewrite goo gt0_muley ?leey. +pose F := normed p f. +pose G := normed q g. +have exp_convex x : (F x * G x <= F x `^ p / p + G x `^ q / q)%R. + have [Fx0|Fx0] := eqVneq (F x) 0%R. + by rewrite Fx0 mul0r powR0 ?gt_eqF// mul0r add0r divr_ge0 ?powR_ge0 ?ltW. + have {}Fx0 : (0 < F x)%R. + by rewrite lt_neqAle eq_sym Fx0 divr_ge0// fine_ge0// L_norm_ge0. + have [Gx0|Gx0] := eqVneq (G x) 0%R. + by rewrite Gx0 mulr0 powR0 ?gt_eqF// mul0r addr0 divr_ge0 ?powR_ge0 ?ltW. + have {}Gx0 : (0 < G x)%R. + by rewrite lt_neqAle eq_sym Gx0/= divr_ge0// fine_ge0// L_norm_ge0. + pose s x := ln ((F x) `^ p). + pose t x := ln ((G x) `^ q). + have : (expR (p^-1 * s x + q^-1 * t x) <= + p^-1 * expR (s x) + q^-1 * expR (t x))%R. + have -> : (p^-1 = 1 - q^-1)%R by rewrite -pq addrK. + have K : (q^-1 \in `[0, 1])%R. + by rewrite in_itv/= invr_ge0 (ltW q0)/= -pq ler_paddl// invr_ge0 ltW. + exact: (convex_expR (@Itv.mk _ `[0, 1] q^-1 K)%R). + rewrite expRD (mulrC _ (s x)) normed_expR ?gt_eqF// -/(F x). + rewrite (mulrC _ (t x)) normed_expR ?gt_eqF// -/(G x) => /le_trans; apply. + rewrite /s /t [X in (_ * X + _)%R](@lnK _ (F x `^ p)%R); last first. + by rewrite posrE powR_gt0. + rewrite (@lnK _ (G x `^ q)%R); last by rewrite posrE powR_gt0. + by rewrite mulrC (mulrC _ q^-1). +have -> : 'N_1[(f \* g)%R] = 'N_1[(F \* G)%R] * 'N_p[f] * 'N_q[g]. + rewrite {1}/L_norm; under eq_integral => x _ do rewrite powRr1//. + rewrite invr1 poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin. + rewrite {1}/L_norm. + under [in RHS]eq_integral. + move=> x _. + rewrite /F /G /= /normed (mulrC `|f x|)%R mulrA -(mulrA (_^-1)). + rewrite (mulrC (_^-1)) -mulrA ger0_norm; last first. + by rewrite mulr_ge0// divr_ge0 ?(fine_ge0,L_norm_ge0,invr_ge0). + rewrite powRr1; last first. + by rewrite mulr_ge0// divr_ge0 ?(fine_ge0,L_norm_ge0,invr_ge0). + 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// L_norm_ge0. + rewrite -muleA muleC invr1 poweRe1; last first. + rewrite mule_ge0//. + by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// L_norm_ge0. + by apply integral_ge0 => x _; rewrite lee_fin. + rewrite muleA EFinM. + rewrite muleCA 2!muleA (_ : _ * 'N_p[f] = 1) ?mul1e; last first. + apply/eqP; rewrite eqe_pdivr_mull ?mule1; last first. + by rewrite gt_eqF// fine_gt0// fpos/= ltey. + by rewrite fineK// ?ge0_fin_numE ?ltey// L_norm_ge0. + rewrite (_ : 'N_q[g] * _ = 1) ?mul1e// muleC. + apply/eqP; rewrite eqe_pdivr_mull ?mule1; last first. + by rewrite gt_eqF// fine_gt0// gpos/= ltey. + by rewrite fineK// ?ge0_fin_numE ?ltey// L_norm_ge0. +rewrite -(mul1e ('N_p[f] * _)) -muleA lee_pmul ?mule_ge0 ?L_norm_ge0//. +apply: (@le_trans _ _ (\int[mu]_x (F x `^ p / p + G x `^ q / q)%:E)). + rewrite /L_norm invr1 poweRe1; last first. + by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. + apply: ae_ge0_le_integral => //. + - by move=> x _; exact: powR_ge0. + - apply: measurableT_comp => //; apply: measurableT_comp_powR => //. + apply: measurableT_comp => //. + by apply: measurable_funM => //; exact: measurable_normed. + - 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_normed. + apply/aeW => x _. + by rewrite lee_fin powRr1// ger0_norm ?exp_convex// mulr_ge0// normed_ge0. +rewrite le_eqVlt; apply/orP; left; apply/eqP. +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_normed. +- 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_normed. +under eq_integral do rewrite EFinM. +rewrite {1}ge0_integralZl//; last 3 first. +- apply: measurableT_comp => //. + by apply: measurableT_comp_powR => //; exact: measurable_normed. +- 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_normed. +- by move=> x _; rewrite lee_fin powR_ge0. +- by rewrite lee_fin invr_ge0 ltW. +rewrite integral_normed//; last exact: integrable_powR. +rewrite integral_normed//; 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 dd0b3aed16..dc14e81575 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1487,6 +1487,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 => /=.