Skip to content

Commit

Permalink
Tidy some proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
pi8027 committed Jul 11, 2024
1 parent 8bd8a06 commit b3c183c
Show file tree
Hide file tree
Showing 11 changed files with 83 additions and 106 deletions.
52 changes: 22 additions & 30 deletions classical/mathcomp_extra.v
Original file line number Diff line number Diff line change
Expand Up @@ -388,64 +388,56 @@ Context {R : archiDomainType}.
Implicit Type x : R.

Lemma ge_floor x : (Num.floor x)%:~R <= x.
Proof. by rewrite Num.Theory.ge_floor. Qed.
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 -Num.Theory.floor_ge_int. Qed.
Proof. by rewrite -floor_ge_int. Qed.

Lemma floor_le0 x : x <= 0 -> Num.floor x <= 0.
Proof. by move/Num.Theory.floor_le; rewrite Num.Theory.floor0. Qed.

Lemma floor_lt0 x : x < 0 -> Num.floor x < 0.
Proof. by move=> x0; rewrite -(@ltrz0 R) (le_lt_trans (ge_floor _)). Qed.
Proof. by rewrite -floor_lt_int. Qed.

Lemma lt_succ_floor x : x < (Num.floor x + 1)%:~R.
Proof. by rewrite Num.Theory.lt_succ_floor. Qed.
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.floor_def _ _ n%:~R)// intr1 !mulrz_nat lexx/= ltr_nat addn1.
Qed.

Lemma floor_ge_int x (z : int) : (z%:~R <= x) = (z <= Num.floor x).
Proof. by rewrite Num.Theory.floor_ge_int. Qed.
Proof. by rewrite (Num.Theory.intrKfloor n) intz. Qed.

Lemma floor_neq0 x : (Num.floor x != 0) = (x < 0) || (x >= 1).
Proof.
apply/idP/orP => [|[x0|/Num.Theory.floor_le r1]]; first rewrite neq_lt => /orP[x0|x0].
- by left; apply: contra_lt x0; rewrite -floor_ge_int.
- by right; rewrite (le_trans _ (ge_floor _))// ler1z -gtz0_ge1.
- by rewrite lt_eqF//; apply: contra_lt x0; rewrite -floor_ge_int.
- by rewrite gt_eqF// (lt_le_trans _ r1)// Num.Theory.floor1.
Qed.

Lemma floor_lt_int x (z : int) : (x < z%:~R) = (Num.floor x < z).
Proof. by rewrite ltNge Num.Theory.floor_ge_int// -ltNge. Qed.
Proof. by rewrite neq_lt -floor_lt_int gtz0_ge1 -floor_ge_int. Qed.

Lemma ceil_ge x : x <= (Num.ceil x)%:~R.
Proof. by rewrite Num.Theory.le_ceil. Qed.
Proof. exact: Num.Theory.le_ceil. Qed.

Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z).
Proof. exact: Num.Theory.ceil_le_int. Qed.

Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x).
Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed.

Lemma ceil_ge0 x : 0 <= x -> 0 <= Num.ceil x.
Proof. by move/(ge_trans (ceil_ge x)); rewrite -(ler_int R). Qed.

Lemma ceil_gt0 x : 0 < x -> 0 < Num.ceil x.
Proof. by move=> ?; rewrite oppr_gt0 floor_lt0 // ltrNl oppr0. Qed.
Proof. by rewrite -ceil_lt_int. Qed.

Lemma ceil_le0 x : x <= 0 -> Num.ceil x <= 0.
Proof. by move=> x0; rewrite -lerNl oppr0 floor_ge0 -lerNr oppr0. Qed.

Lemma ceil_ge_int x (z : int) : (x <= z%:~R) = (Num.ceil x <= z).
Proof. by rewrite Num.Theory.ceil_le_int. Qed.

Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < Num.ceil x).
Proof. by rewrite ltNge ceil_ge_int -ltNge. Qed.
Proof. by rewrite -ceil_ge_int. Qed.

Lemma ceilN x : Num.ceil (- x) = - Num.floor x.
Proof. by rewrite /Num.ceil opprK. Qed.

