From 3e4cf70c9828eeb3b5877e9c684459ecf9fcea3c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 14 Apr 2023 17:44:54 +0900 Subject: [PATCH 01/18] tentative definition of Lp-spaces --- _CoqProject | 1 + theories/lspace.v | 129 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 130 insertions(+) create mode 100644 theories/lspace.v diff --git a/_CoqProject b/_CoqProject index 53b84d50c3..89f1474794 100644 --- a/_CoqProject +++ b/_CoqProject @@ -97,3 +97,4 @@ theories/gauss_integral.v theories/showcase/summability.v analysis_stdlib/Rstruct_topology.v analysis_stdlib/showcase/uniform_bigO.v +theories/lspace.v diff --git a/theories/lspace.v b/theories/lspace.v new file mode 100644 index 0000000000..ca8778d70a --- /dev/null +++ b/theories/lspace.v @@ -0,0 +1,129 @@ +(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect. +From mathcomp Require Import ssralg ssrnum ssrint interval finmap. +Require Import boolp reals ereal. +From HB Require Import structures. +Require Import classical_sets signed functions topology normedtype cardinality. +Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral. +Require Import exp. + +(******************************************************************************) +(* *) +(* LfunType mu p == type of measurable functions f such that the *) +(* integral of |f| ^ p is finite *) +(* LType mu p == type of the elements of the Lp space *) +(* mu.-Lspace p == Lp space *) +(* *) +(******************************************************************************) + +Reserved Notation "mu .-Lspace p" (at level 4, format "mu .-Lspace p"). + +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. + +HB.mixin Record isLfun d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (p : R) (f : T -> R) := { + measurable_lfun : measurable_fun [set: T] f ; + lfuny : (\int[mu]_x (`|f x| `^ p)%:E < +oo)%E +}. + +#[short(type=LfunType)] +HB.structure Definition Lfun d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (p : R) := + {f : T -> R & isLfun d T R mu p f}. + +#[global] Hint Resolve measurable_lfun : core. +Arguments lfuny {d} {T} {R} {mu} {p} _. +#[global] Hint Resolve lfuny : core. + +Section Lfun_canonical. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : R). + +Canonical Lfun_eqType := EqType (LfunType mu p) gen_eqMixin. +Canonical Lfun_choiceType := ChoiceType (LfunType mu p) gen_choiceMixin. +End Lfun_canonical. + +Section Lequiv. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : R). + +Definition Lequiv (f g : LfunType mu p) := `[< {ae mu, forall x, f x = g x} >]. + +Let Lequiv_refl : reflexive Lequiv. +Proof. +by move=> f; exact/asboolP/(ae_imply _ (ae_eq_refl mu setT (EFin \o f))). +Qed. + +Let Lequiv_sym : symmetric Lequiv. +Proof. +by move=> f g; apply/idP/idP => /asboolP h; apply/asboolP; exact: ae_imply h. +Qed. + +Let Lequiv_trans : transitive Lequiv. +Proof. +move=> f g h /asboolP gf /asboolP fh; apply/asboolP/(ae_imply2 _ gf fh). +by move=> x ->. +Qed. + +Canonical Lequiv_canonical := + EquivRel Lequiv Lequiv_refl Lequiv_sym Lequiv_trans. + +Local Open Scope quotient_scope. + +Definition LspaceType := {eq_quot Lequiv}. +Canonical LspaceType_quotType := [quotType of LspaceType]. +Canonical LspaceType_eqType := [eqType of LspaceType]. +Canonical LspaceType_choiceType := [choiceType of LspaceType]. +Canonical LspaceType_eqQuotType := [eqQuotType Lequiv of LspaceType]. + +Lemma LequivP (f g : LfunType mu p) : + reflect {ae mu, forall x, f x = g x} (f == g %[mod LspaceType]). +Proof. by apply/(iffP idP); rewrite eqmodE// => /asboolP. Qed. + +Record LType := MemLType { Lfun_class : LspaceType }. +Coercion LfunType_of_LType (f : LType) : LfunType mu p := + repr (Lfun_class f). + +End Lequiv. + +Section Lspace. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. + +Definition Lspace p := [set: LType mu p]. +Arguments Lspace : clear implicits. + +Lemma LType1_integrable (f : LType mu 1) : mu.-integrable setT (EFin \o f). +Proof. +split; first exact/EFin_measurable_fun. +under eq_integral. + move=> x _ /=. + rewrite -(@powere_pose1 _ `|f x|%:E)//. + over. +exact: lfuny f. +Qed. + +Lemma LType2_integrable_sqr (f : LType mu 2) : + mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)). +Proof. +split; first exact/EFin_measurable_fun/measurable_fun_exprn. +rewrite (le_lt_trans _ (lfuny f))// ge0_le_integral//. +- apply: measurable_funT_comp => //. + exact/EFin_measurable_fun/measurable_fun_exprn. +- by move=> x _; rewrite lee_fin power_pos_ge0. +- apply/EFin_measurable_fun. + under eq_fun do rewrite power_pos_mulrn//. + exact/measurable_fun_exprn/measurable_funT_comp. +- by move=> t _/=; rewrite lee_fin normrX power_pos_mulrn. +Qed. + +End Lspace. +Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope. From 78f41e4aff366ab4c46d0f3d831571e0dc3f6730 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Mon, 27 May 2024 09:45:45 +0200 Subject: [PATCH 02/18] extended reals - compilation, CI fixes --- theories/lspace.v | 212 +++++++++++++++++++++++++++++++++++++++------- 1 file changed, 180 insertions(+), 32 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index ca8778d70a..ddc44368a0 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -5,7 +5,7 @@ Require Import boolp reals ereal. From HB Require Import structures. Require Import classical_sets signed functions topology normedtype cardinality. Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral. -Require Import exp. +Require Import exp hoelder. (******************************************************************************) (* *) @@ -29,14 +29,14 @@ Local Open Scope classical_set_scope. Local Open Scope ring_scope. HB.mixin Record isLfun d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R}) (p : R) (f : T -> R) := { + (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) := { measurable_lfun : measurable_fun [set: T] f ; - lfuny : (\int[mu]_x (`|f x| `^ p)%:E < +oo)%E + lfuny : ('N[ mu ]_p [ f ] < +oo)%E }. #[short(type=LfunType)] HB.structure Definition Lfun d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R}) (p : R) := + (mu : {measure set T -> \bar R}) (p : \bar R) := {f : T -> R & isLfun d T R mu p f}. #[global] Hint Resolve measurable_lfun : core. @@ -45,32 +45,32 @@ Arguments lfuny {d} {T} {R} {mu} {p} _. Section Lfun_canonical. Context d (T : measurableType d) (R : realType). -Variables (mu : {measure set T -> \bar R}) (p : R). +Variables (mu : {measure set T -> \bar R}) (p : \bar R). + +HB.instance Definition _ := gen_eqMixin (LfunType mu p). +HB.instance Definition _ := gen_choiceMixin (LfunType mu p). -Canonical Lfun_eqType := EqType (LfunType mu p) gen_eqMixin. -Canonical Lfun_choiceType := ChoiceType (LfunType mu p) gen_choiceMixin. End Lfun_canonical. Section Lequiv. Context d (T : measurableType d) (R : realType). -Variables (mu : {measure set T -> \bar R}) (p : R). +Variables (mu : {measure set T -> \bar R}) (p : \bar R). Definition Lequiv (f g : LfunType mu p) := `[< {ae mu, forall x, f x = g x} >]. Let Lequiv_refl : reflexive Lequiv. Proof. -by move=> f; exact/asboolP/(ae_imply _ (ae_eq_refl mu setT (EFin \o f))). +by move=> f; exact/asboolP/(filterS _ (ae_eq_refl mu setT (EFin \o f))). Qed. Let Lequiv_sym : symmetric Lequiv. Proof. -by move=> f g; apply/idP/idP => /asboolP h; apply/asboolP; exact: ae_imply h. +by move=> f g; apply/idP/idP => /asboolP h; apply/asboolP; exact: filterS h. Qed. Let Lequiv_trans : transitive Lequiv. Proof. -move=> f g h /asboolP gf /asboolP fh; apply/asboolP/(ae_imply2 _ gf fh). -by move=> x ->. +by move=> f g h /asboolP gf /asboolP fh; apply/asboolP/(filterS2 _ _ gf fh) => x ->. Qed. Canonical Lequiv_canonical := @@ -79,10 +79,10 @@ Canonical Lequiv_canonical := Local Open Scope quotient_scope. Definition LspaceType := {eq_quot Lequiv}. -Canonical LspaceType_quotType := [quotType of LspaceType]. -Canonical LspaceType_eqType := [eqType of LspaceType]. -Canonical LspaceType_choiceType := [choiceType of LspaceType]. -Canonical LspaceType_eqQuotType := [eqQuotType Lequiv of LspaceType]. +Canonical LspaceType_quotType := [the quotType _ of LspaceType]. +Canonical LspaceType_eqType := [the eqType of LspaceType]. +Canonical LspaceType_choiceType := [the choiceType of LspaceType]. +Canonical LspaceType_eqQuotType := [the eqQuotType Lequiv of LspaceType]. Lemma LequivP (f g : LfunType mu p) : reflect {ae mu, forall x, f x = g x} (f == g %[mod LspaceType]). @@ -103,27 +103,175 @@ Arguments Lspace : clear implicits. Lemma LType1_integrable (f : LType mu 1) : mu.-integrable setT (EFin \o f). Proof. -split; first exact/EFin_measurable_fun. -under eq_integral. - move=> x _ /=. - rewrite -(@powere_pose1 _ `|f x|%:E)//. - over. -exact: lfuny f. +apply/integrableP; split; first exact/EFin_measurable_fun. +have := lfuny f. +rewrite unlock /Lnorm ifF ?oner_eq0// invr1 poweRe1; last first. + by apply integral_ge0 => x _; rewrite lee_fin powRr1//. +by under eq_integral => i _ do rewrite powRr1//. Qed. -Lemma LType2_integrable_sqr (f : LType mu 2) : +Lemma LType2_integrable_sqr (f : LType mu 2%:E) : mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)). Proof. -split; first exact/EFin_measurable_fun/measurable_fun_exprn. -rewrite (le_lt_trans _ (lfuny f))// ge0_le_integral//. -- apply: measurable_funT_comp => //. - exact/EFin_measurable_fun/measurable_fun_exprn. -- by move=> x _; rewrite lee_fin power_pos_ge0. -- apply/EFin_measurable_fun. - under eq_fun do rewrite power_pos_mulrn//. - exact/measurable_fun_exprn/measurable_funT_comp. -- by move=> t _/=; rewrite lee_fin normrX power_pos_mulrn. +apply/integrableP; split. + exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f)/measurable_lfun. +rewrite (@lty_poweRy _ _ (2^-1))//. +rewrite (le_lt_trans _ (lfuny f))//. +rewrite unlock /Lnorm ifF ?gt_eqF//. +rewrite gt0_ler_poweR//. +- by rewrite in_itv/= integral_ge0// leey. +- rewrite in_itv/= leey integral_ge0// => x _. + by rewrite lee_fin powR_ge0. +rewrite ge0_le_integral//. +- apply: measurableT_comp => //. + exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f)/measurable_lfun. +- by move=> x _; rewrite lee_fin powR_ge0. +- exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R)/measurableT_comp/measurable_lfun. +- by move=> t _/=; rewrite lee_fin normrX powR_mulrn. Qed. End Lspace. Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope. + +Section Lspace_norm. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. +Variable (p : R). (* add hypothesis p > 1 *) + +(* 0 - + should come with proofs that they are in LfunType mu p *) + +Notation ty := (T -> R). +Definition nm f := fine ('N[mu]_p%:E[f]). + +(* Program Definition fct_zmodMixin := *) +(* @GRing.isZmodule.Build (LfunType mu p%:E) 0 (fun f x => - f x) (fun f g => f \+ g). *) + +(* measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R *) + +(* Notation ty := (LfunType mu p%:E). *) +(* Definition nm (f : ty) := fine ('N[mu]_p%:E[f]). *) + +(* HB.instance Definition _ := GRing.Zmodule.on ty. *) + +Lemma ler_Lnorm_add (f g : ty) : + nm (f \+ g) <= nm f + nm g. +Proof. +rewrite /nm. +have : (-oo < 'N[mu]_p%:E[f])%E by exact: (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _)). +have : (-oo < 'N[mu]_p%:E[g])%E by exact: (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _)). +rewrite !ltNye_eq => /orP[f_fin /orP[g_fin|/eqP foo]|/eqP goo]. +- rewrite -fineD ?fine_le//. + - admit. + - by rewrite fin_numD f_fin g_fin//. + rewrite minkowski//. admit. admit. admit. +- rewrite foo/= add0r. + have : ('N[mu]_p%:E[f] <= 'N[mu]_p%:E[(f \+ g)])%E. + rewrite unlock /Lnorm. + rewrite {1}(@ifF _ (p == 0)). + rewrite {1}(@ifF _ (p == 0)). + rewrite gt0_ler_poweR. + - by []. + - admit. + - admit. + - admit. + rewrite ge0_le_integral//. + - move => x _. rewrite lee_fin powR_ge0//. + - admit. + - move => x _. rewrite lee_fin powR_ge0//. + - admit. + - move => x _. rewrite lee_fin gt0_ler_powR//. admit. (* rewrite normr_le. *) + +Admitted. + +Lemma natmulfctE (U : pointedType) (K : ringType) (f : U -> K) n : + f *+ n = (fun x => f x *+ n). +Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed. + + +Lemma Lnorm_eq0 f : nm f = 0 -> {ae mu, f =1 0}. +rewrite /nm => /eqP. +rewrite fine_eq0; last first. admit. +move/eqP/Lnorm_eq0_eq0. +(* ale: I don't think it holds almost everywhere equal does not mean equal * +rewrite unlock /Lnorm ifF. +rewrite poweR_eq0. +rewrite integral_abs_eq0. *) +Admitted. + +Lemma Lnorm_natmul f k : nm (f *+ k) = nm f *+ k. +rewrite /nm unlock /Lnorm. +case: (ifP (p == 0)). + admit. + +move => p0. +under eq_integral => x _. + rewrite -mulr_natr/=. + rewrite fctE (_ : k%:R _ = k%:R); last by rewrite natmulfctE. + rewrite normrM powRM//=. + rewrite mulrC EFinM. + over. +rewrite /=. +rewrite integralZl//; last first. admit. +rewrite poweRM; last 2 first. +- by rewrite lee_fin powR_ge0. +- by rewrite integral_ge0// => x _; rewrite lee_fin powR_ge0. + +rewrite poweR_EFin -powRrM mulfV; last admit. +rewrite powRr1//. +rewrite fineM//; last admit. +rewrite mulrC. + +Admitted. + +Lemma LnormN f : nm (-f) = nm f. +rewrite /nm. +congr (fine _). +rewrite unlock /Lnorm. +case: ifP. +move=> p0. + admit. + +move=> p0. +congr (_ `^ _)%E. +apply eq_integral => x _. +congr ((_ `^ _)%:E). +by rewrite normrN. +Admitted. + +(* +Lemma ler_Lnorm_add f g : + 'N[mu]_p%:E[(f \+ g)%R] <= 'N[mu]_p%:E[f] + 'N[mu]_p%:E[g]. +Admitted. + +Lemma Lnorm_eq0 f : 'N[mu]_p%:E[f] = 0 -> f = 0%R. +Admitted. + +Lemma Lnorm_natmul f k : 'N[mu]_p%:E [f *+ k]%R = 'N[mu]_p%:E [f] *+ k. +Admitted. + +Lemma LnormN f : 'N[mu]_p%:E [- f]%R = 'N[mu]_p%:E [f]. +Admitted. +*) + +HB.instance Definition _ := + @Num.Zmodule_isNormed.Build R (*LType mu p%:E*) ty + nm ler_Lnorm_add Lnorm_eq0 Lnorm_natmul LnormN. + +(* todo: add equivalent of mx_normZ and HB instance *) + +End Lspace_norm. + +(* +Section Lspace_inclusion. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. + +Lemma Lspace_inclusion p q : (p <= q)%E -> + forall (f : LfunType mu q), ('N[ mu ]_p [ f ] < +oo)%E. +Proof. +move=> pleq f. + +isLfun d T R mu p f. + +End Lspace_inclusion. +*) From c4503cd7ff9b9cbbfdde7d84c79459f4ba8736ec Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 27 Jan 2025 17:35:30 +0100 Subject: [PATCH 03/18] WIP --- .nix/config.nix | 7 ++++--- theories/lspace.v | 2 +- theories/normedtype.v | 32 +++++++++++++++++++++++++------- 3 files changed, 30 insertions(+), 11 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 1dbcc48de0..b92ca6aa89 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -50,12 +50,13 @@ in ## will be created per bundle bundles."8.19".coqPackages = common-bundle // { coq.override.version = "8.19"; - mathcomp.override.version = "2.2.0"; + mathcomp.override.version = "CohenCyril:seminorm"; + mathcomp-bigenough.override.version = "master"; + mathcomp-finmap.override.version = "master"; }; bundles."8.20".coqPackages = common-bundle // { coq.override.version = "8.20"; - mathcomp.override.version = "2.2.0"; }; bundles."9.0".coqPackages = common-bundle // { @@ -74,7 +75,7 @@ in coq-elpi.override.version = "master"; coq-elpi.override.elpi-version = "2.0.7"; hierarchy-builder.override.version = "master"; - mathcomp.override.version = "master"; + mathcomp.override.version = "CohenCyril:seminorm"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; ssprove.job = false; diff --git a/theories/lspace.v b/theories/lspace.v index ddc44368a0..4a39a17202 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect. From mathcomp Require Import ssralg ssrnum ssrint interval finmap. -Require Import boolp reals ereal. +From mathcomp Require Import boolp reals ereal. From HB Require Import structures. Require Import classical_sets signed functions topology normedtype cardinality. Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral. diff --git a/theories/normedtype.v b/theories/normedtype.v index 171b7196d8..6159302d47 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -263,17 +263,27 @@ by rewrite opprK. Qed. HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T - of Num.NormedZmodule R T & PseudoPointedMetric R T := { + of Num.SemiNormedZmodule R T & PseudoPointedMetric R T := { pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |) }. +(* HB.factory Record NormedZmod_PseudoMetric_eq (R : numDomainType) T *) +(* of Num.SemiNormedZmodule R T & PseudoPointedMetric R T := { *) +(* pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |) *) +(* }. *) + +#[short(type="pseudoMetricSemiNormedZmodType")] +HB.structure Definition PseudoMetricSemiNormedZmod (R : numDomainType) := + {T of Num.SemiNormedZmodule R T & PseudoMetric R T + & NormedZmod_PseudoMetric_eq R T & isPointed T}. + #[short(type="pseudoMetricNormedZmodType")] HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) := {T of Num.NormedZmodule R T & PseudoMetric R T & NormedZmod_PseudoMetric_eq R T & isPointed T}. Section pseudoMetricnormedzmodule_lemmas. -Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}. +Context {K : numDomainType} {V : pseudoMetricSemiNormedZmodType K}. Local Notation ball_norm := (ball_ (@normr K V)). @@ -913,21 +923,27 @@ Qed. (** Modules with a norm depending on a numDomain*) HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V - of PseudoMetricNormedZmod K V & Tvs K V := { + of PseudoMetricSemiNormedZmod K V & Tvs K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. +#[short(type="semiNormedModType")] +HB.structure Definition SemiNormedModule (K : numDomainType) := + {T of PseudoMetricSemiNormedZmod K T & Tvs K T + & PseudoMetricNormedZmod_Tvs_isNormedModule K T}. + + #[short(type="normedModType")] HB.structure Definition NormedModule (K : numDomainType) := {T of PseudoMetricNormedZmod K T & Tvs K T & PseudoMetricNormedZmod_Tvs_isNormedModule K T}. -HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V - of PseudoMetricNormedZmod K V & GRing.Lmodule K V := { +HB.factory Record PseudoMetricSemiNormedZmod_Lmodule_isSemiNormedModule (K : numFieldType) V + of PseudoMetricSemiNormedZmod K V & GRing.Lmodule K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. -HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V. +HB.builders Context K V of PseudoMetricSemiNormedZmod_Lmodule_isSemiNormedModule K V. (* NB: These lemmas are done later with more machinery. They should be simplified once normedtype is split, and the present section can @@ -965,7 +981,9 @@ rewrite [leRHS](_ : _ = M^-1 * (M * M)); last first. by rewrite mulrA mulVf ?mul1r// gt_eqF. rewrite [leLHS](_ : _ = M^-1 * (M * (`|x| + `|x|) + `|e| / 2)); last first. by rewrite mulrDr mulrA mulVf ?mul1r ?gt_eqF// mulrC addrA. -by rewrite ler_wpM2l ?invr_ge0// ?ltW// -ltrBrDl -mulrBr ltr_pM// ltrBrDl. +rewrite ler_wpM2l ?invr_ge0// ?ltW// -ltrBrDl -mulrBr ltr_pM// ltrBrDl. +near: M; apply: nbhs_pinfty_gt. +Search "nbhs" (_ < _). Unshelve. all: by end_near. Qed. Lemma locally_convex : From ab968cdad52812b2855ae15e5ffe4aeab408548b Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Tue, 28 Jan 2025 09:38:10 +0100 Subject: [PATCH 04/18] norms - lspace.v headers --- theories/hoelder.v | 70 +++++++++++++++++++++++++++++++++++++++++++ theories/lspace.v | 10 +++---- theories/normedtype.v | 4 +-- 3 files changed, 77 insertions(+), 7 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index d420694d2e..e4b0f88d75 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -93,6 +93,26 @@ move=> r0; rewrite unlock (negbTE r0) -poweRrM mulVf// poweRe1//. by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0. Qed. +Lemma opp_Lnorm f p : + 'N_p[-%R \o f] = 'N_p[f]. +Proof. +rewrite unlock /Lnorm. +case: p => /= [r||//]. + case: eqP => _. congr (mu _). + rewrite !preimage_setI. + congr (_ `&` _). + rewrite -!preimage_setC. + congr (~` _). + rewrite /preimage. + apply: funext => x/=. + rewrite -{1}oppr0. + apply: propext. split; last by move=> ->. + by move/oppr_inj. + by under eq_integral => x _ do rewrite normrN. +rewrite compA (_ : normr \o -%R = normr)//. +apply: funext => x/=; exact: normrN. +Qed. + End Lnorm_properties. #[global] @@ -502,4 +522,54 @@ congr (_ * _); rewrite poweRN. - by rewrite -powR_Lnorm ?gt_eqF// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. Qed. +Lemma minkowski' f g p : + measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R -> + 'N_p%:E[f] <= 'N_p%:E[f \+ g] + 'N_p%:E[g]. +Proof. +move=> mf mg p1. +rewrite (_ : f = ((f \+ g) \+ (-%R \o g))%R); last admit. +rewrite [X in _ <= 'N__[X] + _](_ : ((f \+ g \- g) \+ g)%R = (f \+ g)%R); last admit. +rewrite (_ : 'N__[g] = 'N_p%:E[-%R \o g]); last admit. +apply: minkowski => //. + apply: measurable_funD => //. +apply: measurableT_comp => //. +Admitted. + End minkowski. + +Section Lnorm_properties. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Local Open Scope ereal_scope. +Implicit Types (p : \bar R) (f g : T -> R) (r : R). + +Lemma LnormD_fin_num p f g : + 1 <= p -> + measurable_fun setT f -> measurable_fun setT g -> + 'N[mu]_p[f] \is a fin_num -> 'N[mu]_p[g] \is a fin_num -> + 'N[mu]_p[f \+ g] \is a fin_num. +Proof. +case: p => [p|_|]. +- move=> p1 mf mg Nffin Ngfin. + rewrite fin_numElt (@lt_le_trans _ _ 0)//= ?Lnorm_ge0//. + rewrite (@le_lt_trans _ _ ('N[mu]_p%:E[f] + 'N[mu]_p%:E[g]))//. + apply: minkowski => //. + by rewrite lte_add_pinfty// -ge0_fin_numE// Lnorm_ge0. +- move=> mf mg. + rewrite unlock /Lnorm. + case: ifPn => // mu_ge0. + rewrite !fin_numElt => /andP[_ fley] /andP[_ gley]. + rewrite (@lt_le_trans _ _ 0)//= ?ess_sup_ge0//; last first. + move=> t/=; exact: normr_ge0. + admit. +- by rewrite leeNy_eq => /eqP. +Admitted. + +Lemma LnormD_pinfty p f g : + 1 <= p -> measurable_fun setT f -> measurable_fun setT g -> + 'N[mu]_p[f] = +oo -> 'N[mu]_p[f \+ g] = +oo. +Proof. +case: p => [p||]. +- move=> p1 mf mg. + +End Lnorm_properties. diff --git a/theories/lspace.v b/theories/lspace.v index 4a39a17202..db1807b51f 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -3,9 +3,9 @@ From mathcomp Require Import all_ssreflect. From mathcomp Require Import ssralg ssrnum ssrint interval finmap. From mathcomp Require Import boolp reals ereal. From HB Require Import structures. -Require Import classical_sets signed functions topology normedtype cardinality. -Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral. -Require Import exp hoelder. +From mathcomp Require Import classical_sets signed functions topology normedtype cardinality. +From mathcomp Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral. +From mathcomp Require Import exp hoelder. (******************************************************************************) (* *) @@ -254,8 +254,8 @@ Admitted. *) HB.instance Definition _ := - @Num.Zmodule_isNormed.Build R (*LType mu p%:E*) ty - nm ler_Lnorm_add Lnorm_eq0 Lnorm_natmul LnormN. + @Num.Zmodule_isSemiNormed.Build R (*LType mu p%:E*) ty + nm ler_Lnorm_add Lnorm_natmul LnormN. (* todo: add equivalent of mx_normZ and HB instance *) diff --git a/theories/normedtype.v b/theories/normedtype.v index 6159302d47..96dac5498d 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -983,7 +983,7 @@ rewrite [leLHS](_ : _ = M^-1 * (M * (`|x| + `|x|) + `|e| / 2)); last first. by rewrite mulrDr mulrA mulVf ?mul1r ?gt_eqF// mulrC addrA. rewrite ler_wpM2l ?invr_ge0// ?ltW// -ltrBrDl -mulrBr ltr_pM// ltrBrDl. near: M; apply: nbhs_pinfty_gt. -Search "nbhs" (_ < _). +rewrite !realD// normr_real//. Unshelve. all: by end_near. Qed. Lemma locally_convex : @@ -2552,7 +2552,7 @@ by rewrite !num_max bE dE maxr_pMr. Qed. HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m.+1, n.+1) + PseudoMetricSemiNormedZmod_Lmodule_isSemiNormedModule.Build K 'M[K]_(m.+1, n.+1) mx_normZ. End matrix_NormedModule. From 392139bb1d134a1ccca0d0df8c128f56743d1f5b Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 28 Jan 2025 17:00:55 +0100 Subject: [PATCH 05/18] ae improvements - making ae work as a filter - Adding notations for ae - generalizing ae_eq --- theories/charge.v | 3 ++ theories/lebesgue_integral.v | 13 ++++--- theories/lspace.v | 4 +-- theories/measure.v | 69 ++++++++++++++++++------------------ 4 files changed, 46 insertions(+), 43 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 6ae5e0979a..0c8d846c9f 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1866,6 +1866,9 @@ have nuf A : d.-measurable A -> nu A = \int[mu]_(x in A) f x. move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //. - exact/measurable_funTS. - exact/measurable_funTS. +- move: ff'. + have := @ae_eq_subset _ _ _ mu setT A f f'. + apply: ae_eq_subset. - exact: ae_eq_subset ff'. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 5105187b21..008a388b58 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3833,11 +3833,9 @@ Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}). -Local Notation ae_eq := (ae_eq mu). - Let ae_eq_integral_abs_bounded (D : set T) (mD : measurable D) (f : T -> \bar R) M : measurable_fun D f -> (forall x, D x -> `|f x| <= M%:E) -> - ae_eq D f (cst 0) -> \int[mu]_(x in D) `|f x|%E = 0. + (\forall x \ae mu, D x -> f x = 0) -> \int[mu]_(x in D) `|f x|%E = 0. Proof. move=> mf fM [N [mA mN0 Df0N]]. pose Df_neq0 := D `&` [set x | f x != 0]. @@ -3866,7 +3864,8 @@ by rewrite mule0 -eq_le => /eqP. Qed. Lemma ae_eq_integral_abs (D : set T) (mD : measurable D) (f : T -> \bar R) : - measurable_fun D f -> \int[mu]_(x in D) `|f x| = 0 <-> ae_eq D f (cst 0). + measurable_fun D f -> + \int[mu]_(x in D) `|f x| = 0 <-> (\forall x \ae mu, D x -> f x = 0). Proof. move=> mf; split=> [iDf0|Df0]. exists (D `&` [set x | f x != 0]); split; @@ -3920,7 +3919,7 @@ transitivity (limn (fun n => \int[mu]_(x in D) (f_ n x) )). have [ftm|ftm] := leP `|f t|%E m%:R%:E. by rewrite lexx /= (le_trans ftm)// lee_fin ler_nat. by rewrite (ltW ftm) /= lee_fin ler_nat. -have ae_eq_f_ n : ae_eq D (f_ n) (cst 0). +have ae_eq_f_ n : (f_ n) = (cst 0) %[ae mu in D]. case: Df0 => N [mN muN0 DfN]. exists N; split => // t /= /not_implyP[Dt fnt0]. apply: DfN => /=; apply/not_implyP; split => //. @@ -4029,7 +4028,7 @@ Qed. Lemma ge0_ae_eq_integral (D : set T) (f g : T -> \bar R) : measurable D -> measurable_fun D f -> measurable_fun D g -> (forall x, D x -> 0 <= f x) -> (forall x, D x -> 0 <= g x) -> - ae_eq D f g -> \int[mu]_(x in D) (f x) = \int[mu]_(x in D) (g x). + f = g %[ae mu in D] -> \int[mu]_(x in D) (f x) = \int[mu]_(x in D) (g x). Proof. move=> mD mf mg f0 g0 [N [mN N0 subN]]. rewrite integralEpatch// [RHS]integralEpatch//. @@ -4047,7 +4046,7 @@ Qed. Lemma ae_eq_integral (D : set T) (g f : T -> \bar R) : measurable D -> measurable_fun D f -> measurable_fun D g -> - ae_eq D f g -> \int[mu]_(x in D) f x = \int[mu]_(x in D) g x. + f = g %[ae mu in D] -> \int[mu]_(x in D) f x = \int[mu]_(x in D) g x. Proof. move=> mD mf mg /ae_eq_funeposneg[Dfgp Dfgn]. rewrite integralE// [in RHS]integralE//; congr (_ - _). diff --git a/theories/lspace.v b/theories/lspace.v index db1807b51f..f8c3ad6901 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -56,7 +56,7 @@ Section Lequiv. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (p : \bar R). -Definition Lequiv (f g : LfunType mu p) := `[< {ae mu, forall x, f x = g x} >]. +Definition Lequiv (f g : LfunType mu p) := `[< f = g [%ae mu] >]. Let Lequiv_refl : reflexive Lequiv. Proof. @@ -85,7 +85,7 @@ Canonical LspaceType_choiceType := [the choiceType of LspaceType]. Canonical LspaceType_eqQuotType := [the eqQuotType Lequiv of LspaceType]. Lemma LequivP (f g : LfunType mu p) : - reflect {ae mu, forall x, f x = g x} (f == g %[mod LspaceType]). + reflect (f = g %[ae mu]) (f == g %[mod LspaceType]). Proof. by apply/(iffP idP); rewrite eqmodE// => /asboolP. Qed. Record LType := MemLType { Lfun_class : LspaceType }. diff --git a/theories/measure.v b/theories/measure.v index 06338ce393..730adf22ff 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4064,7 +4064,8 @@ Qed. Section ae. Definition almost_everywhere d (T : semiRingOfSetsType d) (R : realFieldType) - (mu : set T -> \bar R) (P : T -> Prop) := mu.-negligible (~` [set x | P x]). + (mu : set T -> \bar R) : set_system T := + fun P => mu.-negligible (~` [set x | P x]). Let almost_everywhereT d (T : semiRingOfSetsType d) (R : realFieldType) (mu : {content set T -> \bar R}) : almost_everywhere mu setT. @@ -4083,16 +4084,14 @@ Proof. by rewrite /almost_everywhere => mA mB; rewrite setCI; exact: negligibleU. Qed. -#[global] -Instance ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType) +Definition ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType) (mu : {measure set T -> \bar R}) : Filter (almost_everywhere mu). Proof. by split; [exact: almost_everywhereT|exact: almost_everywhereI| exact: almost_everywhereS]. Qed. -#[global] -Instance ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d} +Definition ae_properfilter_algebraOfSetsType d {T : algebraOfSetsType d} (R : realFieldType) (mu : {measure set T -> \bar R}) : mu [set: T] > 0 -> ProperFilter (almost_everywhere mu). Proof. @@ -4105,19 +4104,27 @@ End ae. #[global] Hint Extern 0 (Filter (almost_everywhere _)) => (apply: ae_filter_ringOfSetsType) : typeclass_instances. +#[global] Hint Extern 0 (Filter (nbhs (almost_everywhere _))) => + (apply: ae_filter_ringOfSetsType) : typeclass_instances. #[global] Hint Extern 0 (ProperFilter (almost_everywhere _)) => (apply: ae_properfilter_algebraOfSetsType) : typeclass_instances. +#[global] Hint Extern 0 (ProperFilter (nbhs (almost_everywhere _))) => + (apply: ae_properfilter_algebraOfSetsType) : typeclass_instances. -Definition almost_everywhere_notation d (T : semiRingOfSetsType d) - (R : realFieldType) (mu : set T -> \bar R) (P : T -> Prop) - & (phantom Prop (forall x, P x)) := almost_everywhere mu P. -Notation "{ 'ae' m , P }" := - (almost_everywhere_notation m (inPhantom P)) : type_scope. - -Lemma aeW {d} {T : semiRingOfSetsType d} {R : realFieldType} +Notation "{ 'ae' m , P }" := {near almost_everywhere m, P} : type_scope. +Notation "\forall x \ae mu , P" := (\forall x \near almost_everywhere mu, P) + (format "\forall x \ae mu , P", + x name, P at level 200, at level 200): type_scope. +Notation ae_eq mu D f g := (\forall x \ae mu, D x -> f x = g x). +Notation "f = g %[ae mu 'in' D ]" := (\forall x \ae mu, D x -> f x = g x) + (format "f = g '%[ae' mu 'in' D ]", g at next level, D at level 200, at level 70). +Notation "f = g %[ae mu ]" := (f = g %[ae mu in setT ]) + (format "f = g '%[ae' mu ]", g at next level, at level 70). + +Lemma aeW {d} {T : ringOfSetsType d} {R : realFieldType} (mu : {measure set _ -> \bar R}) (P : T -> Prop) : - (forall x, P x) -> {ae mu, forall x, P x}. + (forall x, P x) -> \forall x \ae mu, P x. Proof. move=> aP; have -> : P = setT by rewrite predeqE => t; split. by apply/negligibleP; [rewrite setCT|rewrite setCT measure0]. @@ -4125,29 +4132,26 @@ Qed. Section ae_eq. Local Open Scope ereal_scope. -Context d (T : sigmaRingType d) (R : realType). +Context d (T : sigmaRingType d) (R : realType) (U V : Type). Variables (mu : {measure set T -> \bar R}) (D : set T). -Implicit Types f g h i : T -> \bar R. +Local Notation ae_eq f g := (\forall x \ae mu, D x -> f x = g x). -Definition ae_eq f g := {ae mu, forall x, D x -> f x = g x}. - -Lemma ae_eq0 f g : measurable D -> mu D = 0 -> ae_eq f g. +Lemma ae_eq0 (f g : T -> U) : measurable D -> mu D = 0 -> f = g %[ae mu in D]. Proof. by move=> mD D0; exists D; split => // t/= /not_implyP[]. Qed. -Lemma ae_eq_comp (j : \bar R -> \bar R) f g : +Lemma ae_eq_comp (j : U -> V) f g : ae_eq f g -> ae_eq (j \o f) (j \o g). Proof. by apply: filterS => x /[apply] /= ->. Qed. -Lemma ae_eq_funeposneg f g : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-. +Lemma ae_eq_funeposneg (f g : T -> \bar R) : + ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-. Proof. -split=> [fg|[]]. - split; apply: filterS fg => x /[apply]. - by rewrite !funeposE => ->. - by rewrite !funenegE => ->. -apply: filterS2 => x + + Dx => /(_ Dx) fg /(_ Dx) gf. -by rewrite (funeposneg f) (funeposneg g) fg gf. -Qed. +split=> [fg|[pfg nfg]]. + by split; near=> x => Dx; rewrite !(funeposE,funenegE) (near fg). +by near=> x => Dx; rewrite (funeposneg f) (funeposneg g) ?(near pfg, near nfg). +Unshelve. all: by end_near. Qed. +Implicit Types (f g : T -> U). Lemma ae_eq_refl f : ae_eq f f. Proof. exact/aeW. Qed. Lemma ae_eq_sym f g : ae_eq f g -> ae_eq g f. @@ -4174,14 +4178,11 @@ Proof. by apply: filterS => x /[apply] /= ->. Qed. End ae_eq. Section ae_eq_lemmas. -Context d (T : sigmaRingType d) (R : realType). -Implicit Types mu : {measure set T -> \bar R}. +Context d (T : sigmaRingType d) (R : realType) (U : Type). +Implicit Types (mu : {measure set T -> \bar R}) (A : set T) (f g : T -> U). Lemma ae_eq_subset mu A B f g : B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g. -Proof. -move=> BA [N [mN N0 fg]]; exists N; split => //. -by apply: subset_trans fg; apply: subsetC => z /= /[swap] /BA ? ->. -Qed. +Proof. by move=> BA; apply: filterS => x + /BA; apply. Qed. End ae_eq_lemmas. @@ -5308,7 +5309,7 @@ Notation "m1 `<< m2" := (measure_dominates m1 m2). Section absolute_continuity_lemmas. Context d (T : measurableType d) (R : realType). -Implicit Types m : {measure set T -> \bar R}. +Implicit Types (m : {measure set T -> \bar R}) (f g : T -> U). Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E -> m2 `<< m1 -> ae_eq m1 E f g -> ae_eq m2 E f g. From c22517e4d586ab6f7736e36404874ecc17aa200e Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Tue, 28 Jan 2025 18:11:08 +0100 Subject: [PATCH 06/18] improvements - more generalizations of ae_eq - hoelder.v doc - better interface in lspace.v --- theories/charge.v | 9 +- theories/hoelder.v | 56 +---- theories/lebesgue_integral.v | 3 + theories/lspace.v | 435 +++++++++++++++++++++++++---------- theories/measure.v | 98 ++++++-- 5 files changed, 412 insertions(+), 189 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 0c8d846c9f..d9a8c59484 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1866,10 +1866,7 @@ have nuf A : d.-measurable A -> nu A = \int[mu]_(x in A) f x. move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //. - exact/measurable_funTS. - exact/measurable_funTS. -- move: ff'. - have := @ae_eq_subset _ _ _ mu setT A f f'. - apply: ae_eq_subset. -- exact: ae_eq_subset ff'. +- exact: (@ae_eq_subset _ _ _ _ mu setT A f f' (@subsetT _ A)). Qed. End radon_nikodym_sigma_finite. @@ -2095,6 +2092,10 @@ move=> mE; apply: integral_ae_eq => //. by rewrite -Radon_Nikodym_SigmaFinite.f_integral. Qed. +(* TODO: move back to measure.v, current version incompatible *) +Lemma ae_eq_mul2l (f g h : T -> \bar R) D : f = g %[ae mu in D] -> (h \* f) = (h \* g) %[ae mu in D]. +Proof. by apply: filterS => x /= /[apply] ->. Qed. + Lemma Radon_Nikodym_change_of_variables f E : measurable E -> nu.-integrable E f -> \int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) = diff --git a/theories/hoelder.v b/theories/hoelder.v index e4b0f88d75..a3674c84cb 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -10,10 +10,10 @@ From mathcomp Require Import numfun exp convex interval_inference. (**md**************************************************************************) (* # Hoelder's Inequality *) (* *) -(* This file provides Hoelder's inequality. *) +(* This file provides Hoelder's inequality and its consequences, most notably *) +(* Minkowski's inequality and the convexity of the power function. *) (* ``` *) -(* 'N[mu]_p[f] := (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 *) -(* The corresponding definition is Lnorm. *) +(* 'N[mu]_p[f] == the p-norm of f with measure mu *) (* ``` *) (* *) (******************************************************************************) @@ -93,7 +93,7 @@ move=> r0; rewrite unlock (negbTE r0) -poweRrM mulVf// poweRe1//. by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0. Qed. -Lemma opp_Lnorm f p : +Lemma oppr_Lnorm f p : 'N_p[-%R \o f] = 'N_p[f]. Proof. rewrite unlock /Lnorm. @@ -527,49 +527,15 @@ Lemma minkowski' f g p : 'N_p%:E[f] <= 'N_p%:E[f \+ g] + 'N_p%:E[g]. Proof. move=> mf mg p1. -rewrite (_ : f = ((f \+ g) \+ (-%R \o g))%R); last admit. -rewrite [X in _ <= 'N__[X] + _](_ : ((f \+ g \- g) \+ g)%R = (f \+ g)%R); last admit. -rewrite (_ : 'N__[g] = 'N_p%:E[-%R \o g]); last admit. +rewrite (_ : f = ((f \+ g) \+ (-%R \o g))%R); last first. + by apply: funext => x /=; rewrite -addrA subrr addr0. +rewrite [X in _ <= 'N__[X] + _](_ : ((f \+ g \- g) \+ g)%R = (f \+ g)%R); last first. + by apply: funext => x /=; rewrite -addrA [X in _ + _ + X]addrC subrr addr0. +rewrite (_ : 'N__[g] = 'N_p%:E[-%R \o g]); last first. + by rewrite oppr_Lnorm. apply: minkowski => //. apply: measurable_funD => //. apply: measurableT_comp => //. -Admitted. +Qed. End minkowski. - -Section Lnorm_properties. -Context d {T : measurableType d} {R : realType}. -Variable mu : {measure set T -> \bar R}. -Local Open Scope ereal_scope. -Implicit Types (p : \bar R) (f g : T -> R) (r : R). - -Lemma LnormD_fin_num p f g : - 1 <= p -> - measurable_fun setT f -> measurable_fun setT g -> - 'N[mu]_p[f] \is a fin_num -> 'N[mu]_p[g] \is a fin_num -> - 'N[mu]_p[f \+ g] \is a fin_num. -Proof. -case: p => [p|_|]. -- move=> p1 mf mg Nffin Ngfin. - rewrite fin_numElt (@lt_le_trans _ _ 0)//= ?Lnorm_ge0//. - rewrite (@le_lt_trans _ _ ('N[mu]_p%:E[f] + 'N[mu]_p%:E[g]))//. - apply: minkowski => //. - by rewrite lte_add_pinfty// -ge0_fin_numE// Lnorm_ge0. -- move=> mf mg. - rewrite unlock /Lnorm. - case: ifPn => // mu_ge0. - rewrite !fin_numElt => /andP[_ fley] /andP[_ gley]. - rewrite (@lt_le_trans _ _ 0)//= ?ess_sup_ge0//; last first. - move=> t/=; exact: normr_ge0. - admit. -- by rewrite leeNy_eq => /eqP. -Admitted. - -Lemma LnormD_pinfty p f g : - 1 <= p -> measurable_fun setT f -> measurable_fun setT g -> - 'N[mu]_p[f] = +oo -> 'N[mu]_p[f \+ g] = +oo. -Proof. -case: p => [p||]. -- move=> p1 mf mg. - -End Lnorm_properties. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 008a388b58..d21d39f54d 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -273,6 +273,8 @@ Lemma mfunN f : - f = \- f :> (_ -> _). Proof. by []. Qed. Lemma mfunD f g : f + g = f \+ g :> (_ -> _). Proof. by []. Qed. Lemma mfunB f g : f - g = f \- g :> (_ -> _). Proof. by []. Qed. Lemma mfunM f g : f * g = f \* g :> (_ -> _). Proof. by []. Qed. +Lemma mfunMn f n : (f *+ n) = (fun x => f x *+ n) :> (_ -> _). +Proof. by apply/funext=> x; elim: n => //= n; rewrite !mulrS !mfunD /= => ->. Qed. Lemma mfun_sum I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. @@ -286,6 +288,7 @@ HB.instance Definition _ f g := MeasurableFun.copy (f \+ g) (f + g). HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f). HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g). HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g). +(* TODO: fix this: HB.instance Definition _ f (n : nat) := MeasurableFun.copy (fun x => f x *+ n) (f *+ n). *) Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D. diff --git a/theories/lspace.v b/theories/lspace.v index f8c3ad6901..7da76be76a 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -28,35 +28,40 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. +Definition finite_norm d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) := + ('N[ mu ]_p [ f ] < +oo)%E. + HB.mixin Record isLfun d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) := { - measurable_lfun : measurable_fun [set: T] f ; - lfuny : ('N[ mu ]_p [ f ] < +oo)%E + (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) (f : T -> R) + of @MeasurableFun d _ T R f := { + lfuny : finite_norm mu p f }. #[short(type=LfunType)] HB.structure Definition Lfun d (T : measurableType d) (R : realType) - (mu : {measure set T -> \bar R}) (p : \bar R) := - {f : T -> R & isLfun d T R mu p f}. + (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) := + {f of @MeasurableFun d _ T R f & isLfun d T R mu p p1 f}. -#[global] Hint Resolve measurable_lfun : core. Arguments lfuny {d} {T} {R} {mu} {p} _. #[global] Hint Resolve lfuny : core. +#[global] Hint Extern 0 (@LfunType _ _ _ _ _) => + solve [apply: lfuny] : core. Section Lfun_canonical. Context d (T : measurableType d) (R : realType). -Variables (mu : {measure set T -> \bar R}) (p : \bar R). +Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E). -HB.instance Definition _ := gen_eqMixin (LfunType mu p). -HB.instance Definition _ := gen_choiceMixin (LfunType mu p). +HB.instance Definition _ := gen_eqMixin (LfunType mu p1). +HB.instance Definition _ := gen_choiceMixin (LfunType mu p1). End Lfun_canonical. Section Lequiv. Context d (T : measurableType d) (R : realType). -Variables (mu : {measure set T -> \bar R}) (p : \bar R). +Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E). -Definition Lequiv (f g : LfunType mu p) := `[< f = g [%ae mu] >]. +Definition Lequiv (f g : LfunType mu p1) := `[< f = g %[ae mu] >]. Let Lequiv_refl : reflexive Lequiv. Proof. @@ -65,12 +70,12 @@ Qed. Let Lequiv_sym : symmetric Lequiv. Proof. -by move=> f g; apply/idP/idP => /asboolP h; apply/asboolP; exact: filterS h. +by move=> f g; apply/idP/idP => /asboolP h; apply/asboolP/ae_eq_sym. Qed. Let Lequiv_trans : transitive Lequiv. Proof. -by move=> f g h /asboolP gf /asboolP fh; apply/asboolP/(filterS2 _ _ gf fh) => x ->. +by move=> f g h /asboolP gf /asboolP fh; apply/asboolP/(ae_eq_trans gf fh). Qed. Canonical Lequiv_canonical := @@ -84,12 +89,12 @@ Canonical LspaceType_eqType := [the eqType of LspaceType]. Canonical LspaceType_choiceType := [the choiceType of LspaceType]. Canonical LspaceType_eqQuotType := [the eqQuotType Lequiv of LspaceType]. -Lemma LequivP (f g : LfunType mu p) : +Lemma LequivP (f g : LfunType mu p1) : reflect (f = g %[ae mu]) (f == g %[mod LspaceType]). Proof. by apply/(iffP idP); rewrite eqmodE// => /asboolP. Qed. Record LType := MemLType { Lfun_class : LspaceType }. -Coercion LfunType_of_LType (f : LType) : LfunType mu p := +Coercion LfunType_of_LType (f : LType) : LfunType mu p1 := repr (Lfun_class f). End Lequiv. @@ -98,25 +103,31 @@ Section Lspace. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. -Definition Lspace p := [set: LType mu p]. +Definition Lspace p (p1 : (1 <= p)%E) := [set: LType mu p1]. Arguments Lspace : clear implicits. -Lemma LType1_integrable (f : LType mu 1) : mu.-integrable setT (EFin \o f). +Lemma LType1_integrable (f : LType mu (@lexx _ _ 1%E)) : mu.-integrable setT (EFin \o f). Proof. apply/integrableP; split; first exact/EFin_measurable_fun. -have := lfuny f. -rewrite unlock /Lnorm ifF ?oner_eq0// invr1 poweRe1; last first. +have := lfuny _ f. +rewrite /finite_norm unlock /Lnorm ifF ?oner_eq0// invr1 poweRe1; last first. by apply integral_ge0 => x _; rewrite lee_fin powRr1//. by under eq_integral => i _ do rewrite powRr1//. Qed. -Lemma LType2_integrable_sqr (f : LType mu 2%:E) : +Let le12 : (1 <= 2%:E :> \bar R)%E. +rewrite lee_fin. +rewrite (ler_nat _ 1 2). +by []. +Qed. + +Lemma LType2_integrable_sqr (f : LType mu le12) : mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)). Proof. apply/integrableP; split. - exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f)/measurable_lfun. + exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f). rewrite (@lty_poweRy _ _ (2^-1))//. -rewrite (le_lt_trans _ (lfuny f))//. +rewrite (le_lt_trans _ (lfuny _ f))//. rewrite unlock /Lnorm ifF ?gt_eqF//. rewrite gt0_ler_poweR//. - by rewrite in_itv/= integral_ge0// leey. @@ -124,27 +135,219 @@ rewrite gt0_ler_poweR//. by rewrite lee_fin powR_ge0. rewrite ge0_le_integral//. - apply: measurableT_comp => //. - exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f)/measurable_lfun. + exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f). - by move=> x _; rewrite lee_fin powR_ge0. -- exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R)/measurableT_comp/measurable_lfun. +- exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R)/measurableT_comp. - by move=> t _/=; rewrite lee_fin normrX powR_mulrn. Qed. End Lspace. Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope. +(* move to hoelder.v *) +Section conjugate. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : \bar R). +Hypothesis (p1 : (1 <= p)%E). + +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. + +Definition conjugate := + match p with + | r%:E => [get q : R | r^-1 + q^-1 = 1]%:E + | +oo => 1 + | -oo => 0 + end. + +Lemma conjugateE : + conjugate = if p is r%:E then (r * (r-1)^-1)%:E + else if p == +oo then 1 else 0. +Proof. +rewrite /conjugate. +move: p1. +case: p => [r|//=|//]. +rewrite lee_fin => r1. +have r0 : r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1). +congr (_%:E). +apply: get_unique. + by rewrite invf_div mulrBl divff// mul1r addrCA subrr addr0. +move=> /= y h0. +suffices -> : y = (1 - r^-1)^-1. + by rewrite -(mul1r r^-1) -{1}(divff r0) -mulrBl invf_div. +by rewrite -h0 -addrAC subrr add0r invrK. +Qed. + +End conjugate. + + +Section lfun_pred. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : \bar R). + +Definition finlfun : {pred _ -> _} := mem [set f | finite_norm mu p f]. +Definition lfun : {pred _ -> _} := [predI @mfun _ _ T R & finlfun]. +Definition lfun_key : pred_key lfun. Proof. exact. Qed. +Canonical lfun_keyed := KeyedPred lfun_key. +Lemma sub_lfun_mfun : {subset lfun <= mfun}. Proof. by move=> x /andP[]. Qed. +Lemma sub_lfun_finlfun : {subset lfun <= finlfun}. Proof. by move=> x /andP[]. Qed. +End lfun_pred. + + +Lemma minkowskie : +forall [d : measure_display] [T : measurableType d] [R : realType] + (mu : measure T R) [f g : T -> R] [p : \bar R], +measurable_fun [set: T] f -> +measurable_fun [set: T] g -> +(1 <= p)%E -> ('N[mu]_p[(f \+ g)%R] <= 'N[mu]_p[f] + 'N[mu]_p[g])%E. +(* TODO: Jairo is working on this *) +Admitted. + + +Section lfun. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E). + +Notation lfun := (@lfun _ T R mu p). +Section Sub. +Context (f : T -> R) (fP : f \in lfun). +Definition lfun_Sub1_subproof := + @isMeasurableFun.Build d _ T R f (set_mem (sub_lfun_mfun fP)). +#[local] HB.instance Definition _ := lfun_Sub1_subproof. +Definition lfun_Sub2_subproof := + @isLfun.Build d T R mu p p1 f (set_mem (sub_lfun_finlfun fP)). + +Import HBSimple. + +#[local] HB.instance Definition _ := lfun_Sub2_subproof. +Definition lfun_Sub : LfunType mu p1 := f. +End Sub. + +Lemma lfun_rect (K : LfunType mu p1 -> Type) : + (forall f (Pf : f \in lfun), K (lfun_Sub Pf)) -> forall u, K u. +Proof. +move=> Ksub [f [[Pf1] [Pf2]]]. +have Pf : f \in lfun by apply/andP; rewrite ?inE. +have -> : Pf1 = set_mem (sub_lfun_mfun Pf) by []. +have -> : Pf2 = set_mem (sub_lfun_finlfun Pf) by []. +exact: Ksub. +Qed. + +Lemma lfun_valP f (Pf : f \in lfun) : lfun_Sub Pf = f :> (_ -> _). +Proof. by []. Qed. + +HB.instance Definition _ := isSub.Build _ _ (LfunType mu p1) lfun_rect lfun_valP. + +Lemma lfuneqP (f g : LfunType mu p1) : f = g <-> f =1 g. +Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed. + +HB.instance Definition _ := [Choice of LfunType mu p1 by <:]. + +Import numFieldNormedType.Exports. + +Lemma ess_sup_cst_lty r : (0 < mu setT)%E -> (ess_sup mu (cst r) < +oo)%E. +Proof. +rewrite /ess_sup => mu0. +under eq_set do rewrite preimage_cst/=. +rewrite ereal_inf_EFin ?ltry//. +- exists r => x/=; case: ifPn => [_|]. + by move: mu0 => /[swap] ->; rewrite ltNge lexx. + by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. +by exists r => /=; rewrite ifF//; rewrite set_itvE; + rewrite memNset //=; apply/negP; rewrite -real_leNgt ?num_real. +Qed. + +Lemma ess_sup_cst r : (0 < mu setT)%E -> (ess_sup mu (cst r) = r%:E)%E. +Proof. +rewrite /ess_sup => mu0. +under eq_set do rewrite preimage_cst/=. +rewrite ereal_inf_EFin. +- congr (_%:E). + rewrite [X in inf X](_ : _ = `[r, +oo[%classic); last first. + apply/seteqP; split => /=x/=. + case: ifPn => [_|]; first by move: mu0=> /[swap] ->; rewrite ltNge lexx. + by rewrite set_itvE notin_setE/= ltNge in_itv andbT/= => /negP /negPn. + rewrite in_itv/= => /andP[x0 _]. + by rewrite ifF// set_itvE; apply/negP; rewrite in_setE/= ltNge => /negP. + by rewrite inf_itv. +- exists r => x/=; case: ifPn => [_|]. + by move: mu0 => /[swap] ->; rewrite ltNge lexx. + by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. +by exists r => /=; rewrite ifF//; rewrite set_itvE; + rewrite memNset //=; apply/negP; rewrite -real_leNgt ?num_real. +Qed. + +Lemma Lnorm0 : 'N[mu]_p[cst 0] = 0. +Proof. +rewrite unlock /Lnorm. +move: p1. +case: p => [r||//]. +- rewrite lee_fin => r1. + have r0: r != 0 by rewrite gt_eqF// (lt_le_trans _ r1). + rewrite gt_eqF ?(lt_le_trans _ r1)//. + under eq_integral => x _ do rewrite /= normr0 powR0//. + by rewrite integral0 poweR0r// invr_neq0. +case: ifPn => //mu0 _. +rewrite (_ : normr \o _ = 0); last by apply: funext => x/=; rewrite normr0. +exact: ess_sup_cst. +Qed. + +Lemma lfuny0 : finite_norm mu p (cst 0). +Proof. by rewrite /finite_norm Lnorm0. Qed. + +HB.instance Definition _ := @isLfun.Build d T R mu p p1 (cst 0) lfuny0. + +Lemma mfunP (f : {mfun T >-> R}) : (f : T -> R) \in mfun. +Proof. exact: valP. Qed. + +Lemma lfunP (f : LfunType mu p1) : (f : T -> R) \in lfun. +Proof. exact: valP. Qed. + +Lemma mfun_scaler_closed : scaler_closed (@mfun _ _ T R). +Proof. move=> a/= f; rewrite !inE; exact: measurable_funM. Qed. + +HB.instance Definition _ := GRing.isScaleClosed.Build _ _ (@mfun _ _ T R) + mfun_scaler_closed. +HB.instance Definition _ := [SubZmodule_isSubLmodule of {mfun T >-> R} by <:]. + +Lemma LnormZ (f : LfunType mu p1) a : ('N[mu]_p[a \*: f] = `|a|%:E * 'N[mu]_p[f])%E. +Admitted. + +Lemma lfun_submod_closed : submod_closed (lfun). +Proof. +split. + rewrite -[0]/(cst 0). exact: lfunP. +move=> a/= f g fP gP. +rewrite -[f]lfun_valP -[g]lfun_valP. +move: (lfun_Sub _) (lfun_Sub _) => {fP} f {gP} g. +rewrite !inE rpredD ?rpredZ ?mfunP//=. +apply: mem_set => /=. +rewrite /finite_norm. +apply: (le_lt_trans (minkowskie _ _ _ _)) => //=. + suff: a *: (g : T -> R) \in mfun by exact: set_mem. + by rewrite rpredZ//; exact: mfunP. +rewrite lte_add_pinfty//; last exact: lfuny. +by rewrite LnormZ lte_mul_pinfty//; exact: lfuny. +Qed. + +HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ lfun + lfun_submod_closed. +HB.instance Definition _ := [SubChoice_isSubLmodule of LfunType mu p1 by <:]. + +End lfun. + Section Lspace_norm. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. -Variable (p : R). (* add hypothesis p > 1 *) +Variable (p : \bar R) (p1 : (1 <= p)%E). (* 0 - + should come with proofs that they are in LfunType mu p *) -Notation ty := (T -> R). -Definition nm f := fine ('N[mu]_p%:E[f]). +Notation ty := (LfunType mu p1). +Definition nm f := fine ('N[mu]_p[f]). -(* Program Definition fct_zmodMixin := *) -(* @GRing.isZmodule.Build (LfunType mu p%:E) 0 (fun f x => - f x) (fun f g => f \+ g). *) + +(* HB.instance Definition _ := GRing.Zmodule.on ty. *) (* measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R *) @@ -154,110 +357,110 @@ Definition nm f := fine ('N[mu]_p%:E[f]). (* HB.instance Definition _ := GRing.Zmodule.on ty. *) Lemma ler_Lnorm_add (f g : ty) : - nm (f \+ g) <= nm f + nm g. + nm (f + g) <= nm f + nm g. Proof. -rewrite /nm. -have : (-oo < 'N[mu]_p%:E[f])%E by exact: (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _)). -have : (-oo < 'N[mu]_p%:E[g])%E by exact: (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _)). -rewrite !ltNye_eq => /orP[f_fin /orP[g_fin|/eqP foo]|/eqP goo]. -- rewrite -fineD ?fine_le//. - - admit. - - by rewrite fin_numD f_fin g_fin//. - rewrite minkowski//. admit. admit. admit. -- rewrite foo/= add0r. - have : ('N[mu]_p%:E[f] <= 'N[mu]_p%:E[(f \+ g)])%E. - rewrite unlock /Lnorm. - rewrite {1}(@ifF _ (p == 0)). - rewrite {1}(@ifF _ (p == 0)). - rewrite gt0_ler_poweR. - - by []. - - admit. - - admit. - - admit. - rewrite ge0_le_integral//. - - move => x _. rewrite lee_fin powR_ge0//. - - admit. - - move => x _. rewrite lee_fin powR_ge0//. - - admit. - - move => x _. rewrite lee_fin gt0_ler_powR//. admit. (* rewrite normr_le. *) - -Admitted. +rewrite /nm -fineD ?fine_le ?minkowskie// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=. +- rewrite (le_lt_trans (minkowskie _ _ _ _))//. + by rewrite lte_add_pinfty//; exact: lfuny. +- by rewrite lte_add_pinfty//; exact: lfuny. +- by rewrite adde_ge0 ?Lnorm_ge0. +all: exact: lfuny. +Qed. Lemma natmulfctE (U : pointedType) (K : ringType) (f : U -> K) n : f *+ n = (fun x => f x *+ n). Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed. +Lemma LnormN (f : ty) : nm (\-f) = nm f. +Proof. by rewrite /nm oppr_Lnorm. Qed. -Lemma Lnorm_eq0 f : nm f = 0 -> {ae mu, f =1 0}. -rewrite /nm => /eqP. -rewrite fine_eq0; last first. admit. -move/eqP/Lnorm_eq0_eq0. -(* ale: I don't think it holds almost everywhere equal does not mean equal * -rewrite unlock /Lnorm ifF. -rewrite poweR_eq0. -rewrite integral_abs_eq0. *) -Admitted. +Lemma enatmul_ninfty (n : nat) : (-oo *+ n.+1 = -oo :> \bar R)%E \/ (-oo *+ n.+1 = +oo :> \bar R)%E. +Proof. by elim: n => //=[|n []->]; rewrite ?addNye; left. Qed. + +Lemma Lnorm_natmul (f : ty) k : nm (f *+ k) = nm f *+ k. +Proof. +rewrite /nm -scaler_nat LnormZ fineM//= ?normr_nat ?mulr_natl// fin_numElt. +have := lfuny p1 f. +by rewrite /finite_norm (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _)) => ->. +Qed. -Lemma Lnorm_natmul f k : nm (f *+ k) = nm f *+ k. -rewrite /nm unlock /Lnorm. -case: (ifP (p == 0)). - admit. - -move => p0. -under eq_integral => x _. - rewrite -mulr_natr/=. - rewrite fctE (_ : k%:R _ = k%:R); last by rewrite natmulfctE. - rewrite normrM powRM//=. - rewrite mulrC EFinM. - over. -rewrite /=. -rewrite integralZl//; last first. admit. -rewrite poweRM; last 2 first. -- by rewrite lee_fin powR_ge0. -- by rewrite integral_ge0// => x _; rewrite lee_fin powR_ge0. - -rewrite poweR_EFin -powRrM mulfV; last admit. -rewrite powRr1//. -rewrite fineM//; last admit. -rewrite mulrC. -Admitted. +HB.about Num.Zmodule_isSemiNormed.Build. -Lemma LnormN f : nm (-f) = nm f. -rewrite /nm. -congr (fine _). -rewrite unlock /Lnorm. -case: ifP. -move=> p0. - admit. - -move=> p0. -congr (_ `^ _)%E. -apply eq_integral => x _. -congr ((_ `^ _)%:E). -by rewrite normrN. -Admitted. +(* TODO : fix the definition *) +HB.instance Definition _ := + @Num.Zmodule_isSemiNormed.Build R (LfunType mu p1) + nm ler_Lnorm_add Lnorm_natmul LnormN. -(* -Lemma ler_Lnorm_add f g : - 'N[mu]_p%:E[(f \+ g)%R] <= 'N[mu]_p%:E[f] + 'N[mu]_p%:E[g]. -Admitted. +(* todo: add equivalent of mx_normZ and HB instance *) -Lemma Lnorm_eq0 f : 'N[mu]_p%:E[f] = 0 -> f = 0%R. -Admitted. +Lemma ess_sup_ger f (r : R) : (forall x, f x <= r) -> (ess_sup mu f <= r%:E)%E. +Proof. +move=> fr. +rewrite /ess_sup. +apply: ereal_inf_le. +apply/exists2P. +exists r%:E => /=; split => //. +apply/exists2P. +exists r; split => //. +rewrite preimage_itvoy. +suffices -> : [set x | r < f x] = set0 by []. +apply/seteqP; split => x //=. +rewrite lt_neqAle => /andP[rneqfx rlefx]. +move: (fr x) => fxler. +have: (f x <= r <= f x) by rewrite rlefx fxler. +by move/le_anti; move: rneqfx => /[swap] -> /eqP. +Qed. -Lemma Lnorm_natmul f k : 'N[mu]_p%:E [f *+ k]%R = 'N[mu]_p%:E [f] *+ k. +Lemma ess_sup_eq0 (f : {mfun T >-> R}) : ess_sup mu (normr \o f) = 0 -> f = 0 %[ae mu]. Admitted. -Lemma LnormN f : 'N[mu]_p%:E [- f]%R = 'N[mu]_p%:E [f]. -Admitted. -*) -HB.instance Definition _ := - @Num.Zmodule_isSemiNormed.Build R (*LType mu p%:E*) ty - nm ler_Lnorm_add Lnorm_natmul LnormN. +(* TODO: move to hoelder *) +Lemma Lnorm_eq0_eq0 (f : {mfun T >-> R}) : (0 < p)%E -> + 'N[mu]_p[f] = 0 -> f = 0 %[ae mu]. +Proof. +rewrite unlock /Lnorm => p0. +move: p0. +case: p => [r r0||]. +- case: ifPn => _. + rewrite preimage_setI preimage_setT setTI -preimage_setC => /negligibleP. + move/(_ (measurableC _)); rewrite -[X in d.-measurable X]setTI. + move/(_ (measurable_funP _ measurableT _ (measurable_set1 _))) => /=. + by case => A [mA muA0 fA]; exists A; split => // x/= ?; exact: fA. + move=> /poweR_eq0_eq0. + move=> /(_ (integral_ge0 _ _)) h. + have: (\int[mu]_x (`|f x| `^ r)%:E)%E = 0 by apply: h => x _; rewrite lee_fin powR_ge0. + under eq_integral => x _ do rewrite -[_%:E]gee0_abs ?lee_fin ?powR_ge0//. + have mp: measurable_fun [set: T] (fun x : T => (`|f x| `^ r)%:E). + apply: measurableT_comp => //. + apply (measurableT_comp (measurable_powR _)) => //. + apply: measurableT_comp => //. + move/(ae_eq_integral_abs _ measurableT mp). + apply: filterS => x/= /[apply]. + by case=> /powR_eq0_eq0 /eqP; rewrite normr_eq0 => /eqP. +- case: ifPn => [mu0 _|]. + exact: ess_sup_eq0. + rewrite ltNge => /negbNE mu0 _ _. + suffices mueq0: mu setT = 0 by exact: ae_eq0. + move: mu0 (measure_ge0 mu setT) => mu0 mu1. + suffices: (mu setT <= 0 <= mu setT)%E by move/le_anti. + by rewrite mu0 mu1. +by []. +Qed. + + +Lemma Lnorm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. +Proof. +have: 'N[mu]_p[f] \is a fin_num by + rewrite fin_numElt (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _))//=; exact: lfuny. +have p0 : (0 < p)%E by exact: lt_le_trans. +rewrite /nm => h /eqP. +rewrite fine_eq0//. +move/eqP. +exact: Lnorm_eq0_eq0. +Qed. -(* todo: add equivalent of mx_normZ and HB instance *) End Lspace_norm. diff --git a/theories/measure.v b/theories/measure.v index 730adf22ff..75fa432737 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4116,7 +4116,8 @@ Notation "{ 'ae' m , P }" := {near almost_everywhere m, P} : type_scope. Notation "\forall x \ae mu , P" := (\forall x \near almost_everywhere mu, P) (format "\forall x \ae mu , P", x name, P at level 200, at level 200): type_scope. -Notation ae_eq mu D f g := (\forall x \ae mu, D x -> f x = g x). +Definition ae_eq d (T : semiRingOfSetsType d) (R : realType) (mu : {measure set T -> \bar R}) + (V : T -> Type) D (f g : forall x, V x) := (\forall x \ae mu, D x -> f x = g x). Notation "f = g %[ae mu 'in' D ]" := (\forall x \ae mu, D x -> f x = g x) (format "f = g '%[ae' mu 'in' D ]", g at next level, D at level 200, at level 70). Notation "f = g %[ae mu ]" := (f = g %[ae mu in setT ]) @@ -4130,18 +4131,70 @@ move=> aP; have -> : P = setT by rewrite predeqE => t; split. by apply/negligibleP; [rewrite setCT|rewrite setCT measure0]. Qed. +Require Import -(notations) Setoid. + +Declare Scope signature_scope. +Delimit Scope signature_scope with signature. +Import -(notations) Morphisms. +Module ProperNotations. + + Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) + (right associativity, at level 55) : signature_scope. + + Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature)) + (right associativity, at level 55) : signature_scope. + + Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R'%signature)) + (right associativity, at level 55) : signature_scope. + +End ProperNotations. +Import ProperNotations. + +Arguments Proper {A}%_type R%_signature m. +Arguments respectful {A B}%_type (R R')%_signature _ _. + +Instance ae_eq_equiv d (T : ringOfSetsType d) R mu V D: Equivalence (@ae_eq d T R mu V D). +Proof. +split. +- by move=> f; near=> x. +- by move=> f g eqfg; near=> x => Dx; rewrite (near eqfg). +- by move=> f g h eqfg eqgh; near=> x => Dx; rewrite (near eqfg) ?(near eqgh). +Unshelve. all: by end_near. Qed. + + + Section ae_eq. -Local Open Scope ereal_scope. -Context d (T : sigmaRingType d) (R : realType) (U V : Type). +Local Open Scope ring_scope. +Context d (T : sigmaRingType d) (R : realType). +Implicit Types (U V : Type) (W : nzRingType). Variables (mu : {measure set T -> \bar R}) (D : set T). -Local Notation ae_eq f g := (\forall x \ae mu, D x -> f x = g x). +Local Notation ae_eq := (ae_eq mu D). -Lemma ae_eq0 (f g : T -> U) : measurable D -> mu D = 0 -> f = g %[ae mu in D]. +Lemma ae_eq0 U (f g : T -> U) : measurable D -> mu D = 0 -> f = g %[ae mu in D]. Proof. by move=> mD D0; exists D; split => // t/= /not_implyP[]. Qed. -Lemma ae_eq_comp (j : U -> V) f g : +Instance comp_ae_eq U V (j : T -> U -> V) : Proper (ae_eq ==> ae_eq) (fun f x => j x (f x)). +Proof. by move=> f g; apply: filterS => x /[apply] /= ->. Qed. + +Instance comp_ae_eq2 U U' V (j : T -> U -> U' -> V) : Proper (ae_eq ==> ae_eq ==> ae_eq) (fun f g x => j x (f x) (g x)). +Proof. by move=> f f' + g g'; apply: filterS2 => x + + Dx => -> // ->. Qed. + +Instance comp_ae_eq2' U U' V (j : U -> U' -> V) : Proper (ae_eq ==> ae_eq ==> ae_eq) (fun f g x => j (f x) (g x)). +Proof. by move=> f f' + g g'; apply: filterS2 => x + + Dx => -> // ->. Qed. + +Instance sub_ae_eq2 : Proper (ae_eq ==> ae_eq ==> ae_eq) (@GRing.sub_fun T R). +Proof. exact: (@comp_ae_eq2' _ _ R (fun x y => x - y)). Qed. + +Lemma ae_eq_refl U (f : T -> U) : ae_eq f f. Proof. exact/aeW. Qed. +Hint Resolve ae_eq_refl : core. + +Lemma ae_eq_comp U V (j : U -> V) f g : ae_eq f g -> ae_eq (j \o f) (j \o g). -Proof. by apply: filterS => x /[apply] /= ->. Qed. +Proof. by move->. Qed. + +Lemma ae_eq_comp2 U V (j : T -> U -> V) f g : + ae_eq f g -> ae_eq (fun x => j x (f x)) (fun x => j x (g x)). +Proof. by apply: filterS => x /[swap] + ->. Qed. Lemma ae_eq_funeposneg (f g : T -> \bar R) : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-. @@ -4151,28 +4204,25 @@ split=> [fg|[pfg nfg]]. by near=> x => Dx; rewrite (funeposneg f) (funeposneg g) ?(near pfg, near nfg). Unshelve. all: by end_near. Qed. -Implicit Types (f g : T -> U). -Lemma ae_eq_refl f : ae_eq f f. Proof. exact/aeW. Qed. - -Lemma ae_eq_sym f g : ae_eq f g -> ae_eq g f. -Proof. by apply: filterS => x + Dx => /(_ Dx). Qed. +Lemma ae_eq_sym U (f g : T -> U) : ae_eq f g -> ae_eq g f. +Proof. by symmetry. Qed. -Lemma ae_eq_trans f g h : ae_eq f g -> ae_eq g h -> ae_eq f h. -Proof. by apply: filterS2 => x + + Dx => /(_ Dx) ->; exact. Qed. +Lemma ae_eq_trans U (f g h : T -> U) : ae_eq f g -> ae_eq g h -> ae_eq f h. +Proof. by apply transitivity. Qed. -Lemma ae_eq_sub f g h i : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i). -Proof. by apply: filterS2 => x + + Dx => /(_ Dx) -> /(_ Dx) ->. Qed. +Lemma ae_eq_sub W (f g h i : T -> W) : ae_eq f g -> ae_eq h i -> ae_eq (f \- h) (g \- i). +Proof. by apply: filterS2 => x + + Dx => /= /(_ Dx) -> /(_ Dx) ->. Qed. -Lemma ae_eq_mul2r f g h : ae_eq f g -> ae_eq (f \* h) (g \* h). -Proof. by apply: filterS => x /[apply] ->. Qed. +Lemma ae_eq_mul2r W (f g h : T -> W) : ae_eq f g -> ae_eq (f \* h) (g \* h). +Proof. by move=>/(ae_eq_comp2 (fun x y => y * h x)). Qed. -Lemma ae_eq_mul2l f g h : ae_eq f g -> ae_eq (h \* f) (h \* g). -Proof. by apply: filterS => x /[apply] ->. Qed. +Lemma ae_eq_mul2l W (f g h : T -> W) : ae_eq f g -> ae_eq (h \* f) (h \* g). +Proof. by move=>/(ae_eq_comp2 (fun x y => h x * y)). Qed. -Lemma ae_eq_mul1l f g : ae_eq f (cst 1) -> ae_eq g (g \* f). -Proof. by apply: filterS => x /[apply] ->; rewrite mule1. Qed. +Lemma ae_eq_mul1l W (f g : T -> W) : ae_eq f (cst 1) -> ae_eq g (g \* f). +Proof. by apply: filterS => x /= /[apply] ->; rewrite mulr1. Qed. -Lemma ae_eq_abse f g : ae_eq f g -> ae_eq (abse \o f) (abse \o g). +Lemma ae_eq_abse (f g : T -> \bar R) : ae_eq f g -> ae_eq (abse \o f) (abse \o g). Proof. by apply: filterS => x /[apply] /= ->. Qed. End ae_eq. @@ -5308,7 +5358,7 @@ End absolute_continuity. Notation "m1 `<< m2" := (measure_dominates m1 m2). Section absolute_continuity_lemmas. -Context d (T : measurableType d) (R : realType). +Context d (T : measurableType d) (R : realType) (U : Type). Implicit Types (m : {measure set T -> \bar R}) (f g : T -> U). Lemma measure_dominates_ae_eq m1 m2 f g E : measurable E -> From 518f8df0345d8c474bf01a6784df860daa1c5399 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 7 Feb 2025 17:57:47 +0100 Subject: [PATCH 07/18] compressions --- theories/lspace.v | 21 ++++++++------------- 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 7da76be76a..8d8393c89a 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -277,22 +277,17 @@ by exists r => /=; rewrite ifF//; rewrite set_itvE; rewrite memNset //=; apply/negP; rewrite -real_leNgt ?num_real. Qed. -Lemma Lnorm0 : 'N[mu]_p[cst 0] = 0. +Lemma Lnorm0 : 'N[mu]_p[0] = 0. Proof. -rewrite unlock /Lnorm. -move: p1. -case: p => [r||//]. -- rewrite lee_fin => r1. - have r0: r != 0 by rewrite gt_eqF// (lt_le_trans _ r1). - rewrite gt_eqF ?(lt_le_trans _ r1)//. - under eq_integral => x _ do rewrite /= normr0 powR0//. - by rewrite integral0 poweR0r// invr_neq0. -case: ifPn => //mu0 _. -rewrite (_ : normr \o _ = 0); last by apply: funext => x/=; rewrite normr0. -exact: ess_sup_cst. +rewrite unlock /Lnorm; case: p p1 => [r| |//]; last first. + case: ifPn => // *; under [_ \o _]funext do rewrite /= normr0. + exact: ess_sup_cst. +rewrite lee_fin => r1; have r0 : r != 0 by rewrite gt_eqF// (lt_le_trans _ r1). +rewrite (negPf r0) integral0_eq ?poweR0r ?invr_eq0// => *. +by rewrite normr0 powR0. Qed. -Lemma lfuny0 : finite_norm mu p (cst 0). +Lemma lfuny0 : finite_norm mu p 0. Proof. by rewrite /finite_norm Lnorm0. Qed. HB.instance Definition _ := @isLfun.Build d T R mu p p1 (cst 0) lfuny0. From 5c3f3255374adca229de7b82031bb79bbf19f60a Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 8 Feb 2025 00:28:59 +0100 Subject: [PATCH 08/18] inclusion of lp spaces - refactoring - extension to Loo - measure 0 --- .nix/config.nix | 4 +- theories/hoelder.v | 75 ++++++++++--- theories/lspace.v | 257 +++++++++++++++++++++------------------------ theories/measure.v | 49 +++++++++ 4 files changed, 232 insertions(+), 153 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index b92ca6aa89..225ad16e8c 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -50,7 +50,7 @@ in ## will be created per bundle bundles."8.19".coqPackages = common-bundle // { coq.override.version = "8.19"; - mathcomp.override.version = "CohenCyril:seminorm"; + mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; }; @@ -75,7 +75,7 @@ in coq-elpi.override.version = "master"; coq-elpi.override.elpi-version = "2.0.7"; hierarchy-builder.override.version = "master"; - mathcomp.override.version = "CohenCyril:seminorm"; + mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; ssprove.job = false; diff --git a/theories/hoelder.v b/theories/hoelder.v index a3674c84cb..53687475cc 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -40,11 +40,11 @@ HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType} (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) := match p with | p%:E => (if p == 0%R then - mu (f @^-1` (setT `\ 0%R)) + (mu (f @^-1` (setT `\ 0%R))) else (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1)%E | +oo%E => (if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0)%E - | -oo%E => 0%E + | -oo%E => (if mu [set: T] > 0 then ess_inf mu (normr \o f) else 0)%E end. Canonical locked_Lnorm := Unlockable Lnorm.unlock. Arguments Lnorm {d T R} mu p f. @@ -57,6 +57,20 @@ Implicit Types (p : \bar R) (f g : T -> R) (r : R). Local Notation "'N_ p [ f ]" := (Lnorm mu p f). +Lemma Lnorm0 p : 1 <= p -> 'N_p[cst 0%R] = 0. +Proof. +rewrite unlock /Lnorm. +case: p => [r||//]. +- rewrite lee_fin => r1. + have r0: r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1). + rewrite gt_eqF ?(lt_le_trans _ r1)//. + under eq_integral => x _ do rewrite /= normr0 powR0//. + by rewrite integral0 poweR0r// invr_neq0. +case: ifPn => //mu0 _. +rewrite (_ : normr \o _ = 0%R); last by apply: funext => x/=; rewrite normr0. +exact: ess_sup_cst. +Qed. + Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E. Proof. rewrite unlock oner_eq0 invr1// poweRe1//. @@ -74,16 +88,36 @@ Qed. Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g]. Proof. by move=> fg; congr Lnorm; exact/funext. Qed. -Lemma Lnorm_eq0_eq0 r f : (0 < r)%R -> measurable_fun setT f -> - 'N_r%:E[f] = 0 -> ae_eq mu [set: T] (fun t => (`|f t| `^ r)%:E) (cst 0). +Lemma Lnorm_eq0_eq0 (f : T -> R) p : + measurable_fun setT f -> (0 < p)%E -> 'N_p[f] = 0 -> f = 0%R %[ae mu]. Proof. -move=> r0 mf; rewrite unlock (gt_eqF r0) => /poweR_eq0_eq0 fp. -apply/ae_eq_integral_abs => //=. - apply: measurableT_comp => //. - apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. - exact: measurableT_comp. -under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//. -by rewrite fp//; apply: integral_ge0 => t _; rewrite lee_fin powR_ge0. +rewrite unlock /Lnorm => mf. +case: p => [r r0||]. +- case: ifPn => _. + rewrite preimage_setI preimage_setT setTI -preimage_setC. + move=> /poweR_eq0_eq0 /negligibleP. + move/(_ (measurableC _)); rewrite -[X in d.-measurable X]setTI. + move/(_ (mf _ _ _)). + by case=> // A [mA muA0 fA]; exists A; split => // x/= ?; exact: fA. + move=> /poweR_eq0_eq0. + move=> /(_ (integral_ge0 _ _)) h. + have: (\int[mu]_x (`|f x| `^ r)%:E)%E = 0 by apply: h => x _; rewrite lee_fin powR_ge0. + under eq_integral => x _ do rewrite -[_%:E]gee0_abs ?lee_fin ?powR_ge0//. + have mp: measurable_fun [set: T] (fun x : T => (`|f x| `^ r)%:E). + apply: measurableT_comp => //. + apply (measurableT_comp (measurable_powR _)) => //. + exact: measurableT_comp. + move/(ae_eq_integral_abs _ measurableT mp). + apply: filterS => x/= /[apply]. + by case=> /powR_eq0_eq0 /eqP; rewrite normr_eq0 => /eqP. +- case: ifPn => [mu0 _|]. + exact: ess_sup_eq0. + rewrite ltNge => /negbNE mu0 _ _. + suffices mueq0: mu setT = 0 by exact: ae_eq0. + move: mu0 (measure_ge0 mu setT) => mu0 mu1. + suffices: (mu setT <= 0 <= mu setT)%E by move/le_anti. + by rewrite mu0 mu1. +by []. Qed. Lemma powR_Lnorm f r : r != 0%R -> @@ -94,11 +128,11 @@ by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0. Qed. Lemma oppr_Lnorm f p : - 'N_p[-%R \o f] = 'N_p[f]. + 'N_p[\- f]%R = 'N_p[f]. Proof. rewrite unlock /Lnorm. case: p => /= [r||//]. - case: eqP => _. congr (mu _). + case: eqP => _. congr ((mu _) `^ _). rewrite !preimage_setI. congr (_ `&` _). rewrite -!preimage_setC. @@ -113,9 +147,19 @@ rewrite compA (_ : normr \o -%R = normr)//. apply: funext => x/=; exact: normrN. Qed. +Lemma Lnorm_cst1 r : ('N_r%:E[cst 1%R] = (mu setT)`^(r^-1)). +Proof. +rewrite unlock /Lnorm. +case: ifPn => [_|]. + by rewrite preimage_cst ifT// inE/=; split => //; apply/eqP; rewrite oner_neq0. +under eq_integral => x _ do rewrite normr1 powR1 (_ : 1 = cst 1 x)%R// -indicT. +by rewrite integral_indic// setTI. +Qed. + End Lnorm_properties. #[global] + Hint Extern 0 (0 <= Lnorm _ _ _) => solve [apply: Lnorm_ge0] : core. Notation "'N[ mu ]_ p [ f ]" := (Lnorm mu p f). @@ -164,11 +208,12 @@ Let hoelder0 f g p q : measurable_fun setT f -> measurable_fun setT g -> (0 < p)%R -> (0 < q)%R -> (p^-1 + q^-1 = 1)%R -> 'N_p%:E[f] = 0 -> 'N_1[(f \* g)%R] <= 'N_p%:E[f] * 'N_q%:E[g]. Proof. +rewrite -lte_fin. move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//. rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0. - by do 2 apply: measurableT_comp => //; exact: measurable_funM. -- apply: filterS (Lnorm_eq0_eq0 p0 mf f0) => x /(_ I)[] /powR_eq0_eq0 + _. - by rewrite normrM => ->; rewrite mul0r. +- apply: filterS (Lnorm_eq0_eq0 mf p0 f0) => x /(_ I)[] + _. + by rewrite normrM => ->; rewrite normr0 mul0r. Qed. Let normalized p f x := `|f x| / fine 'N_p%:E[f]. diff --git a/theories/lspace.v b/theories/lspace.v index 8d8393c89a..60a3b887c1 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -245,49 +245,7 @@ HB.instance Definition _ := [Choice of LfunType mu p1 by <:]. Import numFieldNormedType.Exports. -Lemma ess_sup_cst_lty r : (0 < mu setT)%E -> (ess_sup mu (cst r) < +oo)%E. -Proof. -rewrite /ess_sup => mu0. -under eq_set do rewrite preimage_cst/=. -rewrite ereal_inf_EFin ?ltry//. -- exists r => x/=; case: ifPn => [_|]. - by move: mu0 => /[swap] ->; rewrite ltNge lexx. - by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. -by exists r => /=; rewrite ifF//; rewrite set_itvE; - rewrite memNset //=; apply/negP; rewrite -real_leNgt ?num_real. -Qed. - -Lemma ess_sup_cst r : (0 < mu setT)%E -> (ess_sup mu (cst r) = r%:E)%E. -Proof. -rewrite /ess_sup => mu0. -under eq_set do rewrite preimage_cst/=. -rewrite ereal_inf_EFin. -- congr (_%:E). - rewrite [X in inf X](_ : _ = `[r, +oo[%classic); last first. - apply/seteqP; split => /=x/=. - case: ifPn => [_|]; first by move: mu0=> /[swap] ->; rewrite ltNge lexx. - by rewrite set_itvE notin_setE/= ltNge in_itv andbT/= => /negP /negPn. - rewrite in_itv/= => /andP[x0 _]. - by rewrite ifF// set_itvE; apply/negP; rewrite in_setE/= ltNge => /negP. - by rewrite inf_itv. -- exists r => x/=; case: ifPn => [_|]. - by move: mu0 => /[swap] ->; rewrite ltNge lexx. - by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. -by exists r => /=; rewrite ifF//; rewrite set_itvE; - rewrite memNset //=; apply/negP; rewrite -real_leNgt ?num_real. -Qed. - -Lemma Lnorm0 : 'N[mu]_p[0] = 0. -Proof. -rewrite unlock /Lnorm; case: p p1 => [r| |//]; last first. - case: ifPn => // *; under [_ \o _]funext do rewrite /= normr0. - exact: ess_sup_cst. -rewrite lee_fin => r1; have r0 : r != 0 by rewrite gt_eqF// (lt_le_trans _ r1). -rewrite (negPf r0) integral0_eq ?poweR0r ?invr_eq0// => *. -by rewrite normr0 powR0. -Qed. - -Lemma lfuny0 : finite_norm mu p 0. +Lemma lfuny0 : finite_norm mu p (cst 0). Proof. by rewrite /finite_norm Lnorm0. Qed. HB.instance Definition _ := @isLfun.Build d T R mu p p1 (cst 0) lfuny0. @@ -305,8 +263,36 @@ HB.instance Definition _ := GRing.isScaleClosed.Build _ _ (@mfun _ _ T R) mfun_scaler_closed. HB.instance Definition _ := [SubZmodule_isSubLmodule of {mfun T >-> R} by <:]. -Lemma LnormZ (f : LfunType mu p1) a : ('N[mu]_p[a \*: f] = `|a|%:E * 'N[mu]_p[f])%E. -Admitted. +Lemma LnormZ (f : LfunType mu p1) a : + ('N[mu]_p[a \*: f] = `|a|%:E * 'N[mu]_p[f])%E. +Proof. +rewrite unlock /Lnorm. +move: p p1 f. +case=> //[r r1 f|]. + rewrite gt_eqF ?(lt_le_trans ltr01)//. + under eq_integral => x _/= do rewrite -mulr_algl scaler1 normrM powRM ?EFinM//. + rewrite integralZl//; last first. + apply /integrableP; split. + apply: measurableT_comp => //. + rewrite (_ : (fun x : T => `|f x| `^ r) = (@powR R)^~ r \o normr \o f)//. + by repeat apply: measurableT_comp => //. + apply: (@lty_poweRy _ _ r^-1). + by rewrite gt_eqF// invr_gt0 ?(lt_le_trans ltr01). + have -> : ((\int[mu]_x `|(`|f x| `^ r)%:E|) `^ r^-1 = 'N[mu]_r%:E[f])%E. + rewrite unlock /Lnorm gt_eqF ?(lt_le_trans ltr01)//. + by under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. + exact: (lfuny r1 f). + rewrite poweRM ?integral_ge0=> //[||x _]; rewrite ?lee_fin ?powR_ge0//. + by rewrite poweR_EFin -powRrM mulfV ?gt_eqF ?(lt_le_trans ltr01)// powRr1. +move=> p0 f. +case: ifP => mu0. + rewrite (_ : normr \o a \*: f = (`|a|) \*: (normr \o f)); last first. + by apply: funext => x/=; rewrite normrZ. + rewrite ess_supM//. + by near=> x=> /=. +by rewrite mule0. +Unshelve. end_near. +Qed. Lemma lfun_submod_closed : submod_closed (lfun). Proof. @@ -331,6 +317,7 @@ HB.instance Definition _ := [SubChoice_isSubLmodule of LfunType mu p1 by <:]. End lfun. + Section Lspace_norm. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. @@ -341,26 +328,14 @@ Variable (p : \bar R) (p1 : (1 <= p)%E). Notation ty := (LfunType mu p1). Definition nm f := fine ('N[mu]_p[f]). - -(* HB.instance Definition _ := GRing.Zmodule.on ty. *) - -(* measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R *) - -(* Notation ty := (LfunType mu p%:E). *) -(* Definition nm (f : ty) := fine ('N[mu]_p%:E[f]). *) - -(* HB.instance Definition _ := GRing.Zmodule.on ty. *) +Lemma finite_norm_fine (f : ty) : (nm f)%:E = 'N[mu]_p[f]. +Proof. +by rewrite /nm fineK// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=; exact: lfuny. +Qed. Lemma ler_Lnorm_add (f g : ty) : nm (f + g) <= nm f + nm g. -Proof. -rewrite /nm -fineD ?fine_le ?minkowskie// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=. -- rewrite (le_lt_trans (minkowskie _ _ _ _))//. - by rewrite lte_add_pinfty//; exact: lfuny. -- by rewrite lte_add_pinfty//; exact: lfuny. -- by rewrite adde_ge0 ?Lnorm_ge0. -all: exact: lfuny. -Qed. +Proof. by rewrite -lee_fin EFinD !finite_norm_fine minkowskie. Qed. Lemma natmulfctE (U : pointedType) (K : ringType) (f : U -> K) n : f *+ n = (fun x => f x *+ n). @@ -374,9 +349,8 @@ Proof. by elim: n => //=[|n []->]; rewrite ?addNye; left. Qed. Lemma Lnorm_natmul (f : ty) k : nm (f *+ k) = nm f *+ k. Proof. -rewrite /nm -scaler_nat LnormZ fineM//= ?normr_nat ?mulr_natl// fin_numElt. -have := lfuny p1 f. -by rewrite /finite_norm (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _)) => ->. +apply/EFin_inj; rewrite finite_norm_fine -scaler_nat LnormZ normr_nat. +by rewrite -[in RHS]mulr_natl EFinM finite_norm_fine. Qed. @@ -389,87 +363,98 @@ HB.instance Definition _ := (* todo: add equivalent of mx_normZ and HB instance *) -Lemma ess_sup_ger f (r : R) : (forall x, f x <= r) -> (ess_sup mu f <= r%:E)%E. +Lemma nm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. Proof. -move=> fr. -rewrite /ess_sup. -apply: ereal_inf_le. -apply/exists2P. -exists r%:E => /=; split => //. -apply/exists2P. -exists r; split => //. -rewrite preimage_itvoy. -suffices -> : [set x | r < f x] = set0 by []. -apply/seteqP; split => x //=. -rewrite lt_neqAle => /andP[rneqfx rlefx]. -move: (fr x) => fxler. -have: (f x <= r <= f x) by rewrite rlefx fxler. -by move/le_anti; move: rneqfx => /[swap] -> /eqP. -Qed. - -Lemma ess_sup_eq0 (f : {mfun T >-> R}) : ess_sup mu (normr \o f) = 0 -> f = 0 %[ae mu]. -Admitted. - - -(* TODO: move to hoelder *) -Lemma Lnorm_eq0_eq0 (f : {mfun T >-> R}) : (0 < p)%E -> - 'N[mu]_p[f] = 0 -> f = 0 %[ae mu]. -Proof. -rewrite unlock /Lnorm => p0. -move: p0. -case: p => [r r0||]. -- case: ifPn => _. - rewrite preimage_setI preimage_setT setTI -preimage_setC => /negligibleP. - move/(_ (measurableC _)); rewrite -[X in d.-measurable X]setTI. - move/(_ (measurable_funP _ measurableT _ (measurable_set1 _))) => /=. - by case => A [mA muA0 fA]; exists A; split => // x/= ?; exact: fA. - move=> /poweR_eq0_eq0. - move=> /(_ (integral_ge0 _ _)) h. - have: (\int[mu]_x (`|f x| `^ r)%:E)%E = 0 by apply: h => x _; rewrite lee_fin powR_ge0. - under eq_integral => x _ do rewrite -[_%:E]gee0_abs ?lee_fin ?powR_ge0//. - have mp: measurable_fun [set: T] (fun x : T => (`|f x| `^ r)%:E). - apply: measurableT_comp => //. - apply (measurableT_comp (measurable_powR _)) => //. - apply: measurableT_comp => //. - move/(ae_eq_integral_abs _ measurableT mp). - apply: filterS => x/= /[apply]. - by case=> /powR_eq0_eq0 /eqP; rewrite normr_eq0 => /eqP. -- case: ifPn => [mu0 _|]. - exact: ess_sup_eq0. - rewrite ltNge => /negbNE mu0 _ _. - suffices mueq0: mu setT = 0 by exact: ae_eq0. - move: mu0 (measure_ge0 mu setT) => mu0 mu1. - suffices: (mu setT <= 0 <= mu setT)%E by move/le_anti. - by rewrite mu0 mu1. -by []. -Qed. - - -Lemma Lnorm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. -Proof. -have: 'N[mu]_p[f] \is a fin_num by - rewrite fin_numElt (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _))//=; exact: lfuny. -have p0 : (0 < p)%E by exact: lt_le_trans. -rewrite /nm => h /eqP. -rewrite fine_eq0//. -move/eqP. -exact: Lnorm_eq0_eq0. +rewrite /nm=> /eqP; rewrite -eqe=> /eqP; rewrite finite_norm_fine=> /Lnorm_eq0_eq0. +by apply; rewrite ?(lt_le_trans _ p1). Qed. End Lspace_norm. -(* Section Lspace_inclusion. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. -Lemma Lspace_inclusion p q : (p <= q)%E -> - forall (f : LfunType mu q), ('N[ mu ]_p [ f ] < +oo)%E. -Proof. -move=> pleq f. +(* the following lemma is not needed, but looks useful, should we include it anyways? *) +Lemma mul_lte_pinfty (x y : \bar R) : (x \is a fin_num -> 0 < x -> x * y < +oo -> y < +oo)%E. +Proof. rewrite fin_numE => /andP[/eqP xNoo /eqP xoo]. +move: x xNoo xoo. +case => // r _ _ rgt0. +rewrite /mule. +case: y => //[r0 ?|]. + by rewrite ltry. +case: ifP => //. by move: rgt0 => /[swap] /eqP -> /eqP; rewrite ltxx. +case: ifP => //. by rewrite rgt0. +Qed. + +Local Open Scope ereal_scope. -isLfun d T R mu p f. +Lemma measure_is_zero : mu [set: T] = 0%E -> mu = mzero. +Admitted. + +Lemma Lspace_inclusion (p q : \bar R) : + forall (p1 : 1 <= p) (q1 : 1 <= q), + mu [set: T] < +oo -> p < q -> forall (f : {mfun T >-> R}), finite_norm mu q f -> finite_norm mu p f. +Proof. +have := measure_ge0 mu [set: T]; rewrite le_eqVlt => /orP[/eqP mu0 p1 q1 _ _ f _|mu_pos]. + rewrite /finite_norm unlock /Lnorm. + move: p p1; case=> //; last by rewrite -mu0 ltxx. + move=> r r1; rewrite gt_eqF ?(lt_le_trans ltr01)//. + rewrite measure_is_zero// integral_measure_zero. + by rewrite poweR0r// gt_eqF// invr_gt0 (lt_le_trans ltr01). +move: p q. +case=> //[p|]; case=> //[q|] p1 q1; last first. + have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). + move=> muoo _ f. + rewrite /finite_norm unlock /Lnorm mu_pos gt_eqF// => supf_lty. + rewrite poweR_lty// integral_fune_lt_pinfty => //. + apply: measurable_bounded_integrable => //. + rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)%R//. + apply: measurableT_comp => //=. + exact: measurableT_comp. + rewrite boundedE. + near=> A=> x/= _. + rewrite norm_powR// normr_id normr1 mulr1. + admit. +move=> mu_fin pleq f ffin. +have:= ffin; rewrite /finite_norm. +have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). +have q0 : (0 < q)%R by rewrite ?(lt_le_trans ltr01). +have qinv0 : q^-1 != 0%R by rewrite invr_neq0// gt_eqF. +pose r := q/p. +pose r' := (1 - r^-1)^-1. +have := (@hoelder _ _ _ mu (fun x => `|f x| `^ p) (cst 1)%R r r')%R. +rewrite (_ : (_ \* cst 1)%R = (fun x : T => `|f x| `^ p))%R -?fctM ?mulr1//. +rewrite Lnorm_cst1 unlock /Lnorm invr1. +rewrite !ifF; last 4 first. +- by apply/eqP => p0'; rewrite p0' ltxx in p0. +- by apply/eqP => q0'; rewrite q0' ltxx in q0. +- by rewrite /r gt_eqF// divr_gt0// (lt_le_trans ltr01). +- exact/negP/negP. +under [X in X `^ 1 <= _] eq_integral => x _ do + rewrite powRr1// norm_powR// normrE. +under [X in X`^ r^-1 * mu _ `^_]eq_integral => x _ do + rewrite /r norm_powR normrE ?powR_ge0// -powRrM mulrCA mulfV ?mulr1// ?gt_eqF//. +rewrite [X in X <= _]poweRe1; last + by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. +move=> h1 /lty_poweRy h2. +apply: poweR_lty. +apply: le_lt_trans. + apply: h1. + - rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)%R//. + apply: measurableT_comp => //=. + exact: measurableT_comp => //=. + - exact: measurable_cst. + - rewrite/r divr_gt0//. + - rewrite /r' invr_gt0 subr_gt0 invf_lt1 ?(lt_trans ltr01)//; + by rewrite /r ltr_pdivlMr// mul1r. + - by rewrite /r' /r invf_div invrK addrCA subrr addr0. +rewrite muleC lte_mul_pinfty ?fin_numElt?poweR_ge0//. + by rewrite (lt_le_trans _ (poweR_ge0 _ _)) ?poweR_lty. +rewrite poweR_lty// (lty_poweRy qinv0)//. +have:= ffin; rewrite /finite_norm unlock/Lnorm ifF//. +by apply/eqP => q0'; rewrite q0' ltxx in q0. +Admitted. End Lspace_inclusion. -*) diff --git a/theories/measure.v b/theories/measure.v index 75fa432737..1d6c3f692a 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -5375,6 +5375,10 @@ Implicit Types f : T -> R. Definition ess_sup f := ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]). +Definition ess_inf f := -ess_sup (-f). + +Lemma ess_infE f : ess_inf f f = ereal_sup (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. @@ -5383,4 +5387,49 @@ 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. +Lemma ess_sup_cst r : (0 < mu setT)%E -> (ess_sup (cst r) = r%:E)%E. +Proof. +rewrite /ess_sup => mu0. +under eq_set do rewrite preimage_cst/=. +rewrite ereal_inf_EFin. +- congr (_%:E). + rewrite [X in inf X](_ : _ = `[r, +oo[%classic); last first. + apply/seteqP; split => /=x/=. + case: ifPn => [_|]; first by move: mu0=> /[swap] ->; rewrite ltNge lexx. + by rewrite set_itvE notin_setE/= ltNge in_itv andbT/= => /negP /negPn. + rewrite in_itv/= => /andP[x0 _]. + by rewrite ifF// set_itvE; apply/negP; rewrite in_setE/= ltNge => /negP. + by rewrite inf_itv. +- exists r => x/=; case: ifPn => [_|]. + by move: mu0 => /[swap] ->; rewrite ltNge lexx. + by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. +by exists r => /=; rewrite ifF//; rewrite set_itvE; + rewrite memNset //=; apply/negP; rewrite -real_leNgt ?num_real. +Qed. + +Lemma ess_sup_ger f (r : R) : (forall x, f x <= r)%R -> (ess_sup f <= r%:E). +Proof. +move=> fr. +rewrite /ess_sup. +apply: ereal_inf_le. +apply/exists2P. +exists r%:E => /=; split => //. +apply/exists2P. +exists r; split => //. +rewrite preimage_itvoy. +suffices -> : [set x | r < f x]%R = set0 by []. +apply/seteqP; split => x //=. +rewrite lt_neqAle => /andP[rneqfx rlefx]. +move: (fr x) => fxler. +have: (f x <= r <= f x)%R by rewrite rlefx fxler. +by move/le_anti; move: rneqfx => /[swap] -> /eqP. +Qed. + +Lemma ess_sup_eq0 f : ess_sup (normr \o f) = 0 -> f = 0%R %[ae mu]. +Admitted. + +Lemma ess_supM (f : T -> R) (a : R) : (0 <= a)%R -> (\forall x \ae mu, 0 <= f x)%R -> + (ess_sup (cst a \* f)%R = a%:E * ess_sup f)%E. +Admitted. + End essential_supremum. From 8ef16be9b1b03386e7cb72e65a25efc3a224d87c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 28 Feb 2025 12:25:30 +0900 Subject: [PATCH 09/18] make it compile on top of master - temporary admits --- .nix/config.nix | 4 +--- experimental_reals/discrete.v | 2 +- reals/reals.v | 2 +- theories/hoelder.v | 15 ++++++++------- theories/lspace.v | 21 ++++++++++++--------- theories/measure.v | 13 ++++++++----- theories/normedtype.v | 34 ++++++++-------------------------- 7 files changed, 39 insertions(+), 52 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 225ad16e8c..3d2c9c457b 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -50,9 +50,7 @@ in ## will be created per bundle bundles."8.19".coqPackages = common-bundle // { coq.override.version = "8.19"; - mathcomp.override.version = "master"; - mathcomp-bigenough.override.version = "master"; - mathcomp-finmap.override.version = "master"; + mathcomp.override.version = "2.2.0"; }; bundles."8.20".coqPackages = common-bundle // { diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 63ca0e73b8..412877a07b 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From Corelib Require Setoid. +From Coq Require Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra. From mathcomp.classical Require Import boolp. diff --git a/reals/reals.v b/reals/reals.v index 6d747774d5..2e0ae6052b 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -38,7 +38,7 @@ (* *) (******************************************************************************) -From Corelib Require Import Setoid. +From Coq Require Import Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp Require Import boolp classical_sets set_interval. diff --git a/theories/hoelder.v b/theories/hoelder.v index 53687475cc..1f05eabb45 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -83,7 +83,8 @@ Proof. rewrite unlock; move: p => [r/=|/=|//]. by case: ifPn => // r0; exact: poweR_ge0. by case: ifPn => // /ess_sup_ge0; apply => t/=. -Qed. +case: ifPn => // muT0. +Admitted. Lemma eq_Lnorm p f g : f =1 g -> 'N_p[f] = 'N_p[g]. Proof. by move=> fg; congr Lnorm; exact/funext. Qed. @@ -95,7 +96,7 @@ rewrite unlock /Lnorm => mf. case: p => [r r0||]. - case: ifPn => _. rewrite preimage_setI preimage_setT setTI -preimage_setC. - move=> /poweR_eq0_eq0 /negligibleP. +(* move=> /poweR_eq0_eq0 /negligibleP. move/(_ (measurableC _)); rewrite -[X in d.-measurable X]setTI. move/(_ (mf _ _ _)). by case=> // A [mA muA0 fA]; exists A; split => // x/= ?; exact: fA. @@ -118,7 +119,7 @@ case: p => [r r0||]. suffices: (mu setT <= 0 <= mu setT)%E by move/le_anti. by rewrite mu0 mu1. by []. -Qed. +Qed.*) Admitted. Lemma powR_Lnorm f r : r != 0%R -> 'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E. @@ -132,7 +133,7 @@ Lemma oppr_Lnorm f p : Proof. rewrite unlock /Lnorm. case: p => /= [r||//]. - case: eqP => _. congr ((mu _) `^ _). + case: eqP => _. (*congr ((mu _) `^ _). rewrite !preimage_setI. congr (_ `&` _). rewrite -!preimage_setC. @@ -145,16 +146,16 @@ case: p => /= [r||//]. by under eq_integral => x _ do rewrite normrN. rewrite compA (_ : normr \o -%R = normr)//. apply: funext => x/=; exact: normrN. -Qed. +Qed.*) Admitted. Lemma Lnorm_cst1 r : ('N_r%:E[cst 1%R] = (mu setT)`^(r^-1)). Proof. rewrite unlock /Lnorm. case: ifPn => [_|]. - by rewrite preimage_cst ifT// inE/=; split => //; apply/eqP; rewrite oner_neq0. +(* by rewrite preimage_cst ifT// inE/=; split => //; apply/eqP; rewrite oner_neq0. under eq_integral => x _ do rewrite normr1 powR1 (_ : 1 = cst 1 x)%R// -indicT. by rewrite integral_indic// setTI. -Qed. +Qed.*) Admitted. End Lnorm_properties. diff --git a/theories/lspace.v b/theories/lspace.v index 60a3b887c1..8d35992abd 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -130,10 +130,13 @@ rewrite (@lty_poweRy _ _ (2^-1))//. rewrite (le_lt_trans _ (lfuny _ f))//. rewrite unlock /Lnorm ifF ?gt_eqF//. rewrite gt0_ler_poweR//. -- by rewrite in_itv/= integral_ge0// leey. +- rewrite in_itv/= leey integral_ge0// => x _. + by rewrite lee_fin. - rewrite in_itv/= leey integral_ge0// => x _. by rewrite lee_fin powR_ge0. rewrite ge0_le_integral//. +- move=> x _. + by rewrite abse_ge0. - apply: measurableT_comp => //. exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f). - by move=> x _; rewrite lee_fin powR_ge0. @@ -246,7 +249,7 @@ HB.instance Definition _ := [Choice of LfunType mu p1 by <:]. Import numFieldNormedType.Exports. Lemma lfuny0 : finite_norm mu p (cst 0). -Proof. by rewrite /finite_norm Lnorm0. Qed. +Proof. by rewrite /finite_norm Lnorm0// ltry. Qed. HB.instance Definition _ := @isLfun.Build d T R mu p p1 (cst 0) lfuny0. @@ -308,7 +311,8 @@ apply: (le_lt_trans (minkowskie _ _ _ _)) => //=. suff: a *: (g : T -> R) \in mfun by exact: set_mem. by rewrite rpredZ//; exact: mfunP. rewrite lte_add_pinfty//; last exact: lfuny. -by rewrite LnormZ lte_mul_pinfty//; exact: lfuny. +rewrite LnormZ lte_mul_pinfty// ?lee_fin//. +exact: lfuny. Qed. HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ lfun @@ -353,13 +357,12 @@ apply/EFin_inj; rewrite finite_norm_fine -scaler_nat LnormZ normr_nat. by rewrite -[in RHS]mulr_natl EFinM finite_norm_fine. Qed. - -HB.about Num.Zmodule_isSemiNormed.Build. - (* TODO : fix the definition *) +(* waiting for MathComp 2.4.0 HB.instance Definition _ := @Num.Zmodule_isSemiNormed.Build R (LfunType mu p1) nm ler_Lnorm_add Lnorm_natmul LnormN. +*) (* todo: add equivalent of mx_normZ and HB instance *) @@ -399,10 +402,10 @@ Lemma Lspace_inclusion (p q : \bar R) : Proof. have := measure_ge0 mu [set: T]; rewrite le_eqVlt => /orP[/eqP mu0 p1 q1 _ _ f _|mu_pos]. rewrite /finite_norm unlock /Lnorm. - move: p p1; case=> //; last by rewrite -mu0 ltxx. + move: p p1; case=> //; last admit. (*by rewrite -mu0 ltxx.*) move=> r r1; rewrite gt_eqF ?(lt_le_trans ltr01)//. rewrite measure_is_zero// integral_measure_zero. - by rewrite poweR0r// gt_eqF// invr_gt0 (lt_le_trans ltr01). + by rewrite poweR0r ?ltry// gt_eqF// invr_gt0 (lt_le_trans ltr01). move: p q. case=> //[p|]; case=> //[q|] p1 q1; last first. have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). @@ -451,7 +454,7 @@ apply: le_lt_trans. by rewrite /r ltr_pdivlMr// mul1r. - by rewrite /r' /r invf_div invrK addrCA subrr addr0. rewrite muleC lte_mul_pinfty ?fin_numElt?poweR_ge0//. - by rewrite (lt_le_trans _ (poweR_ge0 _ _)) ?poweR_lty. + by rewrite (lt_le_trans _ (poweR_ge0 _ _)) ?ltNyr// ?poweR_lty. rewrite poweR_lty// (lty_poweRy qinv0)//. have:= ffin; rewrite /finite_norm unlock/Lnorm ifF//. by apply/eqP => q0'; rewrite q0' ltxx in q0. diff --git a/theories/measure.v b/theories/measure.v index 1d6c3f692a..6387b183b0 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4161,12 +4161,10 @@ split. - by move=> f g h eqfg eqgh; near=> x => Dx; rewrite (near eqfg) ?(near eqgh). Unshelve. all: by end_near. Qed. - - Section ae_eq. Local Open Scope ring_scope. Context d (T : sigmaRingType d) (R : realType). -Implicit Types (U V : Type) (W : nzRingType). +Implicit Types (U V : Type) (W : ringType). Variables (mu : {measure set T -> \bar R}) (D : set T). Local Notation ae_eq := (ae_eq mu D). @@ -5375,9 +5373,14 @@ Implicit Types f : T -> R. Definition ess_sup f := ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]). -Definition ess_inf f := -ess_sup (-f). +Definition ess_inf f := -ess_sup (-f)%R. -Lemma ess_infE f : ess_inf f f = ereal_sup (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]). +Lemma ess_infE f : + ess_inf f = ereal_sup (EFin @` [set r | mu (f @^-1` `]-oo, r[) = 0]). +Proof. +rewrite /ess_inf /ess_sup /ereal_inf oppeK; congr ereal_sup. +rewrite !image_comp. +Admitted. Lemma ess_sup_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R -> 0 <= ess_sup f. diff --git a/theories/normedtype.v b/theories/normedtype.v index 96dac5498d..171b7196d8 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -263,27 +263,17 @@ by rewrite opprK. Qed. HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T - of Num.SemiNormedZmodule R T & PseudoPointedMetric R T := { + of Num.NormedZmodule R T & PseudoPointedMetric R T := { pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |) }. -(* HB.factory Record NormedZmod_PseudoMetric_eq (R : numDomainType) T *) -(* of Num.SemiNormedZmodule R T & PseudoPointedMetric R T := { *) -(* pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |) *) -(* }. *) - -#[short(type="pseudoMetricSemiNormedZmodType")] -HB.structure Definition PseudoMetricSemiNormedZmod (R : numDomainType) := - {T of Num.SemiNormedZmodule R T & PseudoMetric R T - & NormedZmod_PseudoMetric_eq R T & isPointed T}. - #[short(type="pseudoMetricNormedZmodType")] HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) := {T of Num.NormedZmodule R T & PseudoMetric R T & NormedZmod_PseudoMetric_eq R T & isPointed T}. Section pseudoMetricnormedzmodule_lemmas. -Context {K : numDomainType} {V : pseudoMetricSemiNormedZmodType K}. +Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}. Local Notation ball_norm := (ball_ (@normr K V)). @@ -923,27 +913,21 @@ Qed. (** Modules with a norm depending on a numDomain*) HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V - of PseudoMetricSemiNormedZmod K V & Tvs K V := { + of PseudoMetricNormedZmod K V & Tvs K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. -#[short(type="semiNormedModType")] -HB.structure Definition SemiNormedModule (K : numDomainType) := - {T of PseudoMetricSemiNormedZmod K T & Tvs K T - & PseudoMetricNormedZmod_Tvs_isNormedModule K T}. - - #[short(type="normedModType")] HB.structure Definition NormedModule (K : numDomainType) := {T of PseudoMetricNormedZmod K T & Tvs K T & PseudoMetricNormedZmod_Tvs_isNormedModule K T}. -HB.factory Record PseudoMetricSemiNormedZmod_Lmodule_isSemiNormedModule (K : numFieldType) V - of PseudoMetricSemiNormedZmod K V & GRing.Lmodule K V := { +HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V + of PseudoMetricNormedZmod K V & GRing.Lmodule K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. -HB.builders Context K V of PseudoMetricSemiNormedZmod_Lmodule_isSemiNormedModule K V. +HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V. (* NB: These lemmas are done later with more machinery. They should be simplified once normedtype is split, and the present section can @@ -981,9 +965,7 @@ rewrite [leRHS](_ : _ = M^-1 * (M * M)); last first. by rewrite mulrA mulVf ?mul1r// gt_eqF. rewrite [leLHS](_ : _ = M^-1 * (M * (`|x| + `|x|) + `|e| / 2)); last first. by rewrite mulrDr mulrA mulVf ?mul1r ?gt_eqF// mulrC addrA. -rewrite ler_wpM2l ?invr_ge0// ?ltW// -ltrBrDl -mulrBr ltr_pM// ltrBrDl. -near: M; apply: nbhs_pinfty_gt. -rewrite !realD// normr_real//. +by rewrite ler_wpM2l ?invr_ge0// ?ltW// -ltrBrDl -mulrBr ltr_pM// ltrBrDl. Unshelve. all: by end_near. Qed. Lemma locally_convex : @@ -2552,7 +2534,7 @@ by rewrite !num_max bE dE maxr_pMr. Qed. HB.instance Definition _ := - PseudoMetricSemiNormedZmod_Lmodule_isSemiNormedModule.Build K 'M[K]_(m.+1, n.+1) + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m.+1, n.+1) mx_normZ. End matrix_NormedModule. From e6a61a39cce81f27d169f36a566628644c75b865 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Fri, 28 Feb 2025 04:54:28 +0100 Subject: [PATCH 10/18] wip --- theories/measure.v | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/theories/measure.v b/theories/measure.v index 6387b183b0..51f07c286c 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -5373,14 +5373,8 @@ Implicit Types f : T -> R. Definition ess_sup f := ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]). -Definition ess_inf f := -ess_sup (-f)%R. - -Lemma ess_infE f : - ess_inf f = ereal_sup (EFin @` [set r | mu (f @^-1` `]-oo, r[) = 0]). -Proof. -rewrite /ess_inf /ess_sup /ereal_inf oppeK; congr ereal_sup. -rewrite !image_comp. -Admitted. +Definition ess_inf f := + ereal_sup (EFin @` [set r | mu (f @^-1` `]-oo, r[) = 0]). Lemma ess_sup_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R -> 0 <= ess_sup f. From a9ae291f652349434fa062fdcacdb8a84eb96a3a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 2 Mar 2025 00:17:16 +0900 Subject: [PATCH 11/18] proved one property of ess_sup --- theories/hoelder.v | 110 +++++++---------- theories/lspace.v | 152 ++++++++++++------------ theories/measurable_realfun.v | 94 ++++++++++++++- theories/measure.v | 76 +++++------- theories/topology_theory/nat_topology.v | 13 +- 5 files changed, 248 insertions(+), 197 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 1f05eabb45..2b23d61266 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -2,10 +2,10 @@ 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 reals ereal. -From mathcomp Require Import topology normedtype sequences real_interval. -From mathcomp Require Import esum measure lebesgue_measure lebesgue_integral. -From mathcomp Require Import numfun exp convex interval_inference. +From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. +From mathcomp Require Import topology normedtype sequences real_interval esum. +From mathcomp Require Import measure measurable_realfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral numfun exp convex. (**md**************************************************************************) (* # Hoelder's Inequality *) @@ -36,18 +36,18 @@ Reserved Notation "'N_ p [ F ]" Declare Scope Lnorm_scope. +Local Open Scope ereal_scope. HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType} (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) := match p with - | p%:E => (if p == 0%R then - (mu (f @^-1` (setT `\ 0%R))) - else - (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1)%E - | +oo%E => (if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0)%E - | -oo%E => (if mu [set: T] > 0 then ess_inf mu (normr \o f) else 0)%E + | p%:E => (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 + (* (mu (f @^-1` (setT `\ 0%R))) when p = 0? *) + | +oo%E => if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0 + | -oo%E => if mu [set: T] > 0 then ess_inf mu (normr \o f) else 0 end. Canonical locked_Lnorm := Unlockable Lnorm.unlock. Arguments Lnorm {d T R} mu p f. +Local Close Scope ereal_scope. Section Lnorm_properties. Context d {T : measurableType d} {R : realType}. @@ -62,8 +62,7 @@ Proof. rewrite unlock /Lnorm. case: p => [r||//]. - rewrite lee_fin => r1. - have r0: r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1). - rewrite gt_eqF ?(lt_le_trans _ r1)//. + have r0 : r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1). under eq_integral => x _ do rewrite /= normr0 powR0//. by rewrite integral0 poweR0r// invr_neq0. case: ifPn => //mu0 _. @@ -73,18 +72,17 @@ Qed. Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E. Proof. -rewrite unlock oner_eq0 invr1// poweRe1//. +rewrite unlock 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. -rewrite unlock; move: p => [r/=|/=|//]. - by case: ifPn => // r0; exact: poweR_ge0. -by case: ifPn => // /ess_sup_ge0; apply => t/=. -case: ifPn => // muT0. -Admitted. +rewrite unlock; move: p => [r/=|/=|//]; first exact: poweR_ge0. +- by case: ifPn => // /ess_sup_ger; apply => t/=. +- by case: ifPn => // muT0; apply: ess_inf_ge0 => //=. +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. @@ -93,69 +91,47 @@ Lemma Lnorm_eq0_eq0 (f : T -> R) p : measurable_fun setT f -> (0 < p)%E -> 'N_p[f] = 0 -> f = 0%R %[ae mu]. Proof. rewrite unlock /Lnorm => mf. -case: p => [r r0||]. -- case: ifPn => _. - rewrite preimage_setI preimage_setT setTI -preimage_setC. -(* move=> /poweR_eq0_eq0 /negligibleP. - move/(_ (measurableC _)); rewrite -[X in d.-measurable X]setTI. - move/(_ (mf _ _ _)). - by case=> // A [mA muA0 fA]; exists A; split => // x/= ?; exact: fA. - move=> /poweR_eq0_eq0. - move=> /(_ (integral_ge0 _ _)) h. - have: (\int[mu]_x (`|f x| `^ r)%:E)%E = 0 by apply: h => x _; rewrite lee_fin powR_ge0. +case: p => [r||//]. +- rewrite lte_fin => r0 /poweR_eq0_eq0 => /(_ (integral_ge0 _ _)) h. + have : \int[mu]_x (`|f x| `^ r)%:E = 0. + by apply: h => x _; rewrite lee_fin powR_ge0. under eq_integral => x _ do rewrite -[_%:E]gee0_abs ?lee_fin ?powR_ge0//. - have mp: measurable_fun [set: T] (fun x : T => (`|f x| `^ r)%:E). + have mp : measurable_fun [set: T] (fun x : T => (`|f x| `^ r)%:E). apply: measurableT_comp => //. apply (measurableT_comp (measurable_powR _)) => //. exact: measurableT_comp. move/(ae_eq_integral_abs _ measurableT mp). apply: filterS => x/= /[apply]. by case=> /powR_eq0_eq0 /eqP; rewrite normr_eq0 => /eqP. -- case: ifPn => [mu0 _|]. - exact: ess_sup_eq0. +- case: ifPn => [mu0 _|]; first exact: ess_sup_eq0_ae. rewrite ltNge => /negbNE mu0 _ _. suffices mueq0: mu setT = 0 by exact: ae_eq0. - move: mu0 (measure_ge0 mu setT) => mu0 mu1. - suffices: (mu setT <= 0 <= mu setT)%E by move/le_anti. - by rewrite mu0 mu1. -by []. -Qed.*) Admitted. + by apply/eqP; rewrite eq_le mu0/=. +Qed. Lemma powR_Lnorm f r : r != 0%R -> 'N_r%:E[f] `^ r = \int[mu]_x (`| f x | `^ r)%:E. Proof. -move=> r0; rewrite unlock (negbTE r0) -poweRrM mulVf// poweRe1//. +move=> r0; rewrite unlock -poweRrM mulVf// poweRe1//. by apply: integral_ge0 => x _; rewrite lee_fin// powR_ge0. Qed. -Lemma oppr_Lnorm f p : - 'N_p[\- f]%R = 'N_p[f]. +Lemma oppr_Lnorm f p : 'N_p[\- f]%R = 'N_p[f]. Proof. -rewrite unlock /Lnorm. -case: p => /= [r||//]. - case: eqP => _. (*congr ((mu _) `^ _). - rewrite !preimage_setI. - congr (_ `&` _). - rewrite -!preimage_setC. - congr (~` _). - rewrite /preimage. - apply: funext => x/=. - rewrite -{1}oppr0. - apply: propext. split; last by move=> ->. - by move/oppr_inj. - by under eq_integral => x _ do rewrite normrN. -rewrite compA (_ : normr \o -%R = normr)//. -apply: funext => x/=; exact: normrN. -Qed.*) Admitted. +rewrite unlock /Lnorm; case: p => /= [r||//]. +- by under eq_integral => x _ do rewrite normrN. +- rewrite compA (_ : normr \o -%R = normr)//. + by apply: funext => x/=; exact: normrN. +- rewrite compA (_ : normr \o -%R = normr)//. + by apply: funext => x/=; exact: normrN. +Qed. Lemma Lnorm_cst1 r : ('N_r%:E[cst 1%R] = (mu setT)`^(r^-1)). Proof. rewrite unlock /Lnorm. -case: ifPn => [_|]. -(* by rewrite preimage_cst ifT// inE/=; split => //; apply/eqP; rewrite oner_neq0. under eq_integral => x _ do rewrite normr1 powR1 (_ : 1 = cst 1 x)%R// -indicT. by rewrite integral_indic// setTI. -Qed.*) Admitted. +Qed. End Lnorm_properties. @@ -174,7 +150,7 @@ Local Notation "'N_ p [ f ]" := (Lnorm counting p f). Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R -> 'N_p%:E [f] = (\sum_(k p0; rewrite unlock gt_eqF// ge0_integral_count// => k. +move=> p0; rewrite unlock ge0_integral_count// => k. by rewrite lee_fin powR_ge0. Qed. @@ -201,7 +177,7 @@ 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) <-. -rewrite unlock (gt_eqF p0); apply/eqP; congr (_ `^ _). +rewrite unlock; apply/eqP; congr (_ `^ _). by apply/eq_integral => t _; rewrite [RHS]gee0_abs// lee_fin powR_ge0. Qed. @@ -237,10 +213,10 @@ transitivity (\int[mu]_x (`|f x| `^ p / fine ('N_p%:E[f] `^ p))%:E). 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 unlock (gt_eqF p0) in fpos. + rewrite unlock in fpos. apply: gt0_poweR fpos; rewrite ?invr_gt0//. by apply integral_ge0 => x _; rewrite lee_fin; exact: powR_ge0. -rewrite unlock (gt_eqF p0) -poweRrM mulVf ?(gt_eqF p0)// (poweRe1 (ltW fp0))//. +rewrite unlock -poweRrM mulVf ?(gt_eqF p0)// (poweRe1 (ltW fp0))//. under eq_integral do rewrite EFinM muleC. have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo. move/integrableP: ifp => -[_]. @@ -448,7 +424,7 @@ have h x : (`| f x + g x | `^ p <= rewrite !normrM (@ger0_norm _ 2)// !mulrA mulVf// !mul1r => /le_trans; apply. rewrite !powRM// !mulrA -powR_inv1// -powRD ?pnatr_eq0 ?implybT//. by rewrite (addrC _ p) -mulrDr. -rewrite unlock (gt_eqF (lt_le_trans _ p1))// poweR_lty//. +rewrite unlock poweR_lty//. pose x := \int[mu]_x (2 `^ (p - 1) * (`|f x| `^ p + `|g x| `^ p))%:E. apply: (@le_lt_trans _ _ x). rewrite ge0_le_integral//=. @@ -536,7 +512,7 @@ rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) * rewrite Lnorm1; apply: eq_integral => x _. by rewrite normrM (ger0_norm (powR_ge0 _ _)). rewrite [X in _ * X](_ : _ = 'N_(p / (p - 1))%:E[h]); last first. - rewrite unlock mulf_eq0 gt_eqF//= invr_eq0 subr_eq0 (gt_eqF p1). + rewrite unlock. rewrite onemV ?gt_eqF// invf_div; apply: congr2; last by []. apply: eq_integral => x _; congr EFin. rewrite norm_powR// normr_id -powRrM mulrCA divff ?mulr1//. @@ -550,8 +526,8 @@ rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) * rewrite Lnorm1; apply: eq_integral => x _ . by rewrite normrM norm_powR// normr_id. rewrite [X in _ * X](_ : _ = 'N_((1 - p^-1)^-1)%:E[h])//; last first. - rewrite unlock invrK invr_eq0 subr_eq0 eq_sym invr_eq1 (gt_eqF p1). - apply: congr2; last by []. + rewrite unlock. + apply: congr2; last by rewrite invrK. apply: eq_integral => x _; congr EFin. rewrite -/(onem p^-1) onemV ?gt_eqF// norm_powR// normr_id -powRrM. by rewrite invf_div mulrCA divff ?subr_eq0 ?gt_eqF// ?mulr1. @@ -564,7 +540,7 @@ under [X in X * _]eq_integral=> x _ do rewrite mulr_powRB1 ?subr_gt0//. rewrite poweRD; last by rewrite poweRD_defE gt_eqF ?implyFb// subr_gt0 invf_lt1. rewrite poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. congr (_ * _); rewrite poweRN. -- by rewrite unlock gt_eqF// fine_poweR. +- by rewrite unlock fine_poweR. - by rewrite -powR_Lnorm ?gt_eqF// fin_num_poweR// ge0_fin_numE ?Lnorm_ge0. Qed. diff --git a/theories/lspace.v b/theories/lspace.v index 8d35992abd..2077f21cb1 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -1,11 +1,11 @@ (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect. From mathcomp Require Import ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import boolp reals ereal. -From HB Require Import structures. -From mathcomp Require Import classical_sets signed functions topology normedtype cardinality. -From mathcomp Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral. -From mathcomp Require Import exp hoelder. +From mathcomp Require Import boolp classical_sets interval_inference reals. +From mathcomp Require Import functions cardinality topology normedtype ereal. +From mathcomp Require Import sequences esum exp measure numfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral hoelder. (******************************************************************************) (* *) @@ -106,12 +106,13 @@ Variable mu : {measure set T -> \bar R}. Definition Lspace p (p1 : (1 <= p)%E) := [set: LType mu p1]. Arguments Lspace : clear implicits. -Lemma LType1_integrable (f : LType mu (@lexx _ _ 1%E)) : mu.-integrable setT (EFin \o f). +Lemma LType1_integrable (f : LType mu (@lexx _ _ 1%E)) : + mu.-integrable setT (EFin \o f). Proof. -apply/integrableP; split; first exact/EFin_measurable_fun. +apply/integrableP; split; first exact/measurable_EFinP. have := lfuny _ f. -rewrite /finite_norm unlock /Lnorm ifF ?oner_eq0// invr1 poweRe1; last first. - by apply integral_ge0 => x _; rewrite lee_fin powRr1//. +rewrite /finite_norm unlock /Lnorm invr1 poweRe1; last first. + by apply integral_ge0 => x _; rewrite lee_fin powRr1. by under eq_integral => i _ do rewrite powRr1//. Qed. @@ -125,23 +126,23 @@ Lemma LType2_integrable_sqr (f : LType mu le12) : mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)). Proof. apply/integrableP; split. - exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f). -rewrite (@lty_poweRy _ _ (2^-1))//. + apply/measurable_EFinP. + exact/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f). +rewrite (@lty_poweRy _ _ 2^-1)//. rewrite (le_lt_trans _ (lfuny _ f))//. -rewrite unlock /Lnorm ifF ?gt_eqF//. +rewrite unlock. rewrite gt0_ler_poweR//. -- rewrite in_itv/= leey integral_ge0// => x _. - by rewrite lee_fin. +- by rewrite in_itv/= leey integral_ge0// => x _. - rewrite in_itv/= leey integral_ge0// => x _. by rewrite lee_fin powR_ge0. -rewrite ge0_le_integral//. -- move=> x _. - by rewrite abse_ge0. -- apply: measurableT_comp => //. - exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f). -- by move=> x _; rewrite lee_fin powR_ge0. -- exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R)/measurableT_comp. -- by move=> t _/=; rewrite lee_fin normrX powR_mulrn. +- rewrite ge0_le_integral//. + + apply: measurableT_comp => //; apply/measurable_EFinP. + exact/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f). + + by move=> x _; rewrite lee_fin powR_ge0. + + apply/measurable_EFinP. + apply/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R) => //. + exact/measurableT_comp. + + by move=> t _/=; rewrite lee_fin normrX powR_mulrn. Qed. End Lspace. @@ -196,17 +197,15 @@ Lemma sub_lfun_mfun : {subset lfun <= mfun}. Proof. by move=> x /andP[]. Qed. Lemma sub_lfun_finlfun : {subset lfun <= finlfun}. Proof. by move=> x /andP[]. Qed. End lfun_pred. - -Lemma minkowskie : -forall [d : measure_display] [T : measurableType d] [R : realType] - (mu : measure T R) [f g : T -> R] [p : \bar R], -measurable_fun [set: T] f -> -measurable_fun [set: T] g -> -(1 <= p)%E -> ('N[mu]_p[(f \+ g)%R] <= 'N[mu]_p[f] + 'N[mu]_p[g])%E. +Lemma minkowskie [d : measure_display] [T : measurableType d] [R : realType] + (mu : measure T R) [f g : T -> R] [p : \bar R] : + measurable_fun [set: T] f -> + measurable_fun [set: T] g -> + (1 <= p)%E -> ('N[mu]_p[(f \+ g)%R] <= 'N[mu]_p[f] + 'N[mu]_p[g])%E. +Proof. (* TODO: Jairo is working on this *) Admitted. - Section lfun. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E). @@ -272,8 +271,7 @@ Proof. rewrite unlock /Lnorm. move: p p1 f. case=> //[r r1 f|]. - rewrite gt_eqF ?(lt_le_trans ltr01)//. - under eq_integral => x _/= do rewrite -mulr_algl scaler1 normrM powRM ?EFinM//. +- under eq_integral => x _/= do rewrite -mulr_algl scaler1 normrM powRM ?EFinM//. rewrite integralZl//; last first. apply /integrableP; split. apply: measurableT_comp => //. @@ -282,20 +280,19 @@ case=> //[r r1 f|]. apply: (@lty_poweRy _ _ r^-1). by rewrite gt_eqF// invr_gt0 ?(lt_le_trans ltr01). have -> : ((\int[mu]_x `|(`|f x| `^ r)%:E|) `^ r^-1 = 'N[mu]_r%:E[f])%E. - rewrite unlock /Lnorm gt_eqF ?(lt_le_trans ltr01)//. + rewrite unlock /Lnorm. by under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. exact: (lfuny r1 f). rewrite poweRM ?integral_ge0=> //[||x _]; rewrite ?lee_fin ?powR_ge0//. by rewrite poweR_EFin -powRrM mulfV ?gt_eqF ?(lt_le_trans ltr01)// powRr1. -move=> p0 f. -case: ifP => mu0. - rewrite (_ : normr \o a \*: f = (`|a|) \*: (normr \o f)); last first. - by apply: funext => x/=; rewrite normrZ. - rewrite ess_supM//. - by near=> x=> /=. -by rewrite mule0. -Unshelve. end_near. -Qed. +- move=> p0 f. + case: ifP => mu0. + rewrite (_ : normr \o a \*: f = (`|a|) \*: (normr \o f)); last first. + by apply: funext => x/=; rewrite normrZ. + rewrite ess_supMr//. + by near=> x=> /=. + by rewrite mule0. +Unshelve. end_near. Qed. Lemma lfun_submod_closed : submod_closed (lfun). Proof. @@ -321,7 +318,6 @@ HB.instance Definition _ := [SubChoice_isSubLmodule of LfunType mu p1 by <:]. End lfun. - Section Lspace_norm. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. @@ -333,8 +329,9 @@ Notation ty := (LfunType mu p1). Definition nm f := fine ('N[mu]_p[f]). Lemma finite_norm_fine (f : ty) : (nm f)%:E = 'N[mu]_p[f]. -Proof. -by rewrite /nm fineK// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=; exact: lfuny. +Proof. +rewrite /nm fineK// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=. +exact: lfuny. Qed. Lemma ler_Lnorm_add (f g : ty) : @@ -348,7 +345,8 @@ Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed. Lemma LnormN (f : ty) : nm (\-f) = nm f. Proof. by rewrite /nm oppr_Lnorm. Qed. -Lemma enatmul_ninfty (n : nat) : (-oo *+ n.+1 = -oo :> \bar R)%E \/ (-oo *+ n.+1 = +oo :> \bar R)%E. +Lemma enatmul_ninfty (n : nat) : + (-oo *+ n.+1 = -oo :> \bar R)%E \/ (-oo *+ n.+1 = +oo :> \bar R)%E. Proof. by elim: n => //=[|n []->]; rewrite ?addNye; left. Qed. Lemma Lnorm_natmul (f : ty) k : nm (f *+ k) = nm f *+ k. @@ -372,7 +370,6 @@ rewrite /nm=> /eqP; rewrite -eqe=> /eqP; rewrite finite_norm_fine=> /Lnorm_eq0_e by apply; rewrite ?(lt_le_trans _ p1). Qed. - End Lspace_norm. Section Lspace_inclusion. @@ -380,37 +377,42 @@ Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. (* the following lemma is not needed, but looks useful, should we include it anyways? *) -Lemma mul_lte_pinfty (x y : \bar R) : (x \is a fin_num -> 0 < x -> x * y < +oo -> y < +oo)%E. -Proof. rewrite fin_numE => /andP[/eqP xNoo /eqP xoo]. +Lemma mul_lte_pinfty (x y : \bar R) : + (x \is a fin_num -> 0 < x -> x * y < +oo -> y < +oo)%E. +Proof. +rewrite fin_numE => /andP[/eqP xNoo /eqP xoo]. move: x xNoo xoo. -case => // r _ _ rgt0. +case => // r _ _; rewrite lte_fin => r0. rewrite /mule. -case: y => //[r0 ?|]. - by rewrite ltry. -case: ifP => //. by move: rgt0 => /[swap] /eqP -> /eqP; rewrite ltxx. -case: ifP => //. by rewrite rgt0. +case: y => //[s|]. + by rewrite !ltry. +by rewrite eqe gt_eqF// lte_fin r0. Qed. Local Open Scope ereal_scope. Lemma measure_is_zero : mu [set: T] = 0%E -> mu = mzero. +Proof. +move=> mu0. Admitted. Lemma Lspace_inclusion (p q : \bar R) : forall (p1 : 1 <= p) (q1 : 1 <= q), - mu [set: T] < +oo -> p < q -> forall (f : {mfun T >-> R}), finite_norm mu q f -> finite_norm mu p f. + mu [set: T] < +oo -> p < q -> + forall f : {mfun T >-> R}, finite_norm mu q f -> finite_norm mu p f. Proof. -have := measure_ge0 mu [set: T]; rewrite le_eqVlt => /orP[/eqP mu0 p1 q1 _ _ f _|mu_pos]. +have := measure_ge0 mu [set: T]. +rewrite le_eqVlt => /predU1P[mu0 p1 q1 _ _ f _|mu_pos]. rewrite /finite_norm unlock /Lnorm. - move: p p1; case=> //; last admit. (*by rewrite -mu0 ltxx.*) - move=> r r1; rewrite gt_eqF ?(lt_le_trans ltr01)//. + move: p p1; case=> //; last by rewrite -mu0 ltxx ltry. + move=> r r1. rewrite measure_is_zero// integral_measure_zero. by rewrite poweR0r ?ltry// gt_eqF// invr_gt0 (lt_le_trans ltr01). move: p q. case=> //[p|]; case=> //[q|] p1 q1; last first. have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). move=> muoo _ f. - rewrite /finite_norm unlock /Lnorm mu_pos gt_eqF// => supf_lty. + rewrite /finite_norm unlock /Lnorm mu_pos => supf_lty. rewrite poweR_lty// integral_fune_lt_pinfty => //. apply: measurable_bounded_integrable => //. rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)%R//. @@ -430,11 +432,19 @@ pose r' := (1 - r^-1)^-1. have := (@hoelder _ _ _ mu (fun x => `|f x| `^ p) (cst 1)%R r r')%R. rewrite (_ : (_ \* cst 1)%R = (fun x : T => `|f x| `^ p))%R -?fctM ?mulr1//. rewrite Lnorm_cst1 unlock /Lnorm invr1. -rewrite !ifF; last 4 first. -- by apply/eqP => p0'; rewrite p0' ltxx in p0. -- by apply/eqP => q0'; rewrite q0' ltxx in q0. -- by rewrite /r gt_eqF// divr_gt0// (lt_le_trans ltr01). -- exact/negP/negP. +have mfp : measurable_fun [set: T] (fun x : T => (`|f x| `^ p)%R). + rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)%R//. + apply: measurableT_comp => //=. + exact: measurableT_comp => //=. +have m1 : measurable_fun [set: T] (@cst _ R 1%R). + exact: measurable_cst. +have r0 : (0 < r)%R by rewrite/r divr_gt0. +have r'0 : (0 < r')%R. + by rewrite /r' invr_gt0 subr_gt0 invf_lt1 ?(lt_trans ltr01)//; + rewrite /r ltr_pdivlMr// mul1r. +have rr'1 : r^-1 + r'^-1 = 1%R. + by rewrite /r' /r invf_div invrK addrCA subrr addr0. +move=> /(_ mfp m1 r0 r'0 rr'1). under [X in X `^ 1 <= _] eq_integral => x _ do rewrite powRr1// norm_powR// normrE. under [X in X`^ r^-1 * mu _ `^_]eq_integral => x _ do @@ -443,21 +453,11 @@ rewrite [X in X <= _]poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. move=> h1 /lty_poweRy h2. apply: poweR_lty. -apply: le_lt_trans. - apply: h1. - - rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)%R//. - apply: measurableT_comp => //=. - exact: measurableT_comp => //=. - - exact: measurable_cst. - - rewrite/r divr_gt0//. - - rewrite /r' invr_gt0 subr_gt0 invf_lt1 ?(lt_trans ltr01)//; - by rewrite /r ltr_pdivlMr// mul1r. - - by rewrite /r' /r invf_div invrK addrCA subrr addr0. +apply: (le_lt_trans h1). rewrite muleC lte_mul_pinfty ?fin_numElt?poweR_ge0//. by rewrite (lt_le_trans _ (poweR_ge0 _ _)) ?ltNyr// ?poweR_lty. rewrite poweR_lty// (lty_poweRy qinv0)//. -have:= ffin; rewrite /finite_norm unlock/Lnorm ifF//. -by apply/eqP => q0'; rewrite q0' ltxx in q0. +by have:= ffin; rewrite /finite_norm unlock /Lnorm. Admitted. End Lspace_inclusion. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index a36e041a9b..fe16ec2df1 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1633,10 +1633,102 @@ Qed. End open_itv_cover. +Section essential_supremum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> R. +Local Open Scope ereal_scope. + +Lemma ess_sup_max f : measurable_fun setT f -> + ess_sup mu (normr \o f) != -oo -> + mu [set r | ess_sup mu (normr \o f) < `|f r|%:E] = 0. +Proof. +move=> mf fNy. +move hm : (ess_sup mu (normr \o f)) => m. +case: m hm => [m| |] hm. +- pose x_ n := m%:E + n.+1%:R^-1%:E. + have -> : [set r | m%:E < `|f r|%:E] = \bigcup_n [set r | x_ n < `|f r|%:E]. + apply/seteqP; split => [r /= mfr|r/=]. + near \oo => n. + suff : x_ n < `|f r|%:E by move=> ?; exists n. + rewrite /x_ -EFinD lte_fin -ltrBrDl. + rewrite invf_plt ?posrE//; last by rewrite subr_gt0 -lte_fin. + by rewrite -natr1 -ltrBlDr; near: n; exact: nbhs_infty_gtr. + by move=> [n _/=]; apply: le_lt_trans;rewrite /x_ -EFinD lee_fin lerDl. + have H n : mu [set r | x_ n < `|f r|%:E] = 0%R. + have : ess_sup mu (normr \o f) \is a fin_num by rewrite hm. + move/lb_ereal_inf_adherent => /(_ n.+1%:R^-1). + rewrite invr_gt0// ltr0n => /(_ erefl)[_ /= [r/= mufr0] <-]. + rewrite -/(ess_sup mu _) hm /x_ => rmn. + apply/eqP; rewrite eq_le measure_ge0 andbT. + rewrite -mufr0 le_measure// ?inE//. + + rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. + by apply/measurable_EFinP; exact/measurableT_comp. + + rewrite (_ : _ @^-1` _ = [set t | r%:E < `|f t|%:E]); last first. + by apply/seteqP; split => [x|x]/=; rewrite in_itv/= andbT. + rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. + by apply/measurable_EFinP; exact/measurableT_comp. + + move=> x/=; rewrite in_itv/= andbT. + rewrite -EFinD lte_fin; apply/le_lt_trans. + by move: rmn; rewrite -EFinD lte_fin => /ltW. + apply/eqP; rewrite eq_le measure_ge0 andbT. + have <- : \sum_(0 <= i [i|]. + + rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. + by apply/measurable_EFinP; exact/measurableT_comp. + + apply: bigcup_measurable => i _. + rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. + by apply/measurable_EFinP; exact/measurableT_comp. +- rewrite (_ : [set r | +oo < `|f r|%:E] = set0)// -subset0 => x/=. + by rewrite ltNge leey. +- by rewrite hm in fNy. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_eq0 f : measurable_fun setT f -> + f = 0%R %[ae mu] <-> mu [set r | (0%R < `|f r|)%R] = 0. +Proof. +move=> mf; split=> [|f0]. +- case => N [mN N0 fN]. + apply/eqP; rewrite eq_le measure_ge0 andbT -N0. + rewrite le_measure ?inE//. + rewrite [X in measurable X](_ : _ = [set t | 0 < `|f t|%:E]); last first. + by apply/seteqP; split => [x|x]/=; rewrite lte_fin. + rewrite -[X in measurable X]setTI. + apply: emeasurable_fun_o_infty => //. + by apply/measurable_EFinP; exact/measurableT_comp. + apply: subset_trans fN => t/= ft0. + apply/not_implyP; split => //. + apply/eqP. + by rewrite -normr_eq0 gt_eqF. +- exists [set r | (0 < `|f r|)%R]; split => //. + rewrite [X in measurable X](_ : _ = [set t | 0 < `|f t|%:E]); last first. + by apply/seteqP; split => [x|x]/=; rewrite lte_fin. + rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. + by apply/measurable_EFinP; exact/measurableT_comp. + move=> t/= /not_implyP[_ /eqP]; rewrite -normr_eq0 => ft0. + by rewrite lt_neqAle eq_sym ft0/=. +Qed. + +Lemma ess_sup_eq0_ae f : measurable_fun setT f -> + ess_sup mu (normr \o f) = 0 -> f = 0%R %[ae mu]. +Proof. +move=> mf f0; apply/ess_sup_eq0 => //. +rewrite [X in mu X](_ : _ = [set r | (0 < `|f r|%:E)%E]); last first. + by apply/seteqP; split => [x|x]/=; rewrite lte_fin. +by rewrite -f0 ess_sup_max// f0. +Qed. + +Lemma ess_supMr f (r : R) : (0 <= r)%R -> (\forall x \ae mu, 0 <= f x)%R -> + ess_sup mu (cst r \* f)%R = r%:E * ess_sup mu f. +Proof. +Admitted. + +End essential_supremum. + Section egorov. Context d {R : realType} {T : measurableType d}. Context (mu : {measure set T -> \bar R}). - Local Open Scope ereal_scope. (*TODO : this generalizes to any metric space with a borel measure*) diff --git a/theories/measure.v b/theories/measure.v index 51f07c286c..1478d48637 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -274,6 +274,7 @@ From HB Require Import structures. (* 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 *) (* semiRingOfSetsType and R is a realType *) +(* ess_inf f == essential infimum *) (* ``` *) (* *) (******************************************************************************) @@ -5373,60 +5374,39 @@ Implicit Types f : T -> R. Definition ess_sup f := ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]). -Definition ess_inf f := - ereal_sup (EFin @` [set r | mu (f @^-1` `]-oo, r[) = 0]). - -Lemma ess_sup_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R -> - 0 <= ess_sup f. +Lemma ess_sup_ger f x : 0 < mu [set: T] -> (forall t, x <= f t)%R -> + x%:E <= 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)). +by apply/seteqP; split => // t _ /=; rewrite in_itv/= (lt_le_trans _ (f0 t)). +Qed. + +Lemma ess_sup_ler f (r : R) : (forall x, f x <= r)%R -> ess_sup f <= r%:E. +Proof. +move=> fr; apply: ereal_inf_le; apply/exists2P. +exists r%:E => /=; split => //; apply/exists2P; exists r; split => //. +rewrite preimage_itvoy [X in mu X](_ : _ = set0)// -subset0 => x //=. +rewrite lt_neqAle => /andP[+ rlefx]. +by apply/negP/negPn; rewrite eq_le rlefx fr. Qed. Lemma ess_sup_cst r : (0 < mu setT)%E -> (ess_sup (cst r) = r%:E)%E. Proof. -rewrite /ess_sup => mu0. -under eq_set do rewrite preimage_cst/=. -rewrite ereal_inf_EFin. -- congr (_%:E). - rewrite [X in inf X](_ : _ = `[r, +oo[%classic); last first. - apply/seteqP; split => /=x/=. - case: ifPn => [_|]; first by move: mu0=> /[swap] ->; rewrite ltNge lexx. - by rewrite set_itvE notin_setE/= ltNge in_itv andbT/= => /negP /negPn. - rewrite in_itv/= => /andP[x0 _]. - by rewrite ifF// set_itvE; apply/negP; rewrite in_setE/= ltNge => /negP. - by rewrite inf_itv. -- exists r => x/=; case: ifPn => [_|]. - by move: mu0 => /[swap] ->; rewrite ltNge lexx. - by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. -by exists r => /=; rewrite ifF//; rewrite set_itvE; - rewrite memNset //=; apply/negP; rewrite -real_leNgt ?num_real. -Qed. - -Lemma ess_sup_ger f (r : R) : (forall x, f x <= r)%R -> (ess_sup f <= r%:E). -Proof. -move=> fr. -rewrite /ess_sup. -apply: ereal_inf_le. -apply/exists2P. -exists r%:E => /=; split => //. -apply/exists2P. -exists r; split => //. -rewrite preimage_itvoy. -suffices -> : [set x | r < f x]%R = set0 by []. -apply/seteqP; split => x //=. -rewrite lt_neqAle => /andP[rneqfx rlefx]. -move: (fr x) => fxler. -have: (f x <= r <= f x)%R by rewrite rlefx fxler. -by move/le_anti; move: rneqfx => /[swap] -> /eqP. -Qed. - -Lemma ess_sup_eq0 f : ess_sup (normr \o f) = 0 -> f = 0%R %[ae mu]. -Admitted. - -Lemma ess_supM (f : T -> R) (a : R) : (0 <= a)%R -> (\forall x \ae mu, 0 <= f x)%R -> - (ess_sup (cst a \* f)%R = a%:E * ess_sup f)%E. -Admitted. +move => mu0. +by apply/eqP; rewrite eq_le; apply/andP; split; + [exact: ess_sup_ler|exact: ess_sup_ger]. +Qed. + +Definition ess_inf f := + ereal_sup (EFin @` [set r | mu (f @^-1` `]-oo, r[) = 0]). + +Lemma ess_inf_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R -> + 0 <= ess_inf f. +Proof. +move=> muT f0; apply: ereal_sup_le; exists 0 => //=; exists 0%R => //=. +rewrite [X in mu X](_ : _ = set0)// -subset0 => x/=. +by rewrite in_itv/= ltNge => /negP; exact. +Qed. End essential_supremum. diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v index 79bc3a1b39..82c92c7270 100644 --- a/theories/topology_theory/nat_topology.v +++ b/theories/topology_theory/nat_topology.v @@ -38,7 +38,7 @@ Qed. HB.instance Definition _ := Order_isNbhs.Build _ nat nat_nbhs_itv. HB.instance Definition _ := DiscreteUniform_ofNbhs.Build nat. -HB.instance Definition _ {R : numDomainType} := +HB.instance Definition _ {R : numDomainType} := @DiscretePseudoMetric_ofUniform.Build R nat. Lemma nbhs_infty_gt N : \forall n \near \oo, (N < n)%N. @@ -48,13 +48,16 @@ Proof. by exists N.+1. Qed. Lemma nbhs_infty_ge N : \forall n \near \oo, (N <= n)%N. Proof. by exists N. Qed. -Lemma nbhs_infty_ger {R : realType} (r : R) : - \forall n \near \oo, (r <= n%:R)%R. +Lemma nbhs_infty_gtr {R : realType} (r : R) : \forall n \near \oo, r < n%:R. Proof. -exists `|Num.ceil r|%N => // n /=; rewrite -(ler_nat R); apply: le_trans. -by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm. +exists `|Num.ceil r|.+1%N => // n /=; rewrite -(ler_nat R); apply: lt_le_trans. +rewrite (le_lt_trans (ceil_ge _))// -natr1 natr_absz ltr_pwDr// ler_int. +exact: ler_norm. Qed. +Lemma nbhs_infty_ger {R : realType} (r : R) : \forall n \near \oo, r <= n%:R. +Proof. by apply: filterS (nbhs_infty_gtr r) => x /ltW. Qed. + Lemma cvg_addnl N : addn N @ \oo --> \oo. Proof. by move=> P [n _ Pn]; exists (n - N)%N => // m; rewrite /= leq_subLR => /Pn. From 40275ee975ba36606aa48ff0f04e00cdca6a300f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 2 Mar 2025 17:41:19 +0900 Subject: [PATCH 12/18] ess_supM --- theories/lspace.v | 35 ++++++++---------- theories/measurable_realfun.v | 68 +++++++++++++++++++++++++++++++++-- theories/measure.v | 20 ++++++----- 3 files changed, 92 insertions(+), 31 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 2077f21cb1..9261fade4d 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -148,7 +148,7 @@ Qed. End Lspace. Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope. -(* move to hoelder.v *) +(* TODO: move to hoelder.v *) Section conjugate. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (p : \bar R). @@ -169,22 +169,19 @@ Lemma conjugateE : else if p == +oo then 1 else 0. Proof. rewrite /conjugate. -move: p1. -case: p => [r|//=|//]. +case: p p1 => [r|//=|//]. rewrite lee_fin => r1. have r0 : r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1). -congr (_%:E). -apply: get_unique. +congr EFin; apply: get_unique. by rewrite invf_div mulrBl divff// mul1r addrCA subrr addr0. -move=> /= y h0. -suffices -> : y = (1 - r^-1)^-1. +move=> /= y ry1. +suff -> : y = (1 - r^-1)^-1. by rewrite -(mul1r r^-1) -{1}(divff r0) -mulrBl invf_div. -by rewrite -h0 -addrAC subrr add0r invrK. +by rewrite -ry1 -addrAC subrr add0r invrK. Qed. End conjugate. - Section lfun_pred. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (p : \bar R). @@ -269,14 +266,13 @@ Lemma LnormZ (f : LfunType mu p1) a : ('N[mu]_p[a \*: f] = `|a|%:E * 'N[mu]_p[f])%E. Proof. rewrite unlock /Lnorm. -move: p p1 f. -case=> //[r r1 f|]. +case: p p1 f => //[r r1 f|]. - under eq_integral => x _/= do rewrite -mulr_algl scaler1 normrM powRM ?EFinM//. rewrite integralZl//; last first. apply /integrableP; split. apply: measurableT_comp => //. - rewrite (_ : (fun x : T => `|f x| `^ r) = (@powR R)^~ r \o normr \o f)//. - by repeat apply: measurableT_comp => //. + rewrite [X in measurable_fun _ X](_ : _ = (@powR R)^~ r \o normr \o f)//. + by apply: measurableT_comp => //; apply: measurableT_comp. apply: (@lty_poweRy _ _ r^-1). by rewrite gt_eqF// invr_gt0 ?(lt_le_trans ltr01). have -> : ((\int[mu]_x `|(`|f x| `^ r)%:E|) `^ r^-1 = 'N[mu]_r%:E[f])%E. @@ -285,14 +281,11 @@ case=> //[r r1 f|]. exact: (lfuny r1 f). rewrite poweRM ?integral_ge0=> //[||x _]; rewrite ?lee_fin ?powR_ge0//. by rewrite poweR_EFin -powRrM mulfV ?gt_eqF ?(lt_le_trans ltr01)// powRr1. -- move=> p0 f. - case: ifP => mu0. - rewrite (_ : normr \o a \*: f = (`|a|) \*: (normr \o f)); last first. - by apply: funext => x/=; rewrite normrZ. - rewrite ess_supMr//. - by near=> x=> /=. - by rewrite mule0. -Unshelve. end_near. Qed. +- move=> p0 f; case: ifP => mu0; last by rewrite mule0. + rewrite (_ : normr \o a \*: f = `|a| \*: (normr \o f)); last first. + by apply: funext => x/=; rewrite normrZ. + by rewrite ess_supMl. +Qed. Lemma lfun_submod_closed : submod_closed (lfun). Proof. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index fe16ec2df1..1d5138b22e 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1633,6 +1633,58 @@ Qed. End open_itv_cover. +Section ereal_supZ. +Context {R : realType}. +Implicit Types (r s : R) (A : set R). +Local Open Scope ereal_scope. + +Lemma ereal_supZl A r : (0 < r)%R -> + ereal_sup [set r%:E * x%:E | x in A] = r%:E * ereal_sup (EFin @` A). +Proof. +move=> r0. +apply/eqP; rewrite eq_le; apply/andP; split. + (*TODO: should be ereal_sup_le and the current ereal_sup_le should be named something else*) + apply: ub_ereal_sup => /= _ [s As <-]. + rewrite -lee_pdivlMl// muleA -EFinM mulVf ?gt_eqF// mul1e. + by apply: ereal_sup_le; exists s%:E => //=; exists s. +rewrite -lee_pdivlMl//. +apply: ub_ereal_sup => /= _ [s As <-]. +rewrite lee_pdivlMl//. +apply: ereal_sup_le; exists (r * s)%:E => //=. +by exists s => //; rewrite EFinM. +Qed. + +Let ereal_infZl' A r : (0 < r)%R -> + ereal_sup [set - x | x in [set r%:E * x%:E | x in A]] = + r%:E * ereal_sup [set - x | x in [set x%:E | x in A]]. +Proof. +move=> r0. +apply/eqP; rewrite eq_le; apply/andP; split. + apply: ub_ereal_sup => /= _ [_ [s As <-]] <-. + rewrite -muleN -lee_pdivlMl// muleA -EFinM mulVf ?gt_eqF// mul1e. + apply: ereal_sup_le; exists (- s%:E) => //=. + exists s%:E. + by exists s. + by rewrite EFinN. +rewrite -lee_pdivlMl//. +apply: ub_ereal_sup => /= _ [_ [s As <-]] <-. +rewrite lee_pdivlMl//. +apply: ereal_sup_le; exists (- (r * s)%:E) => //=. + exists (r * s)%:E. + by exists s => //; rewrite EFinM. + by rewrite EFinN. +by rewrite EFinN muleN -EFinM EFinN. +Qed. + +Lemma ereal_infZl A r : (0 < r)%R -> + ereal_inf [set r%:E * x%:E | x in A] = r%:E * ereal_inf (EFin @` A). +Proof. +move=> r0; rewrite /ereal_inf muleN; congr -%E. +exact: ereal_infZl'. +Qed. + +End ereal_supZ. + Section essential_supremum. Context d {T : measurableType d} {R : realType}. Variable mu : {measure set T -> \bar R}. @@ -1719,10 +1771,22 @@ rewrite [X in mu X](_ : _ = [set r | (0 < `|f r|%:E)%E]); last first. by rewrite -f0 ess_sup_max// f0. Qed. -Lemma ess_supMr f (r : R) : (0 <= r)%R -> (\forall x \ae mu, 0 <= f x)%R -> +Lemma ess_supMl f (r : R) : mu setT > 0 -> (0 <= r)%R -> ess_sup mu (cst r \* f)%R = r%:E * ess_sup mu f. Proof. -Admitted. +move=> muT0; rewrite le_eqVlt => /predU1P[<-|r0]. + rewrite mul0e (_ : _ \* f = cst 0)%R; first by rewrite ess_sup_cst. + by apply/funext => ?; rewrite /= mul0r. +rewrite -ereal_infZl//. +have rf s : (cst r \* f)%R @^-1` `]s, +oo[ = f%R @^-1` `]s / r, +oo[. + by apply/seteqP; split => [y|y]/=; rewrite !in_itv/= !andbT; + rewrite ltr_pdivrMr// mulrC. +congr ereal_inf; apply/seteqP; split => [_ [s /= M <-]|_ [s /= M <-]]/=. +- exists (s / r)%R; first by rewrite -rf. + by rewrite EFinM muleCA -EFinM divff ?mulr1// gt_eqF. +- exists (r * s)%R; last by rewrite EFinM. + by rewrite rf mulrAC divff ?mul1r// gt_eqF. +Qed. End essential_supremum. diff --git a/theories/measure.v b/theories/measure.v index 1478d48637..0776e1472f 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -5374,21 +5374,25 @@ Implicit Types f : T -> R. Definition ess_sup f := ereal_inf (EFin @` [set r | mu (f @^-1` `]r, +oo[) = 0]). -Lemma ess_sup_ger f x : 0 < mu [set: T] -> (forall t, x <= f t)%R -> - x%:E <= ess_sup f. +Lemma ess_sup_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) -> + x <= 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 => // t _ /=; rewrite in_itv/= (lt_le_trans _ (f0 t)). +move=> muT f0; apply: lb_ereal_inf => _ /= [r /eqP fr0 <-]; rewrite leNgt. +apply/negP => rx; apply/negP : fr0; rewrite gt_eqF// (_ : _ @^-1` _ = setT)//. +apply/seteqP; split => // t _ /=; rewrite in_itv/= andbT. +by rewrite -lte_fin (lt_le_trans _ (f0 t)). Qed. -Lemma ess_sup_ler f (r : R) : (forall x, f x <= r)%R -> ess_sup f <= r%:E. +Lemma ess_sup_ler f r : (forall t, (f t)%:E <= r) -> ess_sup f <= r. Proof. -move=> fr; apply: ereal_inf_le; apply/exists2P. +case: r => [r| |] fr; last 2 first. + by rewrite leey. + by have := fr point; rewrite leNgt ltNye. +apply: ereal_inf_le; apply/exists2P. exists r%:E => /=; split => //; apply/exists2P; exists r; split => //. rewrite preimage_itvoy [X in mu X](_ : _ = set0)// -subset0 => x //=. rewrite lt_neqAle => /andP[+ rlefx]. -by apply/negP/negPn; rewrite eq_le rlefx fr. +by apply/negP/negPn; rewrite eq_le rlefx/= -lee_fin. Qed. Lemma ess_sup_cst r : (0 < mu setT)%E -> (ess_sup (cst r) = r%:E)%E. From 2dda351e175904894c56c4a02d6fd0c1434cf68c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 2 Mar 2025 18:14:15 +0900 Subject: [PATCH 13/18] do w.o. measure_is_zero --- theories/lspace.v | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 9261fade4d..5cca442942 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -271,8 +271,8 @@ case: p p1 f => //[r r1 f|]. rewrite integralZl//; last first. apply /integrableP; split. apply: measurableT_comp => //. - rewrite [X in measurable_fun _ X](_ : _ = (@powR R)^~ r \o normr \o f)//. - by apply: measurableT_comp => //; apply: measurableT_comp. + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. + exact: measurableT_comp. apply: (@lty_poweRy _ _ r^-1). by rewrite gt_eqF// invr_gt0 ?(lt_le_trans ltr01). have -> : ((\int[mu]_x `|(`|f x| `^ r)%:E|) `^ r^-1 = 'N[mu]_r%:E[f])%E. @@ -384,11 +384,6 @@ Qed. Local Open Scope ereal_scope. -Lemma measure_is_zero : mu [set: T] = 0%E -> mu = mzero. -Proof. -move=> mu0. -Admitted. - Lemma Lspace_inclusion (p q : \bar R) : forall (p1 : 1 <= p) (q1 : 1 <= q), mu [set: T] < +oo -> p < q -> @@ -399,8 +394,17 @@ rewrite le_eqVlt => /predU1P[mu0 p1 q1 _ _ f _|mu_pos]. rewrite /finite_norm unlock /Lnorm. move: p p1; case=> //; last by rewrite -mu0 ltxx ltry. move=> r r1. - rewrite measure_is_zero// integral_measure_zero. - by rewrite poweR0r ?ltry// gt_eqF// invr_gt0 (lt_le_trans ltr01). + under eq_integral. + move=> x _. + have -> : (`|f x| `^ r)%:E = `| (`|f x| `^ r) |%:E. + by rewrite ger0_norm// powR_ge0. + over. + rewrite /=. + rewrite (@integral_abs_eq0 _ _ _ _ setT setT (fun x => (`|f x| `^ r)%:E))//. + by rewrite poweR0r// invr_neq0// gt_eqF// -lte_fin (lt_le_trans _ r1). + apply/measurable_EFinP. + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ r)) => //. + exact: measurableT_comp. move: p q. case=> //[p|]; case=> //[q|] p1 q1; last first. have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). @@ -408,8 +412,7 @@ case=> //[p|]; case=> //[q|] p1 q1; last first. rewrite /finite_norm unlock /Lnorm mu_pos => supf_lty. rewrite poweR_lty// integral_fune_lt_pinfty => //. apply: measurable_bounded_integrable => //. - rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)%R//. - apply: measurableT_comp => //=. + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. exact: measurableT_comp. rewrite boundedE. near=> A=> x/= _. @@ -426,9 +429,8 @@ have := (@hoelder _ _ _ mu (fun x => `|f x| `^ p) (cst 1)%R r r')%R. rewrite (_ : (_ \* cst 1)%R = (fun x : T => `|f x| `^ p))%R -?fctM ?mulr1//. rewrite Lnorm_cst1 unlock /Lnorm invr1. have mfp : measurable_fun [set: T] (fun x : T => (`|f x| `^ p)%R). - rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)%R//. - apply: measurableT_comp => //=. - exact: measurableT_comp => //=. + apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. + exact: measurableT_comp. have m1 : measurable_fun [set: T] (@cst _ R 1%R). exact: measurable_cst. have r0 : (0 < r)%R by rewrite/r divr_gt0. From 473881eb8230ee54c6bbbad8da7f99b7df04e0d0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 2 Mar 2025 19:33:21 +0900 Subject: [PATCH 14/18] only one admit left in lspace.v --- theories/hoelder.v | 2 +- theories/lspace.v | 23 +++++++++++++++-------- theories/measurable_realfun.v | 14 +++++++++++++- 3 files changed, 29 insertions(+), 10 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 2b23d61266..6a5f0dfa29 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -189,7 +189,7 @@ rewrite -lte_fin. move=> mf mg p0 q0 pq f0; rewrite f0 mul0e Lnorm1 [leLHS](_ : _ = 0)//. rewrite (ae_eq_integral (cst 0)) => [|//||//|]; first by rewrite integral0. - by do 2 apply: measurableT_comp => //; exact: measurable_funM. -- apply: filterS (Lnorm_eq0_eq0 mf p0 f0) => x /(_ I)[] + _. +- apply: filterS (Lnorm_eq0_eq0 mf p0 f0) => x /(_ I) + _. by rewrite normrM => ->; rewrite normr0 mul0r. Qed. diff --git a/theories/lspace.v b/theories/lspace.v index 5cca442942..6b61072781 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -117,6 +117,7 @@ by under eq_integral => i _ do rewrite powRr1//. Qed. Let le12 : (1 <= 2%:E :> \bar R)%E. +Proof. rewrite lee_fin. rewrite (ler_nat _ 1 2). by []. @@ -355,7 +356,7 @@ HB.instance Definition _ := nm ler_Lnorm_add Lnorm_natmul LnormN. *) -(* todo: add equivalent of mx_normZ and HB instance *) +(* TODO: add equivalent of mx_normZ and HB instance *) Lemma nm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. Proof. @@ -410,14 +411,20 @@ case=> //[p|]; case=> //[q|] p1 q1; last first. have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). move=> muoo _ f. rewrite /finite_norm unlock /Lnorm mu_pos => supf_lty. - rewrite poweR_lty// integral_fune_lt_pinfty => //. - apply: measurable_bounded_integrable => //. + rewrite poweR_lty//. + have : measurable_fun setT (normr \o f) by exact/measurableT_comp. + move/ess_sup_bounded => /(_ _ supf_lty)[M fM]. + rewrite (@le_lt_trans _ _ (\int[mu]_x (M `^ p)%:E)); [by []| |]; last first. + by rewrite integral_cst// lte_mul_pinfty// lee_fin powR_ge0. + apply: ae_ge0_le_integral => //. + - by move=> x _; rewrite lee_fin powR_ge0. + apply/measurable_EFinP. apply: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)) => //. exact: measurableT_comp. - rewrite boundedE. - near=> A=> x/= _. - rewrite norm_powR// normr_id normr1 mulr1. - admit. + - by move=> x _; rewrite lee_fin powR_ge0. + apply: filterS fM => t/= ftM _. + rewrite lee_fin ge0_ler_powR//; first exact: ltW. + by rewrite nnegrE (le_trans _ ftM). move=> mu_fin pleq f ffin. have:= ffin; rewrite /finite_norm. have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). @@ -453,6 +460,6 @@ rewrite muleC lte_mul_pinfty ?fin_numElt?poweR_ge0//. by rewrite (lt_le_trans _ (poweR_ge0 _ _)) ?ltNyr// ?poweR_lty. rewrite poweR_lty// (lty_poweRy qinv0)//. by have:= ffin; rewrite /finite_norm unlock /Lnorm. -Admitted. +Qed. End Lspace_inclusion. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 1d5138b22e..a627bdf5b4 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -303,7 +303,7 @@ HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)). (* NB: Until we dropped support for Coq 8.12, we were using HB.instance (\bar (Real.sort R)) (ereal_isMeasurable (@measurable (@itvs_semiRingOfSets R))). -This was producing a warning but the alternative was failing with Coq 8.12 with +This was producing as warning but the alternative was failing with Coq 8.12 with the following message (according to the CI): # [redundant-canonical-projection,typechecker] # forall (T : measurableType) (f : T -> R), measurable_fun setT f @@ -1691,6 +1691,18 @@ Variable mu : {measure set T -> \bar R}. Implicit Types f : T -> R. Local Open Scope ereal_scope. +Lemma ess_sup_bounded f : measurable_fun setT f -> ess_sup mu f < +oo -> + exists M, \forall x \ae mu, (f x <= M)%R. +Proof. +move=> mf /ereal_inf_lt[_ /= [r fr0] <-] _. +exists r, (f @^-1` `]r, +oo[); split => //. + rewrite (_ : _ @^-1` _ = [set t | r%:E < (f t)%:E]); last first. + by apply/seteqP; split => [x|x]/=; rewrite in_itv/= andbT. + rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. + by apply/measurable_EFinP; exact/measurableT_comp. +by move=> t/= ftr; rewrite in_itv/= andbT ltNge; exact/negP. +Qed. + Lemma ess_sup_max f : measurable_fun setT f -> ess_sup mu (normr \o f) != -oo -> mu [set r | ess_sup mu (normr \o f) < `|f r|%:E] = 0. From 934c5ebcc8678753d15076fc25c725dd88dc7433 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 2 Mar 2025 19:38:10 +0900 Subject: [PATCH 15/18] typo --- theories/measurable_realfun.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index a627bdf5b4..0660fe36c1 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -303,7 +303,7 @@ HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)). (* NB: Until we dropped support for Coq 8.12, we were using HB.instance (\bar (Real.sort R)) (ereal_isMeasurable (@measurable (@itvs_semiRingOfSets R))). -This was producing as warning but the alternative was failing with Coq 8.12 with +This was producing a warning but the alternative was failing with Coq 8.12 with the following message (according to the CI): # [redundant-canonical-projection,typechecker] # forall (T : measurableType) (f : T -> R), measurable_fun setT f From 509203cd443c9e8c32ea08acf78ce2461612559f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 3 Mar 2025 13:13:14 +0900 Subject: [PATCH 16/18] ess_supD --- theories/measurable_realfun.v | 72 ++++++++++++++++++++++++++++++++++- 1 file changed, 71 insertions(+), 1 deletion(-) diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 0660fe36c1..708cc77c8f 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1688,7 +1688,7 @@ End ereal_supZ. Section essential_supremum. Context d {T : measurableType d} {R : realType}. Variable mu : {measure set T -> \bar R}. -Implicit Types f : T -> R. +Implicit Types f g : T -> R. Local Open Scope ereal_scope. Lemma ess_sup_bounded f : measurable_fun setT f -> ess_sup mu f < +oo -> @@ -1800,6 +1800,76 @@ congr ereal_inf; apply/seteqP; split => [_ [s /= M <-]|_ [s /= M <-]]/=. by rewrite rf mulrAC divff ?mul1r// gt_eqF. Qed. +Lemma ess_sup_ub f : measurable_fun setT f -> ess_sup mu (normr \o f) != -oo -> + {ae mu, forall x, `|f x|%:E <= ess_sup mu (normr \o f)}. +Proof. +move=> mf fNy. +have [->|] := eqVneq (ess_sup mu (normr \o f)) +oo. + by apply/nearW => ?; rewrite leey. +rewrite -ltey => fy. +exists [set r | ess_sup mu (normr \o f) < `|f r|%:E]. +split. +- rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. + by apply/measurable_EFinP; exact/measurableT_comp. +- exact: ess_sup_max. +- by move=> t/= /negP; rewrite -ltNge. +Qed. + +Lemma ess_supD f g : + measurable_fun setT f -> measurable_fun setT g -> + ess_sup mu (normr \o f) != -oo -> ess_sup mu (normr \o g) != -oo -> + ess_sup mu (normr \o (f \+ g)) <= + ess_sup mu (normr \o f) + ess_sup mu (normr \o g). +Proof. +move=> mf mg fNy gNy. +have [->|] := eqVneq (ess_sup mu (normr \o f)) +oo. + by rewrite addye// leey. +rewrite -ltey => fy. +have [->|] := eqVneq (ess_sup mu (normr \o g)) +oo. + by rewrite addey// leey. +rewrite -ltey => gy. +pose a := ess_sup mu (normr \o f); pose b := ess_sup mu (normr \o g). +have a_fin_num : a \is a fin_num by rewrite fin_real// fy andbT ltNye. +have b_fin_num : b \is a fin_num by rewrite fin_real// gy andbT ltNye. +have fa : {ae mu, forall x, `|f x|%:E <= a}. + exact: ess_sup_ub. +have gb : {ae mu, forall x, `|g x|%:E <= b}. + exact: ess_sup_ub. +have {fa gb}fg : + {ae mu, forall x, (((normr \o f) \+ (normr \o g)) x)%:E <= a + b}. + case: fa => A [mA A0 Af]. + case: gb => B [mB B0 Bg]. + exists (A `|` B); split; first exact: measurableU. + by rewrite measureU0. + move=> t/= /negP; rewrite -ltNge => abfg. + have [At|At] := pselect (A t); [by left|right]. + apply: Bg => //=. + apply: contra_not At => gb. + apply: Af => /= fa. + have : (`|f t|%R + `|g t|%R)%E%:E <= a + b. + by rewrite EFinD leeD. + by rewrite leNgt abfg. +apply: ereal_inf_lbound => /=. +exists (fine a + fine b). + case: fg => N [mN N0 fgN]. + apply/eqP; rewrite eq_le measure_ge0 andbT -N0. + rewrite le_measure ?inE//. + rewrite -[X in measurable X]setTI. + have : measurable_fun setT (normr \o (f \+ g)). + apply: measurableT_comp => //. + exact: measurable_funD. + exact. + apply: subset_trans fgN => t/=. + rewrite in_itv/= andbT => abfg. + apply/negP; rewrite -ltNge. + rewrite -lte_fin in abfg. + (* TODO: we don't have lee_absD? *) + rewrite (@lt_le_trans _ _ `|(f t + g t)|%:E)%R//. + by move: abfg; rewrite EFinD !fineK. + exact: ler_normD. +by rewrite EFinD !fineK. +Qed. + End essential_supremum. Section egorov. From 6f2b1d6f479498591a0831240106a3bd8cd9c1a0 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Mon, 3 Mar 2025 14:28:52 +0900 Subject: [PATCH 17/18] wip (#26) * minkowskie --- theories/hoelder.v | 28 ++++++++++++++++++++++++++++ theories/lspace.v | 12 ++---------- 2 files changed, 30 insertions(+), 10 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 6a5f0dfa29..6391d6677f 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -560,4 +560,32 @@ apply: minkowski => //. apply: measurableT_comp => //. Qed. +Lemma le_ess_sup (f g : T -> R) : + measurable_fun setT f -> measurable_fun setT g -> + (forall x, f x <= g x)%R -> ess_sup mu f <= ess_sup mu g. +Proof. +rewrite /ess_sup => mf mg h. +apply: le_ereal_inf => x [r]/= mu0 rx. +exists r => //. +move: mu0. +apply: subset_measure0. +- by rewrite -[X in _ X]setTI; exact: mf. +- by rewrite -[X in _ X]setTI; exact: mg. +move=> t/=. +rewrite !in_itv !andbT/= => fgtt. +by rewrite (lt_le_trans fgtt)//. +Qed. + +Lemma minkowskie (f g : T -> R) (p : \bar R) : + measurable_fun setT f -> measurable_fun setT g -> 1 <= p -> + 'N_p[(f \+ g)%R] <= 'N_p[f] + 'N_p[g]. +Proof. +case: p => //[r|]; first exact: minkowski. +move=> mf mg _. +rewrite unlock /Lnorm. +case: ifPn => mugt0; last by rewrite adde0 lexx. +apply: ess_supD => //. +all: by rewrite gt_eqF// (lt_le_trans ltNy0)// ess_sup_ger// => x/=; rewrite lee_fin normr_ge0. +Qed. + End minkowski. diff --git a/theories/lspace.v b/theories/lspace.v index 6b61072781..a7bdd757a1 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -195,15 +195,6 @@ Lemma sub_lfun_mfun : {subset lfun <= mfun}. Proof. by move=> x /andP[]. Qed. Lemma sub_lfun_finlfun : {subset lfun <= finlfun}. Proof. by move=> x /andP[]. Qed. End lfun_pred. -Lemma minkowskie [d : measure_display] [T : measurableType d] [R : realType] - (mu : measure T R) [f g : T -> R] [p : \bar R] : - measurable_fun [set: T] f -> - measurable_fun [set: T] g -> - (1 <= p)%E -> ('N[mu]_p[(f \+ g)%R] <= 'N[mu]_p[f] + 'N[mu]_p[g])%E. -Proof. -(* TODO: Jairo is working on this *) -Admitted. - Section lfun. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E). @@ -298,7 +289,8 @@ move: (lfun_Sub _) (lfun_Sub _) => {fP} f {gP} g. rewrite !inE rpredD ?rpredZ ?mfunP//=. apply: mem_set => /=. rewrite /finite_norm. -apply: (le_lt_trans (minkowskie _ _ _ _)) => //=. +apply: le_lt_trans. + apply: minkowskie => //. suff: a *: (g : T -> R) \in mfun by exact: set_mem. by rewrite rpredZ//; exact: mfunP. rewrite lte_add_pinfty//; last exact: lfuny. From 899dce35326e863bfba6b1c7cac5fc0fc44f4513 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 9 Mar 2025 17:50:27 +0100 Subject: [PATCH 18/18] refactor essential_supremum / infimum theory --- _CoqProject | 1 + classical/boolp.v | 24 ++ classical/classical_sets.v | 5 + classical/mathcomp_extra.v | 14 ++ theories/Make | 1 + theories/all_analysis.v | 1 + theories/ereal.v | 90 +++++++- theories/ess_sup_inf.v | 344 +++++++++++++++++++++++++++++ theories/hoelder.v | 73 +++---- theories/lspace.v | 38 ++-- theories/measurable_realfun.v | 401 +++++++++++----------------------- theories/measure.v | 72 ++---- theories/normedtype.v | 2 +- theories/sequences.v | 3 + 14 files changed, 677 insertions(+), 392 deletions(-) create mode 100644 theories/ess_sup_inf.v diff --git a/_CoqProject b/_CoqProject index 89f1474794..41bbb4a235 100644 --- a/_CoqProject +++ b/_CoqProject @@ -67,6 +67,7 @@ theories/homotopy_theory/homotopy.v theories/homotopy_theory/wedge_sigT.v theories/homotopy_theory/continuous_path.v +theories/ess_sup_inf.v theories/separation_axioms.v theories/function_spaces.v theories/ereal.v diff --git a/classical/boolp.v b/classical/boolp.v index 3c3b726907..80607a9dab 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -329,6 +329,30 @@ Proof. by rewrite /asbool; case: pselect=> h; constructor. Qed. Lemma asboolW (P : Prop) : `[

] -> P. Proof. by case: asboolP. Qed. +Lemma orW A B : A \/ B -> A + B. +Proof. +have [|NA] := asboolP A; first by left. +have [|NB] := asboolP B; first by right. +by move=> AB; exfalso; case: AB. +Qed. + +Lemma or3W A B C : [\/ A, B | C] -> A + B + C. +Proof. +have [|NA] := asboolP A; first by left; left. +have [|NB] := asboolP B; first by left; right. +have [|NC] := asboolP C; first by right. +by move=> ABC; exfalso; case: ABC. +Qed. + +Lemma or4W A B C D : [\/ A, B, C | D] -> A + B + C + D. +Proof. +have [|NA] := asboolP A; first by left; left; left. +have [|NB] := asboolP B; first by left; left; right. +have [|NC] := asboolP C; first by left; right. +have [|ND] := asboolP D; first by right. +by move=> ABCD; exfalso; case: ABCD. +Qed. + (* Shall this be a coercion ?*) Lemma asboolT (P : Prop) : P -> `[

]. Proof. by case: asboolP. Qed. diff --git a/classical/classical_sets.v b/classical/classical_sets.v index c550fdeaa8..5427168b9b 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1523,6 +1523,9 @@ Proof. by move=> b [x [Aa Ba <-]]; split; apply: imageP. Qed. Lemma nonempty_image f A : f @` A !=set0 -> A !=set0. Proof. by case=> b [a]; exists a. Qed. +Lemma image_nonempty f A : A !=set0 -> f @` A !=set0. +Proof. by move=> [x] Ax; exists (f x), x. Qed. + Lemma image_subset f A B : A `<=` B -> f @` A `<=` f @` B. Proof. by move=> AB _ [a Aa <-]; exists a => //; apply/AB. Qed. @@ -1645,6 +1648,8 @@ Proof. by rewrite preimage_false; under eq_fun do rewrite inE. Qed. End image_lemmas. Arguments sub_image_setI {aT rT f A B} t _. +Arguments subset_set1 {_ _ _}. +Arguments subset_set2 {_ _ _ _}. Lemma image2_subset {aT bT rT : Type} (f : aT -> bT -> rT) (A B : set aT) (C D : set bT) : A `<=` B -> C `<=` D -> diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 1795e300d6..7572527453 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -681,3 +681,17 @@ Proof. exact: comparable_max_le_max. Qed. Lemma real_sqrtC {R : numClosedFieldType} (x : R) : 0 <= x -> sqrtC x \in Num.real. Proof. by rewrite -sqrtC_ge0; apply: ger0_real. Qed. + +Lemma eq_exists2l (A : Type) (P P' Q : A -> Prop) : + (forall x, P x <-> P' x) -> + (exists2 x, P x & Q x) <-> (exists2 x, P' x & Q x). +Proof. +by move=> eqQ; split=> -[x p q]; exists x; move: p q; rewrite ?eqQ. +Qed. + +Lemma eq_exists2r (A : Type) (P Q Q' : A -> Prop) : + (forall x, Q x <-> Q' x) -> + (exists2 x, P x & Q x) <-> (exists2 x, P x & Q' x). +Proof. +by move=> eqP; split=> -[x p q]; exists x; move: p q; rewrite ?eqP. +Qed. diff --git a/theories/Make b/theories/Make index aac6828d70..ff9334288c 100644 --- a/theories/Make +++ b/theories/Make @@ -9,6 +9,7 @@ ereal.v landau.v +ess_sup_inf.v topology_theory/topology.v topology_theory/bool_topology.v topology_theory/compact.v diff --git a/theories/all_analysis.v b/theories/all_analysis.v index b567c76901..2a745ee6ac 100644 --- a/theories/all_analysis.v +++ b/theories/all_analysis.v @@ -25,3 +25,4 @@ From mathcomp Require Export charge. From mathcomp Require Export kernel. From mathcomp Require Export pi_irrational. From mathcomp Require Export gauss_integral. +From mathcomp Require Export ess_sup_inf. diff --git a/theories/ereal.v b/theories/ereal.v index d673952373..181b04e4b9 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -463,6 +463,21 @@ rewrite lteNl => /ereal_sup_gt[_ [y Sy <-]]. by rewrite lteNl oppeK => xlty; exists y. Qed. +Lemma ereal_infEN S : ereal_inf S = - ereal_sup [set - x | x in S]. +Proof. by []. Qed. + +Lemma ereal_supN S : ereal_sup [set - x | x in S] = - ereal_inf S. +Proof. by rewrite oppeK. Qed. + +Lemma ereal_infN S : ereal_inf [set - x | x in S] = - ereal_sup S. +Proof. +rewrite /ereal_inf; congr (- ereal_sup _) => /=. +by rewrite image_comp/=; under eq_imagel do rewrite /= oppeK; rewrite image_id. +Qed. + +Lemma ereal_supEN S : ereal_sup S = - ereal_inf [set - x | x in S]. +Proof. by rewrite ereal_infN oppeK. Qed. + End ereal_supremum. Section ereal_supremum_realType. @@ -523,7 +538,7 @@ Proof. by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ubound. Qed. -Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S. +Lemma ereal_sup_ge S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S. Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ubound. Qed. Lemma ereal_sup_ninfty S : ereal_sup S = -oo <-> S `<=` [set -oo]. @@ -591,11 +606,84 @@ rewrite -ereal_sup_EFin; [|exact/has_lb_ubN|exact/nonemptyN]. by rewrite !image_comp. Qed. +Lemma ereal_supP S x : + reflect (forall y : \bar R, S y -> y <= x) (ereal_sup S <= x). +Proof. +apply/(iffP idP) => [+ y Sy|]. + by move=> /(le_trans _)->//; rewrite ereal_sup_ge//; exists y. +apply: contraPP => /negP; rewrite -ltNge -existsPNP. +by move=> /ereal_sup_gt[y Sy ltyx]; exists y => //; rewrite lt_geF. +Qed. + +Lemma ereal_infP S x : + reflect (forall y : \bar R, S y -> x <= y) (x <= ereal_inf S). +Proof. +rewrite leeNr; apply/(equivP (ereal_supP _ _)); setoid_rewrite leeNr. +split=> [ge_x y Sy|ge_x _ [y Sy <-]]; rewrite ?oppeK// ?ge_x//. +by rewrite -[y]oppeK ge_x//; exists y. +Qed. + +Lemma ereal_sup_gtP S x : + reflect (exists2 y : \bar R, S y & x < y) (x < ereal_sup S). +Proof. +rewrite ltNge; apply/(equivP negP); rewrite -(rwP (ereal_supP _ _)) -existsPNP. +by apply/eq_exists2r => y; rewrite (rwP2 negP idP) -ltNge. +Qed. + +Lemma ereal_inf_ltP S x : + reflect (exists2 y : \bar R, S y & y < x) (ereal_inf S < x). +Proof. +rewrite ltNge; apply/(equivP negP); rewrite -(rwP (ereal_infP _ _)) -existsPNP. +by apply/eq_exists2r => y; rewrite (rwP2 negP idP) -ltNge. +Qed. + +Lemma ereal_inf_leP S x : S (ereal_inf S) -> + reflect (exists2 y : \bar R, S y & y <= x) (ereal_inf S <= x). +Proof. +move=> Sinf; apply: (iffP idP); last exact: ereal_inf_le. +by move=> Sx; exists (ereal_inf S). +Qed. + +Lemma ereal_sup_geP S x : S (ereal_sup S) -> + reflect (exists2 y : \bar R, S y & x <= y) (x <= ereal_sup S). +Proof. +move=> Ssup; apply: (iffP idP); last exact: ereal_sup_ge. +by move=> Sx; exists (ereal_sup S). +Qed. + +Lemma lb_ereal_infNy_adherent S e : + ereal_inf S = -oo -> exists2 x : \bar R, S x & x < e%:E. +Proof. by move=> infNy; apply/ereal_inf_ltP; rewrite infNy ltNyr. Qed. + +Lemma ereal_sup_real : @ereal_sup R (range EFin) = +oo. +Proof. +rewrite hasNub_ereal_sup//; last by exists 0%R. +by apply/has_ubPn => x; exists (x+1)%R => //; rewrite ltrDl. +Qed. + +Lemma ereal_inf_real : @ereal_inf R (range EFin) = -oo. +Proof. +rewrite /ereal_inf [X in ereal_sup X](_ : _ = range EFin); last first. + apply/seteqP; split => x/=[y]. + by move=> [z] _ <- <-; exists (-z)%R. + by move=> _ <-; exists (-y%:E); first (by exists (-y)%R); rewrite oppeK. +by rewrite ereal_sup_real. +Qed. + End ereal_supremum_realType. #[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_sup_ubound`.")] Notation ereal_sup_ub := ereal_sup_ubound (only parsing). #[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_inf_lbound`.")] Notation ereal_inf_lb := ereal_inf_lbound (only parsing). +#[deprecated(since="mathcomp-analysis 1.10.0", note="Renamed `ereal_sup_ge`.")] +Notation ereal_sup_le := ereal_sup_ge. + +Arguments ereal_supP {R S x}. +Arguments ereal_infP {R S x}. +Arguments ereal_sup_gtP {R S x}. +Arguments ereal_inf_ltP {R S x}. +Arguments ereal_sup_geP {R S x}. +Arguments ereal_inf_leP {R S x}. Lemma restrict_abse T (R : numDomainType) (f : T -> \bar R) (D : set T) : (abse \o f) \_ D = abse \o (f \_ D). diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v new file mode 100644 index 0000000000..71ad495f55 --- /dev/null +++ b/theories/ess_sup_inf.v @@ -0,0 +1,344 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. +From mathcomp Require Import topology normedtype sequences esum numfun. +From mathcomp Require Import measure lebesgue_measure. + +(**md**************************************************************************) +(* ``` *) +(* ess_sup f == essential supremum of the function f : T -> R where T is a *) +(* semiRingOfSetsType and R is a realType *) +(* ess_inf f == essential infimum *) +(* ``` *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +Section essential_supremum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types (f g : T -> \bar R) (h k : T -> R). + +(* TODO: move *) +Lemma measure0_ae (P : set T) : mu [set: T] = 0 -> \forall x \ae mu, P x. +Proof. by move=> x; exists setT; split. Qed. + +Definition ess_sup f := ereal_inf [set y | \forall x \ae mu, f x <= y]. + +Lemma ess_supEae (f : T -> \bar R) : + ess_sup f = ereal_inf [set y | \forall x \ae mu, f x <= y]. +Proof. by []. Qed. + +Lemma ae_le_measureP f y : measurable_fun setT f -> + (\forall x \ae mu, f x <= y) <-> (mu (f @^-1` `]y, +oo[) = 0). +Proof. +move=> f_meas; have fVroo_meas : d.-measurable (f @^-1` `]y, +oo[). + by rewrite -[_ @^-1` _]setTI; apply/f_meas=> //; exact/emeasurable_itv. +have setCfVroo : (f @^-1` `]y, +oo[) = ~` [set x | f x <= y]. + by apply: setC_inj; rewrite preimage_setC setCitv/= set_itvxx setU0 setCK. +split. + move=> [N [dN muN0 inN]]; rewrite (subset_measure0 _ dN)// => x. + by rewrite setCfVroo; apply: inN. +set N := (X in mu X) => muN0; exists N; rewrite -setCfVroo. +by split => //; exact: fVroo_meas. +Qed. + +Lemma ess_supEmu0 (f : T -> \bar R) : measurable_fun setT f -> + ess_sup f = ereal_inf [set y | mu (f @^-1` `]y, +oo[) = 0]. +Proof. +by move=> ?; congr (ereal_inf _); apply/predeqP => r; exact: ae_le_measureP. +Qed. + +Lemma ess_sup_ge f : \forall x \ae mu, f x <= ess_sup f. +Proof. +rewrite ess_supEae//; set I := (X in ereal_inf X). +have [->|IN0] := eqVneq I set0. + by rewrite ereal_inf0; apply: nearW => ?; rewrite leey. +have [u uI uinf] := ereal_inf_seq IN0. +rewrite -(cvg_lim _ uinf)//; near=> x. +rewrite lime_ge//; first by apply/cvgP: uinf. +by apply: nearW; near: x; apply/ae_foralln => n; apply: uI. +Unshelve. all: by end_near. Qed. + +Lemma ess_supP f a : reflect (\forall x \ae mu, f x <= a) (ess_sup f <= a). +Proof. +apply: (iffP (ereal_inf_leP _)) => /=; last 2 first. +- by move=> [y fy ya]; near do apply: le_trans ya. +- by move=> fa; exists a. +by rewrite -ess_supEae//; exact: ess_sup_ge. +Unshelve. all: by end_near. Qed. + +Lemma le_ess_sup f g : (\forall x \ae mu, f x <= g x) -> ess_sup f <= ess_sup g. +Proof. +move=> fg; apply/ess_supP => //. +near do rewrite (le_trans (near fg _ _))//=. +exact: ess_sup_ge. +Unshelve. all: by end_near. Qed. + +Lemma eq_ess_sup f g : (\forall x \ae mu, f x = g x) -> ess_sup f = ess_sup g. +Proof. +move=> fg; apply/eqP; rewrite eq_le !le_ess_sup//=; + by apply: filterS fg => x ->. +Qed. + +Lemma ess_sup_cst r : 0 < mu [set: T] -> ess_sup (cst r) = r. +Proof. +move=> muT_gt0; apply/eqP; rewrite eq_le; apply/andP; split. + by apply/ess_supP => //; apply: nearW. +have ae_proper := ae_properfilter_algebraOfSetsType muT_gt0. +by near (almost_everywhere mu) => x; near: x; apply: ess_sup_ge. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_ae_cst f r : 0 < mu [set: T] -> + (\forall x \ae mu, f x = r) -> ess_sup f = r. +Proof. by move=> muT_gt0 /= /eq_ess_sup->; rewrite ess_sup_cst. Qed. + +Lemma ess_sup_gee f y : 0 < mu [set: T] -> + (\forall x \ae mu, y <= f x)%E -> y <= ess_sup f. +Proof. by move=> *; rewrite -(ess_sup_cst y)//; apply: le_ess_sup. Qed. + +Lemma abs_sup_eq0_ae_eq f : ess_sup (abse \o f) = 0 -> f = \0 %[ae mu]. +Proof. +move=> ess_sup_f_eq0; near=> x => _ /=; apply/eqP. +rewrite -abse_eq0 eq_le abse_ge0 andbT; near: x. +by apply/ess_supP; rewrite ess_sup_f_eq0. +Unshelve. all: by end_near. Qed. + +Lemma abs_ess_sup_eq0 f : mu [set: T] > 0 -> + f = \0 %[ae mu] -> ess_sup (abse \o f) = 0. +Proof. +move=> muT_gt0 f0; apply/eqP; rewrite eq_le; apply/andP; split. + by apply/ess_supP => /=; near do rewrite (near f0 _ _)//= normr0//. +by rewrite -[0]ess_sup_cst// le_ess_sup//=; near=> x; rewrite abse_ge0. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_pZl f (a : R) : (0 < a)%R -> + (ess_sup (cst a%:E \* f) = a%:E * ess_sup f). +Proof. +move=> /[dup] /ltW a_ge0 a_gt0. +gen have esc_le : a f a_ge0 a_gt0 / + (ess_sup (cst a%:E \* f) <= a%:E * ess_sup f)%E. + by apply/ess_supP; near do rewrite /cst/= lee_pmul2l//; apply/ess_supP. +apply/eqP; rewrite eq_le esc_le// -lee_pdivlMl//=. +apply: le_trans (esc_le _ _ _ _); rewrite ?invr_gt0 ?invr_ge0//. +by under eq_fun do rewrite muleA -EFinM mulVf ?mul1e ?gt_eqF//. +Unshelve. all: by end_near. Qed. + +Lemma ess_supZl f (a : R) : mu [set: T] > 0 -> (0 <= a)%R -> + (ess_sup (cst a%:E \* f) = a%:E * ess_sup f). +Proof. + +move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_sup_pZl. +by under eq_fun do rewrite mul0e; rewrite mul0e ess_sup_cst. +Qed. + +Lemma ess_sup_eqNyP f : ess_sup f = -oo <-> \forall x \ae mu, f x = -oo. +Proof. +rewrite (rwP eqP) -leeNy_eq (eq_near (fun=> rwP eqP)). +by under eq_near do rewrite -leeNy_eq; apply/(rwP2 idP (ess_supP _ _)). +Qed. + +Lemma ess_supD f g : ess_sup (f \+ g) <= ess_sup f + ess_sup g. +Proof. +by apply/ess_supP; near do rewrite lee_add//; apply/ess_supP. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_absD f g : + ess_sup (abse \o (f \+ g)) <= ess_sup (abse \o f) + ess_sup (abse \o g). +Proof. +rewrite (le_trans _ (ess_supD _ _))// le_ess_sup//. +by apply/nearW => x; apply/lee_abs_add. +Qed. + +End essential_supremum. +Arguments ess_sup_ae_cst {d T R mu f}. +Arguments ess_supP {d T R mu f a}. + +Section real_essential_supremum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> R. + +Notation ess_supr f := (ess_sup mu (EFin \o f)). + +Lemma ess_supr_bounded f : ess_supr f < +oo -> + exists M, \forall x \ae mu, (f x <= M)%R. +Proof. +set g := EFin \o f => ltfy; have [|supfNy] := eqVneq (ess_sup mu g) -oo. + by move=> /ess_sup_eqNyP fNy; exists 0%:R; apply: filterS fNy. +have supf_fin : ess_supr f \is a fin_num by case: ess_sup ltfy supfNy. +by exists (fine (ess_supr f)); near do rewrite -lee_fin fineK//; apply/ess_supP. +Unshelve. all: by end_near. Qed. + +Lemma ess_sup_eqr0_ae_eq f : ess_supr (normr \o f) = 0 -> f = 0%R %[ae mu]. +Proof. +under [X in ess_sup _ X]eq_fun do rewrite /= -abse_EFin. +move=> /abs_sup_eq0_ae_eq; apply: filterS => x /= /(_ _)/eqP. +by rewrite eqe => /(_ _)/eqP. +Qed. + +Lemma ess_suprZl f (y : R) : mu setT > 0 -> (0 <= y)%R -> + ess_supr (cst y \* f)%R = y%:E * ess_supr f. +Proof. by move=> muT_gt0 r_ge0; rewrite -ess_supZl. Qed. + +Lemma ess_sup_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) -> + x <= ess_supr f. +Proof. by move=> muT f0; apply/ess_sup_gee => //=; apply: nearW. Qed. + +Lemma ess_sup_ler f y : (forall t, (f t)%:E <= y) -> ess_supr f <= y. +Proof. by move=> ?; apply/ess_supP; apply: nearW. Qed. + +Lemma ess_sup_cstr y : (0 < mu setT)%E -> (ess_supr (cst y) = y%:E)%E. +Proof. by move=> muN0; rewrite (ess_sup_ae_cst y%:E)//=; apply: nearW. Qed. + +Lemma ess_suprD f g : ess_supr (f \+ g) <= ess_supr f + ess_supr g. +Proof. by rewrite (le_trans _ (ess_supD _ _ _)). Qed. + +Lemma ess_sup_normD f g : + ess_supr (normr \o (f \+ g)) <= ess_supr (normr \o f) + ess_supr (normr \o g). +Proof. +rewrite (le_trans _ (ess_suprD _ _))// le_ess_sup//. +by apply/nearW => x; apply/ler_normD. +Qed. + +End real_essential_supremum. +Notation ess_supr mu f := (ess_sup mu (EFin \o f)). + +Section essential_infimum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> \bar R. + +Definition ess_inf f := ereal_sup [set y | \forall x \ae mu, y <= f x]. +Notation ess_sup := (ess_sup mu). + +Lemma ess_infEae (f : T -> \bar R) : + ess_inf f = ereal_sup [set y | \forall x \ae mu, y <= f x]. +Proof. by []. Qed. + +Lemma ess_infEN (f : T -> \bar R) : ess_inf f = - ess_sup (\- f). +Proof. +rewrite ess_supEae ess_infEae ereal_infEN oppeK; congr (ereal_sup _). +apply/seteqP; split=> [y /= y_le|_ [/= y y_ge <-]]. + by exists (- y); rewrite ?oppeK//=; apply: filterS y_le => x; rewrite leeN2. +by apply: filterS y_ge => x; rewrite leeNl. +Qed. + +Lemma ess_supEN (f : T -> \bar R) : ess_sup f = - ess_inf (\- f). +Proof. +by rewrite ess_infEN oppeK; apply/eq_ess_sup/nearW => ?; rewrite oppeK. +Qed. + +Lemma ess_infN (f : T -> \bar R) : ess_inf (\- f) = - ess_sup f. +Proof. by rewrite ess_supEN oppeK. Qed. + +Lemma ess_supN (f : T -> \bar R) : ess_sup (\- f) = - ess_inf f. +Proof. by rewrite ess_infEN oppeK. Qed. + +Lemma ess_infP f a : reflect (\forall x \ae mu, a <= f x) (a <= ess_inf f). +Proof. +by rewrite ess_infEN leeNr; apply: (iffP ess_supP); + apply: filterS => x; rewrite leeN2. +Qed. + +Lemma ess_inf_le f : \forall x \ae mu, ess_inf f <= f x. +Proof. exact/ess_infP. Qed. + +Lemma le_ess_inf f g : (\forall x \ae mu, f x <= g x) -> ess_inf f <= ess_inf g. +Proof. +move=> fg; apply/ess_infP => //. +near do rewrite (le_trans _ (near fg _ _))//=. +exact: ess_inf_le. +Unshelve. all: by end_near. Qed. + +Lemma eq_ess_inf f g : (\forall x \ae mu, f x = g x) -> ess_inf f = ess_inf g. +Proof. +move=> fg; apply/eqP; rewrite eq_le !le_ess_inf//=; + by apply: filterS fg => x ->. +Qed. + +Lemma ess_inf_cst r : 0 < mu [set: T] -> ess_inf (cst r) = r. +Proof. +by move=> ?; rewrite ess_infEN (ess_sup_ae_cst (- r)) ?oppeK//=; apply: nearW. +Qed. + +Lemma ess_inf_ae_cst f r : 0 < mu [set: T] -> + (\forall x \ae mu, f x = r) -> ess_inf f = r. +Proof. by move=> muT_gt0 /= /eq_ess_inf->; rewrite ess_inf_cst. Qed. + +Lemma ess_inf_gee f y : 0 < mu [set: T] -> + (\forall x \ae mu, y <= f x)%E -> y <= ess_inf f. +Proof. by move=> *; rewrite -(ess_inf_cst y)//; apply: le_ess_inf. Qed. + +Lemma ess_inf_pZl f (a : R) : (0 < a)%R -> + (ess_inf (cst a%:E \* f) = a%:E * ess_inf f). +Proof. +move=> a_gt0; rewrite !ess_infEN muleN; congr (- _)%E. +by under eq_fun do rewrite -muleN; rewrite ess_sup_pZl. +Qed. + +Lemma ess_infZl f (a : R) : mu [set: T] > 0 -> (0 <= a)%R -> + (ess_inf (cst a%:E \* f) = a%:E * ess_inf f). +Proof. +move=> muTN0; case: ltgtP => // [a_gt0|<-] _; first exact: ess_inf_pZl. +by under eq_fun do rewrite mul0e; rewrite mul0e ess_inf_cst. +Qed. + +Lemma ess_inf_eqyP f : ess_inf f = +oo <-> \forall x \ae mu, f x = +oo. +Proof. +rewrite (rwP eqP) -leye_eq (eq_near (fun=> rwP eqP)). +by under eq_near do rewrite -leye_eq; apply/(rwP2 idP (ess_infP _ _)). +Qed. + +Lemma ess_infD f g : ess_inf (f \+ g) >= ess_inf f + ess_inf g. +Proof. +by apply/ess_infP; near do rewrite lee_add//; apply/ess_infP. +Unshelve. all: by end_near. Qed. + +End essential_infimum. +Arguments ess_inf_ae_cst {d T R mu f}. +Arguments ess_infP {d T R mu f a}. + +Section real_essential_infimum. +Context d {T : measurableType d} {R : realType}. +Variable mu : {measure set T -> \bar R}. +Implicit Types f : T -> R. + +Notation ess_infr f := (ess_inf mu (EFin \o f)). + +Lemma ess_infr_bounded f : ess_infr f > -oo -> + exists M, \forall x \ae mu, (f x >= M)%R. +Proof. +set g := EFin \o f => ltfy; have [|inffNy] := eqVneq (ess_inf mu g) +oo. + by move=> /ess_inf_eqyP fNy; exists 0%:R; apply: filterS fNy. +have inff_fin : ess_infr f \is a fin_num by case: ess_inf ltfy inffNy. +by exists (fine (ess_infr f)); near do rewrite -lee_fin fineK//; apply/ess_infP. +Unshelve. all: by end_near. Qed. + +Lemma ess_infrZl f (y : R) : mu setT > 0 -> (0 <= y)%R -> + ess_infr (cst y \* f)%R = y%:E * ess_infr f. +Proof. by move=> muT_gt0 r_ge0; rewrite -ess_infZl. Qed. + +Lemma ess_inf_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) -> + x <= ess_infr f. +Proof. by move=> muT f0; apply/ess_inf_gee => //=; apply: nearW. Qed. + +Lemma ess_inf_ler f y : (forall t, y <= (f t)%:E) -> y <= ess_infr f. +Proof. by move=> ?; apply/ess_infP; apply: nearW. Qed. + +Lemma ess_inf_cstr y : (0 < mu setT)%E -> (ess_infr (cst y) = y%:E)%E. +Proof. by move=> muN0; rewrite (ess_inf_ae_cst y%:E)//=; apply: nearW. Qed. + +End real_essential_infimum. +Notation ess_infr mu f := (ess_inf mu (EFin \o f)). diff --git a/theories/hoelder.v b/theories/hoelder.v index 6391d6677f..56af8b4c91 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. From mathcomp Require Import topology normedtype sequences real_interval esum. From mathcomp Require Import measure measurable_realfun lebesgue_measure. -From mathcomp Require Import lebesgue_integral numfun exp convex. +From mathcomp Require Import lebesgue_integral numfun exp convex ess_sup_inf. (**md**************************************************************************) (* # Hoelder's Inequality *) @@ -38,12 +38,12 @@ Declare Scope Lnorm_scope. Local Open Scope ereal_scope. HB.lock Definition Lnorm {d} {T : measurableType d} {R : realType} - (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) := + (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> \bar R) := match p with - | p%:E => (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1 + | p%:E => (\int[mu]_x `|f x| `^ p) `^ p^-1 (* (mu (f @^-1` (setT `\ 0%R))) when p = 0? *) - | +oo%E => if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0 - | -oo%E => if mu [set: T] > 0 then ess_inf mu (normr \o f) else 0 + | +oo%E => if mu [set: T] > 0 then ess_sup mu (abse \o f) else 0 + | -oo%E => if mu [set: T] > 0 then ess_inf mu (abse \o f) else 0 end. Canonical locked_Lnorm := Unlockable Lnorm.unlock. Arguments Lnorm {d T R} mu p f. @@ -55,7 +55,7 @@ Variable mu : {measure set T -> \bar R}. Local Open Scope ereal_scope. Implicit Types (p : \bar R) (f g : T -> R) (r : R). -Local Notation "'N_ p [ f ]" := (Lnorm mu p f). +Local Notation "'N_ p [ f ]" := (Lnorm mu p (EFin \o f)). Lemma Lnorm0 p : 1 <= p -> 'N_p[cst 0%R] = 0. Proof. @@ -65,27 +65,25 @@ case: p => [r||//]. have r0 : r != 0%R by rewrite gt_eqF// (lt_le_trans _ r1). under eq_integral => x _ do rewrite /= normr0 powR0//. by rewrite integral0 poweR0r// invr_neq0. -case: ifPn => //mu0 _. -rewrite (_ : normr \o _ = 0%R); last by apply: funext => x/=; rewrite normr0. -exact: ess_sup_cst. +case: ifPn => //mu0 _; rewrite (ess_sup_ae_cst 0)//. +by apply: nearW => x; rewrite /= normr0. Qed. Lemma Lnorm1 f : 'N_1[f] = \int[mu]_x `|f x|%:E. Proof. -rewrite unlock invr1// poweRe1//. - by apply: eq_integral => t _; rewrite powRr1. -by apply: integral_ge0 => t _; rewrite powRr1. +rewrite unlock invr1// poweRe1//; under eq_integral do [rewrite poweRe1//=] => //. +exact: integral_ge0. Qed. Lemma Lnorm_ge0 p f : 0 <= 'N_p[f]. Proof. rewrite unlock; move: p => [r/=|/=|//]; first exact: poweR_ge0. - by case: ifPn => // /ess_sup_ger; apply => t/=. -- by case: ifPn => // muT0; apply: ess_inf_ge0 => //=. +- by case: ifPn => // muT0; apply/ess_infP/nearW => x /=. 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. +Proof. by move=> fg; congr Lnorm; apply/eq_fun => ?; rewrite /= fg. Qed. Lemma Lnorm_eq0_eq0 (f : T -> R) p : measurable_fun setT f -> (0 < p)%E -> 'N_p[f] = 0 -> f = 0%R %[ae mu]. @@ -103,7 +101,9 @@ case: p => [r||//]. move/(ae_eq_integral_abs _ measurableT mp). apply: filterS => x/= /[apply]. by case=> /powR_eq0_eq0 /eqP; rewrite normr_eq0 => /eqP. -- case: ifPn => [mu0 _|]; first exact: ess_sup_eq0_ae. +- case: ifPn => [mu0 _|]. + move=> /abs_sup_eq0_ae_eq/=. + by apply: filterS => x/= /(_ I) /eqP + _; rewrite eqe => /eqP. rewrite ltNge => /negbNE mu0 _ _. suffices mueq0: mu setT = 0 by exact: ae_eq0. by apply/eqP; rewrite eq_le mu0/=. @@ -118,19 +118,16 @@ Qed. Lemma oppr_Lnorm f p : 'N_p[\- f]%R = 'N_p[f]. Proof. -rewrite unlock /Lnorm; case: p => /= [r||//]. -- by under eq_integral => x _ do rewrite normrN. -- rewrite compA (_ : normr \o -%R = normr)//. - by apply: funext => x/=; exact: normrN. -- rewrite compA (_ : normr \o -%R = normr)//. - by apply: funext => x/=; exact: normrN. +have NfE : abse \o (EFin \o (\- f)%R) = abse \o EFin \o f. + by apply/funext => x /=; rewrite normrN. +rewrite unlock /Lnorm NfE; case: p => /= [r|//|//]. +by under eq_integral => x _ do rewrite normrN. Qed. Lemma Lnorm_cst1 r : ('N_r%:E[cst 1%R] = (mu setT)`^(r^-1)). Proof. -rewrite unlock /Lnorm. -under eq_integral => x _ do rewrite normr1 powR1 (_ : 1 = cst 1 x)%R// -indicT. -by rewrite integral_indic// setTI. +rewrite unlock /Lnorm; under eq_integral do rewrite /= normr1 powR1. +by rewrite integral_cst// mul1e. Qed. End Lnorm_properties. @@ -145,7 +142,7 @@ Section lnorm. (* l-norm is just L-norm applied to counting *) Context d {T : measurableType d} {R : realType}. Local Open Scope ereal_scope. -Local Notation "'N_ p [ f ]" := (Lnorm counting p f). +Local Notation "'N_ p [ f ]" := (Lnorm counting p (EFin \o f)). Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R -> 'N_p%:E [f] = (\sum_(k measurable_fun setT (fun x => f x `^ p)%R. Proof. exact: (@measurableT_comp _ _ _ _ _ _ (@powR R ^~ p)). Qed. -Local Notation "'N_ p [ f ]" := (Lnorm mu p f). +Local Notation "'N_ p [ f ]" := (Lnorm mu p (EFin \o f)). Let integrable_powR f p : (0 < p)%R -> measurable_fun [set: T] f -> 'N_p%:E[f] != +oo -> @@ -397,7 +394,7 @@ 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. -Local Notation "'N_ p [ f ]" := (Lnorm mu p f). +Local Notation "'N_ p [ f ]" := (Lnorm mu p (EFin \o f)). Local Open Scope ereal_scope. Let minkowski1 f g p : measurable_fun setT f -> measurable_fun setT g -> @@ -560,32 +557,14 @@ apply: minkowski => //. apply: measurableT_comp => //. Qed. -Lemma le_ess_sup (f g : T -> R) : - measurable_fun setT f -> measurable_fun setT g -> - (forall x, f x <= g x)%R -> ess_sup mu f <= ess_sup mu g. -Proof. -rewrite /ess_sup => mf mg h. -apply: le_ereal_inf => x [r]/= mu0 rx. -exists r => //. -move: mu0. -apply: subset_measure0. -- by rewrite -[X in _ X]setTI; exact: mf. -- by rewrite -[X in _ X]setTI; exact: mg. -move=> t/=. -rewrite !in_itv !andbT/= => fgtt. -by rewrite (lt_le_trans fgtt)//. -Qed. - Lemma minkowskie (f g : T -> R) (p : \bar R) : measurable_fun setT f -> measurable_fun setT g -> 1 <= p -> 'N_p[(f \+ g)%R] <= 'N_p[f] + 'N_p[g]. Proof. case: p => //[r|]; first exact: minkowski. -move=> mf mg _. -rewrite unlock /Lnorm. +move=> mf mg _; rewrite unlock /Lnorm. case: ifPn => mugt0; last by rewrite adde0 lexx. -apply: ess_supD => //. -all: by rewrite gt_eqF// (lt_le_trans ltNy0)// ess_sup_ger// => x/=; rewrite lee_fin normr_ge0. +exact: ess_sup_normD. Qed. End minkowski. diff --git a/theories/lspace.v b/theories/lspace.v index a7bdd757a1..36bfcd4282 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -5,7 +5,7 @@ From mathcomp Require Import ssralg ssrnum ssrint interval finmap. From mathcomp Require Import boolp classical_sets interval_inference reals. From mathcomp Require Import functions cardinality topology normedtype ereal. From mathcomp Require Import sequences esum exp measure numfun lebesgue_measure. -From mathcomp Require Import lebesgue_integral hoelder. +From mathcomp Require Import lebesgue_integral hoelder ess_sup_inf. (******************************************************************************) (* *) @@ -30,7 +30,7 @@ Local Open Scope ring_scope. Definition finite_norm d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (p : \bar R) (f : T -> R) := - ('N[ mu ]_p [ f ] < +oo)%E. + ('N[ mu ]_p [ EFin \o f ] < +oo)%E. HB.mixin Record isLfun d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E) (f : T -> R) @@ -113,7 +113,7 @@ apply/integrableP; split; first exact/measurable_EFinP. have := lfuny _ f. rewrite /finite_norm unlock /Lnorm invr1 poweRe1; last first. by apply integral_ge0 => x _; rewrite lee_fin powRr1. -by under eq_integral => i _ do rewrite powRr1//. +by under eq_integral => i _ do rewrite poweRe1//. Qed. Let le12 : (1 <= 2%:E :> \bar R)%E. @@ -255,7 +255,7 @@ HB.instance Definition _ := GRing.isScaleClosed.Build _ _ (@mfun _ _ T R) HB.instance Definition _ := [SubZmodule_isSubLmodule of {mfun T >-> R} by <:]. Lemma LnormZ (f : LfunType mu p1) a : - ('N[mu]_p[a \*: f] = `|a|%:E * 'N[mu]_p[f])%E. + ('N[mu]_p[EFin \o (a \*: f)] = `|a|%:E * 'N[mu]_p[EFin \o f])%E. Proof. rewrite unlock /Lnorm. case: p p1 f => //[r r1 f|]. @@ -267,16 +267,15 @@ case: p p1 f => //[r r1 f|]. exact: measurableT_comp. apply: (@lty_poweRy _ _ r^-1). by rewrite gt_eqF// invr_gt0 ?(lt_le_trans ltr01). - have -> : ((\int[mu]_x `|(`|f x| `^ r)%:E|) `^ r^-1 = 'N[mu]_r%:E[f])%E. + have -> : ((\int[mu]_x `|(`|f x| `^ r)%:E|) `^ r^-1 = 'N[mu]_r%:E[EFin \o f])%E. rewrite unlock /Lnorm. by under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. exact: (lfuny r1 f). rewrite poweRM ?integral_ge0=> //[||x _]; rewrite ?lee_fin ?powR_ge0//. by rewrite poweR_EFin -powRrM mulfV ?gt_eqF ?(lt_le_trans ltr01)// powRr1. - move=> p0 f; case: ifP => mu0; last by rewrite mule0. - rewrite (_ : normr \o a \*: f = `|a| \*: (normr \o f)); last first. - by apply: funext => x/=; rewrite normrZ. - by rewrite ess_supMl. + rewrite -ess_supZl//; apply/eq_ess_sup/nearW => x /=. + by rewrite normrZ EFinM. Qed. Lemma lfun_submod_closed : submod_closed (lfun). @@ -312,9 +311,9 @@ Variable (p : \bar R) (p1 : (1 <= p)%E). (* 0 - + should come with proofs that they are in LfunType mu p *) Notation ty := (LfunType mu p1). -Definition nm f := fine ('N[mu]_p[f]). +Definition nm f := fine ('N[mu]_p[EFin \o f]). -Lemma finite_norm_fine (f : ty) : (nm f)%:E = 'N[mu]_p[f]. +Lemma finite_norm_fine (f : ty) : (nm f)%:E = 'N[mu]_p[EFin \o f]. Proof. rewrite /nm fineK// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=. exact: lfuny. @@ -387,12 +386,7 @@ rewrite le_eqVlt => /predU1P[mu0 p1 q1 _ _ f _|mu_pos]. rewrite /finite_norm unlock /Lnorm. move: p p1; case=> //; last by rewrite -mu0 ltxx ltry. move=> r r1. - under eq_integral. - move=> x _. - have -> : (`|f x| `^ r)%:E = `| (`|f x| `^ r) |%:E. - by rewrite ger0_norm// powR_ge0. - over. - rewrite /=. + under eq_integral do rewrite /= -[(_ `^ _)%R]ger0_norm ?powR_ge0//=. rewrite (@integral_abs_eq0 _ _ _ _ setT setT (fun x => (`|f x| `^ r)%:E))//. by rewrite poweR0r// invr_neq0// gt_eqF// -lte_fin (lt_le_trans _ r1). apply/measurable_EFinP. @@ -403,9 +397,7 @@ case=> //[p|]; case=> //[q|] p1 q1; last first. have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). move=> muoo _ f. rewrite /finite_norm unlock /Lnorm mu_pos => supf_lty. - rewrite poweR_lty//. - have : measurable_fun setT (normr \o f) by exact/measurableT_comp. - move/ess_sup_bounded => /(_ _ supf_lty)[M fM]. + rewrite poweR_lty//; move: supf_lty => /ess_supr_bounded[M fM]. rewrite (@le_lt_trans _ _ (\int[mu]_x (M `^ p)%:E)); [by []| |]; last first. by rewrite integral_cst// lte_mul_pinfty// lee_fin powR_ge0. apply: ae_ge0_le_integral => //. @@ -420,6 +412,7 @@ case=> //[p|]; case=> //[q|] p1 q1; last first. move=> mu_fin pleq f ffin. have:= ffin; rewrite /finite_norm. have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). +have pN0 : p != 0%R by rewrite gt_eqF. have q0 : (0 < q)%R by rewrite ?(lt_le_trans ltr01). have qinv0 : q^-1 != 0%R by rewrite invr_neq0// gt_eqF. pose r := q/p. @@ -439,10 +432,9 @@ have r'0 : (0 < r')%R. have rr'1 : r^-1 + r'^-1 = 1%R. by rewrite /r' /r invf_div invrK addrCA subrr addr0. move=> /(_ mfp m1 r0 r'0 rr'1). -under [X in X `^ 1 <= _] eq_integral => x _ do - rewrite powRr1// norm_powR// normrE. -under [X in X`^ r^-1 * mu _ `^_]eq_integral => x _ do - rewrite /r norm_powR normrE ?powR_ge0// -powRrM mulrCA mulfV ?mulr1// ?gt_eqF//. +under [in leLHS] eq_integral do rewrite /= powRr1// norm_powR// normrE. +under [in leRHS] eq_integral do + rewrite /= norm_powR// normr_id -powRrM mulrCA divff// mulr1. rewrite [X in X <= _]poweRe1; last by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. move=> h1 /lty_poweRy h2. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 708cc77c8f..e088d6a5b9 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1564,6 +1564,50 @@ Notation emeasurable_fun_funeneg := measurable_funeneg (only parsing). #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_esup`")] Notation measurable_fun_lim_esup := measurable_fun_limn_esup (only parsing). +Section ereal_inf_sup_seq. +Context {R : realType}. +Implicit Types (S : set (\bar R)). +Local Open Scope ereal_scope. + +Lemma ereal_inf_seq S : S != set0 -> + {u : nat -> \bar R | forall i, S (u i) & u @ \oo --> ereal_inf S}. +Proof. +move=> SN0; apply/cid2; have [|Ninfy] := eqVneq (ereal_inf S) +oo. + move=> /[dup]/ereal_inf_pinfty/subset_set1/orW[/eqP/negPn/[!SN0]//|->] ->. + by exists (fun=> +oo) => //; apply: cvg_cst. +suff: exists2 v : (\bar R)^nat, v @ \oo --> ereal_inf S & + forall n, exists2 x : \bar R, x \in S & x < v n. + move=> [v vcvg] /(_ _)/sig2W-/all_sig/= [u /all_and2[/(_ _)/set_mem Su u_lt]]. + exists u => //; move: vcvg. + have: cst (ereal_inf S) @ \oo --> ereal_inf S by exact: cvg_cst. + apply: squeeze_cvge; apply: nearW => n; rewrite /cst/=. + by rewrite ereal_inf_le /= 1?ltW; last by exists (u n). +have [infNy|NinfNy] := eqVneq (ereal_inf S) -oo. + exists [sequence - (n%:R%:E)]_n => /=; last first. + by move=> n; setoid_rewrite set_mem_set; apply: lb_ereal_infNy_adherent. + rewrite infNy; apply/cvgNey; under eq_cvg do rewrite EFinN oppeK. + by apply/cvgeryP/cvgr_idn. +have inf_fin : ereal_inf S \is a fin_num by case: ereal_inf Ninfy NinfNy. +exists [sequence ereal_inf S + n.+1%:R^-1%:E]_n => /=; last first. + by move=> n; setoid_rewrite set_mem_set; apply: lb_ereal_inf_adherent. + apply/sube_cvg0 => //=; apply/cvg_abse0P. + rewrite (@eq_cvg _ _ _ _ (fun n => n.+1%:R^-1%:E)). + exact: cvge_harmonic. +by move=> n /=; rewrite /= addrAC subee// add0e gee0_abs//. +Unshelve. all: by end_near. Qed. + +Lemma ereal_sup_seq S : S != set0 -> + {u : nat -> \bar R | forall i, S (u i) & u @ \oo --> ereal_sup S}. +Proof. +move=> SN0; have NSN0 : [set - x | x in S] != set0. + by have /set0P[x Sx] := SN0; apply/set0P; exists (- x), x. +have [u /= Nxu] := ereal_inf_seq NSN0. +rewrite ereal_infN => /cvgeN; rewrite oppeK => Nu_to_sup. +by exists (fun n => - u n) => // i; have [? ? <-] := Nxu i; rewrite oppeK. +Qed. + +End ereal_inf_sup_seq. + Section open_itv_cover. Context {R : realType}. Implicit Types (A : set R). @@ -1575,7 +1619,7 @@ Lemma outer_measure_open_itv_cover A : (l^* A)%mu = ereal_inf [set \sum_(k _ /= [F [Fitv AF <-]]. + apply: le_ereal_inf => _ /= [F [Fitv AF <-]]. exists (fun i => `](sval (cid (Fitv i))).1, (sval (cid (Fitv i))).2]%classic). + split=> [i|]. * have [?|?] := ltP (sval (cid (Fitv i))).1 (sval (cid (Fitv i))).2. @@ -1587,290 +1631,109 @@ apply/eqP; rewrite eq_le; apply/andP; split. + apply: eq_eseriesr => k _; rewrite /l wlength_itv/=. case: (Fitv k) => /= -[a b]/= Fkab. by case: cid => /= -[x1 x2] ->; rewrite wlength_itv. -- have [/lb_ereal_inf_adherent lA|] := - boolP ((l^* A)%mu \is a fin_num); last first. - rewrite ge0_fin_numE ?outer_measure_ge0// -leNgt leye_eq => /eqP ->. - exact: leey. - apply/lee_addgt0Pr => /= e e0. - have : (0 < e / 2)%R by rewrite divr_gt0. - move=> /lA[_ [/= F [mF AF]] <-]; rewrite -/((l^* A)%mu) => lFe. - have Fcover n : exists2 B, F n `<=` B & - is_open_itv B /\ l B <= l (F n) + (e / 2 ^+ n.+2)%:E. - have [[a b] _ /= abFn] := mF n. - exists `]a, b + e / 2^+n.+2[%classic. - rewrite -abFn => x/= /[!in_itv] /andP[->/=] /le_lt_trans; apply. - by rewrite ltrDl divr_gt0. - split; first by exists (a, b + e / 2^+n.+2). - have [ab|ba] := ltP a b. - rewrite /l -abFn !wlength_itv//= !lte_fin ifT. - by rewrite ab -!EFinD lee_fin addrAC. - by rewrite ltr_wpDr// divr_ge0// ltW. - rewrite -abFn [in leRHS]set_itv_ge ?bnd_simp -?leNgt// /l wlength0 add0r. - rewrite wlength_itv//=; case: ifPn => [abe|_]; last first. - by rewrite lee_fin divr_ge0// ltW. - by rewrite -EFinD addrAC lee_fin -[leRHS]add0r lerD2r subr_le0. - pose G := fun n => sval (cid2 (Fcover n)). - have FG n : F n `<=` G n by rewrite /G; case: cid2. - have Gitv n : is_open_itv (G n) by rewrite /G; case: cid2 => ? ? []. - have lGFe n : l (G n) <= l (F n) + (e / 2 ^+ n.+2)%:E. - by rewrite /G; case: cid2 => ? ? []. - have AG : A `<=` \bigcup_k G k. - by apply: (subset_trans AF) => [/= r [n _ /FG Gnr]]; exists n. - apply: (@le_trans _ _ (\sum_(0 <= k /=; exists G. - exact: lee_nneseries. - rewrite nneseriesD//; last first. - by move=> i _; rewrite lee_fin// divr_ge0// ltW. - rewrite [in leRHS](splitr e) EFinD addeA leeD//; first exact/ltW. - have := @cvg_geometric_eseries_half R e 1; rewrite expr1. - rewrite [X in eseries X](_ : _ = (fun k => (e / (2 ^+ (k.+2))%:R)%:E)); last first. - by apply/funext => n; rewrite addn2 natrX. - move/cvg_lim => <-//; apply: lee_nneseries => //. - - by move=> n _; rewrite lee_fin divr_ge0// ltW. - - by move=> n _; rewrite lee_fin -natrX. +have [/lb_ereal_inf_adherent lA|] := + boolP ((l^* A)%mu \is a fin_num); last first. + rewrite ge0_fin_numE ?outer_measure_ge0// -leNgt leye_eq => /eqP ->. + exact: leey. +apply/lee_addgt0Pr => /= e e0. +have : (0 < e / 2)%R by rewrite divr_gt0. +move=> /lA[_ [/= F [mF AF]] <-]; rewrite -/((l^* A)%mu) => lFe. +have Fcover n : exists2 B, F n `<=` B & + is_open_itv B /\ l B <= l (F n) + (e / 2 ^+ n.+2)%:E. + have [[a b] _ /= abFn] := mF n. + exists `]a, b + e / 2^+n.+2[%classic. + rewrite -abFn => x/= /[!in_itv] /andP[->/=] /le_lt_trans; apply. + by rewrite ltrDl divr_gt0. + split; first by exists (a, b + e / 2^+n.+2). + have [ab|ba] := ltP a b. + rewrite /l -abFn !wlength_itv//= !lte_fin ifT. + by rewrite ab -!EFinD lee_fin addrAC. + by rewrite ltr_wpDr// divr_ge0// ltW. + rewrite -abFn [in leRHS]set_itv_ge ?bnd_simp -?leNgt// /l wlength0 add0r. + rewrite wlength_itv//=; case: ifPn => [abe|_]; last first. + by rewrite lee_fin divr_ge0// ltW. + by rewrite -EFinD addrAC lee_fin -[leRHS]add0r lerD2r subr_le0. +pose G := fun n => sval (cid2 (Fcover n)). +have FG n : F n `<=` G n by rewrite /G; case: cid2. +have Gitv n : is_open_itv (G n) by rewrite /G; case: cid2 => ? ? []. +have lGFe n : l (G n) <= l (F n) + (e / 2 ^+ n.+2)%:E. + by rewrite /G; case: cid2 => ? ? []. +have AG : A `<=` \bigcup_k G k. + by apply: (subset_trans AF) => [/= r [n _ /FG Gnr]]; exists n. +apply: (@le_trans _ _ (\sum_(0 <= k /=; exists G. + exact: lee_nneseries. +rewrite nneseriesD//; last first. + by move=> i _; rewrite lee_fin// divr_ge0// ltW. +rewrite [in leRHS](splitr e) EFinD addeA leeD//; first exact/ltW. +have := @cvg_geometric_eseries_half R e 1; rewrite expr1. +rewrite [X in eseries X](_ : _ = (fun k => (e / (2 ^+ (k.+2))%:R)%:E)); last first. + by apply/funext => n; rewrite addn2 natrX. +move/cvg_lim => <-//; apply: lee_nneseries => //. +- by move=> n _; rewrite lee_fin divr_ge0// ltW. +- by move=> n _; rewrite lee_fin -natrX. Qed. End open_itv_cover. + Section ereal_supZ. Context {R : realType}. -Implicit Types (r s : R) (A : set R). +Implicit Types (r s : R) (A : set R) (X : set (\bar R)). Local Open Scope ereal_scope. -Lemma ereal_supZl A r : (0 < r)%R -> - ereal_sup [set r%:E * x%:E | x in A] = r%:E * ereal_sup (EFin @` A). +Lemma set_cst I T (x : T) (A : set I) : + [set x | _ in A] = if A == set0 then set0 else [set x]. Proof. -move=> r0. -apply/eqP; rewrite eq_le; apply/andP; split. - (*TODO: should be ereal_sup_le and the current ereal_sup_le should be named something else*) - apply: ub_ereal_sup => /= _ [s As <-]. - rewrite -lee_pdivlMl// muleA -EFinM mulVf ?gt_eqF// mul1e. - by apply: ereal_sup_le; exists s%:E => //=; exists s. -rewrite -lee_pdivlMl//. -apply: ub_ereal_sup => /= _ [s As <-]. -rewrite lee_pdivlMl//. -apply: ereal_sup_le; exists (r * s)%:E => //=. -by exists s => //; rewrite EFinM. -Qed. - -Let ereal_infZl' A r : (0 < r)%R -> - ereal_sup [set - x | x in [set r%:E * x%:E | x in A]] = - r%:E * ereal_sup [set - x | x in [set x%:E | x in A]]. -Proof. -move=> r0. -apply/eqP; rewrite eq_le; apply/andP; split. - apply: ub_ereal_sup => /= _ [_ [s As <-]] <-. - rewrite -muleN -lee_pdivlMl// muleA -EFinM mulVf ?gt_eqF// mul1e. - apply: ereal_sup_le; exists (- s%:E) => //=. - exists s%:E. - by exists s. - by rewrite EFinN. -rewrite -lee_pdivlMl//. -apply: ub_ereal_sup => /= _ [_ [s As <-]] <-. -rewrite lee_pdivlMl//. -apply: ereal_sup_le; exists (- (r * s)%:E) => //=. - exists (r * s)%:E. - by exists s => //; rewrite EFinM. - by rewrite EFinN. -by rewrite EFinN muleN -EFinM EFinN. +apply/seteqP; split=> y /=. + by case=> i Ai ->; case: ifP => //= /eqP A0; rewrite A0 in Ai. +by case: ifPn => //= /set0P[i Ai ->]; exists i. Qed. -Lemma ereal_infZl A r : (0 < r)%R -> - ereal_inf [set r%:E * x%:E | x in A] = r%:E * ereal_inf (EFin @` A). +Lemma ereal_sup_cst T x (A : set T) : A != set0 -> + ereal_sup [set x | _ in A] = x :> \bar R. +Proof. by move=> AN0; rewrite set_cst ifN// ereal_sup1. Qed. + +Lemma ereal_inf_cst T x (A : set T) : A != set0 -> + ereal_inf [set x | _ in A] = x :> \bar R. +Proof. by move=> AN0; rewrite set_cst ifN// ereal_inf1. Qed. + +Lemma ereal_sup_pZl X r : (0 < r)%R -> + ereal_sup [set r%:E * x | x in X] = r%:E * ereal_sup X. Proof. -move=> r0; rewrite /ereal_inf muleN; congr -%E. -exact: ereal_infZl'. +move=> /[dup] r_gt0; rewrite lt0r => /andP[r_neq0 r_ge0]. + gen have gen : r r_gt0 {r_ge0 r_neq0} X / + ereal_sup [set r%:E * x | x in X] <= r%:E * ereal_sup X. + apply/ereal_supP => y/= [x Ax <-]; rewrite lee_pmul2l//=. + by apply/ereal_supP => //=; exists x. +apply/eqP; rewrite eq_le gen//= -lee_pdivlMl//. +rewrite (le_trans _ (gen _ _ _)) ?invr_gt0 ?image_comp//=. +by under eq_imagel do rewrite /= muleA -EFinM mulVf ?mul1e//=; rewrite image_id. Qed. -End ereal_supZ. - -Section essential_supremum. -Context d {T : measurableType d} {R : realType}. -Variable mu : {measure set T -> \bar R}. -Implicit Types f g : T -> R. -Local Open Scope ereal_scope. +Lemma ereal_supZl X r : X != set0 -> (0 <= r)%R -> + ereal_sup [set r%:E * x | x in X] = r%:E * ereal_sup X. +Proof. +move=> AN0; have [r_gt0|//|<-] := ltgtP => _; first by rewrite ereal_sup_pZl. +by rewrite mul0e; under eq_imagel do rewrite mul0e/=; rewrite ereal_sup_cst. +Qed. + +Lemma ereal_inf_pZl X r : (0 < r)%R -> + ereal_inf [set r%:E * x | x in X] = r%:E * ereal_inf X. +Proof. +move=> r_gt0; rewrite !ereal_infEN muleN image_comp/=; congr (- _). +by under eq_imagel do rewrite /= -muleN; rewrite -image_comp ereal_sup_pZl. +Qed. -Lemma ess_sup_bounded f : measurable_fun setT f -> ess_sup mu f < +oo -> - exists M, \forall x \ae mu, (f x <= M)%R. -Proof. -move=> mf /ereal_inf_lt[_ /= [r fr0] <-] _. -exists r, (f @^-1` `]r, +oo[); split => //. - rewrite (_ : _ @^-1` _ = [set t | r%:E < (f t)%:E]); last first. - by apply/seteqP; split => [x|x]/=; rewrite in_itv/= andbT. - rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. - by apply/measurable_EFinP; exact/measurableT_comp. -by move=> t/= ftr; rewrite in_itv/= andbT ltNge; exact/negP. -Qed. - -Lemma ess_sup_max f : measurable_fun setT f -> - ess_sup mu (normr \o f) != -oo -> - mu [set r | ess_sup mu (normr \o f) < `|f r|%:E] = 0. -Proof. -move=> mf fNy. -move hm : (ess_sup mu (normr \o f)) => m. -case: m hm => [m| |] hm. -- pose x_ n := m%:E + n.+1%:R^-1%:E. - have -> : [set r | m%:E < `|f r|%:E] = \bigcup_n [set r | x_ n < `|f r|%:E]. - apply/seteqP; split => [r /= mfr|r/=]. - near \oo => n. - suff : x_ n < `|f r|%:E by move=> ?; exists n. - rewrite /x_ -EFinD lte_fin -ltrBrDl. - rewrite invf_plt ?posrE//; last by rewrite subr_gt0 -lte_fin. - by rewrite -natr1 -ltrBlDr; near: n; exact: nbhs_infty_gtr. - by move=> [n _/=]; apply: le_lt_trans;rewrite /x_ -EFinD lee_fin lerDl. - have H n : mu [set r | x_ n < `|f r|%:E] = 0%R. - have : ess_sup mu (normr \o f) \is a fin_num by rewrite hm. - move/lb_ereal_inf_adherent => /(_ n.+1%:R^-1). - rewrite invr_gt0// ltr0n => /(_ erefl)[_ /= [r/= mufr0] <-]. - rewrite -/(ess_sup mu _) hm /x_ => rmn. - apply/eqP; rewrite eq_le measure_ge0 andbT. - rewrite -mufr0 le_measure// ?inE//. - + rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. - by apply/measurable_EFinP; exact/measurableT_comp. - + rewrite (_ : _ @^-1` _ = [set t | r%:E < `|f t|%:E]); last first. - by apply/seteqP; split => [x|x]/=; rewrite in_itv/= andbT. - rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. - by apply/measurable_EFinP; exact/measurableT_comp. - + move=> x/=; rewrite in_itv/= andbT. - rewrite -EFinD lte_fin; apply/le_lt_trans. - by move: rmn; rewrite -EFinD lte_fin => /ltW. - apply/eqP; rewrite eq_le measure_ge0 andbT. - have <- : \sum_(0 <= i [i|]. - + rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. - by apply/measurable_EFinP; exact/measurableT_comp. - + apply: bigcup_measurable => i _. - rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. - by apply/measurable_EFinP; exact/measurableT_comp. -- rewrite (_ : [set r | +oo < `|f r|%:E] = set0)// -subset0 => x/=. - by rewrite ltNge leey. -- by rewrite hm in fNy. -Unshelve. all: by end_near. Qed. +Lemma ereal_infZl X r : X != set0 -> (0 < r)%R -> + ereal_sup [set r%:E * x | x in X] = r%:E * ereal_sup X. +Proof. +move=> XN0 r_gt0; rewrite !ereal_supEN muleN image_comp/=; congr (- _). +by under eq_imagel do rewrite /= -muleN; rewrite -image_comp ereal_inf_pZl. +Qed. -Lemma ess_sup_eq0 f : measurable_fun setT f -> - f = 0%R %[ae mu] <-> mu [set r | (0%R < `|f r|)%R] = 0. -Proof. -move=> mf; split=> [|f0]. -- case => N [mN N0 fN]. - apply/eqP; rewrite eq_le measure_ge0 andbT -N0. - rewrite le_measure ?inE//. - rewrite [X in measurable X](_ : _ = [set t | 0 < `|f t|%:E]); last first. - by apply/seteqP; split => [x|x]/=; rewrite lte_fin. - rewrite -[X in measurable X]setTI. - apply: emeasurable_fun_o_infty => //. - by apply/measurable_EFinP; exact/measurableT_comp. - apply: subset_trans fN => t/= ft0. - apply/not_implyP; split => //. - apply/eqP. - by rewrite -normr_eq0 gt_eqF. -- exists [set r | (0 < `|f r|)%R]; split => //. - rewrite [X in measurable X](_ : _ = [set t | 0 < `|f t|%:E]); last first. - by apply/seteqP; split => [x|x]/=; rewrite lte_fin. - rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. - by apply/measurable_EFinP; exact/measurableT_comp. - move=> t/= /not_implyP[_ /eqP]; rewrite -normr_eq0 => ft0. - by rewrite lt_neqAle eq_sym ft0/=. -Qed. - -Lemma ess_sup_eq0_ae f : measurable_fun setT f -> - ess_sup mu (normr \o f) = 0 -> f = 0%R %[ae mu]. -Proof. -move=> mf f0; apply/ess_sup_eq0 => //. -rewrite [X in mu X](_ : _ = [set r | (0 < `|f r|%:E)%E]); last first. - by apply/seteqP; split => [x|x]/=; rewrite lte_fin. -by rewrite -f0 ess_sup_max// f0. -Qed. - -Lemma ess_supMl f (r : R) : mu setT > 0 -> (0 <= r)%R -> - ess_sup mu (cst r \* f)%R = r%:E * ess_sup mu f. -Proof. -move=> muT0; rewrite le_eqVlt => /predU1P[<-|r0]. - rewrite mul0e (_ : _ \* f = cst 0)%R; first by rewrite ess_sup_cst. - by apply/funext => ?; rewrite /= mul0r. -rewrite -ereal_infZl//. -have rf s : (cst r \* f)%R @^-1` `]s, +oo[ = f%R @^-1` `]s / r, +oo[. - by apply/seteqP; split => [y|y]/=; rewrite !in_itv/= !andbT; - rewrite ltr_pdivrMr// mulrC. -congr ereal_inf; apply/seteqP; split => [_ [s /= M <-]|_ [s /= M <-]]/=. -- exists (s / r)%R; first by rewrite -rf. - by rewrite EFinM muleCA -EFinM divff ?mulr1// gt_eqF. -- exists (r * s)%R; last by rewrite EFinM. - by rewrite rf mulrAC divff ?mul1r// gt_eqF. -Qed. - -Lemma ess_sup_ub f : measurable_fun setT f -> ess_sup mu (normr \o f) != -oo -> - {ae mu, forall x, `|f x|%:E <= ess_sup mu (normr \o f)}. -Proof. -move=> mf fNy. -have [->|] := eqVneq (ess_sup mu (normr \o f)) +oo. - by apply/nearW => ?; rewrite leey. -rewrite -ltey => fy. -exists [set r | ess_sup mu (normr \o f) < `|f r|%:E]. -split. -- rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //. - by apply/measurable_EFinP; exact/measurableT_comp. -- exact: ess_sup_max. -- by move=> t/= /negP; rewrite -ltNge. -Qed. - -Lemma ess_supD f g : - measurable_fun setT f -> measurable_fun setT g -> - ess_sup mu (normr \o f) != -oo -> ess_sup mu (normr \o g) != -oo -> - ess_sup mu (normr \o (f \+ g)) <= - ess_sup mu (normr \o f) + ess_sup mu (normr \o g). -Proof. -move=> mf mg fNy gNy. -have [->|] := eqVneq (ess_sup mu (normr \o f)) +oo. - by rewrite addye// leey. -rewrite -ltey => fy. -have [->|] := eqVneq (ess_sup mu (normr \o g)) +oo. - by rewrite addey// leey. -rewrite -ltey => gy. -pose a := ess_sup mu (normr \o f); pose b := ess_sup mu (normr \o g). -have a_fin_num : a \is a fin_num by rewrite fin_real// fy andbT ltNye. -have b_fin_num : b \is a fin_num by rewrite fin_real// gy andbT ltNye. -have fa : {ae mu, forall x, `|f x|%:E <= a}. - exact: ess_sup_ub. -have gb : {ae mu, forall x, `|g x|%:E <= b}. - exact: ess_sup_ub. -have {fa gb}fg : - {ae mu, forall x, (((normr \o f) \+ (normr \o g)) x)%:E <= a + b}. - case: fa => A [mA A0 Af]. - case: gb => B [mB B0 Bg]. - exists (A `|` B); split; first exact: measurableU. - by rewrite measureU0. - move=> t/= /negP; rewrite -ltNge => abfg. - have [At|At] := pselect (A t); [by left|right]. - apply: Bg => //=. - apply: contra_not At => gb. - apply: Af => /= fa. - have : (`|f t|%R + `|g t|%R)%E%:E <= a + b. - by rewrite EFinD leeD. - by rewrite leNgt abfg. -apply: ereal_inf_lbound => /=. -exists (fine a + fine b). - case: fg => N [mN N0 fgN]. - apply/eqP; rewrite eq_le measure_ge0 andbT -N0. - rewrite le_measure ?inE//. - rewrite -[X in measurable X]setTI. - have : measurable_fun setT (normr \o (f \+ g)). - apply: measurableT_comp => //. - exact: measurable_funD. - exact. - apply: subset_trans fgN => t/=. - rewrite in_itv/= andbT => abfg. - apply/negP; rewrite -ltNge. - rewrite -lte_fin in abfg. - (* TODO: we don't have lee_absD? *) - rewrite (@lt_le_trans _ _ `|(f t + g t)|%:E)%R//. - by move: abfg; rewrite EFinD !fineK. - exact: ler_normD. -by rewrite EFinD !fineK. -Qed. - -End essential_supremum. +End ereal_supZ. Section egorov. Context d {R : realType} {T : measurableType d}. diff --git a/theories/measure.v b/theories/measure.v index 0776e1472f..0b078e6b2b 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -272,9 +272,6 @@ From HB Require Import structures. (* ## More measure-theoretic definitions *) (* ``` *) (* 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 *) -(* semiRingOfSetsType and R is a realType *) -(* ess_inf f == essential infimum *) (* ``` *) (* *) (******************************************************************************) @@ -1306,6 +1303,10 @@ move=> A B mA mB; case: (semi_measurableD A B) => // [D [Dfin Dl -> _]]. by apply: fin_bigcup_measurable. Qed. +Lemma seqDU_measurable (F : sequence (set T)) : + (forall n, measurable (F n)) -> forall n, measurable (seqDU F n). +Proof. by move=> Fmeas n; apply/measurableD/bigsetU_measurable. Qed. + End ringofsets_lemmas. Section algebraofsets_lemmas. @@ -1979,6 +1980,10 @@ have /[!big_ord0] ->// := @measure_semi_additive _ _ _ mu (fun=> set0) 0%N. exact: trivIset_set0. Qed. +Lemma measure_gt0 x : (0%R < mu x) = (mu x != 0). +Proof. by rewrite lt_def measure_ge0 andbT. Qed. + + Hint Resolve measure0 : core. Hint Resolve measure_ge0 : core. @@ -4224,6 +4229,19 @@ Proof. by apply: filterS => x /= /[apply] ->; rewrite mulr1. Qed. Lemma ae_eq_abse (f g : T -> \bar R) : ae_eq f g -> ae_eq (abse \o f) (abse \o g). Proof. by apply: filterS => x /[apply] /= ->. Qed. +Lemma ae_foralln (P : nat -> T -> Prop) : (forall n, \forall x \ae mu, P n x) -> \forall x \ae mu, forall n, P n x. +Proof. +move=> /(_ _)/cid - /all_sig[A /all_and3[Ameas muA0 NPA]]. +have seqDUAmeas := seqDU_measurable Ameas. +exists (\bigcup_n A n); split => //. +- exact/bigcup_measurable. +- rewrite seqDU_bigcup_eq measure_bigcup//. + rewrite eseries0// => i _ _. + rewrite (@subset_measure0 _ _ _ _ _ (A i))//=. + exact: subset_seqDU. +- by move=> x /=; rewrite -existsNP => -[n NPnx]; exists n => //; apply: NPA. +Qed. + End ae_eq. Section ae_eq_lemmas. @@ -5366,51 +5384,3 @@ Proof. by move=> mE m21 [A [mA A0 ?]]; exists A; split => //; exact: m21. Qed. End absolute_continuity_lemmas. -Section essential_supremum. -Context d {T : semiRingOfSetsType 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_ger f x : 0 < mu [set: T] -> (forall t, x <= (f t)%:E) -> - x <= ess_sup f. -Proof. -move=> muT f0; apply: lb_ereal_inf => _ /= [r /eqP fr0 <-]; rewrite leNgt. -apply/negP => rx; apply/negP : fr0; rewrite gt_eqF// (_ : _ @^-1` _ = setT)//. -apply/seteqP; split => // t _ /=; rewrite in_itv/= andbT. -by rewrite -lte_fin (lt_le_trans _ (f0 t)). -Qed. - -Lemma ess_sup_ler f r : (forall t, (f t)%:E <= r) -> ess_sup f <= r. -Proof. -case: r => [r| |] fr; last 2 first. - by rewrite leey. - by have := fr point; rewrite leNgt ltNye. -apply: ereal_inf_le; apply/exists2P. -exists r%:E => /=; split => //; apply/exists2P; exists r; split => //. -rewrite preimage_itvoy [X in mu X](_ : _ = set0)// -subset0 => x //=. -rewrite lt_neqAle => /andP[+ rlefx]. -by apply/negP/negPn; rewrite eq_le rlefx/= -lee_fin. -Qed. - -Lemma ess_sup_cst r : (0 < mu setT)%E -> (ess_sup (cst r) = r%:E)%E. -Proof. -move => mu0. -by apply/eqP; rewrite eq_le; apply/andP; split; - [exact: ess_sup_ler|exact: ess_sup_ger]. -Qed. - -Definition ess_inf f := - ereal_sup (EFin @` [set r | mu (f @^-1` `]-oo, r[) = 0]). - -Lemma ess_inf_ge0 f : 0 < mu [set: T] -> (forall t, 0 <= f t)%R -> - 0 <= ess_inf f. -Proof. -move=> muT f0; apply: ereal_sup_le; exists 0 => //=; exists 0%R => //=. -rewrite [X in mu X](_ : _ = set0)// -subset0 => x/=. -by rewrite in_itv/= ltNge => /negP; exact. -Qed. - -End essential_supremum. diff --git a/theories/normedtype.v b/theories/normedtype.v index 171b7196d8..21a2424677 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -202,7 +202,7 @@ Lemma limf_esup_ge0 f F : ~ F set0 -> Proof. move=> F0 f0; rewrite limf_esupE; apply: lb_ereal_inf => /= x [A]. have [-> /F0//|/set0P[y Ay FA] <-{x}] := eqVneq A set0. -by apply: ereal_sup_le; exists (f y). +by apply: ereal_sup_ge; exists (f y). Qed. End limf_esup_einf_realType. diff --git a/theories/sequences.v b/theories/sequences.v index a94ac54f8d..8912ec0763 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -282,6 +282,9 @@ apply/funext => n; rewrite -setIDA; apply/seteqP; split; last first. by rewrite /seqDU -setIDA bigcup_mkord -big_distrr/= setDIr setIUr setDIK set0U. Qed. +Lemma subset_seqDU (A : (set T)^nat) (i : nat) : seqDU A i `<=` A i. +Proof. by move=> ?; apply: subDsetl. Qed. + End seqDU. Arguments trivIset_seqDU {T} F. #[global] Hint Resolve trivIset_seqDU : core.