diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 774c2194b..fa364a20d 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -399,20 +399,15 @@ 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 (_ : 1 = 1%:~R)// floor_lt_int -ltzD1 add0r => /le_lt_trans; exact. -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. +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_natz n : Num.floor (n%:R : R) = n%:~R :> int. -Proof. by rewrite (Num.Theory.intrKfloor n) intz. 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. diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v index cc88039f4..900f467ce 100644 --- a/theories/altreals/realsum.v +++ b/theories/altreals/realsum.v @@ -141,16 +141,14 @@ 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 := `|Num.floor (`|f x|^-1)|%N; exists j; rewrite inE. - rewrite mul1r invf_plt ?unfold_in /= ?ltr0z ?normr_gt0 // /j -addn1 /=. - by rewrite PoszD gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0// lt_succ_floor. + 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 := `|Num.floor (M / i.+1%:R)|.+1. -pose K := (`|Num.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. @@ -158,7 +156,7 @@ apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first. by have:= fsvalP m; rewrite in_fset => /le_sEi. rewrite mul1r sumr_const -cardfE card_fseq undup_id // eq_si. rewrite -mulr_natr natrM mulrC mulfK ?pnatr_eq0//. -by rewrite pmulrn -addn1 PoszD gez0_abs ?floor_ge0// lt_succ_floor. +by case/trunc_itv/andP: ge0_M. Qed. End SummableCountable. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 7683f2728..22163c10e 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1287,22 +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 `|floor (r * 2 ^+ n.+1)|%N. - rewrite /= mem_index_iota -ltz_nat -lez_nat gez0_abs ?floor_ge0; last first. - by rewrite 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 /=; apply/andP; split. - rewrite ler_pdivrMr// (le_trans _ (ge_floor _)) //. - by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// (le_trans _ nr). - rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//. - rewrite -[in leRHS]natr1 -intr1 lerD2r// -(@gez0_abs (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 : @@ -1586,7 +1584,7 @@ case/cvg_ex => /= l; have [l0|l0] := leP 0%R l. rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//. 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). + 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 : diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 4d184c1bc..8e2741f29 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1159,7 +1159,7 @@ rewrite predeqE => t; split => [/= [Dt ft]|]. 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. exists `|floor (fine (f t))|%N => //=; split => //; split. - rewrite natr_absz ltr0_norm ?floor_lt0// EFinN. + 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. @@ -1407,7 +1407,7 @@ 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 ltrNr oppr0 -floor_lt0. by rewrite mulrNz lerNl opprK ge_floor. Qed. diff --git a/theories/topology.v b/theories/topology.v index 565e0721e..efd4dd126 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -2282,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 (`|Num.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.