diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2601523135..f8a7569aeb 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -56,6 +56,7 @@ `nbhs_one_point_compactification_weakE`, `locally_compact_completely_regular`, and `completely_regular_regular`. + + new lemmas `near_in_itvoy`, `near_in_itvNyo` - in file `mathcomp_extra.v`, + new definition `sigT_fun`. @@ -87,11 +88,76 @@ `wedge_compact`, `wedge_connected`. - in `boolp.`: - + lemma `existT_inj` + + lemma `existT_inj2` - in file `order_topology.v` + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and `max_fun_continuous`. +- in file `boolp.v`, + + new lemmas `uncurryK`, and `curryK` +- in file `weak_topology.v`, + + new lemma `continuous_comp_weak` +- in file `function_spaces.v`, + + new definition `eval` + + new lemmas `continuous_curry_fun`, `continuous_curry_cvg`, + `eval_continuous`, and `compose_continuous` + +- in file `wedge_sigT.v`, ++ new definitions `wedge_fun`, and `wedge_prod`. ++ new lemmas `wedge_fun_continuous`, `wedge_lift_funE`, + `wedge_fun_comp`, `wedge_prod_pointE`, `wedge_prod_inj`, + `wedge_prod_continuous`, `wedge_prod_open`, `wedge_hausdorff`, and + `wedge_fun_joint_continuous`. + +- in `boolp.v`: + + lemmas `existT_inj1`, `surjective_existT` + +- in file `homotopy_theory/path.v`, + + new definitions `reparameterize`, `mk_path`, and `chain_path`. + + new lemmas `path_eqP`, and `chain_path_cts_point`. +- in file `homotopy_theory/wedge_sigT.v`, + + new definition `bpwedge_shared_pt`. + + new notations `bpwedge`, and `bpwedge_lift`. +- in `constructive_ereal.v`: + + notation `\prod_( i <- r | P ) F` for extended real numbers and its variants + +- in `numfun.v`: + + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` + + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`, + `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`, + `le0_funrposM`, `le0_funrnegM`, `funr_normr`, `funrposneg`, `funrD_Dpos`, + `funrD_posD`, `funrpos_le`, `funrneg_le` + + lemmas `funerpos`, `funerneg` + +- in `measure.v`: + + lemma `preimage_class_comp` + + defintions `mapping_display`, `g_sigma_algebra_mappingType`, `g_sigma_algebra_mapping`, + notations `.-mapping`, `.-mapping.-measurable` + +- in `lebesgue_measure.v`: + + lemma `measurable_indicP` + + lemmas `measurable_funrpos`, `measurable_funrneg` + +- in `lebesgue_integral.v`: + + definition `approx_A` (was `Let A`) + + definition `approx_B` (was `Let B`) + + lemma `measurable_fun_sum` + + lemma `integrable_indic` + +- in `probability.v`: + + lemma `expectationM_ge0` + + definition `independent_events` + + definition `mutual_independence` + + definition `independent_RVs` + + definition `independent_RVs2` + + lemmas `g_sigma_algebra_mapping_comp`, `g_sigma_algebra_mapping_funrpos`, + `g_sigma_algebra_mapping_funrneg` + + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`, + `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`, + `independent_RVs2_funrpospos` + + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`, + ` expectation_prod` + ### Changed - in file `normedtype.v`, @@ -143,10 +209,48 @@ `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`, `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`. +- in `tvs.v`: + + HB structures `NbhsNmodule`, `NbhsZmodule`, `NbhsLmodule`, `TopologicalNmodule`, + `TopologicalZmodule` + + notation `topologicalLmoduleType`, HB structure `TopologicalLmodule` + + HB structures `UniformZmodule`, `UniformLmodule` + + definition `convex` + + mixin `Uniform_isTvs` + + type `tvsType`, HB.structure `Tvs` + + HB.factory `TopologicalLmod_isTvs` + + lemma `nbhs0N` + + lemma `nbhsN` + + lemma `nbhsT` + + lemma `nbhsB` + + lemma `nbhs0Z` + + lemma `nbhZ` + +- in `lebesgue_integrale.v` + + change implicits of `measurable_funP` + ### Changed +- in normedtype.v + + HB structure `normedModule` now depends on a Tvs + instead of a Lmodule + + Factory `PseudoMetricNormedZmod_Lmodule_isNormedModule` becomes + `PseudoMetricNormedZmod_Tvs_isNormedModule` + + Section `prod_NormedModule` now depends on a `numFieldType` + ### Renamed +- in `normedtype.v`: + + `near_in_itv` -> `near_in_itvoo` + +- in normedtype.v + + Section `regular_topology` to `standard_topology` + +- in `lebesgue_measure.v`: + + `measurable_fun_indic` -> `measurable_indic` + +- in `probability.v`: + + `expectationM` -> `expectationMl` + ### Generalized - in `lebesgue_integral.v`: @@ -161,6 +265,9 @@ - in `topology_structure.v`: + lemma `closureC` +- in file `lebesgue_integral.v`: + + lemma `approximation` + ### Removed - in `lebesgue_integral.v`: @@ -175,6 +282,10 @@ + lemma `cst_nnfun_subproof` (turned into a `Let`) + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead) +- in `lebesgue_integral.v`: + + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) + + notation `measurable_fun_indic` (deprecation since 0.6.3) + ### Infrastructure ### Misc diff --git a/_CoqProject b/_CoqProject index e36c71dae4..8825741850 100644 --- a/_CoqProject +++ b/_CoqProject @@ -63,11 +63,13 @@ theories/topology_theory/sigT_topology.v theories/homotopy_theory/homotopy.v theories/homotopy_theory/wedge_sigT.v +theories/homotopy_theory/path.v theories/separation_axioms.v theories/function_spaces.v theories/ereal.v theories/cantor.v +theories/tvs.v theories/normedtype.v theories/realfun.v theories/sequences.v diff --git a/classical/boolp.v b/classical/boolp.v index 07b4c2e097..f1ece5aa2b 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -88,13 +88,21 @@ move=> PQA; suff: {x | P x /\ Q x} by move=> [a [*]]; exists a. by apply: cid; case: PQA => x; exists x. Qed. -Lemma existT_inj (A : eqType) (P : A -> Type) (p : A) (x y : P p) : - existT P p x = existT P p y -> x = y. +Lemma existT_inj1 (T : Type) (P : T -> Type) (x y : T) (Px : P x) (Py : P y) : + existT P x Px = existT P y Py -> x = y. +Proof. by case. Qed. + +Lemma existT_inj2 (T : eqType) (P : T -> Type) (x : T) (Px1 Px2 : P x) : + existT P x Px1 = existT P x Px2 -> Px1 = Px2. Proof. -apply: Eqdep_dec.inj_pair2_eq_dec => a b. -by have [|/eqP] := eqVneq a b; [left|right]. +apply: Eqdep_dec.inj_pair2_eq_dec => y z. +by have [|/eqP] := eqVneq y z; [left|right]. Qed. +Lemma surjective_existT (T : Type) (P : T -> Type) (p : {x : T & P x}): + existT [eta P] (projT1 p) (projT2 p) = p. +Proof. by case: p. Qed. + Record mextensionality := { _ : forall (P Q : Prop), (P <-> Q) -> (P = Q); _ : forall {T U : Type} (f g : T -> U), @@ -969,3 +977,9 @@ Lemma inhabited_witness: inhabited T -> T. Proof. by rewrite inhabitedE => /cid[]. Qed. End Inhabited. + +Lemma uncurryK {X Y Z : Type} : cancel (@uncurry X Y Z) curry. +Proof. by move=> f; rewrite funeq2E. Qed. + +Lemma curryK {X Y Z : Type} : cancel curry (@uncurry X Y Z). +Proof. by move=> f; rewrite funeqE=> -[]. Qed. diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 8c5acd53b7..b773f279de 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -2485,6 +2485,16 @@ Proof. by apply/eqP => /seteqP[] /(_ point) /(_ Logic.I). Qed. End PointedTheory. +HB.mixin Record isBiPointed (X : Type) of Equality X := { + zero : X; + one : X; + zero_one_neq : zero != one; +}. + +#[short(type="biPointedType")] +HB.structure Definition BiPointed := + { X of Choice X & isBiPointed X }. + Variant squashed T : Prop := squash (x : T). Arguments squash {T} x. Notation "$| T |" := (squashed T) : form_scope. diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index a2155ef0e1..27875e3f19 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -551,6 +551,31 @@ Notation "\sum_ ( i 'in' A ) F" := Notation "\sum_ ( i 'in' A ) F" := (\big[+%E/0%E]_(i in A) F%E) : ereal_scope. +Notation "\prod_ ( i <- r | P ) F" := + (\big[*%E/1%:E]_(i <- r | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i <- r ) F" := + (\big[*%E/1%:E]_(i <- r) F%E) : ereal_scope. +Notation "\prod_ ( m <= i < n | P ) F" := + (\big[*%E/1%:E]_(m <= i < n | P%B) F%E) : ereal_scope. +Notation "\prod_ ( m <= i < n ) F" := + (\big[*%E/1%:E]_(m <= i < n) F%E) : ereal_scope. +Notation "\prod_ ( i | P ) F" := + (\big[*%E/1%:E]_(i | P%B) F%E) : ereal_scope. +Notation "\prod_ i F" := + (\big[*%E/1%:E]_i F%E) : ereal_scope. +Notation "\prod_ ( i : t | P ) F" := + (\big[*%E/1%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope. +Notation "\prod_ ( i : t ) F" := + (\big[*%E/1%:E]_(i : t) F%E) (only parsing) : ereal_scope. +Notation "\prod_ ( i < n | P ) F" := + (\big[*%E/1%:E]_(i < n | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i < n ) F" := + (\big[*%E/1%:E]_(i < n) F%E) : ereal_scope. +Notation "\prod_ ( i 'in' A | P ) F" := + (\big[*%E/1%:E]_(i in A | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i 'in' A ) F" := + (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope. + Section ERealOrderTheory. Context {R : numDomainType}. Implicit Types x y z : \bar R. diff --git a/theories/Make b/theories/Make index 0d77fa421b..d82042d37c 100644 --- a/theories/Make +++ b/theories/Make @@ -31,10 +31,12 @@ topology_theory/sigT_topology.v homotopy_theory/homotopy.v homotopy_theory/wedge_sigT.v +homotopy_theory/path.v separation_axioms.v function_spaces.v cantor.v +tvs.v normedtype.v realfun.v sequences.v diff --git a/theories/charge.v b/theories/charge.v index 498cc2228d..1cb0670df5 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -92,7 +92,7 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Import numFieldTopology.Exports. +Import numFieldNormedType.Exports. Local Open Scope ring_scope. Local Open Scope classical_set_scope. @@ -1921,29 +1921,29 @@ Lemma change_of_variables f E : (forall x, 0 <= f x) -> \int[mu]_(x in E) (f x * ('d nu '/d mu) x) = \int[nu]_(x in E) f x. Proof. move=> f0 mE mf; set g := 'd nu '/d mu. -have [h [ndh hf]] := approximation mE mf (fun x _ => f0 x). +pose h := nnsfun_approx mE mf. have -> : \int[nu]_(x in E) f x = lim (\int[nu]_(x in E) (EFin \o h n) x @[n --> \oo]). have fE x : E x -> f x = lim ((EFin \o h n) x @[n --> \oo]). - by move=> Ex; apply/esym/cvg_lim => //; exact: hf. + by move=> Ex; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. under eq_integral => x /[!inE] /fE -> //. apply: monotone_convergence => //. - move=> n; apply/measurable_EFinP. by apply: (measurable_funS measurableT) => //; exact/measurable_funP. - by move=> n x Ex //=; rewrite lee_fin. - - by move=> x Ex a b /ndh /=; rewrite lee_fin => /lefP. + - by move=> x Ex a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. have -> : \int[mu]_(x in E) (f \* g) x = lim (\int[mu]_(x in E) ((EFin \o h n) \* g) x @[n --> \oo]). have fg x :E x -> f x * g x = lim (((EFin \o h n) \* g) x @[n --> \oo]). by move=> Ex; apply/esym/cvg_lim => //; apply: cvgeMr; - [exact: f_fin_num|exact: hf]. + [exact: f_fin_num|exact: cvg_nnsfun_approx]. under eq_integral => x /[!inE] /fg -> //. apply: monotone_convergence => [//| | |]. - move=> n; apply/emeasurable_funM; apply/measurable_funTS. exact/measurable_EFinP. exact: measurable_int (f_integrable _). - by move=> n x Ex //=; rewrite mule_ge0 ?lee_fin//=; exact: f_ge0. - - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0. + - by move=> x Ex a b ab/=; rewrite lee_wpmul2r ?lee_fin ?f_ge0//; exact/lefP/nd_nnsfun_approx. suff suf n : \int[mu]_(x in E) ((EFin \o h n) x * g x) = \int[nu]_(x in E) (EFin \o h n) x. by under eq_fun do rewrite suf. @@ -2008,7 +2008,7 @@ Proof. move=> numu mula mE; have nula := measure_dominates_trans numu mula. have mf : measurable_fun E ('d nu '/d mu). exact/measurable_funTS/(measurable_int _ (f_integrable _)). -have [h [ndh hf]] := approximation mE mf (fun x _ => f_ge0 numu x). +pose h := approximation mE mf. apply: integral_ae_eq => //. - apply: (integrableS measurableT) => //. apply: f_integrable. @@ -2018,7 +2018,7 @@ apply: integral_ae_eq => //. - move=> A AE mA; rewrite change_of_variables//. + by rewrite -!f_integral. + exact: f_ge0. - + exact: measurable_funS mf. + + by move: (mf); exact: measurable_funS. Qed. End chain_rule. diff --git a/theories/derive.v b/theories/derive.v index 2cd1198f76..da703d8d16 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -2,8 +2,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import reals signed topology prodnormedzmodule normedtype. -From mathcomp Require Import landau forms. +From mathcomp Require Import reals signed topology prodnormedzmodule tvs. +From mathcomp Require Import normedtype landau forms. (**md**************************************************************************) (* # Differentiation *) @@ -788,13 +788,14 @@ by rewrite prod_normE/= !normrZ !normfV !normr_id !mulVf ?gt_eqF// maxxx ltr1n. Qed. Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) : - continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ 0 id. + continuous (fun p => f p.1 p.2) -> (fun p => f p.1 p.2) =o_ (0 : U * V') id. Proof. move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc. apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//. rewrite ler_pM ?pmulr_rge0 //; last by rewrite num_le_max /= lexx orbT. rewrite -ler_pdivlMl //. -suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite num_le_max /= lexx. +suff : `|x| <= k%:num ^-1 * e%:num. + by apply: le_trans; rewrite num_le_max /= lexx. near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm. by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite /= distrC subr0 => /ltW. Unshelve. all: by end_near. Qed. @@ -803,7 +804,7 @@ Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p : continuous (fun p => f p.1 p.2) -> continuous (fun q => (f p.1 q.2 + f q.1 p.2)) /\ (fun q => f q.1 q.2) \o shift p = cst (f p.1 p.2) + - (fun q => f p.1 q.2 + f q.1 p.2) +o_ 0 id. + (fun q => f p.1 q.2 + f q.1 p.2) +o_ (0 : U * V') id. Proof. move=> fc; split=> [q|]. by apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2)); diff --git a/theories/exp.v b/theories/exp.v index 2e2d30497c..cb7d2b8b7a 100644 --- a/theories/exp.v +++ b/theories/exp.v @@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import mathcomp_extra reals ereal signed. -From mathcomp Require Import topology normedtype landau sequences derive. +From mathcomp Require Import topology tvs normedtype landau sequences derive. From mathcomp Require Import realfun itv convex. (**md**************************************************************************) @@ -228,7 +228,7 @@ suff Cc : limn (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> limn (series s). apply: cvg_zero => /=. suff Cc : limn (series (fun n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1))) - @[h --> 0^'] --> (0 : R). + @[h --> 0^'] --> 0. apply: cvg_sub0 Cc. apply/cvgrPdist_lt => eps eps_gt0 /=. near=> h; rewrite sub0r normrN /=. diff --git a/theories/ftc.v b/theories/ftc.v index 4f553f2c11..bbc908701b 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop signed reals ereal. -From mathcomp Require Import topology normedtype sequences real_interval. +From mathcomp Require Import topology tvs normedtype sequences real_interval. From mathcomp Require Import esum measure lebesgue_measure numfun realfun. From mathcomp Require Import lebesgue_integral derive charge. @@ -24,7 +24,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Import numFieldTopology.Exports. +Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -358,7 +358,7 @@ Proof. move=> ab intf; pose fab := f \_ `[a, b]. have intfab : mu.-integrable `[a, b] (EFin \o fab). by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr. -apply/cvgrPdist_le => /= e e0; rewrite near_simpl; near=> x. +apply/cvgrPdist_le => /= e e0; near=> x. rewrite {1}/int /parameterized_integral sub0r normrN. have [|xa] := leP a x. move=> ax; apply/ltW; move: ax. @@ -423,7 +423,6 @@ have intfab : mu.-integrable `[a, b] (EFin \o fab). by rewrite -restrict_EFin; apply/integrable_restrict => //=; rewrite setIidr. rewrite /int /parameterized_integral => z; rewrite in_itv/= => /andP[az zb]. apply/cvgrPdist_le => /= e e0. -rewrite near_simpl. have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0. near=> x. have [xz|xz|->] := ltgtP x z; last by rewrite subrr normr0 ltW. @@ -501,7 +500,7 @@ Corollary continuous_FTC2 f F a b : (a < b)%R -> Proof. move=> ab cf dF F'f. pose fab := f \_ `[a, b]. -pose G x : R := (\int[mu]_(t in `[a, x]) fab t)%R. +pose G x := (\int[mu]_(t in `[a, x]) fab t)%R. have iabf : mu.-integrable `[a, b] (EFin \o f). by apply: continuous_compact_integrable => //; exact: segment_compact. have G'f : {in `]a, b[, forall x, G^`() x = fab x /\ derivable G x 1}. @@ -730,7 +729,7 @@ Lemma increasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R -> Proof. move=> ab incrF cFb GFb. apply/cvgrPdist_le => /= e e0. -have/cvgrPdist_le /(_ e e0) [d /= d0 {}GFb] := GFb. +have /cvgrPdist_le /(_ e e0) [d /= d0 {}GFb] := GFb. have := cvg_at_left_within cFb. move/cvgrPdist_lt/(_ _ d0) => [d' /= d'0 {}cFb]. near=> t. @@ -748,7 +747,7 @@ Lemma decreasing_cvg_at_right_comp F G a b (l : R) : (a < b)%R -> Proof. move=> ab decrF cFa GFa. apply/cvgrPdist_le => /= e e0. -have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFa] := GFa. +have /cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFa] := GFa. have := cvg_at_right_within cFa. move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFa]. near=> t. @@ -766,7 +765,7 @@ Lemma decreasing_cvg_at_left_comp F G a b (l : R) : (a < b)%R -> Proof. move=> ab decrF cFb GFb. apply/cvgrPdist_le => /= e e0. -have/cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFb] := GFb. +have /cvgrPdist_le /(_ e e0) [d' /= d'0 {}GFb] := GFb. have := cvg_at_left_within cFb. (* different point from gt0 version *) move/cvgrPdist_lt/(_ _ d'0) => [d'' /= d''0 {}cFb]. near=> t. @@ -863,7 +862,7 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first. exact: decreasing_image_oo. * have : -%R F^`() @ x --> (- f x)%R. by rewrite -fE//; apply: cvgN; exact: cF'. - apply: cvg_trans; apply: near_eq_cvg; rewrite near_simpl. + apply: cvg_trans; apply: near_eq_cvg. apply: (@open_in_nearW _ _ `]a, b[) ; last by rewrite inE. exact: interval_open. by move=> z; rewrite inE/= => zab; rewrite fctE fE. @@ -978,8 +977,8 @@ rewrite (@integration_by_substitution_decreasing (- F)%R); first last. by case: Fab => + _ _; exact. rewrite -derive1E. have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg. - rewrite near_simpl; near=> y; rewrite fctE !derive1E deriveN//. - by case: Fab => + _ _; apply; near: y; exact: near_in_itv. + near=> y; rewrite fctE !derive1E deriveN//. + by case: Fab => + _ _; apply; near: y; exact: near_in_itvoo. - by move=> x y xab yab yx; rewrite ltrN2 incrF. - by []. have mGF : measurable_fun `]a, b[ (G \o F). diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 628142d6a6..cc56990f6e 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -70,6 +70,7 @@ From mathcomp Require Import reals signed topology separation_axioms. (* {family fam, F --> f} == F converges to f in {family fam, U -> V} *) (* {compact_open, U -> V} == compact-open topology *) (* {compact_open, F --> f} == F converges to f in {compact_open, U -> V} *) +(* eval == the evaluation map for continuous functions *) (* ``` *) (* *) (* ## Ascoli's theorem notations *) @@ -1436,6 +1437,17 @@ move=> v Kv; have [[P Q] [Px Qv] PQfO] : nbhs (x, v) (f @^-1` O). by exists (Q, P) => // -[b a] /= [Qb Pa] Kb; exact: PQfO. Unshelve. all: by end_near. Qed. +Lemma continuous_curry_fun (f : U * V -> W) : + continuous f -> continuous (curry f). +Proof. by case/continuous_curry. Qed. + +Lemma continuous_curry_cvg (f : U * V -> W) (u : U) (v : V) : + continuous f -> curry f z.1 z.2 @[z --> (u, v)] --> curry f u v. +Proof. +move=> cf D /cf; rewrite !nbhs_simpl /curry /=; apply: filterS => z ? /=. +by rewrite -surjective_pairing. +Qed. + Lemma continuous_uncurry_regular (f : U -> V -> W) : locally_compact [set: V] -> @regular_space V -> continuous f -> (forall u, continuous (f u)) -> continuous (uncurry f). @@ -1544,3 +1556,46 @@ Unshelve. all: by end_near. Qed. End cartesian_closed. End currying. + +Definition eval {X Y : topologicalType} : continuousType X Y * X -> Y := + uncurry (id : continuousType X Y -> (X -> Y)). + +Section composition. + +Local Import ArrowAsCompactOpen. + +Lemma eval_continuous {X Y : topologicalType} : + locally_compact [set: X] -> regular_space X -> continuous (@eval X Y). +Proof. +move=> lcX rsX; apply: continuous_uncurry_regular => //. + exact: weak_continuous. +by move=> ?; exact: cts_fun. +Qed. + +Lemma compose_continuous {X Y Z : topologicalType} : + locally_compact [set: X] -> @regular_space X -> + locally_compact [set: Y] -> @regular_space Y -> + continuous (uncurry + (comp : continuousType Y Z -> continuousType X Y -> continuousType X Z)). +Proof. +move=> lX rX lY rY; apply: continuous_comp_weak. +set F := _ \o _. +rewrite -[F]uncurryK; apply: continuous_curry_fun. +pose g := uncurry F \o prodAr \o swap; rewrite /= in g *. +have -> : uncurry F = uncurry F \o prodAr \o prodA by rewrite funeqE => -[[]]. +move=> z; apply: continuous_comp; first exact: prodA_continuous. +have -> : uncurry F \o prodAr = uncurry F \o prodAr \o swap \o swap. + by rewrite funeqE => -[[]]. +apply: continuous_comp; first exact: swap_continuous. +pose h (fxg : continuousType X Y * X * continuousType Y Z) : Z := + eval (fxg.2, (eval fxg.1)). +have <- : h = uncurry F \o prodAr \o swap. + by rewrite /h/g/uncurry/swap/F funeqE => -[[]]. +rewrite /h. +apply: (@continuous2_cvg _ _ _ _ _ _ snd (eval \o fst) (curry eval)). +- by apply: continuous_curry_cvg; exact: eval_continuous. +- exact: cvg_snd. +- by apply: cvg_comp; [exact: cvg_fst | exact: eval_continuous]. +Qed. + +End composition. diff --git a/theories/homotopy_theory/homotopy.v b/theories/homotopy_theory/homotopy.v index 33e29737be..d424c7b38b 100644 --- a/theories/homotopy_theory/homotopy.v +++ b/theories/homotopy_theory/homotopy.v @@ -1,2 +1,3 @@ (* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Export wedge_sigT. +From mathcomp Require Export path. diff --git a/theories/homotopy_theory/path.v b/theories/homotopy_theory/path.v new file mode 100644 index 0000000000..e11e80938e --- /dev/null +++ b/theories/homotopy_theory/path.v @@ -0,0 +1,181 @@ +(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals signed topology. +From mathcomp Require Import function_spaces wedge_sigT. + +(**md**************************************************************************) +(* # Paths *) +(* Paths from biPointed spaces. *) +(* *) +(* ``` *) +(* mk_path ctsf f0 f1 == constructs a value in `pathType x y` given proofs *) +(* that the endpoints of `f` are `x` and `y` *) +(* reparameterize f phi == the path `f` with a different parameterization *) +(* chain_path f g == the path which follows f, then follows g *) +(* Only makes sense when `f one = g zero`. The *) +(* domain is the wedge of domains of `f` and `g`. *) +(* ``` *) +(* The type `{path i from x to y in T}` is the continuous functions on the *) +(* bipointed space i that go from x to y staying in T. It is endowed with *) +(* - Topology via the compact-open topology *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Reserved Notation "{ 'path' i 'from' x 'to' y }" ( + at level 0, i at level 69, x at level 69, y at level 69, + only parsing, + format "{ 'path' i 'from' x 'to' y }"). +Reserved Notation "{ 'path' i 'from' x 'to' y 'in' T }" ( + at level 0, i at level 69, x at level 69, y at level 69, T at level 69, + format "{ 'path' i 'from' x 'to' y 'in' T }"). + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope quotient_scope. + +HB.mixin Record isPath {i : bpTopologicalType} {T : topologicalType} (x y : T) + (f : i -> T) of isContinuous i T f := { + path_zero : f zero = x; + path_one : f one = y; +}. + +#[short(type="pathType")] +HB.structure Definition Path {i : bpTopologicalType} {T : topologicalType} + (x y : T) := {f of isPath i T x y f & isContinuous i T f}. + +Notation "{ 'path' i 'from' x 'to' y }" := (pathType i x y) : type_scope. +Notation "{ 'path' i 'from' x 'to' y 'in' T }" := + (@pathType i T x y) : type_scope. + +HB.instance Definition _ {i : bpTopologicalType} + {T : topologicalType} (x y : T) := gen_eqMixin {path i from x to y}. +HB.instance Definition _ {i : bpTopologicalType} + {T : topologicalType} (x y : T) := gen_choiceMixin {path i from x to y}. +HB.instance Definition _ {i : bpTopologicalType} + {T : topologicalType} (x y : T) := + Topological.copy {path i from x to y} + (@weak_topology {path i from x to y} {compact-open, i -> T} id). + +Section path_eq. +Context {T : topologicalType} {i : bpTopologicalType} (x y : T). + +Lemma path_eqP (a b : {path i from x to y}) : a = b <-> a =1 b. +Proof. +split=> [->//|]. +move: a b => [/= f [[+ +]]] [/= g [[+ +]]] fgE. +move/funext : fgE => -> /= a1 [b1 c1] a2 [b2 c2]; congr (_ _). +rewrite (Prop_irrelevance a1 a2) (Prop_irrelevance b1 b2). +by rewrite (Prop_irrelevance c1 c2). +Qed. + +End path_eq. + +Section cst_path. +Context {T : topologicalType} {i : bpTopologicalType} (x: T). + +HB.instance Definition _ := @isPath.Build i T x x (cst x) erefl erefl. +End cst_path. + +Section path_domain_path. +Context {i : bpTopologicalType}. +HB.instance Definition _ := @isPath.Build i i zero one idfun erefl erefl. +End path_domain_path. + +Section path_compose. +Context {T U : topologicalType} (i: bpTopologicalType) (x y : T). +Context (f : continuousType T U) (p : {path i from x to y}). + +Local Lemma fp_zero : (f \o p) zero = f x. +Proof. by rewrite /= !path_zero. Qed. + +Local Lemma fp_one : (f \o p) one = f y. +Proof. by rewrite /= !path_one. Qed. + +HB.instance Definition _ := isPath.Build i U (f x) (f y) (f \o p) + fp_zero fp_one. + +End path_compose. + +Section path_reparameterize. +Context {T : topologicalType} (i j: bpTopologicalType) (x y : T). +Context (f : {path i from x to y}) (phi : {path j from zero to one in i}). + +(* we use reparameterize, as opposed to just `\o` because we can simplify the + endpoints. So we don't end up with `f \o p : {path j from f zero to f one}` + but rather `{path j from zero to one}` +*) +Definition reparameterize := f \o phi. + +Local Lemma fphi_zero : reparameterize zero = x. +Proof. by rewrite /reparameterize /= ?path_zero. Qed. + +Local Lemma fphi_one : reparameterize one = y. +Proof. by rewrite /reparameterize /= ?path_one. Qed. + +Local Lemma fphi_cts : continuous reparameterize. +Proof. by move=> ?; apply: continuous_comp; apply: cts_fun. Qed. + +HB.instance Definition _ := isContinuous.Build _ _ reparameterize fphi_cts. + +HB.instance Definition _ := isPath.Build j T x y reparameterize + fphi_zero fphi_one. + +End path_reparameterize. + +Section mk_path. +Context {i : bpTopologicalType} {T : topologicalType}. +Context {x y : T} (f : i -> T) (ctsf : continuous f). +Context (f0 : f zero = x) (f1 : f one = y). + +Definition mk_path : i -> T := let _ := (ctsf, f0, f1) in f. + +HB.instance Definition _ := isContinuous.Build i T mk_path ctsf. +HB.instance Definition _ := @isPath.Build i T x y mk_path f0 f1. +End mk_path. + +Definition chain_path {i j : bpTopologicalType} {T : topologicalType} + (f : i -> T) (g : j -> T) : bpwedge i j -> T := + wedge_fun (fun b => if b return (if b then i else j) -> T then f else g). + +Lemma chain_path_cts_point {i j : bpTopologicalType} {T : topologicalType} + (f : i -> T) (g : j -> T) : + continuous f -> + continuous g -> + f one = g zero -> + continuous (chain_path f g). +Proof. by move=> cf cg fgE; apply: wedge_fun_continuous => // [[]|[] []]. Qed. + +Section chain_path. +Context {T : topologicalType} {i j : bpTopologicalType} (x y z: T). +Context (p : {path i from x to y}) (q : {path j from y to z}). + +Local Lemma chain_path_zero : chain_path p q zero = x. +Proof. +rewrite /chain_path /= wedge_lift_funE ?path_one ?path_zero //. +by case => //= [][] //=; rewrite ?path_one ?path_zero. +Qed. + +Local Lemma chain_path_one : chain_path p q one = z. +Proof. +rewrite /chain_path /= wedge_lift_funE ?path_zero ?path_one //. +by case => //= [][] //=; rewrite ?path_one ?path_zero. +Qed. + +Local Lemma chain_path_cts : continuous (chain_path p q). +Proof. +apply: chain_path_cts_point; [exact: cts_fun..|]. +by rewrite path_zero path_one. +Qed. + +HB.instance Definition _ := @isContinuous.Build _ T (chain_path p q) + chain_path_cts. +HB.instance Definition _ := @isPath.Build _ T x z (chain_path p q) + chain_path_zero chain_path_one. + +End chain_path. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 08625921fd..86822e545b 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -1,10 +1,9 @@ (* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. -From mathcomp Require Import boolp classical_sets functions. -From mathcomp Require Import cardinality mathcomp_extra fsbigop. -From mathcomp Require Import reals signed topology separation_axioms. -Require Import EqdepFacts. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals signed topology. +From mathcomp Require Import separation_axioms function_spaces. (**md**************************************************************************) (* # wedge sum for sigT *) @@ -19,7 +18,18 @@ Require Import EqdepFacts. (* wedge_lift i == the lifting of elements of (X i) into the wedge *) (* pwedge p0 == the wedge of ptopologicalTypes at their designated *) (* point *) +(* wedge_fun f == lifts a family of functions on each component into *) +(* a function on the wedge, when they all agree at the *) +(* wedge point *) +(* wedge_prod == the mapping from the wedge as a quotient of sums to *) +(* the wedge as a subspace of the product topology. *) +(* It's an embedding when the index is finite. *) +(* bpwedge_shared_pt b == the shared point in the bpwedge. Either zero or one *) +(* depending on `b`. *) +(* bpwedge == wedge of two bipointed spaces gluing zero to one *) +(* bpwedge_lift == wedge_lift specialized to the bipointed wedge *) (* ``` *) +(* *) (* The type `wedge p0` is endowed with the structures of: *) (* - topology via `quotient_topology` *) (* - quotient *) @@ -29,6 +39,10 @@ Require Import EqdepFacts. (* - quotient *) (* - pointed *) (* *) +(* The type `bpwedge` is endowed with the structures of: *) +(* - topology via `quotient_topology` *) +(* - quotient *) +(* - bipointed *) (******************************************************************************) Set Implicit Arguments. @@ -108,14 +122,14 @@ have : open (\bigcup_i (@wedge_lift i @` (@wedge_lift i @^-1` U))). rewrite eqEsubset; split => x /=. by move=> Ux; exists i => //; exists x. case=> j _ /= [] y Uy /eqmodP /predU1P[R|]. - have E : j = i by move: R; exact: eq_sigT_fst. - by rewrite -E in x R *; rewrite -(existT_inj R). + have E : j = i by move: R; apply: existT_inj1. + by rewrite -E in x R *; rewrite -(existT_inj2 R). case/andP => /eqP/= + /eqP -> => yj. by rewrite yj (wedge_liftE x y) in Uy. congr open; rewrite eqEsubset; split => /= z. by case=> i _ /= [x] Ux <-. move=> Uz; exists (projT1 (repr z)) => //=. -by exists (projT2 (repr z)); rewrite /wedge_lift /= -sigT_eta reprK. +by exists (projT2 (repr z)); rewrite /wedge_lift /= surjective_existT reprK. Qed. Lemma wedge_point_nbhs i0 : @@ -135,7 +149,7 @@ exists W; split. - apply/wedge_openP => i; rewrite /W; have [+ Vpj _] := projT2 (V_ i). congr (_ _); rewrite eqEsubset; split => z; first by move=> Viz; exists i. case => j _ /= [] w /= svw /eqmodP /predU1P[[E]|]. - by rewrite E in w svw * => R; rewrite -(existT_inj R). + by rewrite E in w svw * => R; rewrite -(existT_inj2 R). by case/andP => /eqP /= _ /eqP ->. - by exists i0 => //=; exists (p0 i0) => //; have [_ + _] := projT2 (V_ i0). - by move=> ? [j _ [x ? <-]]; have [_ _] := projT2 (V_ j); exact. @@ -159,7 +173,7 @@ Qed. Lemma wedgeTE : \bigcup_i (@wedge_lift i) @` setT = [set: wedge]. Proof. rewrite -subTset => z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //. -by exists (projT2 (repr z)) => //; rewrite /wedge_lift/= -sigT_eta. +by exists (projT2 (repr z)) => //; rewrite /wedge_lift/= surjective_existT. Qed. Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> @@ -186,6 +200,179 @@ move=> i ? /=; apply: connected_continuous_connected => //. exact/continuous_subspaceT/wedge_lift_continuous. Qed. +Definition wedge_fun {Z : Type} (f : forall i, X i -> Z) : wedge -> Z := + sigT_fun f \o repr. + +Lemma wedge_fun_continuous {Z : topologicalType} (f : forall i, X i -> Z) : + (forall i, continuous (f i)) -> (forall i j, f i (p0 i) = f j (p0 j)) -> + continuous (wedge_fun f). +Proof. +move=> cf fE; apply: repr_comp_continuous; first exact: sigT_continuous. +move=> a b /eqP/eqmodP /predU1P[-> //|/andP[/eqP + /eqP +]]. +by rewrite /sigT_fun /= => -> ->; exact/eqP. +Qed. + +Lemma wedge_lift_funE {Z : Type} (f : forall i, X i -> Z) i0 (a : X i0): + (forall i j, f i (p0 i) = f j (p0 j)) -> wedge_fun f (wedge_lift a) = f i0 a. +Proof. +move=> fE. +rewrite /wedge_fun/= /sigT_fun /=; case: piP => z /= /eqmodP. +by move/predU1P => [<- //|/andP[/= /eqP -> /eqP ->]]. +Qed. + +Lemma wedge_fun_comp {Z1 Z2 : Type} (h : Z1 -> Z2) (f : forall i, X i -> Z1) : + h \o wedge_fun f = wedge_fun (fun i => h \o f i). +Proof. exact/funext. Qed. + +(* The wedge maps into the product + \bigcup_i [x | x j = p0 j when j != i] + + For the box topology, it's an embedding. But more practically, + since the box and product agree when `I` is finite, + we get that the finite wedge embeds into the finite product. + *) +Section wedge_as_product. + +Definition wedge_prod : wedge -> prod_topology X := wedge_fun (dfwith p0). + +Lemma wedge_prod_pointE (i j : I) : dfwith p0 i (p0 i) = dfwith p0 j (p0 j). +Proof. +apply: functional_extensionality_dep => k /=. +by case: dfwithP => [|*]; case: dfwithP. +Qed. + +Lemma wedge_prod_inj : injective wedge_prod. +Proof. +have dfwithp0 := wedge_prod_pointE. +move=> a b; rewrite -[a](@reprK _ wedge) -[b](@reprK _ wedge). +move Ea : (repr a)=> [i x]; move Eb : (repr b) => [j y]. +rewrite /wedge_prod !wedge_lift_funE//= => dfij; apply/eqmodP/orP. +have [E|E /=] := eqVneq i j. + rewrite -{}E in x y Ea Eb dfij *; left; apply/eqP; congr existT. + have : dfwith p0 i x i = dfwith p0 i y i by rewrite dfij. + by rewrite !dfwithin. +right; apply/andP; split; apply/eqP. +- have : dfwith p0 i x i = dfwith p0 j y i by rewrite dfij. + by rewrite dfwithin => ->; rewrite dfwithout // eq_sym. +- have : dfwith p0 i x j = dfwith p0 j y j by rewrite dfij. + by rewrite dfwithin => <-; rewrite dfwithout. +Qed. + +Lemma wedge_prod_continuous : continuous wedge_prod. +Proof. +apply: wedge_fun_continuous; last exact: wedge_prod_pointE. +exact: dfwith_continuous. +Qed. + +Lemma wedge_prod_open (x : wedge) (A : set wedge) : + finite_set [set: I] -> + (forall i, closed [set p0 i]) -> + nbhs x A -> + @nbhs _ (subspace (range wedge_prod)) (wedge_prod x) (wedge_prod @` A). +Proof. +move=> fsetI clI; case: wedge_nbhs_specP => [//|i0 bcA|i z zNp0 /= wNz]. + pose B_ i : set (subspace (range wedge_prod)) := + proj i @^-1` (@wedge_lift i @^-1` A). + have /finite_fsetP[fI fIE] := fsetI. + have /filterS : (\bigcap_(i in [set` fI]) B_ i) `&` range wedge_prod + `<=` wedge_prod @` A. + move=> _ [] /[swap] [] [z _] <- /= Bwz; exists z => //. + have /Bwz : [set` fI] (projT1 (repr z)) by rewrite -fIE. + congr (A _); rewrite /wedge_lift /= -[RHS]reprK. + apply/eqmodP/orP; left; rewrite /proj /=. + by rewrite /wedge_prod/= /wedge_fun /sigT_fun/= dfwithin surjective_existT. + apply; apply/nbhs_subspace_ex; first by exists (wedge_lift (p0 i0)). + exists (\bigcap_(i in [set` fI]) B_ i); last by rewrite -setIA setIid. + apply: filter_bigI => i _; rewrite /B_; apply: proj_continuous. + have /bcA : [set: I] i by []. + congr (nbhs _ _). + rewrite /proj /wedge_prod wedge_lift_funE; first by case: dfwithP. + exact: wedge_prod_pointE. +rewrite [x in nbhs x _]/wedge_prod /= wedge_lift_funE; first last. + exact: wedge_prod_pointE. +have : wedge_prod @` (A `&` (@wedge_lift i @` ~`[set p0 i])) + `<=` wedge_prod @` A. + by move=> ? [] ? [] + /= [w] wpi => /[swap] <- Aw <-; exists (wedge_lift w). +move/filterS; apply; apply/nbhs_subspace_ex. + exists (wedge_lift z) => //. + by rewrite /wedge_prod wedge_lift_funE //; exact: wedge_prod_pointE. +exists (proj i @^-1` (@wedge_lift i @^-1` + (A `&` (@wedge_lift i @` ~`[set p0 i])))). + apply/ proj_continuous; rewrite /proj dfwithin preimage_setI; apply: filterI. + exact: wNz. + have /filterS := @preimage_image _ _ (@wedge_lift i) (~` [set p0 i]). + by apply; apply: open_nbhs_nbhs; split; [exact: closed_openC|exact/eqP]. +rewrite eqEsubset; split => // prodX; case => /[swap] [][] r _ <- /=. + case => _ /[swap] /wedge_prod_inj -> [+ [e /[swap]]] => /[swap]. + move=> <- Awe eNpi; rewrite /proj /wedge_prod /=. + rewrite wedge_lift_funE; last exact: wedge_prod_pointE. + rewrite dfwithin; split => //; first by split => //; exists e. + exists (wedge_lift e) => //. + by rewrite wedge_lift_funE //; exact: wedge_prod_pointE. +case=> /[swap] [][y] yNpi E Ay. +have [riE|R] := eqVneq i (projT1 (repr r)); last first. + apply: absurd yNpi. + move: E; rewrite /proj/wedge_prod /wedge_fun /=/sigT_fun /=. + rewrite dfwithout //; last by rewrite eq_sym. + by case/eqmodP/orP => [/eqP E|/andP[/= /eqP//]]; exact: (existT_inj2 E). +split; exists (wedge_lift y); [by split; [rewrite E | exists y]| |by []|]. +- congr wedge_prod; rewrite E. + rewrite /proj /wedge_prod /wedge_fun /=/sigT_fun. + by rewrite riE dfwithin /wedge_lift /= surjective_existT reprK. +- congr wedge_prod; rewrite E. + rewrite /proj /wedge_prod /wedge_fun /=/sigT_fun. + by rewrite riE dfwithin /wedge_lift /= surjective_existT reprK. +Qed. + +End wedge_as_product. + +Lemma wedge_hausdorff : + (forall i, hausdorff_space (X i)) -> hausdorff_space wedge. +Proof. +move=> /hausdorff_product hf x y clxy. +apply/wedge_prod_inj/hf => U V /wedge_prod_continuous nU. +move=> /wedge_prod_continuous nV; have := clxy _ _ nU nV. +by case => z [/= ? ?]; exists (wedge_prod z). +Qed. + +Lemma wedge_fun_joint_continuous (T R : topologicalType) + (k : forall (x : I), T -> X x -> R): + finite_set [set: I] -> + (forall x, closed [set p0 x]) -> + (forall t x y, k x t (p0 x) = k y t (p0 y)) -> + (forall x, continuous (uncurry (k x))) -> + continuous (uncurry (fun t => wedge_fun (k^~ t))). +Proof. +move=> Ifin clp0 kE kcts /= [t u] U. +case : (wedge_nbhs_specP u) => [//|i0 /=|]. + rewrite wedge_lift_funE // => Ukp0. + have pq_ x : {PQ : set T * set (X x) | [/\ nbhs (p0 x) PQ.2, + nbhs t PQ.1 & PQ.1 `*` PQ.2 `<=` uncurry (k x) @^-1` U]}. + apply: cid. + move: Ukp0; rewrite (@kE t i0 x). + rewrite -[k x ]uncurryK /curry=> /kcts[[P Q] [Pt Qp0 pqU]]. + by exists (P, Q). + have UPQ : nbhs (wedge_lift (p0 i0)) + (\bigcup_x (@wedge_lift x) @` (projT1 (pq_ x)).2). + rewrite wedge_point_nbhs => r _. + by case: (projT2 (pq_ r)) => /filterS + ? ?; apply => z /= ?; exists r. + have /finite_fsetP [fI fIE] := Ifin. + have UPt : nbhs t (\bigcap_(r in [set` fI]) (projT1 (pq_ r)).1). + by apply: filter_bigI => x ?; case: (projT2 (pq_ x)). + near_simpl => /=; near=> t1 t2 => /=. + have [//|x _ [w /=] ? <-]:= near UPQ t2. + rewrite wedge_lift_funE //. + case: (projT2 (pq_ x)) => ? Npt /(_ (t1, w)) => /=; apply; split => //. + by apply: (near UPt t1) => //; rewrite -fIE. +move=> x {}u uNp0 /=; rewrite wedge_lift_funE //= -[k x]uncurryK /curry. +move/kcts; rewrite nbhs_simpl /= => -[[P Q] [Pt Qu] PQU]. +have wQu : nbhs (wedge_lift u) ((@wedge_lift x) @` Q). + by rewrite -wedge_lift_nbhs //=; apply: filterS Qu => z; exists z. +near_simpl; near=> t1 t2 => /=. +have [//|l ? <-] := near wQu t2; rewrite wedge_lift_funE//. +by apply: (PQU (t1,l)); split => //; exact: (near Pt t1). +Unshelve. all: by end_near. Qed. + End wedge. Section pwedge. @@ -200,3 +387,26 @@ HB.instance Definition _ := Quotient.on pwedge. HB.instance Definition _ := isPointed.Build pwedge pwedge_point. End pwedge. + +Section bpwedge. +Context (X Y : bpTopologicalType). + +Definition bpwedge_shared_pt b := + if b return (if b then X else Y) then @one X else @zero Y. +Local Notation bpwedge := (@wedge bool _ bpwedge_shared_pt). +Local Notation bpwedge_lift := (@wedge_lift bool _ bpwedge_shared_pt). + +Local Lemma wedge_neq : @bpwedge_lift true zero != @bpwedge_lift false one. +Proof. +by apply/eqP => /eqmodP/predU1P[//|/andP[/= + _]]; exact/negP/zero_one_neq. +Qed. + +Local Lemma bpwedgeE : @bpwedge_lift true one = @bpwedge_lift false zero . +Proof. by apply/eqmodP/orP; rewrite !eqxx; right. Qed. + +HB.instance Definition _ := @isBiPointed.Build + bpwedge (@bpwedge_lift true zero) (@bpwedge_lift false one) wedge_neq. +End bpwedge. + +Notation bpwedge X Y := (@wedge bool _ (bpwedge_shared_pt X Y)). +Notation bpwedge_lift X Y := (@wedge_lift bool _ (bpwedge_shared_pt X Y)). diff --git a/theories/kernel.v b/theories/kernel.v index 4d154d2671..6120babd76 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -571,24 +571,30 @@ Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y) (k0 : forall z, 0 <= k z) (mk : measurable_fun [set: X * Y] k) : measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)). Proof. -have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). -apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. -have [l_ hl_] := measure_uub l. -by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. +pose k_ := nnsfun_approx measurableT mk. +apply: (@measurable_fun_xsection_integral _ k_). +- by move=> a b ab; exact/nd_nnsfun_approx. +- by move=> z; exact/cvg_nnsfun_approx. +- move => n r. + have [l_ hl_] := measure_uub l. + by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. Qed. Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y) (k0 : forall t, 0 <= k t) (mk : measurable_fun [set: X * Y] k) : measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)). Proof. -have [k_ [ndk_ k_k]] := approximation measurableT mk (fun xy _ => k0 xy). -apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. -have [l_ hl_] := sfinite_kernel l. -rewrite (_ : (fun x => _) = (fun x => - mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first. - by apply/funext => x; rewrite hl_//; exact/measurable_xsection. -apply: ge0_emeasurable_fun_sum => // m _. -by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. +pose k_ := nnsfun_approx measurableT mk. +apply: (@measurable_fun_xsection_integral _ k_). +- by move=> a b ab; exact/nd_nnsfun_approx. +- by move=> z; exact/cvg_nnsfun_approx. +- move => n r. + have [l_ hl_] := sfinite_kernel l. + rewrite (_ : (fun x => _) = (fun x => + mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first. + by apply/funext => x; rewrite hl_//; exact/measurable_xsection. + apply: ge0_emeasurable_fun_sum => // m _. + by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. Qed. End measurable_fun_integral_finite_sfinite. @@ -1007,8 +1013,11 @@ Lemma measurable_fun_integral_kernel (k : Y -> \bar R) (k0 : forall z, 0 <= k z) (mk : measurable_fun [set: Y] k) : measurable_fun [set: X] (fun x => \int[l x]_y k y). Proof. -have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). -by apply: (measurable_fun_preimage_integral ndk_ k_k) => n r; exact/ml. +pose k_ := nnsfun_approx measurableT mk. +apply: (@measurable_fun_preimage_integral _ _ _ _ _ _ k_) => //. +- by move=> a b ab; exact/nd_nnsfun_approx. +- by move=> z _; exact/cvg_nnsfun_approx. +- by move=> n r; exact/ml. Qed. End measurable_fun_integral_kernel. @@ -1077,13 +1086,13 @@ Lemma integral_kcomp x f : (forall z, 0 <= f z) -> measurable_fun [set: Z] f -> \int[kcomp l k x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z). Proof. move=> f0 mf. -have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z). +pose f_ := nnsfun_approx measurableT mf. transitivity (\int[kcomp l k x]_z (lim ((f_ n z)%:E @[n --> \oo]))). - by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f. + by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: cvg_nnsfun_approx. rewrite monotone_convergence//; last 3 first. by move=> n; exact/measurable_EFinP. by move=> n z _; rewrite lee_fin. - by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin. + by move=> z _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. rewrite (_ : (fun _ => _) = (fun n => \int[l x]_y (\int[k (x, y)]_z (f_ n z)%:E)))//; last first. by apply/funext => n; rewrite integral_kcomp_nnsfun. @@ -1099,12 +1108,12 @@ transitivity (\int[l x]_y lim ((\int[k (x, y)]_z (f_ n z)%:E) @[n --> \oo])). + exact/measurable_EFinP. + by move=> z _; rewrite lee_fin. + exact/measurable_EFinP. - + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin. + + by move=> z _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first. - by move=> n; exact/measurable_EFinP. - by move=> n z _; rewrite lee_fin. - - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin. -by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f. + - by move=> z _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. +by apply: eq_integral => z _; apply/cvg_lim => //; exact: cvg_nnsfun_approx. Qed. End integral_kcomp. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index b043af47cd..1f47205b40 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop signed reals ereal topology. -From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import tvs normedtype sequences real_interval esum measure. From mathcomp Require Import lebesgue_measure numfun realfun function_spaces. (**md**************************************************************************) @@ -53,6 +53,9 @@ From mathcomp Require Import lebesgue_measure numfun realfun function_spaces. (* `[(k%:R * 2 ^- n), (k.+1%:R * 2 ^- n)[ *) (* approx D f == nondecreasing sequence of functions that *) (* approximates f over D using dyadic intervals *) +(* It uses the sets approx_A and approx_B. *) +(* nnsfun_approx D f == same as approx D f but as a nnsfun *) +(* approximates f over D using dyadic intervals *) (* Rintegral mu D f := fine (\int[mu]_(x in D) f x). *) (* mu.-integrable D f == f is measurable over D and the integral of f *) (* w.r.t. D is < +oo *) @@ -96,7 +99,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Import numFieldTopology.Exports. +Import numFieldNormedType.Exports. From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. @@ -121,6 +124,7 @@ HB.mixin Record isMeasurableFun d d' (aT : sigmaRingType d) (rT : sigmaRingType }. HB.structure Definition MeasurableFun d d' aT rT := {f of @isMeasurableFun d d' aT rT f}. +Arguments measurable_funP {d d' aT rT} s. (* #[global] Hint Resolve fimfun_inP : core. *) @@ -222,8 +226,8 @@ HB.instance Definition _ x := isMeasurableFun.Build d _ aT rT (cst x) End mfun. -Section mfun_realType. -Context {d} {aT : sigmaRingType d} {rT : realType}. +Section mfun_sigmaRing_realType. +Context {rT : realType}. HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT (@normr rT rT) (@normr_measurable rT setT). @@ -231,7 +235,7 @@ HB.instance Definition _ := @isMeasurableFun.Build _ _ _ rT HB.instance Definition _ := isMeasurableFun.Build _ _ _ _ (@expR rT) (@measurable_expR rT). -End mfun_realType. +End mfun_sigmaRing_realType. Section mfun_measurableType. Context {d d'} {aT : measurableType d} {rT : measurableType d'}. @@ -288,7 +292,7 @@ Lemma mindicE (D : set aT) (mD : measurable D) : Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ aT rT (mindic mD) - (@measurable_fun_indic _ aT rT setT D mD). + (@measurable_indic _ aT rT setT D mD). Definition indic_mfun (D : set aT) (mD : measurable D) := [the {mfun aT >-> rT} of mindic mD]. @@ -305,17 +309,9 @@ Definition max_mfun f g := [the {mfun aT >-> _} of f \max g]. End ring. Arguments indic_mfun {d aT rT} _. - -Lemma measurable_indic d (T : measurableType d) (R : realType) - (D A : set T) : measurable A -> - measurable_fun D (\1_A : T -> R). -Proof. -by move=> mA; apply/measurable_funTS; rewrite (_ : \1__ = mindic R mA). -Qed. +(* TODO: move earlier?*) #[global] Hint Extern 0 (measurable_fun _ (\1__ : _ -> _)) => (exact: measurable_indic ) : core. -#[deprecated(since="mathcomp-analysis 0.6.3", note="use `measurable_indic` instead")] -Notation measurable_fun_indic := measurable_indic (only parsing). Section sfun_pred. Context {d} {aT : sigmaRingType d} {rT : realType}. @@ -1042,7 +1038,7 @@ apply/eqP; rewrite eq_le; apply/andP; split. by apply: ereal_sup_ubound => /=; exists h. Qed. -Local Notation "\int_ ( x 'in' D ) F" := (integral mu D (fun x => F)) +Local Notation "\int_ ( x 'in' D ) F" := (integral mu D (fun x => F)%E) (at level 36, F at level 36, x, D at level 50, format "'[' \int_ ( x 'in' D ) '/ ' F ']'"). @@ -1095,9 +1091,9 @@ Qed. End integral. Notation "\int [ mu ]_ ( x 'in' D ) f" := - (integral mu D (fun x => f)) : ereal_scope. + (integral mu D (fun x => f)%E) : ereal_scope. Notation "\int [ mu ]_ x f" := - ((integral mu setT (fun x => f)))%E : ereal_scope. + ((integral mu setT (fun x => f)%E))%E : ereal_scope. Arguments eq_integral {d T R mu D} g. Section eq_measure_integral. @@ -1312,10 +1308,13 @@ Variables (f : T -> \bar R) (mf : measurable_fun D f). Local Notation I := (@dyadic_itv R). -Let A n k := if (k < n * 2 ^ n)%N then +Definition approx_A n k := if (k < n * 2 ^ n)%N then D `&` [set x | f x \in EFin @` [set` I n k]] else set0. -Let B n := D `&` [set x | n%:R%:E <= f x]%E. +Definition approx_B n := D `&` [set x | n%:R%:E <= f x]%E. + +Local Notation A := approx_A. +Local Notation B := approx_B. Definition approx : (T -> R)^nat := fun n x => \sum_(k < n * 2 ^ n) k%:R * 2 ^- n * \1_(A n k) x + n%:R * \1_(B n) x. @@ -1617,6 +1616,7 @@ move=> m n mn; rewrite (nnsfun_approxE n) (nnsfun_approxE m). exact: nd_approx. Qed. +#[deprecated(since="mathcomp-analysis 1.7.0", note="use `nnsfun_approx`, `cvg_nnsfun_approx`, and `nd_nnsfun_approx` instead")] Lemma approximation : (forall t, D t -> (0 <= f t)%E) -> exists g : {nnsfun T >-> R}^nat, nondecreasing_seq (g : (T -> R)^nat) /\ (forall x, D x -> EFin \o g^~ x @ \oo --> f x). @@ -1644,21 +1644,21 @@ rewrite integral_mkcond erestrict_scale [in RHS]integral_mkcond => k0. set h1 := f1 \_ D. have h10 x : 0 <= h1 x by apply: erestrict_ge0. have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1. -have [g [nd_g gh1]] := approximation measurableT mh1 (fun x _ => h10 x). +pose g := nnsfun_approx measurableT mh1. pose kg := fun n => scale_nnsfun (g n) k0. rewrite (@nd_ge0_integral_lim _ _ _ mu (fun x => k%:E * h1 x) kg). - rewrite (_ : _ \o _ = fun n => sintegral mu (scale_nnsfun (g n) k0))//. rewrite (_ : (fun _ => _) = (fun n => k%:E * sintegral mu (g n))). rewrite limeMl //; last first. - by apply: is_cvg_sintegral => // x m n mn; apply/(lef_at x nd_g). - by rewrite -(nd_ge0_integral_lim mu h10) // => x; - [exact/(lef_at x nd_g)|exact: gh1]. + by apply: is_cvg_sintegral => // x m n mn; exact/lefP/nd_nnsfun_approx. + by rewrite -(nd_ge0_integral_lim mu h10)// => [x m n mn|x]; + [exact/lefP/nd_nnsfun_approx|exact: cvg_nnsfun_approx]. by under eq_fun do rewrite (sintegralrM mu k (g _)). - by move=> t; rewrite mule_ge0. -- by move=> x m n mn; rewrite /kg ler_pM//; exact/lefP/nd_g. +- by move=> x m n mn; rewrite /kg ler_pM//; exact/lefP/nd_nnsfun_approx. - move=> x. rewrite [X in X @ \oo --> _](_ : _ = (fun n => k%:E * (g n x)%:E)) ?funeqE//. - by apply: cvgeMl => //; exact: gh1. + by apply: cvgeMl => //; exact: cvg_nnsfun_approx. Qed. End ge0_linearityZ. @@ -1686,29 +1686,28 @@ have h10 x : 0 <= h1 x by apply: erestrict_ge0. have h20 x : 0 <= h2 x by apply: erestrict_ge0. have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1. have mh2 : measurable_fun setT h2 by exact/(measurable_restrictT _ _).1. -have [g1 [nd_g1 gh1]] := approximation measurableT mh1 (fun x _ => h10 x). -have [g2 [nd_g2 gh2]] := approximation measurableT mh2 (fun x _ => h20 x). +pose g1 := nnsfun_approx measurableT mh1. +pose g2 := nnsfun_approx measurableT mh2. pose g12 := fun n => add_nnsfun (g1 n) (g2 n). rewrite (@nd_ge0_integral_lim _ _ _ mu _ g12) //; last 3 first. - by move=> x; rewrite adde_ge0. - - by apply: nondecreasing_seqD => // x; - [exact/(lef_at x nd_g1)|exact/(lef_at x nd_g2)]. + - by apply: nondecreasing_seqD => // x m n mn; + [exact/lefP/nd_nnsfun_approx|exact/lefP/nd_nnsfun_approx]. - move=> x; rewrite (_ : _ \o _ = (fun n => (g1 n x)%:E + (g2 n x)%:E))//. - apply: cvgeD => //; [|exact: gh1|exact: gh2]. + apply: cvgeD => //; [|exact: cvg_nnsfun_approx..]. by apply: ge0_adde_def => //; rewrite !inE; [exact: h10|exact: h20]. under [_ \o _]eq_fun do rewrite sintegralD. -rewrite (nd_ge0_integral_lim _ _ (fun x => lef_at x nd_g1)) //; last first. - by move=> x; exact: gh1. -rewrite (nd_ge0_integral_lim _ _ (fun x => lef_at x nd_g2)) //; last first. - by move=> x; exact: gh2. -rewrite limeD //. - by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g1). - by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g2). -rewrite ge0_adde_def => //; rewrite inE; apply: lime_ge. -- by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g1). -- by apply: nearW => n; exact: sintegral_ge0. -- by apply: is_cvg_sintegral => // x Dx; exact/(lef_at x nd_g2). -- by apply: nearW => n; exact: sintegral_ge0. +rewrite (@nd_ge0_integral_lim _ _ _ _ _ g1)//; last 2 first. + by move=> x m n mn; exact/lefP/nd_nnsfun_approx. + by move=> x; exact/cvg_nnsfun_approx. +rewrite (@nd_ge0_integral_lim _ _ _ _ _ g2)//; last 2 first. + by move=> x m n mn; exact/lefP/nd_nnsfun_approx. + by move=> x; exact/cvg_nnsfun_approx. +rewrite limeD//; [ + by apply: is_cvg_sintegral => // x m n mn; exact/lefP/nd_nnsfun_approx..|]. +by rewrite ge0_adde_def => //; rewrite inE; apply: lime_ge; solve[ + (by apply: is_cvg_sintegral => // x m n mn; exact/lefP/nd_nnsfun_approx) || + (by apply: nearW => n; exact: sintegral_ge0)]. Qed. Lemma ge0_le_integral : (forall x, D x -> f1 x <= f2 x) -> @@ -1721,24 +1720,24 @@ have h20 x : 0 <= h2 x by apply: erestrict_ge0. have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1. have mh2 : measurable_fun setT h2 by exact/(measurable_restrictT _ _).1. have h12 x : h1 x <= h2 x by apply: lee_restrict. -have [g1 [nd_g1 /(_ _ Logic.I) gh1]] := - approximation measurableT mh1 (fun x _ => h10 _). -rewrite (nd_ge0_integral_lim _ h10 (fun x => lef_at x nd_g1) gh1)//. +pose g1 := nnsfun_approx measurableT mh1. +rewrite (@nd_ge0_integral_lim _ _ _ _ _ g1)//; last 2 first. + by move=> x m n mn; exact/lefP/nd_nnsfun_approx. + by move=> x; exact: cvg_nnsfun_approx. apply: lime_le. - by apply: is_cvg_sintegral => // t Dt; exact/(lef_at t nd_g1). + by apply: is_cvg_sintegral => // t m n mn; exact/lefP/nd_nnsfun_approx. near=> n; rewrite ge0_integralTE//; apply: ereal_sup_ubound => /=. -exists (g1 n) => // t; rewrite (le_trans _ (h12 _)) //. -have := gh1 t. +exists (g1 n) => // t; rewrite (le_trans _ (h12 _))//. have := leey (h1 t); rewrite le_eqVlt => /predU1P[->|ftoo]. by rewrite leey. have h1tfin : h1 t \is a fin_num. by rewrite fin_numE gt_eqF/= ?lt_eqF// (lt_le_trans _ (h10 t)). -have := gh1 t. +have /= := @cvg_nnsfun_approx _ _ _ _ measurableT _ mh1 (fun x _ => h10 x) t Logic.I. rewrite -(fineK h1tfin) => /fine_cvgP[ft_near]. -set u_ := (X in X --> _) => u_h1 g1h1. +set u_ := (X in X --> _) => u_h1. have <- : lim u_ = fine (h1 t) by exact/cvg_lim. rewrite lee_fin; apply: nondecreasing_cvgn_le. - by move=> // a b ab; rewrite /u_ /=; exact/lefP/nd_g1. + by move=> // a b ab; rewrite /u_ /=; exact/lefP/nd_nnsfun_approx. by apply/cvg_ex; eexists; exact: u_h1. Unshelve. all: by end_near. Qed. @@ -1760,22 +1759,20 @@ HB.instance Definition _ x : @NonNegFun T R (cst x%:num) := Lemma approximation_sfun : exists g : {sfun T >-> R}^nat, (forall x, D x -> EFin \o g ^~ x @ \oo --> f x). Proof. -have [fp_ [fp_nd fp_cvg]] := - approximation mD (measurable_funepos mf) (fun=> ltac:(by [])). -have [fn_ [fn_nd fn_cvg]] := - approximation mD (measurable_funeneg mf) (fun=> ltac:(by [])). +pose fp_ := nnsfun_approx mD (measurable_funepos mf). +pose fn_ := nnsfun_approx mD (measurable_funeneg mf). exists (fun n => [the {sfun T >-> R} of fp_ n \+ cst (-1) \* fn_ n]) => x /=. rewrite [X in X @ \oo --> _](_ : _ = EFin \o fp_^~ x \+ (-%E \o EFin \o fn_^~ x))%E; last first. by apply/funext => n/=; rewrite EFinD mulN1r. by move=> Dx; rewrite (funeposneg f); apply: cvgeD; - [exact: add_def_funeposneg|apply: fp_cvg|apply:cvgeN; exact: fn_cvg]. + [exact: add_def_funeposneg|apply: cvg_nnsfun_approx|apply:cvgeN; apply: cvg_nnsfun_approx]. Qed. End approximation_sfun. Section lusin. -Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff ) : core. +Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff) : core. Local Open Scope ereal_scope. Context (rT : realType) (A : set rT). Let mu := [the measure _ _ of @lebesgue_measure rT]. @@ -2055,6 +2052,22 @@ Proof. by move=> mf; exact/(emeasurable_funM _ mf). Qed. End emeasurable_fun. +Section measurable_fun. +Context d (T : measurableType d) (R : realType). +Implicit Types (D : set T) (f g : T -> R). + +Lemma measurable_fun_sum D I s (h : I -> (T -> R)) : + (forall n, measurable_fun D (h n)) -> + measurable_fun D (fun x => \sum_(i <- s) h i x). +Proof. +move=> mh; apply/measurable_EFinP. +rewrite (_ : _ \o _ = (fun t => \sum_(i <- s) (h i t)%:E)); last first. + by apply/funext => t/=; rewrite -sumEFin. +by apply/emeasurable_fun_sum => i; exact/measurable_EFinP. +Qed. + +End measurable_fun. + Section measurable_fun_measurable2. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). @@ -2396,13 +2409,14 @@ Section integral_indic. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). +Implicit Type A : set T. Import HBNNSimple. -Lemma integral_indic (E : set T) : measurable E -> - \int[mu]_(x in D) (\1_E x)%:E = mu (E `&` D). +Lemma integral_indic A : measurable A -> + \int[mu]_(x in D) (\1_A x)%:E = mu (A `&` D). Proof. -move=> mE; rewrite (_ : \1_E = indic_nnsfun R mE)// integral_nnsfun//=. +move=> mA; rewrite (_ : \1_A = indic_nnsfun R mA)// integral_nnsfun//=. by rewrite restrict_indic sintegral_indic//; exact: measurableI. Qed. @@ -2483,20 +2497,20 @@ Lemma ge0_integral_mscale (mf : measurable_fun D f) : (forall x, D x -> 0 <= f x) -> \int[mscale k m]_(x in D) f x = k%:num%:E * \int[m]_(x in D) f x. Proof. -move=> f0; have [f_ [ndf_ f_f]] := approximation mD mf f0. +move=> f0; pose f_ := nnsfun_approx mD mf. transitivity (limn (fun n => \int[mscale k m]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//=. - - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=; exact: f_f. + - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=; exact: cvg_nnsfun_approx. - by move=> n; apply: measurableT_comp => //; exact: measurable_funTS. - by move=> n x _; rewrite lee_fin. - - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin. + - by move=> x _ a b ab; rewrite lee_fin//; exact/lefP/nd_nnsfun_approx. rewrite (_ : \int[m]_(x in D) _ = limn (fun n => \int[m]_(x in D) (f_ n x)%:E)); last first. rewrite -monotone_convergence//=. - - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f. + - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n x _; rewrite lee_fin. - - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin. + - by move=> x _ a b ab; rewrite lee_fin//; exact/lefP/nd_nnsfun_approx. rewrite -limeMl//. by congr (limn _); apply/funext => n /=; rewrite integral_mscale_nnsfun. apply/ereal_nondecreasing_is_cvgn => a b ab; apply: ge0_le_integral => //. @@ -2504,7 +2518,7 @@ apply/ereal_nondecreasing_is_cvgn => a b ab; apply: ge0_le_integral => //. - exact/measurable_EFinP/measurable_funTS. - by move=> x _; rewrite lee_fin. - exact/measurable_EFinP/measurable_funTS. -- by move=> x _; rewrite lee_fin; move/ndf_ : ab => /lefP. +- by move=> x _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. End integral_mscale. @@ -2653,19 +2667,19 @@ Lemma ge0_integral_pushforward (f : Y -> \bar R) : \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x. Proof. move=> mf f0. -have [f_ [ndf_ f_f]] := approximation measurableT mf (fun t _ => f0 t). +pose f_ := nnsfun_approx measurableT mf. transitivity (limn (fun n => \int[pushforward mu mphi]_x (f_ n x)%:E)). rewrite -monotone_convergence//. - - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: f_f. + - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP. - by move=> n y _; rewrite lee_fin. - - by move=> y _ m n mn; rewrite lee_fin; apply/lefP/ndf_. + - by move=> y _ m n mn; rewrite lee_fin; apply/lefP/nd_nnsfun_approx. rewrite (_ : (fun _ => _) = (fun n => \int[mu]_x (EFin \o f_ n \o phi) x)). rewrite -monotone_convergence//; last 3 first. - by move=> n /=; apply: measurableT_comp => //; exact: measurableT_comp. - by move=> n x _ /=; rewrite lee_fin. - - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_. - by apply: eq_integral => x _ /=; apply/cvg_lim => //; exact: f_f. + - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => x _ /=; apply/cvg_lim => //; exact: cvg_nnsfun_approx. apply/funext => n. have mfnphi r : measurable (f_ n @^-1` [set r] \o phi). rewrite -[_ \o _]/(phi @^-1` (f_ n @^-1` [set r])) -(setTI (_ @^-1` _)). @@ -2699,16 +2713,15 @@ Let ge0_integral_dirac (f : T -> \bar R) (mf : measurable_fun D f) (f0 : forall x, D x -> 0 <= f x) : D a -> \int[\d_a]_(x in D) (f x) = f a. Proof. -move=> Da; have [f_ [ndf_ f_f]] := approximation mD mf f0. +move=> Da; pose f_ := nnsfun_approx mD mf. transitivity (limn (fun n => \int[\d_ a]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//. - - apply: eq_integral => x Dx; apply/esym/cvg_lim => //; apply: f_f. - by rewrite inE in Dx. + - by apply: eq_integral => x /set_mem Dx; apply/esym/cvg_lim => //; apply: cvg_nnsfun_approx. - by move=> n; apply/measurable_EFinP; exact/measurable_funTS. - by move=> *; rewrite lee_fin. - - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_. + - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. rewrite (_ : (fun _ => _) = (fun n => (f_ n a)%:E)). - by apply/cvg_lim => //; exact: f_f. + by apply/cvg_lim => //; exact: cvg_nnsfun_approx. apply/funext => n. under eq_integral do rewrite fimfunE// -fsumEFin//. rewrite ge0_integral_fsum//. @@ -2812,8 +2825,7 @@ Lemma ge0_integral_measure_sum (D : set T) (mD : measurable D) (forall x, D x -> 0 <= f x) -> measurable_fun D f -> forall N, \int[msum m_ N]_(x in D) f x = \sum_(n < N) \int[m_ n]_(x in D) f x. Proof. -move=> f0 mf. -have [f_ [f_nd f_f]] := approximation mD mf f0. +move=> f0 mf; pose f_ := nnsfun_approx mD mf. elim => [|N ih]; first by rewrite big_ord0 msum_mzero integral_measure_zero. rewrite big_ord_recr/= -ih. rewrite (_ : _ m_ N.+1 = measure_add (msum m_ N) (m_ N)); last first. @@ -2825,12 +2837,12 @@ have cvg_f_ (m : {measure set T -> \bar R}) : cvgn (fun x => \int[m]_(x0 in D) (f_ x x0)%:E). apply: ereal_nondecreasing_is_cvgn => a b ab. apply: ge0_le_integral => //; [exact: f_ge0|exact: f_ge0|]. - by move=> t Dt; rewrite lee_fin; apply/lefP/f_nd. + by move=> t Dt; rewrite lee_fin; apply/lefP/nd_nnsfun_approx. transitivity (limn (fun n => \int[measure_add (msum m_ N) (m_ N)]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//; last first. - by move=> t Dt a b ab; rewrite lee_fin; exact/lefP/f_nd. - by apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //; exact: f_f. + by move=> t Dt a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. transitivity (limn (fun n => \int[msum m_ N]_(x in D) (f_ n x)%:E + \int[m_ N]_(x in D) (f_ n x)%:E)). by congr (limn _); apply/funext => n; by rewrite integral_measure_add_nnsfun. @@ -2838,8 +2850,8 @@ rewrite limeD//; do?[exact: cvg_f_]; last first. by apply: ge0_adde_def; rewrite inE; apply: lime_ge => //; do?[exact: cvg_f_]; apply: nearW => n; apply: integral_ge0 => //; exact: f_ge0. by congr (_ + _); (rewrite -monotone_convergence//; [ - apply: eq_integral => t /[!inE] Dt; apply/cvg_lim => //; exact: f_f | - move=> t Dt a b ab; rewrite lee_fin; exact/lefP/f_nd]). + apply: eq_integral => t /[!inE] Dt; apply/cvg_lim => //; exact: cvg_nnsfun_approx | + move=> t Dt a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx]). Qed. End integral_mfun_measure_sum. @@ -3054,9 +3066,9 @@ Definition Rintegral (D : set T) (f : T -> R) := End Rintegral. Notation "\int [ mu ]_ ( x 'in' D ) f" := - (Rintegral mu D (fun x => f)) : ring_scope. + (Rintegral mu D (fun x => f)%R) : ring_scope. Notation "\int [ mu ]_ x f" := - (Rintegral mu setT (fun x => f)) : ring_scope. + (Rintegral mu setT (fun x => f)%R) : ring_scope. HB.lock Definition integrable {d} {T : measurableType d} {R : realType} (mu : set T -> \bar R) D f := @@ -3289,6 +3301,24 @@ End integrable_theory. Notation "mu .-integrable" := (integrable mu) : type_scope. Arguments eq_integrable {d T R mu D} mD f. +Section integrable_theory_finite_measure. +Context {R : realType} d (T : measurableType d). +Variable mu : {finite_measure set T -> \bar R}. +Local Open Scope ereal_scope. + +Lemma integrable_indic A : measurable A -> + mu.-integrable [set: T] (fun x : T => (\1_A x)%:E). +Proof. +move=> mA; apply/integrableP; split; first exact/measurable_EFinP. +rewrite (eq_integral (fun x => (\1_A x)%:E)); last first. + by move=> t _; rewrite gee0_abs// lee_fin. +rewrite integral_indic// setIT. +rewrite (@le_lt_trans _ _ (mu setT)) ?le_measure ?inE//. +by rewrite ?ltry ?fin_num_fun_lty//; exact: fin_num_measure. +Qed. + +End integrable_theory_finite_measure. + Section sequence_measure. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). @@ -3305,7 +3335,7 @@ Proof. move=> fi mf fmoo fpoo; rewrite integralE. rewrite ge0_integral_measure_series//; last exact/measurable_funepos. rewrite ge0_integral_measure_series//; last exact/measurable_funeneg. -transitivity (\sum_(n n _; rewrite fineK//; [exact: integrable_pos_fin_num|exact: integrable_neg_fin_num]. @@ -5523,49 +5553,49 @@ Let G_ (g : {nnsfun T >-> R}^nat) n y := \int[m1]_x (g n (x, y))%:E. Lemma measurable_fun_fubini_tonelli_F : measurable_fun setT F. Proof. -have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). +pose g := nnsfun_approx measurableT mf. apply: (emeasurable_fun_cvg (F_ g)) => //. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_F. - move=> x _. rewrite /F_ /F /fubini_F [in X in _ --> X](_ : (fun _ => _) = fun y => limn (EFin \o g ^~ (x, y))); last first. - by rewrite funeqE => y; apply/esym/cvg_lim => //; exact: g_f. + by rewrite funeqE => y; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. apply: cvg_monotone_convergence => //. - by move=> n; apply/measurable_EFinP => //; exact/measurableT_comp. - by move=> n y _; rewrite lee_fin//; exact: fun_ge0. - - by move=> y _ a b ab; rewrite lee_fin; exact/lefP/g_nd. + - by move=> y _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. Lemma measurable_fun_fubini_tonelli_G : measurable_fun setT G. Proof. -have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). +pose g := nnsfun_approx measurableT mf. apply: (emeasurable_fun_cvg (G_ g)) => //. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_G. - move=> y _; rewrite /G_ /G /fubini_G [in X in _ --> X](_ : (fun _ => _) = fun x => limn (EFin \o g ^~ (x, y))); last first. - by rewrite funeqE => x; apply/esym/cvg_lim => //; exact: g_f. + by rewrite funeqE => x; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. apply: cvg_monotone_convergence => //. - by move=> n; apply/measurable_EFinP => //; exact/measurableT_comp. - by move=> n x _; rewrite lee_fin; exact: fun_ge0. - - by move=> x _ a b ab; rewrite lee_fin; exact/lefP/g_nd. + - by move=> x _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. Lemma fubini_tonelli1 : \int[m1 \x m2]_z f z = \int[m1]_x F x. Proof. -have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). +pose g := nnsfun_approx measurableT mf. have F_F x : F x = limn (F_ g ^~ x). rewrite [RHS](_ : _ = limn (fun n => \int[m2]_y (EFin \o g n) (x, y)))//. rewrite -monotone_convergence//; last 3 first. - by move=> n; exact/measurable_EFinP/measurableT_comp. - by move=> n /= y _; rewrite lee_fin; exact: fun_ge0. - - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: g_f. + - by move=> y /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. rewrite [RHS](_ : _ = limn (fun n => \int[m1 \x m2]_z (EFin \o g n) z)). rewrite -monotone_convergence //; last 3 first. - by move=> n; exact/measurable_EFinP. - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0. - - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. - by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: g_f. + - by move=> y /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. rewrite [LHS](_ : _ = limn (fun n => \int[m1]_x (\int[m2]_y (EFin \o g n) (x, y)))). set r := fun _ => _; set l := fun _ => _; have -> // : l = r. @@ -5580,26 +5610,26 @@ rewrite -monotone_convergence //; first exact: eq_integral. + exact/measurable_EFinP/measurableT_comp. + by move=> *; rewrite lee_fin; exact: fun_ge0. + exact/measurable_EFinP/measurableT_comp. - + by move=> y _; rewrite lee_fin; move/g_nd : ab => /lefP; exact. + + by move=> y _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. Lemma fubini_tonelli2 : \int[m1 \x m2]_z f z = \int[m2]_y G y. Proof. -have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). +pose g := nnsfun_approx measurableT mf. have G_G y : G y = limn (G_ g ^~ y). rewrite /G /fubini_G. rewrite [RHS](_ : _ = limn (fun n => \int[m1]_x (EFin \o g n) (x, y)))//. rewrite -monotone_convergence//; last 3 first. - by move=> n; exact/measurable_EFinP/measurableT_comp. - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0. - - by move=> x /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. - by apply: eq_integral => x _; apply/esym/cvg_lim => //; exact: g_f. + - by move=> x /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => x _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. rewrite [RHS](_ : _ = limn (fun n => \int[m1 \x m2]_z (EFin \o g n) z)). rewrite -monotone_convergence //; last 3 first. - by move=> n; exact/measurable_EFinP. - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0. - - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. - by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: g_f. + - by move=> y /= _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. + by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. rewrite [LHS](_ : _ = limn (fun n => \int[m2]_y (\int[m1]_x (EFin \o g n) (x, y)))). set r := fun _ => _; set l := fun _ => _; have -> // : l = r. @@ -5613,7 +5643,7 @@ rewrite -monotone_convergence //; first exact: eq_integral. + exact/measurable_EFinP/measurableT_comp. + by move=> *; rewrite lee_fin fun_ge0. + exact/measurable_EFinP/measurableT_comp. - + by move=> x _; rewrite lee_fin; move/g_nd : ab => /lefP; exact. + + by move=> x _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. Lemma fubini_tonelli : diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index e658b9a261..6903b55c69 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp Require Import finmap fingroup perm rat archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals ereal signed. -From mathcomp Require Import topology numfun normedtype function_spaces. +From mathcomp Require Import topology numfun tvs normedtype function_spaces. From HB Require Import structures. From mathcomp Require Import sequences esum measure real_interval realfun exp. From mathcomp Require Export lebesgue_stieltjes_measure. @@ -61,7 +61,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. -Import numFieldTopology.Exports. +Import numFieldNormedType.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -1053,6 +1053,12 @@ by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf]. Qed. +Lemma measurable_funrpos D f : measurable_fun D f -> measurable_fun D f^\+. +Proof. by move=> mf; exact: measurable_maxr. Qed. + +Lemma measurable_funrneg D f : measurable_fun D f -> measurable_fun D f^\-. +Proof. by move=> mf; apply: measurable_maxr => //; exact: measurableT_comp. Qed. + Lemma measurable_minr D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g). Proof. @@ -1113,7 +1119,7 @@ apply: (@measurable_fun_limn_sup _ h) => // t Dt. - by apply/bounded_fun_has_lbound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. Qed. -Lemma measurable_fun_indic D (U : set T) : measurable U -> +Lemma measurable_indic D (U : set T) : measurable U -> measurable_fun D (\1_U : _ -> R). Proof. move=> mU mD /= Y mY. @@ -1133,6 +1139,16 @@ have [Y0|Y0] := pselect (Y 0%R); have [Y1|Y1] := pselect (Y 1%R). by apply/seteqP; split => // r /= -[_]; rewrite indicE; case: (_ \in _). Qed. +Lemma measurable_indicP D : measurable D <-> measurable_fun setT (\1_D : _ -> R). +Proof. +split=> [|m1]; first exact: measurable_indic. +have -> : D = (\1_D : _ -> R) @^-1` `]0, +oo[. + apply/seteqP; split => t/=. + by rewrite indicE => /mem_set ->; rewrite in_itv/= ltr01. + by rewrite in_itv/= andbT indicE ltr0n; have [/set_mem|//] := boolP (t \in D). +by rewrite -[_ @^-1` _]setTI; exact: m1. +Qed. + End measurable_fun_realType. #[deprecated(since="mathcomp-analysis 0.6.6", note="renamed `measurable_fun_limn_sup`")] Notation measurable_fun_lim_sup := measurable_fun_limn_sup (only parsing). @@ -1447,7 +1463,7 @@ Notation EFin_measurable_fun := measurable_EFinP (only parsing). Lemma measurable_fun_dirac d {T : measurableType d} {R : realType} D (U : set T) : measurable U -> measurable_fun D (fun x => \d_x U : \bar R). -Proof. by move=> /measurable_fun_indic/measurable_EFinP. Qed. +Proof. by move=> /measurable_indic/measurable_EFinP. Qed. Lemma measurable_er_map d (T : measurableType d) (R : realType) (f : R -> R) : measurable_fun setT f -> measurable_fun [set: \bar R] (er_map f). @@ -1709,7 +1725,7 @@ Lemma ae_pointwise_almost_uniform Proof. move=> mf mg mA Afin [C [mC C0 nC] epspos]. have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E & - {uniform (A `\` C) `\` B, f @ \oo --> g}]. + {uniform (A `\` C) `\` B, f @\oo --> g}]. apply: pointwise_almost_uniform => //. - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? []. - by apply: measurableI => //; exact: measurableC. diff --git a/theories/measure.v b/theories/measure.v index 6cfd34f05f..0830283695 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -70,6 +70,11 @@ From HB Require Import structures. (* G.-sigma.-measurable A == A is measurable for the sigma-algebra <> *) (* g_sigma_algebraType G == the measurableType corresponding to <> *) (* This is an HB alias. *) +(* g_sigma_algebra_mapping f == sigma-algebra generated by the mapping f *) +(* g_sigma_algebra_mappingType f == the measurableType corresponding to *) +(* g_sigma_algebra_mapping f *) +(* This is an HB alias. *) +(* f.-mapping.-measurable A == A is measurable for g_sigma_algebra_mapping f *) (* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *) (* ``` *) (* *) @@ -296,6 +301,9 @@ Reserved Notation "'\d_' a" (at level 8, a at level 2, format "'\d_' a"). Reserved Notation "G .-sigma" (at level 1, format "G .-sigma"). Reserved Notation "G .-sigma.-measurable" (at level 2, format "G .-sigma.-measurable"). +Reserved Notation "f .-mapping" (at level 1, format "f .-mapping"). +Reserved Notation "f .-mapping.-measurable" + (at level 2, format "f .-mapping.-measurable"). Reserved Notation "d .-ring" (at level 1, format "d .-ring"). Reserved Notation "d .-ring.-measurable" (at level 2, format "d .-ring.-measurable"). @@ -1735,6 +1743,16 @@ Definition preimage_class (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set rT)) : set (set aT) := [set D `&` f @^-1` B | B in G]. +Lemma preimage_class_comp (aT : Type) + d (rT : measurableType d) d' (T : sigmaRingType d') + (g : rT -> T) (f : aT -> rT) (D : set aT) : + measurable_fun setT g -> + preimage_class D (g \o f) measurable `<=` preimage_class D f measurable. +Proof. +move=> mg A; rewrite /preimage_class/= => -[B GB]; exists (g @^-1` B) => //. +by rewrite -[X in measurable X]setTI; exact: mg. +Qed. + (* f is measurable on the sigma-algebra generated by itself *) Lemma preimage_class_measurable_fun d (aT : pointedType) (rT : measurableType d) (D : set aT) (f : aT -> rT) : @@ -1819,6 +1837,58 @@ Qed. End measurability. +Definition mapping_display {T T'} : (T -> T') -> measure_display. +Proof. exact. Qed. + +Definition g_sigma_algebra_mappingType d' (T : pointedType) + (T' : measurableType d') (f : T -> T') : Type := T. + +Definition g_sigma_algebra_mapping d' (T : pointedType) + (T' : measurableType d') (f : T -> T') := + preimage_class setT f (@measurable _ T'). + +Section mapping_generated_sigma_algebra. +Context {d'} (T : pointedType) (T' : measurableType d'). +Variable f : T -> T'. + +Let mapping_set0 : g_sigma_algebra_mapping f set0. +Proof. +rewrite /g_sigma_algebra_mapping /preimage_class/=. +by exists set0 => //; rewrite preimage_set0 setI0. +Qed. + +Let mapping_setC A : + g_sigma_algebra_mapping f A -> g_sigma_algebra_mapping f (~` A). +Proof. +rewrite /g_sigma_algebra_mapping /preimage_class/= => -[B mB] <-{A}. +by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC]. +Qed. + +Let mapping_bigcup (F : (set T)^nat) : + (forall i, g_sigma_algebra_mapping f (F i)) -> + g_sigma_algebra_mapping f (\bigcup_i (F i)). +Proof. +move=> mF; rewrite /g_sigma_algebra_mapping /preimage_class/=. +pose g := fun i => sval (cid2 (mF i)). +pose mg := fun i => svalP (cid2 (mF i)). +exists (\bigcup_i g i). + by apply: bigcup_measurable => k; case: (mg k). +rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _. +by case: (mg k) => _; rewrite setTI. +Qed. + +HB.instance Definition _ := Pointed.on (g_sigma_algebra_mappingType f). + +HB.instance Definition _ := @isMeasurable.Build (mapping_display f) + (g_sigma_algebra_mappingType f) (g_sigma_algebra_mapping f) + mapping_set0 mapping_setC mapping_bigcup. + +End mapping_generated_sigma_algebra. + +Notation "f .-mapping" := (mapping_display f) : measure_display_scope. +Notation "f .-mapping.-measurable" := + (measurable : set (set (g_sigma_algebra_mappingType f))) : classical_set_scope. + Local Open Scope ereal_scope. Definition subset_sigma_subadditive {T} {R : numFieldType} diff --git a/theories/normedtype.v b/theories/normedtype.v index debaf7d26c..bf18d7bcde 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -6,7 +6,8 @@ From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import archimedean. From mathcomp Require Import cardinality set_interval ereal reals. From mathcomp Require Import signed topology prodnormedzmodule function_spaces. -From mathcomp Require Export real_interval separation_axioms. +From mathcomp Require Export real_interval separation_axioms tvs. + (**md**************************************************************************) (* # Norm-related Notions *) @@ -804,28 +805,110 @@ Lemma cvgenyP {R : realType} {T} {F : set_system T} {FF : Filter F} (f : T -> na (((f n)%:R : R)%:E @[n --> F] --> +oo%E) <-> (f @ F --> \oo). Proof. by rewrite cvgeryP cvgrnyP. Qed. -(** Modules with a norm *) +(** Modules with a norm depending on a numDomain*) -HB.mixin Record PseudoMetricNormedZmod_Lmodule_isNormedModule K V - of PseudoMetricNormedZmod K V & GRing.Lmodule K V := { +HB.mixin Record PseudoMetricNormedZmod_Tvs_isNormedModule K V + of PseudoMetricNormedZmod K V & Tvs K V := { normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; }. #[short(type="normedModType")] HB.structure Definition NormedModule (K : numDomainType) := - {T of PseudoMetricNormedZmod K T & GRing.Lmodule K T - & PseudoMetricNormedZmod_Lmodule_isNormedModule K T}. + {T of PseudoMetricNormedZmod K T & Tvs K T + & PseudoMetricNormedZmod_Tvs_isNormedModule K T}. -Section regular_topology. +HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldType) V + of PseudoMetricNormedZmod K V & GRing.Lmodule K V := { + normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |; +}. -Variable R : numFieldType. +HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V. + +(* NB: These lemmas are done later with more machinery. They should + be simplified once normedtype is split, and the present section can + depend on near lemmas on pseudometricnormedzmodtype ?*) +Lemma add_continuous : continuous (fun x : V * V => x.1 + x.2). +Proof. +move=> [/= x y]; apply/cvg_ballP => e e0 /=. +exists (ball x (e / 2), ball y (e / 2)) => /=. + by split; apply: nbhsx_ballx; rewrite divr_gt0. +rewrite -ball_normE /ball_/= => xy /= [nx ny]. +by rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (splitr e) ltrD. +Qed. + +Lemma scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2). +Proof. +move=> [/= k x]; apply/cvg_ballP => e e0 /=. +near +oo_K => M. +pose r := `|e| / 2 / M. +exists (ball k r, ball x r). + by split; apply: nbhsx_ballx; rewrite !divr_gt0// normr_gt0// gt_eqF. +rewrite -ball_normE /ball/= => lz /= [nk nx]. +have := @ball_split _ _ (k *: lz.2) (k *: x) (lz.1 *: lz.2) `|e|. +rewrite -ball_normE /= real_lter_normr ?gtr0_real//. +rewrite (_ : _ < - e = false) ?orbF; last by rewrite ltr_nnorml// oppr_le0 ltW. +apply. + rewrite -scalerBr normrZ -(@ltr_pM2r _ M^-1) ?invr_gt0//. + by rewrite (le_lt_trans _ nx)// mulrC ler_pdivrMl// ler_wpM2r// invr_gt0. +rewrite -scalerBl normrZ. +rewrite (@le_lt_trans _ _ (`|k - lz.1| * M)) ?ler_wpM2l -?ltr_pdivlMr//. +rewrite (@le_trans _ _ (`|lz.2| + `|x|)) ?lerDl//. +rewrite (@le_trans _ _ (`|x| + (`|x| + r)))//. + rewrite addrC lerD// -lerBlDl -(normrN x) (le_trans (lerB_normD _ _))//. + by rewrite distrC ltW. +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. +Unshelve. all: by end_near. Qed. + +Lemma locally_convex : + exists2 B : set (set V), (forall b, b \in B -> convex b) & basis B. +Proof. +exists [set B | exists x r, B = ball x r]. + move=> b; rewrite inE /= => [[x]] [r] -> z y l. + rewrite !inE -!ball_normE /= => zx yx l0; rewrite -subr_gt0 => l1. + have -> : x = l *: x + (1 - l) *: x. + by rewrite scalerBl addrCA subrr addr0 scale1r. + rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first. + by rewrite opprD addrACA -scalerBr -scalerBr. + rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//. + by rewrite -!normrZ ler_normD. + rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//. + rewrite ltr_leD//. + by rewrite -ltr_pdivlMl ?mulrA ?mulVf ?mul1r // ?normrE ?gt_eqF. + by rewrite -ler_pdivlMl ?mulrA ?mulVf ?mul1r ?ltW // ?normrE ?gt_eqF. + have -> : `|1 - l| = 1 - `| l |. + by move: l0 l1 => /ltW/normr_idP -> /ltW/normr_idP ->. + by rewrite -mulrDl addrCA subrr addr0 mul1r. +split. + move=> B [x] [r] ->. + rewrite openE/= -ball_normE/= /interior => y /= bxy; rewrite -nbhs_ballE. + exists (r - `|x - y|) => /=; first by rewrite subr_gt0. + move=> z; rewrite -ball_normE/= ltrBrDr. + by apply: le_lt_trans; rewrite [in leRHS]addrC ler_distD. +move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. +by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. +Qed. + +HB.instance Definition _ := + Uniform_isTvs.Build K V add_continuous scale_continuous locally_convex. +HB.instance Definition _ := + PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ. + +HB.end. + +Section standard_topology. +Variable R : numFieldType. HB.instance Definition _ := Num.NormedZmodule.on R^o. + HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R R^o erefl. HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R R^o (@normrM _). + PseudoMetricNormedZmod_Tvs_isNormedModule.Build R R^o (@normrM _). -End regular_topology. +End standard_topology. Lemma ball_itv {R : realFieldType} (x r : R) : ball x r = `]x - r, x + r[%classic. @@ -2301,14 +2384,14 @@ HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K (U * V)%type End prod_PseudoMetricNormedZmodule. Section prod_NormedModule. -Context {K : numDomainType} {U V : normedModType K}. +Context {K : numFieldType} {U V : normedModType K}. Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed. HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K (U * V)%type - prod_norm_scale. + PseudoMetricNormedZmod_Tvs_isNormedModule.Build K (U * V)%type + prod_norm_scale. End prod_NormedModule. @@ -5336,10 +5419,26 @@ Lemma bound_itvE (R : numDomainType) (a b : R) : (a \in `]-oo, a]). Proof. by rewrite !(boundr_in_itv, boundl_in_itv). Qed. -Lemma near_in_itv {R : realFieldType} (a b : R) : +Section near_in_itv. +Context {R : realFieldType} (a b : R). + +Lemma near_in_itvoo : {in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}. Proof. exact: interval_open. Qed. +Lemma near_in_itvoy : + {in `]a, +oo[, forall y, \forall z \near y, z \in `]a, +oo[}. +Proof. exact: interval_open. Qed. + +Lemma near_in_itvNyo : + {in `]-oo, b[, forall y, \forall z \near y, z \in `]-oo, b[}. +Proof. exact: interval_open. Qed. + +End near_in_itv. +#[deprecated(since="mathcomp-analysis 1.7.0", + note="use `near_in_itvoo` instead")] +Notation near_in_itv := near_in_itvoo (only parsing). + Lemma cvg_patch {R : realType} (f : R -> R^o) (a b : R) (x : R) : (a < b)%R -> x \in `]a, b[ -> f @ (x : subspace `[a, b]) --> f x -> @@ -5350,7 +5449,7 @@ move/cvgrPdist_lt : xf => /(_ e e0) xf. near=> z. rewrite patchE ifT//; last first. rewrite inE; apply: subset_itv_oo_cc. - by near: z; exact: near_in_itv. + by near: z; exact: near_in_itvoo. near: z. rewrite /prop_near1 /nbhs/= /nbhs_subspace ifT// in xf; last first. by rewrite inE/=; exact: subset_itv_oo_cc xab. @@ -5358,7 +5457,7 @@ case: xf => x0 /= x00 xf. near=> z. apply: xf => //=. rewrite inE; apply: subset_itv_oo_cc. -by near: z; exact: near_in_itv. +by near: z; exact: near_in_itvoo. Unshelve. all: by end_near. Qed. Notation "f @`[ a , b ]" := diff --git a/theories/numfun.v b/theories/numfun.v index f3361cce02..d38b7216e5 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -14,12 +14,15 @@ From mathcomp Require Import function_spaces. (* ``` *) (* {nnfun T >-> R} == type of non-negative functions *) (* f ^\+ == the function formed by the non-negative outputs *) -(* of f (from a type to the type of extended real *) -(* numbers) and 0 otherwise *) -(* rendered as f ⁺ with company-coq (U+207A) *) +(* of f and 0 otherwise *) +(* The codomain of f is the real numbers in scope *) +(* ring_scope and the extended real numbers in scope *) +(* ereal_scope. *) +(* It is rendered as f ⁺ with company-coq (U+207A). *) (* f ^\- == the function formed by the non-positive outputs *) (* of f and 0 o.w. *) -(* rendered as f ⁻ with company-coq (U+207B) *) +(* Similar to ^\+. *) +(* It is rendered as f ⁻ with company-coq (U+207B). *) (* \1_ A == indicator function 1_A *) (* ``` *) (* *) @@ -127,6 +130,149 @@ Proof. by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed. End erestrict_lemmas. +Section funrposneg. +Local Open Scope ring_scope. + +Definition funrpos T (R : realDomainType) (f : T -> R) := + fun x => maxr (f x) 0. +Definition funrneg T (R : realDomainType) (f : T -> R) := + fun x => maxr (- f x) 0. + +End funrposneg. + +Notation "f ^\+" := (funrpos f) : ring_scope. +Notation "f ^\-" := (funrneg f) : ring_scope. + +Section funrposneg_lemmas. +Local Open Scope ring_scope. +Variables (T : Type) (R : realDomainType) (D : set T). +Implicit Types (f g : T -> R) (r : R). + +Lemma funrpos_ge0 f x : 0 <= f^\+ x. +Proof. by rewrite /funrpos /= le_max lexx orbT. Qed. + +Lemma funrneg_ge0 f x : 0 <= f^\- x. +Proof. by rewrite /funrneg le_max lexx orbT. Qed. + +Lemma funrposN f : (\- f)^\+ = f^\-. Proof. exact/funext. Qed. + +Lemma funrnegN f : (\- f)^\- = f^\+. +Proof. by apply/funext => x; rewrite /funrneg opprK. Qed. + +(* TODO: the following lemmas require a pointed type and realDomainType does +not seem to be at this point + +Lemma funrpos_restrict f : (f \_ D)^\+ = (f^\+) \_ D. +Proof. +by apply/funext => x; rewrite /patch/_^\+; case: ifP; rewrite //= maxxx. +Qed. + +Lemma funrneg_restrict f : (f \_ D)^\- = (f^\-) \_ D. +Proof. +by apply/funext => x; rewrite /patch/_^\-; case: ifP; rewrite //= oppr0 maxxx. +Qed.*) + +Lemma ge0_funrposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}. +Proof. by move=> f0 x; rewrite inE => Dx; apply/max_idPl/f0. Qed. + +Lemma ge0_funrnegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}. +Proof. +by move=> f0 x; rewrite inE => Dx; apply/max_idPr; rewrite lerNl oppr0 f0. +Qed. + +Lemma le0_funrposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}. +Proof. by move=> f0 x; rewrite inE => Dx; exact/max_idPr/f0. Qed. + +Lemma le0_funrnegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}. +Proof. +by move=> f0 x; rewrite inE => Dx; apply/max_idPl; rewrite lerNr oppr0 f0. +Qed. + +Lemma ge0_funrposM r f : (0 <= r)%R -> + (fun x => r * f x)^\+ = (fun x => r * (f^\+ x)). +Proof. by move=> ?; rewrite funeqE => x; rewrite /funrpos maxr_pMr// mulr0. Qed. + +Lemma ge0_funrnegM r f : (0 <= r)%R -> + (fun x => r * f x)^\- = (fun x => r * (f^\- x)). +Proof. +by move=> r0; rewrite funeqE => x; rewrite /funrneg -mulrN maxr_pMr// mulr0. +Qed. + +Lemma le0_funrposM r f : (r <= 0)%R -> + (fun x => r * f x)^\+ = (fun x => - r * (f^\- x)). +Proof. +move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. +by rewrite funrposN ge0_funrnegM ?oppr_ge0. +Qed. + +Lemma le0_funrnegM r f : (r <= 0)%R -> + (fun x => r * f x)^\- = (fun x => - r * (f^\+ x)). +Proof. +move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. +by rewrite funrnegN ge0_funrposM ?oppr_ge0. +Qed. + +Lemma funr_normr f : normr \o f = f^\+ \+ f^\-. +Proof. +rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. +- rewrite ler0_norm// /funrpos /funrneg. + move/max_idPr : (fx0) => ->; rewrite add0r. + by move: fx0; rewrite -{1}oppr0 lerNr => /max_idPl ->. +- rewrite ger0_norm// /funrpos /funrneg; move/max_idPl : (fx0) => ->. + by move: fx0; rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0. +Qed. + +Lemma funrposneg f : f = (fun x => f^\+ x - f^\- x). +Proof. +rewrite funeqE => x; rewrite /funrpos /funrneg; have [|/ltW] := leP (f x) 0. + by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. +by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. +Qed. + +Lemma funrD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-. +Proof. +apply/funext => x; rewrite /funrpos /funrneg/=; have [|/ltW] := lerP 0 (f x + g x). +- by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. +- by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. +Qed. + +Lemma funrD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-). +Proof. +apply/funext => x; rewrite /funrpos /funrneg/=. +have [|fx0] := lerP 0 (f x); last rewrite add0r. +- rewrite -{1}oppr0 lerNl => /max_idPr ->; have [|/ltW] := lerP 0 (g x). + by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 subr0. + by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite addr0 sub0r opprK. +- move/ltW : (fx0); rewrite -{1}oppr0 lerNr => /max_idPl ->. + have [|]/= := lerP 0 (g x); last rewrite add0r. + by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 opprK addrC. + by rewrite -oppr0 ltrNr -{1}oppr0 => /ltW/max_idPl ->; rewrite opprD !opprK. +Qed. + +Lemma funrpos_le f g : + {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}. +Proof. +move=> fg x Dx; rewrite /funrpos /maxr; case: ifPn => fx; case: ifPn => gx //. +- by rewrite leNgt. +- by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg. +- exact: fg. +Qed. + +Lemma funrneg_le f g : + {in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}. +Proof. +move=> fg x Dx; rewrite /funrneg /maxr; case: ifPn => gx; case: ifPn => fx //. +- by rewrite leNgt. +- by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite ltrN2 ltNge fg. +- by rewrite lerN2; exact: fg. +Qed. + +End funrposneg_lemmas. +#[global] +Hint Extern 0 (is_true (0%R <= _ ^\+ _)%R) => solve [apply: funrpos_ge0] : core. +#[global] +Hint Extern 0 (is_true (0%R <= _ ^\- _)%R) => solve [apply: funrneg_ge0] : core. + Section funposneg. Local Open Scope ereal_scope. @@ -276,6 +422,17 @@ Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core. #[global] Hint Extern 0 (is_true (0%R <= _ ^\- _)%E) => solve [apply: funeneg_ge0] : core. +Section funrpos_funepos_lemmas. +Context {T : Type} {R : realDomainType}. + +Lemma funerpos (f : T -> R) : (EFin \o f)^\+%E = (EFin \o f^\+). +Proof. by apply/funext => x; rewrite /funepos /funrpos/= EFin_max. Qed. + +Lemma funerneg (f : T -> R) : (EFin \o f)^\-%E = (EFin \o f^\-). +Proof. by apply/funext => x; rewrite /funeneg /funrneg/= EFin_max. Qed. + +End funrpos_funepos_lemmas. + Definition indic {T} {R : ringType} (A : set T) (x : T) : R := (x \in A)%:R. Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") . Notation "'\1_' A" := (indic A) : ring_scope. diff --git a/theories/probability.v b/theories/probability.v index c57cac324d..39ad37fe6e 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -34,6 +34,10 @@ From mathcomp Require Import lebesgue_integral kernel. (* dRV_enum X == bijection between the domain and the range of X *) (* pmf X r := fine (P (X @^-1` [set r])) *) (* enum_prob X k == probability of the kth value in the range of X *) +(* independent_events I F == the events F indexed by I are independent *) +(* mutual_independence I F == the classes F indexed by I are independent *) +(* independent_RVs I X == the random variables X indexed by I are independent *) +(* independent_RVs2 X Y == the random variables X and Y are independent *) (* ``` *) (* *) (* ``` *) @@ -56,6 +60,8 @@ From mathcomp Require Import lebesgue_integral kernel. Reserved Notation "'{' 'RV' P >-> R '}'" (at level 0, format "'{' 'RV' P '>->' R '}'"). Reserved Notation "''E_' P [ X ]" (format "''E_' P [ X ]", at level 5). + (at level 0, format "'{' 'RV' P '>->' R '}'"). +Reserved Notation "''E_' P [ f . X ]" (format "''E_' P [ f . X ]", at level 5). Reserved Notation "''V_' P [ X ]" (format "''V_' P [ X ]", at level 5). Reserved Notation "{ 'dmfun' aT >-> T }" (at level 0, format "{ 'dmfun' aT >-> T }"). @@ -72,22 +78,23 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Definition random_variable (d : _) (T : measurableType d) (R : realType) - (P : probability T R) := {mfun T >-> R}. +Definition random_variable (d d' : _) (T : measurableType d) + (T' : measurableType d') (R : realType) (P : probability T R) := {mfun T >-> T'}. -Notation "{ 'RV' P >-> R }" := (@random_variable _ _ R P) : form_scope. +Notation "{ 'RV' P >-> T }" := (@random_variable _ _ _ T _ P) : form_scope. Lemma notin_range_measure d (T : measurableType d) (R : realType) (P : {measure set T -> \bar R}) (X : T -> R) r : r \notin range X -> P (X @^-1` [set r]) = 0%E. Proof. by rewrite notin_setE => hr; rewrite preimage10. Qed. -Lemma probability_range d (T : measurableType d) (R : realType) - (P : probability T R) (X : {RV P >-> R}) : P (X @^-1` range X) = 1%E. +Lemma probability_range d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (P : probability T R) (X : {RV P >-> T'}) : + P (X @^-1` range X) = 1%E. Proof. by rewrite preimage_range probability_setT. Qed. -Definition distribution d (T : measurableType d) (R : realType) - (P : probability T R) (X : {mfun T >-> R}) := +Definition distribution d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (P : probability T R) (X : {mfun T >-> T'}) := pushforward P (@measurable_funP _ _ _ _ X). Section distribution_is_probability. @@ -118,31 +125,36 @@ End distribution_is_probability. Section transfer_probability. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). +Context d d' (T : measurableType d) (T' : measurableType d') (R : realType). +Variable (P : probability T R). -Lemma probability_distribution (X : {RV P >-> R}) r : +Lemma probability_distribution (X : {RV P >-> T'}) r : P [set x | X x = r] = distribution P X [set r]. Proof. by []. Qed. -Lemma integral_distribution (X : {RV P >-> R}) (f : R -> \bar R) : - measurable_fun [set: R] f -> (forall y, 0 <= f y) -> +Lemma integral_distribution (X : {RV P >-> T'}) (f : T' -> \bar R) : + measurable_fun [set: T'] f -> (forall y, 0 <= f y) -> \int[distribution P X]_y f y = \int[P]_x (f \o X) x. Proof. by move=> mf f0; rewrite ge0_integral_pushforward. Qed. End transfer_probability. -HB.lock Definition expectation {d} {T : measurableType d} {R : realType} - (P : probability T R) (X : T -> R) := (\int[P]_w (X w)%:E)%E. +HB.lock Definition expectation {d d'} {T : measurableType d} {T' : measurableType d'} {R : realType} + (P : probability T R) (X : T -> T') (f : T' -> \bar R) := (\int[P]_w (f \o X) w)%E. Canonical expectation_unlockable := Unlockable expectation.unlock. Arguments expectation {d T R} P _%_R. -Notation "''E_' P [ X ]" := (@expectation _ _ _ P X) : ereal_scope. +Notation "''E_' P [ X ]" := (@expectation _ _ _ _ _ P X EFin) : ereal_scope. +Notation "''E_' P [ f . X ]" := (@expectation _ _ _ _ _ P X f) : ereal_scope. Section expectation_lemmas. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). +Context d d' (T : measurableType d) (U : measurableType d') (R : realType) (P : probability T R). + +Lemma expectation_def (X : {RV P >-> U}) f : 'E_P[f . X] = (\int[P]_w (f \o X) w)%E. +Proof. by rewrite unlock. Qed. -Lemma expectation_fin_num (X : {RV P >-> R}) : P.-integrable setT (EFin \o X) -> - 'E_P[X] \is a fin_num. +Lemma expectation_fin_num (X : {RV P >-> U}) : P.-integrable setT (f \o X) -> + 'E_P[f . X] \is a fin_num. Proof. by move=> ?; rewrite unlock integral_fune_fin_num. Qed. Lemma expectation_cst r : 'E_P[cst r] = r%:E. @@ -151,26 +163,26 @@ Proof. by rewrite unlock/= integral_cst//= probability_setT mule1. Qed. Lemma expectation_indic (A : set T) (mA : measurable A) : 'E_P[\1_A] = P A. Proof. by rewrite unlock integral_indic// setIT. Qed. -Lemma integrable_expectation (X : {RV P >-> R}) - (iX : P.-integrable [set: T] (EFin \o X)) : `| 'E_P[X] | < +oo. +Lemma integrable_expectation (X : {RV P >-> U}) f + (iX : P.-integrable [set: T] (f \o X)) : `| 'E_P[f . X] | < +oo. Proof. move: iX => /integrableP[? Xoo]; rewrite (le_lt_trans _ Xoo)// unlock. exact: le_trans (le_abse_integral _ _ _). Qed. -Lemma expectationM (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X)) - (k : R) : 'E_P[k \o* X] = k%:E * 'E_P [X]. +Lemma expectationMl (X : {RV P >-> U}) (iX : P.-integrable [set: T] (f \o X)) + (k : R) : 'E_P[k \o* f \o X] = k%:E * 'E_P [f . X]. Proof. by rewrite unlock muleC -integralZr. Qed. -Lemma expectation_ge0 (X : {RV P >-> R}) : - (forall x, 0 <= X x)%R -> 0 <= 'E_P[X]. +Lemma expectation_ge0 (X : {RV P >-> U}) f : + (forall x, 0 <= (f \o X) x)%R -> 0 <= 'E_P[f . X]. Proof. by move=> ?; rewrite unlock integral_ge0// => x _; rewrite lee_fin. Qed. -Lemma expectation_le (X Y : T -> R) : +Lemma expectation_le (X Y : T -> U) f : measurable_fun [set: T] X -> measurable_fun [set: T] Y -> - (forall x, 0 <= X x)%R -> (forall x, 0 <= Y x)%R -> + (forall x, 0 <= (f \o X) x) -> (forall x, 0 <= (f \o Y) x) -> {ae P, (forall x, X x <= Y x)%R} -> 'E_P[X] <= 'E_P[Y]. Proof. move=> mX mY X0 Y0 XY; rewrite unlock ae_ge0_le_integral => //. @@ -208,6 +220,8 @@ by apply/funext => t/=; rewrite big_map sumEFin mfun_sum. Qed. End expectation_lemmas. +#[deprecated(since="mathcomp-analysis 1.7.0", note="use `expectationMl` instead")] +Notation expectationM := expectationMl (only parsing). HB.lock Definition covariance {d} {T : measurableType d} {R : realType} (P : probability T R) (X Y : T -> R) := @@ -238,7 +252,7 @@ rewrite expectationD/=; last 2 first. - by rewrite compreBr// integrableB// compre_scale ?integrableZl. - by rewrite compre_scale// integrableZl// finite_measure_integrable_cst. rewrite 2?expectationB//= ?compre_scale// ?integrableZl//. -rewrite 3?expectationM//= ?finite_measure_integrable_cst//. +rewrite 3?expectationMl//= ?finite_measure_integrable_cst//. by rewrite expectation_cst mule1 fineM// EFinM !fineK// muleC subeK ?fin_numM. Qed. @@ -278,7 +292,7 @@ have aXY : (a \o* X * Y = a \o* (X * Y))%R. rewrite [LHS]covarianceE => [||//|] /=; last 2 first. - by rewrite compre_scale ?integrableZl. - by rewrite aXY compre_scale ?integrableZl. -rewrite covarianceE// aXY !expectationM//. +rewrite covarianceE// aXY !expectationMl//. by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num. Qed. @@ -525,6 +539,24 @@ Qed. End variance. Notation "'V_ P [ X ]" := (variance P X). +(* TODO: move earlier *) +Section mfun_measurable_realType. +Context {d} {aT : measurableType d} {rT : realType}. + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\+ + (measurable_funrpos (@measurable_funP _ _ _ _ f)). + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\- + (measurable_funrneg (@measurable_funP _ _ _ _ f)). + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ (@normr _ _ \o f) + (measurableT_comp (@normr_measurable _ _) (@measurable_funP _ _ _ _ f)). + +End mfun_measurable_realType. + Section markov_chebyshev_cantelli. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). @@ -554,7 +586,7 @@ Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> Proof. move=> t0. rewrite /mmt_gen_fun; have -> : expR \o r \o* X = - (normr \o normr) \o [the {mfun T >-> R} of expR \o r \o* X]. + (normr \o normr) \o [the {mfun _ >-> _} of expR \o r \o* X]. by apply: funext => t /=; rewrite normr_id ger0_norm ?expR_ge0. rewrite expRN lee_pdivlMr ?expR_gt0//. rewrite (le_trans _ (markov _ (expR_gt0 (r * a)) _ _ _))//; last first. @@ -841,6 +873,841 @@ Qed. End discrete_distribution. +Section independent_events. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Definition independent_events (I0 : choiceType) (I : set I0) (A : I0 -> set T) := + forall J : {fset I0}, [set` J] `<=` I -> + P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i). + +End independent_events. + +Section mutual_independence. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Definition mutual_independence (I0 : choiceType) (I : set I0) + (F : I0 -> set (set T)) := + (forall i : I0, I i -> F i `<=` @measurable _ T) /\ + forall J : {fset I0}, + [set` J] `<=` I -> + forall E : I0 -> set T, + (forall i : I0, i \in J -> E i \in F i) -> + P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). + +End mutual_independence. + +Section independent_RVs. +Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. + +Definition independent_RVs (I0 : choiceType) + (I : set I0) (X : I0 -> {mfun T >-> T'}) : Prop := + mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). + +Definition independent_RVs2 (X Y : {mfun T >-> T'}) := + independent_RVs [set: bool] [eta (fun=> cst point) with false |-> X, true |-> Y]. + +End independent_RVs. + +Section g_sigma_algebra_mapping_lemmas. +Context d {T : measurableType d} {R : realType}. + +Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : + measurable_fun setT f -> + g_sigma_algebra_mapping (f \o X)%R `<=` g_sigma_algebra_mapping X. +Proof. exact: preimage_class_comp. Qed. + +Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : + g_sigma_algebra_mapping X^\+%R `<=` d.-measurable. +Proof. +by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. +Qed. + +Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : + g_sigma_algebra_mapping X^\-%R `<=` d.-measurable. +Proof. +by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. +Qed. + +End g_sigma_algebra_mapping_lemmas. +Arguments g_sigma_algebra_mapping_comp {d T R X} f. + +Section independent_RVs_lemmas. +Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. +Local Open Scope ring_scope. + +Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y). +Proof. +move=> indeXY; split => /=. +- move=> [] _ /= A. + + by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; + exact/measurableT_comp. + + by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; + exact/measurableT_comp. +- move=> J _ E JE. + apply indeXY => //= i iJ; have := JE _ iJ. + by move: i {iJ} =>[|]//=; rewrite !inE => Eg; + exact: g_sigma_algebra_mapping_comp Eg. +Qed. + +Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. +Proof. +move=> indeXY; split=> [[|]/= _|J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R) => //. + exact: measurable_funrpos. +Qed. + +Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. +Proof. +move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. +Qed. + +Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. +Proof. +move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. +Qed. + +Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. +Proof. +move=> indeXY; split=> [/= [|]//= _ |J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. +Qed. + +End independent_RVs_lemmas. + +Definition preimage_classes I (d : I -> measure_display) + (Tn : forall k, semiRingOfSetsType (d k)) (T : Type) (fn : forall k, T -> Tn k) := + <>. +Arguments preimage_classes {I} d Tn {T} fn. + +Lemma measurable_fun_prod d [T : measurableType d] [R : realType] [D : set T] [I : eqType] + (s : seq I) [h : I -> T -> R] : + (forall n : I, n \in s -> measurable_fun D (h n)) -> + measurable_fun D (fun x => (\prod_(i <- s) h i x)%R). +Proof. +elim: s. + move=> mh. + under eq_fun do rewrite big_nil//=. + exact: measurable_cst. +move=> x y ih mh. +under eq_fun do rewrite big_cons//=. +apply: measurable_funM => //. + apply: mh. + by rewrite mem_head. +apply: ih => n ny. +apply: mh. +by rewrite inE orbC ny. +Qed. + +Section pairRV. +Context d d' {T : measurableType d} {T' : measurableType d'} {R : realType} + (P : probability T R). + +Definition pairRV (X Y : {RV P >-> T'}) : T * T -> T' * T' := + (fun x => (X x.1, Y x.2)). + +Lemma pairM (X Y : {RV P >-> T'}) : measurable_fun setT (pairRV X Y). +Proof. +rewrite /pairRV. +apply/prod_measurable_funP; split => //=. + rewrite (_ : (fst \o (fun x : T * T => (X x.1, Y x.2))) = (fun x => X x.1))//. + by apply/measurableT_comp => //=. +rewrite (_ : (snd \o (fun x : T * T => (X x.1, Y x.2))) = (fun x => Y x.2))//. +by apply/measurableT_comp => //=. +Qed. + +HB.instance Definition _ (X Y : {RV P >-> T'}) := + @isMeasurableFun.Build _ _ _ _ (pairRV X Y) (pairM X Y). + +End pairRV. + +Section product_expectation. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. +Local Open Scope ereal_scope. + +Let mu := @lebesgue_measure R. + +Let mprod_m (X Y : {RV P >-> R}) (A1 : set R) (A2 : set R) : + measurable A1 -> measurable A2 -> + (distribution P X \x distribution P Y) (A1 `*` A2) = + ((distribution P X) A1 * (distribution P Y) A2)%E. +Proof. +move=> mA1 mA2. +etransitivity. + by apply: product_measure1E. +rewrite /=. +done. +Qed. + +Lemma tmp0 (X Y : {RV P >-> R}) (B1 B2 : set R) : + measurable B1 -> measurable B2 -> + independent_RVs2 P X Y -> + P (X @^-1` B1 `&` Y @^-1` B2) = P (X @^-1` B1) * P (Y @^-1` B2). +Proof. +move=> mB1 mB2. +rewrite /independent_RVs2 /independent_RVs /mutual_independence /= => -[_]. +move/(_ [fset false; true]%fset (@subsetT _ _) + (fun b => if b then Y @^-1` B2 else X @^-1` B1)). +rewrite !big_fsetU1 ?inE//= !big_seq_fset1/=. +apply => -[|] /= _; rewrite !inE; rewrite /g_sigma_algebra_mapping. +by exists B2 => //; rewrite setTI. +by exists B1 => //; rewrite setTI. +Qed. + +Lemma tmp1 (X Y : {RV P >-> R}) (B1 B2 : set R) : + measurable B1 -> measurable B2 -> + independent_RVs2 P X Y -> + P (X @^-1` B1 `&` Y @^-1` B2) = (P \x P) (pairRV X Y @^-1` (B1 `*` B2)). +Proof. +move=> mB1 mB2 XY. +rewrite (_ : ((fun x : T * T => (X x.1, Y x.2)) @^-1` (B1 `*` B2)) = + (X @^-1` B1) `*` (Y @^-1` B2)); last first. + by apply/seteqP; split => [[x1 x2]|[x1 x2]]//. +rewrite product_measure1E; last 2 first. + rewrite -[_ @^-1` _]setTI. + by apply: (measurable_funP X). + rewrite -[_ @^-1` _]setTI. + by apply: (measurable_funP Y). +by rewrite tmp0//. +Qed. + +Let phi (x : R * R) := (x.1 * x.2)%R. +Let mphi : measurable_fun setT phi. +Proof. +rewrite /= /phi. +by apply: measurable_funM. +Qed. + +Lemma PP : (P \x P) setT = 1. +Proof. +rewrite /product_measure1 /=. +rewrite /xsection/=. +under eq_integral. + move=> t _. + rewrite (_ : [set y | (t, y) \in [set: T * T]] = setT); last first. + apply/seteqP; split => [x|x]// _ /=. + by rewrite in_setT. + rewrite probability_setT. + over. +rewrite integral_cst // mul1e. +apply: probability_setT. +Qed. + +HB.instance Definition _ := @Measure_isProbability.Build _ _ R (P \x P) PP. + +Lemma integrable_expectationM (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + 'E_(P \x P) [(fun x => `|X x.1 * Y x.2|)%R] < +oo +(* `|'E_(P) [(fun x => X x * Y x)%R]| < +oo *) . +Proof. +move=> indeXY iX iY. +(*apply: (@le_lt_trans _ _ 'E_(P \x P)[(fun x => `|(X x.1 * Y x.2)|%R)] + (* 'E_(P)[(fun x => `|(X x * Y x)|%R)] *) ). + rewrite unlock/=. + rewrite (le_trans (le_abse_integral _ _ _))//. + apply/measurable_EFinP/measurable_funM. + by apply/measurableT_comp => //. + by apply/measurableT_comp => //.*) +rewrite unlock. +rewrite [ltLHS](_ : _ = + \int[distribution (P \x P) (pairRV X Y)%R]_x `|x.1 * x.2|%:E); last first. + rewrite integral_distribution//=; last first. + apply/measurable_EFinP => //=. + by apply/measurableT_comp => //=. +(* admit. (* NG *)*) +rewrite [ltLHS](_ : _ = + \int[distribution P X \x distribution P Y]_x `|x.1 * x.2|%:E); last first. + apply: eq_measure_integral => //= A mA _. + apply/esym. + apply: product_measure_unique => //= A1 A2 mA1 mA2. + rewrite /pushforward/=. + rewrite -tmp1//. + by rewrite tmp0//. +rewrite fubini_tonelli1//=; last first. + by apply/measurable_EFinP => /=; apply/measurableT_comp => //=. +rewrite /fubini_F/= -/mu. +rewrite [ltLHS](_ : _ = \int[distribution P X]_x `|x|%:E * + \int[distribution P Y]_y `|y|%:E); last first. + rewrite -ge0_integralZr//=; last 2 first. + exact/measurable_EFinP. + by apply: integral_ge0 => //. + apply: eq_integral => x _. + rewrite -ge0_integralZl//=. + by under eq_integral do rewrite normrM. + exact/measurable_EFinP. +rewrite integral_distribution//=; last exact/measurable_EFinP. +rewrite integral_distribution//=; last exact/measurable_EFinP. +rewrite lte_mul_pinfty//. + by apply: integral_ge0 => //. + apply: integral_fune_fin_num => //=. + by move/integrable_abse : iX => //. +apply: integral_fune_lt_pinfty => //. +by move/integrable_abse : iY => //. +Qed. + +Lemma expectation_prod (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + 'E_(P \x P) [(fun x => X x.1 * Y x.2)%R] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> indeXY iX iY. +rewrite unlock. +rewrite -fubini1//=; last first. + apply/integrableP; split. + admit. + have := integrable_expectationM indeXY iX iY. + rewrite unlock. + apply: le_lt_trans. + rewrite le_eqVlt; apply/orP; left. + by apply/eqP/eq_integral => y _//. +rewrite /fubini_F/=. +Admitted. + +End product_expectation. + +Section product_expectation. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. +Local Open Scope ereal_scope. + +Import HBNNSimple. + +Let expectationM_nnsfun (f g : {nnsfun T >-> R}) : + (forall y y', y \in range f -> y' \in range g -> + P (f @^-1` [set y] `&` g @^-1` [set y']) = + P (f @^-1` [set y]) * P (g @^-1` [set y'])) -> + 'E_P [f \* g] = 'E_P [f] * 'E_P [g]. +Proof. +move=> fg; transitivity + ('E_P [(fun x => (\sum_(y \in range f) y * \1_(f @^-1` [set y]) x)%R) + \* (fun x => (\sum_(y \in range g) y * \1_(g @^-1` [set y]) x)%R)]). + by congr ('E_P [_]); apply/funext => t/=; rewrite (fimfunE f) (fimfunE g). +transitivity ('E_P [(fun x => (\sum_(y \in range f) \sum_(y' \in range g) y * y' + * \1_(f @^-1` [set y] `&` g @^-1` [set y']) x)%R)]). + congr ('E_P [_]); apply/funext => t/=. + rewrite mulrC; rewrite fsbig_distrr//=. (* TODO: lemma fsbig_distrl *) + apply: eq_fsbigr => y yf; rewrite mulrC; rewrite fsbig_distrr//=. + by apply: eq_fsbigr => y' y'g; rewrite indicI mulrCA !mulrA (mulrC y'). +rewrite unlock. +under eq_integral do rewrite -fsumEFin//. +transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + ((y * y')%:E * \int[P]_w (\1_(f @^-1` [set y] `&` g @^-1` [set y']) w)%:E))). + rewrite ge0_integral_fsum//=; last 2 first. + - move=> r; under eq_fun do rewrite -fsumEFin//. + apply: emeasurable_fun_fsum => // s. + apply/measurable_EFinP/measurable_funM => //. + exact/measurable_indic/measurableI. + - move=> r t _; rewrite lee_fin sumr_ge0 // => s _; rewrite -lee_fin. + by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. + apply: eq_fsbigr => y yf. + under eq_integral do rewrite -fsumEFin//. + rewrite ge0_integral_fsum//=; last 2 first. + - move=> r; apply/measurable_EFinP; apply: measurable_funM => //. + exact/measurable_indic/measurableI. + - move=> r t _. + by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. + apply: eq_fsbigr => y' y'g. + under eq_integral do rewrite EFinM. + by rewrite integralZl//; exact/integrable_indic/measurableI. +transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + ((y * y')%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E * + \int[P]_w (\1_(g @^-1` [set y']) w)%:E)))). + apply: eq_fsbigr => y fy; apply: eq_fsbigr => y' gy'; congr *%E. + transitivity ('E_P[\1_(f @^-1` [set y] `&` g @^-1` [set y'])]). + by rewrite unlock. + transitivity ('E_P[\1_(f @^-1` [set y])] * 'E_P[\1_(g @^-1` [set y'])]); + last by rewrite unlock. + rewrite expectation_indic//; last exact: measurableI. + by rewrite !expectation_indic// fg. +transitivity ( + (\sum_(y \in range f) (y%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E))) * + (\sum_(y' \in range g) (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E))). + transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E)%E)%R * + (y%:E * \int[P]_w (\1_(f @^-1` [set y]) w)%:E)%E%R); last first. + rewrite !fsbig_finite//= ge0_sume_distrl//; last first. + move=> r _; rewrite -integralZl//; last exact: integrable_indic. + by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. + by apply: eq_bigr => r _; rewrite muleC. + apply: eq_fsbigr => y fy. + rewrite !fsbig_finite//= ge0_sume_distrl//; last first. + move=> r _; rewrite -integralZl//; last exact: integrable_indic. + by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. + apply: eq_bigr => r _; rewrite (mulrC y) EFinM. + by rewrite [X in _ * X]muleC muleACA. +suff: forall h : {nnsfun T >-> R}, + (\sum_(y \in range h) (y%:E * \int[P]_w (\1_(h @^-1` [set y]) w)%:E)%E)%R + = \int[P]_w (h w)%:E. + by move=> suf; congr *%E; rewrite suf. +move=> h. +apply/esym. +under eq_integral do rewrite (fimfunE h). +under eq_integral do rewrite -fsumEFin//. +rewrite ge0_integral_fsum//; last 2 first. +- by move=> r; exact/measurable_EFinP/measurable_funM. +- by move=> r t _; rewrite lee_fin -lee_fin nnfun_muleindic_ge0. +by apply: eq_fsbigr => y fy; rewrite -integralZl//; exact/integrable_indic. +Qed. + +Lemma expectationM_ge0 (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + 'E_P[X] *? 'E_P[Y] -> + (forall t, 0 <= X t)%R -> (forall t, 0 <= Y t)%R -> + 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> indeXY defXY X0 Y0. +have mX : measurable_fun setT (EFin \o X) by exact/measurable_EFinP. +have mY : measurable_fun setT (EFin \o Y) by exact/measurable_EFinP. +pose X_ := nnsfun_approx measurableT mX. +pose Y_ := nnsfun_approx measurableT mY. +have EXY : 'E_P[X_ n \* Y_ n] @[n --> \oo] --> 'E_P [X * Y]. + rewrite unlock; have -> : \int[P]_w ((X * Y) w)%:E = + \int[P]_x limn (fun n => (EFin \o (X_ n \* Y_ n)%R) x). + apply: eq_integral => t _; apply/esym/cvg_lim => //=. + rewrite fctE EFinM; under eq_fun do rewrite EFinM. + by apply: cvgeM; [rewrite mule_def_fin//| + apply: cvg_nnsfun_approx => //= x _; rewrite lee_fin..]. + apply: cvg_monotone_convergence => //. + - by move=> n; apply/measurable_EFinP; exact: measurable_funM. + - by move=> n t _; rewrite lee_fin. + - move=> t _ m n mn. + by rewrite lee_fin/= ler_pM//; exact/lefP/nd_nnsfun_approx. +have EX : 'E_P[X_ n] @[n --> \oo] --> 'E_P [X]. + rewrite unlock. + have -> : \int[P]_w (X w)%:E = \int[P]_x limn (fun n => (EFin \o X_ n) x). + by apply: eq_integral => t _; apply/esym/cvg_lim => //=; + apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n t _; rewrite lee_fin. + - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. +have EY : 'E_P[Y_ n] @[n --> \oo] --> 'E_P [Y]. + rewrite unlock. + have -> : \int[P]_w (Y w)%:E = \int[P]_x limn (fun n => (EFin \o Y_ n) x). + by apply: eq_integral => t _; apply/esym/cvg_lim => //=; + apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n t _; rewrite lee_fin. + - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. +have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[n --> \oo] --> 'E_P[X] * 'E_P[Y]. + apply: cvgeM => //. +suff : forall n, 'E_P[X_ n \* Y_ n] = 'E_P[X_ n] * 'E_P[Y_ n]. + by move=> suf; apply: (cvg_unique _ EXY) => //=; under eq_fun do rewrite suf. +move=> n; apply: expectationM_nnsfun => x y xX_ yY_. +suff : P (\big[setI/setT]_(j <- [fset false; true]%fset) + [eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], + 1%N |-> Y_ n @^-1` [set y]] j) = + \prod_(j <- [fset false; true]%fset) + P ([eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], + 1%N |-> Y_ n @^-1` [set y]] j). + by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=. +move: indeXY => [/= _]; apply => // i. +pose AX := approx_A setT (EFin \o X). +pose AY := approx_A setT (EFin \o Y). +pose BX := approx_B setT (EFin \o X). +pose BY := approx_B setT (EFin \o Y). +have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> + g_sigma_algebra_mapping Z (approx_A setT (EFin \o Z) m k). + move=> mk; rewrite /g_sigma_algebra_mapping /approx_A mk setTI. + rewrite /preimage_class/=; exists [set` dyadic_itv R m k] => //. + rewrite setTI/=; apply/seteqP; split => z/=. + by rewrite inE/= => Zz; exists (Z z). + by rewrite inE/= => -[r rmk] [<-]. +have mB (Z : {RV P >-> R}) k : + g_sigma_algebra_mapping Z (approx_B setT (EFin \o Z) k). + rewrite /g_sigma_algebra_mapping /approx_B setTI /preimage_class/=. + by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itv_c_infty. +have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> + measurable_fun setT + (\1_(approx_A setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R). + move=> k kn. + exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA. +rewrite !inE => /orP[|]/eqP->{i} //=. + have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_fun_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. + rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). + by rewrite setTI. +have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_fun_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. +move=> /(_ measurableT [set y] (measurable_set1 y)). +by rewrite setTI. +Qed. + +Lemma integrable_expectationM000 (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + `|'E_P [X * Y]| < +oo. +Proof. +move=> indeXY iX iY. +apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). + rewrite unlock/=. + rewrite (le_trans (le_abse_integral _ _ _))//. + apply/measurable_EFinP/measurable_funM. + by have /measurable_EFinP := measurable_int _ iX. + by have /measurable_EFinP := measurable_int _ iY. + apply: ge0_le_integral => //=. + - by apply/measurable_EFinP; exact/measurableT_comp. + - by move=> x _; rewrite lee_fin/= mulr_ge0/=. + - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp. + - by move=> t _; rewrite lee_fin/= normrM. +rewrite expectationM_ge0//=. +- rewrite lte_mul_pinfty//. + + by rewrite expectation_ge0/=. + + rewrite expectation_fin_num//= compA//. + exact: (integrable_abse iX). + + by move/integrableP : iY => [_ iY]; rewrite unlock. +- exact: independent_RVs2_comp. +- apply: mule_def_fin; rewrite unlock integral_fune_fin_num//. + + exact: (integrable_abse iX). + + exact: (integrable_abse iY). +Qed. + +Lemma independent_integrableM (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + P.-integrable setT (EFin \o (X \* Y)%R). +Proof. +move=> indeXY iX iY. +apply/integrableP; split; first exact/measurable_EFinP/measurable_funM. +have := integrable_expectationM000 indeXY iX iY. +rewrite unlock => /abse_integralP; apply => //. +exact/measurable_EFinP/measurable_funM. +Qed. + +(* TODO: rename to expectationM when deprecation is removed *) +Lemma expectation_prod (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> XY iX iY. +transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]). + congr ('E_P[_]). + apply/funext => /=t. + by rewrite [in LHS](funrposneg X)/= [in LHS](funrposneg Y). +have ? : P.-integrable [set: T] (EFin \o X^\-%R). + by rewrite -funerneg; exact/integrable_funeneg. +have ? : P.-integrable [set: T] (EFin \o X^\+%R). + by rewrite -funerpos; exact/integrable_funepos. +have ? : P.-integrable [set: T] (EFin \o Y^\+%R). + by rewrite -funerpos; exact/integrable_funepos. +have ? : P.-integrable [set: T] (EFin \o Y^\-%R). + by rewrite -funerneg; exact/integrable_funeneg. +have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\+)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrpospos. +have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\+)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegpos. +have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\-)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrposneg. +have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\-)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegneg. +transitivity ('E_P[X^\+ * Y^\+] - 'E_P[X^\- * Y^\+] + - 'E_P[X^\+ * Y^\-] + 'E_P[X^\- * Y^\-]). + rewrite mulrDr !mulrDl -expectationB//= -expectationB//=; last first. + rewrite (_ : _ \o _ = EFin \o (X^\+ \* Y^\+)%R \- + (EFin \o (X^\- \* Y^\+)%R))//. + exact: integrableB. + rewrite -expectationD//=; last first. + rewrite (_ : _ \o _ = (EFin \o (X^\+ \* Y^\+)%R) + \- (EFin \o (X^\- \* Y^\+)%R) \- (EFin \o (X^\+ \* Y^\-)%R))//. + by apply: integrableB => //; exact: integrableB. + congr ('E_P[_]); apply/funext => t/=. + by rewrite !fctE !(mulNr,mulrN,opprK,addrA)/=. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrpospos. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrnegpos. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrposneg. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrnegneg. + by rewrite mule_def_fin// expectation_fin_num//=. +transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]). + rewrite -addeA -addeACA -muleBr; last 2 first. + by rewrite expectation_fin_num. + by rewrite fin_num_adde_defr// expectation_fin_num. + rewrite -oppeB; last first. + by rewrite fin_num_adde_defr// fin_numM// expectation_fin_num. + rewrite -muleBr; last 2 first. + by rewrite expectation_fin_num. + by rewrite fin_num_adde_defr// expectation_fin_num. + rewrite -muleBl; last 2 first. + by rewrite fin_numB// !expectation_fin_num//. + by rewrite fin_num_adde_defr// expectation_fin_num. + by rewrite -expectationB//= -expectationB. +by congr *%E; congr ('E_P[_]); rewrite [RHS]funrposneg. +Qed. + +(*Lemma independent_RVsS n (X : {RV P >-> R}^nat) : + independent_RVs P n.+1 X -> independent_RVs P n X. +Proof. +move=> [/= mPnX PnX]. +rewrite /independent_RVs /mutual_independence/=; split. + by move=> i ni A /mPnX; rewrite ltnS//; apply; exact: ltnW. +by move=> J Jn E JE; apply: PnX => // i /Jn/= /ltnW. +Qed. +*) +Lemma prodE (s : seq nat) (X : {RV P >-> R}^nat) (t : T) : + (\prod_(i <- s) X i t)%R = ((\prod_(j <- s) X j)%R t). +Proof. +by elim/big_ind2 : _ => //= {}X x {}Y y -> ->. +Qed. + +Lemma set_cons2 (I : eqType) (x y : I) : [set` [:: x; y]] = [set x ; y]. +Proof. +apply/seteqP; split => z /=; rewrite !inE. + move=> /orP[|] /eqP ->; auto. +by move=> [|] ->; rewrite eqxx// orbT. +Qed. + +Lemma independent_RVsD1 (I : {fset nat}) i0 (X : {RV P >-> R}^nat) : + independent_RVs P [set` I] X -> independent_RVs P [set` (I `\ i0)%fset] X. +Proof. +move=> H. +split => [/= i|/= J JIi0 E EK]. + rewrite !inE => /andP[ii0 iI]. + by apply H. +apply H => //. +by move=> /= x /JIi0 /=; rewrite !inE => /andP[]. +Qed. + +Lemma independent_integrable_prod (I : {fset nat}) (X : {RV P >-> R}^nat) : + independent_RVs P [set` I] X -> + (forall i, i \in I -> P.-integrable setT (EFin \o X i)) -> + P.-integrable setT (EFin \o (\prod_(i <- I) X i)%R). +Proof. +apply: (@finSet_rect _ (fun I => independent_RVs P [set` I] X -> + (forall i : nat, i \in I -> P.-integrable [set: T] (EFin \o X i)) -> + P.-integrable [set: T] (EFin \o (\prod_(i <- I) X i)%R))) => /=. +move=> {}I ih indeX iX. +have [->{I ih indeX iX}|/fset0Pn[i0 i0I]] := eqVneq I fset0. + rewrite big_nil/=. + apply/integrableP; split => //=. + exact/measurable_EFinP. + under eq_integral. + move=> x _. + rewrite (_ : _%:E = cst 1 x)//=; last first. + by rewrite normr1. + over. + rewrite integral_cst// mul1e. + by rewrite [ltLHS]probability_setT ltry. +have IE := fsetD1K i0I. +rewrite -IE big_fsetU1/=; last by rewrite !inE/= eqxx. +rewrite (_ : _ \o _ = (EFin \o X i0) \* (EFin \o (\prod_(j <- (I `\ i0)%fset) X j)%R))//. +apply: independent_integrableM; last 2 first. + exact: iX. + apply: ih => //. + by rewrite fproperD1. + by apply: independent_RVsD1 => //. + move=> i iIi0. + apply: iX. + by move: iIi0; rewrite !inE => /andP[]. +have [|/fset0Pn[i1]] := eqVneq (I `\ i0)%fset fset0. + move=> Ii00. + have IE' : I = [fset i0]%fset by rewrite -IE Ii00 fsetU0. + rewrite Ii00 big_nil. + move: indeX. + rewrite IE' set_fset1. + rewrite /independent_RVs2 => indeX. + split => /=. + move=> [|]/= _. + move=> A [/= B mB] <-. + rewrite setTI. + rewrite preimage_cst. + by case: ifPn. + move=> A [/= B mB] <-. + have := measurable_funP (X i0). + exact. + move=> J + E EJ. + rewrite setT_bool => JT. + have [/eqP| | |] := subset_set2 JT. + - rewrite set_seq_eq0 => /eqP ->. + by rewrite !big_nil probability_setT. + - move=> J0. + rewrite -bigcap_fset J0 bigcap_set1. + by rewrite -(set_fsetK J) J0 fset_set1 big_seq_fset1. + - move=> J1. + rewrite -bigcap_fset J1 bigcap_set1. + by rewrite -(set_fsetK J) J1 fset_set1 big_seq_fset1. + - move=> JE. + clear indeX. + rewrite -bigcap_fset JE !bigcap_setU1 bigcap_set1. + rewrite -(set_fsetK J) JE !fset_setU1// fset_set1. + rewrite !big_fsetU1 ?inE//= big_seq_fset1. + have : g_sigma_algebra_mapping (X i0) (E false). + have /= := EJ false. + rewrite inE. + apply. + by rewrite -(set_fsetK J) JE in_fset_set// !inE/=; right. + case => B mB <-. + have : g_sigma_algebra_mapping (1%R : {RV P >-> R}) (E true). + have /= := EJ true. + rewrite inE. + apply. + by rewrite -(set_fsetK J) JE in_fset_set// !inE/=; left. + case => C mC <-. + rewrite !setTI. + rewrite !preimage_cst. + case: ifPn => C1. + by rewrite !setTI probability_setT mul1e. + by rewrite set0I measure0 mul0e. +rewrite !inE => /andP[i10 i1I]. +split => /=. + move=> [|]/= _. + move=> A [/= B mB] <-. + have : measurable_fun [set: T] (fun x : T => (\prod_(i <- (I `\ i0)%fset) X i x)%R). + by apply: measurable_fun_prod => //=. + move=> /(_ measurableT _ mB). + congr (_ _). + by rewrite !setTI; apply/seteqP; split => t/=; rewrite prodE. + move=> A [/= B mB] <-. + have := measurable_funP (X i0). + exact. +move=> J + E EJ. +rewrite setT_bool => JT. +have [/eqP| | |] := subset_set2 JT. +- rewrite set_seq_eq0 => /eqP ->. + by rewrite !big_nil probability_setT. +- move=> J0. + rewrite -bigcap_fset J0 bigcap_set1. + by rewrite -(set_fsetK J) J0 fset_set1 big_seq_fset1. +- move=> J1. + rewrite -bigcap_fset J1 bigcap_set1. + by rewrite -(set_fsetK J) J1 fset_set1 big_seq_fset1. +- move=> JE. + rewrite -bigcap_fset JE !bigcap_setU1 bigcap_set1. + rewrite -(set_fsetK J) JE !fset_setU1// fset_set1. + rewrite !big_fsetU1 ?inE//= big_seq_fset1. + have Efalse : g_sigma_algebra_mapping (X i0) (E false). + have /= := EJ false. + rewrite inE. + apply. + by rewrite -(set_fsetK J) JE in_fset_set// !inE/=; right. + have Etrue : g_sigma_algebra_mapping + ((\prod_(j <- (I `\ i0)%fset) X j)%R : {RV P >-> R}) (E true). + have /= := EJ true. + rewrite inE. + apply. + by rewrite -(set_fsetK J) JE in_fset_set// !inE/=; left. + clear EJ. + have ? : d.-measurable (E true). + move: Etrue. + move=> [/= B mB] <-. + have : (forall n : Datatypes_nat__canonical__choice_Choice, + n \in (I `\ i0)%fset -> measurable_fun [set: T] (X n)). + move=> n ?. + by apply: measurable_funP. + move=> /(@measurable_fun_prod _ _ _ setT _ (I `\ i0)%fset X). + move=> /(_ measurableT _ mB). + rewrite (_ : (fun x : T => (\prod_(i <- (I `\ i0)%fset) X i x)%R) = + (\prod_(j <- (I `\ i0)%fset) X j)%R); last first. + apply/funext => t. + by rewrite -prodE. + done. + case: indeX => /= H indeX. + pose J' := I. + have J'I : [set` J'] `<=` [set` I]. + by []. + case: Efalse => /= B mB; rewrite setTI => Efalse. + case: Etrue => /= C mC; rewrite setTI => Etrue. + pose E' (i : nat) := if i == i0 then X i0 @^-1` B else X i @^-1` C. + have E'J i : i \in J' -> E' i \in g_sigma_algebra_mapping (X i). + rewrite inE. + rewrite /J' -IE !inE => /orP[/eqP ->|]. + exists B => //. + by rewrite setTI /E' eqxx. + move/andP => [ii0 iI]. + rewrite /E' (negbTE ii0). + exists C => //. + by rewrite setTI. + have := indeX _ J'I _ E'J. + rewrite /J'. + rewrite -IE. + rewrite !big_fsetU1/=; last 2 first. + by rewrite !inE eqxx. + by rewrite !inE eqxx. + rewrite (_ : E' i0 = E false); last first. + by rewrite /E' eqxx -Efalse. + rewrite (_ : \big[setI/[set: T]]_(i <- (I `\ i0)%fset) E' i = + \big[setI/[set: T]]_(i <- (I `\ i0)%fset) (X i @^-1` C)); last first. + rewrite big_seq [RHS]big_seq. + apply/eq_bigr => /= i; rewrite !inE => /andP[ii0 _]. + by rewrite /E' (negbTE ii0). + rewrite (_ : \prod_(i <- (I `\ i0)%fset) P (E' i) = + \prod_(i <- (I `\ i0)%fset) P (X i @^-1` C)); last first. + rewrite big_seq [RHS]big_seq. + apply/eq_bigr => /= i; rewrite !inE => /andP[ii0 _]. + by rewrite /E' (negbTE ii0). + rewrite -indeX; last 2 first. + by move=> z/=; rewrite !inE/= => /andP[]. + move=> i ii0. + rewrite inE. + exists C => //. + by rewrite setTI. +have K : \big[setI/[set: T]]_(i <- (I `\ i0)%fset) X i @^-1` C = + (\prod_(j <- (I `\ i0)%fset) X j)%R @^-1` C. + admit. + rewrite K Etrue. + by rewrite setIC muleC. +Abort. + +End product_expectation. + Section bernoulli_pmf. Context {R : realType} (p : R). Local Open Scope ring_scope. @@ -1323,21 +2190,21 @@ Lemma integral_uniform (f : _ -> \bar R) : (\int[uniform_prob ab]_x f x = (b - a)^-1%:E * \int[mu]_(x in `[a, b]) f x)%E. Proof. move=> mf f0. -have [f_ [ndf_ f_f]] := approximation measurableT mf (fun y _ => f0 y). +pose f_ := nnsfun_approx measurableT mf. transitivity (lim (\int[uniform_prob ab]_x (f_ n x)%:E @[n --> \oo])%E). rewrite -monotone_convergence//=. - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //=. - exact: f_f. + exact/cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n ? _; rewrite lee_fin. - - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/ndf_. + - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. rewrite [X in _ = (_ * X)%E](_ : _ = lim (\int[mu]_(x in `[a, b]) (f_ n x)%:E @[n --> \oo])%E); last first. rewrite -monotone_convergence//=. - - by apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f. + - by apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n ? _; rewrite lee_fin. - - by move=> ? _ ? ? /ndf_ /lefP; rewrite lee_fin. + - by move=> ? _ u v uv; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. rewrite -limeMl//. by apply: congr_lim; apply/funext => n /=; exact: integral_uniform_nnsfun. apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. @@ -1345,7 +2212,7 @@ apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. - exact/measurable_EFinP/measurable_funTS. - by move=> ? _; rewrite lee_fin. - exact/measurable_EFinP/measurable_funTS. -- by move=> ? _; rewrite lee_fin; move/ndf_ : xy => /lefP. +- by move=> ? _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. Qed. End uniform_probability. diff --git a/theories/realfun.v b/theories/realfun.v index ebf570f540..b11415d1c1 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1,12 +1,12 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum archimedean. From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality ereal reals signed. -From mathcomp Require Import topology prodnormedzmodule normedtype derive. +From mathcomp Require Import topology prodnormedzmodule tvs normedtype derive. From mathcomp Require Import sequences real_interval. -From HB Require Import structures. (**md**************************************************************************) (* # Real-valued functions over reals *) @@ -1435,10 +1435,10 @@ have := xb; rewrite le_eqVlt => /orP[/eqP {}xb {ax}|{}xb]. have xoab : x \in `]a, b[ by rewrite in_itv /=; apply/andP; split. near=> y; suff: l <= f y <= u. by rewrite ge_max le_min -!andbA => /and4P[-> _ ->]. -have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; apply: near_in_itv. +have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; exact: near_in_itvoo. have fyab : f y \in `[f a, f b] by rewrite in_itv/= !fle// ?ltW. rewrite -[l <= _]gle -?[_ <= u]gle// ?fK //. -apply: subset_itv_oo_cc; near: y; apply: near_in_itv; rewrite in_itv /=. +apply: subset_itv_oo_cc; near: y; apply: near_in_itvoo; rewrite in_itv /=. rewrite -[x]fK // !glt//= lt_min gt_max ?andbT ltrBlDr ltr_pwDr //. by apply/and3P; split; rewrite // flt. Unshelve. all: by end_near. Qed. diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index afd1f4ad60..c136e2bfdf 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -1139,7 +1139,7 @@ rewrite {}ji {j} in x y cl *. congr existT; apply: hX => U V Ux Vy. have [] := cl (existT X i @` U) (existT X i @` V); [exact: existT_nbhs..|]. move=> z [] [l Ul <-] [r Vr lr]; exists l; split => //. -by rewrite -(existT_inj lr). +by rewrite -(existT_inj2 lr). Qed. End sigT_separations. diff --git a/theories/sequences.v b/theories/sequences.v index bbff8a6244..1e803af799 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -3,8 +3,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import set_interval. -From mathcomp Require Import reals ereal signed topology normedtype landau. +From mathcomp Require Import set_interval reals ereal signed topology. +From mathcomp Require Import tvs normedtype landau. (**md**************************************************************************) (* # Definitions and lemmas about sequences *) @@ -1123,7 +1123,7 @@ move=> k0 kfK; have [K0|K0] := lerP K 0. near: x; exists (k / 2); first by rewrite /mkset divr_gt0. move=> t /=; rewrite distrC subr0 => tk2 t0. by rewrite normr_gt0 t0 (lt_trans tk2) // -[in ltLHS](add0r k) midf_lt. -- apply/(@eqolim0 _ _ R (0^'))/eqoP => _/posnumP[e]; near=> x. +- apply/(@eqolim0 _ _ R 0^')/eqoP => _/posnumP[e]; near=> x. rewrite (le_trans (kfK _ _)) //=. + near: x; exists (k / 2); first by rewrite /mkset divr_gt0. move=> t /=; rewrite distrC subr0 => tk2 t0. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 5e78bde1cd..8eaf56dbb5 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -105,6 +105,10 @@ HB.structure Definition Topological := HB.structure Definition PointedTopological := {T of PointedNbhs T & Nbhs_isTopological T}. +#[short(type="bpTopologicalType")] +HB.structure Definition BiPointedTopological := + { X of BiPointed X & Topological X }. + Section Topological1. Context {T : topologicalType}. diff --git a/theories/topology_theory/weak_topology.v b/theories/topology_theory/weak_topology.v index 184a1ba23c..0b13ca98dc 100644 --- a/theories/topology_theory/weak_topology.v +++ b/theories/topology_theory/weak_topology.v @@ -211,3 +211,11 @@ move=> [][][[]l|[]] [[]r|[]][][]//= _ xlr /filterS; apply. Qed. End weak_order_refine. + +Lemma continuous_comp_weak {Y : choiceType} {X Z : topologicalType} (w : Y -> Z) + (f : X -> weak_topology w) : + continuous (w \o f) -> continuous f. +Proof. +move=> cf z U [?/= [[W oW <-]]] /= Wsfz /filterS; apply; apply: cf. +exact: open_nbhs_nbhs. +Qed. diff --git a/theories/trigo.v b/theories/trigo.v index cfcd3db867..39bebecc98 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -1003,7 +1003,7 @@ move=> /andP[x_gtN1 x_lt1]; rewrite -[x]acosK; first last. by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB. apply: nbhs_singleton (near_can_continuous _ _); last first. by near=> z; apply: continuous_cos. -have /near_in_itv aI : acos x \in `]0, pi[. +have /near_in_itvoo aI : acos x \in `]0, pi[. suff : 0 < acos x < pi by []. by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT. near=> z; apply: cosK. @@ -1016,7 +1016,7 @@ Lemma is_derive1_acos x : Proof. move=> /andP[x_gtN1 x_lt1]; rewrite -sin_acos ?ltW // -invrN. rewrite -{1}[x]acosK; last by have : -1 <= x <= 1 by rewrite ltW // ltW. -have /near_in_itv aI : acos x \in `]0, pi[. +have /near_in_itvoo aI : acos x \in `]0, pi[. suff : 0 < acos x < pi by []. by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT. apply: (@is_derive_inverse R cos). @@ -1103,7 +1103,7 @@ move=> /andP[x_gtN1 x_lt1]; rewrite -[x]asinK; first last. by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB. apply: nbhs_singleton (near_can_continuous _ _); last first. by near=> z; apply: continuous_sin. -have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[. +have /near_in_itvoo aI : asin x \in `](-(pi/2)), (pi/2)[. suff : - (pi / 2) < asin x < pi / 2 by []. by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW. near=> z; apply: sinK. @@ -1117,7 +1117,7 @@ Lemma is_derive1_asin x : Proof. move=> /andP[x_gtN1 x_lt1]; rewrite -cos_asin ?ltW //. rewrite -{1}[x]asinK; last by have : -1 <= x <= 1 by rewrite ltW // ltW. -have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[. +have /near_in_itvoo aI : asin x \in `](-(pi/2)), (pi/2)[. suff : -(pi/2) < asin x < pi/2 by []. by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW. apply: (@is_derive_inverse R sin). @@ -1219,7 +1219,7 @@ Qed. Lemma continuous_atan x : {for x, continuous (@atan R)}. Proof. rewrite -[x]atanK. -have /near_in_itv aI : atan x \in `](-(pi / 2)), (pi / 2)[. +have /near_in_itvoo aI : atan x \in `](-(pi / 2)), (pi / 2)[. suff : - (pi / 2) < atan x < pi / 2 by []. by rewrite atan_gtNpi2 atan_ltpi2. apply: nbhs_singleton (near_can_continuous _ _); last first. @@ -1244,7 +1244,7 @@ Proof. rewrite -{1}[x]atanK. have cosD0 : cos (atan x) != 0. by apply/lt0r_neq0/cos_gt0_pihalf; rewrite atan_gtNpi2 atan_ltpi2. -have /near_in_itv aI : atan x \in `](-(pi/2)), (pi/2)[. +have /near_in_itvoo aI : atan x \in `](-(pi/2)), (pi/2)[. suff : - (pi / 2) < atan x < pi / 2 by []. by rewrite atan_gtNpi2 atan_ltpi2. apply: (@is_derive_inverse R tan). diff --git a/theories/tvs.v b/theories/tvs.v new file mode 100644 index 0000000000..d03357bef1 --- /dev/null +++ b/theories/tvs.v @@ -0,0 +1,419 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. +From mathcomp Require Import rat interval zmodp vector fieldext falgebra. +From mathcomp Require Import archimedean. +From mathcomp Require Import boolp classical_sets functions cardinality. +From mathcomp Require Import set_interval ereal reals signed topology. +From mathcomp Require Import prodnormedzmodule function_spaces. +From mathcomp Require Import separation_axioms. + +(**md**************************************************************************) +(* # Topological vector spaces *) +(* *) +(* This file introduces locally convex topological vector spaces. *) +(* ``` *) +(* NbhsNmodule == HB class, join of Nbhs and Nmodule *) +(* NbhsZmodule == HB class, join of Nbhs and Zmodule *) +(* NbhsLmodule K == HB class, join of Nbhs and Lmodule over K *) +(* K is a numDomainType. *) +(* TopologicalNmodule == HB class, joint of Topological and Nmodule *) +(* TopologicalZmodule == HB class, joint of Topological and Zmodule *) +(* topologicalLmodType K == topological space and Lmodule over K *) +(* K is a numDomainType. *) +(* The HB class is TopologicalLmodule. *) +(* UniformZmodule == HB class, joint of Uniform and Zmodule *) +(* UniformLmodule K == HB class, joint of Uniform and Lmodule over K *) +(* K is a numDomainType. *) +(* convex A == A : set M is a convex set of elements of M *) +(* M is an Lmodule over R : numDomainType. *) +(* tvsType R == interface type for a locally convex topological *) +(* vector space on a numDomain R *) +(* A tvs is constructed over a uniform space. *) +(* The HB class is Tvs. *) +(* TopologicalLmod_isTvs == factory allowing the construction of a tvs from *) +(* an Lmodule which is also a topological space. *) +(* ``` *) +(* HB instances: *) +(* - The type R^o (R : numFieldType) is endowed with the structure of Tvs. *) +(* - The product of two Tvs is endowed with the structure of Tvs. *) +(******************************************************************************) + +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.structure Definition PointedNmodule := {M of Pointed M & GRing.Nmodule M}. *) +(* HB.structure Definition PointedZmodule := {M of Pointed M & GRing.Zmodule M}. *) +(* HB.structure Definition PointedLmodule (K : numDomainType) := *) +(* {M of Pointed M & GRing.Lmodule K M}. *) + +(* HB.structure Definition FilteredNmodule := {M of Filtered M M & GRing.Nmodule M}. *) +(* HB.structure Definition FilteredZmodule := {M of Filtered M M & GRing.Zmodule M}. *) +(* HB.structure Definition FilteredLmodule (K : numDomainType) := *) +(* {M of Filtered M M & GRing.Lmodule K M}. *) +HB.structure Definition NbhsNmodule := {M of Nbhs M & GRing.Nmodule M}. +HB.structure Definition NbhsZmodule := {M of Nbhs M & GRing.Zmodule M}. +HB.structure Definition NbhsLmodule (K : numDomainType) := + {M of Nbhs M & GRing.Lmodule K M}. + +HB.structure Definition TopologicalNmodule := + {M of Topological M & GRing.Nmodule M}. +HB.structure Definition TopologicalZmodule := + {M of Topological M & GRing.Zmodule M}. + +#[short(type="topologicalLmodType")] +HB.structure Definition TopologicalLmodule (K : numDomainType) := + {M of Topological M & GRing.Lmodule K M}. + +HB.structure Definition UniformZmodule := {M of Uniform M & GRing.Zmodule M}. +HB.structure Definition UniformLmodule (K : numDomainType) := + {M of Uniform M & GRing.Lmodule K M}. + +Definition convex (R : numDomainType) (M : lmodType R) (A : set M) := + forall x y (lambda : R), x \in A -> y \in A -> + 0 < lambda -> lambda < 1 -> lambda *: x + (1 - lambda) *: y \in A. + +HB.mixin Record Uniform_isTvs (R : numDomainType) E + of Uniform E & GRing.Lmodule R E := { + add_continuous : continuous (fun x : E * E => x.1 + x.2) ; + scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ; + locally_convex : exists2 B : set (set E), + (forall b, b \in B -> convex b) & basis B +}. + +#[short(type="tvsType")] +HB.structure Definition Tvs (R : numDomainType) := + {E of Uniform_isTvs R E & Uniform E & GRing.Lmodule R E}. + +Section properties_of_topologicalLmodule. +Context (R : numDomainType) (E : topologicalLmodType R) (U : set E). + +Lemma nbhsN_subproof (f : continuous (fun z : R^o * E => z.1 *: z.2)) (x : E) : + nbhs x U -> nbhs (-x) (-%R @` U). +Proof. +move=> Ux; move: (f (-1, -x) U); rewrite /= scaleN1r opprK => /(_ Ux) [] /=. +move=> [B] B12 [B1 B2] BU; near=> y; exists (- y); rewrite ?opprK// -scaleN1r//. +apply: (BU (-1, y)); split => /=; last by near: y. +by move: B1 => [] ? ?; apply => /=; rewrite subrr normr0. +Unshelve. all: by end_near. Qed. + +Lemma nbhs0N_subproof (f : continuous (fun z : R^o * E => z.1 *: z.2)) : + nbhs 0 U -> nbhs 0 (-%R @` U). +Proof. by move => Ux; rewrite -oppr0; exact: nbhsN_subproof. Qed. + +Lemma nbhsT_subproof (f : continuous (fun x : E * E => x.1 + x.2)) (x : E) : + nbhs 0 U -> nbhs x (+%R x @` U). +Proof. +move => U0; have /= := f (x, -x) U; rewrite subrr => /(_ U0). +move=> [B] [B1 B2] BU; near=> x0. +exists (x0 - x); last by rewrite addrCA subrr addr0. +by apply: (BU (x0, -x)); split; [near: x0; rewrite nearE|exact: nbhs_singleton]. +Unshelve. all: by end_near. Qed. + +Lemma nbhsB_subproof (f : continuous (fun x : E * E => x.1 + x.2)) (z x : E) : + nbhs z U -> nbhs (x + z) (+%R x @` U). +Proof. +move=> U0; have /= := f (x + z, -x) U; rewrite addrAC subrr add0r. +move=> /(_ U0)[B] [B1 B2] BU; near=> x0. +exists (x0 - x); last by rewrite addrCA subrr addr0. +by apply: (BU (x0, -x)); split; [near: x0; rewrite nearE|exact: nbhs_singleton]. +Unshelve. all: by end_near. Qed. + +End properties_of_topologicalLmodule. + +HB.factory Record TopologicalLmod_isTvs (R : numDomainType) E + of Topological E & GRing.Lmodule R E := { + add_continuous : continuous (fun x : E * E => x.1 + x.2) ; + scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ; + locally_convex : exists2 B : set (set E), + (forall b, b \in B -> convex b) & basis B + }. + +HB.builders Context R E of TopologicalLmod_isTvs R E. + +Definition entourage : set_system (E * E) := + fun P => exists (U : set E), nbhs (0 : E) U /\ + (forall xy : E * E, (xy.1 - xy.2) \in U -> xy \in P). + +Let nbhs0N (U : set E) : nbhs (0 : E) U -> nbhs (0 : E) (-%R @` U). +Proof. by apply: nbhs0N_subproof; exact: scale_continuous. Qed. + +Lemma nbhsN (U : set E) (x : E) : nbhs x U -> nbhs (-x) (-%R @` U). +Proof. by apply: nbhsN_subproof; exact: scale_continuous. Qed. + +Let nbhsT (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U). +Proof. by apply: nbhsT_subproof; exact: add_continuous. Qed. + +Let nbhsB (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @`U). +Proof. by apply: nbhsB_subproof; exact: add_continuous. Qed. + +Lemma entourage_filter : Filter entourage. +Proof. +split; first by exists [set: E]; split => //; exact: filter_nbhsT. +- move=> P Q; rewrite /entourage nbhsE //=. + move=> [U [[B B0] BU Bxy]] [V [[C C0] CV Cxy]]. + exists (U `&` V); split. + by exists (B `&` C); [exact: open_nbhsI|exact: setISS]. + move=> xy; rewrite !in_setI => /andP[xyU xyV]. + by apply/andP;split; [exact: Bxy|exact: Cxy]. +- move=> P Q PQ; rewrite /entourage /= => [[U [HU Hxy]]]; exists U; split=> //. + by move => xy /Hxy /[!inE] /PQ. +Qed. + +Local Lemma entourage_refl (A : set (E * E)) : + entourage A -> [set xy | xy.1 = xy.2] `<=` A. +Proof. +rewrite /entourage => -[/= U [U0 Uxy]] xy /eqP; rewrite -subr_eq0 => /eqP xyE. +by apply/set_mem/Uxy; rewrite xyE; apply/mem_set; exact: nbhs_singleton. +Qed. + +Local Lemma entourage_inv : + forall A : set (E * E), entourage A -> entourage A^-1%relation. +Proof. +move=> A [/= U [U0 Uxy]]; rewrite /entourage /=. +exists (-%R @` U); split; first exact: nbhs0N. +move=> xy /set_mem /=; rewrite -opprB => [[yx] Uyx] /oppr_inj yxE. +by apply/Uxy/mem_set; rewrite /= -yxE. +Qed. + +Local Lemma entourage_split_ex (A : set (E * E)) : entourage A -> + exists2 B : set (E * E), entourage B & (B \; B)%relation `<=` A. +Proof. +move=> [/= U] [U0 Uxy]; rewrite /entourage /=. +have := @add_continuous (0, 0); rewrite /continuous_at/= addr0 => /(_ U U0)[]/=. +move=> [W1 W2] []; rewrite nbhsE/= => [[U1 nU1 UW1] [U2 nU2 UW2]] Wadd. +exists [set w | (W1 `&` W2) (w.1 - w.2)]. + exists (W1 `&` W2); split; last by []. + exists (U1 `&` U2); first exact: open_nbhsI. + by move=> t [U1t U2t]; split; [exact: UW1|exact: UW2]. +move => xy /= [z [H1 _] [_ H2]]; apply/set_mem/(Uxy xy)/mem_set. +rewrite [_ - _](_ : _ = (xy.1 - z) + (z - xy.2)); last by rewrite addrA subrK. +exact: (Wadd (xy.1 - z,z - xy.2)). +Qed. + +Local Lemma nbhsE : nbhs = nbhs_ entourage. +Proof. +have lem : -1 != 0 :> R by rewrite oppr_eq0 oner_eq0. +rewrite /nbhs_ /=; apply/funext => x; rewrite /filter_from/=. +apply/funext => U; apply/propext => /=; rewrite /entourage /=; split. +- pose V : set E := [set v | x - v \in U]. + move=> nU; exists [set xy | xy.1 - xy.2 \in V]; last first. + by move=> y /xsectionP; rewrite /V /= !inE /= opprB addrCA subrr addr0 inE. + exists V; split => /=; last first. + by move=> xy; rewrite !inE=> Vxy; rewrite /= !inE. + have /= := nbhsB x (nbhsN nU); rewrite subrr /= /V. + rewrite [X in nbhs _ X -> _](_ : _ = [set v | x - v \in U])//. + apply/funext => /= v /=; rewrite inE; apply/propext; split. + by move=> [x0 [x1]] Ux1 <- <-; rewrite opprB addrCA subrr addr0. + move=> Uxy; exists (v - x); last by rewrite addrCA subrr addr0. + by exists (x - v) => //; rewrite opprB. +- move=> [A [U0 [nU UA]] H]; near=> z; apply: H; apply/xsectionP/set_mem/UA. + near: z; rewrite nearE; have := nbhsT x (nbhs0N nU). + rewrite [X in nbhs _ X -> _](_ : _ = [set v | x - v \in U0])//. + apply/funext => /= z /=; apply/propext; split. + move=> [x0] [x1 Ux1 <-] <-; rewrite -opprB addrAC subrr add0r inE opprK//. + rewrite inE => Uxz; exists (z - x); last by rewrite addrCA subrr addr0. + by exists (x - z); rewrite ?opprB. +Unshelve. all: by end_near. Qed. + +HB.instance Definition _ := Nbhs_isUniform_mixin.Build E + entourage_filter entourage_refl + entourage_inv entourage_split_ex + nbhsE. +HB.end. + +Section Tvs_numDomain. +Context (R : numDomainType) (E : tvsType R) (U : set E). + +Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U). +Proof. exact/nbhs0N_subproof/scale_continuous. Qed. + +Lemma nbhsT (x :E) : nbhs 0 U -> nbhs x (+%R x @` U). +Proof. exact/nbhsT_subproof/add_continuous. Qed. + +Lemma nbhsB (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U). +Proof. exact/nbhsB_subproof/add_continuous. Qed. + +End Tvs_numDomain. + +Section Tvs_numField. + +Lemma nbhs0Z (R : numFieldType) (E : tvsType R) (U : set E) (r : R) : + r != 0 -> nbhs 0 U -> nbhs 0 ( *:%R r @` U ). +Proof. +move=> r0 U0; have /= := scale_continuous (r^-1, 0) U. +rewrite scaler0 => /(_ U0)[]/= B [B1 B2] BU. +near=> x => //=; exists (r^-1 *: x); last by rewrite scalerA divff// scale1r. +by apply: (BU (r^-1, x)); split => //=;[exact: nbhs_singleton|near: x]. +Unshelve. all: by end_near. Qed. + +Lemma nbhsZ (R : numFieldType) (E : tvsType R) (U : set E) (r : R) (x :E) : + r != 0 -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U ). +Proof. +move=> r0 U0; have /= := scale_continuous ((r^-1, r *: x)) U. +rewrite scalerA mulVf// scale1r =>/(_ U0)[] /= B [B1 B2] BU. +near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r. +by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z]. +Unshelve. all: by end_near. Qed. + +End Tvs_numField. + +Section standard_topology. +Variable R : numFieldType. + +Local Lemma standard_add_continuous : continuous (fun x : R^o * R^o => x.1 + x.2). +Proof. +(* NB(rei): almost the same code as in normedtype.v *) +move=> [/= x y]; apply/cvg_ballP => e e0 /=. +exists (ball x (e / 2), ball y (e / 2)) => /=. + by split; apply: nbhsx_ballx; rewrite divr_gt0. +rewrite /ball /ball_/= => xy /= [nx ny]. +by rewrite opprD addrACA (le_lt_trans (ler_normD _ _)) // (splitr e) ltrD. +Qed. + +Local Lemma standard_scale_continuous : continuous (fun z : R^o * R^o => z.1 *: z.2). +Proof. +(* NB: This lemma is proved once again in normedtype, in a shorter way with much more machinery *) +(* To be rewritten once normedtype is split and tvs can depend on these lemmas *) +move=> [k x]; apply/cvg_ballP => e le0 /=. +pose M : R := maxr (`|e| + 1) (maxr `|k| (`|x| + `|x| + 2^-1 + 1)). +have M0l : 0 < `|e| + 1 by rewrite ltr_wpDl. +have M0r : 0 < maxr `|k| (`|x| + `|x| + 2^-1 + 1). + rewrite /maxr; case: ifPn => //. + have [->|k0 _] := eqVneq k 0; last by rewrite normr_gt0. + rewrite normr0 -ltrBlDr sub0r ltxx => /negbTE <-. + by rewrite (lt_le_trans (@ltrN10 _)). +have M0 : 0 < M. + by have /= -> := num_lt_max 0 (PosNum M0l) (PosNum M0r); rewrite M0l. +have Me : `|e| < M. + rewrite (@lt_le_trans _ _ (`|e| + 1)) ?ltrDl//. + have /= -> := num_le_max (`|e| + 1) (PosNum M0l) (PosNum M0r). + by rewrite lexx. +pose r := `|e| / 2 / M. +exists (ball k r, ball x r). + by split; exists r => //=; rewrite !divr_gt0// normr_gt0 gt_eqF. +move=> /= [z1 z2] [k1r k2r]. +have := @ball_split _ _ (k * z2) (k * x) (z1 * z2) `|e|. +rewrite /ball /= /= real_lter_normr ?gtr0_real//. +rewrite (_ : _ < - e = false) ?orbF; last by rewrite ltr_nnorml// oppr_le0 ltW. +apply. + rewrite -mulrBr normrM (@le_lt_trans _ _ (M * `|x - z2|)) ?ler_wpM2r//. + have /= -> := num_le_max `|k| (PosNum M0l) (PosNum M0r). + by apply/orP; right; rewrite /maxr; case: ifPn => // /ltW. + by rewrite -ltr_pdivlMl ?(lt_le_trans k2r)// mulrC. +rewrite -mulrBl normrM (@le_lt_trans _ _ (`|k - z1| * M)) ?ler_wpM2l//. + rewrite (@le_trans _ _ (`|z2| + `|x|))// ?lerDl ?normr_ge0//. + have z2xe : `|z2| <= `|x| + r. + by rewrite -lerBlDl -(normrN x) (le_trans (lerB_normD _ _))// distrC ltW. + rewrite (@le_trans _ _ (`|x| + r + `|x|)) ?lerD// addrC. + rewrite [leRHS](_ : _ = M^-1 * (M * M)); last first. + by rewrite mulrA mulVf ?mul1r// gt_eqF. + rewrite [leLHS](_ : _ = M^-1 * (M * (`|x| + `|x|) + `|e| / 2)); last first. + by rewrite mulrDr mulrA mulVf ?mul1r ?gt_eqF// mulrC addrA. + rewrite ler_wpM2l// ?invr_ge0// ?ltW// -ltrBrDl -mulrBr ltr_pM// ltrBrDl//. + rewrite (@lt_le_trans _ _ (`|x| + `|x| + 2^-1 + 1)) //. + by rewrite ltrDl ltr01. + rewrite (num_le_max _ (PosNum M0l) (PosNum M0r))//=. + apply/orP; right; have [->|k0] := eqVneq k 0. + by rewrite normr0 comparable_le_max ?real_comparable// lexx orbT. + have nk0 : 0 < `|k| by rewrite normr_gt0. + have xx21 : 0 < `|x| + `|x| + 2^-1 + 1%R by rewrite addr_gt0. + by rewrite (num_le_max _ (PosNum nk0) (PosNum xx21))// lexx orbT. +by rewrite -ltr_pdivlMr ?(lt_le_trans k1r) ?normr_gt0. +Qed. + +Local Lemma standard_locally_convex : + exists2 B : set (set R^o), (forall b, b \in B -> convex b) & basis B. +Proof. +(* NB(rei): almost the same code as in normedtype.v *) +exists [set B | exists x r, B = ball x r]. + move=> b; rewrite inE /= => [[x]] [r] -> z y l. + rewrite !inE /ball /= => zx yx l0; rewrite -subr_gt0 => l1. + have -> : x = l *: x + (1 - l) *: x. + by rewrite scalerBl addrCA subrr addr0 scale1r. + rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first. + by rewrite opprD addrACA -mulrBr -mulrBr. + rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//. + by rewrite -!normrM ler_normD. + rewrite (@lt_le_trans _ _ (`|l| * r + `|1 - l| * r ))//. + rewrite ltr_leD//. + by rewrite -ltr_pdivlMl ?mulrA ?mulVf ?mul1r // ?normrE ?gt_eqF. + by rewrite -ler_pdivlMl ?mulrA ?mulVf ?mul1r ?ltW // ?normrE ?gt_eqF. + have -> : `|1 - l| = 1 - `| l |. + by move: l0 l1 => /ltW/normr_idP -> /ltW/normr_idP ->. + by rewrite -mulrDl addrCA subrr addr0 mul1r. +split. + move=> B [x] [r] ->. + rewrite openE/= /ball/= /interior => y /= bxy; rewrite -nbhs_ballE. + exists (r - `|x - y|) => /=; first by rewrite subr_gt0. + move=> z; rewrite /ball/= ltrBrDr. + by apply: le_lt_trans; rewrite [in leRHS]addrC ler_distD. +move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=. +by exists (ball x r) => //; split; [exists x, r|exact: ballxx]. +Qed. + +HB.instance Definition _ := Uniform_isTvs.Build R R^o + standard_add_continuous standard_scale_continuous standard_locally_convex. + +End standard_topology. + +Section prod_Tvs. +Context (K : numFieldType) (E F : tvsType K). + +Local Lemma prod_add_continuous : continuous (fun x : (E * F) * (E * F) => x.1 + x.2). +Proof. +move => [/= xy1 xy2] /= U /= [] [A B] /= [nA nB] nU. +have [/= A0 [A01 A02] nA1] := @add_continuous K E (xy1.1, xy2.1) _ nA. +have [/= B0 [B01 B02] nB1] := @add_continuous K F (xy1.2, xy2.2) _ nB. +exists ([set xy | A0.1 xy.1 /\ B0.1 xy.2], [set xy | A0.2 xy.1 /\ B0.2 xy.2]). + by split; [exists (A0.1, B0.1)|exists (A0.2, B0.2)]. +move => [[x1 y1][x2 y2]] /= [] [] a1 b1 [] a2 b2. +by apply: nU; split; [exact: (nA1 (x1, x2))|exact: (nB1 (y1, y2))]. +Qed. + +Local Lemma prod_scale_continuous : continuous (fun z : K^o * (E * F) => z.1 *: z.2). +Proof. +move => [/= r [x y]] /= U /= []/= [A B] /= [nA nB] nU. +have [/= A0 [A01 A02] nA1] := @scale_continuous K E (r, x) _ nA. +have [/= B0 [B01 B02] nB1] := @scale_continuous K F (r, y) _ nB . +exists (A0.1 `&` B0.1, A0.2 `*` B0.2). + by split; [exact: filterI|exists (A0.2,B0.2)]. +by move=> [l [e f]] /= [] [Al Bl] [] Ae Be; apply: nU; split; + [exact: (nA1 (l, e))|exact: (nB1 (l, f))]. +Qed. + +Local Lemma prod_locally_convex : + exists2 B : set (set (E * F)), (forall b, b \in B -> convex b) & basis B. +Proof. +have [Be Bcb Beb] := @locally_convex K E. +have [Bf Bcf Bfb] := @locally_convex K F. +pose B := [set ef : set (E * F) | open ef /\ + exists be, exists2 bf, Be be & Bf bf /\ be `*` bf = ef]. +have : basis B. + rewrite /basis/=; split; first by move=> b => [] []. + move=> /= [x y] ef [[ne nf]] /= [Ne Nf] Nef. + case: Beb => Beo /(_ x ne Ne) /= -[a] [] Bea ax ea. + case: Bfb => Bfo /(_ y nf Nf) /= -[b] [] Beb yb fb. + exists [set z | a z.1 /\ b z.2]; last first. + by apply: subset_trans Nef => -[zx zy] /= [] /ea + /fb. + split=> //=; split; last by exists a, b. + rewrite openE => [[z z'] /= [az bz]]; exists (a, b) => /=; last by []. + rewrite !nbhsE /=; split; first by exists a => //; split => //; exact: Beo. + by exists b => //; split => // []; exact: Bfo. +exists B => // => b; rewrite inE /= => [[]] bo [] be [] bf Bee [] Bff <-. +move => [x1 y1] [x2 y2] l /[!inE] /= -[xe1 yf1] [xe2 yf2] l0 l1. +by split; rewrite -inE; [apply: Bcb; rewrite ?inE|apply: Bcf; rewrite ?inE]. +Qed. + +HB.instance Definition _ := + Uniform_isTvs.Build K (E * F)%type + prod_add_continuous prod_scale_continuous prod_locally_convex. + +End prod_Tvs.