From 0f422af23969b3142a7791a513d0bc8e1acb1ccc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 3 Jun 2023 23:58:04 +0900 Subject: [PATCH 01/13] tentative proof of Hoelder's inequality Co-authored-by: Alessandro Bruni --- CHANGELOG_UNRELEASED.md | 68 ++++++++++ theories/constructive_ereal.v | 8 ++ theories/lebesgue_integral.v | 246 +++++++++++++++++++++++++++++++++- theories/lebesgue_measure.v | 6 + 4 files changed, 327 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 604eb9d08..47db4011e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -22,6 +22,74 @@ - in `exp.v`: + lemmas `concave_ln`, `conjugate_powR` + + lemma `concave_ln` +- in `lebesgue_measure.v`: + + lemma `closed_measurable` + +- in file `lebesgue_measure.v`, + + new lemmas `lebesgue_nearly_bounded`, and `lebesgue_regularity_inner`. +- in file `measure.v`, + + new lemmas `measureU0`, `nonincreasing_cvg_mu`, and `epsilon_trick0`. +- in file `real_interval.v`, + + new lemma `bigcup_itvT`. +- in file `topology.v`, + + new lemma `uniform_nbhsT`. + +- in file `topology.v`, + + new definition `set_nbhs`. + + new lemmas `filterI_iter_sub`, `filterI_iterE`, `finI_fromI`, + `filterI_iter_finI`, `smallest_filter_finI`, and `set_nbhsP`. + +- in file `lebesgue_measure.v`, + + new lemmas `pointwise_almost_uniform`, and + `ae_pointwise_almost_uniform`. + +- in `exp.v`: + + lemmas `powRrM`, `gt0_ler_powR`, + `gt0_powR`, `norm_powR`, `lt0_norm_powR`, + `powRB` + + lemmas `poweRrM`, `poweRAC`, `gt0_poweR`, + `poweR_eqy`, `eqy_poweR`, `poweRD`, `poweRB` + +- in `mathcomp_extra.v`: + + definition `min_fun`, notation `\min` +- in `classical_sets.v`: + + lemmas `set_predC`, `preimage_true`, `preimage_false` +- in `lebesgue_measure.v`: + + lemmas `measurable_fun_ltr`, `measurable_minr` +- in file `lebesgue_integral.v`, + + new lemmas `lusin_simple`, and `measurable_almost_continuous`. +- in file `measure.v`, + + new lemmas `finite_card_sum`, and `measureU2`. + +- in `topology.v`: + + lemma `bigsetU_compact` + +- in `exp.v`: + + notation `` e `^?(r +? s) `` + + lemmas `expR_eq0`, `powRN` + + definition `poweRD_def` + + lemmas `poweRD_defE`, `poweRB_defE`, `add_neq0_poweRD_def`, + `add_neq0_poweRB_def`, `nneg_neq0_poweRD_def`, `nneg_neq0_poweRB_def` + + lemmas `powR_eq0`, `poweR_eq0` +- in file `lebesgue_integral.v`, + + new lemma `approximation_sfun_integrable`. + +- in `classical_sets.v`: + + lemmas `properW`, `properxx` + +- in `classical_sets.v`: + + lemma `Zorn_bigcup` +- 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` - in file `lebesgue_integral.v`, + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 96a8b5c6a..c4d6c2a05 100644 --- a/theories/constructive_ereal.v +++ b/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. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index ff4ab41cf..7ed33ae19 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. @@ -5621,3 +5630,238 @@ by rewrite ritv //= -EFinM lee_fin mulrC. Unshelve. all: by end_near. Qed. End lebesgue_differentiation. + +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 15710aa79..714117b0c 100644 --- a/theories/lebesgue_measure.v +++ b/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 => /=. From 630854e2bb3640beb1573a6dfbd2926e44b14412 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 8 Aug 2023 14:44:43 +0900 Subject: [PATCH 02/13] extract lemma, test notation (cont'd) --- CHANGELOG_UNRELEASED.md | 59 +---------- theories/lebesgue_integral.v | 196 +++++++++++++++++++---------------- theories/topology.v | 2 +- 3 files changed, 110 insertions(+), 147 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 47db4011e..4d887265b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -26,60 +26,7 @@ - in `lebesgue_measure.v`: + lemma `closed_measurable` -- in file `lebesgue_measure.v`, - + new lemmas `lebesgue_nearly_bounded`, and `lebesgue_regularity_inner`. -- in file `measure.v`, - + new lemmas `measureU0`, `nonincreasing_cvg_mu`, and `epsilon_trick0`. -- in file `real_interval.v`, - + new lemma `bigcup_itvT`. -- in file `topology.v`, - + new lemma `uniform_nbhsT`. - -- in file `topology.v`, - + new definition `set_nbhs`. - + new lemmas `filterI_iter_sub`, `filterI_iterE`, `finI_fromI`, - `filterI_iter_finI`, `smallest_filter_finI`, and `set_nbhsP`. - -- in file `lebesgue_measure.v`, - + new lemmas `pointwise_almost_uniform`, and - `ae_pointwise_almost_uniform`. - -- in `exp.v`: - + lemmas `powRrM`, `gt0_ler_powR`, - `gt0_powR`, `norm_powR`, `lt0_norm_powR`, - `powRB` - + lemmas `poweRrM`, `poweRAC`, `gt0_poweR`, - `poweR_eqy`, `eqy_poweR`, `poweRD`, `poweRB` - -- in `mathcomp_extra.v`: - + definition `min_fun`, notation `\min` -- in `classical_sets.v`: - + lemmas `set_predC`, `preimage_true`, `preimage_false` -- in `lebesgue_measure.v`: - + lemmas `measurable_fun_ltr`, `measurable_minr` -- in file `lebesgue_integral.v`, - + new lemmas `lusin_simple`, and `measurable_almost_continuous`. -- in file `measure.v`, - + new lemmas `finite_card_sum`, and `measureU2`. - -- in `topology.v`: - + lemma `bigsetU_compact` -- in `exp.v`: - + notation `` e `^?(r +? s) `` - + lemmas `expR_eq0`, `powRN` - + definition `poweRD_def` - + lemmas `poweRD_defE`, `poweRB_defE`, `add_neq0_poweRD_def`, - `add_neq0_poweRB_def`, `nneg_neq0_poweRD_def`, `nneg_neq0_poweRB_def` - + lemmas `powR_eq0`, `poweR_eq0` -- in file `lebesgue_integral.v`, - + new lemma `approximation_sfun_integrable`. - -- in `classical_sets.v`: - + lemmas `properW`, `properxx` - -- in `classical_sets.v`: - + lemma `Zorn_bigcup` - in `lebesgue_measure.v`: + lemma `measurable_mulrr` @@ -87,9 +34,9 @@ + 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` + + definition `Lnorm`, notations `'N[mu]_p[f]`, `` `| f |_p `` + + lemmas `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0` + + lemma `hoelder` - in file `lebesgue_integral.v`, + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 7ed33ae19..0266f4f6d 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -46,7 +46,7 @@ Require Import esum measure lebesgue_measure numfun exp itv. (* 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 *) +(* The corresponding definition is Lnorm. *) (* *) (******************************************************************************) @@ -5636,34 +5636,55 @@ 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. +Implicit Types (p : R) (f g : T -> R). -Local Notation "'N_ p [ f ]" := (L_norm p f). +Definition Lnorm p f := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1. -Lemma L_norm_ge0 (p : R) (f : T -> R) : (0 <= 'N_p[f])%E. -Proof. by rewrite /L_norm poweR_ge0. Qed. +Local Notation "`| f |_ p" := (Lnorm p f). -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. +Lemma Lnorm1 p f : `| f |_1 = \int[mu]_x `|f x|%:E. +Proof. +rewrite /Lnorm invr1// poweRe1//; last first. + by apply: integral_ge0 => t _; rewrite powRr1. +by apply: eq_integral => t _; rewrite powRr1. +Qed. + +Lemma Lnorm_ge0 p f : 0 <= `| f |_p. Proof. exact: poweR_ge0. Qed. + +Lemma eq_Lnorm p f g : f =1 g -> `|f|_p = `|g|_p. +Proof. by move=> fg; congr Lnorm; exact/funext. Qed. -End L_norm. +Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> `| f |_p = 0 -> + ae_eq mu [set: T] (fun x : T => (`|f x| `^ p)%:E) (cst 0). +Proof. +move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. + apply: measurableT_comp => //. + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. + 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. +Qed. + +End Lnorm. #[global] -Hint Extern 0 (0 <= L_norm _ _ _) => solve [apply: L_norm_ge0] : core. +Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core. -Notation "'N[ mu ]_ p [ f ]" := (L_norm mu p f). +Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f). Section hoelder. -Context d (T : measurableType d) (R : realType). +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 : T -> R) p : +Let measurableT_comp_powR f 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 -> +Local Notation "`| f |_ p" := (Lnorm mu p f). + +Let integrable_powR f p : (0 < p)%R -> + measurable_fun [set: T] f -> `| f |_p != +oo -> mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E). Proof. move=> p0 mf foo; apply/integrableP; split. @@ -5675,42 +5696,33 @@ 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 -> +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[mu]_p[f] = 0 -> - 'N[mu]_1 [(f \* g)%R] <= 'N[mu]_p [f] * 'N[mu]_q [g]. + `| f |_ p = 0 -> `| (f \* g)%R |_1 <= `| f |_p * `| g |_ q. 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. +suff: `| (f \* g)%R |_1 = 0 by move=> ->. +rewrite /Lnorm /= invr1 poweRe1; 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) => [|//||//|]. +rewrite (ae_eq_integral (cst 0)) => [|//||//|]. - 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 _. +- have : ae_eq mu setT (fun x => (`|f x| `^ p)%:E) (cst 0). + exact: Lnorm_eq0_eq0. + apply: filterS => 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 p f x := `|f x| / fine `|f|_p. Let normed_ge0 p f x : (0 <= normed p f x)%R. -Proof. by rewrite /normed divr_ge0// fine_ge0// L_norm_ge0. Qed. +Proof. by rewrite /normed divr_ge0// fine_ge0// Lnorm_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). +move=> mf; rewrite (_ : normed _ _ = *%R (fine (`|f|_p))^-1 \o normr \o f). by apply: measurableT_comp => //; exact: measurableT_comp. by apply/funext => x /=; rewrite mulrC. Qed. @@ -5718,22 +5730,21 @@ 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. +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] -> +Let integral_normed f p : (0 < p)%R -> 0 < `|f|_p -> 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). +transitivity (\int[mu]_x (`|f x| `^ p / fine (`|f|_p `^ 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. + rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0. + rewrite -powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0. by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0. -rewrite /L_norm -poweRrM mulVf ?lt0r_neq0// poweRe1; last first. +rewrite /Lnorm -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. @@ -5754,78 +5765,83 @@ under eq_integral. by []. Qed. -Lemma hoelder (f g : T -> R) (p q : R) : - measurable_fun setT f -> measurable_fun setT g -> +Let normed_convex f g p q x : (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1)%R = 1%R -> + (normed p f x * normed q g x <= + normed p f x `^ p / p + normed q g x `^ q / q)%R. +Proof. +move=> p0 q0 pq; set F := normed p f; set G := normed q g. +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// Lnorm_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// Lnorm_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). +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[mu]_1 [(f \* g)%R] <= 'N[mu]_p [f] * 'N[mu]_q [g]. + `| (f \* g)%R |_1 <= `| f |_p * `| g |_q. 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. +have [f0|f0] := eqVneq `|f|_p 0%E; first exact: hoelder0. +have [g0|g0] := eqVneq `|g|_q 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. + by under eq_Lnorm do rewrite /= mulrC. +have {f0}fpos : 0 < `|f|_p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. +have {g0}gpos : 0 < `|g|_q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0. +have [foo|foo] := eqVneq `|f|_p +oo%E; first by rewrite foo gt0_mulye ?leey. +have [goo|goo] := eqVneq `|g|_q +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//. +have -> : `| (f \* g)%R |_1 = `| (F \* G)%R |_1 * `| f |_p * `| g |_q. + rewrite {1}/Lnorm; under eq_integral => x _ do rewrite powRr1//. rewrite invr1 poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin. - rewrite {1}/L_norm. + rewrite {1}/Lnorm. 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). + by rewrite mulr_ge0// divr_ge0 ?(fine_ge0, Lnorm_ge0, invr_ge0). rewrite powRr1; last first. - by rewrite mulr_ge0// divr_ge0 ?(fine_ge0,L_norm_ge0,invr_ge0). + by rewrite mulr_ge0// divr_ge0 ?(fine_ge0, Lnorm_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. + - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_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 rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0. by apply integral_ge0 => x _; rewrite lee_fin. rewrite muleA EFinM. - rewrite muleCA 2!muleA (_ : _ * 'N_p[f] = 1) ?mul1e; last first. + rewrite muleCA 2!muleA (_ : _ * `|f|_p = 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. + by rewrite fineK// ?ge0_fin_numE ?ltey// Lnorm_ge0. + rewrite (_ : `|g|_q * _ = 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//. + by rewrite fineK// ?ge0_fin_numE ?ltey// Lnorm_ge0. +rewrite -(mul1e (`|f|_p * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//. apply: (@le_trans _ _ (\int[mu]_x (F x `^ p / p + G x `^ q / q)%:E)). - rewrite /L_norm invr1 poweRe1; last first. + rewrite /Lnorm 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. @@ -5836,8 +5852,8 @@ apply: (@le_trans _ _ (\int[mu]_x (F x `^ p / p + G x `^ q / q)%:E)). - 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. + apply/aeW => x _; rewrite lee_fin powRr1// ger0_norm ?normed_convex//. + by rewrite 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. diff --git a/theories/topology.v b/theories/topology.v index 13cb683a0..8b765e829 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -4112,7 +4112,7 @@ Canonical topologicalType. Notation uniformType := type. Notation UniformType T m := (@pack T _ m _ _ idfun _ idfun). Notation UniformMixin := Mixin. -Notation "[ 'uniformType' 'of' T 'for' cT ]" := (@clone T cT _ idfun) +Notation "[ 'uniformType' 'of' T 'for' cT ]" := (@clone T cT _ idfun) (at level 0, format "[ 'uniformType' 'of' T 'for' cT ]") : form_scope. Notation "[ 'uniformType' 'of' T ]" := (@clone T _ _ id) (at level 0, format "[ 'uniformType' 'of' T ]") : form_scope. From 397097665783022addc76f0504c75c0ade52778f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 9 Aug 2023 21:58:59 +0900 Subject: [PATCH 03/13] finish address comments --- CHANGELOG_UNRELEASED.md | 5 +- theories/lebesgue_integral.v | 184 +++++++++++------------------------ 2 files changed, 58 insertions(+), 131 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4d887265b..a59d4ff6c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -22,9 +22,6 @@ - in `exp.v`: + lemmas `concave_ln`, `conjugate_powR` - + lemma `concave_ln` -- in `lebesgue_measure.v`: - + lemma `closed_measurable` - in `lebesgue_measure.v`: @@ -35,7 +32,7 @@ - in `lebesgue_integral.v`: + definition `Lnorm`, notations `'N[mu]_p[f]`, `` `| f |_p `` - + lemmas `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0` + + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0` + lemma `hoelder` - in file `lebesgue_integral.v`, diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 0266f4f6d..453b8a7eb 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -5642,11 +5642,11 @@ Definition Lnorm p f := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1. Local Notation "`| f |_ p" := (Lnorm p f). -Lemma Lnorm1 p f : `| f |_1 = \int[mu]_x `|f x|%:E. +Lemma Lnorm1 f : `| f |_1 = \int[mu]_x `|f x|%:E. Proof. -rewrite /Lnorm invr1// poweRe1//; last first. - by apply: integral_ge0 => t _; rewrite powRr1. -by apply: eq_integral => t _; rewrite powRr1. +rewrite /Lnorm invr1// poweRe1//. + by apply: eq_integral => t _; rewrite powRr1. +by apply: integral_ge0 => t _; rewrite powRr1. Qed. Lemma Lnorm_ge0 p f : 0 <= `| f |_p. Proof. exact: poweR_ge0. Qed. @@ -5655,14 +5655,14 @@ Lemma eq_Lnorm p f g : f =1 g -> `|f|_p = `|g|_p. Proof. by move=> fg; congr Lnorm; exact/funext. Qed. Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> `| f |_p = 0 -> - ae_eq mu [set: T] (fun x : T => (`|f x| `^ p)%:E) (cst 0). + ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0). Proof. move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. apply: measurableT_comp => //. apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. 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. +by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0. Qed. End Lnorm. @@ -5678,7 +5678,7 @@ Local Open Scope ereal_scope. Implicit Types (p q : R) (f g : T -> R). Let measurableT_comp_powR f p : - measurable_fun setT f -> measurable_fun setT (fun x => f x `^ p)%R. + measurable_fun [set: T] f -> measurable_fun setT (fun x => f x `^ p)%R. Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed. Local Notation "`| f |_ p" := (Lnorm mu p f). @@ -5692,51 +5692,35 @@ move=> p0 mf foo; apply/integrableP; split. 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. +apply/eqP; congr (_ `^ _). +by apply/eq_integral => t _; rewrite gee0_abs// ?lee_fin ?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 -> - `| f |_ p = 0 -> `| (f \* g)%R |_1 <= `| f |_p * `| g |_ q. + `| f |_ p = 0 -> `| (f \* g)%R |_1 <= `| f |_p * `| g |_q. Proof. -move=> mf mg p0 q0 pq f0; rewrite f0 mul0e. -suff: `| (f \* g)%R |_1 = 0 by move=> ->. -rewrite /Lnorm /= invr1 poweRe1; last first. - by apply: integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. -rewrite (ae_eq_integral (cst 0)) => [|//||//|]. -- by rewrite integral0. -- apply: measurableT_comp => //; apply: measurableT_comp_powR => //. - by apply: measurableT_comp => //; exact: measurable_funM. -- have : ae_eq mu setT (fun x => (`|f x| `^ p)%:E) (cst 0). - exact: Lnorm_eq0_eq0. - apply: filterS => x /(_ I) /= [] /powR_eq0_eq0 fp0 _. - by rewrite powRr1// normrM fp0 mul0r. +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 mf f0. + apply: filterS => x /(_ I) /= [] /powR_eq0_eq0 + _. + by rewrite normrM => ->; rewrite mul0r. Qed. -Let normed p f x := `|f x| / fine `|f|_p. +Let normalized p f x := `|f x| / fine `|f|_p. -Let normed_ge0 p f x : (0 <= normed p f x)%R. -Proof. by rewrite /normed divr_ge0// fine_ge0// Lnorm_ge0. Qed. +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_normed p f : measurable_fun setT f -> - measurable_fun setT (normed p f). -Proof. -move=> mf; rewrite (_ : normed _ _ = *%R (fine (`|f|_p))^-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 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_normed f p : (0 < p)%R -> 0 < `|f|_p -> +Let integral_normalized f p : (0 < p)%R -> 0 < `|f|_p -> mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E) -> - \int[mu]_x (normed p f x `^ p)%:E = 1. + \int[mu]_x (normalized p f x `^ p)%:E = 1. Proof. move=> p0 fpos ifp. transitivity (\int[mu]_x (`|f x| `^ p / fine (`|f|_p `^ p))%:E). @@ -5744,54 +5728,17 @@ transitivity (\int[mu]_x (`|f x| `^ p / fine (`|f|_p `^ p))%:E). rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0. rewrite -powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0. by rewrite fine_poweR powRAC -powR_inv1 // powR_ge0. -rewrite /Lnorm -poweRrM mulVf ?lt0r_neq0// poweRe1; last first. +have fp0 : 0 < \int[mu]_x (`|f x| `^ p)%:E. + apply: gt0_poweR fpos; rewrite ?invr_gt0//. by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. +rewrite /Lnorm -poweRrM mulVf ?lt0r_neq0// poweRe1//; last exact: ltW. 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. +have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo. 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. - -Let normed_convex f g p q x : (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1)%R = 1%R -> - (normed p f x * normed q g x <= - normed p f x `^ p / p + normed q g x `^ q / q)%R. -Proof. -move=> p0 q0 pq; set F := normed p f; set G := normed q g. -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// Lnorm_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// Lnorm_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). + 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 -> @@ -5807,76 +5754,59 @@ have {f0}fpos : 0 < `|f|_p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. have {g0}gpos : 0 < `|g|_q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0. have [foo|foo] := eqVneq `|f|_p +oo%E; first by rewrite foo gt0_mulye ?leey. have [goo|goo] := eqVneq `|g|_q +oo%E; first by rewrite goo gt0_muley ?leey. -pose F := normed p f. -pose G := normed q g. -have -> : `| (f \* g)%R |_1 = `| (F \* G)%R |_1 * `| f |_p * `| g |_q. - rewrite {1}/Lnorm; under eq_integral => x _ do rewrite powRr1//. - rewrite invr1 poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin. - rewrite {1}/Lnorm. +pose F := normalized p f; pose G := normalized q g. +rewrite [leLHS](_ : _ = `| (F \* G)%R |_1 * `| f |_p * `| g |_q); last first. + rewrite !Lnorm1. under [in RHS]eq_integral. move=> x _. - rewrite /F /G /= /normed (mulrC `|f x|)%R mulrA -(mulrA (_^-1)). + 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). - rewrite powRr1; last first. - by rewrite mulr_ge0// divr_ge0 ?(fine_ge0, Lnorm_ge0, invr_ge0). - rewrite mulrC -normrM EFinM. - over. + 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 invr1 poweRe1; last first. - rewrite mule_ge0//. - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0. - by apply integral_ge0 => x _; rewrite lee_fin. - rewrite muleA EFinM. - rewrite muleCA 2!muleA (_ : _ * `|f|_p = 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// Lnorm_ge0. + rewrite -muleA muleC muleA EFinM muleCA 2!muleA. + rewrite (_ : _ * `|f|_p = 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 (_ : `|g|_q * _ = 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// Lnorm_ge0. + 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 (`|f|_p * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//. -apply: (@le_trans _ _ (\int[mu]_x (F x `^ p / p + G x `^ q / q)%:E)). - rewrite /Lnorm 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. +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_normed. - apply/aeW => x _; rewrite lee_fin powRr1// ger0_norm ?normed_convex//. - by rewrite mulr_ge0// normed_ge0. -rewrite le_eqVlt; apply/orP; left; apply/eqP. + 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_normed. + 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_normed. + 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_normed. + 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_normed. + 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_normed//; last exact: integrable_powR. -rewrite integral_normed//; last exact: integrable_powR. +rewrite integral_normalized//; last exact: integrable_powR. +rewrite integral_normalized//; last exact: integrable_powR. by rewrite 2!mule1 -EFinD pq. Qed. From 6d25b355e6242248433ab162ed20c4beac5050c0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 10 Aug 2023 10:43:33 +0900 Subject: [PATCH 04/13] notation test --- theories/lebesgue_integral.v | 44 ++++++++++++++++++------------------ 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 453b8a7eb..c436d535b 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -5640,21 +5640,21 @@ Implicit Types (p : R) (f g : T -> R). Definition Lnorm p f := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1. -Local Notation "`| f |_ p" := (Lnorm p f). +Local Notation "`| f |~ p" := (Lnorm p f). -Lemma Lnorm1 f : `| f |_1 = \int[mu]_x `|f x|%:E. +Lemma Lnorm1 f : `| f |~1 = \int[mu]_x `|f x|%:E. Proof. rewrite /Lnorm invr1// poweRe1//. by apply: eq_integral => t _; rewrite powRr1. by apply: integral_ge0 => t _; rewrite powRr1. Qed. -Lemma Lnorm_ge0 p f : 0 <= `| f |_p. Proof. exact: poweR_ge0. Qed. +Lemma Lnorm_ge0 p f : 0 <= `| f |~p. Proof. exact: poweR_ge0. Qed. -Lemma eq_Lnorm p f g : f =1 g -> `|f|_p = `|g|_p. +Lemma eq_Lnorm p f g : f =1 g -> `|f|~p = `|g|~p. Proof. by move=> fg; congr Lnorm; exact/funext. Qed. -Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> `| f |_p = 0 -> +Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> `| f |~p = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0). Proof. move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. @@ -5681,10 +5681,10 @@ 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 "`| f |_ p" := (Lnorm mu p f). +Local Notation "`| f |~ p" := (Lnorm mu p f). Let integrable_powR f p : (0 < p)%R -> - measurable_fun [set: T] f -> `| f |_p != +oo -> + measurable_fun [set: T] f -> `| f |~p != +oo -> mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E). Proof. move=> p0 mf foo; apply/integrableP; split. @@ -5698,7 +5698,7 @@ 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 -> - `| f |_ p = 0 -> `| (f \* g)%R |_1 <= `| f |_p * `| g |_q. + `| f |~ p = 0 -> `| (f \* g)%R |~1 <= `| f |~p * `| g |~q. Proof. move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//. rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0. @@ -5709,7 +5709,7 @@ rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0. by rewrite normrM => ->; rewrite mul0r. Qed. -Let normalized p f x := `|f x| / fine `|f|_p. +Let normalized p f x := `|f x| / fine `|f|~p. Let normalized_ge0 p f x : (0 <= normalized p f x)%R. Proof. by rewrite /normalized divr_ge0// fine_ge0// Lnorm_ge0. Qed. @@ -5718,12 +5718,12 @@ 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 < `|f|_p -> +Let integral_normalized f p : (0 < p)%R -> 0 < `|f|~p -> 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 (`|f|_p `^ p))%:E). +transitivity (\int[mu]_x (`|f x| `^ p / fine (`|f|~p `^ p))%:E). apply: eq_integral => t _. rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0. rewrite -powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0. @@ -5743,19 +5743,19 @@ 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 -> - `| (f \* g)%R |_1 <= `| f |_p * `| g |_q. + `| (f \* g)%R |~1 <= `| f |~p * `| g |~q. Proof. move=> mf mg p0 q0 pq. -have [f0|f0] := eqVneq `|f|_p 0%E; first exact: hoelder0. -have [g0|g0] := eqVneq `|g|_q 0%E. +have [f0|f0] := eqVneq `|f|~p 0%E; first exact: hoelder0. +have [g0|g0] := eqVneq `|g|~q 0%E. rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC. by under eq_Lnorm do rewrite /= mulrC. -have {f0}fpos : 0 < `|f|_p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. -have {g0}gpos : 0 < `|g|_q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0. -have [foo|foo] := eqVneq `|f|_p +oo%E; first by rewrite foo gt0_mulye ?leey. -have [goo|goo] := eqVneq `|g|_q +oo%E; first by rewrite goo gt0_muley ?leey. +have {f0}fpos : 0 < `|f|~p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. +have {g0}gpos : 0 < `|g|~q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0. +have [foo|foo] := eqVneq `|f|~p +oo%E; first by rewrite foo gt0_mulye ?leey. +have [goo|goo] := eqVneq `|g|~q +oo%E; first by rewrite goo gt0_muley ?leey. pose F := normalized p f; pose G := normalized q g. -rewrite [leLHS](_ : _ = `| (F \* G)%R |_1 * `| f |_p * `| g |_q); last first. +rewrite [leLHS](_ : _ = `| (F \* G)%R |~1 * `| f |~p * `| g |~q); last first. rewrite !Lnorm1. under [in RHS]eq_integral. move=> x _. @@ -5768,13 +5768,13 @@ rewrite [leLHS](_ : _ = `| (F \* G)%R |_1 * `| f |_p * `| g |_q); last first. exact: measurable_funM. - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0. rewrite -muleA muleC muleA EFinM muleCA 2!muleA. - rewrite (_ : _ * `|f|_p = 1) ?mul1e; last first. + rewrite (_ : _ * `|f|~p = 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 (_ : `|g|_q * _ = 1) ?mul1e// muleC. + rewrite (_ : `|g|~q * _ = 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 (`|f|_p * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//. +rewrite -(mul1e (`|f|~p * _)) -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 => //. From 6f6a1002051cb5d690bda206efbac00168021503 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 11 Aug 2023 18:53:32 +0900 Subject: [PATCH 05/13] use notation || _ ||_ _ --- CHANGELOG_UNRELEASED.md | 2 +- theories/lebesgue_integral.v | 44 ++++++++++++++++++------------------ 2 files changed, 23 insertions(+), 23 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a59d4ff6c..eb99bebdb 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -31,7 +31,7 @@ + lemma `eqe_pdivr_mull` - in `lebesgue_integral.v`: - + definition `Lnorm`, notations `'N[mu]_p[f]`, `` `| f |_p `` + + definition `Lnorm`, notations `'N[mu]_p[f]`, `` `|| f ||_p `` + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0` + lemma `hoelder` diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index c436d535b..e66b372d6 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -5640,21 +5640,21 @@ Implicit Types (p : R) (f g : T -> R). Definition Lnorm p f := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1. -Local Notation "`| f |~ p" := (Lnorm p f). +Local Notation "`|| f ||_ p" := (Lnorm p f). -Lemma Lnorm1 f : `| f |~1 = \int[mu]_x `|f x|%:E. +Lemma Lnorm1 f : `|| f ||_1 = \int[mu]_x `|f x|%:E. Proof. rewrite /Lnorm invr1// poweRe1//. by apply: eq_integral => t _; rewrite powRr1. by apply: integral_ge0 => t _; rewrite powRr1. Qed. -Lemma Lnorm_ge0 p f : 0 <= `| f |~p. Proof. exact: poweR_ge0. Qed. +Lemma Lnorm_ge0 p f : 0 <= `|| f ||_p. Proof. exact: poweR_ge0. Qed. -Lemma eq_Lnorm p f g : f =1 g -> `|f|~p = `|g|~p. +Lemma eq_Lnorm p f g : f =1 g -> `|| f ||_p = `|| g ||_p. Proof. by move=> fg; congr Lnorm; exact/funext. Qed. -Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> `| f |~p = 0 -> +Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> `|| f ||_p = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0). Proof. move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. @@ -5681,10 +5681,10 @@ 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 "`| f |~ p" := (Lnorm mu p f). +Local Notation "`|| f ||_ p" := (Lnorm mu p f). Let integrable_powR f p : (0 < p)%R -> - measurable_fun [set: T] f -> `| f |~p != +oo -> + measurable_fun [set: T] f -> `|| f ||_p != +oo -> mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E). Proof. move=> p0 mf foo; apply/integrableP; split. @@ -5698,7 +5698,7 @@ 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 -> - `| f |~ p = 0 -> `| (f \* g)%R |~1 <= `| f |~p * `| g |~q. + `|| f ||_ p = 0 -> `|| (f \* g)%R ||_1 <= `|| f ||_p * `|| g ||_q. Proof. move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//. rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0. @@ -5709,7 +5709,7 @@ rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0. by rewrite normrM => ->; rewrite mul0r. Qed. -Let normalized p f x := `|f x| / fine `|f|~p. +Let normalized p f x := `|f x| / fine `|| f ||_p. Let normalized_ge0 p f x : (0 <= normalized p f x)%R. Proof. by rewrite /normalized divr_ge0// fine_ge0// Lnorm_ge0. Qed. @@ -5718,12 +5718,12 @@ 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 < `|f|~p -> +Let integral_normalized f p : (0 < p)%R -> 0 < `|| f ||_p -> 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 (`|f|~p `^ p))%:E). +transitivity (\int[mu]_x (`|f x| `^ p / fine (`|| f ||_p `^ p))%:E). apply: eq_integral => t _. rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0. rewrite -powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0. @@ -5743,19 +5743,19 @@ 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 -> - `| (f \* g)%R |~1 <= `| f |~p * `| g |~q. + `|| (f \* g)%R ||_1 <= `|| f ||_p * `|| g ||_q. Proof. move=> mf mg p0 q0 pq. -have [f0|f0] := eqVneq `|f|~p 0%E; first exact: hoelder0. -have [g0|g0] := eqVneq `|g|~q 0%E. +have [f0|f0] := eqVneq `|| f ||_p 0%E; first exact: hoelder0. +have [g0|g0] := eqVneq `|| g ||_q 0%E. rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC. by under eq_Lnorm do rewrite /= mulrC. -have {f0}fpos : 0 < `|f|~p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. -have {g0}gpos : 0 < `|g|~q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0. -have [foo|foo] := eqVneq `|f|~p +oo%E; first by rewrite foo gt0_mulye ?leey. -have [goo|goo] := eqVneq `|g|~q +oo%E; first by rewrite goo gt0_muley ?leey. +have {f0}fpos : 0 < `|| f ||_p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. +have {g0}gpos : 0 < `|| g ||_q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0. +have [foo|foo] := eqVneq `|| f ||_p +oo%E; first by rewrite foo gt0_mulye ?leey. +have [goo|goo] := eqVneq `|| g ||_q +oo%E; first by rewrite goo gt0_muley ?leey. pose F := normalized p f; pose G := normalized q g. -rewrite [leLHS](_ : _ = `| (F \* G)%R |~1 * `| f |~p * `| g |~q); last first. +rewrite [leLHS](_ : _ = `|| (F \* G)%R ||_1 * `|| f ||_p * `|| g ||_q); last first. rewrite !Lnorm1. under [in RHS]eq_integral. move=> x _. @@ -5768,13 +5768,13 @@ rewrite [leLHS](_ : _ = `| (F \* G)%R |~1 * `| f |~p * `| g |~q); last first. exact: measurable_funM. - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0. rewrite -muleA muleC muleA EFinM muleCA 2!muleA. - rewrite (_ : _ * `|f|~p = 1) ?mul1e; last first. + rewrite (_ : _ * `|| f ||_p = 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 (_ : `|g|~q * _ = 1) ?mul1e// muleC. + rewrite (_ : `|| g ||_q * _ = 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 (`|f|~p * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//. +rewrite -(mul1e (`|| f ||_p * _)) -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 => //. From 18f42a5cf6b0b4f56917fa7c9d98f67e31a3e775 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Wed, 16 Aug 2023 14:13:49 +0200 Subject: [PATCH 06/13] Moving lnorm and hoelder --- theories/hoelder.v | 196 +++++++++++++++++++++++++++++++++++ theories/lebesgue_integral.v | 181 -------------------------------- 2 files changed, 196 insertions(+), 181 deletions(-) create mode 100644 theories/hoelder.v diff --git a/theories/hoelder.v b/theories/hoelder.v new file mode 100644 index 000000000..035917eb5 --- /dev/null +++ b/theories/hoelder.v @@ -0,0 +1,196 @@ +(* 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 itv. + +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 "`|| F ||_ p" + (at level 0, F at level 99, format "'[' `|| F ||_ p ']'"). + +Declare Scope Lnorm_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 : R) (f g : T -> R). + +Definition Lnorm p f := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1. + +Local Notation "`|| f ||_ p" := (Lnorm p f). + +Lemma Lnorm1 f : `|| f ||_1 = \int[mu]_x `|f x|%:E. +Proof. +rewrite /Lnorm invr1// poweRe1//. + by apply: eq_integral => t _; rewrite powRr1. +by apply: integral_ge0 => t _; rewrite powRr1. +Qed. + +Lemma Lnorm_ge0 p f : 0 <= `|| f ||_p. Proof. exact: poweR_ge0. Qed. + +Lemma eq_Lnorm p f g : f =1 g -> `|| f ||_p = `|| g ||_p. +Proof. by move=> fg; congr Lnorm; exact/funext. Qed. + +Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> `|| f ||_p = 0 -> + ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0). +Proof. +move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. + apply: measurableT_comp => //. + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. + 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 "`|| f ||_ p" := (Lnorm mu p f). + +Let integrable_powR f p : (0 < p)%R -> + measurable_fun [set: T] f -> `|| f ||_p != +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 (_ `^ _). +by apply/eq_integral => t _; rewrite gee0_abs// ?lee_fin ?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 -> + `|| f ||_ p = 0 -> `|| (f \* g)%R ||_1 <= `|| f ||_p * `|| g ||_q. +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 mf f0. + apply: filterS => x /(_ I) /= [] /powR_eq0_eq0 + _. + by rewrite normrM => ->; rewrite mul0r. +Qed. + +Let normalized p f x := `|f x| / fine `|| f ||_p. + +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 < `|| f ||_p -> + 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 (`|| f ||_p `^ p))%:E). + apply: eq_integral => t _. + rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0. + rewrite -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. + apply: gt0_poweR fpos; rewrite ?invr_gt0//. + by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. +rewrite /Lnorm -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 -> + `|| (f \* g)%R ||_1 <= `|| f ||_p * `|| g ||_q. +Proof. +move=> mf mg p0 q0 pq. +have [f0|f0] := eqVneq `|| f ||_p 0%E; first exact: hoelder0. +have [g0|g0] := eqVneq `|| g ||_q 0%E. + rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC. + by under eq_Lnorm do rewrite /= mulrC. +have {f0}fpos : 0 < `|| f ||_p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. +have {g0}gpos : 0 < `|| g ||_q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0. +have [foo|foo] := eqVneq `|| f ||_p +oo%E; first by rewrite foo gt0_mulye ?leey. +have [goo|goo] := eqVneq `|| g ||_q +oo%E; first by rewrite goo gt0_muley ?leey. +pose F := normalized p f; pose G := normalized q g. +rewrite [leLHS](_ : _ = `|| (F \* G)%R ||_1 * `|| f ||_p * `|| g ||_q); 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 (_ : _ * `|| f ||_p = 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 (_ : `|| g ||_q * _ = 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 (`|| f ||_p * _)) -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_integral.v b/theories/lebesgue_integral.v index e66b372d6..81acc0851 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -5630,184 +5630,3 @@ by rewrite ritv //= -EFinM lee_fin mulrC. Unshelve. all: by end_near. Qed. End lebesgue_differentiation. - -Section L_norm. -Context d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R}). -Local Open Scope ereal_scope. - -Implicit Types (p : R) (f g : T -> R). - -Definition Lnorm p f := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1. - -Local Notation "`|| f ||_ p" := (Lnorm p f). - -Lemma Lnorm1 f : `|| f ||_1 = \int[mu]_x `|f x|%:E. -Proof. -rewrite /Lnorm invr1// poweRe1//. - by apply: eq_integral => t _; rewrite powRr1. -by apply: integral_ge0 => t _; rewrite powRr1. -Qed. - -Lemma Lnorm_ge0 p f : 0 <= `|| f ||_p. Proof. exact: poweR_ge0. Qed. - -Lemma eq_Lnorm p f g : f =1 g -> `|| f ||_p = `|| g ||_p. -Proof. by move=> fg; congr Lnorm; exact/funext. Qed. - -Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> `|| f ||_p = 0 -> - ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0). -Proof. -move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. - apply: measurableT_comp => //. - apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. - 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 "`|| f ||_ p" := (Lnorm mu p f). - -Let integrable_powR f p : (0 < p)%R -> - measurable_fun [set: T] f -> `|| f ||_p != +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 (_ `^ _). -by apply/eq_integral => t _; rewrite gee0_abs// ?lee_fin ?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 -> - `|| f ||_ p = 0 -> `|| (f \* g)%R ||_1 <= `|| f ||_p * `|| g ||_q. -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 mf f0. - apply: filterS => x /(_ I) /= [] /powR_eq0_eq0 + _. - by rewrite normrM => ->; rewrite mul0r. -Qed. - -Let normalized p f x := `|f x| / fine `|| f ||_p. - -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 < `|| f ||_p -> - 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 (`|| f ||_p `^ p))%:E). - apply: eq_integral => t _. - rewrite powRM//; last by rewrite invr_ge0 fine_ge0// Lnorm_ge0. - rewrite -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. - apply: gt0_poweR fpos; rewrite ?invr_gt0//. - by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. -rewrite /Lnorm -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 -> - `|| (f \* g)%R ||_1 <= `|| f ||_p * `|| g ||_q. -Proof. -move=> mf mg p0 q0 pq. -have [f0|f0] := eqVneq `|| f ||_p 0%E; first exact: hoelder0. -have [g0|g0] := eqVneq `|| g ||_q 0%E. - rewrite muleC; apply: le_trans; last by apply: hoelder0 => //; rewrite addrC. - by under eq_Lnorm do rewrite /= mulrC. -have {f0}fpos : 0 < `|| f ||_p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. -have {g0}gpos : 0 < `|| g ||_q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0. -have [foo|foo] := eqVneq `|| f ||_p +oo%E; first by rewrite foo gt0_mulye ?leey. -have [goo|goo] := eqVneq `|| g ||_q +oo%E; first by rewrite goo gt0_muley ?leey. -pose F := normalized p f; pose G := normalized q g. -rewrite [leLHS](_ : _ = `|| (F \* G)%R ||_1 * `|| f ||_p * `|| g ||_q); 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 (_ : _ * `|| f ||_p = 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 (_ : `|| g ||_q * _ = 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 (`|| f ||_p * _)) -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. From 79840ce39603a658ffd64c5b1935126b44942f64 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 17 Aug 2023 16:43:05 +0900 Subject: [PATCH 07/13] going back to the N notation --- CHANGELOG_UNRELEASED.md | 2 + _CoqProject | 1 + theories/Make | 1 + theories/hoelder.v | 75 +++++++++++++++++++++++------------- theories/lebesgue_integral.v | 4 +- 5 files changed, 53 insertions(+), 30 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index eb99bebdb..895d2311f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -51,6 +51,8 @@ - in file `topology.v`, + new definition `regular_space`. + new lemma `ent_closure`. +- new file `hoelder.v`: + + - in file `lebesgue_integral.v`, + new lemmas `simple_bounded`, `measurable_bounded_integrable`, 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/hoelder.v b/theories/hoelder.v index 035917eb5..6e3025c46 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -4,17 +4,38 @@ 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 itv. - -Reserved Notation "'N[ mu ]_ p [ F ]" +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 "`|| F ||_ p" - (at level 0, F at level 99, format "'[' `|| F ||_ p ']'"). +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}. @@ -23,21 +44,21 @@ Implicit Types (p : R) (f g : T -> R). Definition Lnorm p f := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1. -Local Notation "`|| f ||_ p" := (Lnorm p f). +Local Notation "'N_ p [ f ]" := (Lnorm p f). -Lemma Lnorm1 f : `|| f ||_1 = \int[mu]_x `|f x|%:E. +Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E. Proof. rewrite /Lnorm invr1// poweRe1//. by apply: eq_integral => t _; rewrite powRr1. by apply: integral_ge0 => t _; rewrite powRr1. Qed. -Lemma Lnorm_ge0 p f : 0 <= `|| f ||_p. Proof. exact: poweR_ge0. Qed. +Lemma Lnorm_ge0 p f : 0 <= 'N_p[f]. Proof. exact: poweR_ge0. Qed. -Lemma eq_Lnorm p f g : f =1 g -> `|| f ||_p = `|| g ||_p. +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 p f : measurable_fun setT f -> `|| f ||_p = 0 -> +Lemma Lnorm_eq0_eq0 p f : measurable_fun setT f -> 'N_p[f] = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0). Proof. move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. @@ -64,10 +85,10 @@ 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 "`|| f ||_ p" := (Lnorm mu p f). +Local Notation "'N_ p [ f ]" := (Lnorm mu p f). Let integrable_powR f p : (0 < p)%R -> - measurable_fun [set: T] f -> `|| f ||_p != +oo -> + measurable_fun [set: T] f -> 'N_p[f] != +oo -> mu.-integrable [set: T] (fun x => (`|f x| `^ p)%:E). Proof. move=> p0 mf foo; apply/integrableP; split. @@ -81,7 +102,7 @@ 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 -> - `|| f ||_ p = 0 -> `|| (f \* g)%R ||_1 <= `|| f ||_p * `|| g ||_q. + 'N_p[f] = 0 -> 'N_1[(f \* g)%R] <= 'N_p[f] * 'N_q[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. @@ -92,7 +113,7 @@ rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0. by rewrite normrM => ->; rewrite mul0r. Qed. -Let normalized p f x := `|f x| / fine `|| f ||_p. +Let normalized p f x := `|f x| / fine 'N_p[f]. Let normalized_ge0 p f x : (0 <= normalized p f x)%R. Proof. by rewrite /normalized divr_ge0// fine_ge0// Lnorm_ge0. Qed. @@ -101,12 +122,12 @@ 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 < `|| f ||_p -> +Let integral_normalized f p : (0 < p)%R -> 0 < 'N_p[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 (`|| f ||_p `^ p))%:E). +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// Lnorm_ge0. rewrite -powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0. @@ -126,19 +147,19 @@ 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 -> - `|| (f \* g)%R ||_1 <= `|| f ||_p * `|| g ||_q. + 'N_1[(f \* g)%R] <= 'N_p[f] * 'N_q[g]. Proof. move=> mf mg p0 q0 pq. -have [f0|f0] := eqVneq `|| f ||_p 0%E; first exact: hoelder0. -have [g0|g0] := eqVneq `|| g ||_q 0%E. +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_Lnorm do rewrite /= mulrC. -have {f0}fpos : 0 < `|| f ||_p by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. -have {g0}gpos : 0 < `|| g ||_q by rewrite lt_neqAle eq_sym g0//= Lnorm_ge0. -have [foo|foo] := eqVneq `|| f ||_p +oo%E; first by rewrite foo gt0_mulye ?leey. -have [goo|goo] := eqVneq `|| g ||_q +oo%E; first by rewrite goo gt0_muley ?leey. +have {f0}fpos : 0 < 'N_p[f] by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. +have {g0}gpos : 0 < 'N_q[g] by rewrite lt_neqAle eq_sym g0//= Lnorm_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 := normalized p f; pose G := normalized q g. -rewrite [leLHS](_ : _ = `|| (F \* G)%R ||_1 * `|| f ||_p * `|| g ||_q); last first. +rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p[f] * 'N_q[g]); last first. rewrite !Lnorm1. under [in RHS]eq_integral. move=> x _. @@ -151,13 +172,13 @@ rewrite [leLHS](_ : _ = `|| (F \* G)%R ||_1 * `|| f ||_p * `|| g ||_q); last fir exact: measurable_funM. - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0. rewrite -muleA muleC muleA EFinM muleCA 2!muleA. - rewrite (_ : _ * `|| f ||_p = 1) ?mul1e; last first. + rewrite (_ : _ * 'N_p[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 (_ : `|| g ||_q * _ = 1) ?mul1e// muleC. + rewrite (_ : 'N_q[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 (`|| f ||_p * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//. +rewrite -(mul1e ('N_p[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 => //. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 81acc0851..0b90a46fd 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 exp itv. +Require Import esum measure lebesgue_measure numfun. (******************************************************************************) (* Lebesgue Integral *) @@ -45,8 +45,6 @@ Require Import esum measure lebesgue_measure numfun exp itv. (* 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 Lnorm. *) (* *) (******************************************************************************) From 7c8ddb60aedcae920d56def3c9b6dc1ea01c5a3d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 17 Aug 2023 17:29:42 +0900 Subject: [PATCH 08/13] fix changelog --- CHANGELOG_UNRELEASED.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 895d2311f..cb20ce01b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -30,8 +30,8 @@ - in `constructive_ereal.v`: + lemma `eqe_pdivr_mull` -- in `lebesgue_integral.v`: - + definition `Lnorm`, notations `'N[mu]_p[f]`, `` `|| f ||_p `` +- 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` From 0dc95517152e29ab0e4634d43d98c68db58ce87b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 23 Aug 2023 00:07:24 +0900 Subject: [PATCH 09/13] fixes --- CHANGELOG_UNRELEASED.md | 23 ++++++++++------------- theories/lebesgue_integral.v | 7 ------- 2 files changed, 10 insertions(+), 20 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index cb20ce01b..68210f4e7 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -23,18 +23,6 @@ - in `exp.v`: + lemmas `concave_ln`, `conjugate_powR` - -- 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 `integral_le_bound`, `continuous_compact_integrable`, and `lebesgue_differentiation_continuous`. @@ -51,8 +39,17 @@ - in file `topology.v`, + 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`, diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 0b90a46fd..ff4ab41cf 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -67,13 +67,6 @@ 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. From 3d5994e40adfb09a6ae2ca3163c7f5f815055fa4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 7 Sep 2023 18:44:40 +0900 Subject: [PATCH 10/13] tentative def of ess sup Co-authored-by: Alessandro Bruni --- theories/hoelder.v | 104 +++++++++++++++++++++++++++++++++++---------- 1 file changed, 82 insertions(+), 22 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 6e3025c46..2d4d94f25 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -36,13 +36,68 @@ Declare Scope Lnorm_scope. Local Open Scope ereal_scope. +(* TODO: move this elsewhere *) +Lemma ubound_setT {R : realFieldType} : 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 supremums_setT {R : realFieldType} : supremums [set: \bar R] = [set +oo]. +Proof. +rewrite /supremums ubound_setT. +by apply/seteqP; split=> [x []//|x -> /=]; split => // y ->. +Qed. + +Lemma supremum_setT {R : realFieldType} : supremum -oo [set: \bar R] = +oo. +Proof. +rewrite /supremum (negbTE setT0) supremums_setT. +by case: xgetP => // /(_ +oo)/= /eqP; rewrite eqxx. +Qed. + +Lemma ereal_sup_setT {R : realFieldType} : ereal_sup [set: \bar R] = +oo. +Proof. by rewrite /ereal_sup/= supremum_setT. Qed. + +Lemma range_oppe {R : realFieldType} : range -%E = [set: \bar R]. +Proof. +by apply/seteqP; split => [//|x] _; exists (- x) => //; rewrite oppeK. +Qed. + +Lemma ereal_inf_setT {R : realFieldType} : ereal_inf [set: \bar R] = -oo. +Proof. by rewrite /ereal_inf range_oppe/= ereal_sup_setT. Qed. + +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 [set t | f t > r]%R = 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 rf <-]. +rewrite leNgt; apply/negP => r0. +move/eqP: rf; apply/negP; rewrite gt_eqF//. +rewrite [X in mu X](_ : _ = setT) //. +by apply/seteqP; split => // x _ /=; rewrite (lt_le_trans _ (f0 x)). +Qed. + +End essential_supremum. + Section Lnorm. Context d {T : measurableType d} {R : realType}. Variable mu : {measure set T -> \bar R}. Local Open Scope ereal_scope. -Implicit Types (p : R) (f g : T -> R). +Implicit Types (p : \bar R) (f g : T -> R). -Definition Lnorm p f := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1. +Definition Lnorm p f := + match p with + | p%:E => (\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). @@ -53,12 +108,17 @@ rewrite /Lnorm invr1// poweRe1//. by apply: integral_ge0 => t _; rewrite powRr1. Qed. -Lemma Lnorm_ge0 p f : 0 <= 'N_p[f]. Proof. exact: poweR_ge0. Qed. +Lemma Lnorm_ge0 p f : 0 <= 'N_p[f]. +Proof. +move: p => [r|/=|//]; first 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 p f : measurable_fun setT f -> 'N_p[f] = 0 -> +(* TODO: generalize p *) +Lemma Lnorm_eq0_eq0 (p : R) f : measurable_fun setT f -> 'N_p%:E[f] = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0). Proof. move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. @@ -88,7 +148,7 @@ 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[f] != +oo -> + 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. @@ -102,7 +162,7 @@ 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[f] = 0 -> 'N_1[(f \* g)%R] <= 'N_p[f] * 'N_q[g]. + '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. @@ -113,7 +173,7 @@ rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0. by rewrite normrM => ->; rewrite mul0r. Qed. -Let normalized p f x := `|f x| / fine 'N_p[f]. +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. @@ -122,12 +182,12 @@ 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[f] -> +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[f] `^ p))%:E). +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 -powR_inv1; last by rewrite fine_ge0 // Lnorm_ge0. @@ -147,19 +207,19 @@ 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[f] * 'N_q[g]. + '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[f] 0%E; first exact: hoelder0. -have [g0|g0] := eqVneq 'N_q[g] 0%E. +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[f] by rewrite lt_neqAle eq_sym f0//= Lnorm_ge0. -have {g0}gpos : 0 < 'N_q[g] by rewrite lt_neqAle eq_sym g0//= Lnorm_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. +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[f] * 'N_q[g]); last first. +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 _. @@ -167,18 +227,18 @@ rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p[f] * 'N_q[g]); last first. 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. + 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. + - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0//Lnorm_ge0. rewrite -muleA muleC muleA EFinM muleCA 2!muleA. - rewrite (_ : _ * 'N_p[f] = 1) ?mul1e; last first. + 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[g] * _ = 1) ?mul1e// muleC. + 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[f] * _)) -muleA lee_pmul ?mule_ge0 ?Lnorm_ge0//. +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 => //. From 369cd198cba1d2626e7dafc20c30d8bc1d4378ff Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 12 Sep 2023 18:28:02 +0900 Subject: [PATCH 11/13] doc, changelog --- CHANGELOG_UNRELEASED.md | 6 +++++ theories/ereal.v | 31 ++++++++++++++++++++-- theories/hoelder.v | 59 +++-------------------------------------- theories/measure.v | 20 ++++++++++++++ 4 files changed, 59 insertions(+), 57 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 68210f4e7..cc6e632c5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -63,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/theories/ereal.v b/theories/ereal.v index e6be994cb..d1d8185f9 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. +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. diff --git a/theories/hoelder.v b/theories/hoelder.v index 2d4d94f25..8a7d5378c 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -36,61 +36,11 @@ Declare Scope Lnorm_scope. Local Open Scope ereal_scope. -(* TODO: move this elsewhere *) -Lemma ubound_setT {R : realFieldType} : 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 supremums_setT {R : realFieldType} : supremums [set: \bar R] = [set +oo]. -Proof. -rewrite /supremums ubound_setT. -by apply/seteqP; split=> [x []//|x -> /=]; split => // y ->. -Qed. - -Lemma supremum_setT {R : realFieldType} : supremum -oo [set: \bar R] = +oo. -Proof. -rewrite /supremum (negbTE setT0) supremums_setT. -by case: xgetP => // /(_ +oo)/= /eqP; rewrite eqxx. -Qed. - -Lemma ereal_sup_setT {R : realFieldType} : ereal_sup [set: \bar R] = +oo. -Proof. by rewrite /ereal_sup/= supremum_setT. Qed. - -Lemma range_oppe {R : realFieldType} : range -%E = [set: \bar R]. -Proof. -by apply/seteqP; split => [//|x] _; exists (- x) => //; rewrite oppeK. -Qed. - -Lemma ereal_inf_setT {R : realFieldType} : ereal_inf [set: \bar R] = -oo. -Proof. by rewrite /ereal_inf range_oppe/= ereal_sup_setT. Qed. - -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 [set t | f t > r]%R = 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 rf <-]. -rewrite leNgt; apply/negP => r0. -move/eqP: rf; apply/negP; rewrite gt_eqF//. -rewrite [X in mu X](_ : _ = setT) //. -by apply/seteqP; split => // x _ /=; rewrite (lt_le_trans _ (f0 x)). -Qed. - -End essential_supremum. - 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). +Implicit Types (p : \bar R) (f g : T -> R) (r : R). Definition Lnorm p f := match p with @@ -117,13 +67,12 @@ 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. -(* TODO: generalize p *) -Lemma Lnorm_eq0_eq0 (p : R) f : measurable_fun setT f -> 'N_p%:E[f] = 0 -> - ae_eq mu [set: T] (fun t => (`|f t| `^ p)%:E) (cst 0). +Lemma Lnorm_eq0_eq0 r f : measurable_fun setT f -> 'N_r%:E[f] = 0 -> + ae_eq mu [set: T] (fun t => (`|f t| `^ r)%:E) (cst 0). Proof. move=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. apply: measurableT_comp => //. - apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. + 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. diff --git a/theories/measure.v b/theories/measure.v index 0434fa366..5fff3bb6e 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 *) (* *) (******************************************************************************) @@ -4367,3 +4369,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. From 6875f5c0617d720887f578c458796eaf2ad21c6d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 14 Sep 2023 00:02:23 +0900 Subject: [PATCH 12/13] fix case p = 0 of Lnorm --- theories/hoelder.v | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 8a7d5378c..d00f61f27 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -44,7 +44,10 @@ Implicit Types (p : \bar R) (f g : T -> R) (r : R). Definition Lnorm p f := match p with - | p%:E => (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 + | 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. @@ -53,24 +56,26 @@ Local Notation "'N_ p [ f ]" := (Lnorm p f). Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E. Proof. -rewrite /Lnorm invr1// poweRe1//. +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|/=|//]; first exact: poweR_ge0. +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 : measurable_fun setT f -> 'N_r%:E[f] = 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=> mf /poweR_eq0_eq0 fp; apply/ae_eq_integral_abs => //=. +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. @@ -105,8 +110,8 @@ move=> p0 mf foo; apply/integrableP; split. exact: measurableT_comp. rewrite ltey; apply: contra foo. move=> /eqP/(@eqy_poweR _ _ p^-1); rewrite invr_gt0 => /(_ p0) <-. -apply/eqP; congr (_ `^ _). -by apply/eq_integral => t _; rewrite gee0_abs// ?lee_fin ?powR_ge0. +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 -> @@ -117,7 +122,7 @@ 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 mf f0. +- have := Lnorm_eq0_eq0 p0 mf f0. apply: filterS => x /(_ I) /= [] /powR_eq0_eq0 + _. by rewrite normrM => ->; rewrite mul0r. Qed. @@ -139,12 +144,13 @@ 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 -powR_inv1; last by rewrite 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 -poweRrM mulVf ?lt0r_neq0// poweRe1//; last exact: ltW. +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 => -[_]. From dbfc54e7d14e31427275d3036cb302a57c618c18 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 14 Sep 2023 15:50:25 +0900 Subject: [PATCH 13/13] rm spuirous parentheses --- theories/hoelder.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index d00f61f27..2d262c10f 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -47,7 +47,7 @@ Definition Lnorm p f := | p%:E => if p == 0%R then mu (f @^-1` (setT `\ 0%R)) else - ((\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1) + (\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.