From d06ccaabecd29202f444c3e61072305284a1885e Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 6 Dec 2024 11:03:48 +0100 Subject: [PATCH] Remove the use of [the _ of _] notations --- analysis_stdlib/showcase/uniform_bigO.v | 2 +- classical/cardinality.v | 2 +- experimental_reals/discrete.v | 2 +- reals/prodnormedzmodule.v | 3 +- reals/reals.v | 4 +- reals_stdlib/Rstruct.v | 10 ++-- theories/cantor.v | 4 +- theories/charge.v | 40 +++++-------- theories/derive.v | 2 +- theories/forms.v | 3 +- theories/function_spaces.v | 19 +++--- theories/hoelder.v | 4 +- theories/kernel.v | 61 +++++++------------- theories/lebesgue_integral.v | 58 +++++++++---------- theories/lebesgue_measure.v | 35 +++++------ theories/lebesgue_stieltjes_measure.v | 15 ++--- theories/measure.v | 27 ++++----- theories/normedtype.v | 31 +++++----- theories/numfun.v | 7 +-- theories/probability.v | 7 +-- theories/separation_axioms.v | 3 +- theories/topology_theory/bool_topology.v | 4 +- theories/topology_theory/subspace_topology.v | 3 +- theories/topology_theory/supremum_topology.v | 2 +- 24 files changed, 147 insertions(+), 201 deletions(-) diff --git a/analysis_stdlib/showcase/uniform_bigO.v b/analysis_stdlib/showcase/uniform_bigO.v index 58e6e9c5b..9ec3cd264 100644 --- a/analysis_stdlib/showcase/uniform_bigO.v +++ b/analysis_stdlib/showcase/uniform_bigO.v @@ -33,7 +33,7 @@ Definition OuP (f : A -> R * R -> R) (g : R * R -> R) := (* first we replace sig with ex and the l^2 norm with the l^oo norm *) -Let normedR2 := [the normedModType _ of (R^o * R^o)%type]. +Let normedR2 : normedModType _ := (R^o * R^o)%type. Definition OuPex (f : A -> R * R -> R^o) (g : R * R -> R^o) := exists2 alp, 0 < alp & exists2 C, 0 < C & diff --git a/classical/cardinality.v b/classical/cardinality.v index c84602f5f..9b73d1de3 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -1327,7 +1327,7 @@ Qed. HB.instance Definition _ aT rT x := FiniteImage.Build aT rT (cst x) (@finite_image_cst aT rT x). -Definition cst_fimfun {aT rT} x := [the {fimfun aT >-> rT} of cst x]. +Definition cst_fimfun {aT rT} x : {fimfun aT >-> rT} := cst x. Lemma fimfun_cst aT rT x : @cst_fimfun aT rT x =1 cst x. Proof. by []. Qed. diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 029af438e..6e853ac32 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -169,7 +169,7 @@ Variables (T : eqType) (E F : pred T). Lemma countable_sub: {subset E <= F} -> countable F -> countable E. Proof. move=> le_EF [f g fgK]; pose f' (x : [psub E]) := f (pincl le_EF x). -pose g' x := obind (insub (sT := [the subType _ of [psub E]])) (omap val (g x)). +pose g' x := obind (insub (sT := [psub E])) (omap val (g x)). by exists f' g' => x; rewrite /f' /g' fgK /= valK. Qed. End CountSub. diff --git a/reals/prodnormedzmodule.v b/reals/prodnormedzmodule.v index 38bfe229c..ad613feb7 100644 --- a/reals/prodnormedzmodule.v +++ b/reals/prodnormedzmodule.v @@ -57,8 +57,7 @@ Proof. by rewrite /norm/= !normrN. Qed. HB.instance Definition _ := Num.Zmodule_isNormed.Build R (U * V)%type normD norm_eq0 normMn normrN. -Lemma prod_normE (x : [the normedZmodType R of (U * V)%type]) : - `|x| = Num.max `|x.1| `|x.2|. +Lemma prod_normE (x : U * V) : `|x| = Num.max `|x.1| `|x.2|. Proof. by []. Qed. End ProdNormedZmodule. diff --git a/reals/reals.v b/reals/reals.v index bc9d85ce1..2b1fd3ad1 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -116,9 +116,9 @@ End has_bound_lemmas. (* -------------------------------------------------------------------- *) HB.mixin Record ArchimedeanField_isReal R of Num.ArchiField R := { - sup_upper_bound_subdef : forall E : set [the archiFieldType of R], + sup_upper_bound_subdef : forall E : set R, has_sup E -> ubound E (supremum 0 E) ; - sup_adherent_subdef : forall (E : set [the archiFieldType of R]) (eps : R), + sup_adherent_subdef : forall (E : set R) (eps : R), 0 < eps -> has_sup E -> exists2 e : R, E e & (supremum 0 E - eps) < e }. diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index 4dbe8f0bf..998ed7690 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -250,8 +250,7 @@ Qed. HB.instance Definition _ := Order.POrder_isTotal.Build _ R R_total. -Lemma Rarchimedean_axiom : - Num.archimedean_axiom [the numDomainType of R : Type]. +Lemma Rarchimedean_axiom : Num.archimedean_axiom R. Proof. move=> x; exists (Z.abs_nat (up x) + 2)%N. have [Hx1 Hx2]:= (archimed x). @@ -269,7 +268,7 @@ apply/RltbP/Rabs_def1. apply/Rplus_le_compat_r/IHz; split; first exact: Zlt_le_weak. exact: Zlt_pred. apply: (Rle_trans _ (IZR 0)); first exact: IZR_le. - by apply/RlebP/(ler0n [the numDomainType of R : Type] (Z.abs_nat z)). + by apply/RlebP/(ler0n R (Z.abs_nat z)). apply: (Rlt_le_trans _ (IZR (up x) - 1)). apply: Ropp_lt_cancel; rewrite Ropp_involutive. rewrite Ropp_minus_distr /Rminus -opp_IZR -{2}(Z.opp_involutive (up x)). @@ -287,7 +286,7 @@ apply: (Rlt_le_trans _ (IZR (up x) - 1)). rewrite mulrnDr; apply: (Rlt_le_trans _ 2). by rewrite -{1}[1]Rplus_0_r; apply/Rplus_lt_compat_l/Rlt_0_1. rewrite -[2]Rplus_0_l; apply: Rplus_le_compat_r. - by apply/RlebP/(ler0n [the numDomainType of R : Type] (Z.abs_nat _)). + by apply/RlebP/(ler0n R (Z.abs_nat _)). apply: Rminus_le. rewrite /Rminus Rplus_assoc [- _ + _]Rplus_comm -Rplus_assoc -!/(Rminus _ _). exact: Rle_minus. @@ -334,8 +333,7 @@ have Hg: (fun x=> f x * f x ^+ n)%R =1 g. by apply: (continuity_eq Hg); exact: continuity_mult. Qed. -Lemma Rreal_closed_axiom : - Num.real_closed_axiom [the numDomainType of R : Type]. +Lemma Rreal_closed_axiom : Num.real_closed_axiom R. Proof. move=> p a b; rewrite !le_eqVlt. case Hpa: ((p.[a])%R == 0%R). diff --git a/theories/cantor.v b/theories/cantor.v index 8006e1ced..b40e5631f 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -340,7 +340,7 @@ Lemma homeomorphism_cantor_like : exists f : {splitbij [set: cantor_space] >-> [set: T]}, continuous f /\ (forall A, closed A -> closed (f @` A)). Proof. -exists [the {splitbij _ >-> _} of tree_map] => /=. +exists tree_map => /=. have [cts surj inje] := projT2 (cid cantor_map); split; first exact: cts. move=> A clA; apply: (compact_closed hsdfT). apply: (@continuous_compact _ _ tree_map); first exact: continuous_subspaceT. @@ -527,7 +527,7 @@ have [//| | |? []//| |? []// | |] := @tree_map_props have [z [Dz DzE]] := Csub _ cbD. have /ent_closure := DzE _ Dx => /(_ (ent_count_unif n))/xsectionP/ctE [_ /= Exz]. have /ent_closure := DzE _ Dy => /(_ (ent_count_unif n))/xsectionP/ctE [Ezy _]. - exact: (@entourage_split _ (*[the uniformType of T]*) z). + exact: (@entourage_split T z). by move=> f [ctsf surjf _]; exists f. Qed. diff --git a/theories/charge.v b/theories/charge.v index 9754bc4af..f232b0381 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -520,8 +520,7 @@ Let mu0 : mu set0 = 0. Proof. by apply: measure0. Qed. HB.instance Definition _ := isCharge.Build _ _ _ - mu (measure0 [the content _ _ of mu]) - fin_num_measure measure_semi_sigma_additive. + mu (measure0 mu) fin_num_measure measure_semi_sigma_additive. HB.end. @@ -917,8 +916,7 @@ Let mP : measurable P. Proof. by have [[mP _] _ _ _] := nuPN. Qed. Let mN : measurable N. Proof. by have [_ [mN _] _ _] := nuPN. Qed. -Local Definition cjordan_pos : {charge set T -> \bar R} := - [the charge _ _ of crestr0 nu mP]. +Local Definition cjordan_pos : {charge set T -> \bar R} := crestr0 nu mP. Lemma cjordan_posE A : cjordan_pos A = crestr0 nu mP A. Proof. by []. Qed. @@ -944,7 +942,7 @@ HB.instance Definition _ := @Measure_isFinite.Build _ _ _ jordan_pos finite_jordan_pos. Local Definition cjordan_neg : {charge set T -> \bar R} := - [the charge _ _ of cscale (-1) [the charge _ _ of crestr0 nu mN]]. + cscale (-1) (crestr0 nu mN). Lemma cjordan_negE A : cjordan_neg A = - crestr0 nu mN A. Proof. by rewrite /= /cscale/= EFinN mulN1e. Qed. @@ -970,8 +968,7 @@ HB.instance Definition _ := @Measure_isFinite.Build _ _ _ jordan_neg finite_jordan_neg. Lemma jordan_decomp (A : set T) : measurable A -> - nu A = (cadd [the charge _ _ of jordan_pos] - ([the charge _ _ of cscale (-1) [the charge _ _ of jordan_neg]])) A. + nu A = cadd jordan_pos (cscale (-1) jordan_neg) A. Proof. move=> mA. rewrite /cadd cjordan_posE /= /cscale EFinN mulN1e cjordan_negE oppeK. @@ -1684,8 +1681,7 @@ move=> nu_mu; exists f; split. - by apply/integrableP; split; [exact: mf|exact: int_fRN_lty]. move=> // A mA. apply/eqP; rewrite eq_le int_fRN_ub// andbT leNgt; apply/negP => abs. -pose sigma : {charge set T -> \bar R} := - [the {charge set T -> \bar R} of sigmaRN mA abs]. +pose sigma : {charge set T -> \bar R} := sigmaRN mA abs. have [P [N [[mP posP] [mN negN] PNX PN0]]] := Hahn_decomposition sigma. pose AP := A `&` P. have mAP : measurable AP by exact: measurableI. @@ -1781,11 +1777,9 @@ have muEoo k : mu (E k) < +oo. by rewrite (le_lt_trans _ (muFoo k))// le_measure ?inE//; exact: subDsetl. have UET : \bigcup_i E i = [set: T] by rewrite TF [RHS]seqDU_bigcup_eq. have tE := trivIset_seqDU F. -pose mu_ j : {finite_measure set T -> \bar R} := - [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (muEoo j)]. +pose mu_ j : {finite_measure set T -> \bar R} := mfrestr (mE j) (muEoo j). have nuEoo i : nu (E i) < +oo by rewrite ltey_eq fin_num_measure. -pose nu_ j : {finite_measure set T -> \bar R} := - [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (nuEoo j)]. +pose nu_ j : {finite_measure set T -> \bar R} := mfrestr (mE j) (nuEoo j). have nu_mu_ k : nu_ k `<< mu_ k. by move=> S mS mu_kS0; apply: nu_mu => //; exact: measurableI. have [g_] := choice (fun j => radon_nikodym_finite (nu_mu_ j)). @@ -2034,11 +2028,9 @@ Local Lemma Radon_Nikodym0 : nu `<< mu -> Proof. move=> nu_mu; have [P [N nuPN]] := Hahn_decomposition nu. have [fp [fp0 fpfin intfp fpE]] := @radon_nikodym_sigma_finite _ _ _ mu - [the {finite_measure set _ -> \bar _} of jordan_pos nuPN] - (jordan_pos_dominates nuPN nu_mu). + (jordan_pos nuPN) (jordan_pos_dominates nuPN nu_mu). have [fn [fn0 fnfin intfn fnE]] := @radon_nikodym_sigma_finite _ _ _ mu - [the {finite_measure set _ -> \bar _} of jordan_neg nuPN] - (jordan_neg_dominates nuPN nu_mu). + (jordan_neg nuPN) (jordan_neg_dominates nuPN nu_mu). exists (fp \- fn); split; first by move=> x; rewrite fin_numB// fpfin fnfin. exact: integrableB. move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//; @@ -2091,7 +2083,7 @@ Implicit Types f : T -> \bar R. Lemma ae_eq_Radon_Nikodym_SigmaFinite E : measurable E -> ae_eq mu E (Radon_Nikodym_SigmaFinite.f nu mu) - ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu). + ('d (charge_of_finite_measure nu) '/d mu). Proof. move=> mE; apply: integral_ae_eq => //. - apply: (integrableS measurableT) => //. @@ -2103,8 +2095,7 @@ Qed. Lemma Radon_Nikodym_change_of_variables f E : measurable E -> nu.-integrable E f -> - \int[mu]_(x in E) - (f x * ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu) x) = + \int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) = \int[nu]_(x in E) f x. Proof. move=> mE mf; rewrite [in RHS](funeposneg f) integralB //; last 2 first. @@ -2140,8 +2131,7 @@ Implicit Types (nu : {charge set T -> \bar R}) (mu : {sigma_finite_measure set T -> \bar R}). Lemma Radon_Nikodym_cscale mu nu c E : measurable E -> nu `<< mu -> - ae_eq mu E ('d [the charge _ _ of cscale c nu] '/d mu) - (fun x => c%:E * 'd nu '/d mu x). + ae_eq mu E ('d (cscale c nu) '/d mu) (fun x => c%:E * 'd nu '/d mu x). Proof. move=> mE numu; apply: integral_ae_eq => [//| | |A AE mA]. - apply: (integrableS measurableT) => //. @@ -2155,8 +2145,7 @@ Qed. Lemma Radon_Nikodym_cadd mu nu0 nu1 E : measurable E -> nu0 `<< mu -> nu1 `<< mu -> - ae_eq mu E ('d [the charge _ _ of cadd nu0 nu1] '/d mu) - ('d nu0 '/d mu \+ 'd nu1 '/d mu). + ae_eq mu E ('d (cadd nu0 nu1) '/d mu) ('d nu0 '/d mu \+ 'd nu1 '/d mu). Proof. move=> mE nu0mu nu1mu; apply: integral_ae_eq => [//| | |A AE mA]. - apply: (integrableS measurableT) => //. @@ -2177,8 +2166,7 @@ Variables (nu : {charge set T -> \bar R}) Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la -> ae_eq la setT ('d nu '/d la) - ('d nu '/d mu \* - 'd [the charge _ _ of charge_of_finite_measure mu] '/d la). + ('d nu '/d mu \* 'd (charge_of_finite_measure mu) '/d la). Proof. have [Pnu [Nnu nuPN]] := Hahn_decomposition nu. move=> numu mula; have nula := measure_dominates_trans numu mula. diff --git a/theories/derive.v b/theories/derive.v index fc68330d6..c368957b0 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -671,7 +671,7 @@ Qed. Global Instance is_diff_scalel (k : R) (x : V) : is_diff k ( *:%R ^~ x) ( *:%R ^~ x). Proof. -have sx_lin : linear ( *:%R ^~ x : [the lmodType R of R : Type] -> _). +have sx_lin : linear ( *:%R ^~ x : R -> _). by move=> u y z; rewrite scalerDl scalerA. pose sxlM := GRing.isLinear.Build _ _ _ _ _ sx_lin. pose sxL : {linear _ -> _} := HB.pack ( *:%R ^~ x) sxlM. diff --git a/theories/forms.v b/theories/forms.v index 7b7f2f732..92e9eb164 100644 --- a/theories/forms.v +++ b/theories/forms.v @@ -200,8 +200,7 @@ Qed. HB.instance Definition _ (R : comRingType) m n p := bilinear_isBilinear.Build R - [the lmodType R of 'M[R]_(m, n)] [the lmodType R of 'M[R]_(n, p)] - [the zmodType of 'M[R]_(m, p)] _ _ (@mulmx R m n p) + 'M[R]_(m, n) 'M[R]_(n, p) 'M[R]_(m, p) _ _ (@mulmx R m n p) (mulmx_is_bilinear R m n p). (* Section classfun. *) diff --git a/theories/function_spaces.v b/theories/function_spaces.v index cc56990f6..0f257a568 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -124,20 +124,19 @@ Variable I : Type. Definition product_topology_def (T : I -> topologicalType) := sup_topology (fun i => Topological.class - (weak_topology (fun f : [the choiceType of forall i, T i] => f i))). + (weak_topology (fun f : (forall i, T i) => f i))). HB.instance Definition _ (T : I -> topologicalType) := Topological.copy (prod_topology T) (product_topology_def T). HB.instance Definition _ (T : I -> uniformType) := Uniform.copy (prod_topology T) - (sup_topology (fun i => Uniform.class - [the uniformType of weak_topology (@proj _ T i)])). + (sup_topology (fun i => Uniform.class (weak_topology (@proj _ T i)))). HB.instance Definition _ (R : realType) (Ii : countType) (Tc : Ii -> pseudoMetricType R) := PseudoMetric.copy (prod_topology Tc) - (sup_pseudometric (fun i => PseudoMetric.class - [the pseudoMetricType R of weak_topology (@proj _ Tc i)]) (countableP _)). + (sup_pseudometric (fun i => PseudoMetric.class (weak_topology (@proj _ Tc i))) + (countableP _)). End Product_Topology. @@ -327,10 +326,10 @@ Definition separate_points_from_closed := forall (U : set T) x, Hypothesis sepf : separate_points_from_closed. Hypothesis ctsf : forall i, continuous (f_ i). -Let weakT := [the topologicalType of - sup_topology (fun i => Topological.on (weak_topology (f_ i)))]. +Let weakT : topologicalType := + sup_topology (fun i => Topological.on (weak_topology (f_ i))). -Let PU := [the topologicalType of prod_topology U_]. +Let PU : topologicalType := prod_topology U_. Local Notation sup_open := (@open weakT). Local Notation "'weak_open' i" := (@open weakT) (at level 0). @@ -660,7 +659,7 @@ by move: rBrE; rewrite eqEsubset; case => [+ _]; apply; exists g. Unshelve. all: by end_near. Qed. Lemma uniform_entourage : - @entourage [the uniformType of {uniform` A -> V}] = + @entourage {uniform` A -> V} = filter_from (@entourage V) (fun P => [set fg | forall t : U, A t -> P (fg.1 t, fg.2 t)]). @@ -698,7 +697,7 @@ Notation "{ 'family' fam , F --> f }" := HB.instance Definition _ {U : choiceType} {V : uniformType} (fam : set U -> Prop) := Uniform.copy {family fam, U -> V} (sup_topology (fun k : sigT fam => - Uniform.class [the uniformType of {uniform` projT1 k -> V}])). + Uniform.class {uniform` projT1 k -> V})). Section UniformCvgLemmas. Context {U : choiceType} {V : uniformType}. diff --git a/theories/hoelder.v b/theories/hoelder.v index 346c0cb48..5b5b020f8 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -104,7 +104,7 @@ Section lnorm. (* l-norm is just L-norm applied to counting *) Context d {T : measurableType d} {R : realType}. Local Open Scope ereal_scope. -Local Notation "'N_ p [ f ]" := (Lnorm [the measure _ _ of counting] p f). +Local Notation "'N_ p [ f ]" := (Lnorm counting p f). Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R -> 'N_p%:E [f] = (\sum_(k a10 a20 b10 b20 p0 q0 pq. pose f a b n : R := match n with 0%nat => a | 1%nat => b | _ => 0 end. have mf a b : measurable_fun setT (f a b) by []. -have := hoelder [the measure _ _ of counting] (mf a1 a2) (mf b1 b2) p0 q0 pq. +have := hoelder counting (mf a1 a2) (mf b1 b2) p0 q0 pq. rewrite !Lnorm_counting//. rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0. rewrite add0n ereal_series_cond eseries0 ?adde0; last first. diff --git a/theories/kernel.v b/theories/kernel.v index 71c065e5a..31d8ba818 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -125,8 +125,7 @@ Section kseries. Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). Variable k : (R.-ker X ~> Y)^nat. -Definition kseries : X -> {measure set Y -> \bar R} := - fun x => [the measure _ _ of mseries (k ^~ x) 0]. +Definition kseries (x : X) : {measure set Y -> \bar R} := mseries (k ^~ x) 0. Lemma measurable_fun_kseries (U : set Y) : measurable U -> measurable_fun [set: X] (kseries ^~ U). @@ -209,8 +208,7 @@ HB.factory Record Kernel_isFinite d d' Section kzero. Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). -Definition kzero : X -> {measure set Y -> \bar R} := - fun _ : X => [the measure _ _ of mzero]. +Definition kzero (_ : X) : {measure set Y -> \bar R} := mzero. Let measurable_fun_kzero U : measurable U -> measurable_fun [set: X] (kzero ^~ U). @@ -231,8 +229,7 @@ Let sfinite_finite : exists2 k_ : (R.-ker _ ~> _)^nat, forall n, measure_fam_uub (k_ n) & forall x U, measurable U -> k x U = mseries (k_ ^~ x) 0 U. Proof. -exists (fun n => if n is O then [the _.-ker _ ~> _ of k] else - [the _.-ker _ ~> _ of @kzero _ _ X Y R]). +exists (fun n => if n is O return R.-ker X ~> Y then k else @kzero _ _ X Y R). by case => [|_]; [exact: measure_uub|exact: kzero_uub]. move=> t U mU/=; rewrite /mseries. rewrite (nneseries_split _ 1%N)// big_mkord big_ord_recl/= big_ord0 adde0. @@ -270,10 +267,7 @@ HB.instance Definition _ n := @Kernel_isFinite.Build d d' X Y R (s n) (s_uub n). Lemma sfinite_kernel : exists s : (R.-fker X ~> Y)^nat, forall x U, measurable U -> k x U = kseries s x U. -Proof. -exists (fun n => [the _.-fker _ ~> _ of s n]) => x U mU. -by rewrite /s /= /s; by case: cid2 => ? ? ->. -Qed. +Proof. by exists s => x U mU; rewrite /s /= /s; case: cid2 => ? ? ->. Qed. End sfinite. @@ -605,9 +599,8 @@ Section kdirac. Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). Variable f : X -> Y. -Definition kdirac (mf : measurable_fun [set: X] f) - : X -> {measure set Y -> \bar R} := - fun x => [the measure _ _ of dirac (f x)]. +Definition kdirac (mf : measurable_fun [set: X] f) (x : X) : + {measure set Y -> \bar R} := dirac (f x). Hypothesis mf : measurable_fun [set: X] f. @@ -666,11 +659,10 @@ Section kadd. Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). Variables k1 k2 : R.-ker X ~> Y. -Definition kadd : X -> {measure set Y -> \bar R} := - fun x => [the measure _ _ of measure_add (k1 x) (k2 x)]. +Definition kadd (x : X) : {measure set Y -> \bar R} := + measure_add (k1 x) (k2 x). -Let measurable_fun_kadd U : measurable U -> - measurable_fun [set: X] (kadd ^~ U). +Let measurable_fun_kadd U : measurable U -> measurable_fun [set: X] (kadd ^~ U). Proof. move=> mU; rewrite /kadd. rewrite (_ : (fun _ => _) = (fun x => k1 x U + k2 x U)); last first. @@ -692,7 +684,7 @@ Let sfinite_kadd : exists2 k_ : (R.-ker _ ~> _)^nat, kadd k1 k2 x U = mseries (k_ ^~ x) 0 U. Proof. have [f1 hk1] := sfinite_kernel k1; have [f2 hk2] := sfinite_kernel k2. -exists (fun n => [the _.-ker _ ~> _ of kadd (f1 n) (f2 n)]). +exists (fun n => kadd (f1 n) (f2 n)). move=> n. have [r1 f1r1] := measure_uub (f1 n). have [r2 f2r2] := measure_uub (f2 n). @@ -775,8 +767,7 @@ End knormalize. (* TODO: useful? *) Lemma measurable_fun_mnormalize d d' (X : measurableType d) (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) : - measurable_fun [set: X] (fun x => - [the probability _ _ of mnormalize (k x) point] : pprobability Y R). + measurable_fun [set: X] (fun x => mnormalize (k x) point : pprobability Y R). Proof. apply: (@measurability _ _ _ _ _ _ (@pset _ _ _ : set (set (pprobability Y R)))) => //. @@ -807,7 +798,7 @@ Section kcomp_def. Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2) (Z : measurableType d3) (R : realType). Variable l : X -> {measure set Y -> \bar R}. -Variable k : (X * Y)%type -> {measure set Z -> \bar R}. +Variable k : X * Y -> {measure set Z -> \bar R}. Definition kcomp x U := \int[l x]_y k (x, y) U. @@ -816,8 +807,7 @@ End kcomp_def. Section kcomp_is_measure. Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2) (Z : measurableType d3) (R : realType). -Variable l : R.-ker X ~> Y. -Variable k : R.-ker [the measurableType _ of X * Y] ~> Z. +Variables (l : R.-ker X ~> Y) (k : R.-ker (X * Y) ~> Z). Let kcomp0 x : kcomp l k x set0 = 0. Proof. @@ -841,8 +831,7 @@ Qed. HB.instance Definition _ x := isMeasure.Build _ _ R (kcomp l k x) (kcomp0 x) (kcomp_ge0 x) (@kcomp_sigma_additive x). -Definition mkcomp : X -> {measure set Z -> \bar R} := fun x => - [the measure _ _ of kcomp l k x]. +Definition mkcomp : X -> {measure set Z -> \bar R} := kcomp l k. End kcomp_is_measure. @@ -853,7 +842,7 @@ Module KCOMP_FINITE_KERNEL. Section kcomp_finite_kernel_kernel. Context d d' d3 (X : measurableType d) (Y : measurableType d') (Z : measurableType d3) (R : realType) (l : R.-fker X ~> Y) - (k : R.-ker [the measurableType _ of X * Y] ~> Z). + (k : R.-ker (X * Y) ~> Z). Lemma measurable_fun_kcomp_finite U : measurable U -> measurable_fun [set: X] ((l \; k) ^~ U). @@ -870,8 +859,7 @@ End kcomp_finite_kernel_kernel. Section kcomp_finite_kernel_finite. Context d d' d3 (X : measurableType d) (Y : measurableType d') (Z : measurableType d3) (R : realType). -Variable l : R.-fker X ~> Y. -Variable k : R.-fker [the measurableType _ of X * Y] ~> Z. +Variables (l : R.-fker X ~> Y) (k : R.-fker (X * Y) ~> Z). Let mkcomp_finite : measure_fam_uub (kcomp l k). Proof. @@ -894,8 +882,7 @@ End KCOMP_FINITE_KERNEL. Section kcomp_sfinite_kernel. Context d d' d3 (X : measurableType d) (Y : measurableType d') (Z : measurableType d3) (R : realType). -Variable l : R.-sfker X ~> Y. -Variable k : R.-sfker [the measurableType _ of X * Y] ~> Z. +Variable (l : R.-sfker X ~> Y) (k : R.-sfker (X * Y) ~> Z). Import KCOMP_FINITE_KERNEL. @@ -907,11 +894,10 @@ have [kl hkl] : exists kl : (R.-fker X ~> Z) ^nat, forall x U, \esum_(i in setT) (l_ i.2 \; k_ i.1) x U = \sum_(i [the _.-fker _ ~> _ of l_ (f i).2 \; k_ (f i).1]) => x U. + exists (fun i => l_ (f i).2 \; k_ (f i).1) => x U. by rewrite (reindex_esum [set: nat] _ f)// nneseries_esum// fun_true. exists kl => x U mU. -transitivity (([the _.-ker _ ~> _ of kseries l_] \; - [the _.-ker _ ~> _ of kseries k_]) x U). +transitivity ((kseries l_ \; kseries k_) x U). rewrite /= /kcomp [in RHS](eq_measure_integral (l x)); last first. by move=> *; rewrite hl_. by apply: eq_integral => y _; rewrite hk_. @@ -940,8 +926,7 @@ Module KCOMP_SFINITE_KERNEL. Section kcomp_sfinite_kernel. Context d d' d3 (X : measurableType d) (Y : measurableType d') (Z : measurableType d3) (R : realType). -Variable l : R.-sfker X ~> Y. -Variable k : R.-sfker [the measurableType _ of X * Y] ~> Z. +Variables (l : R.-sfker X ~> Y) (k : R.-sfker (X * Y) ~> Z). HB.instance Definition _ := isKernel.Build _ _ X Z R (l \; k) (measurable_fun_mkcomp_sfinite l k). @@ -986,8 +971,7 @@ Lemma measurable_fun_preimage_integral (l : X -> {measure set Y -> \bar R}) : (forall n r, measurable_fun [set: X] (l ^~ (k_ n @^-1` [set r]))) -> measurable_fun [set: X] (fun x => \int[l x]_z k z). Proof. -move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l - (fun n => [the {nnsfun _ >-> _} of k_2 n])) => /=. +move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l k_2) => /=. - by rewrite /k_2 => m n mn; apply/lefP => -[x y] /=; exact/lefP/ndk_. - by move=> [x y]; exact: k_k. - move=> n r _ /= B mB. @@ -1024,8 +1008,7 @@ End measurable_fun_integral_kernel. Section integral_kcomp. Context d d2 d3 (X : measurableType d) (Y : measurableType d2) (Z : measurableType d3) (R : realType). -Variables (l : R.-sfker X ~> Y) - (k : R.-sfker [the measurableType _ of X * Y] ~> Z). +Variables (l : R.-sfker X ~> Y) (k : R.-sfker (X * Y) ~> Z). Let integral_kcomp_indic x E (mE : measurable E) : \int[kcomp l k x]_z (\1_E z)%:E = \int[l x]_y (\int[k (x, y)]_z (\1_E z)%:E). diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 5553c2ad2..dabbbcc8d 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -295,18 +295,18 @@ Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed. HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ aT rT (mindic mD) (@measurable_indic _ aT rT setT D mD). -Definition indic_mfun (D : set aT) (mD : measurable D) := - [the {mfun aT >-> rT} of mindic mD]. +Definition indic_mfun (D : set aT) (mD : measurable D) : {mfun aT >-> rT} := + mindic mD. HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k). -Definition scale_mfun k f := [the {mfun aT >-> rT} of k \o* f]. +Definition scale_mfun k f : {mfun aT >-> rT} := k \o* f. Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g). Proof. by split; apply: measurable_maxr. Qed. HB.instance Definition _ f g := max_mfun_subproof f g. -Definition max_mfun f g := [the {mfun aT >-> _} of f \max g]. +Definition max_mfun f g : {mfun aT >-> _} := f \max g. End ring. Arguments indic_mfun {d aT rT} _. @@ -365,7 +365,7 @@ HB.instance Definition _ := [Choice of {sfun aT >-> rT} by <:]. (* NB: already instantiated in cardinality.v *) HB.instance Definition _ x : @FImFun aT rT (cst x) := FImFun.on (cst x). -Definition cst_sfun x := [the {sfun aT >-> rT} of cst x]. +Definition cst_sfun x : {sfun aT >-> rT} := cst x. Lemma cst_sfunE x : @cst_sfun x =1 cst x. Proof. by []. Qed. @@ -426,14 +426,14 @@ Import HBSimple. HB.instance Definition _ (D : set aT) (mD : measurable D) : @FImFun aT rT (mindic _ mD) := FImFun.on (mindic _ mD). -Definition indic_sfun (D : set aT) (mD : measurable D) := - [the {sfun aT >-> rT} of mindic rT mD]. +Definition indic_sfun (D : set aT) (mD : measurable D) : {sfun aT >-> rT} := + mindic rT mD. HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_sfun k). -Definition scale_sfun k f := [the {sfun aT >-> rT} of k \o* f]. +Definition scale_sfun k f : {sfun aT >-> rT} := k \o* f. HB.instance Definition _ f g := max_mfun_subproof f g. -Definition max_sfun f g := [the {sfun aT >-> _} of f \max g]. +Definition max_sfun f g : {sfun aT >-> _} := f \max g. End ring. Arguments indic_sfun {d aT rT} _. @@ -495,7 +495,7 @@ HB.instance Definition _ x := @isNonNegFun.Build T R (cst x%:num) (* NB: already instantiated in cardinality.v *) HB.instance Definition _ x : @FImFun T R (cst x) := FImFun.on (cst x). -Definition cst_nnsfun (r : {nonneg R}) := [the {nnsfun T >-> R} of cst r%:num]. +Definition cst_nnsfun (r : {nonneg R}) : {nnsfun T >-> R} := cst r%:num. Definition nnsfun0 : {nnsfun T >-> R} := cst_nnsfun 0%R%:nng. @@ -535,15 +535,15 @@ Variables f g : {nnsfun T >-> R}. Import HBNNSimple. HB.instance Definition _ := MeasurableFun.on (f \+ g). -Definition add_nnsfun := [the {nnsfun T >-> R} of f \+ g]. +Definition add_nnsfun : {nnsfun T >-> R} := f \+ g. HB.instance Definition _ := MeasurableFun.on (f \* g). -Definition mul_nnsfun := [the {nnsfun T >-> R} of f \* g]. +Definition mul_nnsfun : {nnsfun T >-> R} := f \* g. HB.instance Definition _ := MeasurableFun.on (f \max g). -Definition max_nnsfun := [the {nnsfun T >-> R} of f \max g]. +Definition max_nnsfun : {nnsfun T >-> R} := f \max g. -Definition indic_nnsfun A (mA : measurable A) := [the {nnsfun T >-> R} of mindic R mA]. +Definition indic_nnsfun A (mA : measurable A) : {nnsfun T >-> R} := mindic R mA. End nnsfun_bin. Arguments add_nnsfun {d T R} _ _. @@ -1500,7 +1500,7 @@ Lemma cvg_approx x (f0 : forall x, D x -> (0 <= f x)%E) : D x -> (f x < +oo)%E -> approx^~ x @ \oo --> fine (f x). Proof. move=> Dx fxoo; have fxfin : f x \is a fin_num by rewrite ge0_fin_numE// f0. -apply/(@cvgrPdist_lt _ [the normedModType R of R^o]) => _/posnumP[e]. +apply/(@cvgrPdist_lt _ R^o) => _/posnumP[e]. have [fx0|fx0] := eqVneq (f x) 0%E. by near=> n; rewrite f0_approx0 // fx0 /= subrr normr0. have /(fpos_approx_neq0 Dx)[m _ Hm] : (0 < f x < +oo)%E by rewrite lt0e fx0 f0. @@ -1753,7 +1753,7 @@ Lemma approximation_sfun : Proof. 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 /=. +exists (fun n => 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. @@ -1767,8 +1767,8 @@ Section lusin. 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]. -Let R := [the measurableType _ of measurableTypeR rT]. +Let mu : measure _ _ := @lebesgue_measure rT. +Let R : measurableType _ := measurableTypeR rT. Hypothesis mA : measurable A. Hypothesis finA : mu A < +oo. @@ -4254,10 +4254,10 @@ Lemma integral_count (a : nat -> \bar R) : summable setT a -> \int[counting]_t (a t) = \sum_(k sa. -transitivity (\int[mseries (fun n => [the measure _ _ of \d_ n]) O]_t a t). +transitivity (\int[mseries (fun n => \d_ n) O]_t a t). congr (integral _ _ _); apply/funext => A. by rewrite /= counting_dirac. -rewrite (@integral_measure_series _ _ R (fun n => [the measure _ _ of \d_ n]) setT)//=. +rewrite (@integral_measure_series _ _ R (fun n => \d_ n) setT)//=. - by apply: eq_eseriesr=> i _; rewrite integral_dirac//= diracT mul1e. - move=> n; apply/integrableP; split=> [//|]. by rewrite integral_dirac//= diracT mul1e (summable_pinfty sa). @@ -4269,7 +4269,7 @@ Lemma ge0_integral_count (a : nat -> \bar R) : (forall k, 0 <= a k) -> \int[counting]_t (a t) = \sum_(k sa. -transitivity (\int[mseries (fun n => [the measure _ _ of \d_ n]) O]_t a t). +transitivity (\int[mseries (fun n => \d_ n) O]_t a t). congr (integral _ _ _); apply/funext => A. by rewrite /= counting_dirac. rewrite (@ge0_integral_measure_series _ _ R (fun n => \d_ n) setT)//=. @@ -5087,7 +5087,7 @@ HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2) product_measure_sigma_finite. Lemma product_measure_unique - (m' : {measure set [the semiRingOfSetsType _ of T1 * T2] -> \bar R}) : + (m' : {measure set (T1 * T2) -> \bar R}) : (forall A B, measurable A -> measurable B -> m' (A `*` B) = m1 A * m2 B) -> forall X : set (T1 * T2), measurable X -> (m1 \x m2) X = m' X. Proof. @@ -5283,8 +5283,8 @@ End simple_density_L1. Section continuous_density_L1. Context (rT : realType). -Let mu := [the measure _ _ of @lebesgue_measure rT]. -Let R := [the measurableType _ of measurableTypeR rT]. +Let mu : measure _ _ := @lebesgue_measure rT. +Let R : measurableType _ := measurableTypeR rT. Local Open Scope ereal_scope. Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo. @@ -5475,7 +5475,7 @@ Qed. End indic_fubini_tonelli. Section sfun_fubini_tonelli. -Variable f : {nnsfun [the measurableType _ of T1 * T2 : Type] >-> R}. +Variable f : {nnsfun T1 * T2 >-> R}. Import HBNNSimple. @@ -5599,7 +5599,7 @@ Section fubini_tonelli. Variable f : T1 * T2 -> \bar R. Hypothesis mf : measurable_fun setT f. Hypothesis f0 : forall x, 0 <= f x. -Let T := [the measurableType _ of T1 * T2 : Type]. +Let T : measurableType _ := (T1 * T2)%type. Let F := fubini_F m2 f. Let G := fubini_G m1 f. @@ -5928,7 +5928,7 @@ Lemma sfinite_Fubini : Proof. pose s1 := sfinite_measure_seq m1. pose s2 := sfinite_measure_seq m2. -rewrite [LHS](eq_measure_integral [the measure _ _ of mseries s1 0]); last first. +rewrite [LHS](eq_measure_integral (mseries s1 0)); last first. by move=> A mA _; rewrite /=; exact: sfinite_measure_seqP. transitivity (\int[mseries s1 0]_x \int[mseries s2 0]_y f (x, y)). apply: eq_integral => x _; apply: eq_measure_integral => ? ? _. @@ -5973,8 +5973,8 @@ Arguments sfinite_Fubini {d d' X Y R} m1 m2 f. Section lebesgue_differentiation_continuous. Context (rT : realType). -Let mu := [the measure _ _ of @lebesgue_measure rT]. -Let R := [the measurableType _ of measurableTypeR rT]. +Let mu : measure _ _ := @lebesgue_measure rT. +Let R : measurableType _ := measurableTypeR rT. Let ballE (x : R) (r : {posnum rT}) : ball x r%:num = `](x - r%:num), (x + r%:num)[%classic :> set rT. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index c0abfbdd3..ecde135c1 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1959,8 +1959,7 @@ HB.instance Definition _ := isContent.Build _ _ R Hint Extern 0 ((_ .-ocitv).-measurable _) => solve [apply: is_ocitv] : core. -Lemma hlength_sigma_subadditive : - measurable_subset_sigma_subadditive (hlength : set (ocitv_type R) -> _). +Lemma hlength_sigma_subadditive : measurable_subset_sigma_subadditive hlength. Proof. move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE => -[a _ <-]. rewrite /subset_sigma_subadditive hlength_itv ?lte_fin/= -EFinB => lebig. @@ -1987,8 +1986,7 @@ move=> /[apply]-[i _|X _ Xc]; first exact: interval_open. have: `](a.1 + e%:num / 2), a.2] `<=` \bigcup_(i in [set` X]) Aoc i. move=> x /subset_itv_oc_cc /Xc [i /= Xi] Aooix. by exists i => //; apply: subset_itv_oo_oc Aooix. -have /[apply] := @content_sub_fsum _ _ _ - [the content _ _ of hlength : set (ocitv_type R) -> _] _ [set` X]. +have /[apply] := @content_sub_fsum _ _ _ hlength _ [set` X]. move=> /(_ _ _ _)/Box[]//=; apply: le_le_trans. rewrite hlength_itv ?lte_fin -?EFinD/= -addrA -opprD. by case: ltP => //; rewrite lee_fin subr_le0. @@ -2004,7 +2002,7 @@ Qed. HB.instance Definition _ := Content_SigmaSubAdditive_isMeasure.Build _ _ _ hlength hlength_sigma_subadditive. -Lemma hlength_sigma_finite : sigma_finite setT (hlength : set (ocitv_type R) -> _). +Lemma hlength_sigma_finite : sigma_finite setT hlength. Proof. exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic); first by rewrite bigcup_itvT. by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltry. @@ -2024,15 +2022,14 @@ End hlength_extension. End LebesgueMeasure. Definition lebesgue_measure {R : realType} : - set [the measurableType _.-sigma of - g_sigma_algebraType R.-ocitv.-measurable] -> \bar R := - [the measure _ _ of lebesgue_stieltjes_measure idfun]. + set (g_sigma_algebraType R.-ocitv.-measurable) -> \bar R := + lebesgue_stieltjes_measure idfun. HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). HB.instance Definition _ (R : realType) := SigmaFiniteMeasure.on (@lebesgue_measure R). Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R := - [the measure _ _ of completed_lebesgue_stieltjes_measure idfun]. + completed_lebesgue_stieltjes_measure idfun. HB.instance Definition _ (R : realType) := Measure.on (@completed_lebesgue_measure R). HB.instance Definition _ (R : realType) := @@ -2301,8 +2298,7 @@ Section lebesgue_measure_itv. Variable R : realType. Let lebesgue_measure_itvoc (a b : R) : - (lebesgue_measure (`]a, b] : set R) = - wlength [the cumulative _ of idfun] `]a, b])%classic. + (lebesgue_measure (`]a, b] : set R) = wlength idfun `]a, b])%classic. Proof. rewrite /lebesgue_measure/= /lebesgue_stieltjes_measure/= /measure_extension/=. by rewrite measurable_mu_extE//; exact: is_ocitv. @@ -2327,7 +2323,7 @@ rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)); last first. by rewrite ler_ltB// invr_lt1 ?unitfE// ltr1n ltnS lt0n. by rewrite !(EFinB,EFinN) fin_num_oppeB// addeAC addeA subee// add0e. apply/cvg_lim => //=; apply/fine_cvgP; split => /=; first exact: nearW. -apply/(@cvgrPdist_lt _ [the pseudoMetricNormedZmodType R of R^o]) => _/posnumP[e]. +apply/(@cvgrPdist_lt _ R^o) => _/posnumP[e]. near=> n; rewrite opprB addrCA subrr addr0 ger0_norm//. by near: n; exact: near_infty_natSinv_lt. Unshelve. all: by end_near. Qed. @@ -2347,8 +2343,7 @@ by rewrite in_itv/= => + xa; rewrite xa ltxx andbF. Qed. Let lebesgue_measure_itvoo (a b : R) : - (lebesgue_measure (`]a, b[ : set R) = - wlength [the cumulative _ of idfun] `]a, b[)%classic. + (lebesgue_measure (`]a, b[ : set R) = wlength idfun `]a, b[)%classic. Proof. have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt. have := lebesgue_measure_itvoc a b. @@ -2358,8 +2353,7 @@ rewrite 2!wlength_itv => <-; rewrite -setUitv1// measureU//. Qed. Let lebesgue_measure_itvcc (a b : R) : - (lebesgue_measure (`[a, b] : set R) = - wlength [the cumulative _ of idfun] `[a, b])%classic. + (lebesgue_measure (`[a, b] : set R) = wlength idfun `[a, b])%classic. Proof. have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0// -leNgt. have := lebesgue_measure_itvoc a b. @@ -2369,8 +2363,7 @@ rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//. Qed. Let lebesgue_measure_itvco (a b : R) : - (lebesgue_measure (`[a, b[ : set R) = - wlength [the cumulative _ of idfun] `[a, b[)%classic. + (lebesgue_measure (`[a, b[ : set R) = wlength idfun `[a, b[)%classic. Proof. have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt. have := lebesgue_measure_itvoo a b. @@ -2381,7 +2374,7 @@ Qed. Let lebesgue_measure_itv_bnd (x y : bool) (a b : R) : lebesgue_measure ([set` Interval (BSide x a) (BSide y b)] : set R) = - wlength [the cumulative _ of idfun] [set` Interval (BSide x a) (BSide y b)]. + wlength idfun [set` Interval (BSide x a) (BSide y b)]. Proof. by move: x y => [|] [|]; [exact: lebesgue_measure_itvco | exact: lebesgue_measure_itvcc | exact: lebesgue_measure_itvoo | @@ -2566,7 +2559,7 @@ End negligible_outer_measure. Section lebesgue_regularity. Local Open Scope ereal_scope. Context {R : realType}. -Let mu := [the measure _ _ of @lebesgue_measure R]. +Let mu : measure _ _ := @lebesgue_measure R. Lemma lebesgue_regularity_outer (D : set R) (eps : R) : measurable D -> mu D < +oo -> (0 < eps)%R -> @@ -2888,7 +2881,7 @@ have FE : \sum_(n k _. exact: measurable_closure. rewrite esum_mkcond//= nneseries_esum// -fun_true//=. - by under eq_esum do rewrite (fun_if mu) (measure0 [the measure _ _ of mu]). + by under eq_esum do rewrite (fun_if mu) (measure0 mu). apply/eqP; rewrite -measure_le0. apply/lee_addgt0Pr => _ /posnumP[e]; rewrite add0e. have [N F5e] : exists N, \sum_(N <= n 0 -> exists d : {posnum R}, f (a + d%:num) <= f a + e. Proof. move=> e0; move: (cumulative_is_right_continuous f). -move=> /(_ a)/(@cvgr_dist_lt _ [the normedModType R of R^o]). -move=> /(_ _ e0)[] _ /posnumP[d] => h. +move=> /(_ a) /(@cvgr_dist_lt _ R^o) /(_ _ e0)[] _ /posnumP[d] => h. exists (PosNum [gt0 of (d%:num / 2)]) => //=. move: h => /(_ (a + d%:num / 2)) /=. rewrite opprD addrA subrr distrC subr0 ger0_norm //. @@ -397,11 +396,9 @@ move=> Dab h; have [ab|ab] := leP a0 b0; last first. by rewrite subr_ge0 cumulative_is_nondecreasing// Dab. have mab k : [set` D] k -> R.-ocitv.-measurable `]a k, b k]%classic by []. move: h; rewrite -bigcup_fset. -move/(@content_sub_fsum _ R _ [the content _ _ of wlength f] _ [set` D] - `]a0, b0]%classic (fun x => `](a x), (b x)]%classic) (finite_fset D) mab - (is_ocitv _ _)) => /=. +move/(content_sub_fsum (wlength f) (finite_fset D) mab (is_ocitv a0 b0)) => /=. rewrite wlength_itv_bnd// -lee_fin => /le_trans; apply. -rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in X in (_ <= X)%E]big_seq. +rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in leRHS]big_seq. by apply: lee_sum => i iD; rewrite wlength_itv_bnd// Dab. Qed. @@ -495,7 +492,7 @@ by case: ifP; rewrite ltey. Qed. Definition lebesgue_stieltjes_measure (f : cumulative R) := - measure_extension [the measure _ _ of wlength f]. + measure_extension (wlength f). HB.instance Definition _ (f : cumulative R) := Measure.on (lebesgue_stieltjes_measure f). @@ -514,7 +511,7 @@ Notation wlength_sigma_sub_additive := wlength_sigma_subadditive (only parsing). Section lebesgue_stieltjes_measure. Variable R : realType. -Let gitvs := [the measurableType _ of g_sigma_algebraType (@ocitv R)]. +Let gitvs : measurableType _ := g_sigma_algebraType (@ocitv R). Lemma lebesgue_stieltjes_measure_unique (f : cumulative R) (mu : {measure set gitvs -> \bar R}) : @@ -532,7 +529,7 @@ Section completed_lebesgue_stieltjes_measure. Context {R : realType}. Definition completed_lebesgue_stieltjes_measure (f : cumulative R) := - @completed_measure_extension _ _ _ [the measure _ _ of wlength f]. + @completed_measure_extension _ _ _ (wlength f). HB.instance Definition _ (f : cumulative R) := Measure.on (@completed_lebesgue_stieltjes_measure f). diff --git a/theories/measure.v b/theories/measure.v index b26b412db..691b79f9b 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -3256,7 +3256,7 @@ move=> [F UF mF]; rewrite /sfinite_measure. have mDF k : measurable (seqDU F k). apply: measurableD; first exact: (mF k).1. by apply: bigsetU_measurable => i _; exact: (mF i).1. -exists (fun k => [the measure _ _ of mrestr mu (mDF k)]) => [n|U mU]. +exists (fun k => mrestr mu (mDF k)) => [n|U mU]. - apply: lty_fin_num_fun => //=. rewrite /mrestr setTI (@le_lt_trans _ _ (mu (F n)))//. + apply: le_measure; last exact: subDsetl. @@ -3320,7 +3320,7 @@ HB.builders Context d (T : measurableType d) (R : realType) mu of @Measure_isSigmaFinite d T R mu. Lemma sfinite : sfinite_measure mu. -Proof. by apply: sfinite_measure_sigma_finite; exact: sigma_finiteT. Qed. +Proof. exact/sfinite_measure_sigma_finite/sigma_finiteT. Qed. HB.instance Definition _ := @isSFinite.Build _ _ _ mu sfinite. @@ -3337,7 +3337,7 @@ HB.instance Definition _ d (T : measurableType d) (R : realFieldType) := Lemma sfinite_mzero d (T : measurableType d) (R : realType) : sfinite_measure (@mzero d T R). -Proof. by apply: sfinite_measure_sigma_finite; exact: sigma_finite_mzero. Qed. +Proof. exact/sfinite_measure_sigma_finite/sigma_finite_mzero. Qed. HB.instance Definition _ d (T : measurableType d) (R : realType) := @isSFinite.Build d T R mzero (@sfinite_mzero d T R). @@ -3464,8 +3464,7 @@ Proof. by rewrite /s; case: cid2 => F finF muE; exact: finF. Qed. HB.instance Definition _ n := @Measure_isFinite.Build d T R (s n) (s_fin n). -Definition sfinite_measure_seq : {finite_measure set T -> \bar R}^nat := - fun n => [the {finite_measure set T -> \bar R} of s n]. +Definition sfinite_measure_seq : {finite_measure set T -> \bar R}^nat := s. Lemma sfinite_measure_seqP U : measurable U -> mu U = mseries sfinite_measure_seq O U. @@ -3627,7 +3626,7 @@ HB.instance Definition _ x := End pdirac. HB.instance Definition _ d (T : measurableType d) (R : realType) := - isPointed.Build (probability T R) [the probability _ _ of dirac point]. + isPointed.Build (probability T R) (dirac point). Section dist_sigma_algebra_instance. Context d (T : measurableType d) (R : realType). @@ -3651,7 +3650,7 @@ Definition pset : set (set (probability T R)) := [set mset U r | r in `[0%R,1%R] & U in measurable]. Definition pprobability : measurableType pset.-sigma := - [the measurableType _ of g_sigma_algebraType pset]. + g_sigma_algebraType pset. End dist_sigma_algebra_instance. @@ -4946,7 +4945,7 @@ near=> n; apply: lee_sum => i _; rewrite -measure_semi_additive2. - by rewrite setIACA setICr setI0. Unshelve. all: by end_near. Qed. -Let I := [the measurableType _ of g_sigma_algebraType (@measurable _ T)]. +Let I : measurableType _ := g_sigma_algebraType (@measurable _ T). Definition measure_extension : set I -> \bar R := mu^*. @@ -4984,7 +4983,7 @@ Lemma measure_extension_unique : sigma_finite [set: T] mu -> measure_extension X = mu' X)). Proof. move=> [F TF /all_and2[Fm muF]] mu' mu'mu X mX. -apply: (@measure_unique _ _ [the measurableType _ of I] d.-measurable F) => //. +apply: (@measure_unique _ _ I d.-measurable F) => //. - by move=> A B Am Bm; apply: measurableI. - by move=> A Am; rewrite /= /measure_extension measurable_mu_extE// mu'mu. - by move=> k; rewrite /= /measure_extension measurable_mu_extE. @@ -5006,7 +5005,7 @@ Variable mu : {measure set T -> \bar R}. Notation rT := (SetRing.type T). Let Rmu : set rT -> \bar R := SetRing.measure mu. -Let I := [the measurableType _ of caratheodory_type (mu^*)%mu]. +Let I : measurableType _ := caratheodory_type (mu^*)%mu. Definition completed_measure_extension : set I -> \bar R := (mu^*)%mu. @@ -5140,7 +5139,7 @@ Hypothesis setTC2 : setT `<=` C2. (* NB: useful? *) Lemma measurable_prod_g_measurableTypeR : - @measurable _ [the measurableType _ of T1 * g_sigma_algebraType C2 : Type] + @measurable _ (T1 * g_sigma_algebraType C2)%type = <>. Proof. rewrite measurable_prod_measurableType //; congr (<>). @@ -5198,15 +5197,13 @@ Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). Lemma measurable_fst : measurable_fun [set: T1 * T2] fst. Proof. -by have /prod_measurable_funP[] := - @measurable_id _ [the measurableType _ of (T1 * T2)%type] setT. +by have /prod_measurable_funP[] := @measurable_id _ (T1 * T2)%type setT. Qed. #[local] Hint Resolve measurable_fst : core. Lemma measurable_snd : measurable_fun [set: T1 * T2] snd. Proof. -by have /prod_measurable_funP[] := - @measurable_id _ [the measurableType _ of (T1 * T2)%type] setT. +by have /prod_measurable_funP[] := @measurable_id _ (T1 * T2)%type setT. Qed. #[local] Hint Resolve measurable_snd : core. diff --git a/theories/normedtype.v b/theories/normedtype.v index 46eba5707..81ef032d2 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1473,8 +1473,8 @@ Lemma open_itvoo_subset : Proof. move=> /[apply] -[] _/posnumP[r] /subset_ball_prop_in_itv xrA. exists r%:num => //= k; rewrite /= distrC subr0 set_itvoo => /ltr_normlW kr k0. -by apply/(subset_trans _ xrA)/subset_itvW; - [rewrite lerB//; exact: ltW | rewrite lerD//; exact: ltW]. +by apply/(subset_trans _ xrA)/subset_itvW; apply/ltW; + [rewrite ler_ltB | rewrite ler_ltD]. Qed. Lemma open_itvcc_subset : @@ -2398,8 +2398,7 @@ Variables (K : numFieldType) (m n : nat). Local Lemma ball_gt0 (x y : 'M[K]_(m.+1, n.+1)) e : ball x e y -> 0 < e. Proof. by move/(_ ord0 ord0); apply: le_lt_trans. Qed. -Lemma mx_norm_ball : - @ball _ [the pseudoMetricType K of 'M[K]_(m.+1, n.+1)] = ball_ (fun x => `| x |). +Lemma mx_norm_ball : @ball _ 'M[K]_(m.+1, n.+1) = ball_ (fun x => `| x |). Proof. rewrite /normr /ball_ predeq3E => x e y /=; rewrite mx_normE; split => xey. - have e_gt0 : 0 < e := ball_gt0 xey. @@ -2441,8 +2440,7 @@ rewrite /ball /= /prod_ball -!ball_normE /ball_ /=. by rewrite comparable_gt_max// ?real_comparable//; split=> /andP. Qed. -Lemma prod_norm_ball : - @ball _ [the pseudoMetricType K of (U * V)%type] = ball_ (fun x => `|x|). +Lemma prod_norm_ball : @ball _ (U * V)%type = ball_ (fun x => `|x|). Proof. by rewrite /= - ball_prod_normE. Qed. HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K (U * V)%type @@ -3041,7 +3039,7 @@ Qed. Lemma abse_continuous : continuous (@abse R). Proof. case=> [r|A /= [r [rreal rA]]|A /= [r [rreal rA]]]/=. -- exact/(cvg_comp (@norm_continuous _ [the normedModType R of R^o] r)). +- exact/(cvg_comp (@norm_continuous _ R r)). - by exists r; split => // y ry; apply: rA; rewrite (lt_le_trans ry)// lee_abs. - exists (- r)%R; rewrite realN; split => // y; rewrite EFinN -lteNr => yr. by apply: rA; rewrite (lt_le_trans yr)// -abseN lee_abs. @@ -4207,8 +4205,7 @@ Unshelve. all: by end_near. Qed. HB.instance Definition _ (R : realType) := Uniform_isComplete.Build R^o (@R_complete R). (* todo : delete *) -HB.instance Definition _ (R : realType) := Complete.copy R - [the completeType of R^o]. +HB.instance Definition _ (R : realType) := Complete.copy R R^o. (* new *) Section cvg_seq_bounded. @@ -4794,27 +4791,27 @@ case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=. rewrite !(lteifF, lteifT). + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx]. rewrite le_eqVlt => /orP[/eqP -> //|xsupX]. - apply: (@interior_subset [the topologicalType of R : Type]). + apply: (@interior_subset R). by rewrite interval_bounded_interior // /mkset infXx. + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx supXx]. - apply: (@interior_subset [the topologicalType of R : Type]). + apply: (@interior_subset R). by rewrite interval_bounded_interior // /mkset infXx. + move=> /andP[infXx]; rewrite le_eqVlt => /orP[/eqP -> //|xsupX]. - apply: (@interior_subset [the topologicalType of R : Type]). + apply: (@interior_subset R). by rewrite interval_bounded_interior // /mkset infXx. - + move=> ?; apply: (@interior_subset [the topologicalType of R : Type]). + + move=> ?; apply: (@interior_subset R). by rewrite interval_bounded_interior // /mkset infXx. - case: asboolP => XinfX; rewrite !(lteifF, lteifT, andbT). + rewrite le_eqVlt => /orP[/eqP<-//|infXx]. - apply: (@interior_subset [the topologicalType of R : Type]). + apply: (@interior_subset R). by rewrite interval_right_unbounded_interior. - + move=> infXx; apply: (@interior_subset [the topologicalType of R : Type]). + + move=> infXx; apply: (@interior_subset R). by rewrite interval_right_unbounded_interior. - case: asboolP => XsupX /=. + rewrite le_eqVlt => /orP[/eqP->//|xsupX]. - apply: (@interior_subset [the topologicalType of R : Type]). + apply: (@interior_subset R). by rewrite interval_left_unbounded_interior. - + move=> xsupX; apply: (@interior_subset [the topologicalType of R : Type]). + + move=> xsupX; apply: (@interior_subset R). by rewrite interval_left_unbounded_interior. - by move=> _; rewrite (interval_unbounded_setT iX). Qed. diff --git a/theories/numfun.v b/theories/numfun.v index 3a892df55..92f31a9c9 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -440,11 +440,11 @@ Qed. HB.instance Definition _ X := indic_fimfun_subproof X. -Definition indic_fimfun (X : set aT) := [the {fimfun aT >-> rT} of \1_X]. +Definition indic_fimfun (X : set aT) : {fimfun aT >-> rT} := \1_X. HB.instance Definition _ k f := FImFun.copy (k \o* f) (f * cst_fimfun k). -Definition scale_fimfun k f := [the {fimfun aT >-> rT} of k \o* f]. +Definition scale_fimfun k f : {fimfun aT >-> rT} := k \o* f. End ring. Arguments indic_fimfun {aT rT} _. @@ -598,8 +598,7 @@ exists (lim (h_ @ \oo)); split. - move=> t /set_mem At; have /pointwise_cvgP/(_ t)/(cvg_lim (@Rhausdorff _)) := !! pointwise_uniform_cvg _ cvgh. rewrite -fmap_comp /comp /h_ => <-; apply/esym/(@cvg_lim _ (@Rhausdorff R)). - apply: (@cvg_zero R [the pseudoMetricNormedZmodType R of R^o]). - apply: norm_cvg0; under eq_fun => n. + apply: (@cvg_zero R R^o); apply: norm_cvg0; under eq_fun => n. rewrite distrC /series /cst /= -mulN1r fct_sumE mulr_sumr. under [fun _ : nat => _]eq_fun => ? do rewrite mulN1r -fgE opprB. rewrite telescope_sumr //= addrCA subrr addr0. diff --git a/theories/probability.v b/theories/probability.v index c958e511f..11f4d758c 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -569,9 +569,8 @@ Local Notation "'M_ X t" := (mmt_gen_fun X t). Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> P [set x | X x >= a]%R <= 'M_X r * (expR (- (r * a)))%:E. Proof. -move=> t0. -rewrite /mmt_gen_fun; have -> : expR \o r \o* X = - (normr \o normr) \o [the {mfun _ >-> _} of expR \o r \o* X]. +move=> t0; rewrite /mmt_gen_fun. +have -> : expR \o r \o* X = (normr \o normr) \o (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. @@ -600,7 +599,7 @@ have h (Y : {RV P >-> R}) : - by move=> x /=; exact: sqr_ge0. - by move=> x /=; exact: sqr_ge0. - by apply/aeW => t /=; rewrite real_normK// num_real. -have := h [the {mfun T >-> R} of (X \- cst (fine ('E_P[X])))%R]. +have := h (X \- cst (fine ('E_P[X])))%R. by move=> /le_trans; apply; rewrite /variance [in leRHS]unlock. Qed. diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index 89a01e9d6..023e28739 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -955,8 +955,7 @@ Definition type : Type := let _ := countableBase in let _ := entF in T. #[export] HB.instance Definition _ {q : Pointed T} := Pointed.copy type (Pointed.Pack q). -Lemma countable_uniform_bounded (x y : T) : - let U := [the pseudoMetricType R of type] in @ball _ U x 2 y. +Lemma countable_uniform_bounded (x y : T) : @ball _ type x 2 y. Proof. rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN. rewrite [X in `|X|%N](_ : _ = 0) ?absz0//. diff --git a/theories/topology_theory/bool_topology.v b/theories/topology_theory/bool_topology.v index 29b8dc62f..ef2df6951 100644 --- a/theories/topology_theory/bool_topology.v +++ b/theories/topology_theory/bool_topology.v @@ -48,7 +48,7 @@ End bool_ord_topology. Lemma discrete_bool_compact : compact [set: discrete_topology discrete_bool]. Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed. -Definition pseudoMetric_bool {R : realType} := - [the pseudoMetricType R of discrete_topology discrete_bool : Type]. +Definition pseudoMetric_bool {R : realType} : pseudoMetricType R := + discrete_topology discrete_bool. #[global] Hint Resolve discrete_bool : core. diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index 0168e1809..adada2fa9 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -249,8 +249,7 @@ Lemma closure_subspaceW (U : set T) : U `<=` A -> closure (U : set (subspace A)) = closure (U : set T) `&` A. Proof. have /closed_subspaceP := (@closed_closure _ (U : set (subspace A))). -move=> [V] [clV VAclUA]. -move=> /[dup] /(@closure_subset [the topologicalType of subspace _]). +move=> [V] [clV VAclUA] /[dup] /(@closure_subset (subspace _)). have /closure_id <- := closed_subspaceT => /setIidr <-; rewrite setIC. move=> UsubA; rewrite eqEsubset; split. apply: setSI; rewrite closureE; apply: smallest_sub (@subset_closure _ U). diff --git a/theories/topology_theory/supremum_topology.v b/theories/topology_theory/supremum_topology.v index 7546e0b1b..14cec1014 100644 --- a/theories/topology_theory/supremum_topology.v +++ b/theories/topology_theory/supremum_topology.v @@ -45,7 +45,7 @@ move=> Ffilt; split=> cvFt. move=> _ ->; exists [fset B]%fset. by move=> ?; rewrite inE inE => /eqP->; exists i. by rewrite predeqE=> ?; split=> [|??]; [apply|]; rewrite /= inE // =>/eqP->. -move=> A /=; rewrite (@nbhsE [the topologicalType of S]). +move=> A /=; rewrite (@nbhsE S). move=> [_ [[B sB <-] [C BC Ct] sUBA]]. rewrite nbhs_filterE; apply: filterS sUBA _; apply: (@filterS _ _ _ C). by move=> ? ?; exists C.