From c515b27495628b167b7289e5990fc5c667a1f4e7 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 3 Mar 2026 00:26:16 +0100 Subject: [PATCH] Fixed the infamous `%E` scope bug --- CHANGELOG_UNRELEASED.md | 3 + experimental_reals/discrete.v | 2 +- reals/constructive_ereal.v | 88 ++++++++++++++++--- theories/ess_sup_inf.v | 4 +- theories/ftc.v | 40 ++++----- theories/gauss_integral.v | 2 +- theories/hoelder.v | 4 +- theories/probability_theory/random_variable.v | 6 +- theories/realfun.v | 2 +- theories/sequences.v | 4 +- 10 files changed, 109 insertions(+), 46 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 549045ba2a..09a764e6c3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -71,6 +71,9 @@ + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV` ### Changed + +- in `constructive_ereal.v`: fixed the infamous `%E` scope bug. + - in set_interval.v + `setUitv1`, `setU1itv`, `setDitv1l`, `setDitv1r` (generalized) diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v index 79bc14c24e..0d82cefca3 100644 --- a/experimental_reals/discrete.v +++ b/experimental_reals/discrete.v @@ -4,7 +4,7 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) -From Corelib Require Setoid. +From Coq Require Setoid. From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp.classical Require Import boolp. diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v index 996ef3cd23..3bcc26a7c7 100644 --- a/reals/constructive_ereal.v +++ b/reals/constructive_ereal.v @@ -570,14 +570,63 @@ End ERealArith. Arguments mule : simpl never. Arguments inve : simpl never. -Notation "+%dE" := (@GRing.add (\bar^d _)). -Notation "+%E" := (@GRing.add (\bar _)). -Notation "-%E" := oppe. -Notation "x + y" := (GRing.add (x%dE : \bar^d _) y%dE) : ereal_dual_scope. -Notation "x + y" := (GRing.add x%E y%E) : ereal_scope. -Notation "x - y" := ((x%dE : \bar^d _) + oppe y%dE) : ereal_dual_scope. -Notation "x - y" := (x%E + (oppe y%E)) : ereal_scope. -Notation "- x" := (oppe x%dE : \bar^d _) : ereal_dual_scope. + +(* We use elpi to name the canonical nmodule for \bar R and \bar^d R. *) +(* This used to be called `extended_nmodType` and `dual_extended_nmodType`. *) +(* HB gives them generated names now, though we should restore naming cf *) +(* https://github.com/math-comp/hierarchy-builder/issues/328 *) +Elpi Command canonical_notation_ereal. +Elpi Accumulate lp:{{ + main [] :- + coq.unify-leq {{\bar lp:_}} {{GRing.Nmodule.sort lp:M}} ok, + coq.safe-dest-app M CR _, + coq.notation.add-abbreviation "extended_nmodType" 0 CR tt _. + }}. +Elpi canonical_notation_ereal. +Elpi Command canonical_notation_dual_ereal. +Elpi Accumulate lp:{{ + main [] :- + coq.unify-leq {{dual_extended lp:_}} {{GRing.Nmodule.sort lp:M}} ok, + coq.safe-dest-app M CR _, + coq.notation.add-abbreviation "dual_extended_nmodType" 0 CR tt _. + }}. +Elpi canonical_notation_dual_ereal. + +(* We provide local notations for parsing and printing of particular *) +(* instances of generic notations. *) +Local Notation add_parsingde := (@GRing.add (\bar^d _)). +Local Notation add_rcde := (@GRing.add (@reverse_coercion _ _ _ (\bar^d _))). +Local Notation add_cande := (@GRing.add dual_extended_nmodType). +Local Notation add_parsinge := (@GRing.add (\bar _)). +Local Notation add_rce := (@GRing.add (@reverse_coercion _ _ _ (\bar _))). +Local Notation add_cane := (@GRing.add extended_nmodType). + +Notation "+%dE" := add_parsingde (only parsing). +Notation "+%dE" := add_rcde (only printing). +Notation "+%dE" := add_cande (only printing). +Notation "+%E" := add_parsinge (only parsing). +Notation "+%E" := add_rce (only printing). +Notation "+%E" := add_cane (only printing). +Notation "-%E" := oppe. +Notation "x + y" := (add_parsingde x%dE y%dE) (only parsing) : ereal_dual_scope. +Notation "x + y" := (add_rcde x%dE y%dE) (only printing) : ereal_dual_scope. +Notation "x + y" := (add_cande x%dE y%dE) (only printing) : ereal_dual_scope. +Notation "x + y" := (add_parsinge x%E y%E) (only parsing) : ereal_scope. +Notation "x + y" := (add_rce x%E y%E) (only printing) : ereal_scope. +Notation "x + y" := (add_cane x%E y%E) (only printing) : ereal_scope. +Notation "x - y" := (add_parsingde x%dE (oppe (y%dE : \bar^d _))%dE) + (only parsing) : ereal_dual_scope. +Notation "x - y" := (add_rcde x%dE (oppe y%dE)) + (only printing) : ereal_dual_scope. +Notation "x - y" := (add_cande x%dE (oppe y%dE)) + (only printing) : ereal_dual_scope. +Notation "x - y" := (add_parsinge x%E (oppe y%E)) (only parsing) : ereal_scope. +Notation "x - y" := (add_rce x%E (oppe y%E)) (only printing) : ereal_scope. +Notation "x - y" := (add_cane x%E (oppe y%E)) (only printing) : ereal_scope. +(* All previous notations should ideal by generated too, *) +(* but elpi lacks support for string notations. *) + +Notation "- x" := (oppe (x%dE : \bar^d _)) : ereal_dual_scope. Notation "- x" := (oppe x%E) : ereal_scope. Notation "*%E" := mule. Notation "x * y" := (mule x%dE y%dE : \bar^d _) : ereal_dual_scope. @@ -643,12 +692,23 @@ Notation "- 1" := (oppe 1) : ereal_scope. Notation "\- f" := (fun x => - f x)%dE : ereal_dual_scope. Notation "\- f" := (fun x => - f x)%E : ereal_scope. -Notation "f \+ g" := (fun x => f x + g x)%dE : ereal_dual_scope. -Notation "f \+ g" := (fun x => f x + g x)%E : ereal_scope. -Notation "f \* g" := (fun x => f x * g x)%dE : ereal_dual_scope. -Notation "f \* g" := (fun x => f x * g x)%E : ereal_scope. -Notation "f \- g" := (fun x => f x - g x)%dE : ereal_dual_scope. -Notation "f \- g" := (fun x => f x - g x)%E : ereal_scope. +Notation "f \+ g" := (fun x => add_parsingde (f x)%dE (g x)%dE) (only parsing) : ereal_dual_scope. +Notation "f \+ g" := (fun x => add_rcde (f x)%dE (g x)%dE) (only printing) : ereal_dual_scope. +Notation "f \+ g" := (fun x => add_cande (f x)%dE (g x)%dE) (only printing) : ereal_dual_scope. +Notation "f \+ g" := (fun x => add_parsinge (f x)%E (g x)%E) (only parsing) : ereal_scope. +Notation "f \+ g" := (fun x => add_rce (f x)%E (g x)%E) (only printing) : ereal_scope. +Notation "f \+ g" := (fun x => add_cane (f x)%E (g x)%E) (only printing) : ereal_scope. +Notation "f \- g" := (fun x => add_parsingde ((f x)%dE : \bar^d _) (oppe ((g%dE x) : \bar^d _))%dE) + (only parsing) : ereal_dual_scope. +Notation "f \- g" := (fun x => add_rcde (f x)%dE (oppe (g x)%dE)) + (only printing) : ereal_dual_scope. +Notation "f \- g" := (fun x => add_cande (f x)%dE (oppe (g x)%dE)) + (only printing) : ereal_dual_scope. +Notation "f \- g" := (fun x => add_parsinge ((f x)%E : \bar _) (oppe (g x)%E)) (only parsing) : ereal_scope. +Notation "f \- g" := (fun x => add_rce (f x)%E (oppe (g x)%E)) (only printing) : ereal_scope. +Notation "f \- g" := (fun x => add_cane (f x)%E (oppe (g x)%E)) (only printing) : ereal_scope. +Notation "f \* g" := (fun x => (f x * g x)%dE) : ereal_dual_scope. +Notation "f \* g" := (fun x => (f x * g x)%E) : ereal_scope. Notation "\sum_ ( i <- r | P ) F" := (\big[+%dE/0%dE]_(i <- r | P%B) F%dE) : ereal_dual_scope. diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v index 6848111cf1..633b3dd220 100644 --- a/theories/ess_sup_inf.v +++ b/theories/ess_sup_inf.v @@ -217,11 +217,11 @@ Proof. by move=> ?; apply/ess_supP; apply: nearW. Qed. Lemma ess_sup_cstr y : 0 < mu [set: T] -> ess_supr (cst y) = y%:E. Proof. by move=> muN0; rewrite (ess_sup_ae_cst y%:E)//=; apply: nearW. Qed. -Lemma ess_suprD f g : ess_supr (f \+ g) <= ess_supr f + ess_supr g. +Lemma ess_suprD f g : ess_supr (f \+ g)%R <= ess_supr f + ess_supr g. Proof. by rewrite (le_trans _ (ess_supD _ _ _)). Qed. Lemma ess_sup_normD f g : - ess_supr (normr \o (f \+ g)) <= ess_supr (normr \o f) + ess_supr (normr \o g). + ess_supr (normr \o (f \+ g)%R) <= ess_supr (normr \o f) + ess_supr (normr \o g). Proof. rewrite (le_trans _ (ess_suprD _ _))// le_ess_sup//. by apply/nearW => x; apply/ler_normD. diff --git a/theories/ftc.v b/theories/ftc.v index 976a3e9b79..495c86b866 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -88,7 +88,7 @@ Qed. Let FTC0 f a : mu.-integrable setT (EFin \o f) -> let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in forall x, a < BRight x -> lebesgue_pt f x -> - h^-1 *: (F (h + x) - F x) @[h --> 0%R^'] --> f x. + h^-1 *: (F (h + x)%R - F x) @[h --> 0%R^'] --> f x. Proof. move=> intf F x ax fx. have locf : locally_integrable setT f. @@ -106,7 +106,7 @@ apply: cvg_at_right_left_dnbhs. by rewrite (lt_le_trans _ yz)// ltrBlDr ltrDl. rewrite (lebesgue_measure_ball _ (ltW _))// -/mu muE -EFinM lee_fin. by rewrite mulr_natl. - have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E - + have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n)%R)]) (f t)%:E - \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E = \int[mu]_(y in E x n) (f y)%:E. rewrite -[in X in X - _]integral_itv_bndo_bndc; last first. @@ -161,7 +161,7 @@ apply: cvg_at_right_left_dnbhs. rewrite lebesgue_measure_ball//; last exact: ltW. by rewrite -/mu muE -EFinM lee_fin mulr_natl. have ixdf : {near \oo, - (fun n => \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E - + (fun n => \int[mu]_(t in [set` Interval a (BRight (x + d n)%R)]) (f t)%:E - \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E) =1 (fun n => - (\int[mu]_(y in E x n) (f y)%:E))}. case: a ax {F}; last first. @@ -236,7 +236,7 @@ Let FTC0_restrict f a x (u : R) : (x < u)%R -> mu.-integrable [set` Interval a (BRight u)] (EFin \o f) -> let F y := (\int[mu]_(t in [set` Interval a (BRight y)]) f t)%R in a < BRight x -> lebesgue_pt f x -> - h^-1 *: (F (h + x) - F x) @[h --> 0%R^'] --> f x. + h^-1 *: (F (h + x)%R - F x) @[h --> 0%R^'] --> f x. Proof. move=> xu + F ax fx. rewrite integrable_mkcond//= (restrict_EFin f) => intf. @@ -270,7 +270,7 @@ have /= := FTC0_restrict xu intf ax fx. set g := (f in f n @[n --> _] --> _ -> _). set h := (f in _ -> f n @[n --> _] --> _). suff : g = h by move=> <-. -by apply/funext => y;rewrite /g /h /= [X in F (X + _)]mulr1. +by apply/funext => y;rewrite /g /h /= [X in F (X + _)%R]mulr1. Qed. Corollary FTC1 f a : @@ -606,7 +606,7 @@ have GacFa : G x @[x --> a^'+] --> (- c + F a)%R. rewrite opprB GFc; last by rewrite in_itv/=; apply/andP. by rewrite addNr normr0 ltW. have := @cvgD _ _ _ _ Fap _ _ _ _ GFac Fa. - rewrite (_ : (G \- F)%R + F = G)//. + rewrite (_ : (G \- F) + F = G)%R//. by apply/funext => x/=; rewrite subrK. have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R. have Fbn : Filter b^'- by exact: at_left_proper_filter. @@ -615,7 +615,7 @@ have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R. rewrite opprB GFc; last by rewrite in_itv/=; apply/andP. by rewrite addNr normr0 ltW. have := @cvgD _ _ _ _ Fbn _ _ _ _ GFbc Fb. - rewrite (_ : (G \- F)%R + F = G)//. + rewrite (_ : G \- F + F = G)%R //. by apply/funext => x/=; rewrite subrK. have contF : {within `[a, b], continuous F}. apply/(continuous_within_itvP _ ab); split => //. @@ -661,18 +661,18 @@ rewrite ge0_integral_bigcup//=; last 3 first. - by rewrite -seqDU_bigcup_eq -itv_bndy_bigcup_BRight; exact: measurableT_comp. - move=> x/=; rewrite -seqDU_bigcup_eq -itv_bndy_bigcup_BRight/=. by rewrite /= in_itv/= => /andP[/ltW + _]; rewrite lee_fin; exact: f_ge0. -have dFEn n : {in `]a + n%:R, a + n.+1%:R[, F^`() =1 f}. +have dFEn n : {in `](a + n%:R)%R, (a + n.+1%:R)%R[, F^`() =1 f}. apply: in1_subset_itv dFE. apply: subset_trans (subset_itvl _) (subset_itvr _) => //=. by rewrite bnd_simp lerDl. -have liml : limn (EFin \o (fun k => F (a + k%:R))) = l%:E. +have liml : limn (EFin \o (fun k => F (a + k%:R)%R)) = l%:E. apply/cvg_lim => //. apply: cvg_EFin; first exact: nearW. apply/((cvg_pinftyP F l).1 Fxl)/cvgryPge => r. by near do rewrite -lerBlDl; exact: nbhs_infty_ger. transitivity (\sum_(0 <= i `]a, (a + k%:R)]%classic) i.+1) (f x)%:E). + \int[mu]_(x in seqDU (fun k => `]a, (a + k%:R)%R]%classic) i.+1) (f x)%:E). apply/cvg_lim => //; rewrite -cvg_shiftS/=. under eq_cvg. move=> k /=; rewrite big_nat_recl//. @@ -700,13 +700,13 @@ transitivity (\sum_(0 <= i x; rewrite in_itv/= => /andP[anx _]. by apply/dF; rewrite (le_lt_trans _ anx)// lerDl. + move: n => [|n]; first by rewrite addr0. - have : {within `[a + n.+1%:R, a + n.+2%:R], continuous F}. + have : {within `[(a + n.+1%:R)%R, (a + n.+2%:R)%R], continuous F}. apply: derivable_within_continuous => /= x. rewrite in_itv/= => /andP[aSn _]. by apply: dF; rewrite (lt_le_trans _ aSn)// ltrDl. move/continuous_within_itvP. by rewrite ltrD2l ltr_nat ltnS => /(_ (ltnSn _))[]. - - have : {within `[a + n%:R + 2^-1%R, a + n.+1%:R], continuous F}. + - have : {within `[(a + n%:R + 2^-1%R)%R, (a + n.+1%:R)%R], continuous F}. apply: derivable_within_continuous => x. rewrite in_itv/= => /andP[aSn _]. by apply: dF; rewrite (lt_le_trans _ aSn)// -addrA ltrDl ltr_wpDl. @@ -717,7 +717,7 @@ rewrite nondecreasing_telescope_sumey. - by rewrite addr0 EFinN; congr (_ - _). - by rewrite liml. - apply/nondecreasing_seqP => n; rewrite -subr_ge0. - have isdF (x : R) : x \in `]a + n%:R, a + n.+1%:R[ -> is_derive x 1%R F (f x). + have isdF (x : R) : x \in `](a + n%:R)%R, (a + n.+1%:R)%R[ -> is_derive x 1%R F (f x). rewrite in_itv/= => /andP[anx _]. rewrite -dFE; last by rewrite in_itv/= andbT (le_lt_trans _ anx)// lerDl. rewrite derive1E. @@ -1283,12 +1283,12 @@ Lemma decreasing_ge0_integration_by_substitutiony F G a : Proof. move=> decrF cdF /cvg_ex[/= dFa cdFa] /cvg_ex[/= dFoo cdFoo]. move=> [dF cFa] Fny /continuous_within_itvNycP[cG cGFa] G0. -have mG n : measurable_fun `](F (a + n.+1%:R)), (F a)] G. +have mG n : measurable_fun `](F (a + n.+1%:R)%R), (F a)] G. apply/measurable_fun_itv_bndo_bndcP. apply: open_continuous_measurable_fun; first exact: interval_open. move=> x; rewrite inE/= in_itv/= => /andP[_ xFa]. by apply: cG; rewrite in_itv. -have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R. +have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)%R[ ((G \o F) * - F^`())%R. apply/measurable_fun_itv_obnd_cbndP. apply: open_continuous_measurable_fun; first exact: interval_open. move=> x; rewrite inE/= in_itv/= => /andP[ax _]. @@ -1330,7 +1330,7 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)). apply: G0. move: xFaSkFa. rewrite big_mkord -bigsetU_seqDU. - rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R), F a[%classic)). + rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R)%R, F a[%classic)). by move: x; apply: bigcup_sub => k/= nk; exact: subset_itvr. rewrite -integral_itv_obnd_cbnd; last first. apply/measurable_EFinP; case: n => [|n]. @@ -1338,7 +1338,7 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)). by apply: measurable_funS (mG n) => //; exact: subset_itvW. congr (integral _). rewrite big_mkord -bigsetU_seqDU. - rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R), F a[%classic)). + rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R)%R, F a[%classic)). exact/esym/decreasing_itvoo_bigcup. transitivity (limn (fun n => \int[mu]_(x in `]a, (a + n%:R)%R[) (((G \o F) * - F^`()) x)%:E)); last first. @@ -1375,15 +1375,15 @@ transitivity (limn (fun n => - exact: iota_uniq. - exact: (@sub_trivIset _ _ _ [set: nat]). - apply/measurable_EFinP. - apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)[)). + apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)%R[)). rewrite big_mkord -bigsetU_seqDU. - rewrite -(bigcup_mkord _ (fun k => `]a, (a + k.+1%:R)[%classic)). + rewrite -(bigcup_mkord _ (fun k => `]a, (a + k.+1%:R)%R[%classic)). apply: bigcup_sub => k/= kn. by apply: subset_itvl; rewrite bnd_simp/= lerD2l ler_nat ltnS ltnW. by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co. congr (integral _). rewrite big_mkord -bigsetU_seqDU. - rewrite -(bigcup_mkord n (fun k => `]a, (a + k.+1%:R)[%classic)). + rewrite -(bigcup_mkord n (fun k => `]a, (a + k.+1%:R)%R[%classic)). rewrite eqEsubset; split. move: n => [|n]; first by rewrite addr0 set_itvoo0. by apply: (@bigcup_sup _ _ n) => /=. diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v index 3170422435..e225a7f298 100644 --- a/theories/gauss_integral.v +++ b/theories/gauss_integral.v @@ -170,7 +170,7 @@ by rewrite expr0n/= oppr0 expR0 gauss_fun_le1. Unshelve. all: end_near. Qed. Let cvg_dintegral01_u x : - h^-1 *: (integral01_u (h + x)%E - integral01_u x) @[h --> 0^'] --> + h^-1 *: (integral01_u (h + x) - integral01_u x) @[h --> 0^'] --> - 2 * x * gauss_fun x * \int[mu]_(t in `[0, 1]) gauss_fun (t * x). Proof. have [c [e e0 cex]] : exists c : R, exists2 e : R, 0 < e & ball c e x. diff --git a/theories/hoelder.v b/theories/hoelder.v index 9f72d5a457..6baba0ff93 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -742,7 +742,7 @@ Qed. Lemma lerB_DLnorm f g p : measurable_fun [set: T] f -> measurable_fun [set: T] g -> (1 <= p)%R -> - 'N_p%:E[f] <= 'N_p%:E[f \+ g] + 'N_p%:E[g]. + 'N_p%:E[f] <= 'N_p%:E[(f \+ g)%R] + 'N_p%:E[g]. Proof. move=> mf mg p1. rewrite [in leLHS](_ : f = ((f + g) + (-%R \o g))%R); last by rewrite addrK. @@ -756,7 +756,7 @@ Qed. Lemma lerB_LnormD f g p : measurable_fun [set: T] f -> measurable_fun [set: T] g -> (1 <= p)%R -> - 'N_p%:E[f] - 'N_p%:E[g] <= 'N_p%:E[f \+ g]. + 'N_p%:E[f] - 'N_p%:E[g] <= 'N_p%:E[(f \+ g)%R]. Proof. move=> mf mg p1. set rhs := (leRHS); have [?|] := boolP (rhs \is a fin_num). diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 07ad1f329a..479f47b7f6 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -303,7 +303,7 @@ Qed. Lemma cdf_right_continuous : right_continuous (cdf X). Proof. move=> a. -pose s := fine (ereal_inf (cdf X @` `]a, a + 1%R]%classic)). +pose s := fine (ereal_inf (cdf X @` `]a, (a + 1)%R]%classic)). have cdf_s : cdf X r @[r --> a^'+] --> s%:E. rewrite /s fineK. - apply: nondecreasing_at_right_cvge; first by rewrite ltBSide /= ?ltrDl. @@ -312,13 +312,13 @@ have cdf_s : cdf X r @[r --> a^'+] --> s%:E. + by rewrite (lt_le_trans (ltNyr 0%R)) ?le_ereal_inf_tmp//= => l[? _] <-. + rewrite (le_lt_trans _ (ltry 1%R))// ge_ereal_inf//=. exists (cdf X (a + 1)); last exact: cdf_le1. - by exists (a + 1%R) => //; rewrite in_itv /=; apply/andP; rewrite ltrDl. + by exists (a + 1)%R => //; rewrite in_itv /=; apply/andP; rewrite ltrDl. have cdf_ns : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> s%:E. move/cvge_at_rightP : cdf_s; apply; split=> [n|]; rewrite ?ltrDl //. rewrite -[X in _ --> X]addr0; apply: (@cvgD _ R^o); first exact: cvg_cst. by rewrite gtr0_cvgV0 ?cvg_shiftS; [exact: cvgr_idn | near=> n]. have cdf_na : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> cdf X a. - pose F n := X @^-1` `]-oo, a + n.+1%:R^-1%R]. + pose F n := X @^-1` `]-oo, (a + n.+1%:R^-1)%R]. suff : P (F n) @[n --> \oo] --> P (\bigcap_n F n). by rewrite [in X in _ --> X -> _]/F -preimage_bigcap -itvNycEbigcap. apply: nonincreasing_cvg_mu => [| | |m n mn]. diff --git a/theories/realfun.v b/theories/realfun.v index 2268132a6c..05fd42c615 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -2042,7 +2042,7 @@ by move/hasNub_ereal_sup; apply; exact: variations_neq0. Qed. Lemma total_variation_le a b f g : a <= b -> - (TV a b (f \+ g) <= TV a b f + TV a b g)%E. + (TV a b (f \+ g)%R <= TV a b f + TV a b g)%E. Proof. rewrite le_eqVlt => /predU1P[<-{b}|ab]. by rewrite !total_variationxx adde0. diff --git a/theories/sequences.v b/theories/sequences.v index 8b54f628c0..ce27f54e76 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1478,14 +1478,14 @@ have <- : sup (range v_) = fine l. by exists (m + N)%N => //; rewrite /v_/= fineK// u_fin_num// leq_addl. apply: ge_ereal_sup => /= _ [m _] <-. rewrite (@le_trans _ _ (u_ (m + N)%N))//; first by rewrite nd_u_// leq_addr. - apply: ereal_sup_ubound => /=; exists (fine (u_ (m + N))); first by exists m. + apply: ereal_sup_ubound => /=; exists (fine (u_ (m + N)%N)); first by exists m. by rewrite fineK// u_fin_num// leq_addl. apply: nondecreasing_cvgn. - move=> m n mn /=; rewrite /v_ /= fine_le ?u_fin_num ?leq_addl//. by rewrite nd_u_// leq_add2r. - exists (fine l) => /= _ [m _ <-]; rewrite /v_ /= fine_le//. by rewrite u_fin_num// leq_addl. - by apply: ereal_sup_ubound; exists (m + N). + by apply: ereal_sup_ubound; exists (m + N)%N. Unshelve. all: by end_near. Qed. Lemma ereal_nondecreasing_is_cvgn (R : realType) (u_ : (\bar R) ^nat) :