From 319c75b95aa62a660d0768c1b091da36e5bf837a Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Tue, 16 Jul 2024 19:37:20 +0900 Subject: [PATCH] fixes #330 (floor and ceil subsumed by MathComp) (#1244) * fixes #330 --------- Co-authored-by: Kazuhiko Sakaguchi --- CHANGELOG_UNRELEASED.md | 35 ++++++ classical/mathcomp_extra.v | 80 ++++++++++++ theories/Rstruct.v | 5 +- theories/altreals/realsum.v | 33 +++-- theories/ereal.v | 23 ++-- theories/lebesgue_integral.v | 113 ++++++++--------- theories/lebesgue_measure.v | 21 ++-- theories/lebesgue_stieltjes_measure.v | 12 +- theories/measure.v | 6 +- theories/normedtype.v | 27 ++-- theories/real_interval.v | 25 ++-- theories/realfun.v | 14 +-- theories/reals.v | 170 +++++++------------------- theories/sequences.v | 9 +- theories/topology.v | 53 ++++---- 15 files changed, 332 insertions(+), 294 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b27e544cf..272348558 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -27,6 +27,15 @@ + lemma `FTC1` (specialization of the previous `FTC1` lemma, now renamed to `FTC1_lebesgue_pt`) + lemma `FTC1Ny` +- in `reals.v`: + + lemma `mem_rg1_floor` + +- in `mathcomp_extra.v`: + + lemma `ge_floor` + +- in `mathcomp_extra.v`: + + lemmas `intr1D`, `intrD1`, `floor_eq`, `floorN` + ### Changed - in `topology.v`: @@ -34,6 +43,21 @@ `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned into local `Let`'s +- in `reals.v`: + + definitions `Rceil`, `Rfloor` + +- moved from `reals.v` to `mathcomp_extra.v` + + lemma `lt_succ_floor`: conclusion changed to match `lt_succ_floor` in MathComp, + generalized to `archiDomainType` + + generalized to `archiDomainType`: + lemmas `floor_ge0`, `floor_lt0`, `floor_natz`, + `floor_ge_int`, `floor_neq0`, `floor_lt_int`, `ceil_ge`, `ceil_ge0`, `ceil_gt0`, + `ceil_le0`, `ceil_ge_int`, `ceilN`, `abs_ceil_ge` + + generalized to `archiDomainType` and precondition generalized: + * `floor_le0` + + generalized to `archiDomainType` and renamed: + * `ceil_lt_int` -> `ceil_gt_int` + ### Renamed - in `constructive_ereal.v`: @@ -62,8 +86,19 @@ ### Deprecated +- in `reals.v`: + + `floor_le` (use `ge_floor` instead) + + `le_floor` (use `Num.Theory.floor_le` instead) + + `le_ceil` (use `ceil_ge` instead) + ### Removed +- in `reals.v`: + + definition `floor` (use `Num.floor` instead) + + definition `ceil` (use `Num.ceil` instead) + + lemmas `floor0`, `floor1` + + lemma `le_floor` (use `Num.Theory.floor_le` instead) + ### Infrastructure ### Misc diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 0e82043f4..c4338dd58 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -374,3 +374,83 @@ by elim: p => //= p <-; Qed. End positive. + +Lemma intrD1 {R : ringType} (i : int) : i%:~R + 1 = (i + 1)%:~R :> R. +Proof. by rewrite intrD. Qed. + +Lemma intr1D {R : ringType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R. +Proof. by rewrite intrD. Qed. + +From mathcomp Require Import archimedean. + +Section floor_ceil. +Context {R : archiDomainType}. +Implicit Type x : R. + +Lemma ge_floor x : (Num.floor x)%:~R <= x. +Proof. exact: Num.Theory.ge_floor. Qed. + +Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x). +Proof. exact: Num.Theory.floor_ge_int. Qed. + +Lemma floor_lt_int x (z : int) : (x < z%:~R) = (Num.floor x < z). +Proof. by rewrite ltNge floor_ge_int -ltNge. Qed. + +Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x). +Proof. by rewrite -floor_ge_int. Qed. + +Lemma floor_le0 x : (x < 1) = (Num.floor x <= 0). +Proof. by rewrite -ltzD1 add0r -floor_lt_int. Qed. + +Lemma floor_lt0 x : (x < 0) = (Num.floor x < 0). +Proof. by rewrite -floor_lt_int. Qed. + +Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R. +Proof. exact: Num.Theory.lt_succ_floor. Qed. + +Lemma floor_eq x m : (Num.floor x == m) = (m%:~R <= x < (m + 1)%:~R). +Proof. +apply/eqP/idP; [move=> <-|by move=> /Num.Theory.floor_def ->]. +by rewrite Num.Theory.ge_floor//= Num.Theory.lt_succ_floor. +Qed. + +Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1). +Proof. by rewrite neq_lt -floor_lt_int gtz0_ge1 -floor_ge_int. Qed. + +#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.le_ceil` instead")] +Lemma ceil_ge x : x <= (Num.ceil x)%:~R. +Proof. exact: Num.Theory.le_ceil. Qed. + +#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.ceil_le_int`")] +Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z). +Proof. exact: Num.Theory.ceil_le_int. Qed. + +Lemma ceil_gt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x). +Proof. by rewrite ltNge Num.Theory.ceil_le_int// -ltNge. Qed. + +Lemma ceilN x : Num.ceil (- x) = - Num.floor x. +Proof. by rewrite /Num.ceil opprK. Qed. + +Lemma floorN x : Num.floor (- x) = - Num.ceil x. +Proof. by rewrite /Num.ceil opprK. Qed. + +Lemma ceil_ge0 x : (- 1 < x) = (0 <= Num.ceil x). +Proof. by rewrite ltrNl floor_le0 floorN lerNl oppr0. Qed. + +Lemma ceil_gt0 x : (0 < x) = (0 < Num.ceil x). +Proof. by rewrite -ceil_gt_int. Qed. + +Lemma ceil_le0 x : (x <= 0) = (Num.ceil x <= 0). +Proof. by rewrite -Num.Theory.ceil_le_int. Qed. + +Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R. +Proof. +rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x. + by rewrite !gtr0_norm// -?ceil_gt0// (le_trans (Num.Theory.le_ceil _))// lerDl. +by rewrite !ler0_norm -?ceil_le0// opprK intrD1 ltW// lt_succ_floor. +Qed. + +End floor_ceil. + +#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to `ceil_gt_int`")] +Notation ceil_lt_int := ceil_gt_int (only parsing). diff --git a/theories/Rstruct.v b/theories/Rstruct.v index 50a515281..903d00db6 100644 --- a/theories/Rstruct.v +++ b/theories/Rstruct.v @@ -29,6 +29,7 @@ Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf. Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. Require Import Rtrigo1 Reals. From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum. +From mathcomp Require Import archimedean. From HB Require Import structures. From mathcomp Require Import mathcomp_extra. @@ -87,7 +88,7 @@ Proof. by move=> *; rewrite Rplus_assoc. Qed. HB.instance Definition _ := GRing.isZmodule.Build R RplusA Rplus_comm Rplus_0_l Rplus_opp_l. -Fact RmultA : associative (Rmult). +Fact RmultA : associative Rmult. Proof. by move=> *; rewrite Rmult_assoc. Qed. Fact R1_neq_0 : R1 != R0. @@ -292,7 +293,7 @@ rewrite /Rminus Rplus_assoc [- _ + _]Rplus_comm -Rplus_assoc -!/(Rminus _ _). exact: Rle_minus. Qed. -HB.instance Definition _ := Num.RealField_isArchimedean.Build R +HB.instance Definition _ := Num.NumDomain_bounded_isArchimedean.Build R Rarchimedean_axiom. (** Here are the lemmas that we will use to prove that R has diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v index c5eac8ae6..900f467ce 100644 --- a/theories/altreals/realsum.v +++ b/theories/altreals/realsum.v @@ -2,12 +2,11 @@ (* Copyright (c) - 2015--2016 - IMDEA Software Institute *) (* Copyright (c) - 2015--2018 - Inria *) (* Copyright (c) - 2016--2018 - Polytechnique *) - (* -------------------------------------------------------------------- *) -From mathcomp Require Import all_ssreflect all_algebra. +From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp.classical Require Import boolp. Require Import xfinmap ereal reals discrete realseq. -From mathcomp.classical Require Import classical_sets functions mathcomp_extra. +From mathcomp.classical Require Import classical_sets functions. Require Import topology. Set Implicit Arguments. @@ -16,6 +15,7 @@ Unset Printing Implicit Defensive. Unset SsrOldRewriteGoalsOrder. Import Order.TTheory GRing.Theory Num.Theory. +From mathcomp.classical Require Import mathcomp_extra. Local Open Scope fset_scope. Local Open Scope ring_scope. @@ -141,28 +141,24 @@ Lemma summable_countn0 : summable f -> countable [pred x | f x != 0]. Proof. case/summableP=> M ge0_M bM; pose E (p : nat) := [pred x | `|f x| > 1 / p.+1%:~R]. set F := [pred x | _]; have le: {subset F <= [pred x | `[< exists p, x \in E p >]]}. - move=> x; rewrite !inE => nz_fx. - pose j := `|floor (1 / `|f x|)|%N; exists j; rewrite inE. - rewrite ltr_pdivrMr ?ltr0z // -ltr_pdivrMl ?normr_gt0 //. - rewrite mulr1 /j div1r -addn1 /= PoszD intrD mulr1z. - rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0 //. - by rewrite -RfloorE; apply lt_succ_Rfloor. + move=> x; rewrite !inE => nz_fx; exists (Num.trunc `|f x|^-1). + rewrite inE mul1r invf_plt ?unfold_in /= ?normr_gt0 //. + by have/trunc_itv/andP[]: 0 <= `|f x|^-1 by rewrite invr_ge0 normr_ge0. apply/(countable_sub le)/cunion_countable=> i /=. case: (existsTP (fun s : seq T => {subset E i <= s}))=> /= [[s le_Eis]|]. by apply/finite_countable/finiteP; exists s => x /le_Eis. -move/finiteNP; pose j := `|floor (M / i.+1%:R)|.+1. -pose K := (`|floor M|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP. -move=> h; have /asboolP[] := xchooseP h. +move=> /finiteNP/(_ ((Num.trunc M).+1 * i.+1)%N)/asboolP/exists_asboolP h. +have/asboolP[] := xchooseP h. set s := xchoose h=> eq_si uq_s le_sEi; pose J := [fset x in s]. suff: \sum_(x : J) `|f (val x)| > M by rewrite ltNge bM. apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first. apply/ler_sum=> /= m _; apply/ltW. by have:= fsvalP m; rewrite in_fset => /le_sEi. -rewrite sumr_const -cardfE card_fseq undup_id // eq_si -mulr_natr -pmulrn. -rewrite mul1r natrM mulrCA mulVf ?mulr1 ?pnatr_eq0 //. -have /andP[_] := mem_rg1_Rfloor M; rewrite RfloorE -addn1. -by rewrite natrD /= mulr1n pmulrn -{1}[floor _]gez0_abs // floor_ge0. +rewrite mul1r sumr_const -cardfE card_fseq undup_id // eq_si. +rewrite -mulr_natr natrM mulrC mulfK ?pnatr_eq0//. +by case/trunc_itv/andP: ge0_M. Qed. + End SummableCountable. (* -------------------------------------------------------------------- *) @@ -1201,9 +1197,8 @@ Qed. Lemma sum_seq1 S x : (forall y, S y != 0 -> x == y) -> sum S = S x. Proof. -move=> domS; rewrite (sum_finseq (r := [:: x])) //. - by move=> y; rewrite !inE => /domS /eqP->. -by rewrite big_seq1. +move=> domS; rewrite (sum_finseq (r := [:: x])) ?big_seq1//. +by move=> y; rewrite !inE => /domS /eqP->. Qed. End SumTheory. diff --git a/theories/ereal.v b/theories/ereal.v index 4d2fcce6f..414423e22 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -5,8 +5,8 @@ (* Copyright (c) - 2016--2018 - Polytechnique *) (* -------------------------------------------------------------------- *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra finmap archimedean. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import fsbigop cardinality set_interval. Require Import reals signed topology. Require Export constructive_ereal. @@ -55,6 +55,7 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. Import numFieldTopology.Exports. +From mathcomp Require Import mathcomp_extra. Local Open Scope ring_scope. @@ -1266,7 +1267,7 @@ rewrite predeq2E => x A; split. case=> [r' /= re'r'| |]/=. * rewrite /ereal_ball in re'r'. have [r'r|rr'] := lerP (contract r'%:E) (contract r%:E). - apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //. + apply: reA; rewrite /ball /= ltr_norml//. rewrite ger0_norm ?subr_ge0// in re'r'. have : (contract (r%:E - e%:num%:E) < contract r'%:E)%R. move: re'r'; rewrite /e' lt_min => /andP[+ _]. @@ -1276,7 +1277,7 @@ rewrite predeq2E => x A; split. rewrite ltrBlDr addrC -ltrBlDr => ->; rewrite andbT. rewrite (@lt_le_trans _ _ 0%R)// 1?ltrNl 1?oppr0// subr_ge0. by rewrite -lee_fin -le_contract. - apply: reA; rewrite /ball /= real_ltr_norml // ?num_real //. + apply: reA; rewrite /ball /= ltr_norml//. rewrite ltr0_norm ?subr_lt0// opprB in re'r'. apply/andP; split; last first. by rewrite (@lt_trans _ _ 0%R) // subr_lt0 -lte_fin -lt_contract. @@ -1402,21 +1403,23 @@ Lemma cvg_ereal_loc_seq (R : realType) (x : \bar R) : Proof. move=> P; rewrite /ereal_loc_seq. case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 first. - have /ZnatP[N Nfloor] : floor (Num.max d 0%R) \is a Znat. + have /natrP[N Nfloor] : Num.floor (Num.max d 0%R) \is a Num.nat. by rewrite Znat_def floor_ge0 le_max lexx orbC. exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin. have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_max lexx. - by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat. - have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat. + apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor. + by rewrite natr1 mulrz_nat ler_nat. + have /natrP[N Nfloor] : Num.floor (Num.max (- d)%R 0%R) \is a Num.nat. by rewrite Znat_def floor_ge0 le_max lexx orbC. exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltrNl. have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_max lexx. - by apply; rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor natr1 ler_nat. -have /ZnatP[N Nfloor] : floor (d%:num^-1) \is a Num.nat. + apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor. + by rewrite natr1 mulrz_nat ler_nat. +have /natrP[N Nfloor] : Num.floor d%:num^-1 \is a Num.nat. by rewrite Znat_def floor_ge0. exists N => // n leNn; apply: dP; last first. by rewrite eq_sym addrC -subr_eq subrr eq_sym; exact/invr_neq0/lt0r_neq0. rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0. rewrite -[ltLHS]mulr1 ltr_pdivrMl // -ltr_pdivrMr // div1r. -by rewrite (lt_le_trans (reals.lt_succ_floor _))// Nfloor lerD// ler_nat. +by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor !natr1 mulrz_nat ler_nat. Qed. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 16910f726..4daa6e2f6 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import archimedean. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop. Require Import signed reals ereal topology normedtype sequences real_interval. Require Import esum measure lebesgue_measure numfun realfun function_spaces. @@ -83,6 +83,7 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. Import numFieldTopology.Exports. +From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -1286,28 +1287,20 @@ Qed. Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic = \big[setU/set0]_(n * 2 ^ n.+1 <= k < n.+1 * 2 ^ n.+1) [set` I n.+1 k]. Proof. -rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]. -- rewrite -bigcup_seq /=; exists `|reals.floor (r * 2 ^+ n.+1)|%N. - rewrite /= mem_index_iota; apply/andP; split. - rewrite -ltez_nat gez0_abs ?reals.floor_ge0; last first. - by rewrite mulr_ge0// (le_trans _ nr). - apply: (@le_trans _ _ (reals.floor (n * 2 ^ n.+1)%:R)); last first. - by apply: le_floor; rewrite natrM natrX ler_pM2r. - by rewrite floor_natz intz. - rewrite -ltz_nat gez0_abs; last first. - by rewrite floor_ge0 mulr_ge0// (le_trans _ nr). - rewrite -(@ltr_int R) (le_lt_trans (reals.floor_le _))//. - by rewrite PoszM intrM -natrX ltr_pM2r. - rewrite /= in_itv /=; apply/andP; split. - rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//. - by rewrite -(@gez0_abs (reals.floor _))// floor_ge0 mulr_ge0// (le_trans _ nr). - rewrite ltr_pdivlMr// (lt_le_trans (reals.lt_succ_floor _))//. - rewrite -[in leRHS]natr1 lerD2r// -(@gez0_abs (reals.floor _))// floor_ge0. - by rewrite mulr_ge0// (le_trans _ nr). -- rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn]. - rewrite in_itv /= => /andP[knr rkn]; rewrite in_itv /=; apply/andP; split. +rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|]; last first. + rewrite -bigcup_seq => -[/= k] /[!mem_index_iota] /andP[nk kn]. + rewrite !in_itv /= => /andP[knr rkn]; apply/andP; split. by rewrite (le_trans _ knr)// ler_pdivlMr// -natrX -natrM ler_nat. by rewrite (lt_le_trans rkn)// ler_pdivrMr// -natrX -natrM ler_nat. +rewrite -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N. + rewrite /= mem_index_iota -ltz_nat -lez_nat gez0_abs; last first. + by rewrite floor_ge0 mulr_ge0// (le_trans _ nr). + rewrite -floor_ge_int -floor_lt_int. + by rewrite !PoszM -!natrXE !rmorphM !rmorphXn /= ler_wpM2r ?ltr_pM2r. +rewrite /= in_itv /= ler_pdivrMr// ltr_pdivlMr//. +rewrite pmulrn [(`|_|.+1%:R)]pmulrn intS addrC gez0_abs; last first. + by rewrite floor_ge0 mulr_ge0 ?exprn_ge0 // (le_trans _ nr). +by rewrite ge_floor lt_succ_floor. Qed. Lemma dyadic_itv_image n T (f : T -> \bar R) x : @@ -1430,18 +1423,19 @@ rewrite pnatr_eq0 => /eqP. have [//|] := boolP (x \in B n). rewrite notin_setE /B /setI /= => /not_andP[] // /negP. rewrite -ltNge => fxn _. -have K : (`|reals.floor (fine (f x) * 2 ^+ n)| < n * 2 ^ n)%N. - rewrite -ltz_nat gez0_abs; last by rewrite reals.floor_ge0 mulr_ge0// ltW. - rewrite -(@ltr_int R); rewrite (le_lt_trans (reals.floor_le _))// PoszM intrM. +have K : (`|floor (fine (f x) * 2 ^+ n)| < n * 2 ^ n)%N. + rewrite -ltz_nat gez0_abs; last by rewrite floor_ge0 mulr_ge0// ltW. + rewrite -(@ltr_int R); rewrite (le_lt_trans (ge_floor _))// PoszM intrM. by rewrite -natrX ltr_pM2r// -lte_fin (fineK fxfin). have /[!mem_index_enum]/(_ isT) := An0 (Ordinal K). rewrite implyTb indicE mem_set ?mulr1; last first. rewrite /A K /= inE; split=> //=; exists (fine (f x)); last by rewrite fineK. rewrite in_itv /=; apply/andP; split. - rewrite ler_pdivrMr// (le_trans _ (reals.floor_le _))//. - by rewrite -(@gez0_abs (reals.floor _))// reals.floor_ge0 mulr_ge0// ltW. - rewrite ltr_pdivlMr// (lt_le_trans (reals.lt_succ_floor _))// -[in leRHS]natr1. - by rewrite lerD2r// -{1}(@gez0_abs (reals.floor _))// reals.floor_ge0// mulr_ge0// ltW. + rewrite ler_pdivrMr// (le_trans _ (ge_floor _))//. + by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// ltW. + rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//. + rewrite -[in leRHS]natr1 -intrD1 lerD2r// -{1}(@gez0_abs (floor _))//. + by rewrite floor_ge0// mulr_ge0// ltW. rewrite mulf_eq0// -exprVn; apply/negP; rewrite negb_or expf_neq0//= andbT. rewrite pnatr_eq0 -lt0n absz_gt0 floor_neq0// -ler_pdivrMr//. apply/orP; right; apply/ltW; near: n. @@ -1538,11 +1532,11 @@ near=> n. have mn : (m <= n)%N by near: n; exists m. have : fine (f x) < n%:R. near: n. - exists `|reals.floor (fine (f x))|.+1%N => //= p /=. + exists `|floor (fine (f x))|.+1%N => //= p /=. rewrite -(@ler_nat R); apply: lt_le_trans. - rewrite -natr1 (_ : `| _ |%:R = (reals.floor (fine (f x)))%:~R); last first. - by rewrite -[in RHS](@gez0_abs (reals.floor _))// reals.floor_ge0//; exact/fine_ge0/f0. - by rewrite reals.lt_succ_floor. + rewrite -natr1 (_ : `| _ |%:R = (floor (fine (f x)))%:~R); last first. + by rewrite -[in RHS](@gez0_abs (floor _))// floor_ge0//; exact/fine_ge0/f0. + by rewrite intrD1 lt_succ_floor. rewrite -lte_fin (fineK fxfin) => fxn. have [approx_nx0|[k [/andP[k0 kn2n] ? ->]]] := f_ub_approx fxn. by have := Hm _ mn; rewrite approx_nx0. @@ -1578,21 +1572,19 @@ move=> Dx fxoo; have approx_x n : approx n x = n%:R. by rewrite fgen_A0 // ?mulr0 // fxoo leey. case/cvg_ex => /= l; have [l0|l0] := leP 0%R l. - move=> /cvgrPdist_lt/(_ _ ltr01) -[n _]. - move=> /(_ (`|reals.ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)). + move=> /(_ (`|ceil l|.+1 + n)%N) /= /(_ (leq_addl _ _)). rewrite approx_x. apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //. rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//. rewrite natrD lerD// ?ler1n// ger0_norm // (le_trans (ceil_ge _)) //. - by rewrite -(@gez0_abs (reals.ceil _)) // ceil_ge0. -- move/cvgrPdist_lt => /(_ _ ltr01) -[n _]. - move=> /(_ (`|reals.floor l|.+1 + n)%N) /= /(_ (leq_addl _ _)). - rewrite approx_x. - apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //. + by rewrite -(@gez0_abs (ceil _)) // -ceil_ge0 (lt_le_trans _ l0). +- move=> /cvgrPdist_lt/(_ _ ltr01)[n _]. + move=> /(_ (`|floor l|.+1 + n)%N)/(_ (leq_addl _ _)); apply/negP. + rewrite approx_x -leNgt distrC (le_trans _ (lerB_normD _ _))//. rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//. - rewrite natrD lerD// ?ler1n// ler0_norm //; last by rewrite ltW. - rewrite (@le_trans _ _ (- reals.floor l)%:~R) //. - by rewrite mulrNz lerNl opprK reals.floor_le. - by rewrite -(@lez0_abs (reals.floor _)) // reals.floor_le0 // ltW. + rewrite natrD lerD ?ler1n// ltr0_norm// (@le_trans _ _ (- floor l)%:~R)//. + by rewrite mulrNz lerNl opprK ge_floor. + by rewrite -(@lez0_abs (floor _))// -floor_le0// (lt_le_trans l0). Qed. Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x : @@ -2346,19 +2338,20 @@ transitivity (\int[mu]_(x in D) limn (g^~ x)). exists 1%N => // m /= m0. by rewrite mulry gtr0_sg// ?mul1e ?leey// ltr0n. near=> n; rewrite lee_fin -ler_pdivrMr//. - near: n; exists `|reals.ceil (M / r)|%N => // m /=. + near: n; exists `|ceil (M / r)|%N => // m /=. rewrite -(ler_nat R); apply: le_trans. - by rewrite natr_absz ger0_norm ?ceil_ge// ceil_ge0// divr_ge0// ?ltW. + rewrite natr_absz ger0_norm ?ceil_ge// -ceil_ge0// (lt_le_trans (ltrN10 _))//. + by rewrite divr_ge0// ?ltW. - rewrite lt0_mulye//; apply/cvgeNyPleNy; near=> M; have M0 : (M <= 0)%R by []. rewrite /g; case: (f x) fx0 => [r r0|//|_]; last first. exists 1%N => // m /= m0. by rewrite mulrNy gtr0_sg// ?ltr0n// mul1e ?leNye. near=> n; rewrite lee_fin -ler_ndivrMr//. - near: n; exists `|reals.ceil (M / r)|%N => // m /=. + near: n; exists `|ceil (M / r)|%N => // m /=. rewrite -(ler_nat R); apply: le_trans. - rewrite natr_absz ger0_norm ?ceil_ge// ceil_ge0// -mulrNN. - by rewrite mulr_ge0// lerNr oppr0// ltW// invr_lt0. + rewrite natr_absz ger0_norm ?ceil_ge// -ceil_ge0// (lt_le_trans (ltrN10 _))//. + by rewrite -mulrNN mulr_ge0// lerNr oppr0// ltW// invr_lt0. - rewrite -fx0 mule0 /g -fx0. under eq_fun do rewrite mule0/=. (*TODO: notation broken*) exact: cvg_cst. @@ -2377,9 +2370,10 @@ rewrite -(@fineK _ (\int[mu]_(x in D) f x)); last first. rewrite -lee_pdivrMr//; last first. by move: if_gt0 ifoo; case: (\int[mu]_(x in D) f x). near: n. -exists `|reals.ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //. +exists `|ceil (M * (fine (\int[mu]_(x in D) f x))^-1)|%N => //. move=> n /=; rewrite -(@ler_nat R) -lee_fin; apply: le_trans. -rewrite lee_fin natr_absz ger0_norm ?ceil_ge// ceil_ge0//. +rewrite lee_fin natr_absz ger0_norm ?ceil_ge// -ceil_ge0//. +rewrite (lt_le_trans (ltrN10 _))//. by rewrite mulr_ge0// ?invr_ge0//; exact/fine_ge0/integral_ge0. Unshelve. all: by end_near. Qed. @@ -2608,7 +2602,7 @@ Proof. move=> muD0; pose g : (T -> \bar R)^nat := fun n => cst n%:R%:E. have <- : (fun t => limn (g^~ t)) = cst +oo. rewrite funeqE => t; apply/cvg_lim => //=. - apply/cvgeryP/cvgryPge => M; exists `|reals.ceil M|%N => //= m. + apply/cvgeryP/cvgryPge => M; exists `|ceil M|%N => //= m. rewrite /= -(ler_nat R); apply: le_trans. by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm. rewrite monotone_convergence //. @@ -2617,7 +2611,7 @@ rewrite monotone_convergence //. have [muDoo|muDoo] := ltP (mu D) +oo; last first. exists 1%N => // m /= m0; move: muDoo; rewrite leye_eq => /eqP ->. by rewrite mulry gtr0_sg ?mul1e ?leey// ltr0n. - exists `|reals.ceil (M / fine (mu D))|%N => // m /=. + exists `|ceil (M / fine (mu D))|%N => // m /=. rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//. rewrite -lee_pdivrMr; last by rewrite fine_gt0// lt0e muD0 measure_ge0. rewrite lee_fin (le_trans _ MDm)//. @@ -3438,14 +3432,14 @@ have [M M0 muM] : exists2 M, (0 <= M)%R & apply/eqP/negPn/negP => /eqP muED0; move/not_forallP : muM; apply. have [muEDoo|] := ltP (mu (E `&` D)) +oo; last first. by rewrite leye_eq => /eqP ->; exists 1%N; rewrite mul1e leye_eq. -exists `|reals.ceil (M * (fine (mu (E `&` D)))^-1)|%N.+1. +exists `|ceil (M * (fine (mu (E `&` D)))^-1)|%N.+1. apply/negP; rewrite -ltNge. rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first. by rewrite fin_numElt muEDoo (lt_le_trans _ (measure_ge0 _ _)). rewrite lte_fin -ltr_pdivrMr. rewrite -natr1 natr_absz ger0_norm. by rewrite (le_lt_trans (ceil_ge _))// ltrDl. - by rewrite ceil_ge0// divr_ge0//; apply/le0R/measure_ge0; exact: measurableI. + by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _))// divr_ge0. rewrite -lte_fin fineK. rewrite lt0e measure_ge0 andbT. suff: E `&` D = E by move=> ->; exact/eqP. @@ -3686,14 +3680,15 @@ move=> mf; split=> [iDf0|Df0]. rewrite predeqE => t; split=> [[Dt ft0]|[n _ /= [Dt nft]]]. have [ftoo|ftoo] := eqVneq `|f t| +oo. by exists 0%N => //; split => //=; rewrite ftoo /= leey. - pose m := `|reals.ceil (fine `|f t|)^-1|%N. + pose m := `|ceil (fine `|f t|)^-1|%N. have ftfin : `|f t|%E \is a fin_num by rewrite ge0_fin_numE// ltey. exists m => //; split => //=. rewrite -(@fineK _ `|f t|) // lee_fin -ler_pV2; last 2 first. - rewrite inE unitfE fine_eq0// abse_eq0 ft0/= fine_gt0//. by rewrite lt0e abse_ge0 abse_eq0 ft0 ltey. - by rewrite inE unitfE invr_eq0 pnatr_eq0 /= invr_gt0. - rewrite invrK /m -natr1 natr_absz ger0_norm ?ceil_ge0//. + rewrite invrK /m -natr1 natr_absz ger0_norm; last first. + by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _)). rewrite (@le_trans _ _ ((fine `|f t|)^-1 + 1)%R) ?lerDl//. by rewrite lerD2r// ceil_ge. by split => //; apply: contraTN nft => /eqP ->; rewrite abse0 -ltNge. @@ -6456,7 +6451,7 @@ move=> Ef; have {Ef} : mu.-negligible (E `&` [set x | 0 < f^* x]). near \oo => m; exists m => //=. rewrite -(@fineK _ (f^* x)) ?gt0_fin_numE ?ltey// lte_fin. rewrite invf_plt ?posrE//; last by rewrite fine_gt0// ltey fx0. - set r := _^-1; rewrite (@le_lt_trans _ _ `|reals.ceil r|.+1%:R)//. + set r := _^-1; rewrite (@le_lt_trans _ _ `|ceil r|.+1%:R)//. by rewrite (le_trans _ (abs_ceil_ge _))// ler_norm. by rewrite ltr_nat ltnS; near: m; exact: nbhs_infty_gt. apply: negligibleS => z /= /not_implyP[Ez H]; split => //. @@ -6658,14 +6653,14 @@ have fE y k r : (ball 0%R k.+1%:R) y -> (r < 1)%R -> rewrite (le_trans (ltW yk1))// -lerBlDr opprK -lerBrDl. rewrite -natrB//; last by rewrite -addnn addSnnS ltn_addl. by rewrite -addnn addnK ler1n. -have := h `|reals.ceil x|.+1%N Logic.I. -have Bxx : B `|reals.ceil x|.+1 x. +have := h `|ceil x|.+1%N Logic.I. +have Bxx : B `|ceil x|.+1 x. rewrite /B /ball/= sub0r normrN (le_lt_trans (abs_ceil_ge _))// ltr_nat. by rewrite -addnn addSnnS ltn_addl. move=> /(_ Bxx)/fine_cvgP[davg_fk_fin_num davg_fk0]. have f_fk_ceil : \forall t \near 0^'+, \int[mu]_(y in ball x t) `|(f y)%:E - (f x)%:E| = - \int[mu]_(y in ball x t) `|fk `|reals.ceil x|.+1 y - fk `|reals.ceil x|.+1 x|%:E. + \int[mu]_(y in ball x t) `|fk `|ceil x|.+1 y - fk `|ceil x|.+1 x|%:E. near=> t. apply: eq_integral => /= y /[1!inE] xty. rewrite -(fE x _ t)//; last first. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 3a85507b3..2190aa44c 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1,6 +1,6 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. -From mathcomp Require Import finmap fingroup perm rat. +From mathcomp Require Import finmap fingroup perm rat archimedean. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop. Require Import reals ereal signed topology numfun normedtype function_spaces. @@ -1157,10 +1157,12 @@ rewrite predeqE => t; split => [/= [Dt ft]|]. have [ft0|ft0] := leP 0%R (fine (f t)). exists `|ceil (fine (f t))|%N => //=; split => //; split. by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// lerNl oppr0. - by rewrite natr_absz ger0_norm ?ceil_ge0// -(fineK ft) lee_fin ceil_ge. + rewrite natr_absz ger0_norm; last first. + by rewrite -ceil_ge0 (lt_le_trans _ ft0). + by rewrite -(fineK ft) lee_fin ceil_ge. exists `|floor (fine (f t))|%N => //=; split => //; split. - rewrite natr_absz ltr0_norm ?floor_lt0// EFinN. - by rewrite -{2}(fineK ft) lee_fin mulrNz opprK floor_le. + rewrite natr_absz ltr0_norm -?floor_lt0// EFinN. + by rewrite -{2}(fineK ft) lee_fin mulrNz opprK ge_floor// ?num_real. by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)). move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt. by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry. @@ -1407,8 +1409,8 @@ move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge. rewrite lee_fin; have [r0|r0] := leP 0%R r. by rewrite (le_trans _ r0) // lerNl oppr0 ler0n. rewrite lerNl -abszN natr_absz gtr0_norm; last first. - by rewrite ltrNr oppr0 floor_lt0. -by rewrite mulrNz lerNl opprK floor_le. + by rewrite ltrNr oppr0 -floor_lt0. +by rewrite mulrNz lerNl opprK ge_floor. Qed. Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R). @@ -1417,7 +1419,7 @@ rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry. move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=. rewrite andbT lte_fin ltNge. have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0). -by rewrite natr_absz gtr0_norm // ?ceil_ge// ceil_gt0. +by rewrite natr_absz gtr0_norm// ?ceil_ge// -ceil_gt0. Qed. End erealwithrays. @@ -2440,8 +2442,9 @@ have finite_set_F i : finite_set (F i). - by move=> /= x [n Fni Bnx]; exists n => //; exists i. have {CFi Fir2} := le_trans MC (le_trans CFi Fir2). apply/negP; rewrite -ltNge lebesgue_measure_ball// lte_fin. - rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm ?ceil_ge0// -ltr_pdivrMr//. - by rewrite -ltrBlDr (lt_le_trans _ (ceil_ge _))// ltrBlDr ltrDl. + rewrite -(@natr1 _ `| _ |%N) natr_absz ger0_norm; last first. + by rewrite -ceil_ge0// (lt_le_trans (ltrN10 _)). + by rewrite -ltr_pdivrMr// -ltrBlDr (lt_le_trans _ (ceil_ge _))// ltrBlDr ltrDl. have mur2_fin_num_ : mu (ball (0:R) (r%:num + 2))%R < +oo. by rewrite lebesgue_measure_ball// ltry. have FE : \sum_(n R) : Proof. exists (fun k => `](- k%:R), k%:R]%classic). apply/esym; rewrite -subTset => /= x _ /=. - exists `|(floor `|x|%R + 1)%R|%N; rewrite //= in_itv/=. - rewrite !natr_absz intr_norm intrD -RfloorE. - suff: `|x| < `|Rfloor `|x| + 1| by rewrite ltr_norml => /andP[-> /ltW->]. + exists `|(floor `|x| + 1)%R|%N; rewrite //= in_itv/=. + rewrite !natr_absz intr_norm intrD. + suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->]. rewrite [ltRHS]ger0_norm//. - by rewrite (le_lt_trans _ (lt_succ_Rfloor _))// ?ler_norm. - by rewrite addr_ge0// -Rfloor0 le_Rfloor. + by rewrite intrD1 (le_lt_trans _ (lt_succ_floor _))// ?ler_norm. + by rewrite addr_ge0// ler0z floor_ge0. move=> k; split => //; rewrite wlength_itv /= -EFinB. by case: ifP; rewrite ltey. Qed. diff --git a/theories/measure.v b/theories/measure.v index 59f84235d..7bcba633e 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1,5 +1,5 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect all_algebra finmap. +From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop. Require Import reals ereal signed topology normedtype sequences esum numfun. @@ -2202,7 +2202,7 @@ Proof. move=> infA; apply/eqyP => r r0. have [B BA Br] := infinite_set_fset `|ceil r| infA. apply: esum_ge; exists [set` B] => //; apply: (@le_trans _ _ `|ceil r|%:R%:E). - by rewrite lee_fin natr_absz gtr0_norm ?ceil_gt0// ceil_ge. + by rewrite lee_fin natr_absz gtr0_norm -?ceil_gt0// ceil_ge. move: Br; rewrite -(@ler_nat R) -lee_fin => /le_trans; apply. rewrite (eq_fsbigr (cst 1))/=; last first. by move=> i /[!inE] /BA /mem_set iA; rewrite diracE iA. @@ -2294,7 +2294,7 @@ move=> F mF tF mUF; rewrite [X in X @ \oo --> _](_ : _ = (fun n => (r%:num)%:E * \sum_(0 <= i < n) m (F i))); last first. by apply/funext => k; rewrite ge0_sume_distrr. rewrite /mscale; have [->|r0] := eqVneq r%:num 0%R. - rewrite mul0e [X in X @ \oo --> _](_ : _ = (fun=> 0)); first exact: cvg_cst. + rewrite mul0e [X in X @ \oo --> _](_ : _ = cst 0); first exact: cvg_cst. by under eq_fun do rewrite mul0e. by apply: cvgeMl => //; exact: measure_semi_sigma_additive. Qed. diff --git a/theories/normedtype.v b/theories/normedtype.v index 6b5b67271..721569595 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2,7 +2,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. From mathcomp Require Import rat interval zmodp vector fieldext falgebra. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import archimedean. From mathcomp Require Import cardinality set_interval Rstruct. Require Import ereal reals signed topology prodnormedzmodule function_spaces. @@ -146,6 +146,7 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. Import numFieldTopology.Exports. +From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -252,13 +253,13 @@ End pseudoMetricnormedzmodule_lemmas. Lemma bigcup_ballT {R : realType} : \bigcup_n ball (0%R : R) n%:R = setT. Proof. apply/seteqP; split => // x _; have [x0|x0] := ltP 0%R x. - exists `|reals.ceil x|.+1 => //. + exists `|ceil x|.+1 => //. rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (ceil_ge _))//. - by rewrite -natr1 natr_absz -abszE gtz0_abs// ?ceil_gt0// ltr_pwDr. -exists `|reals.ceil (- x)|.+1 => //. + by rewrite -natr1 natr_absz -abszE gtz0_abs// -?ceil_gt0// ltr_pwDr. +exists `|ceil (- x)|.+1 => //. rewrite /ball /= sub0r normrN ler0_norm// (le_lt_trans (ceil_ge _))//. -rewrite -natr1 natr_absz -abszE gez0_abs ?ceil_ge0// 1?lerNr ?oppr0//. -by rewrite ltr_pwDr. +rewrite -natr1 natr_absz -abszE gez0_abs ?ltr_pwDr// -ceil_ge0 ltrNl opprK. +by rewrite (le_lt_trans x0). Qed. Section lower_semicontinuous. @@ -596,8 +597,8 @@ Proof. split=> [/cvgryPge|/cvgnyPge] Foo. by apply/cvgnyPge => A; near do rewrite -(@ler_nat R); apply: Foo. apply/cvgryPgey; near=> A; near=> n. -rewrite (le_trans (@ceil_ge R A))// (ler_int _ _ (f n)) [reals.ceil _]intEsign. -by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo. +rewrite (le_trans (@ceil_ge R A))// (ler_int _ _ (f n)) [ceil _]intEsign. +by rewrite le_gtF ?expr0 ?mul1r ?lez_nat -?ceil_ge0//; near: n; apply: Foo. Unshelve. all: by end_near. Qed. Section ecvg_infty_numField. @@ -4919,7 +4920,7 @@ Lemma compact_bounded (K : realType) (V : normedModType K) (A : set V) : Proof. rewrite compact_cover => Aco. have covA : A `<=` \bigcup_(n : int) [set p | `|p| < n%:~R]. - by move=> p _; exists (reals.floor `|p| + 1) => //; rewrite rmorphD/= reals.lt_succ_floor. + by move=> p _; exists (floor `|p| + 1) => //=; rewrite lt_succ_floor. have /Aco [] := covA. move=> n _; rewrite openE => p; rewrite /= -subr_gt0 => ltpn. apply/nbhs_ballP; exists (n%:~R - `|p|) => // q. @@ -5763,13 +5764,13 @@ Notation r_gt0 := vitali_collection_partition_ub_gt0. Lemma ex_vitali_collection_partition i : V i -> exists n, vitali_collection_partition n i. Proof. -move=> Vi; pose f := reals.floor (r / (radius (B i))%:num). +move=> Vi; pose f := floor (r / (radius (B i))%:num). have f_ge0 : 0 <= f by rewrite floor_ge0// divr_ge0// ltW// (r_gt0 Vi). have [m /andP[mf fm]] := leq_ltn_expn `|f|.-1. exists m; split => //; apply/andP; split => [{mf}|{fm}]. rewrite -(@ler_nat R) in fm. rewrite ltr_pdivrMr// mulrC -ltr_pdivrMr// (lt_le_trans _ fm)//. - rewrite (lt_le_trans (reals.lt_succ_floor _))//= -/f -natr1 lerD2r//. + rewrite (lt_le_trans (lt_succ_floor _))//= -/f intrD -natr1 lerD2r//. have [<-|f0] := eqVneq 0 f; first by rewrite /= ler0n. rewrite prednK//; last by rewrite absz_gt0 eq_sym. by rewrite natr_absz// ger0_norm. @@ -5779,7 +5780,7 @@ rewrite ler_pdivlMr// mulrC -ler_pdivlMr//. have [f0|f0] := eqVneq 0 f. by move: mf; rewrite -f0 absz0 leNgt expnS ltr_nat leq_pmulr// expn_gt0. rewrite (le_trans mf)// prednK//; last by rewrite absz_gt0 eq_sym. -by rewrite natr_absz// ger0_norm// reals.floor_le. +by rewrite natr_absz// ger0_norm// ge_floor. Qed. Lemma cover_vitali_collection_partition : @@ -5972,7 +5973,7 @@ exists j; split => //. Qed. Lemma vitali_lemma_infinite_cover : { D : set I | [/\ countable D, - D `<=` V, trivIset D (closure\o B) & + D `<=` V, trivIset D (closure \o B) & cover V (closure \o B) `<=` cover D (closure \o scale_ball 5%:R \o B)] }. Proof. have [D [cD DV tD maxD]] := vitali_lemma_infinite. diff --git a/theories/real_interval.v b/theories/real_interval.v index cc90e5e51..f9feec095 100644 --- a/theories/real_interval.v +++ b/theories/real_interval.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. -From mathcomp Require Import finmap fingroup perm rat. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import fingroup perm rat archimedean finmap. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Export set_interval. From HB Require Import structures. Require Import reals ereal signed topology normedtype sequences. @@ -14,6 +14,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. +From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -176,7 +177,7 @@ rewrite predeqE => y; split=> /=; last first. rewrite in_itv /= andbT => xy; exists `|floor y|%N.+1 => //=. rewrite in_itv /= xy /=. have [y0|y0] := ltP 0 y; last by rewrite (le_lt_trans y0)// ltr_pwDr. -by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// lt_succ_floor. +by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// intrD1 lt_succ_floor. Qed. Lemma itv_o_inftyEbigcup x : @@ -340,10 +341,10 @@ move gxE : (g x) => gx; case: gx gxE => [gx| |gxoo fxoo]; last 2 first. - by exists 0%N => //; rewrite /E/= gxoo addey// ?leey// -ltNye. move fxE : (f x) => fx; case: fx fxE => [fx fxE gxE|fxoo gxE _|//]; last first. by exists 0%N => //; rewrite /E/= fxoo gxE// addye// leey. -rewrite lte_fin -subr_gt0 => fgx; exists `|floor (fx - gx)^-1%R|%N => //. +rewrite lte_fin -subr_gt0 => fgx; exists `|floor (fx - gx)^-1|%N => //. rewrite /E/= -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0; last exact/ltW. rewrite fxE gxE lee_fin -[leRHS]invrK lef_pV2//. -- by apply/ltW; rewrite lt_succ_floor. +- by rewrite intrD1 ltW// lt_succ_floor. - by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW. - by rewrite posrE invr_gt0. Qed. @@ -363,9 +364,10 @@ apply/seteqP; split=> [x ->|]. by move=> i _/=; rewrite in_itv/= lexx ltrBlDr ltrDl invr_gt0 ltr0n. move=> x rx; apply/esym/eqP; rewrite eq_le (itvP (rx 0%N _))// andbT. apply/ler_addgt0Pl => e e_gt0; rewrite -lerBlDl ltW//. -have := rx `|floor e^-1%R|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//. +have := rx `|floor e^-1|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//. rewrite lerD2l lerN2 -lef_pV2 ?invrK//; last by rewrite posrE. -by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW// lt_succ_floor. +rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//. +by rewrite intrD1 lt_succ_floor. Qed. Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) : @@ -375,11 +377,11 @@ Proof. apply/seteqP; split => [x/=|]; last first. move=> x [n _ /=] /[!in_itv] /andP[-> /le_lt_trans]; apply. by rewrite ltrBlDr ltrDl invr_gt0 ltr0n. -rewrite in_itv/= => /andP[sx xs]; exists `|ceil ((s - x)^-1)|%N => //=. +rewrite in_itv/= => /andP[sx xs]; exists `|ceil (s - x)^-1|%N => //=. rewrite in_itv/= sx/= lerBrDl addrC -lerBrDl. rewrite -[in X in _ <= X](invrK (s - x)) ler_pV2. - rewrite -natr1 natr_absz ger0_norm; last first. - by rewrite ceil_ge0// invr_ge0 subr_ge0 ltW. + by rewrite -ceil_ge0 (lt_le_trans (ltrN10 R))// invr_ge0 subr_ge0 ltW. by rewrite (@le_trans _ _ (ceil (s - x)^-1)%:~R)// ?lerDl// ceil_ge. - by rewrite inE unitfE ltr0n andbT pnatr_eq0. - by rewrite inE invr_gt0 subr_gt0 xs andbT unitfE invr_eq0 subr_eq0 gt_eqF. @@ -403,7 +405,8 @@ Proof. apply/seteqP; split=> y; rewrite /= !in_itv/= andbT; last first. by move=> [k _ /=]; move: b => [|] /=; rewrite in_itv/= => /andP[//] /ltW. move=> xy; exists `|ceil (y - x)|%N => //=; rewrite in_itv/= xy/= -lerBlDl. -rewrite !natr_absz/= ger0_norm ?ceil_ge0 ?subr_ge0 ?ceil_ge//. +rewrite !natr_absz/= ger0_norm -?ceil_ge0 ?ceil_ge//. +rewrite (lt_le_trans (ltrN10 R))// subr_ge0. by case: b xy => //= /ltW. Qed. @@ -424,7 +427,7 @@ Proof. rewrite -subTset => x _ /=; exists `|(floor `|x| + 1)%R|%N => //=. rewrite in_itv/= !natr_absz intr_norm intrD. have : `|x| < `|(floor `|x|)%:~R + 1|. - by rewrite [ltRHS]ger0_norm ?lt_succ_floor// addr_ge0// ler0z floor_ge0. + by rewrite [ltRHS]ger0_norm ?intrD1 ?lt_succ_floor// ler0z addr_ge0// floor_ge0. case: b => /=. - by move/ltW; rewrite ler_norml => /andP[-> ->]. - by rewrite ltr_norml => /andP[-> /ltW->]. diff --git a/theories/realfun.v b/theories/realfun.v index 1507cc6eb..24735d797 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1,6 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap. +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum archimedean. From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. +From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality. Require Import ereal reals signed topology prodnormedzmodule normedtype derive. @@ -183,9 +184,9 @@ exists (fun n => sval (cid (He (PosNum (invn n))))). apply/cvgrPdist_lt => r r0; near=> t. rewrite /sval/=; case: cid => x [px xpt _]. rewrite distrC (lt_le_trans xpt)// -(@invrK _ r) lef_pV2 ?posrE ?invr_gt0//. - near: t; exists `|ceil (r^-1)|%N => // s /=. + near: t; exists `|ceil r^-1|%N => // s /=. rewrite -ltnS -(@ltr_nat R) => /ltW; apply: le_trans. - by rewrite natr_absz gtr0_norm ?ceil_gt0 ?invr_gt0// ceil_ge. + by rewrite natr_absz gtr0_norm -?ceil_gt0 ?invr_gt0// ceil_ge. move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)). rewrite /sval/=; case: cid => // x [px xpn]. by rewrite leNgt distrC => /negP. @@ -235,7 +236,7 @@ have y_p : y_ n @[n --> \oo] --> p. near: t. exists `|ceil e^-1|%N => // k /= ek. rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%:~R)//. - by rewrite ger0_norm// ?ceil_ge0// ?invr_ge0// ltW. + by rewrite ger0_norm -?ceil_ge0// (lt_le_trans (ltrN10 _))// invr_ge0// ltW. by move: ek;rewrite -(leq_add2r 1) !addn1 -(ltr_nat R) => /ltW. have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p). near \oo => n. @@ -1426,7 +1427,6 @@ Proof. by move=> fct fK; have [] := near_can_continuousAcan_sym fK fct. Qed. End real_inverse_functions. Section real_inverse_function_instances. - Variable R : realType. Lemma exprn_continuous n : continuous (@GRing.exp R ^~ n). @@ -2268,7 +2268,7 @@ have Nffin : TV a x (\- f) \is a fin_num. exact: (bounded_variationl ax xb). rewrite /pos_tv /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //. - rewrite addeAC oppeD //= ?fin_num_adde_defl //. - by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr. + by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -splitr. - by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split. - by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split. - by rewrite fin_numM // fin_numD; apply/andP; split. @@ -2343,7 +2343,7 @@ rewrite {1}variation_prev; last exact: itv_partition1. rewrite /= -addeA -lteBrDr; last by rewrite fin_numD; apply/andP. rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA. move/lt_trans; apply. -rewrite [x in (_ < x%:E)%E]Num.Theory.splitr EFinD addeC lteD2lE //. +rewrite [x in (_ < x%:E)%E]splitr EFinD addeC lteD2lE //. rewrite -addeA. apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E). rewrite [in leRHS]variation_prev; last exact: itv_partition1. diff --git a/theories/reals.v b/theories/reals.v index cf231eb6e..1e41479c7 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -32,18 +32,15 @@ (* Rtoint r == r when r is an integer, 0 otherwise *) (* floor_set x := [set y | Rtoint y /\ y <= x] *) (* Rfloor x == the floor of x as a real number *) -(* floor x == the floor of x as an integer (type int) *) (* range1 x := [set y |x <= y < x + 1] *) (* Rceil x == the ceil of x as a real number, i.e., - Rfloor (- x) *) -(* ceil x := - floor (- x) *) (* ``` *) (* *) (******************************************************************************) From HB Require Import structures. -From mathcomp Require Import all_ssreflect all_algebra. -From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect all_algebra archimedean. +From mathcomp Require Import boolp classical_sets set_interval. Require Import Setoid. @@ -56,6 +53,7 @@ Unset Printing Implicit Defensive. Unset SsrOldRewriteGoalsOrder. Import Order.TTheory Order.Syntax GRing.Theory Num.Def Num.Theory. +From mathcomp Require Import mathcomp_extra. (* -------------------------------------------------------------------- *) Delimit Scope real_scope with real. @@ -97,9 +95,7 @@ Implicit Types x : R. Lemma has_ub_image_norm E : has_ubound (normr @` E) -> has_ubound E. Proof. case => M /ubP uM; exists `|M|; apply/ubP => r rS. -rewrite (le_trans (real_ler_norm _)) ?num_real //. -rewrite (le_trans (uM _ _)) ?real_ler_norm ?num_real //. -by exists r. +by rewrite (le_trans (ler_norm _))// (le_trans (uM _ _))//; exact: ler_norm. Qed. Lemma has_inf_supN E : has_sup (-%R @` E) <-> has_inf E. @@ -121,12 +117,10 @@ 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], - has_sup E -> ubound E (supremum 0 E) ; - sup_adherent_subdef : - forall (E : set [the archiFieldType of R]) (eps : R), 0 < eps -> - has_sup E -> exists2 e : R, E e & (supremum 0 E - eps) < e ; + sup_upper_bound_subdef : forall E : set [the archiFieldType of R], + has_sup E -> ubound E (supremum 0 E) ; + sup_adherent_subdef : forall (E : set [the archiFieldType of R]) (eps : R), + 0 < eps -> has_sup E -> exists2 e : R, E e & (supremum 0 E - eps) < e }. #[short(type=realType)] @@ -137,8 +131,6 @@ Bind Scope ring_scope with Real.sort. (* -------------------------------------------------------------------- *) Definition sup {R : realType} := @supremum _ R 0. -(*Local Notation "-` E" := [pred x | - x \in E] - (at level 35, right associativity) : function_scope.*) Definition inf {R : realType} (E : set R) := - sup (-%R @` E). (* -------------------------------------------------------------------- *) @@ -238,21 +230,18 @@ Qed. End ToInt. (* -------------------------------------------------------------------- *) + Section RealDerivedOps. Variable R : realType. Implicit Types x y : R. Definition floor_set x := [set y : R | (y \is a Rint) && (y <= x)]. -Definition Rfloor x : R := sup (floor_set x). - -Definition floor x : int := Rtoint (Rfloor x). +Definition Rfloor x : R := (floor x)%:~R. Definition range1 (x : R) := [set y | x <= y < x + 1]. -Definition Rceil x := - Rfloor (- x). - -Definition ceil x := - floor (- x). +Definition Rceil x : R := (ceil x)%:~R. End RealDerivedOps. @@ -340,14 +329,14 @@ have ABsup : has_sup [set x + y | x in A & y in B]. apply: le_anti; apply/andP; split. apply: sup_le_ub; first by case: ABsup. by move=> ? [p Ap [q Bq] <-]; apply: lerD; exact: sup_ub. -rewrite real_leNgt ?num_real// -subr_gt0; apply/negP. +rewrite leNgt -subr_gt0; apply/negP. set eps := (_ + _ - _) => epos. have e2pos : 0 < eps / 2%:R by rewrite divr_gt0// ltr0n. have [r Ar supBr] := sup_adherent e2pos supA. have [s Bs supAs] := sup_adherent e2pos supB. have := ltrD supBr supAs. rewrite -addrA [-_+_]addrC -addrA -opprD -splitr addrA /= opprD opprK addrA. -rewrite subrr add0r; apply/negP; rewrite -real_leNgt ?num_real//. +rewrite subrr add0r; apply/negP; rewrite -leNgt. by apply: sup_upper_bound => //; exists r => //; exists s. Qed. @@ -470,27 +459,23 @@ by rewrite absz_eq0 subr_eq0 eq_sym (negbTE ne_yz). Qed. Lemma isint_Rfloor x : Rfloor x \is a Rint. -Proof. by case/andP: (sup_in_floor_set x). Qed. +Proof. by rewrite inE; exists (floor x). Qed. Lemma RfloorE x : Rfloor x = (floor x)%:~R. -Proof. by rewrite /floor RtointK ?isint_Rfloor. Qed. +Proof. by []. Qed. + +Lemma mem_rg1_floor x : (range1 (floor x)%:~R) x. +Proof. by rewrite /range1 /mkset intrD1 ge_floor lt_succ_floor. Qed. Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x. -Proof. -rewrite /range1/mkset. -have /andP[_ ->] /= := sup_in_floor_set x. -have [|] := pselect ((floor_set x) (Rfloor x + 1)); last first. - rewrite /floor_set => /negP. - by rewrite negb_and -ltNge rpredD // ?(Rint1, isint_Rfloor). -move/ubP : (sup_upper_bound (has_sup_floor_set x)) => h/h. -by rewrite gerDl ler10. -Qed. +Proof. exact: mem_rg1_floor. Qed. Lemma Rfloor_le x : Rfloor x <= x. Proof. by case/andP: (mem_rg1_Rfloor x). Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="use `ge_floor` instead")] Lemma floor_le x : (floor x)%:~R <= x. -Proof. by rewrite -RfloorE; exact: Rfloor_le. Qed. +Proof. by rewrite ge_floor. Qed. Lemma lt_succ_Rfloor x : x < Rfloor x + 1. Proof. by case/andP: (mem_rg1_Rfloor x). Qed. @@ -511,34 +496,24 @@ Proof. by rewrite /range1/mkset lexx /= ltrDl ltr01. Qed. Lemma range1zP (m : int) x : Rfloor x = m%:~R <-> (range1 m%:~R) x. Proof. split=> [<-|h]; first exact/mem_rg1_Rfloor. -apply/eqP; rewrite RfloorE eqr_int; apply/eqP/(@range1z_inj x) => //. -by rewrite /range1/mkset -RfloorE mem_rg1_Rfloor. +by congr intmul; apply/floor_def; rewrite -intrD1. Qed. Lemma Rfloor_natz (z : int) : Rfloor z%:~R = z%:~R :> R. Proof. by apply/range1zP/range1rr. Qed. -Lemma Rfloor0 : Rfloor 0 = 0 :> R. -Proof. by rewrite -{1}(mulr0z 1) Rfloor_natz. Qed. +Lemma Rfloor0 : Rfloor 0 = 0 :> R. Proof. by rewrite /Rfloor floor0. Qed. -Lemma Rfloor1 : Rfloor 1 = 1 :> R. -Proof. by rewrite -{1}(mulr1z 1) Rfloor_natz. Qed. +Lemma Rfloor1 : Rfloor 1 = 1 :> R. Proof. by rewrite /Rfloor floor1. Qed. Lemma le_Rfloor : {homo (@Rfloor R) : x y / x <= y}. -Proof. -move=> x y le_xy; case: lerP=> //=; rewrite -Rint_ler_addr1 ?isint_Rfloor //. -move/(lt_le_trans (lt_succ_Rfloor y))/lt_le_trans/(_ (Rfloor_le x)). -by rewrite ltNge le_xy. -Qed. +Proof. by move=> x y /Num.Theory.floor_le; rewrite ler_int. Qed. Lemma Rfloor_ge_int x (n : int) : (n%:~R <= x)= (n%:~R <= Rfloor x). -Proof. -apply/idP/idP; last by move/le_trans => /(_ _ (Rfloor_le x)). -by move/le_Rfloor; apply le_trans; rewrite Rfloor_natz. -Qed. +Proof. by rewrite ler_int floor_ge_int. Qed. Lemma Rfloor_lt_int x (z : int) : (x < z%:~R) = (Rfloor x < z%:~R). -Proof. by rewrite ltNge Rfloor_ge_int -ltNge. Qed. +Proof. by rewrite ltr_int floor_lt_int. Qed. Lemma Rfloor_le0 x : x <= 0 -> Rfloor x <= 0. Proof. by move=> ?; rewrite -Rfloor0 le_Rfloor. Qed. @@ -546,44 +521,9 @@ Proof. by move=> ?; rewrite -Rfloor0 le_Rfloor. Qed. Lemma Rfloor_lt0 x : x < 0 -> Rfloor x < 0. Proof. by move=> x0; rewrite (le_lt_trans _ x0) // Rfloor_le. Qed. -Lemma floor_natz n : floor (n%:R : R) = n%:~R :> int. -Proof. by rewrite /floor (Rfloor_natz n) Rtointz intz. Qed. - -Lemma floor0 : floor (0 : R) = 0. -Proof. by rewrite /floor Rfloor0 (_ : 0 = 0%:R) // Rtointn. Qed. - -Lemma floor1 : floor (1 : R) = 1. -Proof. by rewrite /floor Rfloor1 (_ : 1 = 1%:R) // Rtointn. Qed. - -Lemma floor_ge0 x : (0 <= floor x) = (0 <= x). -Proof. by rewrite -(@ler_int R) -RfloorE -Rfloor_ge_int. Qed. - -Lemma floor_le0 x : x <= 0 -> floor x <= 0. -Proof. by move=> ?; rewrite -(@ler_int R) -RfloorE Rfloor_le0. Qed. - -Lemma floor_lt0 x : x < 0 -> floor x < 0. -Proof. by move=> ?; rewrite -(@ltrz0 R) RtointK ?isint_Rfloor// Rfloor_lt0. Qed. - -Lemma le_floor : {homo @floor R : x y / x <= y}. -Proof. by move=>*; rewrite -(@ler_int R) !RtointK ?isint_Rfloor ?le_Rfloor. Qed. - -Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1). -Proof. -apply/idP/orP => [|[x0|/le_floor r1]]; first rewrite neq_lt => /orP[x0|x0]. -- by left; apply: contra_lt x0; rewrite floor_ge0. -- by right; rewrite (le_trans _ (floor_le _))// ler1z -gtz0_ge1. -- by rewrite lt_eqF//; apply: contra_lt x0; rewrite floor_ge0. -- by rewrite gt_eqF// (lt_le_trans _ r1)// floor1. -Qed. - -Lemma lt_succ_floor x : x < (floor x)%:~R + 1. -Proof. by rewrite -RfloorE lt_succ_Rfloor. Qed. - -Lemma floor_lt_int x (z : int) : (x < z%:~R) = (floor x < z). -Proof. by rewrite Rfloor_lt_int RfloorE ltr_int. Qed. - -Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= floor x). -Proof. by rewrite Rfloor_ge_int RfloorE ler_int. Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.floor_le` instead")] +Lemma le_floor : {homo @Num.floor R : x y / x <= y}. +Proof. exact: Num.Theory.floor_le. Qed. Lemma ltr_add_invr (y x : R) : y < x -> exists k, y + k.+1%:R^-1 < x. Proof. @@ -591,8 +531,8 @@ move=> yx; exists `|floor (x - y)^-1|%N. rewrite -ltrBrDl -{2}(invrK (x - y)%R) ltf_pV2 ?qualifE/= ?ltr0n//. by rewrite invr_gt0 subr_gt0. rewrite -natr1 natr_absz ger0_norm. - by rewrite floor_ge0 invr_ge0 subr_ge0 ltW. -by rewrite -RfloorE lt_succ_Rfloor. + by rewrite -floor_ge_int// invr_ge0 subr_ge0 ltW. +by rewrite intrD1 lt_succ_floor. Qed. End FloorTheory. @@ -603,54 +543,26 @@ Variable R : realType. Implicit Types x y : R. Lemma isint_Rceil x : Rceil x \is a Rint. -Proof. by rewrite /Rceil rpredN isint_Rfloor. Qed. +Proof. by rewrite /Rceil RintC. Qed. Lemma Rceil0 : Rceil 0 = 0 :> R. -Proof. by rewrite /Rceil oppr0 Rfloor0 oppr0. Qed. +Proof. by rewrite /Rceil ceil0. Qed. Lemma Rceil_ge x : x <= Rceil x. -Proof. by rewrite /Rceil lerNr Rfloor_le. Qed. +Proof. by rewrite /Rceil le_ceil// num_real. Qed. Lemma le_Rceil : {homo (@Rceil R) : x y / x <= y}. -Proof. by move=> x y ?; rewrite lerNl opprK le_Rfloor // lerNl opprK. Qed. +Proof. by move=> x y ?; rewrite /Rceil ler_int ceil_le. Qed. Lemma Rceil_ge0 x : 0 <= x -> 0 <= Rceil x. -Proof. by move=> ?; rewrite -Rceil0 le_Rceil. Qed. +Proof. by move=> x0; rewrite /Rceil ler0z -(ceil0 R) ceil_le. Qed. Lemma RceilE x : Rceil x = (ceil x)%:~R. -Proof. by rewrite /Rceil /ceil RfloorE mulrNz. Qed. - -Lemma ceil_ge x : x <= (ceil x)%:~R. -Proof. by rewrite -RceilE; exact: Rceil_ge. Qed. - -Lemma ceil_ge0 x : 0 <= x -> 0 <= ceil x. -Proof. by move/(ge_trans (ceil_ge x)); rewrite -(ler_int R). Qed. - -Lemma ceil_gt0 x : 0 < x -> 0 < ceil x. -Proof. by move=> ?; rewrite /ceil oppr_gt0 floor_lt0 // ltrNl oppr0. Qed. - -Lemma ceil_le0 x : x <= 0 -> ceil x <= 0. -Proof. by move=> x0; rewrite -lerNl oppr0 floor_ge0 -lerNr oppr0. Qed. - -Lemma le_ceil : {homo @ceil R : x y / x <= y}. -Proof. by move=> x y xy; rewrite lerNl opprK le_floor // lerNl opprK. Qed. - -Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (ceil x <= z). -Proof. by rewrite /ceil lerNl -floor_ge_int// -lerNr mulrNz opprK. Qed. - -Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < ceil x). -Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed. - -Lemma ceilN x : ceil (- x) = - floor x. Proof. by rewrite /ceil opprK. Qed. - -Lemma floorN x : floor (- x) = - ceil x. Proof. by rewrite /ceil opprK. Qed. +Proof. by []. Qed. -Lemma abs_ceil_ge x : `|x| <= `|ceil x|.+1%:R. -Proof. -rewrite -natr1 natr_absz; have [x0|x0] := ltP 0%R x. - by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl. -by rewrite !ler0_norm ?ceil_le0// /ceil opprK; exact/ltW/lt_succ_floor. -Qed. +#[deprecated(since="mathcomp-analysis 1.3.0", note="use `Num.Theory.ceil_le` instead")] +Lemma le_ceil : {homo @Num.ceil R : x y / x <= y}. +Proof. exact: ceil_le. Qed. End CeilTheory. diff --git a/theories/sequences.v b/theories/sequences.v index cdd82622d..703fae4aa 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix. From mathcomp Require Import interval rat archimedean. -From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import boolp classical_sets functions. From mathcomp Require Import set_interval. Require Import reals ereal signed topology normedtype landau. @@ -92,6 +92,7 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. Import numFieldNormedType.Exports. +From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -1274,9 +1275,9 @@ Proof. rewrite /series; near \oo => N; have xN : x < N%:R; last first. rewrite -(@is_cvg_series_restrict N.+1). by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; apply: S1_sup. -near: N; exists (absz (reals.floor x)).+1 => // m; rewrite /mkset -(@ler_nat R). -move/lt_le_trans => -> //; rewrite (lt_le_trans (reals.lt_succ_floor x)) // -addn1. -by rewrite natrD lerD2r -(@gez0_abs (reals.floor x)) ?reals.floor_ge0// ltW. +near: N; exists `|floor x|.+1 => // m; rewrite /mkset -(@ler_nat R). +move/lt_le_trans => -> //; rewrite (lt_le_trans (lt_succ_floor x))//. +by rewrite -intrD1 -natr1 lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW. Unshelve. all: by end_near. Qed. End exponential_series_cvg. diff --git a/theories/topology.v b/theories/topology.v index 82834994d..a9230bead 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. From mathcomp Require Import archimedean. From mathcomp Require Import boolp classical_sets functions. -From mathcomp Require Import cardinality mathcomp_extra fsbigop. +From mathcomp Require Import cardinality fsbigop. Require Import reals signed. (**md**************************************************************************) @@ -447,6 +447,7 @@ Unset Printing Implicit Defensive. Obligation Tactic := idtac. Import Order.TTheory GRing.Theory Num.Theory. +From mathcomp Require Import mathcomp_extra. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -2281,7 +2282,7 @@ Proof. by exists N. Qed. Lemma nbhs_infty_ger {R : realType} (r : R) : \forall n \near \oo, (r <= n%:R)%R. Proof. -exists (`|ceil r|)%N => // n /=; rewrite -(ler_nat R); apply: le_trans. +exists `|Num.ceil r|%N => // n /=; rewrite -(ler_nat R); apply: le_trans. by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm. Qed. @@ -4988,9 +4989,11 @@ apply/countable_uniformityP. exists (fun n => [set xy : T * T | ball xy.1 n.+1%:R^-1 xy.2]); last first. by move=> n; exact: (entourage_ball _ n.+1%:R^-1%:pos). move=> E; rewrite -entourage_ballE => -[e e0 subE]. -exists `|floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball. +exists `|Num.floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball. rewrite /= -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0// -natr1. -by rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0// 1?ltW// reals.lt_succ_floor. +rewrite natr_absz ger0_norm; last first. + by rewrite -floor_ge_int ?invr_ge0// ltW. +by rewrite intrD1 ltW// lt_succ_floor. Qed. (** Specific pseudoMetric spaces *) @@ -4998,16 +5001,20 @@ Qed. (** matrices *) Section matrix_PseudoMetric. Variables (m n : nat) (R : numDomainType) (T : pseudoMetricType R). -Implicit Types x y : 'M[T]_(m, n). -Definition mx_ball x (e : R) y := forall i j, ball (x i j) e (y i j). -Lemma mx_ball_center x (e : R) : 0 < e -> mx_ball x e x. -Proof. by move=> ???; apply: ballxx. Qed. -Lemma mx_ball_sym x y (e : R) : mx_ball x e y -> mx_ball y e x. -Proof. by move=> xe_y ??; apply/ball_sym/xe_y. Qed. -Lemma mx_ball_triangle x y z (e1 e2 : R) : +Implicit Types (x y : 'M[T]_(m, n)) (e : R). + +Definition mx_ball x e y := forall i j, ball (x i j) e (y i j). + +Lemma mx_ball_center x e : 0 < e -> mx_ball x e x. +Proof. by move=> ? ? ?; exact: ballxx. Qed. + +Lemma mx_ball_sym x y e : mx_ball x e y -> mx_ball y e x. +Proof. by move=> xe_y ? ?; apply/ball_sym/xe_y. Qed. + +Lemma mx_ball_triangle x y z e1 e2 : mx_ball x e1 y -> mx_ball y e2 z -> mx_ball x (e1 + e2) z. Proof. -by move=> xe1_y ye2_z ??; apply: ball_triangle; [apply: xe1_y| apply: ye2_z]. +by move=> xe1_y ye2_z ??; apply: ball_triangle; [exact: xe1_y|exact: ye2_z]. Qed. Lemma mx_entourage : entourage = entourage_ mx_ball. @@ -5016,14 +5023,14 @@ rewrite predeqE=> A; split; last first. move=> [_/posnumP[e] sbeA]. by exists (fun _ _ => [set xy | ball xy.1 e%:num xy.2]). move=> [P]; rewrite -entourage_ballE => entP sPA. -set diag := fun (e : {posnum R}) => [set xy : T * T | ball xy.1 e%:num xy.2]. +set diag := fun e : {posnum R} => [set xy : T * T | ball xy.1 e%:num xy.2]. exists (\big[Num.min/1%:pos]_i \big[Num.min/1%:pos]_j xget 1%:pos (fun e : {posnum R} => diag e `<=` P i j))%:num => //=. move=> MN MN_min; apply: sPA => i j. have /(xgetPex 1%:pos): exists e : {posnum R}, diag e `<=` P i j. by have [_/posnumP[e]] := entP i j; exists e. apply; apply: le_ball (MN_min i j). -apply: le_trans (@bigmin_le _ [the orderType _ of {posnum R}] _ _ i _) _. +apply: le_trans (@bigmin_le _ {posnum R} _ _ i _) _. exact: bigmin_le. Qed. @@ -5675,21 +5682,23 @@ Qed. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Local Definition distN (e : R) : nat := `|floor e^-1|%N. +Local Definition distN (e : R) : nat := `|Num.floor e^-1|%N. Local Lemma distN0 : distN 0 = 0%N. -Proof. by rewrite /distN invr0 reals.floor0. Qed. +Proof. by rewrite /distN invr0 floor0. Qed. -Local Lemma distN_nat (n : nat): distN (n%:R^-1) = n. +Local Lemma distN_nat (n : nat) : distN n%:R^-1 = n. Proof. -by rewrite /distN invrK floor_natz -[RHS]distn0; congr absz; rewrite subr0 intz. +rewrite /distN invrK. +apply/eqP; rewrite -(@eqr_nat R) natr_absz ger0_norm ?floor_ge0//. +by rewrite -intrEfloor intrEge0. Qed. Local Lemma distN_le e1 e2 : e1 > 0 -> e1 <= e2 -> (distN e2 <= distN e1)%N. Proof. move=> e1pos e1e2; rewrite /distN; apply: lez_abs2. by rewrite floor_ge0 ltW// invr_gt0 (lt_le_trans _ e1e2). -by rewrite le_floor// lef_pV2 ?invrK ?invr_gt0//; exact: (lt_le_trans _ e1e2). +by rewrite floor_le// lef_pV2 ?invrK ?invr_gt0//; exact: (lt_le_trans _ e1e2). Qed. Local Fixpoint n_step_ball n x e z := @@ -5819,7 +5828,7 @@ move: e1 e2 x z; elim: n. rewrite -[e2]addr0 -(subrr e1) addrA -lerBlDr opprK addrC. by rewrite [e2 + _]addrC -deE; exact: lerD. - by rewrite addn0. - move=> /negP; rewrite -real_ltNge ?num_real //. + move=> /negP; rewrite -ltNge//. move=> e1d1; exists y, z, 0%N, 0%N; split. - by apply: n_step_ball_le; last (exact: Oxy); exact: ltW. - rewrite -deE; apply: (@n_step_ball_le _ _ d2) => //. @@ -5837,7 +5846,7 @@ case: (pselect (e2 <= d2)). - by rewrite addn0. have d1E' : d1 = e1 + (e2 - d2). by move: deE; rewrite addrA [e1 + _]addrC => <-; rewrite -addrA subrr addr0. -move=> /negP; rewrite -?real_ltNge // ?num_real // => d2lee2. +move=> /negP; rewrite -ltNge// => d2lee2. case: (IH e1 (e2 - d2) x y); rewrite ?subr_gt0 // -d1E' //. move=> t1 [t2] [c1] [c2] [] Oxy1 gt1t2 t2y <-. exists t1, t2, c1, c2.+1; split => //. @@ -5896,7 +5905,7 @@ Lemma countable_uniform_bounded (x y : T) : in @ball _ U x 2 y. Proof. rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN. -suff -> : @floor R 2^-1 = 0 by rewrite absz0 /=. +rewrite [X in `|X|%N](_ : _ = 0) ?absz0//. apply/eqP; rewrite -[_ == _]negbK; rewrite floor_neq0 negb_or -?ltNge -?leNgt. by apply/andP; split => //; rewrite invf_lt1 //= ltrDl. Qed.