Lemma abs_ceil_ge x : `|x| <= `|Num.ceil x|.+1%:R.
Proof.
rewrite -natr1 natr_absz; have [x0|x0] := ltP 0%R x.
rewrite -natr1 natr_absz; have [x0|x0] := ltP 0 x.
by rewrite !gtr0_norm ?ceil_gt0// (le_trans (ceil_ge _))// lerDl.
by rewrite !ler0_norm ?ceil_le0// opprK intr1 ltW// lt_succ_floor.
Qed.
Expand Down
18 changes: 8 additions & 10 deletions theories/altreals/realsum.v
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
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.
Expand All @@ -15,6 +15,7 @@ Unset Printing Implicit Defensive.
Unset SsrOldRewriteGoalsOrder.

Import Order.TTheory GRing.Theory Num.Theory.
Require Import mathcomp_extra.

Local Open Scope fset_scope.
Local Open Scope ring_scope.
Expand Down Expand Up @@ -141,11 +142,9 @@ 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 (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 intr1 mathcomp_extra.lt_succ_floor.
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.
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.
Expand All @@ -157,10 +156,9 @@ 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_floor M; rewrite -addn1.
by rewrite natrD /= mulr1n pmulrn -{1}[Num.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 rewrite pmulrn -addn1 PoszD gez0_abs ?floor_ge0// lt_succ_floor.
Qed.

End SummableCountable.
Expand Down
10 changes: 5 additions & 5 deletions theories/ereal.v
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
(* -------------------------------------------------------------------- *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
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.
Expand Down Expand Up @@ -55,6 +55,7 @@ Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Theory.
Import numFieldTopology.Exports.
Require Import mathcomp_extra.

Local Open Scope ring_scope.

Expand Down Expand Up @@ -1406,20 +1407,19 @@ case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 firs
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.
apply; rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor _))// Nfloor.
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.
apply; rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor _))// Nfloor.
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.
rewrite (lt_le_trans (mathcomp_extra.lt_succ_floor _))// Nfloor.
by rewrite !natr1 mulrz_nat ler_nat.
by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor !natr1 mulrz_nat ler_nat.
Qed.
29 changes: 12 additions & 17 deletions theories/lebesgue_integral.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -83,6 +83,7 @@ Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Require Import mathcomp_extra.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Expand Down Expand Up @@ -1288,20 +1289,14 @@ Lemma bigsetU_dyadic_itv n : `[n%:R, n.+1%:R[%classic =
Proof.
rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
- rewrite -bigcup_seq /=; exists `|floor (r * 2 ^+ n.+1)|%N.
rewrite /= mem_index_iota; apply/andP; split.
rewrite -ltez_nat gez0_abs ?floor_ge0; last first.
by rewrite mulr_ge0// (le_trans _ nr).
apply: (@le_trans _ _ (floor (n * 2 ^ n.+1)%:R)); last first.
by apply: floor_le; rewrite natrM natrX ler_pM2r.
by rewrite -floor_ge_int.
rewrite -ltz_nat gez0_abs; last first.
by rewrite floor_ge0 mulr_ge0// (le_trans _ nr).
rewrite -(@ltr_int R) (le_lt_trans (ge_floor _)) ?num_real//.
by rewrite PoszM intrM -natrX ltr_pM2r.
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 _)) ?num_real//.
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 (mathcomp_extra.lt_succ_floor _))//.
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].
Expand Down Expand Up @@ -1432,15 +1427,15 @@ rewrite notin_setE /B /setI /= => /not_andP[] // /negP.
rewrite -ltNge => fxn _.
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 _)) ?num_real// PoszM intrM.
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 _ (ge_floor _)) ?num_real//.
rewrite ler_pdivrMr// (le_trans _ (ge_floor _))//.
by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// ltW.
rewrite ltr_pdivlMr// (lt_le_trans (mathcomp_extra.lt_succ_floor _))//.
rewrite ltr_pdivlMr// (lt_le_trans (lt_succ_floor _))//.
rewrite -[in leRHS]natr1 -intr1 lerD2r// -{1}(@gez0_abs (floor _))//.
by rewrite floor_ge0// mulr_ge0// ltW.
rewrite mulf_eq0// -exprVn; apply/negP; rewrite negb_or expf_neq0//= andbT.
Expand Down Expand Up @@ -1543,7 +1538,7 @@ have : fine (f x) < n%:R.
rewrite -(@ler_nat R); apply: lt_le_trans.
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 intr1 mathcomp_extra.lt_succ_floor.
by rewrite intr1 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.
Expand Down
10 changes: 5 additions & 5 deletions theories/lebesgue_measure.v
Original file line number Diff line number Diff line change
Expand Up @@ -1155,10 +1155,10 @@ rewrite [X in measurable X](_ : _ =
exact: emeasurable_fun_infty_c].
rewrite predeqE => t; split => [/= [Dt ft]|].
have [ft0|ft0] := leP 0%R (fine (f t)).
exists `|(ceil (fine (f t)))%real|%N => //=; split => //; split.
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.
exists `|(floor (fine (f t)))%real|%N => //=; split => //; split.
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 ge_floor// ?num_real.
by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)).
Expand Down Expand Up @@ -1403,7 +1403,7 @@ Lemma eset1Ny :
Proof.
rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr.
move=> [r|/(_ O Logic.I)|]//.
move=> /(_ `|(floor r)%real|%N Logic.I); rewrite /= in_itv/= ltNge.
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.
Expand All @@ -1414,7 +1414,7 @@ Qed.
Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R).
Proof.
rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry.
move=> [r| |/(_ O Logic.I)] // /(_ `|(ceil r)%real|%N Logic.I); rewrite /= in_itv /=.
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.
Expand Down Expand Up @@ -2400,7 +2400,7 @@ have {}EBr2 : \esum_(i in E) mu (closure (B i)) <=
by apply: bigcup_measurable => *; exact: measurable_closure.
have finite_set_F i : finite_set (F i).
apply: contrapT.
pose M := `|(ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R)))%real|.+1.
pose M := `|ceil ((r%:num + 2) *+ 2 / (1 / (2 ^ i.+1)%:R))|.+1.
move/(infinite_set_fset M) => [/= C] CsubFi McardC.
have MC : (M%:R * (1 / (2 ^ i.+1)%:R))%:E <=
mu (\bigcup_(j in [set` C]) closure (B j)).
Expand Down
4 changes: 2 additions & 2 deletions theories/lebesgue_stieltjes_measure.v
Original file line number Diff line number Diff line change
Expand Up @@ -482,9 +482,9 @@ Lemma wlength_sigma_finite (f : R -> R) :
Proof.
exists (fun k => `](- k%:R), k%:R]%classic).
apply/esym; rewrite -subTset => /= x _ /=.
exists `|((floor `|x|%R)%real + 1)%R|%N; rewrite //= in_itv/=.
exists `|(floor `|x| + 1)%R|%N; rewrite //= in_itv/=.
rewrite !natr_absz intr_norm intrD.
suff: `|x| < `|(floor `|x|)%real%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->].
suff: `|x| < `|(floor `|x|)%:~R + 1| by rewrite ltr_norml => /andP[-> /ltW->].
rewrite [ltRHS]ger0_norm//.
by rewrite intr1 (le_lt_trans _ (lt_succ_floor _))// ?ler_norm.
by rewrite addr_ge0// ler0z floor_ge0.
Expand Down
5 changes: 3 additions & 2 deletions theories/normedtype.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -146,6 +146,7 @@ Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Require Import mathcomp_extra.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Expand Down Expand Up @@ -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// mathcomp_extra.ge_floor.
by rewrite natr_absz// ger0_norm// ge_floor.
Qed.

