Skip to content

minor generalization #1461

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

Merged
affeldt-aist merged 2 commits into from
Jan 31, 2025
Merged

minor generalization #1461

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
00d150f
minor generalization
affeldt-aist Jan 31, 2025
a61cddc
fix
affeldt-aist Jan 31, 2025
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
3 changes: 3 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,9 @@
- in `normedtype.v`:
+ lemmas `not_near_at_rightP`, `not_near_at_leftP`

- in `Rstruct.v`:
+ lemma `RsqrtE`

### Deprecated

### Removed
Expand Down
5 changes: 2 additions & 3 deletions analysis_stdlib/showcase/uniform_bigO.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,7 @@ Definition OuPex (f : A -> R * R -> R^o) (g : R * R -> R^o) :=
Lemma ler_norm2 (x : normedR2) :
`|x| <= sqrt (Rsqr (fst x) + Rsqr (snd x)) <= Num.sqrt 2 * `|x|.
Proof.
rewrite RsqrtE; last by rewrite addr_ge0 //; apply/RleP/Rle_0_sqr.
rewrite !Rsqr_pow2 !RpowE; apply/andP; split.
rewrite RsqrtE !Rsqr_pow2 !RpowE; apply/andP; split.
by rewrite ge_max; apply/andP; split;
rewrite -[`|_|]sqrtr_sqr ler_wsqrtr // (lerDl, lerDr) sqr_ge0.
wlog lex12 : x / (`|x.1| <= `|x.2|).
Expand Down Expand Up @@ -79,7 +78,7 @@ Qed.

Definition OuO (f : A -> R * R -> R^o) (g : R * R -> R^o) :=
(fun x => f x.1 x.2) =O_ (filter_prod [set setT]%classic
(within P (nbhs (0%R:R^o,0%R:R^o))(*[filter of 0 : R^o * R^o]*))) (fun x => g x.2).
(within P (nbhs (0%R:R^o, 0%R:R^o))(*[filter of 0 : R^o * R^o]*))) (fun x => g x.2).

Lemma OuP_to_O f g : OuP f g -> OuO f g.
Proof.
Expand Down
12 changes: 11 additions & 1 deletion reals_stdlib/Rstruct.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -477,13 +477,23 @@ Proof. elim: n => // n IH; by rewrite S_INR IH RplusE -addn1 natrD. Qed.
Lemma IZRposE (p : positive) : IZR (Z.pos p) = INR (nat_of_pos p).
Proof. by rewrite -Pos_to_natE INR_IPR. Qed.

Lemma RsqrtE x : 0 <= x -> sqrt x = Num.sqrt x.
Let ge0_RsqrtE x : 0 <= x -> sqrt x = Num.sqrt x.
Proof.
move => x0; apply/eqP; have [t1 t2] := conj (sqrtr_ge0 x) (sqrt_pos x).
rewrite eq_sym -(eqrXn2 (_: 0 < 2)%N t1) //; last exact/RleP.
by rewrite sqr_sqrtr // !exprS expr0 mulr1 -RmultE ?sqrt_sqrt //; exact/RleP.
Qed.

Lemma RsqrtE x : sqrt x = Num.sqrt x.
Proof.
set Rx := Rbasic_fun.Rcase_abs x.
have RxE : Rx = Rbasic_fun.Rcase_abs x by [].
rewrite /R_sqrt.sqrt -RxE.
move: RxE; case: Rbasic_fun.Rcase_abs => x0 RxE.
by rewrite RxE ler0_sqrtr//; exact/ltW/RltP.
by rewrite /Rx -/(R_sqrt.sqrt _) ge0_RsqrtE //; exact/RleP/Rge_le.
Qed.

Lemma RpowE x n : pow x n = x ^+ n.
Proof. by elim: n => [ | n In] //=; rewrite exprS In RmultE. Qed.

Expand Down