Skip to content

Remove abs_ceil_ge #1818

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
pi8027 wants to merge 1 commit into
base: master
Choose a base branch
from
+15 −30
Open

Remove abs_ceil_ge #1818

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 0 additions & 14 deletions classical/unstable.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -395,20 +395,6 @@ Proof. by rewrite intrD. Qed.
Lemma intr1D {R : pzRingType} (i : int) : 1 + i%:~R = (1 + i)%:~R :> R.
Proof. by rewrite intrD. Qed.

Section trunc_floor_ceil.
Context {R : archiRealDomainType}.
Implicit Type x : R.

(* PR in progress: https://github.com/math-comp/math-comp/pull/1515 *)
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.ceil_ge _))// lerDl.
by rewrite !ler0_norm ?ceil_le0// ?ceilNfloor opprK intrD1 ltW// floorD1_gt.
Qed.

End trunc_floor_ceil.

Section bijection_forall.

Lemma bij_forall A B (f : A -> B) (P : B -> Prop) :
Expand Down
14 changes: 7 additions & 7 deletions theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1076,21 +1076,21 @@ have fE y k r : (ball 0%R k.+1%:R) y -> (r < 1)%R ->
rewrite (lt_le_trans xrt)// lerBlDl (le_trans (ltW r1))//.
rewrite -lerBlDl addrC -lerBrDr (le_trans (ler_norm _))// normrN.
by rewrite (le_trans (ltW yk1))// lerBrDr natr1 ler_nat -muln2 ltn_Pmulr.
have := h `|ceil x|.+1%N Logic.I.
have Bxx : B `|ceil x|.+1 x.
rewrite /B /ball/= sub0r normrN (le_lt_trans (unstable.abs_ceil_ge _))// ltr_nat.
by rewrite -addnn addSnnS ltn_addl.
have := h (truncn `|x|) Logic.I.
have Bxx : B (truncn `|x|) x.
rewrite /B /ball/= sub0r normrN doubleS -truncn_le_nat.
Copy link
Member Author

@pi8027 pi8027 Jan 7, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps, one thing you missed was the lemmas for going back and forth between inequations over reals and integers (including nat), e.g., truncn_le_nat, floor_ge_int, and floor_lt_int.

Ideally, this kind of proof should be fully automated, since mixed real-integer linear arithmetic (with floor, ceil, and truncn) is decidable.

by rewrite -addnn -addnS leq_addr.
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 `|ceil x|.+1 y - fk `|ceil x|.+1 x|%:E.
\int[mu]_(y in ball x t) `|fk (truncn `|x|) y - fk (truncn `|x|) x|%:E.
near=> t.
apply: eq_integral => /= y /[1!inE] xty.
rewrite -(fE x _ t)//; last first.
by rewrite /ball/= sub0r normrN (le_lt_trans (unstable.abs_ceil_ge _))// ltr_nat.
by rewrite /ball/= sub0r normrN -truncn_le_nat.
rewrite -(fE x _ t)//; last first.
by apply: ballxx; near: t; exact: nbhs_right_gt.
by rewrite /ball/= sub0r normrN (le_lt_trans (unstable.abs_ceil_ge _))// ltr_nat.
by rewrite /ball/= sub0r normrN -truncn_le_nat.
apply/fine_cvgP; split=> [{davg_fk0}|{davg_fk_fin_num}].
- move: davg_fk_fin_num => -[M /= M0] davg_fk_fin_num.
apply: filter_app f_fk_ceil; near=> t => Ht.
Expand Down
17 changes: 8 additions & 9 deletions theories/normedtype_theory/num_normedtype.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -560,9 +560,9 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split.
by exists (truncn (z - a)); rewrite zFan// -ltrBlDl truncnS_gt.
by exists i => //=; rewrite in_itv/= yFa (lt_le_trans _ Fany).
- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa].
exists `|ceil (F (a + n.+1%:R) - F a)%R|.+1 => //=.
rewrite in_itv/= zFa andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//.
by rewrite ler_normr orbC opprB lerB// ltW.
exists (truncn (F a - F (a + n.+1%:R))).+1 => //=.
rewrite in_itv/= zFa andbT lerBlDr -lerBlDl ltW//.
by rewrite -truncn_le_nat le_truncn// lerB// ltW.
Qed.

Lemma decreasing_itvoo_bigcup F a n :
Expand All @@ -586,14 +586,13 @@ move=> dF nyF; rewrite itvNy_bnd_bigcup_BLeft eqEsubset; split.
- move=> y/= [n _]/=; rewrite in_itv/= => /andP[Fany yFa].
have [i iFan] : exists i, F (a - i.+1%:R) < F a - n%:R.
move/cvgrNy_lt : nyF => /(_ (F a - n%:R))[z [zreal zFan]].
exists `|ceil (a - z)|%N.
rewrite zFan// ltrBlDr -ltrBlDl (le_lt_trans (ceil_ge _)) ?num_real//.
by rewrite (le_lt_trans (ler_norm _))// -natr1 -intr_norm ltrDl.
exists (truncn (a - z)).
by rewrite zFan// ltrBlDr -ltrBlDl -truncn_le_nat.
by exists i => //=; rewrite in_itv/= yFa andbT (lt_le_trans _ Fany).
- move=> z/= [n _ /=]; rewrite in_itv/= => /andP[Fanz zFa].
exists `|ceil (F (a - n.+1%:R) - F a)|.+1 => //=.
rewrite in_itv/= zFa andbT lerBlDr -lerBlDl (le_trans _ (abs_ceil_ge _))//.
by rewrite ler_normr orbC opprB lerB// ltW.
exists (truncn (F a - F (a - n.+1%:R))).+1 => //=.
rewrite in_itv/= zFa andbT lerBlDr -lerBlDl ltW//.
by rewrite -truncn_le_nat le_truncn// lerB// ltW.
Qed.

Lemma increasing_itvoc_bigcup F a n :
Expand Down