diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c676bc2941..253eb2e83d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -52,6 +52,9 @@ + global instance `is_derive_exp` + lemma `derive1_shift` +- in `Rstruct_topology.v`: + + lemmas `RcosE`, `Rtrigo_PIE`, `RsinE` + ### Changed - in `derive.v`: @@ -69,6 +72,9 @@ - moved from `realfun.v` to `derive.v`: + lemmas `is_deriveV`, `is_derive1_comp` +- in `Rstruct_topology.v`: + + lemma `RealsE` to include `RcosE`, `Rtrigo_PIE`, `RsinE` + ### Renamed - in `esum.v`: diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index 2fa87fe480..43d477f980 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -9,13 +9,18 @@ From Stdlib Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def From Stdlib Require Import Rtrigo1 Reals. From HB Require Import structures. From mathcomp Require Import boot order ssralg ssrnum archimedean. +From mathcomp Require Import interval arithmetic_tactic. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets reals interval_inference. From mathcomp Require Export Rstruct. From mathcomp Require Import topology. -(* The following line is for RexpE. *) +(* The following line is for RexpE and RcosE. *) From mathcomp Require normedtype sequences. (* The following line is for RlnE. *) From mathcomp Require exp. +(* The following line is for RcosE, PIE and RsinE. *) +From mathcomp Require trigonometry_functions. Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. @@ -120,5 +125,89 @@ case: (Rlt_dec 0 x) => [/= ? | /RltP/[!xgt0]//]. by case: ln_exists => y ->; rewrite RexpE exp.expRK. Qed. +Module RtrigoE. +Import normedtype sequences trigonometry_functions. +Local Open Scope classical_set_scope. + +Lemma RcosE (x : R) : Rtrigo_def.cos x = cos x. +Proof. +apply/esym; rewrite /Rtrigo_def.cos. +case: exist_cos => y. +rewrite /cos_in /cos_n /infinite_sum/=. +set G : nat -> R^o := (G in sum_f_R0 G). +move=> cos_ub. +have Gy : series G x @[x --> \oo] --> y. + rewrite -cvg_shiftS/=; apply/cvgrPdist_lt => /= e /RltP /cos_ub[N Ncos_ub]. + near=> n. + have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge. + move: Ncos_ub => /(_ _ nN) /[!RdistE] /RltP /=. + by rewrite /G distrC sum_f_R0E. +rewrite cosE /series/=; apply: (@cvg_lim R^o) => //. +evar (F : nat -> R); rewrite [X in fmap X](_ : _ = fun n => F n.+1). + apply: funext => n. + under eq_bigr do rewrite -dvdn2 -!mulrA mulr_natl mulrb. + rewrite -big_mkcond/=. + rewrite big_nat_dvdn. + rewrite addn1. + pattern n.+1; rewrite [EQ in EQ n.+1]lock. + have : forall f g, f = g -> forall y, locked (fun x => f x = g x) y. + by move=> ? ? ? ? ->; rewrite -lock. + by apply; unlock; rewrite {}/F; reflexivity. +rewrite -/(mk_sequence F) cvg_shiftS/= -[X in _ --> X]/(nbhs y). +have divn2_cofinal : divn^~ 2 @ \oo --> \oo. + move=> N [] n _ nN. + exists (n * 2)%N => // m/=. + have := nN (m %/ 2)%N => /=. + by rewrite leq_divRL. +have := (cvg_comp (divn^~ 2%N) _ divn2_cofinal Gy). +rewrite [X in fmap X](_ : _ = F)//. +apply: funext => n/=. +apply: eq_bigr => i _. +rewrite /G/= plusE addn0 addnn Rsqr_def !RealsE. +by rewrite -expr2 -exprM mul2n doubleK mulrA. +Unshelve. all: by end_near. Qed. + +Section PIE. + +Let pihalf_spec (x : R) := 0 <= x <= 2 /\ cos x = 0. + +Let pihalf_unique (x y : R) : pihalf_spec x -> pihalf_spec y -> x = y. +Proof. +case=> /andP[] x0 x2 cosx0 [] /andP[] y0 y2 cosy0. +apply: cos_inj. +- rewrite in_itv/=; apply/andP; split => //. + by rewrite (le_trans x2)// pi_ge2. +- rewrite in_itv/=; apply/andP; split => //. + by rewrite (le_trans y2)// pi_ge2. +by rewrite cosx0 cosy0. +Qed. + +Let PI2E : PI2 = pi / 2. +Proof. +rewrite /PI2; case: PI_2_aux => x /= [] [] /RleP x78 /RleP x74. +move/Ropp_eq_compat; rewrite Ropp_involutive Ropp_0 RealsE => cosx0. +rewrite pihalfE. +have x_pihalf : pihalf_spec x. + split; [|by rewrite -RcosE]. + rewrite (le_trans _ x78)/= ?RealsE/=; [lra|]. + by rewrite (le_trans x74)// ?RealsE/=; lra. +apply/esym/get_unique => //= y y_pihalf. +exact: pihalf_unique. +Qed. + +Lemma PIE : PI = pi. +Proof. by rewrite /PI PI2E !RealsE/= mulrCA divff// mulr1. Qed. + +End PIE. + +Lemma RsinE (x : R) : Rtrigo_def.sin x = sin x. +Proof. by rewrite sin_cos RcosE PIE !RealsE/= addrC cosDpihalf opprK. Qed. + +End RtrigoE. + +Definition RcosE := RtrigoE.RcosE. +Definition Rtrigo_PIE := RtrigoE.PIE. +Definition RsinE := RtrigoE.RsinE. + (* extend RealsE from Rstruct.v *) -Definition RealsE := (RealsE, RexpE, RlnE). +Definition RealsE := (RealsE, RexpE, RlnE, RcosE, Rtrigo_PIE, RsinE). diff --git a/classical/unstable.v b/classical/unstable.v index 3d634c27c1..47536ebce7 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -9,7 +9,7 @@ From mathcomp Require Import vector archimedean interval matrix. (* This files contains lemmas that should eventually be backported *) (* to mathcomp. These lemmas may change before being backported to mathcomp, *) (* don't use anything in this file outside of Analysis. For this same reason, *) -(* nothing in this file should be mentionned in the changelog. *) +(* nothing in this file should be mentioned in the changelog. *) (* Once a result is backported to mathcomp, please move it to mathcomp_extra.v*) (* and mention it in the changelog. *) (* *) @@ -647,3 +647,39 @@ End Theory. Module Import Exports. HB.reexport. End Exports. End Norm. Export Norm.Exports. + +(* PR to mathcomp in progress (#1637) *) +Section big_nat_dvdn. + +Lemma iotaS (m n : nat) : iota m n.+1 = rcons (iota m n) (m + n)%N. +Proof. by rewrite -addn1 iotaD cats1. Qed. + +Lemma index_iotaS (m n : nat) : + (m <= n)%N -> index_iota m n.+1 = rcons (index_iota m n) n. +Proof. by move=> ?; rewrite /index_iota subSn// iotaS subnKC. Qed. + +Lemma big_nat_recr_op (R : Type) (idx : R) (op : R -> R -> R) + (n m : nat) (P : pred nat) (F : nat -> R) : + (m <= n)%N -> + let idx' := if P n then op (F n) idx else idx in + \big[op/idx]_(m <= i < n.+1 | P i) F i = \big[op/idx']_(m <= i < n | P i) F i. +Proof. by move=> ?; rewrite index_iotaS// big_rcons_op. Qed. + +Lemma big_nat_dvdn (R : Type) (idx : R) (op : R -> R -> R) + (n d : nat) (F : nat -> R) : + \big[op/idx]_(0 <= i < n | d.+1 %| i) F i = + \big[op/idx]_(0 <= i < (n + d) %/ d.+1) F (d.+1 * i)%N. +Proof. +elim: n idx. + by move=> ?; rewrite divn_small// !big_nil. +move=> n IHn idx. +rewrite addSn divnS// -addnS dvdn_addl// big_nat_recr_op// IHn. +case/boolP: (d.+1 %| n) => H /=. + rewrite add1n big_nat_recr_op//. + rewrite divnDl// (@divn_small d)// addn0. + congr bigop.body; congr op; congr F. + by rewrite muln_divCA// divnn muln1. +by rewrite add0n. +Qed. + +End big_nat_dvdn.