From 79da61a531b4ef92ec7f01fdc0c7df473404eb1e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 14 Apr 2023 17:44:54 +0900 Subject: [PATCH 01/33] 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 713f59627..5735b84f1 100644 --- a/_CoqProject +++ b/_CoqProject @@ -94,3 +94,4 @@ theories/pi_irrational.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 000000000..ca8778d70 --- /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 cb8b9f643059ff10d935fdce8723adfffea3a9df Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Mon, 27 May 2024 09:45:45 +0200 Subject: [PATCH 02/33] fixed compilation errors --- theories/lspace.v | 34 +++++++++++++++++++--------------- 1 file changed, 19 insertions(+), 15 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index ca8778d70..22fc30a78 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -47,8 +47,9 @@ 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. +HB.instance Definition _ := gen_eqMixin (LfunType mu p). +HB.instance Definition _ := gen_choiceMixin (LfunType mu p). + End Lfun_canonical. Section Lequiv. @@ -59,18 +60,17 @@ 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 := @@ -103,10 +103,10 @@ Arguments Lspace : clear implicits. Lemma LType1_integrable (f : LType mu 1) : mu.-integrable setT (EFin \o f). Proof. -split; first exact/EFin_measurable_fun. +apply/integrableP; split; first exact/EFin_measurable_fun. under eq_integral. move=> x _ /=. - rewrite -(@powere_pose1 _ `|f x|%:E)//. + rewrite -(@poweRe1 _ `|f x|%:E)//. over. exact: lfuny f. Qed. @@ -114,15 +114,19 @@ 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. +apply/integrableP; split. + +apply/EFin_measurable_fun. +exact: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f) => //. 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: measurableT_comp => //. + apply/EFin_measurable_fun. + exact: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f) => //. +- by move=> x _; rewrite lee_fin powR_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: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R) => //. + exact: measurableT_comp. +- by move=> t _/=; rewrite lee_fin normrX powR_mulrn. Qed. End Lspace. From 0616933bd7f2aba710b57b80705cf1270950c78f Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 30 May 2024 07:49:47 +0200 Subject: [PATCH 03/33] attempt to fix CI --- theories/lspace.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 22fc30a78..623ea6dad 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -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]). From 43888e3ce71aec34e4847c20f7a4d016f72b68e9 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 15 Aug 2024 20:03:59 +0200 Subject: [PATCH 04/33] fix --- theories/lspace.v | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 623ea6dad..aaed30615 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -115,17 +115,12 @@ Lemma LType2_integrable_sqr (f : LType mu 2) : mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)). Proof. apply/integrableP; split. - -apply/EFin_measurable_fun. -exact: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f) => //. + exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f)/measurable_lfun. rewrite (le_lt_trans _ (lfuny f))// ge0_le_integral//. - apply: measurableT_comp => //. - apply/EFin_measurable_fun. - exact: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f) => //. + exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f)/measurable_lfun. - by move=> x _; rewrite lee_fin powR_ge0. -- apply/EFin_measurable_fun. - apply: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x `^ 2)%R) => //. - exact: measurableT_comp. +- 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. From cfad0d0111b99c13940c3f3ee3d07cba621a25c0 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 15 Aug 2024 20:58:49 +0200 Subject: [PATCH 05/33] extended reals --- theories/lspace.v | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index aaed30615..958c7da99 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,7 +45,7 @@ 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). @@ -54,7 +54,7 @@ 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} >]. @@ -104,19 +104,25 @@ Arguments Lspace : clear implicits. Lemma LType1_integrable (f : LType mu 1) : mu.-integrable setT (EFin \o f). Proof. apply/integrableP; split; first exact/EFin_measurable_fun. -under eq_integral. - move=> x _ /=. - rewrite -(@poweRe1 _ `|f x|%:E)//. - over. -exact: lfuny f. +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. apply/integrableP; split. exact/EFin_measurable_fun/(@measurableT_comp _ _ _ _ _ _ (fun x : R => x ^+ 2)%R _ f)/measurable_lfun. -rewrite (le_lt_trans _ (lfuny f))// ge0_le_integral//. +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. From e324bc38bedbf9e6acf498e563ca132a7e827a53 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 15 Aug 2024 21:04:34 +0200 Subject: [PATCH 06/33] wip --- theories/lspace.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/theories/lspace.v b/theories/lspace.v index 958c7da99..891d26915 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -132,3 +132,13 @@ Qed. End Lspace. Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope. + +Section Lspace_inclusion. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. +Variables (p q : \bar R). + +Lemma Lspace_inclusion : (p <= q)%E -> mu.-Lspace q `<=` mu.-Lspace p. + + +End Lspace_inclusion. From 184c68ee897ff955bbb64941b8d2e2e8f3683d32 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Fri, 16 Aug 2024 12:28:31 +0200 Subject: [PATCH 07/33] up --- theories/lspace.v | 65 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 63 insertions(+), 2 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 891d26915..26badf6b7 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -133,12 +133,73 @@ 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. +Admitted. + +Lemma Lnorm_eq0 f : nm f = 0 -> f = 0. +Admitted. + +Lemma Lnorm_natmul f k : nm (f *+ k) = nm f *+ k. +Admitted. + +Lemma LnormN f : nm (-f) = nm f. +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}. -Variables (p q : \bar R). -Lemma Lspace_inclusion : (p <= q)%E -> mu.-Lspace q `<=` mu.-Lspace p. +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 d91bea53bb31419a4a6feb5913ad37d1302bd9c8 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 22 Aug 2024 12:06:26 +0200 Subject: [PATCH 08/33] wip --- theories/lspace.v | 74 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 73 insertions(+), 1 deletion(-) diff --git a/theories/lspace.v b/theories/lspace.v index 26badf6b7..ddc44368a 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -155,15 +155,87 @@ Definition nm f := fine ('N[mu]_p%:E[f]). 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 Lnorm_eq0 f : nm f = 0 -> f = 0. +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. (* From addd307b64a0917e00d2d4b6903d8ffc45b6360e Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 27 Jan 2025 17:35:30 +0100 Subject: [PATCH 09/33] Setup nix to follow the seminorm branch of mathcomp --- .nix/config.nix | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index 25a13ce7a..e43c0ede7 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -50,12 +50,16 @@ 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"; + mathcomp.override.version = "CohenCyril:seminorm"; + mathcomp-bigenough.override.version = "master"; + mathcomp-finmap.override.version = "master"; ssprove.job = false; }; @@ -65,7 +69,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; From a181b67dc3c02a5576b534b61ea2c3b1fe9bc7b7 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 27 Jan 2025 17:54:58 +0100 Subject: [PATCH 10/33] WIP --- theories/lspace.v | 2 +- theories/normedtype.v | 32 +++++++++++++++++++++++++------- 2 files changed, 26 insertions(+), 8 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index ddc44368a..4a39a1720 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 5008548ff..d47be766a 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -252,17 +252,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)). @@ -807,21 +817,27 @@ Proof. by rewrite cvgeryP cvgrnyP. 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 @@ -859,7 +875,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 8fe12a6238e13c54f134d5f8ccd4dde7589fbd46 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Tue, 28 Jan 2025 09:38:10 +0100 Subject: [PATCH 11/33] normedtype.v compiles --- theories/normedtype.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index d47be766a..a7ab17e11 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -877,7 +877,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 : @@ -2462,7 +2462,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 a0a6c9ccb62536d4dae998f9fc0d4daa0163e0a7 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Tue, 28 Jan 2025 10:07:22 +0100 Subject: [PATCH 12/33] lspace.v headers --- theories/lspace.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 4a39a1720..84a77d390 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. (******************************************************************************) (* *) From bc4eec82d39cdbbcc1285f79c0014205a535f836 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Tue, 28 Jan 2025 13:24:55 +0100 Subject: [PATCH 13/33] norms --- theories/hoelder.v | 70 ++++++++++++++++++++++++++++++++++++++++++++++ theories/lspace.v | 4 +-- 2 files changed, 72 insertions(+), 2 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 5b5b020f8..5d1e30120 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 84a77d390..db1807b51 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -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 *) From 9c8b52c203494e528ffae578be12383d33c95914 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 28 Jan 2025 17:00:55 +0100 Subject: [PATCH 14/33] making ae work as a filter --- theories/measure.v | 38 ++++++++++++++++---------------------- 1 file changed, 16 insertions(+), 22 deletions(-) diff --git a/theories/measure.v b/theories/measure.v index 013b1a804..06ef7cafe 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4044,7 +4044,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. @@ -4063,16 +4064,15 @@ Proof. by rewrite /almost_everywhere => mA mB; rewrite setCI; exact: negligibleU. Qed. -#[global] -Instance ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType) +HB.about semiRingOfSetsType. +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. @@ -4085,17 +4085,17 @@ 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. +Notation "{ 'ae' m , P }" := {near almost_everywhere m, P} : type_scope. -Lemma aeW {d} {T : semiRingOfSetsType d} {R : realFieldType} +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}. Proof. @@ -4120,13 +4120,10 @@ 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^\-. 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. Lemma ae_eq_refl f : ae_eq f f. Proof. exact/aeW. Qed. @@ -4158,10 +4155,7 @@ Context d (T : sigmaRingType d) (R : realType). Implicit Types mu : {measure set T -> \bar R}. 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. From 23d86257504c1a37b7ba4d97326ad84eed2cbdb6 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 28 Jan 2025 17:33:02 +0100 Subject: [PATCH 15/33] Adding notations for ae --- theories/lebesgue_integral.v | 13 ++++++------- theories/lspace.v | 4 ++-- theories/measure.v | 20 +++++++++++++------- 3 files changed, 21 insertions(+), 16 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 8a966ebcb..6fb4d75d6 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3726,11 +3726,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]. @@ -3759,7 +3757,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; @@ -3813,7 +3812,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 => //. @@ -3922,7 +3921,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//. @@ -3940,7 +3939,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 -> integral mu D f = integral mu D g. + f = g %[ae mu in D] -> integral mu D f = integral mu D g. 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 db1807b51..f8c3ad690 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 06ef7cafe..a33e82888 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4064,7 +4064,6 @@ Proof. by rewrite /almost_everywhere => mA mB; rewrite setCI; exact: negligibleU. Qed. -HB.about semiRingOfSetsType. Definition ae_filter_ringOfSetsType d {T : ringOfSetsType d} (R : realFieldType) (mu : {measure set T -> \bar R}) : Filter (almost_everywhere mu). Proof. @@ -4094,10 +4093,18 @@ End ae. (apply: ae_properfilter_algebraOfSetsType) : typeclass_instances. 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]. @@ -4108,10 +4115,9 @@ Local Open Scope ereal_scope. Context d (T : sigmaRingType d) (R : realType). 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 : 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 : @@ -4152,7 +4158,7 @@ End ae_eq. Section ae_eq_lemmas. Context d (T : sigmaRingType d) (R : realType). -Implicit Types mu : {measure set T -> \bar R}. +Implicit Types (mu : {measure set T -> \bar R}) (A : set T) (f g : T -> R). Lemma ae_eq_subset mu A B f g : B `<=` A -> ae_eq mu A f g -> ae_eq mu B f g. Proof. by move=> BA; apply: filterS => x + /BA; apply. Qed. @@ -5285,7 +5291,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 -> R). 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 69ff8b918bbb7467b453112e9269de45ba37bb67 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 28 Jan 2025 17:40:52 +0100 Subject: [PATCH 16/33] generalizing ae_eq --- theories/charge.v | 3 +++ theories/measure.v | 19 ++++++++++--------- 2 files changed, 13 insertions(+), 9 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 64323cb44..676f3777d 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1867,6 +1867,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/measure.v b/theories/measure.v index a33e82888..f86406dff 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4100,7 +4100,7 @@ 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). + (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) : @@ -4112,25 +4112,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). -Lemma ae_eq0 f g : measurable D -> mu D = 0 -> f = g %[ae mu in D]. +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|[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. @@ -4157,8 +4158,8 @@ 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}) (A : set T) (f g : T -> 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. by move=> BA; apply: filterS => x + /BA; apply. Qed. @@ -5291,7 +5292,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}) (f g : T -> 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 f0845848ed19d9081d972999d3e2fef9c2dfd1a8 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Tue, 28 Jan 2025 18:11:08 +0100 Subject: [PATCH 17/33] more generalizations of ae_eq --- theories/measure.v | 31 +++++++++++++++---------------- 1 file changed, 15 insertions(+), 16 deletions(-) diff --git a/theories/measure.v b/theories/measure.v index f86406dff..325c3ca2a 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4111,8 +4111,8 @@ by apply/negligibleP; [rewrite setCT|rewrite setCT measure0]. 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) (U V : Type) (W : ringType). 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). @@ -4131,28 +4131,27 @@ 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_refl (f : T -> U) : ae_eq f f. Proof. exact/aeW. Qed. -Lemma ae_eq_sym f g : ae_eq f g -> ae_eq g f. +Lemma ae_eq_sym (f g : T -> U) : ae_eq f g -> ae_eq g f. Proof. by apply: filterS => x + Dx => /(_ Dx). Qed. -Lemma ae_eq_trans f g h : ae_eq f g -> ae_eq g h -> ae_eq f h. +Lemma ae_eq_trans (f g h : T -> U) : ae_eq f g -> ae_eq g h -> ae_eq f h. Proof. by apply: filterS2 => x + + Dx => /(_ Dx) ->; exact. 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 (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 (f g h : T -> W) : ae_eq f g -> ae_eq (f \* h) (g \* h). +Proof. by apply: filterS => x /= /[apply] ->. 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 (f g h : T -> W) : ae_eq f g -> ae_eq (h \* f)%R (h \* g). +Proof. by apply: filterS => x /= /[apply] ->. 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 (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. @@ -5291,7 +5290,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 4ca52c497548d3dc81c243c405684538312940be Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Wed, 29 Jan 2025 10:34:45 +0100 Subject: [PATCH 18/33] wip --- theories/charge.v | 9 +++++---- theories/hoelder.v | 21 +++++++++------------ theories/lspace.v | 39 ++++++++++++++------------------------- theories/measure.v | 4 ++-- 4 files changed, 30 insertions(+), 43 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 676f3777d..433f5b492 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1867,10 +1867,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. @@ -2096,6 +2093,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 5d1e30120..39b8a8f2d 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -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,13 +527,16 @@ 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. @@ -560,16 +563,10 @@ case: p => [p|_|]. 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. + by 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 f8c3ad690..4cc634f04 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) := `[< f = g [%ae mu] >]. +Definition Lequiv (f g : LfunType mu p) := `[< f = g %[ae mu] >]. Let Lequiv_refl : reflexive Lequiv. Proof. @@ -65,12 +65,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 := @@ -136,7 +136,7 @@ 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 *) +Variable (p : R) (p1 : 1 <= p). (* 0 - + should come with proofs that they are in LfunType mu p *) @@ -159,28 +159,17 @@ 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 !ltNye_eq => /orP[f_fin /orP[g_fin|/eqP foo]|/eqP goo /orP[f_fin|/eqP foo]]. - rewrite -fineD ?fine_le//. - - admit. + - apply: LnormD_fin_num => //. admit. 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. *) - + rewrite minkowski//. admit. admit. +- rewrite foo/= add0r (_ : 'N[mu]_p%:E[(f \+ g)] = +oo%E) ?fine_ge0 ?Lnorm_ge0//. + admit. +- rewrite goo/= addr0 (_ : 'N[mu]_p%:E[(f \+ g)] = +oo%E) ?fine_ge0 ?Lnorm_ge0//. + admit. +- rewrite foo goo/= add0r (_ : 'N[mu]_p%:E[(f \+ g)] = +oo%E)//=. + admit. Admitted. Lemma natmulfctE (U : pointedType) (K : ringType) (f : U -> K) n : @@ -188,7 +177,7 @@ Lemma natmulfctE (U : pointedType) (K : ringType) (f : U -> K) 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}. +Lemma Lnorm_eq0 f : nm f = 0 -> f = 0 %[ae mu]. (* we need to get rid of fine *) rewrite /nm => /eqP. rewrite fine_eq0; last first. admit. move/eqP/Lnorm_eq0_eq0. diff --git a/theories/measure.v b/theories/measure.v index 325c3ca2a..399757de2 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4112,7 +4112,7 @@ Qed. Section ae_eq. Local Open Scope ring_scope. -Context d (T : sigmaRingType d) (R : realType) (U V : Type) (W : ringType). +Context d (T : sigmaRingType d) (R : realType) (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). @@ -4145,7 +4145,7 @@ Proof. by apply: filterS2 => x + + Dx => /= /(_ Dx) -> /(_ Dx) ->. Qed. Lemma ae_eq_mul2r (f g h : T -> W) : ae_eq f g -> ae_eq (f \* h) (g \* h). Proof. by apply: filterS => x /= /[apply] ->. Qed. -Lemma ae_eq_mul2l (f g h : T -> W) : ae_eq f g -> ae_eq (h \* f)%R (h \* g). +Lemma ae_eq_mul2l (f g h : T -> W) : ae_eq f g -> ae_eq (h \* f) (h \* g). Proof. by apply: filterS => x /= /[apply] ->. Qed. Lemma ae_eq_mul1l (f g : T -> W) : ae_eq f (cst 1) -> ae_eq g (g \* f). From 6e3ad8d4e38b6712bd741f8a8febe5c0721dd58e Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Wed, 29 Jan 2025 14:11:27 +0100 Subject: [PATCH 19/33] wip --- theories/measure.v | 86 ++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 71 insertions(+), 15 deletions(-) diff --git a/theories/measure.v b/theories/measure.v index 399757de2..0be9c08f0 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4096,7 +4096,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 ]) @@ -4110,18 +4111,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 ring_scope. -Context d (T : sigmaRingType d) (R : realType) (U V : Type) (W : nzRingType). +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. move=> eqfg. Fail setoid_rewrite eqfg. *) Lemma ae_eq_funeposneg (f g : T -> \bar R) : ae_eq f g <-> ae_eq f^\+ g^\+ /\ ae_eq f^\- g^\-. @@ -4131,19 +4184,22 @@ split=> [fg|[pfg nfg]]. by near=> x => Dx; rewrite (funeposneg f) (funeposneg g) ?(near pfg, near nfg). Unshelve. all: by end_near. Qed. -Lemma ae_eq_refl (f : T -> U) : ae_eq f f. Proof. exact/aeW. 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_sym (f g : T -> U) : ae_eq f g -> ae_eq g f. -Proof. by apply: filterS => x + Dx => /(_ Dx). 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_trans (f g h : T -> U) : ae_eq f g -> ae_eq g h -> ae_eq f h. -Proof. by apply: filterS2 => x + + Dx => /(_ Dx) ->; exact. Qed. +Set Typeclasses Debug. +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. Fail move=> ->. -Lemma ae_eq_sub (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. +by apply: filterS2 => x + + Dx => /= /(_ Dx) -> /(_ Dx) ->. Qed. -Lemma ae_eq_mul2r (f g h : T -> W) : 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. move=>/(ae_eq_comp2 (fun x y => y * h x)). apply. + +by apply: filterS => x /= /[apply] ->. Qed. Lemma ae_eq_mul2l (f g h : T -> W) : ae_eq f g -> ae_eq (h \* f) (h \* g). Proof. by apply: filterS => x /= /[apply] ->. Qed. From 39f05386f389ddf6831c1b79d80574a2dc86eedc Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Tue, 4 Feb 2025 19:25:16 +0100 Subject: [PATCH 20/33] wip --- theories/lebesgue_integral.v | 2 + theories/lspace.v | 148 ++++++++++++++++++++++++++--------- theories/measure.v | 21 ++--- 3 files changed, 121 insertions(+), 50 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 6fb4d75d6..91ecd54f7 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -272,6 +272,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 : {mfun aT >-> rT}) = (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. diff --git a/theories/lspace.v b/theories/lspace.v index 4cc634f04..4b4a3ffe5 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -28,20 +28,24 @@ 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) (f : {mfun T >-> R}) := { + 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}. + {f : {mfun 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. +#[global] Hint Extern 0 (@LfunType _ _ _ _ _) => + solve [apply: lfuny] : core. Section Lfun_canonical. Context d (T : measurableType d) (R : realType). @@ -105,7 +109,7 @@ Lemma LType1_integrable (f : LType mu 1) : 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. +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. @@ -114,7 +118,7 @@ Lemma LType2_integrable_sqr (f : LType mu 2%:E) : 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 unlock /Lnorm ifF ?gt_eqF//. @@ -124,15 +128,95 @@ 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. + +Section lfun_pred. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : \bar R). +Definition lfun : {pred (LType mu p)} := topred (mu.-Lspace p). +Definition lfun_key : pred_key lfun. Proof. exact. Qed. +Canonical lfun_keyed := KeyedPred lfun_key. +End lfun_pred. + +Section Lspace_zmodule. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : \bar R). + +Lemma lfuny0 : finite_norm mu p (cst 0). +Proof. +rewrite /finite_norm unlock /Lnorm. +case: p => //[r|]. +- case: ifPn => r0. + rewrite preimage_cst ifF ?measure0// in_setD in_setT/=. + by apply /negP; rewrite in_setE/=. + under eq_integral => x _ do rewrite /= normr0 powR0//. + by rewrite integral0 poweR0r// invr_neq0. +case: ifPn => //mu0. +rewrite (_ : normr \o _ = cst 0); last by apply: funext => x/=; rewrite normr0. +rewrite /ess_sup. +under eq_set do rewrite preimage_cst/=. +rewrite ereal_inf_EFin ?ltry//. +rewrite /has_lbound/lbound. +- exists 0 => /= x. + case: ifPn => [_|]; first by move: mu0 => /[swap] ->; rewrite ltNge lexx. + by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. +by exists 0 => /=; rewrite ifF//; rewrite set_itvE; + rewrite memNset //=; apply/negP; rewrite -real_leNgt. +Qed. + +HB.instance Definition _ := @isLfun.Build d T R mu p (cst 0) lfuny0. + +Lemma measurable_funN (f : T -> R) D : measurable_fun D f -> measurable_fun D (\-f). +Proof. +move=> mf x Y my. +rewrite (_ : (- f) @^-1` Y = f @^-1` [set -x | x in Y]); last first. + admit. +apply: mf => //. +admit. +Admitted. + +Lemma measurable_funN_subproof (f : {mfun T >-> R}) : + measurable_fun setT (\-f). +Proof. exact: measurable_funN. Qed. + +HB.instance Definition _ (f : {mfun T >-> R}) := + isMeasurableFun.Build _ _ _ _ (\-f) (measurable_funN_subproof _). + +Lemma lfuny_opp f : finite_norm mu p f -> finite_norm mu p (\-f). +Admitted. + +Lemma Lfun_opp_subproof (f : LfunType mu p) : finite_norm mu p (\-f). +Proof. exact: lfuny_opp. Qed. + +HB.instance Definition _ (f : LfunType mu p) := + @isLfun.Build d T R mu p (\- f) (Lfun_opp_subproof _). + +Lemma lfunyD f g : + finite_norm mu p f -> finite_norm mu p g -> + finite_norm mu p (f + g). +Admitted. + +Lemma LfunD_subproof (f g : LfunType mu p) : finite_norm mu p (f \+ g). +Proof. exact: lfunyD. Qed. + +HB.instance Definition _ (f g : LfunType mu p) := + @isLfun.Build d T R mu p (f \+ g) (LfunD_subproof _ _). + +HB.about GRing.isZmodule.Build. +(* Program Definition fct_zmodMixin := *) +(* @GRing.isZmodule.Build (LfunType mu p) _ _ _ _ _ _ _. *) + +End Lspace_zmodule. + + Section Lspace_norm. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. @@ -140,11 +224,11 @@ Variable (p : R) (p1 : 1 <= p). (* 0 - + should come with proofs that they are in LfunType mu p *) -Notation ty := (T -> R). +Notation ty := (LType mu (p%:E)). 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). *) + +(* HB.instance Definition _ := GRing.Zmodule.on ty. *) (* measurable_fun setT f -> measurable_fun setT g -> (1 <= p)%R *) @@ -159,45 +243,34 @@ 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 /orP[f_fin|/eqP foo]]. +rewrite !ltNye_eq => /orP[f_fin /orP[g_fin|/eqP foo]|/eqP goo]. - rewrite -fineD ?fine_le//. - - apply: LnormD_fin_num => //. admit. admit. + - apply: LnormD_fin_num => //. - by rewrite fin_numD f_fin g_fin//. - rewrite minkowski//. admit. admit. -- rewrite foo/= add0r (_ : 'N[mu]_p%:E[(f \+ g)] = +oo%E) ?fine_ge0 ?Lnorm_ge0//. - admit. -- rewrite goo/= addr0 (_ : 'N[mu]_p%:E[(f \+ g)] = +oo%E) ?fine_ge0 ?Lnorm_ge0//. - admit. -- rewrite foo goo/= add0r (_ : 'N[mu]_p%:E[(f \+ g)] = +oo%E)//=. - admit. -Admitted. + rewrite minkowski//. +- by move: (lfuny f); rewrite /finite_norm ltey foo. +- by move: (lfuny g); rewrite /finite_norm ltey goo. +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 Lnorm_eq0 f : nm f = 0 -> f = 0 %[ae mu]. (* we need to get rid of fine *) +Lemma Lnorm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. rewrite /nm => /eqP. -rewrite fine_eq0; last first. admit. +rewrite fine_eq0; last by + rewrite fin_numElt (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _))//=; exact: lfuny. 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. +Lemma Lnorm_natmul (f : ty) 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. + rewrite mfunMn normrMn -mulr_natr powRM//= mulrC EFinM. over. rewrite /=. rewrite integralZl//; last first. admit. @@ -209,10 +282,9 @@ rewrite poweR_EFin -powRrM mulfV; last admit. rewrite powRr1//. rewrite fineM//; last admit. rewrite mulrC. - Admitted. -Lemma LnormN f : nm (-f) = nm f. +Lemma LnormN (f : ty) : nm (-f) = nm f. rewrite /nm. congr (fine _). rewrite unlock /Lnorm. @@ -221,7 +293,7 @@ move=> p0. admit. move=> p0. -congr (_ `^ _)%E. +congr (_ `^ p^-1)%E. apply eq_integral => x _. congr ((_ `^ _)%:E). by rewrite normrN. @@ -242,6 +314,8 @@ Lemma LnormN f : 'N[mu]_p%:E [- f]%R = 'N[mu]_p%:E [f]. Admitted. *) +HB.about Num.Zmodule_isSemiNormed.Build. + HB.instance Definition _ := @Num.Zmodule_isSemiNormed.Build R (*LType mu p%:E*) ty nm ler_Lnorm_add Lnorm_natmul LnormN. diff --git a/theories/measure.v b/theories/measure.v index 0be9c08f0..f04f0eaa0 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4172,9 +4172,9 @@ 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 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. move=> eqfg. Fail setoid_rewrite eqfg. *) +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^\-. @@ -4190,21 +4190,16 @@ Proof. by symmetry. 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. -Set Typeclasses Debug. 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. Fail move=> ->. - -by apply: filterS2 => x + + Dx => /= /(_ Dx) -> /(_ Dx) ->. Qed. +Proof. by apply: filterS2 => x + + Dx => /= /(_ Dx) -> /(_ Dx) ->. Qed. Lemma ae_eq_mul2r W (f g h : T -> W) : ae_eq f g -> ae_eq (f \* h) (g \* h). -Proof. move=>/(ae_eq_comp2 (fun x y => y * h x)). apply. - -by apply: filterS => x /= /[apply] ->. Qed. +Proof. by move=>/(ae_eq_comp2 (fun x y => y * h x)). Qed. -Lemma ae_eq_mul2l (f g h : T -> W) : 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 : T -> W) : ae_eq f (cst 1) -> ae_eq g (g \* f). +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 : T -> \bar R) : ae_eq f g -> ae_eq (abse \o f) (abse \o g). From a6aad220a273624f279fa95bf432cd3b9ec4d659 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Tue, 4 Feb 2025 21:22:20 +0100 Subject: [PATCH 21/33] wip --- theories/lebesgue_integral.v | 3 +- theories/lspace.v | 147 ++++++++++++++++++++--------------- 2 files changed, 87 insertions(+), 63 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 91ecd54f7..091e4d1cd 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -272,7 +272,7 @@ 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 : {mfun aT >-> rT}) = (fun x => f x *+ n) :> (_ -> _). +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. @@ -287,6 +287,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 4b4a3ffe5..1f4027f74 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -149,6 +149,7 @@ End lfun_pred. Section Lspace_zmodule. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (p : \bar R). +Hypothesis (p1 : (1 <= p)%E). Lemma lfuny0 : finite_norm mu p (cst 0). Proof. @@ -174,24 +175,16 @@ Qed. HB.instance Definition _ := @isLfun.Build d T R mu p (cst 0) lfuny0. -Lemma measurable_funN (f : T -> R) D : measurable_fun D f -> measurable_fun D (\-f). -Proof. -move=> mf x Y my. -rewrite (_ : (- f) @^-1` Y = f @^-1` [set -x | x in Y]); last first. - admit. -apply: mf => //. -admit. -Admitted. - +(* TODO: move to lebesgue_measure.v *) Lemma measurable_funN_subproof (f : {mfun T >-> R}) : measurable_fun setT (\-f). -Proof. exact: measurable_funN. Qed. +Proof. exact: measurableT_comp. Qed. HB.instance Definition _ (f : {mfun T >-> R}) := isMeasurableFun.Build _ _ _ _ (\-f) (measurable_funN_subproof _). Lemma lfuny_opp f : finite_norm mu p f -> finite_norm mu p (\-f). -Admitted. +Proof. by rewrite /finite_norm oppr_Lnorm. Qed. Lemma Lfun_opp_subproof (f : LfunType mu p) : finite_norm mu p (\-f). Proof. exact: lfuny_opp. Qed. @@ -199,10 +192,23 @@ Proof. exact: lfuny_opp. Qed. HB.instance Definition _ (f : LfunType mu p) := @isLfun.Build d T R mu p (\- f) (Lfun_opp_subproof _). -Lemma lfunyD f g : +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. + +Lemma lfunyD (f g : {mfun T >-> R}) : finite_norm mu p f -> finite_norm mu p g -> finite_norm mu p (f + g). -Admitted. +Proof. +rewrite /finite_norm => ff fg. +apply: le_lt_trans; first exact: minkowskie. +exact: lte_add_pinfty. +Qed. Lemma LfunD_subproof (f g : LfunType mu p) : finite_norm mu p (f \+ g). Proof. exact: lfunyD. Qed. @@ -214,6 +220,42 @@ HB.about GRing.isZmodule.Build. (* Program Definition fct_zmodMixin := *) (* @GRing.isZmodule.Build (LfunType mu p) _ _ _ _ _ _ _. *) +Lemma powRMn (x : R) r n : 0 <= x -> ((x *+ n) `^ r) = ((x `^ r) * (n%:R `^ r)). +Proof. by move=> x0; rewrite -[in LHS]mulr_natr powRM. Qed. + +Lemma LnormMn (f : {mfun T >-> R}) n : 'N[mu]_p[f *+ n] = 'N[mu]_p[f] *+ n. +Proof. +rewrite unlock /Lnorm. +case: p => [r||]. +- case: ifPn => r0. + admit. + under eq_integral => x _. rewrite mfunMn normrMn powRMn// EFinM. over. + rewrite integralZr//; last first. + admit. + rewrite poweRM; last 2 first. + - by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. + - by rewrite lee_fin powR_ge0. + by rewrite poweR_EFin -powRrM divff// powRr1// muleC mule_natl. +- case: ifPn => mu0. admit. +all: by rewrite mul0rn. +Admitted. + +Lemma lfunyMn (f : {mfun T >-> R}) n : + finite_norm mu p f -> finite_norm mu p (f *+ n). +Proof. +rewrite/finite_norm LnormMn=> ff. +rewrite (_ : ('N[mu]_p[f] *+ n)%R = n%:R%:E * 'N[mu]_p[f])%E; last by rewrite mule_natl. +exact: lte_mul_pinfty. +Qed. + +Notation "f \*+ n" := (fun x => f x *+ n) (at level 10). + +Lemma LfunyMn_subproof (f : LfunType mu p) (n : nat) : finite_norm mu p (f \*+ n). +Proof. by rewrite -mfunMn; exact: lfunyMn. Qed. + +(* HB.instance Definition _ (f : LfunType mu p) n := *) +(* @isLfun.Build d T R mu p (fun x => f x \* n) (LfunyMn_subproof _ _). *) + End Lspace_zmodule. @@ -240,65 +282,45 @@ Definition nm f := fine ('N[mu]_p%:E[f]). 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//. - - apply: LnormD_fin_num => //. - - by rewrite fin_numD f_fin g_fin//. - rewrite minkowski//. -- by move: (lfuny f); rewrite /finite_norm ltey foo. -- by move: (lfuny g); rewrite /finite_norm ltey goo. +rewrite /nm -fineD ?fine_le ?minkowski// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=. +- rewrite (le_lt_trans (minkowski _ _ _ _))//. + 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 enatmul_ninfty (n : nat) : (-oo *+ n.+1 = -oo :> \bar R)%E \/ (-oo *+ n.+1 = +oo :> \bar R)%E. +Proof. +Admitted. + +Lemma Lnorm_natmul (f : ty) k : nm (fun x => f x *+ k) = nm f *+ k. +rewrite /nm. rewrite -mfunMn LnormMn// /fine. +case: k => [|n]; first by rewrite !mulr0n. +case: 'N[mu]_p%:E[f] => [r||]. +- by rewrite (_ : r%:E *+ n.+1 = (r *+ n.+1)%:E)// EFin_natmul. +- rewrite (_ : +oo%E *+ n.+1 = +oo%E); last exact: enatmul_pinfty. + by rewrite mul0rn. +- have [noo|noo] := enatmul_ninfty n. + by rewrite (_ : -oo%E *+ n.+1 = -oo%E)// mul0rn. + by rewrite (_ : -oo%E *+ n.+1 = +oo%E)// mul0rn. +Qed. + Lemma Lnorm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. +Proof. rewrite /nm => /eqP. rewrite fine_eq0; last by rewrite fin_numElt (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _))//=; exact: lfuny. move/eqP/Lnorm_eq0_eq0. Admitted. -Lemma Lnorm_natmul (f : ty) k : nm (f *+ k) = nm f *+ k. -rewrite /nm unlock /Lnorm. -case: (ifP (p == 0)). - admit. - -move => p0. -under eq_integral => x _. - rewrite mfunMn normrMn -mulr_natr powRM//= 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 : ty) : nm (-f) = nm f. -rewrite /nm. -congr (fine _). -rewrite unlock /Lnorm. -case: ifP. -move=> p0. - admit. - -move=> p0. -congr (_ `^ p^-1)%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]. @@ -316,9 +338,10 @@ Admitted. HB.about Num.Zmodule_isSemiNormed.Build. -HB.instance Definition _ := - @Num.Zmodule_isSemiNormed.Build R (*LType mu p%:E*) ty - nm ler_Lnorm_add Lnorm_natmul LnormN. +(* TODO : fix the definition *) +(* HB.instance Definition _ := *) +(* @Num.Zmodule_isSemiNormed.Build R (LfunType mu p%:E) ty *) +(* nm ler_Lnorm_add Lnorm_natmul LnormN. *) (* todo: add equivalent of mx_normZ and HB instance *) From c2e26585b3c3070cc630e48fe41d6120cbaa0d15 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Wed, 5 Feb 2025 00:53:00 +0100 Subject: [PATCH 22/33] wip --- theories/lspace.v | 110 ++++++++++++++++++++++++++-------------------- 1 file changed, 62 insertions(+), 48 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 1f4027f74..f90f2bb18 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -223,41 +223,61 @@ HB.about GRing.isZmodule.Build. Lemma powRMn (x : R) r n : 0 <= x -> ((x *+ n) `^ r) = ((x `^ r) * (n%:R `^ r)). Proof. by move=> x0; rewrite -[in LHS]mulr_natr powRM. Qed. -Lemma LnormMn (f : {mfun T >-> R}) n : 'N[mu]_p[f *+ n] = 'N[mu]_p[f] *+ n. +Local Notation "f \*+ n" := (fun x => f x *+ n) (at level 10). + +Lemma ess_sup0 : (ess_sup mu (cst 0)%R = 0)%E. +Admitted. + +Lemma ess_supMn f n : (ess_sup mu (f \*+ n) = ess_sup mu f *+ n)%E. +Admitted. + +Lemma mule0n n : (0 *+ n = 0 :> \bar R)%E. +Proof. by rewrite -mule_natl mule0. Qed. + + +Lemma LnormMn (f : LfunType mu p) n : ('N[mu]_p[f \*+ n] = 'N[mu]_p[f] *+ n)%E. Proof. rewrite unlock /Lnorm. +move: p1 f. case: p => [r||]. -- case: ifPn => r0. - admit. - under eq_integral => x _. rewrite mfunMn normrMn powRMn// EFinM. over. - rewrite integralZr//; last first. - admit. +- rewrite lee_fin => r1 f. + have r0 : 0 < r by rewrite (lt_le_trans _ r1). + under eq_integral => x _ do rewrite normrMn powRMn// EFinM. + rewrite (gt_eqF r0) integralZr//; last first. + apply/integrableP; split. + apply: measurable_funT_comp => //. + apply: (measurable_funT_comp (measurable_powR _)) => //. + exact: measurable_funT_comp. + under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. + apply: (@lty_poweRy _ _ (r^-1)); first by rewrite invr_neq0// gt_eqF. + have := lfuny f. + by rewrite /finite_norm unlock /Lnorm gt_eqF. rewrite poweRM; last 2 first. - by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. - by rewrite lee_fin powR_ge0. - by rewrite poweR_EFin -powRrM divff// powRr1// muleC mule_natl. -- case: ifPn => mu0. admit. -all: by rewrite mul0rn. -Admitted. + by rewrite poweR_EFin -powRrM divff// ?gt_eqF// powRr1// muleC mule_natl. +- move=> _ f; case: ifPn => mu0. + rewrite (_ : normr \o f \*+ n = (normr \o f) \*+ n); last first. + by apply: funext => x/=; rewrite normrMn. + exact: ess_supMn. +- by rewrite mule0n. +by rewrite leeNy_eq => /eqP. +Qed. -Lemma lfunyMn (f : {mfun T >-> R}) n : - finite_norm mu p f -> finite_norm mu p (f *+ n). +Lemma lfunyMn (f : LfunType mu p) n : + finite_norm mu p f -> finite_norm mu p (f \*+ n)%E. Proof. -rewrite/finite_norm LnormMn=> ff. -rewrite (_ : ('N[mu]_p[f] *+ n)%R = n%:R%:E * 'N[mu]_p[f])%E; last by rewrite mule_natl. -exact: lte_mul_pinfty. +by rewrite/finite_norm LnormMn => ff; rewrite -mule_natl; exact: lte_mul_pinfty. Qed. -Notation "f \*+ n" := (fun x => f x *+ n) (at level 10). - Lemma LfunyMn_subproof (f : LfunType mu p) (n : nat) : finite_norm mu p (f \*+ n). -Proof. by rewrite -mfunMn; exact: lfunyMn. Qed. +Proof. exact: lfunyMn. Qed. (* HB.instance Definition _ (f : LfunType mu p) n := *) -(* @isLfun.Build d T R mu p (fun x => f x \* n) (LfunyMn_subproof _ _). *) +(* @isLfun.Build d T R mu p (f \*+ n) (LfunyMn_subproof _ _). *) End Lspace_zmodule. - +Notation "f \*+ n" := (fun x => f x *+ n) (at level 10). Section Lspace_norm. Context d (T : measurableType d) (R : realType). @@ -298,19 +318,22 @@ 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. +Proof. by elim: n => //=[|n []->]; rewrite ?addNye; left. Qed. + +Lemma Lnorm0 : ('N[mu]_p%:E[0%R] = 0)%E. Proof. -Admitted. +rewrite unlock /Lnorm. +case: ifPn => _. + by rewrite preimage_cst ifF//=; apply/negP; rewrite in_setE/=; case. +under eq_integral => x _ do rewrite normr0 powR0 ?gt_eqF// ?(lt_le_trans _ p1)//. +by rewrite integral0 poweR0r// gt_eqF// invr_gt0 (lt_le_trans _ p1). +Qed. -Lemma Lnorm_natmul (f : ty) k : nm (fun x => f x *+ k) = nm f *+ k. -rewrite /nm. rewrite -mfunMn LnormMn// /fine. -case: k => [|n]; first by rewrite !mulr0n. -case: 'N[mu]_p%:E[f] => [r||]. -- by rewrite (_ : r%:E *+ n.+1 = (r *+ n.+1)%:E)// EFin_natmul. -- rewrite (_ : +oo%E *+ n.+1 = +oo%E); last exact: enatmul_pinfty. - by rewrite mul0rn. -- have [noo|noo] := enatmul_ninfty n. - by rewrite (_ : -oo%E *+ n.+1 = -oo%E)// mul0rn. - by rewrite (_ : -oo%E *+ n.+1 = +oo%E)// mul0rn. +Lemma Lnorm_natmul (f : ty) k : nm (f \*+ k) = nm f *+ k. +Proof. +rewrite /nm LnormMn// -mule_natl -[RHS]mulr_natl fineM// fin_numElt. +have := lfuny f. +by rewrite /finite_norm (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _)) => ->. Qed. Lemma Lnorm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. @@ -318,23 +341,14 @@ Proof. rewrite /nm => /eqP. rewrite fine_eq0; last by rewrite fin_numElt (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _))//=; exact: lfuny. -move/eqP/Lnorm_eq0_eq0. -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. -*) +have p0 : 0 < p by exact: lt_le_trans. +move/eqP/Lnorm_eq0_eq0 => /(_ p0 (measurable_funP _)) eqnorm. +near=> x => Dx. +suffices: ((`|f x| `^ p)%:E = cst 0 x)%E. + by rewrite (_ : 0 x = 0)//=; case; move/powR_eq0_eq0/normr0_eq0. +apply: (near eqnorm x) => //. +Unshelve. all: by end_near. +Qed. HB.about Num.Zmodule_isSemiNormed.Build. From a2527b7efaac165ca95a16544fca22f3c09ad1b1 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Wed, 5 Feb 2025 11:35:21 +0100 Subject: [PATCH 23/33] - hoelder.v doc - better interface in lspace.v --- theories/hoelder.v | 37 +++---------------------------------- theories/lspace.v | 17 +++++++++-------- 2 files changed, 12 insertions(+), 42 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 39b8a8f2d..6019fdc8f 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -10,10 +10,10 @@ From mathcomp Require Import numfun exp convex itv. (**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 *) (* ``` *) (* *) (******************************************************************************) @@ -539,34 +539,3 @@ apply: measurableT_comp => //. 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. - by move=> t/=; exact: normr_ge0. - admit. -- by rewrite leeNy_eq => /eqP. -Admitted. - - -End Lnorm_properties. diff --git a/theories/lspace.v b/theories/lspace.v index f90f2bb18..a8c10e77d 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -33,14 +33,15 @@ Definition finite_norm d (T : measurableType d) (R : realType) ('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 : {mfun T >-> R}) := { + (mu : {measure set T -> \bar R}) (p : \bar R) (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 : {mfun T >-> R} & isLfun d T R mu p f}. + {f of @MeasurableFun d _ T R f & isLfun d T R mu p f}. Arguments lfuny {d} {T} {R} {mu} {p} _. #[global] Hint Resolve lfuny : core. @@ -138,7 +139,7 @@ End Lspace. Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope. -Section lfun_pred. +Section lfun_pred. (* find a good name *) Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (p : \bar R). Definition lfun : {pred (LType mu p)} := topred (mu.-Lspace p). @@ -201,9 +202,9 @@ measurable_fun [set: T] g -> (* TODO: Jairo is working on this *) Admitted. -Lemma lfunyD (f g : {mfun T >-> R}) : +Lemma lfunyD (f g : LfunType mu p) : finite_norm mu p f -> finite_norm mu p g -> - finite_norm mu p (f + g). + finite_norm mu p (f \+ g). Proof. rewrite /finite_norm => ff fg. apply: le_lt_trans; first exact: minkowskie. @@ -353,9 +354,9 @@ Qed. HB.about Num.Zmodule_isSemiNormed.Build. (* TODO : fix the definition *) -(* HB.instance Definition _ := *) -(* @Num.Zmodule_isSemiNormed.Build R (LfunType mu p%:E) ty *) -(* nm ler_Lnorm_add Lnorm_natmul LnormN. *) +HB.instance Definition _ := + @Num.Zmodule_isSemiNormed.Build R (LfunType mu p%:E) ty + nm ler_Lnorm_add Lnorm_natmul LnormN. (* todo: add equivalent of mx_normZ and HB instance *) From 11b66a9258ba73990e0af55469a8e71e38fb47fc Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Wed, 5 Feb 2025 18:53:30 +0100 Subject: [PATCH 24/33] wip --- theories/lspace.v | 79 ++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 72 insertions(+), 7 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index a8c10e77d..47e811ef9 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -138,15 +138,77 @@ Qed. End Lspace. Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope. - -Section lfun_pred. (* find a good name *) +(* move to hoelder.v *) +Section conjugate. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (p : \bar R). -Definition lfun : {pred (LType mu p)} := topred (mu.-Lspace p). +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) (p1 : (1 <= p)%E). + +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. +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 f (set_mem (sub_lfun_finlfun fP)). + +Import HBSimple. + +#[local] HB.instance Definition _ := lfun_Sub2_subproof. +End Sub. + + +End lfun. + + Section Lspace_zmodule. Context d (T : measurableType d) (R : realType). Variables (mu : {measure set T -> \bar R}) (p : \bar R). @@ -218,8 +280,12 @@ HB.instance Definition _ (f g : LfunType mu p) := @isLfun.Build d T R mu p (f \+ g) (LfunD_subproof _ _). HB.about GRing.isZmodule.Build. -(* Program Definition fct_zmodMixin := *) -(* @GRing.isZmodule.Build (LfunType mu p) _ _ _ _ _ _ _. *) +Program Definition fct_zmodMixin := + @GRing.isZmodule.Build (LfunType mu p) (cst 0) (fun f => \- f) (fun f g => f \+ g) _ _ _ _. +Next Obligation. move=> f g h; rewrite -!fctD addrA !fctD. Admitted. +Next Obligation. move=> f g; rewrite -!fctD addrC !fctD. Admitted. +Next Obligation. move=> f; rewrite -fctD. Admitted. +Next Obligation. move=> f. Admitted. Lemma powRMn (x : R) r n : 0 <= x -> ((x *+ n) `^ r) = ((x `^ r) * (n%:R `^ r)). Proof. by move=> x0; rewrite -[in LHS]mulr_natr powRM. Qed. @@ -278,7 +344,6 @@ Proof. exact: lfunyMn. Qed. (* @isLfun.Build d T R mu p (f \*+ n) (LfunyMn_subproof _ _). *) End Lspace_zmodule. -Notation "f \*+ n" := (fun x => f x *+ n) (at level 10). Section Lspace_norm. Context d (T : measurableType d) (R : realType). @@ -301,7 +366,7 @@ 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 -fineD ?fine_le ?minkowski// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=. - rewrite (le_lt_trans (minkowski _ _ _ _))//. From 40e631fe4c9b6237b70611f43ffbe569015da31a Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Fri, 7 Feb 2025 00:08:50 +0100 Subject: [PATCH 25/33] wip --- theories/lspace.v | 338 ++++++++++++++++++++++++---------------------- 1 file changed, 178 insertions(+), 160 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 47e811ef9..7941998cc 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -33,15 +33,15 @@ Definition finite_norm d (T : measurableType d) (R : realType) ('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) + (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 of @MeasurableFun d _ T R f & 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}. Arguments lfuny {d} {T} {R} {mu} {p} _. #[global] Hint Resolve lfuny : core. @@ -50,18 +50,18 @@ 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 : \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. @@ -89,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. @@ -103,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. +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). 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. @@ -177,7 +183,7 @@ End conjugate. Section lfun_pred. Context d (T : measurableType d) (R : realType). -Variables (mu : {measure set T -> \bar R}) (p : \bar R) (p1 : (1 <= p)%E). +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]. @@ -187,6 +193,17 @@ 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). @@ -198,162 +215,136 @@ 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 f (set_mem (sub_lfun_finlfun fP)). + @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. -End lfun. +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. -Section Lspace_zmodule. -Context d (T : measurableType d) (R : realType). -Variables (mu : {measure set T -> \bar R}) (p : \bar R). -Hypothesis (p1 : (1 <= p)%E). +HB.instance Definition _ := [Choice of LfunType mu p1 by <:]. -Lemma lfuny0 : finite_norm mu p (cst 0). +Import numFieldNormedType.Exports. + +Lemma ess_sup0_lty : (0 < mu setT)%E -> (ess_sup mu 0%R < +oo)%E. Proof. -rewrite /finite_norm unlock /Lnorm. -case: p => //[r|]. -- case: ifPn => r0. - rewrite preimage_cst ifF ?measure0// in_setD in_setT/=. - by apply /negP; rewrite in_setE/=. - under eq_integral => x _ do rewrite /= normr0 powR0//. - by rewrite integral0 poweR0r// invr_neq0. -case: ifPn => //mu0. -rewrite (_ : normr \o _ = cst 0); last by apply: funext => x/=; rewrite normr0. -rewrite /ess_sup. +rewrite /ess_sup => mu0. under eq_set do rewrite preimage_cst/=. rewrite ereal_inf_EFin ?ltry//. -rewrite /has_lbound/lbound. -- exists 0 => /= x. - case: ifPn => [_|]; first by move: mu0 => /[swap] ->; rewrite ltNge lexx. +- exists 0 => x/=; case: ifPn => [_|]. + by move: mu0 => /[swap] ->; rewrite ltNge lexx. by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. by exists 0 => /=; rewrite ifF//; rewrite set_itvE; rewrite memNset //=; apply/negP; rewrite -real_leNgt. Qed. -HB.instance Definition _ := @isLfun.Build d T R mu p (cst 0) lfuny0. - -(* TODO: move to lebesgue_measure.v *) -Lemma measurable_funN_subproof (f : {mfun T >-> R}) : - measurable_fun setT (\-f). -Proof. exact: measurableT_comp. Qed. - -HB.instance Definition _ (f : {mfun T >-> R}) := - isMeasurableFun.Build _ _ _ _ (\-f) (measurable_funN_subproof _). - -Lemma lfuny_opp f : finite_norm mu p f -> finite_norm mu p (\-f). -Proof. by rewrite /finite_norm oppr_Lnorm. Qed. - -Lemma Lfun_opp_subproof (f : LfunType mu p) : finite_norm mu p (\-f). -Proof. exact: lfuny_opp. Qed. - -HB.instance Definition _ (f : LfunType mu p) := - @isLfun.Build d T R mu p (\- f) (Lfun_opp_subproof _). - -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. +Lemma ess_sup0 : (0 < mu setT)%E -> (ess_sup mu 0%R = 0)%E. +Proof. +rewrite /ess_sup => mu0. +under eq_set do rewrite preimage_cst/=. +rewrite ereal_inf_EFin. +- congr (_%:E). + rewrite [X in inf X](_ : _ = `[0, +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 0 => x/=; case: ifPn => [_|]. + by move: mu0 => /[swap] ->; rewrite ltNge lexx. + by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. +by exists 0 => /=; rewrite ifF//; rewrite set_itvE; + rewrite memNset //=; apply/negP; rewrite -real_leNgt. +Qed. -Lemma lfunyD (f g : LfunType mu p) : - finite_norm mu p f -> finite_norm mu p g -> - finite_norm mu p (f \+ g). +Lemma Lnorm0 : 'N[mu]_p[cst 0] = 0. Proof. -rewrite /finite_norm => ff fg. -apply: le_lt_trans; first exact: minkowskie. -exact: lte_add_pinfty. +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_sup0. Qed. -Lemma LfunD_subproof (f g : LfunType mu p) : finite_norm mu p (f \+ g). -Proof. exact: lfunyD. Qed. +Lemma lfuny0 : finite_norm mu p (cst 0). +Proof. by rewrite /finite_norm Lnorm0. Qed. -HB.instance Definition _ (f g : LfunType mu p) := - @isLfun.Build d T R mu p (f \+ g) (LfunD_subproof _ _). +HB.instance Definition _ := @isLfun.Build d T R mu p p1 (cst 0) lfuny0. -HB.about GRing.isZmodule.Build. -Program Definition fct_zmodMixin := - @GRing.isZmodule.Build (LfunType mu p) (cst 0) (fun f => \- f) (fun f g => f \+ g) _ _ _ _. -Next Obligation. move=> f g h; rewrite -!fctD addrA !fctD. Admitted. -Next Obligation. move=> f g; rewrite -!fctD addrC !fctD. Admitted. -Next Obligation. move=> f; rewrite -fctD. Admitted. -Next Obligation. move=> f. Admitted. +Lemma mfunP (f : {mfun T >-> R}) : (f : T -> R) \in mfun. +Proof. exact: valP. Qed. -Lemma powRMn (x : R) r n : 0 <= x -> ((x *+ n) `^ r) = ((x `^ r) * (n%:R `^ r)). -Proof. by move=> x0; rewrite -[in LHS]mulr_natr powRM. Qed. +Lemma lfunP (f : LfunType mu p1) : (f : T -> R) \in lfun. +Proof. exact: valP. Qed. -Local Notation "f \*+ n" := (fun x => f x *+ n) (at level 10). +Lemma mfun_scaler_closed : scaler_closed (@mfun _ _ T R). +Proof. move=> a/= f; rewrite !inE; exact: measurable_funM. Qed. -Lemma ess_sup0 : (ess_sup mu (cst 0)%R = 0)%E. -Admitted. +HB.instance Definition _ := GRing.isScaleClosed.Build _ _ (@mfun _ _ T R) + mfun_scaler_closed. +HB.instance Definition _ := [SubZmodule_isSubLmodule of {mfun T >-> R} by <:]. -Lemma ess_supMn f n : (ess_sup mu (f \*+ n) = ess_sup mu f *+ n)%E. +Lemma LnormZ (f : LfunType mu p1) a : ('N[mu]_p[a \*: f] = `|a|%:E * 'N[mu]_p[f])%E. Admitted. -Lemma mule0n n : (0 *+ n = 0 :> \bar R)%E. -Proof. by rewrite -mule_natl mule0. Qed. - - -Lemma LnormMn (f : LfunType mu p) n : ('N[mu]_p[f \*+ n] = 'N[mu]_p[f] *+ n)%E. +Lemma lfun_submod_closed : submod_closed (lfun). Proof. -rewrite unlock /Lnorm. -move: p1 f. -case: p => [r||]. -- rewrite lee_fin => r1 f. - have r0 : 0 < r by rewrite (lt_le_trans _ r1). - under eq_integral => x _ do rewrite normrMn powRMn// EFinM. - rewrite (gt_eqF r0) integralZr//; last first. - apply/integrableP; split. - apply: measurable_funT_comp => //. - apply: (measurable_funT_comp (measurable_powR _)) => //. - exact: measurable_funT_comp. - under eq_integral => x _ do rewrite gee0_abs ?lee_fin ?powR_ge0//. - apply: (@lty_poweRy _ _ (r^-1)); first by rewrite invr_neq0// gt_eqF. - have := lfuny f. - by rewrite /finite_norm unlock /Lnorm gt_eqF. - rewrite poweRM; last 2 first. - - by apply: integral_ge0 => x _; rewrite lee_fin powR_ge0. - - by rewrite lee_fin powR_ge0. - by rewrite poweR_EFin -powRrM divff// ?gt_eqF// powRr1// muleC mule_natl. -- move=> _ f; case: ifPn => mu0. - rewrite (_ : normr \o f \*+ n = (normr \o f) \*+ n); last first. - by apply: funext => x/=; rewrite normrMn. - exact: ess_supMn. -- by rewrite mule0n. -by rewrite leeNy_eq => /eqP. +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. -Lemma lfunyMn (f : LfunType mu p) n : - finite_norm mu p f -> finite_norm mu p (f \*+ n)%E. -Proof. -by rewrite/finite_norm LnormMn => ff; rewrite -mule_natl; exact: lte_mul_pinfty. -Qed. - -Lemma LfunyMn_subproof (f : LfunType mu p) (n : nat) : finite_norm mu p (f \*+ n). -Proof. exact: lfunyMn. Qed. - -(* HB.instance Definition _ (f : LfunType mu p) n := *) -(* @isLfun.Build d T R mu p (f \*+ n) (LfunyMn_subproof _ _). *) +HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ lfun + lfun_submod_closed. +HB.instance Definition _ := [SubChoice_isSubLmodule of LfunType mu p1 by <:]. -End Lspace_zmodule. +End lfun. Section Lspace_norm. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. -Variable (p : R) (p1 : 1 <= p). +Variable (p : \bar R) (p1 : (1 <= p)%E). (* 0 - + should come with proofs that they are in LfunType mu p *) -Notation ty := (LType mu (p%:E)). -Definition nm f := fine ('N[mu]_p%:E[f]). +Notation ty := (LfunType mu p1). +Definition nm f := fine ('N[mu]_p[f]). (* HB.instance Definition _ := GRing.Zmodule.on ty. *) @@ -368,8 +359,8 @@ Definition nm f := fine ('N[mu]_p%:E[f]). Lemma ler_Lnorm_add (f g : ty) : nm (f + g) <= nm f + nm g. Proof. -rewrite /nm -fineD ?fine_le ?minkowski// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=. -- rewrite (le_lt_trans (minkowski _ _ _ _))//. +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. @@ -386,45 +377,72 @@ 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. Proof. by elim: n => //=[|n []->]; rewrite ?addNye; left. Qed. -Lemma Lnorm0 : ('N[mu]_p%:E[0%R] = 0)%E. -Proof. -rewrite unlock /Lnorm. -case: ifPn => _. - by rewrite preimage_cst ifF//=; apply/negP; rewrite in_setE/=; case. -under eq_integral => x _ do rewrite normr0 powR0 ?gt_eqF// ?(lt_le_trans _ p1)//. -by rewrite integral0 poweR0r// gt_eqF// invr_gt0 (lt_le_trans _ p1). -Qed. - -Lemma Lnorm_natmul (f : ty) k : nm (f \*+ k) = nm f *+ k. +Lemma Lnorm_natmul (f : ty) k : nm (f *+ k) = nm f *+ k. Proof. -rewrite /nm LnormMn// -mule_natl -[RHS]mulr_natl fineM// fin_numElt. -have := lfuny f. +rewrite /nm. +rewrite -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_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. -Proof. -rewrite /nm => /eqP. -rewrite fine_eq0; last by - rewrite fin_numElt (lt_le_trans ltNy0 (Lnorm_ge0 _ _ _))//=; exact: lfuny. -have p0 : 0 < p by exact: lt_le_trans. -move/eqP/Lnorm_eq0_eq0 => /(_ p0 (measurable_funP _)) eqnorm. -near=> x => Dx. -suffices: ((`|f x| `^ p)%:E = cst 0 x)%E. - by rewrite (_ : 0 x = 0)//=; case; move/powR_eq0_eq0/normr0_eq0. -apply: (near eqnorm x) => //. -Unshelve. all: by end_near. -Qed. HB.about Num.Zmodule_isSemiNormed.Build. (* TODO : fix the definition *) HB.instance Definition _ := - @Num.Zmodule_isSemiNormed.Build R (LfunType mu p%:E) ty - nm ler_Lnorm_add Lnorm_natmul LnormN. + @Num.Zmodule_isSemiNormed.Build R (LfunType mu p1) + nm ler_Lnorm_add Lnorm_natmul LnormN. (* todo: add equivalent of mx_normZ and HB instance *) +(* ess_sup mu (normr \o f) = 0 -> ae_eq mu [set: T] f (cst 0) *) + +(* TODO: move to hoelder *) +Lemma Lnorm_eq0_eq0 (f : {mfun T >-> R}) : (0 < p)%E -> + 'N[mu]_p[f] = 0 -> ae_eq mu [set: T] f (cst 0). +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 _|]. + admit. + 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 []. +Admitted. + + +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. + + End Lspace_norm. (* From 9cb80f38d0e2df55838aecbd9986506aac668316 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Fri, 7 Feb 2025 01:43:40 +0100 Subject: [PATCH 26/33] wip --- theories/lspace.v | 51 ++++++++++++++++++++++++++++++++--------------- 1 file changed, 35 insertions(+), 16 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 7941998cc..7da76be76 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -245,36 +245,36 @@ HB.instance Definition _ := [Choice of LfunType mu p1 by <:]. Import numFieldNormedType.Exports. -Lemma ess_sup0_lty : (0 < mu setT)%E -> (ess_sup mu 0%R < +oo)%E. +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 0 => x/=; case: ifPn => [_|]. +- exists r => x/=; case: ifPn => [_|]. by move: mu0 => /[swap] ->; rewrite ltNge lexx. by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. -by exists 0 => /=; rewrite ifF//; rewrite set_itvE; - rewrite memNset //=; apply/negP; rewrite -real_leNgt. +by exists r => /=; rewrite ifF//; rewrite set_itvE; + rewrite memNset //=; apply/negP; rewrite -real_leNgt ?num_real. Qed. -Lemma ess_sup0 : (0 < mu setT)%E -> (ess_sup mu 0%R = 0)%E. +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](_ : _ = `[0, +oo[%classic); last first. + 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 0 => x/=; case: ifPn => [_|]. +- exists r => x/=; case: ifPn => [_|]. by move: mu0 => /[swap] ->; rewrite ltNge lexx. by rewrite set_itvE notin_setE//= ltNge => /negP/negbNE. -by exists 0 => /=; rewrite ifF//; rewrite set_itvE; - rewrite memNset //=; apply/negP; rewrite -real_leNgt. +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. @@ -289,7 +289,7 @@ case: p => [r||//]. by rewrite integral0 poweR0r// invr_neq0. case: ifPn => //mu0 _. rewrite (_ : normr \o _ = 0); last by apply: funext => x/=; rewrite normr0. -exact: ess_sup0. +exact: ess_sup_cst. Qed. Lemma lfuny0 : finite_norm mu p (cst 0). @@ -379,8 +379,7 @@ Proof. by elim: n => //=[|n []->]; rewrite ?addNye; left. Qed. Lemma Lnorm_natmul (f : ty) k : nm (f *+ k) = nm f *+ k. Proof. -rewrite /nm. -rewrite -scaler_nat LnormZ fineM//= ?normr_nat ?mulr_natl// fin_numElt. +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. @@ -395,11 +394,31 @@ HB.instance Definition _ := (* todo: add equivalent of mx_normZ and HB instance *) -(* ess_sup mu (normr \o f) = 0 -> ae_eq mu [set: T] f (cst 0) *) +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 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 -> ae_eq mu [set: T] f (cst 0). + 'N[mu]_p[f] = 0 -> f = 0 %[ae mu]. Proof. rewrite unlock /Lnorm => p0. move: p0. @@ -421,14 +440,14 @@ case: p => [r r0||]. apply: filterS => x/= /[apply]. by case=> /powR_eq0_eq0 /eqP; rewrite normr_eq0 => /eqP. - case: ifPn => [mu0 _|]. - admit. + 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 []. -Admitted. +Qed. Lemma Lnorm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. From 4fa4057d730399cd636856c63ea7d3b475da1c7e Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 7 Feb 2025 17:57:47 +0100 Subject: [PATCH 27/33] compressions --- theories/lspace.v | 21 ++++++++------------- 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 7da76be76..8d8393c89 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 9dbf281b52d32fbff4bb55e7dfdcec5019732de5 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 8 Feb 2025 00:28:59 +0100 Subject: [PATCH 28/33] wip refactoring --- theories/hoelder.v | 73 +++++++++++++---- theories/lspace.v | 196 +++++++++++++++++---------------------------- theories/measure.v | 41 ++++++++++ 3 files changed, 173 insertions(+), 137 deletions(-) diff --git a/theories/hoelder.v b/theories/hoelder.v index 6019fdc8f..55e0a73fc 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -40,7 +40,7 @@ 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))) `^ p^-1 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 @@ -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 8d8393c89..6dfe7a6db 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,7 +263,30 @@ 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. +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. admit. +by rewrite mule0. Admitted. Lemma lfun_submod_closed : submod_closed (lfun). @@ -331,6 +312,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,6 +323,10 @@ Variable (p : \bar R) (p1 : (1 <= p)%E). 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. +Qed. (* HB.instance Definition _ := GRing.Zmodule.on ty. *) @@ -353,14 +339,7 @@ Definition nm f := fine ('N[mu]_p[f]). 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 +353,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 +367,59 @@ 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. -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]. +Lemma nm_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. +Lemma Lspace_inclusion (p q : R) (p1 : 1 <= p) (q1 : (1 <= q%:E)%E) : + (p <= q) -> forall (f : LfunType mu q1), finite_norm mu (p%:E) f. Proof. -move=> pleq f. - -isLfun d T R mu p f. +(* move=> pleq f. *) +(* have := lfuny q1 f. *) +(* rewrite /finite_norm. *) +(* pose r := [get x : R | p = q * x] : R. *) +(* pose r' := [get x : R | r^-1 + x^-1 = 1] : R. *) +(* have := (@hoelder _ _ _ mu (fun x => `|f x| `^ p) (cst 1)%R r r'). *) +(* rewrite (_ : ((fun x : T => `|f x| `^ p) \* cst 1)%R = (fun x : T => `|f x| `^ p)); last first. *) +(* by rewrite -fctM mulr1. *) + +(* have /=r := conjugate q. *) +(* have h : forall h : p < +oo, exists r, q = p * r /\ 1 <= r. *) +(* exists (q * ((fine p)^-1)%:E). *) +(* move: p1 q1 pleq f h. *) +(* case q=> //[r|]. *) +(* case p=> //=t t1 r1. *) +(* rewrite -!EFinM -mulrCA divff ?(gt_eqF (lt_le_trans ltr01 _))// mulr1 !lee_fin. *) +(* by move=> tr _; rewrite ler_pdivlMr ?(lt_le_trans ltr01 _)// mul1r. *) +(* case p=> //=t. *) +(* by rewrite lee_fin=> t1 ? _ _; rewrite !gt0_mulye ?gt0_muley// lte_fin ?invr_gt0 (lt_le_trans ltr01). *) +(* move: h p1 q1 pleq f. *) +(* case p=> //=[t|]; case q=> //[r|]. *) +(* case=>[|x rtx t1 q1 tr f]; first by rewrite ltey. *) +(* (* hoelder *) admit. *) +(* rewrite !lee_fin => /[swap] t1 []. _ q1 _ f. *) +(* rewrite unlock /Lnorm. *) +(* move=> r[]. *) +(* case p => //=[t|]. => //=[r p1 r1 rle1 _|]. *) +(* rewrite muleCA -EFinM. divff ?(gt_eqF (lt_le_trans ltr01 _))//. *) +(* split; first by rewrite mule1. *) +(* move: r1 p1 rle1; case p => /=[t||]; rewrite !lee_fin. *) +(* - by move=> r1 t1 tr; rewrite ler_pdivlMr ?mul1r ?(lt_le_trans ltr01). *) +(* - by move=> r1 ? rfin; rewrite gt0_mulye// lte_fin invr_gt0 (lt_le_trans ltr01). *) +(* by rewrite leeNy_eq => _ /eqP. *) +(* move=> p1 ?. rewrite !invr0 !mule0. leye_eq => /eqP -> _. rewrite invr0 !mule0//. case. *) +Admitted. End Lspace_inclusion. -*) diff --git a/theories/measure.v b/theories/measure.v index f04f0eaa0..39232bb53 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -5366,4 +5366,45 @@ 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 : T -> R) : ess_sup (normr \o f) = 0 -> f = 0%R %[ae mu]. +Admitted. + End essential_supremum. From d975e870b5d10d52c3020e22842a9c244ec56f3d Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 8 Feb 2025 19:02:18 +0100 Subject: [PATCH 29/33] inclusion of lp spaces --- theories/lspace.v | 103 ++++++++++++++++++++++++---------------------- 1 file changed, 54 insertions(+), 49 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index 6dfe7a6db..a68800366 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -328,15 +328,6 @@ Proof. by rewrite /nm fineK// fin_numElt (lt_le_trans ltNy0) ?Lnorm_ge0//=; exact: lfuny. Qed. -(* 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 ler_Lnorm_add (f g : ty) : nm (f + g) <= nm f + nm g. Proof. by rewrite -lee_fin EFinD !finite_norm_fine minkowskie. Qed. @@ -367,13 +358,10 @@ HB.instance Definition _ := (* todo: add equivalent of mx_normZ and HB instance *) - -(* TODO: move to hoelder *) - Lemma nm_eq0 (f : ty) : nm f = 0 -> f = 0 %[ae mu]. Proof. rewrite /nm=> /eqP; rewrite -eqe=> /eqP; rewrite finite_norm_fine=> /Lnorm_eq0_eq0. -by apply; rewrite (lt_le_trans _ p1). +by apply; rewrite ?(lt_le_trans _ p1). Qed. @@ -383,43 +371,60 @@ Section Lspace_inclusion. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. +Lemma foo (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. + Lemma Lspace_inclusion (p q : R) (p1 : 1 <= p) (q1 : (1 <= q%:E)%E) : - (p <= q) -> forall (f : LfunType mu q1), finite_norm mu (p%:E) f. + (0 < mu [set: T] < +oo)%E -> (p < q) -> forall (f : LfunType mu q1), finite_norm mu (p%:E) f. Proof. -(* move=> pleq f. *) -(* have := lfuny q1 f. *) -(* rewrite /finite_norm. *) -(* pose r := [get x : R | p = q * x] : R. *) -(* pose r' := [get x : R | r^-1 + x^-1 = 1] : R. *) -(* have := (@hoelder _ _ _ mu (fun x => `|f x| `^ p) (cst 1)%R r r'). *) -(* rewrite (_ : ((fun x : T => `|f x| `^ p) \* cst 1)%R = (fun x : T => `|f x| `^ p)); last first. *) -(* by rewrite -fctM mulr1. *) - -(* have /=r := conjugate q. *) -(* have h : forall h : p < +oo, exists r, q = p * r /\ 1 <= r. *) -(* exists (q * ((fine p)^-1)%:E). *) -(* move: p1 q1 pleq f h. *) -(* case q=> //[r|]. *) -(* case p=> //=t t1 r1. *) -(* rewrite -!EFinM -mulrCA divff ?(gt_eqF (lt_le_trans ltr01 _))// mulr1 !lee_fin. *) -(* by move=> tr _; rewrite ler_pdivlMr ?(lt_le_trans ltr01 _)// mul1r. *) -(* case p=> //=t. *) -(* by rewrite lee_fin=> t1 ? _ _; rewrite !gt0_mulye ?gt0_muley// lte_fin ?invr_gt0 (lt_le_trans ltr01). *) -(* move: h p1 q1 pleq f. *) -(* case p=> //=[t|]; case q=> //[r|]. *) -(* case=>[|x rtx t1 q1 tr f]; first by rewrite ltey. *) -(* (* hoelder *) admit. *) -(* rewrite !lee_fin => /[swap] t1 []. _ q1 _ f. *) -(* rewrite unlock /Lnorm. *) -(* move=> r[]. *) -(* case p => //=[t|]. => //=[r p1 r1 rle1 _|]. *) -(* rewrite muleCA -EFinM. divff ?(gt_eqF (lt_le_trans ltr01 _))//. *) -(* split; first by rewrite mule1. *) -(* move: r1 p1 rle1; case p => /=[t||]; rewrite !lee_fin. *) -(* - by move=> r1 t1 tr; rewrite ler_pdivlMr ?mul1r ?(lt_le_trans ltr01). *) -(* - by move=> r1 ? rfin; rewrite gt0_mulye// lte_fin invr_gt0 (lt_le_trans ltr01). *) -(* by rewrite leeNy_eq => _ /eqP. *) -(* move=> p1 ?. rewrite !invr0 !mule0. leye_eq => /eqP -> _. rewrite invr0 !mule0//. case. *) -Admitted. +move=> /andP[mu_pos mu_fin] pleq f. +have := lfuny q1 f. +rewrite /finite_norm. +have p0 : 0 < p by rewrite ?(lt_le_trans ltr01). +have q0 : 0 < q by rewrite ?(lt_le_trans ltr01). +have qinv0 : q^-1 != 0 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'). +rewrite (_ : (_ \* cst 1)%R = (fun x : T => `|f x| `^ p)) -?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 <= _)%E] eq_integral => x _ do + rewrite powRr1// norm_powR// normrE. +under [X in (X`^ r^-1 * mu _ `^_)%E]eq_integral => x _ do + rewrite /r norm_powR normrE ?powR_ge0// -powRrM mulrCA mulfV ?mulr1// ?gt_eqF//. +rewrite [X in (X <= _)%E]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)//. + 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 := lfuny q1 f. +rewrite /finite_norm unlock/Lnorm ifF//. +by apply/eqP => q0'; rewrite q0' ltxx in q0. +Qed. End Lspace_inclusion. From 1ead98125ccacb7d228c174fb38df12598e408d0 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 8 Feb 2025 19:39:07 +0100 Subject: [PATCH 30/33] extension to Loo --- theories/lspace.v | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index a68800366..d17e0ad5d 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -382,9 +382,23 @@ case: ifP => //. by move: rgt0 => /[swap] /eqP -> /eqP; rewrite ltxx. case: ifP => //. by rewrite rgt0. Qed. -Lemma Lspace_inclusion (p q : R) (p1 : 1 <= p) (q1 : (1 <= q%:E)%E) : - (0 < mu [set: T] < +oo)%E -> (p < q) -> forall (f : LfunType mu q1), finite_norm mu (p%:E) f. +Lemma Lspace_inclusion (p q : \bar R) (p1 : (1 <= p)%E) (q1 : (1 <= q)%E) : + (0 < mu [set: T] < +oo)%E -> (p < q) %E-> forall (f : LfunType mu q1), finite_norm mu p f. Proof. +move: p q p1 q1. +case=> //[p|]; case=> //[q|] p1 q1; last first. + move=> /andP[mu0 muoo] _ f. + have p0 : 0 < p by rewrite ?(lt_le_trans ltr01). + rewrite /finite_norm unlock /Lnorm gt_eqF//. + rewrite poweR_lty//. + apply: integral_fune_lt_pinfty => //. + apply: measurable_bounded_integrable => //. + rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)//. + apply: measurableT_comp => //=. + exact: measurableT_comp. + rewrite boundedE. + near=> A. + admit. move=> /andP[mu_pos mu_fin] pleq f. have := lfuny q1 f. rewrite /finite_norm. @@ -425,6 +439,6 @@ rewrite poweR_lty// (lty_poweRy qinv0)//. have := lfuny q1 f. rewrite /finite_norm unlock/Lnorm ifF//. by apply/eqP => q0'; rewrite q0' ltxx in q0. -Qed. +Admitted. End Lspace_inclusion. From 75d27c69a460f7d889c8ebdcc8de5879c5f7752a Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 8 Feb 2025 19:55:22 +0100 Subject: [PATCH 31/33] wip --- theories/lspace.v | 43 ++++++++++++++++++++++++------------------- 1 file changed, 24 insertions(+), 19 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index d17e0ad5d..ebf09c60f 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -371,7 +371,8 @@ Section Lspace_inclusion. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. -Lemma foo (x y : \bar R) : (x \is a fin_num -> 0 < x -> x * y < +oo -> y < +oo)%E. +(* 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. @@ -382,50 +383,54 @@ case: ifP => //. by move: rgt0 => /[swap] /eqP -> /eqP; rewrite ltxx. case: ifP => //. by rewrite rgt0. Qed. -Lemma Lspace_inclusion (p q : \bar R) (p1 : (1 <= p)%E) (q1 : (1 <= q)%E) : - (0 < mu [set: T] < +oo)%E -> (p < q) %E-> forall (f : LfunType mu q1), finite_norm mu p f. +Local Open Scope ereal_scope. + +Lemma Lspace_inclusion (p q : \bar R) : + forall (p1 : 1 <= p) (q1 : 1 <= q), + 0 < mu [set: T] < +oo -> p < q -> forall (f : LfunType mu q1), finite_norm mu p f. Proof. -move: p q p1 q1. +move: p q. case=> //[p|]; case=> //[q|] p1 q1; last first. move=> /andP[mu0 muoo] _ f. - have p0 : 0 < p by rewrite ?(lt_le_trans ltr01). - rewrite /finite_norm unlock /Lnorm gt_eqF//. - rewrite poweR_lty//. - apply: integral_fune_lt_pinfty => //. + have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). + have := lfuny _ f. + rewrite /finite_norm unlock /Lnorm mu0 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)//. + 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. + near=> A=> x/= _. + rewrite norm_powR// normr_id normr1 mulr1. admit. move=> /andP[mu_pos mu_fin] pleq f. have := lfuny q1 f. rewrite /finite_norm. -have p0 : 0 < p by rewrite ?(lt_le_trans ltr01). -have q0 : 0 < q by rewrite ?(lt_le_trans ltr01). -have qinv0 : q^-1 != 0 by rewrite invr_neq0// gt_eqF. +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'). -rewrite (_ : (_ \* cst 1)%R = (fun x : T => `|f x| `^ p)) -?fctM ?mulr1//. +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 <= _)%E] eq_integral => x _ do +under [X in X `^ 1 <= _] eq_integral => x _ do rewrite powRr1// norm_powR// normrE. -under [X in (X`^ r^-1 * mu _ `^_)%E]eq_integral => x _ do +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 <= _)%E]poweRe1; last +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)//. + - rewrite (_ : (fun x : T => `|f x| `^ p) = (@powR R)^~ p \o normr \o f)%R//. apply: measurableT_comp => //=. exact: measurableT_comp => //=. - exact: measurable_cst. From 8e6602aa8a5b2d13cde6148a6a6e3c5148c27480 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 8 Feb 2025 20:35:57 +0100 Subject: [PATCH 32/33] wip --- .nix/config.nix | 6 +++--- theories/lspace.v | 9 +++++++-- theories/measure.v | 6 +++++- 3 files changed, 15 insertions(+), 6 deletions(-) diff --git a/.nix/config.nix b/.nix/config.nix index e43c0ede7..3431ddf46 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -50,14 +50,14 @@ 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"; }; bundles."8.20".coqPackages = common-bundle // { coq.override.version = "8.20"; - mathcomp.override.version = "CohenCyril:seminorm"; + mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "master"; mathcomp-finmap.override.version = "master"; ssprove.job = false; @@ -69,7 +69,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/lspace.v b/theories/lspace.v index ebf09c60f..f0bb58a77 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -285,9 +285,14 @@ case=> //[r 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. admit. +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. -Admitted. +Unshelve. end_near. +Qed. Lemma lfun_submod_closed : submod_closed (lfun). Proof. diff --git a/theories/measure.v b/theories/measure.v index 39232bb53..11178680d 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -5404,7 +5404,11 @@ 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 : T -> R) : ess_sup (normr \o f) = 0 -> f = 0%R %[ae mu]. +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 905866b316ba2d5c654be768a11094d3e14afefa Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sat, 8 Feb 2025 21:28:39 +0100 Subject: [PATCH 33/33] measure 0 --- theories/lspace.v | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/theories/lspace.v b/theories/lspace.v index f0bb58a77..60a3b887c 100644 --- a/theories/lspace.v +++ b/theories/lspace.v @@ -390,16 +390,24 @@ Qed. Local Open Scope ereal_scope. +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), - 0 < mu [set: T] < +oo -> p < q -> forall (f : LfunType mu q1), 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]. + 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. - move=> /andP[mu0 muoo] _ f. have p0 : (0 < p)%R by rewrite ?(lt_le_trans ltr01). - have := lfuny _ f. - rewrite /finite_norm unlock /Lnorm mu0 gt_eqF// => supf_lty. + 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//. @@ -409,9 +417,8 @@ case=> //[p|]; case=> //[q|] p1 q1; last first. near=> A=> x/= _. rewrite norm_powR// normr_id normr1 mulr1. admit. -move=> /andP[mu_pos mu_fin] pleq f. -have := lfuny q1 f. -rewrite /finite_norm. +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. @@ -446,8 +453,7 @@ apply: le_lt_trans. 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 := lfuny q1 f. -rewrite /finite_norm unlock/Lnorm ifF//. +have:= ffin; rewrite /finite_norm unlock/Lnorm ifF//. by apply/eqP => q0'; rewrite q0' ltxx in q0. Admitted.