Lemma cover_vitali_collection_partition :
Expand Down
10 changes: 5 additions & 5 deletions theories/real_interval.v
Original file line number Diff line number Diff line change
@@ -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 fingroup perm rat archimedean finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
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.
Expand All @@ -14,6 +14,7 @@ Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Require Import mathcomp_extra.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Expand Down Expand Up @@ -176,8 +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.
rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW//.
by rewrite intr1 mathcomp_extra.lt_succ_floor.
by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 1?ltW// intr1 lt_succ_floor.
Qed.

Lemma itv_o_inftyEbigcup x :
Expand Down Expand Up @@ -344,7 +344,7 @@ move fxE : (f x) => fx; case: fx fxE => [fx fxE gxE|fxoo gxE _|//]; last first.
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 rewrite intr1 ltW// mathcomp_extra.lt_succ_floor.
- by rewrite intr1 ltW// lt_succ_floor.
- by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW.
- by rewrite posrE invr_gt0.
Qed.
Expand All @@ -367,7 +367,7 @@ apply/ler_addgt0Pl => e e_gt0; rewrite -lerBlDl ltW//.
have := rx `|floor e^-1|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
rewrite lerD2l lerN2 -lef_pV2 ?invrK//; last by rewrite posrE.
rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW//.
by rewrite intr1 mathcomp_extra.lt_succ_floor.
by rewrite intr1 lt_succ_floor.
Qed.

Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :
Expand Down
Loading

0 comments on commit b3c183c

Please sign in to comment.