diff --git a/classical/boolp.v b/classical/boolp.v index ab36ee72c1..0eda8522c7 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -106,8 +106,11 @@ Proof. by have [propext _] := extensionality; apply: propext. Qed. Ltac eqProp := apply: propext; split. +Lemma funext_dep {T} {U : T -> Type} (f g : forall t, U t) : (forall t, f t = g t) -> f = g. +Proof. exact/functional_extensionality_dep. Qed. + Lemma funext {T U : Type} (f g : T -> U) : (f =1 g) -> f = g. -Proof. by case: extensionality=> _; apply. Qed. +Proof. exact/funext_dep. Qed. Lemma propeqE (P Q : Prop) : (P = Q) = (P <-> Q). Proof. by apply: propext; split=> [->|/propext]. Qed. diff --git a/classical/cardinality.v b/classical/cardinality.v index c84602f5f8..d072a56223 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -1340,7 +1340,7 @@ Section zmod. Context (aT : Type) (rT : zmodType). Lemma fimfun_zmod_closed : zmod_closed (@fimfun aT rT). Proof. -split=> [|f g]; rewrite !inE/=; first exact: finite_image_cst. +split=> [|f g]; rewrite !inE/=; first exact: (finite_image_cst 0). by move=> fA gA; apply: (finite_image11 (fun x y => x - y)). Qed. HB.instance Definition _ := diff --git a/classical/functions.v b/classical/functions.v index e40e2819cb..dd55415560 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -2568,61 +2568,132 @@ Qed. Obligation Tactic := idtac. -Program Definition fct_zmodMixin (T : Type) (M : zmodType) := - @GRing.isZmodule.Build (T -> M) \0 (fun f x => - f x) (fun f g => f \+ g) +Definition add_fun {aT} {rT : aT -> nmodType} (f g : forall x, rT x) x := f x + g x. +Definition opp_fun {aT} {rT : aT -> zmodType} (f : forall x, rT x) x := - f x. +Definition sub_fun {aT} {rT : aT -> zmodType} (f g : forall x, rT x) x := f x - g x. +Definition mul_fun {aT} {rT : aT -> semiRingType} (f g : forall x, rT x) x := f x * g x. +Definition scale_fun {aT} {R} {rT : aT -> lmodType R} (k : R) (f : forall x, rT x) x := k *: f x. + +Notation "f \+ g" := (add_fun f g) : ring_scope. +Notation "\- f" := (opp_fun f) : ring_scope. +Notation "f \- g" := (sub_fun f g) : ring_scope. +Notation "f \* g" := (mul_fun f g) : ring_scope. +Notation "k \*: f" := (scale_fun k f) : ring_scope. + +Arguments add_fun {_ _} f g _ /. +Arguments opp_fun {_ _} f _ /. +Arguments sub_fun {_ _} f g _ /. +Arguments mul_fun {_ _} f g _ /. +Arguments scale_fun {_ _ _} k f _ /. + +Program Definition fct_zmodMixin (T : Type) (M : T -> zmodType) := + @GRing.isZmodule.Build (forall t, M t) (fun=> 0) (fun f => \- f) (fun f g => f \+ g) _ _ _ _. -Next Obligation. by move=> T M f g h; rewrite funeqE=> x /=; rewrite addrA. Qed. -Next Obligation. by move=> T M f g; rewrite funeqE=> x /=; rewrite addrC. Qed. -Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite add0r. Qed. -Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite addNr. Qed. -HB.instance Definition _ (T : Type) (M : zmodType) := fct_zmodMixin T M. - -Program Definition fct_ringMixin (T : pointedType) (M : ringType) := - @GRing.Zmodule_isRing.Build (T -> M) (cst 1) (fun f g => f \* g) _ _ _ _ _ _. -Next Obligation. by move=> T M f g h; rewrite funeqE=> x /=; rewrite mulrA. Qed. -Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite mul1r. Qed. -Next Obligation. by move=> T M f; rewrite funeqE=> x /=; rewrite mulr1. Qed. -Next Obligation. by move=> T M f g h; rewrite funeqE=> x/=; rewrite mulrDl. Qed. -Next Obligation. by move=> T M f g h; rewrite funeqE=> x/=; rewrite mulrDr. Qed. Next Obligation. -by move=> T M ; apply/eqP; rewrite funeqE => /(_ point) /eqP; rewrite oner_eq0. +by move=> T M f g h; apply/funext_dep => x /=; rewrite addrA. Qed. -HB.instance Definition _ (T : pointedType) (M : ringType) := fct_ringMixin T M. +Next Obligation. +by move=> T M f g; apply/funext_dep => x /=; rewrite addrC. +Qed. +Next Obligation. +by move=> T M f; apply/funext_dep => x /=; rewrite add0r. +Qed. +Next Obligation. +by move=> T M f; apply/funext_dep => x /=; rewrite addNr. +Qed. +HB.instance Definition _ (T : Type) (M : T -> zmodType) := fct_zmodMixin M. -Program Definition fct_comRingType (T : pointedType) (M : comRingType) := - GRing.Ring_hasCommutativeMul.Build (T -> M) _. +Program Definition fct_ringMixin (T : pointedType) (M : T -> ringType) := + @GRing.Zmodule_isRing.Build (forall t, M t) (fun=> 1) (fun f g => f \* g) _ _ _ _ _ _. +Next Obligation. +by move=> T M f g h; apply/funext_dep => x /=; rewrite mulrA. +Qed. Next Obligation. -by move=> T M f g; rewrite funeqE => x; rewrite /GRing.mul/= mulrC. +by move=> T M f; apply/funext_dep => x /=; rewrite mul1r. Qed. -HB.instance Definition _ (T : pointedType) (M : comRingType) := - fct_comRingType T M. +Next Obligation. +by move=> T M f; apply/funext_dep => x /=; rewrite mulr1. +Qed. +Next Obligation. +by move=> T M f g h; apply/funext_dep => x/=; rewrite mulrDl. +Qed. +Next Obligation. +by move=> T M f g h; apply/funext_dep => x/=; rewrite mulrDr. +Qed. +Next Obligation. +by move=> T M ; apply/eqP => /(congr1 (fun f => f point)) /eqP; rewrite oner_eq0. +Qed. +HB.instance Definition _ (T : pointedType) (M : T -> ringType) := fct_ringMixin M. + +Program Definition fct_comRingType (T : pointedType) (M : T -> comRingType) := + GRing.Ring_hasCommutativeMul.Build (forall t, M t) _. +Next Obligation. +by move=> T M f g; apply/funext_dep => x; apply/mulrC. +Qed. +HB.instance Definition _ (T : pointedType) (M : T -> comRingType) := + fct_comRingType M. Section fct_lmod. -Variables (U : Type) (R : ringType) (V : lmodType R). -Program Definition fct_lmodMixin := @GRing.Zmodule_isLmodule.Build R (U -> V) +Variables (U : Type) (R : ringType) (V : U -> lmodType R). +Program Definition fct_lmodMixin := @GRing.Zmodule_isLmodule.Build R (forall u, V u) (fun k f => k \*: f) _ _ _ _. -Next Obligation. by move=> k f v; rewrite funeqE=> x; exact: scalerA. Qed. -Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite scale1r. Qed. Next Obligation. -by move=> f g h; rewrite funeqE => x /=; rewrite scalerDr. +by move=> k f v; apply/funext_dep => x; exact: scalerA. +Qed. +Next Obligation. +by move=> f; apply/funext_dep => x /=; rewrite scale1r. +Qed. +Next Obligation. +by move=> f g h; apply/funext_dep => x /=; rewrite scalerDr. Qed. Next Obligation. -by move=> f g h; rewrite funeqE => x /=; rewrite scalerDl. +by move=> f g h; apply/funext_dep => x /=; rewrite scalerDl. Qed. HB.instance Definition _ := fct_lmodMixin. End fct_lmod. -Lemma fct_sumE (I T : Type) (M : zmodType) r (P : {pred I}) (f : I -> T -> M) +Lemma add_funE (T : pointedType) (M : T -> zmodType) (f g : forall t, M t) : + (f + g) = f \+ g. +Proof. exact/funext_dep. Qed. + +Lemma opp_funE (T : Type) (M : T -> zmodType) (f : forall t, M t) : - f = \- f. +Proof. exact/funext_dep. Qed. + +Lemma sub_funE (T : Type) (M : T -> zmodType) (f g : forall t, M t) : + (f - g) = f \- g. +Proof. exact/funext_dep. Qed. + +Lemma fct_sumE (I T : Type) (M : T -> zmodType) r (P : {pred I}) (f : I -> forall t, M t) (x : T) : (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x. Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed. +Lemma mul_funE (T : pointedType) (M : T -> ringType) (f g : forall t, M t) : + (f * g) = f \* g. +Proof. exact/funext_dep. Qed. + +Lemma scale_funE (T : Type) (R : ringType) (M : T -> lmodType R) (k : R) (f : forall t, M t) : + k *: f = k \*: f. +Proof. exact/funext_dep. Qed. + Lemma mul_funC (T : Type) {R : comSemiRingType} (f : T -> R) (r : R) : r \*o f = r \o* f. Proof. by apply/funext => x/=; rewrite mulrC. Qed. End function_space. +Notation "f \+ g" := (add_fun f g) : ring_scope. +Notation "\- f" := (opp_fun f) : ring_scope. +Notation "f \- g" := (sub_fun f g) : ring_scope. +Notation "f \* g" := (mul_fun f g) : ring_scope. +Notation "k \*: f" := (scale_fun k f) : ring_scope. + +Arguments add_fun {_ _} f g _ /. +Arguments opp_fun {_ _} f _ /. +Arguments sub_fun {_ _} f g _ /. +Arguments mul_fun {_ _} f g _ /. +Arguments scale_fun {_ _ _} k f _ /. + Section function_space_lemmas. Local Open Scope ring_scope. Import GRing.Theory. diff --git a/theories/derive.v b/theories/derive.v index 2cd1198f76..8c7615a735 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -224,7 +224,7 @@ Section diff_locally_converse_tentative. (* and thus a littleo of 1, and so is id *) (* This can be generalized to any dimension *) Lemma diff_locally_converse_part1 (f : R -> R) (a b x : R) : - f \o shift x = cst a + b *: idfun +o_ 0 id -> f x = a. + f \o shift x = cst a + b *: (@idfun R) +o_ 0 id -> f x = a. Proof. rewrite funeqE => /(_ 0) /=; rewrite add0r => ->. by rewrite -[LHS]/(_ 0 + _ 0 + _ 0) /cst [X in a + X]scaler0 littleo_lim0 ?addr0. @@ -253,12 +253,12 @@ Lemma derivable_nbhs (f : V -> W) a v : Proof. move=> df; apply/eqaddoP => _/posnumP[e]. rewrite -nbhs_nearE nbhs_simpl /= dnbhsE; split; last first. - rewrite /at_point opprD -![(_ + _ : _ -> _) _]/(_ + _) scale0r add0r. + rewrite /at_point opprD !add_funE !opp_funE/= scale0r add0r. by rewrite addrA subrr add0r normrN scale0r !normr0 mulr0. have /eqolimP := df. move=> /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]). apply: filter_app; rewrite /= !near_simpl near_withinE; near=> h => hN0. -rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _). +rewrite /= opprD !add_funE !opp_funE. rewrite /cst /= [`|1|]normr1 mulr1 => dfv. rewrite addrA -[X in X + _]scale1r -(@mulVf _ h) //. rewrite mulrC -scalerA -scalerBr normrZ. @@ -276,7 +276,7 @@ move=> df; apply/cvg_ex; exists ('D_v f a). apply/(@eqolimP _ _ _ (dnbhs_filter_on _))/eqaddoP => _/posnumP[e]. have /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]) := df. rewrite /= !(near_simpl, near_withinE); apply: filter_app; near=> h. -rewrite /= opprD -![(_ + _ : _ -> _) _]/(_ + _) -![(- _ : _ -> _) _]/(- _). +rewrite /= opprD !add_funE !opp_funE. rewrite /cst /= [`|1|]normr1 mulr1 addrA => dfv hN0. rewrite -[X in _ - X]scale1r -(@mulVf _ h) //. rewrite -scalerA -scalerBr normrZ normfV ler_pdivrMl ?normr_gt0 //. @@ -398,7 +398,7 @@ Variable R : numFieldType. Fact dcst (V W : normedModType R) (a : W) (x : V) : continuous (0 : V -> W) /\ cst a \o shift x = cst (cst a x) + \0 +o_ 0 id. Proof. -split; first exact: cst_continuous. +split; first exact: (@cst_continuous _ _ 0). apply/eqaddoE; rewrite addr0 funeqE => ? /=; rewrite -[LHS]addr0; congr (_ + _). by rewrite littleoE; last exact: littleo0_subproof. Qed. @@ -412,7 +412,7 @@ Fact dadd (f g : V -> W) x : Proof. move=> df dg; split => [?|]; do ?exact: continuousD. apply/(@eqaddoE R); rewrite funeqE => y /=; rewrite -[(f + g) _]/(_ + _). -by rewrite ![_ (_ + x)]diff_locallyx// addrACA addox addrACA. +by rewrite add_funE ![_ (_ + x)]diff_locallyx// addrACA addox addrACA. Qed. Fact dopp (f : V -> W) x : @@ -521,8 +521,8 @@ Lemma diff_unique (V W : normedModType R) (f : V -> W) continuous df -> f \o shift x = cst (f x) + df +o_ 0 id -> 'd f x = df :> (V -> W). Proof. -move=> dfc dxf; apply/subr0_eq; rewrite -[LHS]/(_ \- _). -apply/littleo_linear0/eqoP/eq_some_oP => /=; rewrite funeqE => y /=. +move=> dfc dxf; apply/subr0_eq/(@littleo_linear0 _ _ (GRing.sub_fun _ _))/eqoP. +apply/eq_some_oP => /=; rewrite funeqE => y /=. have hdf h : (f \o shift x = cst (f x) + h +o_ 0 id) -> h = f \o shift x - cst (f x) +o_ 0 id. move=> hdf; apply: eqaddoE. @@ -544,7 +544,7 @@ by rewrite littleo_center0 (comp_centerK x id) -[- _ in RHS](comp_centerK x). Qed. Lemma diff_cst (V W : normedModType R) a x : ('d (cst a) x : V -> W) = 0. -Proof. by apply/diff_unique; have [] := dcst a x. Qed. +Proof. by apply/(@diff_unique _ _ _ \0); have [] := dcst a x. Qed. Variables (V W : normedModType R). @@ -558,7 +558,10 @@ Proof. exact: DiffDef (differentiable_cst _ _) (diff_cst _ _). Qed. Lemma diffD (f g : V -> W) x : differentiable f x -> differentiable g x -> 'd (f + g) x = 'd f x \+ 'd g x :> (V -> W). -Proof. by move=> df dg; apply/diff_unique; have [] := dadd df dg. Qed. +Proof. +move=> df dg. +by apply/(@diff_unique _ _ _ (GRing.add_fun _ _)); have [] := dadd df dg. +Qed. Lemma differentiableD (f g : V -> W) x : differentiable f x -> differentiable g x -> differentiable (f + g) x. @@ -576,7 +579,8 @@ Qed. Lemma differentiable_sum n (f : 'I_n -> V -> W) (x : V) : (forall i, differentiable (f i) x) -> differentiable (\sum_(i < n) f i) x. Proof. -by elim/big_ind : _ => // ? ? g h ?; apply: differentiableD; [exact:g|exact:h]. +elim/big_ind : _ => //[_|? ? g h ?]; first exact/(@differentiable_cst _ 0). +by apply: differentiableD; [exact:g|exact:h]. Qed. Lemma diffN (f : V -> W) x : @@ -614,7 +618,10 @@ Proof. by move=> /differentiableP df /differentiableP dg. Qed. Lemma diffZ (f : V -> W) k x : differentiable f x -> 'd (k *: f) x = k \*: 'd f x :> (V -> W). -Proof. by move=> df; apply/diff_unique; have [] := dscale k df. Qed. +Proof. +move=> df. +by apply/(@diff_unique _ _ _ (GRing.scale_fun _ _)); have [] := dscale k df. +Qed. Lemma differentiableZ (f : V -> W) k x : differentiable f x -> differentiable (k *: f) x. @@ -1152,7 +1159,7 @@ Global Instance is_derive_sum n (h : 'I_n -> V -> W) (x v : V) (dh : 'I_n -> W) : (forall i, is_derive x v (h i) (dh i)) -> is_derive x v (\sum_(i < n) h i) (\sum_(i < n) dh i). Proof. -by elim/big_ind2 : _ => // [|] *; [exact: is_derive_cst|exact: is_deriveD]. +by elim/big_ind2 : _ => // [|] *; [exact/(is_derive_cst 0)|exact: is_deriveD]. Qed. Lemma derivable_sum n (h : 'I_n -> V -> W) (x v : V) : @@ -1324,7 +1331,10 @@ by rewrite [in LHS]mulr_natl exprfctE -mulrSr mulr_natl. Qed. Lemma derivableX f n (x v : V) : derivable f x v -> derivable (f ^+ n) x v. -Proof. by case: n => [_|n /derivableP]; [rewrite expr0|]. Qed. +Proof. +case: n => [_|n /derivableP]; last by []. +by rewrite expr0; apply/(derivable_cst (1 : R)). +Qed. Lemma deriveX f n (x v : V) : derivable f x v -> 'D_v (f ^+ n.+1) x = (n.+1%:R * f x ^+ n) *: 'D_v f x. @@ -1378,7 +1388,7 @@ Proof. by rewrite derive1E derive_cst. Qed. Lemma exprn_derivable {R : numFieldType} n (x : R) v : derivable (@GRing.exp R ^~ n) x v. Proof. -elim: n => [/=|n ih]; first by rewrite (_ : _ ^~ _ = 1). +elim: n => [/=|n ih]; first by rewrite (_ : _ ^~ _ = cst 1). rewrite (_ : _ ^~ _ = (fun x => x * x ^+ n)); last first. by apply/funext => y; rewrite exprS. by apply: derivableM; first exact: derivable_id. @@ -1573,7 +1583,7 @@ have gcont : {within `[a, b], continuous g}. move=> x; apply: continuousD _ ; first by move=>?; exact: fcont. by apply/continuousN/continuous_subspaceT=> ?; exact: scalel_continuous. have gaegb : g a = g b. - rewrite /g -![(_ - _ : _ -> _) _]/(_ - _). + rewrite /g !add_funE !opp_funE. apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl. rewrite [_ *: _]mulrA mulrC mulrA mulVf. by rewrite mul1r addrCA subrr addr0. diff --git a/theories/esum.v b/theories/esum.v index 57959228b9..9fbff2bd2b 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -587,9 +587,10 @@ move=> /cvgrPdist_lt cvgAB; apply/cvgrPdist_lt => e e0. move: cvgAB => /(_ _ e0) [N _/= hN] /=. near=> n. rewrite distrC subr0. -have -> : (C_ = A_ \- B_)%R. +have -> : (C_ = A_ - B_)%R. apply/funext => k. - rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//. + rewrite /= /A_ /C_ /B_ sub_funE/=. + rewrite -sumrN -big_split/= -summable_fine_sum//. apply eq_bigr => i Pi; rewrite -fineB//. - by rewrite [in LHS](funeposneg f). - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funepos. diff --git a/theories/ftc.v b/theories/ftc.v index 4f553f2c11..d91c2f961f 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -839,7 +839,8 @@ set f := fun x => if x == a then r else if x == b then l else F^`() x. have fE : {in `]a, b[, F^`() =1 f}. by move=> x; rewrite in_itv/= => /andP[ax xb]; rewrite /f gt_eqF// lt_eqF. have DPGFE : {in `]a, b[, (- (PG \o F))%R^`() =1 ((G \o F) * (- f))%R}. - move=> x /[dup]xab /andP[ax xb]; rewrite derive1_comp //; last first. + move=> x /[dup]xab /andP[ax xb]. + rewrite (@derive1_comp _ _ (@GRing.opp R)) //; last first. apply: diff_derivable; apply: differentiable_comp; apply/derivable1_diffP. by case: Fab => + _ _; exact. by case: PGFbFa => + _ _; apply; exact: decreasing_image_oo. @@ -886,7 +887,8 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first. - have [/= dF rF lF] := Fab. have := derivable_oo_continuous_bnd_within PGFbFa. move=> /(continuous_within_itvP _ FbFa)[_ PGFb PGFa]; split => /=. - - move=> x xab; apply/derivable1_diffP; apply: differentiable_comp => //. +- move=> x xab; apply/derivable1_diffP. + apply: (differentiable_comp (g:=@GRing.opp R)) => //. apply: differentiable_comp; apply/derivable1_diffP. by case: Fab => + _ _; exact. by case: PGFbFa => + _ _; apply; exact: decreasing_image_oo. @@ -909,7 +911,7 @@ rewrite oppeD//= -(continuous_FTC2 ab _ _ DPGFE); last 2 first. rewrite gtr0_norm// ?subr_gt0//. by near: t; exact: nbhs_left_ltBl. apply: eq_integral_itv_bounded. -- rewrite mulrN; apply: measurableT_comp => //. + - rewrite mulrN; apply: (measurableT_comp (f:=@GRing.opp R)) => //. apply: (eq_measurable_fun ((G \o F) * F^`())%R) => //. by move=> x; rewrite inE/= => xab; rewrite !fctE fE. by move: mGFF'; apply: measurable_funS => //; exact: subset_itv_oo_cc. @@ -994,13 +996,14 @@ have mF' : measurable_fun `]a, b[ F^`(). apply: subspace_continuous_measurable_fun => //. by apply: continuous_in_subspaceT => x /[!inE] xab; exact: cF'. rewrite integral_itv_bndoo//; last first. - rewrite compA -(compA G -%R) (_ : -%R \o -%R = id); last first. + rewrite (compA _ -%R) -(compA G -%R) (_ : -%R \o -%R = id); last first. by apply/funext => y; rewrite /= opprK. - apply: measurable_funM => //; apply: measurableT_comp => //. + apply: measurable_funM => //. + apply: (measurableT_comp (f:=@GRing.opp R)) => //. apply: (@eq_measurable_fun _ _ _ _ _ (- F^`())%R). move=> x /[!inE] xab; rewrite [in RHS]derive1E deriveN -?derive1E//. by case: Fab => + _ _; apply. - exact: measurableT_comp. + exact: (measurableT_comp (f:=@GRing.opp R)). rewrite [in RHS]integral_itv_bndoo//; last exact: measurable_funM. apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN. - by rewrite opprK -derive1E. diff --git a/theories/landau.v b/theories/landau.v index bee296e962..e6a9660137 100644 --- a/theories/landau.v +++ b/theories/landau.v @@ -414,7 +414,7 @@ Proof. by rewrite [RHS]littleoE. Qed. Lemma oppox (F : filter_on T) (f : T -> V) e x : - [o_F e of f] x = [o_F e of - [o_F e of f]] x. -Proof. by move: x; rewrite -/(- _ =1 _) {1}oppo. Qed. +Proof. by move: x; rewrite -/(- [o_F e of f] =1 _) {1}oppo. Qed. Lemma eqadd_some_oP (F : filter_on T) (f g : T -> V) (e : T -> W) h : f = g + [o_F e of h] -> littleo_def F (f - g) e. @@ -596,7 +596,7 @@ Proof. by rewrite [RHS]bigOE. Qed. Lemma oppOx (F : filter_on T) (f : T -> V) e x : - [O_F e of f] x = [O_F e of - [O_F e of f]] x. -Proof. by move: x; rewrite -/(- _ =1 _) {1}oppO. Qed. +Proof. by move: x; rewrite -/(- [O_F e of f] =1 _) {1}oppO. Qed. Lemma add_bigO_subproof (F : filter_on T) e (df dg : {O_F e}) : bigO_def F (df \+ dg) e. @@ -618,7 +618,7 @@ Proof. by rewrite [RHS]bigOE. Qed. Lemma addOx (F : filter_on T) (f g: T -> V) e x : [O_F e of f] x + [O_F e of g] x = [O_F e of [O_F e of f] + [O_F e of g]] x. -Proof. by move: x; rewrite -/(_ + _ =1 _) {1}addO. Qed. +Proof. by move: x; rewrite -/([O_F e of f] + _ =1 _) {1}addO. Qed. Lemma eqadd_some_OP (F : filter_on T) (f g : T -> V) (e : T -> W) h : f = g + [O_F e of h] -> bigO_def F (f - g) e. @@ -848,7 +848,7 @@ Proof. by rewrite [RHS]littleoE. Qed. Lemma addox (F : filter_on T) (f g: T -> V) (e : _ -> W) x : [o_F e of f] x + [o_F e of g] x = [o_F e of [o_F e of f] + [o_F e of g]] x. -Proof. by move: x; rewrite -/(_ + _ =1 _) {1}addo. Qed. +Proof. by move: x; rewrite -/([o_F e of f] + _ =1 _) {1}addo. Qed. (* duplicate from Section Domination *) Hint Extern 0 (littleo_def _ _ _) => solve[apply: littleoP] : core. @@ -871,7 +871,7 @@ Proof. by rewrite [RHS]littleoE. Qed. Lemma scaleox (F : filter_on T) a (f : T -> V) (e : _ -> W) x : a *: ([o_F e of f] x) = [o_F e of a *: [o_F e of f]] x. -Proof. by move: x; rewrite -/(_ *: _ =1 _) {1}scaleo. Qed. +Proof. by move: x; rewrite -/(_ *: [o_F e of f] =1 _) {1}scaleo. Qed. End Domination_numFieldType. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index b043af47cd..c6c0afb28d 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -251,7 +251,7 @@ Context d (aT : measurableType d) (rT : realType). Lemma mfun_subring_closed : subring_closed (@mfun _ _ aT rT). Proof. split=> [|f g|f g]; rewrite !inE/=. -- exact: measurable_cst. +- exact: measurable_cst (1 : rT). - exact: measurable_funB. - exact: measurable_funM. Qed. @@ -5991,7 +5991,8 @@ Qed. Lemma locally_integrableN D f : locally_integrable D f -> locally_integrable D (\- f)%R. Proof. -move=> [mf oD foo]; split => //; first exact: measurableT_comp. +move=> [mf oD foo]; split => //. + exact: (measurableT_comp (f:=@GRing.opp R)). by move=> K KD cK; under eq_integral do rewrite normrN; exact: foo. Qed. @@ -6482,10 +6483,10 @@ Proof. move=> xU mU mUf cg locg; apply/eqP; rewrite eq_le; apply/andP; split. - rewrite [leRHS](_ : _ = f^* x + (\- g)%R^* x). apply: (lim_sup_davg_le xU) => //. - apply/(measurable_comp measurableT) => //. + apply/(measurable_comp (f:=@GRing.opp R) measurableT) => //. by case: locg => + _ _; exact: measurable_funS. rewrite (@continuous_lim_sup_davg (- g)%R _ _ xU mU); first by rewrite adde0. - - apply/(measurable_comp measurableT) => //. + - apply/(measurable_comp (f:=@GRing.opp R) measurableT) => //. by case: locg => + _ _; apply: measurable_funS. + by move=> y; exact/continuousN/cg. - rewrite [leRHS](_ : _ = ((f \- g)%R^* \+ g^*) x)//. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index e658b9a261..9e3631e656 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1002,7 +1002,9 @@ Qed. Lemma measurable_funB D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \- g). -Proof. by move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp. Qed. +Proof. +by move=> ? ?; apply: measurable_funD =>//; exact: measurableT_comp. +Qed. Lemma measurable_funM D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \* g). diff --git a/theories/numfun.v b/theories/numfun.v index f3361cce02..845be3339a 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -409,13 +409,15 @@ Context (aT : pointedType) (rT : ringType). Lemma fimfun_mulr_closed : mulr_closed (@fimfun aT rT). Proof. -split=> [|f g]; rewrite !inE/=; first exact: finite_image_cst. +split=> [|f g]; rewrite !inE/=; first exact: finite_image_cst 1. by move=> fA gA; exact: (finite_image11 (fun x y => x * y)). Qed. HB.instance Definition _ := @GRing.isMulClosed.Build _ (@fimfun aT rT) fimfun_mulr_closed. -HB.instance Definition _ := [SubZmodule_isSubRing of {fimfun aT >-> rT} by <:]. +(* TODO: Why is this not known to HB? *) +HB.instance Definition _ := @GRing.ZmodClosed.on (@fimfun aT rT). +HB.instance Definition _ := [SubZmodule_isSubRing of {fimfun aT >-> rT} by <:]. Implicit Types f g : {fimfun aT >-> rT}. @@ -575,7 +577,7 @@ have g_cts n : continuous (g_ n). have g_bd n : forall x, `|g_ n x| <= geometric ((1/3) * M%:num) (2/3) n. have [ctsN bdfN] := f_geo n; rewrite /geometric /= -[_ * M%:num * _]mulrA. by have [_ _] := projT2 (tietze_step (f_ n) _) ctsN (MN0 n) bdfN. -pose h_ : nat -> arrow_uniform_type X R^o := @series {uniform X -> _} g_. +pose h_ : nat -> arrow_uniform_type X R^o := @series {uniform X -> R^o} g_. have cvgh' : cvg (h_ @ \oo). apply/cauchy_cvgP/cauchy_ballP => eps epos; near_simpl. suff : \forall x & x' \near \oo, (x' <= x)%N -> ball (h_ x) eps (h_ x'). diff --git a/theories/probability.v b/theories/probability.v index c57cac324d..9b84276a35 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -196,7 +196,7 @@ Lemma expectation_sum (X : seq {RV P >-> R}) : (forall Xi, Xi \in X -> P.-integrable [set: T] (EFin \o Xi)) -> 'E_P[\sum_(Xi <- X) Xi] = \sum_(Xi <- X) 'E_P[Xi]. Proof. -elim: X => [|X0 X IHX] intX; first by rewrite !big_nil expectation_cst. +elim: X => [|X0 X IHX] intX; first by rewrite !big_nil (expectation_cst 0). have intX0 : P.-integrable [set: T] (EFin \o X0). by apply: intX; rewrite in_cons eqxx. have {}intX Xi : Xi \in X -> P.-integrable [set: T] (EFin \o Xi). @@ -331,7 +331,7 @@ Lemma covarianceDl (X Y Z : {RV P >-> R}) : Proof. move=> X1 X2 Y1 Y2 Z1 Z2 XZ1 YZ1. rewrite [LHS]covarianceE//= ?mulrDl ?compreDr// ?integrableD//. -rewrite 2?expectationD//=. +rewrite add_funE 2?expectationD//=. rewrite muleDl ?fin_num_adde_defr ?expectation_fin_num//. rewrite oppeD ?fin_num_adde_defr ?fin_numM ?expectation_fin_num//. by rewrite addeACA 2?covarianceE. @@ -397,7 +397,7 @@ Proof. by move=> /[dup]; apply: covariance_fin_num. Qed. Lemma variance_ge0 (X : {RV P >-> R}) : (0 <= 'V_P[X])%E. Proof. -by rewrite /variance unlock; apply: expectation_ge0 => x; apply: sqr_ge0. +by rewrite /variance unlock mul_funE; apply: expectation_ge0 => x; apply: sqr_ge0. Qed. Lemma variance_cst r : 'V_P[cst r] = 0%E. @@ -459,7 +459,7 @@ rewrite varianceD/= ?varianceN ?covarianceNr ?muleN//. - by rewrite mulrN compreN ?integrableN. Qed. -Lemma varianceD_cst_l c (X : {RV P >-> R}) : +Lemma varianceD_cst_l (c : R) (X : {RV P >-> R}) : P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> 'V_P[(cst c \+ X)%R] = 'V_P[X]. Proof. @@ -480,7 +480,7 @@ have -> : (X \+ cst c = cst c \+ X)%R by apply/funeqP => x /=; rewrite addrC. exact: varianceD_cst_l. Qed. -Lemma varianceB_cst_l c (X : {RV P >-> R}) : +Lemma varianceB_cst_l (c : R) (X : {RV P >-> R}) : P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> 'V_P[(cst c \- X)%R] = 'V_P[X]. Proof.