diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1d0c8f12e..cbd2e0561 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,7 +13,7 @@ + lemma `EFinB` + lemmas `mule_eq0`, `mule_lt0_lt0`, `mule_gt0_lt0`, `mule_lt0_gt0`, `pmule_rge0`, `pmule_lge0`, `nmule_lge0`, `nmule_rge0`, - `pmule_rgt0`, `pmule_lgt0`, `nmule_lgt0`, `nmule_rgt0`, + `pmule_rgt0`, `pmule_lgt0`, `nmule_lgt0`, `nmule_rgt0` - in `measure.v`: + hints for `measurable0` and `measurableT` - in `ereal.v`: @@ -21,6 +21,94 @@ + lemma `eqe_absl` + lemma `lee_pmul` + lemmas `cover_restr`, `eqcover_r` +- in `topology.v` : + + lemmas `cstE`, `compE`, `opprfunE`, `addrfunE`, `mulrfunE`, `scalrfunE`, `exprfunE` + + multi-rule `fctE` +- in `normedtype.v` + + lemmas `continuous_shift`, `continuous_withinNshiftx` +- in `derive.v` + + lemmas `derive1_comp`, `derivable_cst`, `derivable_id`, trigger_derive` + + instances `is_derive_id`, `is_derive_Nid` +- in `sequences.v`: + + lemmas `cvg_series_bounded`, `cvg_to_0_linear`, `lim_cvg_to_0_linear`. + + lemma `cvg_sub0` + + lemma `cvg_zero` +- file `realfun.v`: + + lemma `is_derive1_caratheodory`, `is_derive_0_is_cst` + + instance `is_derive1_comp` + + lemmas `is_deriveV`, `is_derive_inverse` +- new file `nsatz_realType` +- new file `exp.v` + + lemma `normr_nneg` (hint) + + definitions `pseries`, `pseries_diffs` + + facts `is_cvg_pseries_inside_norm`, `is_cvg_pseries_inside` + + lemmas `pseries_diffsN`, `pseries_diffs_inv_fact`, `pseries_diffs_sumE`, + `pseries_diffs_equiv`, `is_cvg_pseries_diffs_equiv`, + `pseries_snd_diffs` + + lemmas `expR0`, `expR_ge1Dx`, `exp_coeffE`, `expRE` + + instance `is_derive_expR` + + lemmas `derivable_expR`, `continuous_expR`, `expRxDyMexpx`, `expRxMexpNx_1` + + lemmas `pexpR_gt1`, `expR_gt0`, `expRN`, `expRD`, `expRMm` + + lemmas `expR_gt1`, `expR_lt1`, `expRB`, `ltr_expR`, `ler_expR`, `expR_inj`, + `expR_total_gt1`, `expR_total` + + definition `ln` + + fact `ln0` + + lemmas `expK`, `lnK`, `ln1`, `lnM`, `ln_inj`, `lnV`, `ln_div`, `ltr_ln`, `ler_ln`, `lnX` + + lemmas `le_ln1Dx`, `ln_sublinear`, `ln_ge0`, `ln_gt0` + + lemma `continuous_ln` + + instance `is_derive1_ln` + + definition `exp_fun`, notation `` `^ `` + + lemmas `exp_fun_gt0`, `exp_funr1`, `exp_funr0`, `exp_fun1`, `ler_exp_fun`, + `exp_funD`, `exp_fun_inv`, `exp_fun_mulrn` + + definition `riemannR`, lemmas `riemannR_gt0`, `dvg_riemannR` +- new file `trigo.v` + + lemmas `sqrtvR`, `eqr_div`, `big_nat_mul`, `cvg_series_cvg_series_group`, + `lt_sum_lim_series` + + definitions `periodic`, `alternating` + + lemmas `periodicn`, `alternatingn` + + definition `sin_coeff` + + lemmas `sin_coeffE`, `sin_coeff_even`, `is_cvg_series_sin_coeff` + + definition `sin` + + lemmas `sinE` + + definition `sin_coeff'` + + lemmas `sin_coeff'E`, `cvg_sin_coeff'`, `diffs_sin`, `series_sin_coeff0`, `sin0` + + definition `cos_coeff` + + lemmas `cos_ceff_2_0`, `cos_coeff_2_2`, `cos_coeff_2_4`, `cos_coeffE`, `is_cvg_series_cos_coeff` + + definition `cos` + + lemma `cosE` + + definition `cos_coeff'` + + lemmas `cos_coeff'E`, `cvg_cos_coeff'`, `diffs_cos`, `series_cos_coeff0`, `cos0` + + instance `is_derive_sin` + + lemmas `derivable_sin`, `continuous_sin`, `is_derive_cos`, `derivable_cos`, `continuous_cos` + + lemmas `cos2Dsin2`, `cos_max`, `cos_geN1`, `cos_le1`, `sin_max`, `sin_geN1`, `sin_le1` + + fact `sinD_cosD` + + lemmas `sinD`, `cosD` + + lemmas `sin2cos2`, `cos2sin2`, `sin_mulr2n`, `cos_mulr2n` + + fact `sinN_cosN` + + lemmas `sinN`, `cosN` + + lemmas `sin_sg`, `cos_sg`, `cosB`, `sinB` + + lemmas `norm_cos_eq1`, `norm_sin_eq1`, `cos1sin0`, `sin0cos1`, `cos_norm` + + definition `pi` + + lemmas `pihalfE`, `cos2_lt0`, `cos_exists` + + lemmas `sin2_gt0`, `cos_pihalf_uniq`, `pihalf_02_cos_pihalf`, `pihalf_02`, `pi_gt0`, `pi_ge0` + + lemmas `sin_gt0_pihalf`, `cos_gt0_pihalf`, `cos_pihalf`, `sin_pihalf`, `cos_ge0_pihalf`, `cospi`, `sinpi` + + lemmas `cos2pi`, `sin2pi`, `sinDpi`, `cosDpi`, `sinD2pi`, `cosD2pi` + + lemmas `cosDpihalf`, `cosBpihalf`, `sinDpihalf`, `sinBpihalf`, `sin_ge0_pi` + + lemmas `ltr_cos`, `ltr_sin`, `cos_inj`, `sin_inj` + + definition `tan` + + lemmas `tan0`, `tanpi`, `tanN`, `tanD`, `tan_mulr2n`, `cos2_tan2` + + lemmas `tan_pihalf`, `tan_piquarter`, `tanDpi`, `continuous_tan` + + lemmas `is_derive_tan`, `derivable_tan`, `ltr_tan`, `tan_inj` + + definition `acos` + + lemmas `acos_def`, `acos_ge0`, `acos_lepi`, `acosK`, `acos_gt0`, `acos_ltpi` + + lemmas `cosK`, `sin_acos`, `near_lift`, `continuous_acos`, `is_derive1_acos` + + definition `asin` + + lemmas `asin_def`, `asin_geNpi2`, `asin_lepi2`, `asinK`, `asin_ltpi2`, `asin_gtNpi2` + + lemmas `sinK`, `cos_asin`, `continuous_asin`, `is_derive1_asin` + + definition `atan` + + lemmas `atan_def`, `atan_gtNpi2`, `atan_ltpi2`, `atanK`, `tanK` + + lemmas `continuous_atan`, `cos_atan` + + instance `is_derive1_atan` ### Changed diff --git a/_CoqProject b/_CoqProject index 3c33453ab..2ef71010a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -21,6 +21,9 @@ theories/prodnormedzmodule.v theories/normedtype.v theories/realfun.v theories/sequences.v +theories/exp.v +theories/trigo.v +theories/nsatz_realtype.v theories/cardinality.v theories/csum.v theories/forms.v diff --git a/theories/derive.v b/theories/derive.v index 9440a9fff..3a3f5e35e 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -895,17 +895,16 @@ move=> dfx dgx; apply: DiffDef; first exact: differentiable_pair. by rewrite diff_pair // !diff_val. Qed. -Global Instance is_diffM (f g df dg : V -> R) x : +Global Instance is_diffM (f g df dg : V -> R) x : is_diff x f df -> is_diff x g dg -> is_diff x (f * g) (f x *: dg + g x *: df). Proof. move=> dfx dgx. have -> : f * g = (fun p => p.1 * p.2) \o (fun y => (f y, g y)) by []. -(* TODO: type class inference should succeed or fail, not leave an evar *) -apply: is_diff_eq; do ?exact: is_diff_comp. -by rewrite funeqE => ?; rewrite /= [_ * g _]mulrC. +(* TODO: type class inference should succeed or fail, not leave an evar *) +apply: is_diff_eq; do ?exact: is_diff_comp. +by rewrite funeqE => ?; rewrite /= [_ * g _]mulrC. Qed. - Lemma diffM (f g : V -> R) x : differentiable f x -> differentiable g x -> 'd (f * g) x = f x \*: 'd g x + g x \*: 'd f x :> (V -> R). @@ -994,12 +993,6 @@ Proof. by move=> df fxn0; apply: differentiable_comp _ (differentiable_Rinv fxn0). Qed. -Lemma exprfunE (T : pointedType) (K : ringType) (f : T -> K) n : - f ^+ n = (fun x => f x ^+ n). -Proof. -by elim: n => [|n ihn]; rewrite funeqE=> ?; [rewrite !expr0|rewrite !exprS ihn]. -Qed. - Global Instance is_diffX (f df : V -> R) n x : is_diff x f df -> is_diff x (f ^+ n.+1) (n.+1%:R * f x ^+ n *: df). Proof. @@ -1554,3 +1547,41 @@ apply: (@ler0_derive1_nincr _ (- f)) => t tab; first exact/derivableN/fdrvbl. rewrite derive1E deriveN; last exact: fdrvbl. by rewrite oppr_le0 -derive1E; apply: dfge0. Qed. + +Lemma derive1_comp (R : realFieldType) (f g : R -> R) x : + derivable f x 1 -> derivable g (f x) 1 -> + (g \o f)^`() x = g^`() (f x) * f^`() x. +Proof. +move=> /derivable1_diffP df /derivable1_diffP dg. +rewrite derive1E'; last exact/differentiable_comp. +rewrite diff_comp // !derive1E' //= -[X in 'd _ _ X = _]mulr1. +by rewrite [LHS]linearZ mulrC. +Qed. + +Section is_derive_instances. +Variables (R : numFieldType) (V : normedModType R). + +Lemma derivable_cst (x : V) : derivable (fun=> x) 0 1. +Proof. exact/derivable1_diffP/differentiable_cst. Qed. + +Lemma derivable_id (x v : V) : derivable id x v. +Proof. +apply/derivable1P/derivableD; last exact/derivable_cst. +exact/derivable1_diffP/differentiableZl. +Qed. + +Global Instance is_derive_id (x v : V) : is_derive x v id v. +Proof. +apply: (DeriveDef (@derivable_id _ _)). +by rewrite deriveE// (@diff_lin _ _ _ [linear of idfun]). +Qed. + +Global Instance is_deriveNid (x v : V) : is_derive x v -%R (- v). +Proof. by apply: is_deriveN. Qed. + +End is_derive_instances. + +(* Trick to trigger type class resolution *) +Lemma trigger_derive (R : realType) (f : R -> R) x x1 y1 : + is_derive x 1 f x1 -> x1 = y1 -> is_derive x 1 f y1. +Proof. by move=> Hi <-. Qed. diff --git a/theories/exp.v b/theories/exp.v new file mode 100644 index 000000000..d0a6d0fe1 --- /dev/null +++ b/theories/exp.v @@ -0,0 +1,643 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum. +From mathcomp Require Import matrix interval rat. +Require Import boolp reals ereal. +Require Import nsatz_realtype. +Require Import classical_sets posnum topology normedtype landau sequences. +Require Import derive realfun. + +(******************************************************************************) +(* Theory of exponential/logarithm functions *) +(* *) +(* This file defines exponential and logarithm functions and develops their *) +(* theory. *) +(* *) +(* * Differentiability of series (Section PseriesDiff) *) +(* This formalization is inspired by HOL-Light (transc.ml). This part is *) +(* temporary: it should be subsumed by a proper theory of power series. *) +(* pseries f x == [series f n * x ^ n]_n *) +(* pseries_diffs f i == (i + 1) * f (i + 1) *) +(* *) +(* ln x == the natural logarithm *) +(* a `^ x == exponential functions *) +(* riemannR a == sequence n |-> 1 / (n.+1) `^ a where a has a type *) +(* of type realType *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +(* PR to mathcomp in progress *) +Lemma normr_nneg (R : numDomainType) (x : R) : `|x| \is Num.nneg. +Proof. by rewrite qualifE. Qed. +Hint Resolve normr_nneg : core. +(* /PR to mathcomp in progress *) + +Section PseriesDiff. + +Variable R : realType. + +Definition pseries f (x : R) := [series f i * x ^+ i]_i. + +Fact is_cvg_pseries_inside_norm f (x z : R) : + cvg (pseries f x) -> `|z| < `|x| -> cvg (pseries (fun i => `|f i|) z). +Proof. +move=> Cx zLx; have [K [Kreal Kf]] := cvg_series_bounded Cx. +have Kzxn n : 0 <= `|K + 1| * `|z ^+ n| / `|x ^+ n|. + by rewrite !mulr_ge0 ?invr_ge0 // ltW. +apply: normed_cvg. +apply: series_le_cvg Kzxn _ _ => [//=| /= n|]. + rewrite (_ : `|_ * _| = `|f n * x ^+ n| * `|z ^+ n| / `|x ^+ n|); last first. + rewrite !normrM normr_id mulrAC mulfK // normr_eq0 expf_eq0 andbC. + by case: ltrgt0P zLx; rewrite //= normr_lt0. + do! (apply: ler_pmul || apply: mulr_ge0 || rewrite invr_ge0) => //. + by apply Kf => //; rewrite (lt_le_trans _ (ler_norm _))// ltr_addl. +have F : `|z / x| < 1. + by rewrite normrM normfV ltr_pdivr_mulr ?mul1r // (le_lt_trans _ zLx). +rewrite (_ : (fun _ => _) = geometric `|K + 1| `|z / x|); last first. + by apply/funext => i /=; rewrite normrM exprMn mulrA normfV !normrX exprVn. +by apply: is_cvg_geometric_series; rewrite normr_id. +Qed. + +Fact is_cvg_pseries_inside f (x z : R) : + cvg (pseries f x) -> `|z| < `|x| -> cvg (pseries f z). +Proof. +move=> Cx zLx. +apply: normed_cvg; rewrite /normed_series_of /=. +rewrite (_ : (fun _ => _) = (fun i => `|f i| * `|z| ^+ i)); last first. + by apply/funext => i; rewrite normrM normrX. +by apply: is_cvg_pseries_inside_norm Cx _; rewrite normr_id. +Qed. + +Definition pseries_diffs (f : nat -> R) i := i.+1%:R * f i.+1. + +Lemma pseries_diffsN (f : nat -> R) : pseries_diffs (- f) = -(pseries_diffs f). +Proof. by apply/funext => i; rewrite /pseries_diffs /= -mulrN. Qed. + +Lemma pseries_diffs_inv_fact : + pseries_diffs (fun n => (n`!%:R)^-1) = (fun n => (n`!%:R)^-1 : R). +Proof. +apply/funext => i. +by rewrite /pseries_diffs factS natrM invfM mulrA mulfV ?mul1r. +Qed. + +Lemma pseries_diffs_sumE n f x : + \sum_(0 <= i < n) pseries_diffs f i * x ^+ i = + (\sum_(0 <= i < n) i%:R * f i * x ^+ i.-1) + n%:R * f n * x ^+ n.-1. +Proof. +case: n => [|n]; first by rewrite !big_nil !mul0r add0r. +under eq_bigr do unfold pseries_diffs. +by rewrite big_nat_recr //= big_nat_recl //= !mul0r add0r. +Qed. + +Lemma pseries_diffs_equiv f x : + let s i := i%:R * f i * x ^+ i.-1 in + cvg (pseries (pseries_diffs f) x) -> series s --> + lim (pseries (pseries_diffs f) x). +Proof. +move=> s Cx; rewrite -[lim _]subr0 /pseries [X in X --> _]/series /=. +rewrite [X in X --> _](_ : _ = (fun n => \sum_(0 <= i < n) + pseries_diffs f i * x ^+ i - n%:R * f n * x ^+ n.-1)); last first. + by rewrite funeqE => n; rewrite pseries_diffs_sumE addrK. +by apply: cvgB => //; rewrite -cvg_shiftS; exact: cvg_series_cvg_0. +Qed. + +Lemma is_cvg_pseries_diffs_equiv f x : + cvg (pseries (pseries_diffs f) x) -> cvg [series i%:R * f i * x ^+ i.-1]_i. +Proof. +by by move=> Cx; have := pseries_diffs_equiv Cx; move/(cvg_lim _) => -> //. +Qed. + +Let pseries_diffs_P1 m (z h : R) : + \sum_(0 <= i < m) ((h + z) ^+ (m - i) * z ^+ i - z ^+ m) = + \sum_(0 <= i < m) z ^+ i * ((h + z) ^+ (m - i) - z ^+ (m - i)). +Proof. +rewrite !big_mkord; apply: eq_bigr => i _. +by rewrite mulrDr mulrN -exprD mulrC addnC subnK // ltnW. +Qed. + +Let pseries_diffs_P2 n (z h : R) : + h != 0 -> + ((h + z) ^+ n - (z ^+ n)) / h - n%:R * z ^+ n.-1 = + h * \sum_(0 <= i < n.-1) z ^+ i * + \sum_(0 <= j < n.-1 - i) (h + z) ^+ j * z ^+ (n.-2 - i - j). +Proof. +move=> hNZ; apply: (mulfI hNZ). +rewrite mulrBr mulrC divfK //. +case: n => [|n]. + by rewrite !expr0 !(mul0r, mulr0, subr0, subrr, big_geq). +rewrite subrXX addrK -mulrBr; congr (_ * _). +rewrite -(big_mkord xpredT (fun i : nat => (h + z) ^+ (n - i) * z ^+ i)). +rewrite big_nat_recr //= subnn expr0 -addrA -mulrBl. +rewrite -add1n natrD opprD addrA subrr sub0r mulNr. +rewrite mulr_natl -[in X in _ *+ X](subn0 n) -sumr_const_nat -sumrB. +rewrite pseries_diffs_P1 mulr_sumr !big_mkord; apply: eq_bigr => i _. +rewrite mulrCA; congr (_ * _). +rewrite subrXX addrK big_nat_rev /= big_mkord; congr (_ * _). +by apply: eq_bigr => k _; rewrite -!predn_sub subKn // -subnS. +Qed. + +Let pseries_diffs_P3 (z h : R) n K : + h != 0 -> `|z| <= K -> `|h + z| <= K -> + `|((h +z) ^+ n - z ^+ n) / h - n%:R * z ^+ n.-1| + <= n%:R * n.-1%:R * K ^+ n.-2 * `|h|. +Proof. +move=> hNZ zLK zhLk. +rewrite pseries_diffs_P2// normrM mulrC. +rewrite ler_pmul2r ?normr_gt0//. +rewrite (le_trans (ler_norm_sum _ _ _))//. +rewrite -mulrA mulrC -mulrA mulr_natl -[X in _ *+ X]subn0 -sumr_const_nat. +apply ler_sum_nat => i /=. +case: n => //= n ni. +rewrite normrM. +pose d := (n.-1 - i)%nat. +rewrite -[(n - i)%nat]prednK ?subn_gt0// predn_sub -/d. +rewrite -(subnK (_ : i <= n.-1)%nat) -/d; last first. + by rewrite -ltnS prednK// (leq_ltn_trans _ ni). +rewrite addnC exprD mulrAC -mulrA. +apply: ler_pmul => //. + by rewrite normrX ler_expn2r// qualifE (le_trans _ zLK). +apply: le_trans (_ : d.+1%:R * K ^+ d <= _); last first. + rewrite ler_wpmul2r //; first by rewrite exprn_ge0 // (le_trans _ zLK). + by rewrite ler_nat ltnS /d -subn1 -subnDA leq_subr. +rewrite (le_trans (ler_norm_sum _ _ _))//. +rewrite mulr_natl -[X in _ *+ X]subn0 -sumr_const_nat ler_sum_nat//= => j jd1. +rewrite -[in X in _ <= X](subnK (_ : j <= d)%nat) -1?ltnS // addnC exprD normrM. +by rewrite ler_pmul// ?normr_ge0// normrX ler_expn2r// qualifE (le_trans _ zLK). +Qed. + +Lemma pseries_snd_diffs (c : R^nat) K x : + cvg (pseries c K) -> + cvg (pseries (pseries_diffs c) K) -> + cvg (pseries (pseries_diffs (pseries_diffs c)) K) -> + `|x| < `|K| -> + is_derive x 1 + (fun x => lim (pseries c x)) + (lim (pseries (pseries_diffs c) x)). +Proof. +move=> Ck CdK CddK xLK; rewrite /pseries. +set s := (fun n : nat => _); set (f := fun x0 => _). +suff hfxs : h^-1 *: (f (h + x) - f x) @[h --> 0^'] --> lim (series s). + have F : f^`() x = lim (series s) by apply: cvg_lim hfxs. + have Df : derivable f x 1. + move: hfxs; rewrite /derivable [X in X @ _](_ : _ = + (fun h => h^-1 *: (f (h%:A + x) - f x))) /=; last first. + by apply/funext => i //=; rewrite [i%:A]mulr1. + by move=> /(cvg_lim _) -> //. + by constructor; [exact: Df|rewrite -derive1E]. +pose sx := fun n : nat => c n * x ^+ n. +have Csx : cvg (pseries c x) by apply: is_cvg_pseries_inside Ck _. +pose shx := fun h (n : nat) => c n * (h + x) ^+ n. +suff Cc : lim (h^-1 *: (series (shx h - sx))) @[h --> 0^'] --> lim (series s). + apply: cvg_sub0 Cc. + apply/cvg_distP => eps eps_gt0 /=; rewrite !near_simpl /=. + near=> h; rewrite sub0r normrN /=. + rewrite (le_lt_trans _ eps_gt0)//. + rewrite normr_le0 subr_eq0 -/sx -/(shx _); apply/eqP. + have Cshx' : cvg (series (shx h)). + apply: is_cvg_pseries_inside Ck _. + rewrite (le_lt_trans (ler_norm_add _ _))// -(subrK `|x| `|K|) ltr_add2r. + near: h. + apply/nbhs_ballP => /=; exists ((`|K| - `|x|) /2) => /=. + by rewrite divr_gt0 // subr_gt0. + move=> t; rewrite /ball /= sub0r normrN => H tNZ. + rewrite (lt_le_trans H)// ler_pdivr_mulr // mulr2n mulrDr mulr1. + by rewrite ler_paddr // subr_ge0 ltW. + by rewrite limZr; [rewrite lim_seriesB|exact: is_cvg_seriesB]. +apply: cvg_zero => /=. +suff Cc : lim + (series (fun n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1))) + @[h --> 0^'] --> (0 : R). + apply: cvg_sub0 Cc. + apply/cvg_distP => eps eps_gt0 /=. + rewrite !near_simpl /=. + near=> h; rewrite sub0r normrN /=. + rewrite (le_lt_trans _ eps_gt0)// normr_le0 subr_eq0; apply/eqP. + have Cs : cvg (series s) by apply: is_cvg_pseries_inside CdK _. + have Cs1 := is_cvg_pseries_diffs_equiv Cs. + have Fs1 := pseries_diffs_equiv Cs. + set s1 := (fun i => _) in Cs1. + have Cshx : cvg (series (shx h)). + apply: is_cvg_pseries_inside Ck _. + rewrite (le_lt_trans (ler_norm_add _ _))// -(subrK `|x| `|K|) ltr_add2r. + near: h. + apply/nbhs_ballP => /=; exists ((`|K| - `|x|) /2) => /=. + by rewrite divr_gt0 // subr_gt0. + move=> t; rewrite /ball /= sub0r normrN => H tNZ. + rewrite (lt_le_trans H)// ler_pdivr_mulr // mulr2n mulrDr mulr1. + by rewrite ler_paddr // subr_ge0 ltW. + have C1 := is_cvg_seriesB Cshx Csx. + have Ckf := @is_cvg_seriesZ _ _ h^-1 C1. + have Cu : (series (h^-1 *: (shx h - sx)) - series s1) x0 @[x0 --> \oo] --> + lim (series (h^-1 *: (shx h - sx))) - lim (series s). + by apply: cvgB. + set w := (fun n : nat => _ in RHS). + have -> : w = h^-1 *: (shx h - sx) - s1. + apply: funext => i; rewrite !fctE. + rewrite /w /shx /sx /s1 /= mulrBr; congr (_ - _); last first. + by rewrite mulrCA !mulrA. + by rewrite -mulrBr [RHS]mulrCA [_^-1 * _]mulrC. + rewrite [X in X h = _]/+%R /= [X in _ + X h = _]/-%R /=. + have -> : series (h^-1 *: (shx h - sx) - s1) = + series (h^-1 *: (shx h - sx)) - (series s1). + by apply/funext => i; rewrite /series /= sumrB. + have -> : h^-1 *: series (shx h - sx) = series (h^-1 *: (shx h - sx)). + by apply/funext => i; rewrite /series /= -scaler_sumr. + exact/esym/cvg_lim. +pose r := (`|x| + `|K|) / 2. +have xLr : `|x| < r by rewrite ltr_pdivl_mulr // mulr2n mulrDr mulr1 ltr_add2l. +have rLx : r < `|K| by rewrite ltr_pdivr_mulr // mulr2n mulrDr mulr1 ltr_add2r. +have r_gt0 : 0 < r by apply: le_lt_trans xLr. +have rNZ : r != 0by case: ltrgt0P r_gt0. +apply: (@lim_cvg_to_0_linear _ + (fun n => `|c n| * n%:R * (n.-1)%:R * r ^+ n.-2) + (fun h n => c n * (((h + x) ^+ n - x ^+ n) / h - n%:R * x ^+ n.-1)) + (r - `|x|)); first by rewrite subr_gt0. +- have : cvg [series `|pseries_diffs (pseries_diffs c) n| * r ^+ n]_n. + apply: is_cvg_pseries_inside_norm CddK _. + by rewrite ger0_norm // ltW // (le_lt_trans _ xLr). + have -> : (fun n => `|pseries_diffs (pseries_diffs c) n| * r ^+ n) = + (fun n => pseries_diffs (pseries_diffs + (fun m => `|c m|)) n * r ^+ n). + apply/funext => i. + by rewrite /pseries_diffs !normrM !mulrA ger0_norm // ger0_norm. + move=> /is_cvg_pseries_diffs_equiv. + rewrite /pseries_diffs. + have -> : (fun n => n%:R * ((n.+1)%:R * `|c n.+1|) * r ^+ n.-1) = + (fun n => pseries_diffs + (fun m => (m.-1)%:R * `|c m| * r^-1) n * r ^+ n). + apply/funext => n. + rewrite /pseries_diffs /= mulrA. + case: n => [|n /=]; first by rewrite !(mul0r, mulr0). + rewrite [_%:R *_]mulrC !mulrA -[RHS]mulrA exprS. + by rewrite [_^-1 * _]mulrA mulVf ?mul1r. + move/is_cvg_pseries_diffs_equiv. + have ->// : (fun n => n%:R * (n.-1%:R * `|c n| / r) * r ^+ n.-1) = + (fun n => `|c n| * n%:R * n.-1%:R * r ^+ n.-2). + apply/funext => [] [|[|i]]; rewrite ?(mul0r, mulr0) //=. + rewrite mulrA -mulrA exprS [_^-1 * _]mulrA mulVf //. + rewrite mul1r !mulrA; congr (_ * _). + by rewrite mulrC mulrA. +- move=> h /andP[h_gt0 hLrBx] n. + rewrite normrM -!mulrA ler_wpmul2l //. + rewrite (le_trans (pseries_diffs_P3 _ _ (ltW xLr) _))// ?mulrA -?normr_gt0//. + by rewrite (le_trans (ler_norm_add _ _))// -(subrK `|x| r) ler_add2r ltW. +Grab Existential Variables. all: end_near. Qed. + +End PseriesDiff. + +Section expR. +Variable R : realType. +Implicit Types x : R. + +Lemma expR0 : expR 0 = 1 :> R. +Proof. +apply: lim_near_cst => //. +near=> m; rewrite -[m]prednK; last by near: m. +rewrite -addn1 series_addn series_exp_coeff0 big_add1 big1 ?addr0//. +by move=> i _; rewrite /exp_coeff /= expr0n mul0r. +Grab Existential Variables. all: end_near. Qed. + +Lemma expR_ge1Dx x : 0 <= x -> 1 + x <= expR x. +Proof. +move=> x_gt0; rewrite /expR. +pose f (x : R) i := (i == 0%nat)%:R + x *+ (i == 1%nat). +have F n : (1 < n)%nat -> \sum_(0 <= i < n) (f x i) = 1 + x. + move=> /subnK<-. + by rewrite addn2 !big_nat_recl //= /f /= mulr1n !mulr0n big1 ?add0r ?addr0. +have -> : 1 + x = lim (series (f x)). + by apply/esym/lim_near_cst => //; near=> n; apply: F; near: n. +apply: ler_lim; first by apply: is_cvg_near_cst; near=> n; apply: F; near: n. + exact: is_cvg_series_exp_coeff. +by near=> n; apply: ler_sum => [] [|[|i]] _; + rewrite /f /exp_coeff /= !(mulr0n, mulr1n, expr0, expr1, divr1, addr0, add0r) + // exp_coeff_ge0. +Grab Existential Variables. all: end_near. Qed. + +Lemma exp_coeffE x : exp_coeff x = (fun n => (fun n => (n`!%:R)^-1) n * x ^+ n). +Proof. by apply/funext => i; rewrite /exp_coeff /= mulrC. Qed. + +Import GRing.Theory. +Local Open Scope ring_scope. + +Lemma expRE : + expR = fun x => lim (pseries (fun n => (fun n => (n`!%:R)^-1) n) x). +Proof. by apply/funext => x; rewrite /pseries -exp_coeffE. Qed. + +Global Instance is_derive_expR x : is_derive x 1 expR (expR x). +Proof. +pose s1 n := pseries_diffs (fun n => n`!%:R^-1) n * x ^+ n. +rewrite expRE /= /pseries (_ : (fun _ => _) = s1); last first. + by apply/funext => i; rewrite /s1 pseries_diffs_inv_fact. +apply: (@pseries_snd_diffs _ _ (`|x| + 1)); rewrite /pseries. +- by rewrite -exp_coeffE; apply: is_cvg_series_exp_coeff. +- rewrite (_ : (fun _ => _) = exp_coeff (`|x| + 1)). + exact: is_cvg_series_exp_coeff. + by apply/funext => i; rewrite pseries_diffs_inv_fact exp_coeffE. +- rewrite (_ : (fun _ => _) = exp_coeff (`|x| + 1)). + exact: is_cvg_series_exp_coeff. + by apply/funext => i; rewrite !pseries_diffs_inv_fact exp_coeffE. +by rewrite [X in _ < X]ger0_norm ?addr_ge0 // addrC -subr_gt0 addrK. +Qed. + +Lemma derivable_expR x : derivable expR x 1. +Proof. by apply: ex_derive; apply: is_derive_exp. Qed. + +Lemma continuous_expR : continuous (@expR R). +Proof. +by move=> x; exact/differentiable_continuous/derivable1_diffP/derivable_expR. +Qed. + +Lemma expRxDyMexpx x y : expR (x + y) * expR (- x) = expR y. +Proof. +set v := LHS; pattern x in v; move: @v; set f := (X in let _ := X x in _) => /=. +apply: etrans (_ : f x = f 0) _; last by rewrite /f add0r oppr0 expR0 mulr1. +apply: is_derive_0_is_cst => x1. +apply: trigger_derive. +by rewrite /GRing.scale /= mulrN1 addr0 mulr1 mulrN addrC mulrC subrr. +Qed. + +Lemma expRxMexpNx_1 x : expR x * expR (- x) = 1. +Proof. by rewrite -[X in _ X * _ = _]addr0 expRxDyMexpx expR0. Qed. + +Lemma pexpR_gt1 x : 0 < x -> 1 < expR x. +Proof. +by move=> x_gt0; rewrite (lt_le_trans _ (expR_ge1Dx (ltW x_gt0)))// ltr_addl. +Qed. + +Lemma expR_gt0 x : 0 < expR x. +Proof. +case: (ltrgt0P x) => [x_gt0|x_gt0|->]; last by rewrite expR0. +- exact: lt_trans (pexpR_gt1 x_gt0). +- have F : 0 < expR (- x) by rewrite (lt_trans _ (pexpR_gt1 _))// oppr_gt0. + by rewrite -(pmulr_lgt0 _ F) expRxMexpNx_1. +Qed. + +Lemma expRN x : expR (- x) = (expR x)^-1. +Proof. +apply: (mulfI (lt0r_neq0 (expR_gt0 x))). +by rewrite expRxMexpNx_1 mulfV // (lt0r_neq0 (expR_gt0 x)). +Qed. + +Lemma expRD x y : expR (x + y) = expR x * expR y. +Proof. +apply: (mulIf (lt0r_neq0 (expR_gt0 (- x)))). +rewrite expRxDyMexpx expRN [_ * expR y]mulrC mulfK //. +by case: ltrgt0P (expR_gt0 x). +Qed. + +Lemma expRMm n x : expR (n%:R * x) = expR x ^+ n. +Proof. +elim: n x => [x|n IH x] /=; first by rewrite mul0r expr0 expR0. +by rewrite exprS -add1n natrD mulrDl mul1r expRD IH. +Qed. + +Lemma expR_gt1 x: (1 < expR x) = (0 < x). +Proof. +case: ltrgt0P => [x_gt0| xN|->]; last by rewrite expR0. +- by rewrite (pexpR_gt1 x_gt0). +- apply/idP/negP. + rewrite -[x]opprK expRN -leNgt invf_cp1 ?expR_gt0 //. + by rewrite ltW // pexpR_gt1 // lter_oppE. +Qed. + +Lemma expR_lt1 x: (expR x < 1) = (x < 0). +Proof. +case: ltrgt0P => [x_gt0|xN|->]; last by rewrite expR0. +- by apply/idP/negP; rewrite -leNgt ltW // expR_gt1. +- by rewrite -[x]opprK expRN invf_cp1 ?expR_gt0 // expR_gt1 lter_oppE. +Qed. + +Lemma expRB x y : expR (x - y) = expR x / expR y. +Proof. by rewrite expRD expRN. Qed. + +Lemma ltr_expR : {mono (@expR R) : x y / x < y}. +Proof. +move=> x y. +by rewrite -[in LHS](subrK x y) expRD ltr_pmull ?expR_gt0 // expR_gt1 subr_gt0. +Qed. + +Lemma ler_expR : {mono (@expR R) : x y / x <= y}. +Proof. +move=> x y. +case: (ltrgtP x y) => [xLy|yLx|<-]; last by rewrite lexx. +- by rewrite ltW // ltr_expR. +- by rewrite leNgt ltr_expR yLx. +Qed. + +Lemma expR_inj : injective (@expR R). +Proof. +move=> x y exE. +by have [] := (ltr_expR x y, ltr_expR y x); rewrite exE ltxx; case: ltrgtP. +Qed. + +Lemma expR_total_gt1 x : + 1 <= x -> exists y, [/\ 0 <= y, 1 + y <= x & expR y = x]. +Proof. +move=> x_ge1; have x_ge0 : 0 <= x by apply: le_trans x_ge1. +case: (@IVT _ (fun y => expR y - x) 0 x 0) => //. +- by move=> x1 x1Ix; apply: continuousB => // y1; + [exact: continuous_expR|exact: cst_continuous]. +- rewrite expR0; case: (ltrgtP (1- x) (expR x - x)) => [_| |]. + + rewrite subr_le0 x_ge1 subr_ge0. + by apply: le_trans (expR_ge1Dx _); rewrite ?ler_addr. + + by rewrite ltr_add2r expR_lt1 ltNge x_ge0. + + rewrite subr_le0 x_ge1 => -> /=; rewrite subr_ge0. + by apply: le_trans (expR_ge1Dx x_ge0); rewrite ler_addr. +- move=> x1 _ /eqP; rewrite subr_eq0 => /eqP x1_x. + exists x1; split => //; first by rewrite -ler_expR expR0 x1_x. + by rewrite -x1_x expR_ge1Dx // -ler_expR x1_x expR0. +Qed. + +Lemma expR_total x : 0 < x -> exists y, expR y = x. +Proof. +case: (lerP 1 x) => [/expR_total_gt1[y [_ _ Hy]]|x_lt1 x_gt0]. + by exists y. +have /expR_total_gt1[y [H1y H2y H3y]] : 1 <= x^-1 by rewrite ltW // !invf_cp1. +by exists (-y); rewrite expRN H3y invrK. +Qed. + +End expR. + +Section Ln. +Variable R : realType. +Implicit Types x : R. + +Notation exp := (@expR R). + +Definition ln x : R := xget 0 [set y | exp y == x ]. + +Fact ln0 x : x <= 0 -> ln x = 0. +Proof. +rewrite /ln; case: xgetP => //= y _ /eqP yx x0. +by have := expR_gt0 y; rewrite yx => /(le_lt_trans x0); rewrite ltxx. +Qed. + +Lemma expK : cancel exp ln. +Proof. +by move=> x; rewrite /ln; case: xgetP => [x1 _ /eqP/expR_inj //|/(_ x)[]/=]. +Qed. + +Lemma lnK : {in Num.pos, cancel ln exp}. +Proof. +move=> x; rewrite qualifE => x_gt0. +rewrite /ln; case: xgetP=> [x1 _ /eqP// |H]. +by case: (expR_total x_gt0) => y /eqP Hy; case: (H y). +Qed. + +Lemma lnK_eq x : (exp (ln x) == x) = (0 < x). +Proof. +by apply/eqP/idP=> [<-|x0]; [exact: expR_gt0|rewrite lnK// in_itv/= x0]. +Qed. + +Lemma ln1 : ln 1 = 0. +Proof. by apply/expR_inj; rewrite lnK// ?expR0// qualifE. Qed. + +Lemma lnM : {in Num.pos &, {morph ln : x y / x * y >-> x + y}}. +Proof. +move=> x y x0 y0; apply: expR_inj; rewrite expRD !lnK//. +by move: x0 y0; rewrite !qualifE; exact: mulr_gt0. +Qed. + +Lemma ln_inj : {in Num.pos &, injective ln}. +Proof. by move=> x y /lnK {2}<- /lnK {2}<- ->. Qed. + +Lemma lnV : {in Num.pos, {morph ln : x / x ^-1 >-> - x}}. +Proof. +move=> x x0; apply: expR_inj; rewrite lnK// ?expRN ?lnK//. +by move: x0; rewrite !qualifE invr_gt0. +Qed. + +Lemma ln_div : {in Num.pos &, {morph ln : x y / x / y >-> x - y}}. +Proof. +move=> x y x0 y0; rewrite (lnM x0) ?lnV//. +by move: y0; rewrite !qualifE/= invr_gt0. +Qed. + +Lemma ltr_ln : {in Num.pos &, {mono ln : x y / x < y}}. +Proof. by move=> x y x_gt0 y_gt0; rewrite -ltr_expR !lnK. Qed. + +Lemma ler_ln : {in Num.pos &, {mono ln : x y / x <= y}}. +Proof. by move=> x y x_gt0 y_gt0; rewrite -ler_expR !lnK. Qed. + +Lemma lnX n x : 0 < x -> ln(x ^+ n) = ln x *+ n. +Proof. +move=> x_gt0; elim: n => [|n ih] /=; first by rewrite expr0 ln1 mulr0n. +by rewrite !exprS lnM ?qualifE// ?exprn_gt0// mulrS ih. +Qed. + +Lemma le_ln1Dx x : 0 <= x -> ln (1 + x) <= x. +Proof. +move=> x_ge0; rewrite -ler_expR lnK ?expR_ge1Dx //. +by apply: lt_le_trans (_ : 0 < 1) _; rewrite // ler_addl. +Qed. + +Lemma ln_sublinear x : 0 < x -> ln x < x. +Proof. +move=> x_gt0; apply: lt_le_trans (_ : ln (1 + x) <= _). + by rewrite -ltr_expR !lnK ?qualifE ?addr_gt0 // ltr_addr. +by rewrite -ler_expR lnK ?qualifE ?addr_gt0// expR_ge1Dx // ltW. +Qed. + +Lemma ln_ge0 x : 1 <= x -> 0 <= ln x. +Proof. +by move=> x_ge1; rewrite -ler_expR expR0 lnK// qualifE (lt_le_trans _ x_ge1). +Qed. + +Lemma ln_gt0 x : 1 < x -> 0 < ln x. +Proof. +by move=> x_gt1; rewrite -ltr_expR expR0 lnK // qualifE (lt_trans _ x_gt1). +Qed. + +Lemma continuous_ln x : 0 < x -> {for x, continuous ln}. +Proof. +move=> x_gt0; rewrite -[x]lnK//. +apply: nbhs_singleton (near_can_continuous _ _); near=> z; first exact: expK. +by apply: continuous_expR. +Grab Existential Variables. all: end_near. Qed. + +Global Instance is_derive1_ln (x : R) : 0 < x -> is_derive x 1 ln x^-1. +Proof. +move=> x_gt0; rewrite -[x]lnK//. +apply: (@is_derive_inverse R expR); first by near=> z; apply: expK. + by near=>z; apply: continuous_expR. +by rewrite lnK // lt0r_neq0. +Grab Existential Variables. all: end_near. Qed. + +End Ln. + +Section ExpFun. +Variable R : realType. +Implicit Types a x : R. + +Definition exp_fun a x := expR (x * ln a). + +Local Notation "a `^ x" := (exp_fun a x). + +Lemma exp_fun_gt0 a x : 0 < a `^ x. Proof. by rewrite expR_gt0. Qed. + +Lemma exp_funr1 a : 0 < a -> a `^ 1 = a. +Proof. by move=> a0; rewrite /exp_fun mul1r lnK. Qed. + +Lemma exp_funr0 a : 0 < a -> a `^ 0 = 1. +Proof. by move=> a0; rewrite /exp_fun mul0r expR0. Qed. + +Lemma exp_fun1 : exp_fun 1 = fun=> 1. +Proof. by rewrite funeqE => x; rewrite /exp_fun ln1 mulr0 expR0. Qed. + +Lemma ler_exp_fun a : 1 < a -> {homo exp_fun a : x y / x <= y}. +Proof. by move=> a1 x y xy; rewrite /exp_fun ler_expR ler_pmul2r // ln_gt0. Qed. + +Lemma exp_funD a : 0 < a -> {morph exp_fun a : x y / x + y >-> x * y}. +Proof. by move=> a0 x y; rewrite [in LHS]/exp_fun mulrDl expRD. Qed. + +Lemma exp_fun_inv a : 0 < a -> a `^ (-1) = a ^-1. +Proof. +move=> a0. +apply/(@mulrI _ a); first by rewrite unitfE gt_eqF. +rewrite -[X in X * _ = _](exp_funr1 a0) -exp_funD // subrr exp_funr0 //. +by rewrite divrr // unitfE gt_eqF. +Qed. + +Lemma exp_fun_mulrn a n : 0 < a -> exp_fun a n%:R = a ^+ n. +Proof. +move=> a0; elim: n => [|n ih]; first by rewrite mulr0n expr0 exp_funr0. +by rewrite -addn1 natrD exp_funD // exprD ih exp_funr1. +Qed. + +End ExpFun. +Notation "a `^ x" := (exp_fun a x). + +Section riemannR_series. +Variable R : realType. +Implicit Types a : R. +Local Open Scope ring_scope. + +Definition riemannR a : R ^nat := fun n => (n.+1%:R `^ a)^-1. +Arguments riemannR a n /. + +Lemma riemannR_gt0 a i : 0 < a -> 0 < riemannR a i. +Proof. move=> ?; by rewrite /riemannR invr_gt0 exp_fun_gt0. Qed. + +Lemma dvg_riemannR a : 0 < a <= 1 -> ~ cvg (series (riemannR a)). +Proof. +case/andP => a0; rewrite le_eqVlt => /orP[/eqP ->|a1]. + rewrite (_ : riemannR 1 = harmonic); first exact: dvg_harmonic. + by rewrite funeqE => i /=; rewrite exp_funr1. +have : forall n, harmonic n <= riemannR a n. + case=> /= [|n]; first by rewrite exp_fun1 invr1. + rewrite -[X in _ <= X]div1r ler_pdivl_mulr ?exp_fun_gt0 // mulrC. + rewrite ler_pdivr_mulr // mul1r -[X in _ <= X]exp_funr1 //. + by rewrite (ler_exp_fun) // ?ltr1n // ltW. +move/(series_le_cvg harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))). +by move/contra_not; apply; exact: dvg_harmonic. +Qed. + +End riemannR_series. diff --git a/theories/normedtype.v b/theories/normedtype.v index a07fb90c7..a49e29ae4 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2324,6 +2324,14 @@ Qed. Lemma is_cvgDrE f g : cvg (f @ F) -> cvg ((f + g) @ F) = cvg (g @ F). Proof. by rewrite addrC; apply: is_cvgDlE. Qed. +Lemma cvg_sub0 f g a : (f - g) @ F --> (0 : V) -> g @ F --> a -> f @ F --> a. +Proof. +by move=> Cfg Cg; have := cvgD Cfg Cg; rewrite subrK add0r; apply. +Qed. + +Lemma cvg_zero f a : (f - cst a) @ F --> (0 : V) -> f @ F --> a. +Proof. by move=> Cfa; apply: cvg_sub0 Cfa (cvg_cst _). Qed. + Lemma cvgZ s f k a : s @ F --> k -> f @ F --> a -> s x *: f x @[x --> F] --> k *: a. Proof. move=> ? ?; apply: continuous2_cvg => //; exact: scale_continuous. Qed. @@ -3834,6 +3842,23 @@ rewrite funeqE => A; rewrite /= !near_simpl (near_shift (y + x)). by rewrite (_ : _ \o _ = A \o f) // funeqE=> z; rewrite /= opprD addNKr addrNK. Qed. +Section continuous. +Variables (K : numFieldType) (U V : normedModType K). + +Lemma continuous_shift (f : U -> V) u : + {for u, continuous f} = {for 0, continuous (f \o shift u)}. +Proof. by rewrite [in RHS]forE /= add0r cvg_comp_shift add0r. Qed. + +Lemma continuous_withinNshiftx (f : U -> V) u : + f \o shift u @ 0^' --> f u <-> {for u, continuous f}. +Proof. +rewrite continuous_shift; split=> [cfu|]. + by apply/(continuous_withinNx _ _).2/(cvg_trans cfu); rewrite /= add0r. +by move/(continuous_withinNx _ _).1/cvg_trans; apply; rewrite /= add0r. +Qed. + +End continuous. + Section Closed_Ball. Lemma ball_open (R : numDomainType) (V : normedModType R) (x : V) (r : R) : diff --git a/theories/nsatz_realtype.v b/theories/nsatz_realtype.v new file mode 100644 index 000000000..28eacc49f --- /dev/null +++ b/theories/nsatz_realtype.v @@ -0,0 +1,80 @@ +Require Import Nsatz. +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum. +Require Import boolp reals ereal. + +(******************************************************************************) +(* nsatz for realType *) +(* *) +(* This file registers the ring corresponding to the MathComp-Analysis type *) +(* realType to the tactic nsatz of Coq. This enables some automation used for *) +(* example in the file trigo.v. *) +(* *) +(* ref: https://coq.inria.fr/refman/addendum/nsatz.html *) +(* *) +(******************************************************************************) + +Import GRing.Theory Num.Theory. + +Local Open Scope ring_scope. + +Section Nsatz_realType. +Variable T : realType. + +Lemma Nsatz_realType_Setoid_Theory : Setoid.Setoid_Theory T (@eq T). +Proof. by constructor => [x //|x y //|x y z ->]. Qed. + +Definition Nsatz_realType0 := (0%:R : T). +Definition Nsatz_realType1 := (1%:R : T). +Definition Nsatz_realType_add (x y : T) := (x + y)%R. +Definition Nsatz_realType_mul (x y : T) := (x * y)%R. +Definition Nsatz_realType_sub (x y : T) := (x - y)%R. +Definition Nsatz_realType_opp (x : T) := (- x)%R. + +#[global] +Instance Nsatz_realType_Ring_ops: + (@Ncring.Ring_ops T Nsatz_realType0 Nsatz_realType1 + Nsatz_realType_add + Nsatz_realType_mul + Nsatz_realType_sub + Nsatz_realType_opp (@eq T)). +Defined. + +#[global] +Instance Nsatz_realType_Ring : (Ncring.Ring (Ro:=Nsatz_realType_Ring_ops)). +Proof. +constructor => //. +- exact: Nsatz_realType_Setoid_Theory. +- by move=> x y -> x1 y1 ->. +- by move=> x y -> x1 y1 ->. +- by move=> x y -> x1 y1 ->. +- by move=> x y ->. +- exact: add0r. +- exact: addrC. +- exact: addrA. +- exact: mul1r. +- exact: mulr1. +- exact: mulrA. +- exact: mulrDl. +- move=> x y z; exact: mulrDr. +- exact: subrr. +Defined. + +#[global] +Instance Nsatz_realType_Cring: (Cring.Cring (Rr:=Nsatz_realType_Ring)). +Proof. exact: mulrC. Defined. + +#[global] +Instance Nsatz_realType_Integral_domain : + (Integral_domain.Integral_domain (Rcr:=Nsatz_realType_Cring)). +Proof. +constructor. + move=> x y. + rewrite -[_ _ Algebra_syntax.zero]/(x * y = 0)%R => /eqP. + by rewrite mulf_eq0 => /orP[] /eqP->; [left | right]. +rewrite -[_ _ Algebra_syntax.zero]/(1 = 0)%R; apply/eqP. +by rewrite (eqr_nat T 1 0). +Defined. + +End Nsatz_realType. + +Tactic Notation "nsatz" := nsatz_default. diff --git a/theories/realfun.v b/theories/realfun.v index 1e9ae639c..5ef40ad2c 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -4,7 +4,7 @@ From mathcomp Require Import seq fintype bigop order ssralg ssrint ssrnum finmap From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. Require Import boolp ereal reals. Require Import classical_sets posnum nngnum topology prodnormedzmodule. -Require Import cardinality normedtype. +Require Import cardinality normedtype derive. (******************************************************************************) (* This file provides properties of standard real-valued functions over real *) @@ -438,3 +438,105 @@ move=> x; case: (ltrgtP x 0) => [xlt0 | xgt0 | ->]. Grab Existential Variables. all: end_near. Qed. End real_inverse_function_instances. + +Section is_derive_inverse. +Variable R : realType. + +(* Attempt to prove the diff of inverse *) + +Lemma is_derive1_caratheodory (f : R -> R) (x a : R) : + is_derive x 1 f a <-> + exists g, [/\ forall z, f z - f x = g z * (z - x), + {for x, continuous g} & g x = a]. +Proof. +split => [Hd|[g [fxE Cg gxE]]]. + exists (fun z => if z == x then a else (f(z) - f(x)) / (z - x)); split. + - move=> z; case: eqP => [->|/eqP]; first by rewrite !subrr mulr0. + by rewrite -subr_eq0 => /divfK->. + - apply/continuous_withinNshiftx; rewrite eqxx /=. + pose g1 h := (h^-1 *: ((f \o shift x) h%:A - f x)). + have F1 : g1 @ 0^' --> a by case: Hd => H1 <-. + apply: cvg_trans F1; apply: near_eq_cvg; rewrite /g1 !fctE. + near=> i. + rewrite ifN; first by rewrite addrK mulrC /= [_%:A]mulr1. + rewrite -subr_eq0 addrK. + by near: i; rewrite near_withinE /= near_simpl; near=> x1. + by rewrite eqxx. +suff Hf : h^-1 *: ((f \o shift x) h%:A - f x) @[h --> 0^'] --> a. + have F1 : 'D_1 f x = a by apply: cvg_lim. + rewrite -F1 in Hf. + by constructor. + have F1 : (g \o shift x) y @[y --> 0^'] --> a. + by rewrite -gxE; apply/continuous_withinNshiftx. +apply: cvg_trans F1; apply: near_eq_cvg. +near=> y. +rewrite /= fxE /= addrK [_%:A]mulr1. +suff yNZ : y != 0 by rewrite [RHS]mulrC mulfK. +by near: y; rewrite near_withinE /= near_simpl; near=> x1. +Grab Existential Variables. all: end_near. Qed. + +Lemma is_derive_0_is_cst (f : R -> R) x y : + (forall x, is_derive x 1 f 0) -> f x = f y. +Proof. +move=> Hd. +wlog xLy : x y / x <= y. + by move=> H; case: (leP x y) => [/H |/ltW /H]. +rewrite -(subKr (f y) (f x)). +case: (MVT xLy) => [x1 _ | _ _]. + by apply/differentiable_continuous/derivable1_diffP. +by rewrite mul0r => ->; rewrite subr0. +Qed. + +Global Instance is_derive1_comp (f g : R -> R) (x a b : R) : + is_derive (g x) 1 f a -> is_derive x 1 g b -> + is_derive x 1 (f \o g) (a * b). +Proof. +move=> [fgxv <-{a}] [gv <-{b}]; apply: (@DeriveDef _ _ _ _ _ (f \o g)). + apply/derivable1_diffP/differentiable_comp; first exact/derivable1_diffP. + by move/derivable1_diffP in fgxv. +by rewrite -derive1E (derive1_comp gv fgxv) 2!derive1E. +Qed. + +Lemma is_deriveV (f : R -> R) (x t v : R) : + f x != 0 -> is_derive x v f t -> + is_derive x v (fun y => (f y)^-1) (- (f x) ^- 2 *: t). +Proof. +move=> fxNZ Df. +constructor; first by apply: derivableV => //; case: Df. +by rewrite deriveV //; case: Df => _ ->. +Qed. + +Lemma is_derive_inverse (f g : R -> R) l x : + {near x, cancel f g} -> + {near x, continuous f} -> + is_derive x 1 f l -> l != 0 -> is_derive (f x) 1 g l^-1. +Proof. +move=> fgK fC fD lNZ. +have /is_derive1_caratheodory [h [fE hC hxE]] := fD. +(* There should be something simpler *) +have gfxE : g (f x) = x by have [d Hd]:= nbhs_ex fgK; apply: Hd. +pose g1 y := if y == f x then (h (g y))^-1 + else (g y - g (f x)) / (y - f x). +apply/is_derive1_caratheodory. +exists g1; split; first 2 last. +- by rewrite /g1 eqxx gfxE hxE. +- move=> z; rewrite /g1; case: eqP => [->|/eqP]; first by rewrite !subrr mulr0. + by rewrite -subr_eq0 => /divfK. +have F1 : (h (g x))^-1 @[x --> f x] --> g1 (f x). + rewrite /g1 eqxx; apply: continuousV; first by rewrite /= gfxE hxE. + apply: continuous_comp; last by rewrite gfxE. + by apply: nbhs_singleton (near_can_continuous _ _). +apply: cvg_sub0 F1. +apply/cvg_distP => eps eps_gt0 /=; rewrite !near_simpl /=. +near=> y; rewrite sub0r normrN !fctE. +have fgyE : f (g y) = y by near: y; apply: near_continuous_can_sym. +rewrite /g1; case: eqP => [_|/eqP x1Dfx]; first by rewrite subrr normr0. +have -> : y - f x = h (g y) * (g y - x) by rewrite -fE fgyE. +rewrite gfxE invfM mulrC divfK ?subrr ?normr0 // subr_eq0. +by apply: contra x1Dfx => /eqP<-; apply/eqP. +Grab Existential Variables. all: end_near. Qed. + +End is_derive_inverse. + +Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => + (eapply is_deriveV; first by []) : typeclass_instances. diff --git a/theories/sequences.v b/theories/sequences.v index 7dcc12e85..2eb5a93a0 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -450,7 +450,6 @@ Lemma eq_sum_telescope (V : zmodType) (u_ : V ^nat) n : Proof. by rewrite telescopeK/= addrC addrNK. Qed. Section series_patched. - Variables (N : nat) (K : numFieldType) (V : normedModType K). Implicit Types (f : nat -> V) (u : V ^nat) (l : V). @@ -728,7 +727,7 @@ move=> cvg_series. rewrite (_ : u_ = fun n => series u_ (n + 1)%nat - series u_ n); last first. by rewrite funeqE => i; rewrite addn1 seriesSB. rewrite -(subrr (lim (series u_))). -by apply: cvgD; rewrite ?cvg_shiftn//; apply: cvgN. +by apply: cvgB => //; rewrite ?cvg_shiftn. Qed. Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) : @@ -747,6 +746,7 @@ Qed. End series_convergence. + Definition arithmetic (R : zmodType) a z : R ^nat := [sequence a + z *+ n]_n. Arguments arithmetic {R} a z n /. @@ -862,6 +862,54 @@ rewrite -lim_norm // (ler_lim (is_cvg_norm cf) cnf) //. by near=> x; rewrite ler_norm_sum. Grab Existential Variables. all: end_near. Qed. +Section series_linear. + +Lemma cvg_series_bounded (R : realFieldType) (f : R ^nat) : + cvg (series f) -> bounded_fun f. +Proof. +by move/cvg_series_cvg_0 => f0; apply/cvg_seq_bounded/cvg_ex; exists 0. +Qed. + +Lemma cvg_to_0_linear (R : realFieldType) (f : R -> R) K k : + 0 < k -> (forall r, 0 < `| r | < k -> `|f r| <= K * `| r |) -> + f x @[x --> 0^'] --> 0. +Proof. +move=> k0 kfK; have [K0|K0] := lerP K 0. +- apply/cvg_distP => _/posnumP[e]; rewrite near_map; near=> x. + rewrite distrC subr0 (le_lt_trans (kfK _ _)) //; last first. + by rewrite (@le_lt_trans _ _ 0)// mulr_le0_ge0. + near: x; exists (k / 2); first by rewrite /mkset divr_gt0. + move=> t /=; rewrite distrC subr0 => tk2 t0. + by rewrite normr_gt0 t0 (lt_trans tk2) // -[in X in X < _](add0r k) midf_lt. +- apply/eqolim0/eqoP => _/posnumP[e]; near=> x. + rewrite (le_trans (kfK _ _)) //=. + + near: x; exists (k / 2); first by rewrite /mkset divr_gt0. + move=> t /=; rewrite distrC subr0 => tk2 t0. + by rewrite normr_gt0 t0 (lt_trans tk2) // -[in X in X < _](add0r k) midf_lt. + + rewrite normr1 mulr1 mulrC -ler_pdivl_mulr //. + near: x; exists (e%:num / K); first by rewrite /mkset divr_gt0. + by move=> t /=; rewrite distrC subr0 => /ltW. +Grab Existential Variables. all: end_near. Qed. + +Lemma lim_cvg_to_0_linear (R : realType) (f : nat -> R) (g : R -> nat -> R) k : + 0 < k -> cvg (series f) -> + (forall r, 0 < `|r| < k -> forall n, `|g r n| <= f n * `| r |) -> + lim (series (g x)) @[x --> 0^'] --> 0. +Proof. +move=> k_gt0 Cf Hg. +apply: (@cvg_to_0_linear _ _ (lim (series f)) k) => // h hLk; rewrite mulrC. +have Ckf := @is_cvg_seriesZ _ _ `|h| Cf. +have Cng : cvg [normed series (g h)]. + apply: series_le_cvg (Hg _ hLk) _ => [//|?|]. + exact: le_trans (Hg _ hLk _). + by under eq_fun do rewrite mulrC. +apply: (le_trans (lim_series_norm Cng)). +rewrite -[_ * _](lim_seriesZ _ Cf) (lim_series_le Cng Ckf) // => n. +by rewrite [X in _ <= X]mulrC; apply: Hg. +Qed. + +End series_linear. + (* TODO: backport to MathComp? *) Section fact_facts. @@ -1003,7 +1051,7 @@ Proof. exact: (cvg_series_cvg_0 (@is_cvg_series_exp_coeff x)). Qed. End exponential_series. (* TODO: generalize *) -Definition expR (R : realType) (x : R) : R := lim (series (exp_coeff x)). +Definition expR {R : realType} (x : R) : R := lim (series (exp_coeff x)). Notation "\big [ op / idx ]_ ( m <= i (\big[ op / idx ]_(m <= i < n | P) F))) : big_scope. diff --git a/theories/topology.v b/theories/topology.v index 115ec0fa1..5a2448c95 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -5,7 +5,7 @@ From mathcomp Require Import matrix finmap. Require Import boolp reals classical_sets posnum. (******************************************************************************) -(* Filters and basic topological notions *) +(* Filters and basic topological notions *) (* *) (* This file develops tools for the manipulation of filters and basic *) (* topological notions. The development of topological notions builds on *) @@ -17,6 +17,11 @@ Require Import boolp reals classical_sets posnum. (* *) (* monotonous A f := {in A &, {mono f : x y / x <= y}} \/ *) (* {in A &, {mono f : x y /~ x <= y}}. *) +(* Section function_space == canonical ringType and lmodType *) +(* structures for functions whose range is *) +(* a ringType, comRingType,or lmodType. *) +(* fctE == multi-rule for fct *) +(* *) (* * Filters : *) (* filteredType U == interface type for types whose *) (* elements represent sets of sets on U. *) @@ -393,10 +398,7 @@ Unset Printing Implicit Defensive. (* Making sure that [Program] does not automatically introduce *) Obligation Tactic := idtac. -(********************************) -(* Missing lemmas for mathcommp *) -(********************************) - +(* NB: these lemmas are in the recent versions of MathComp *) Section inj_can_sym_in_on. Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}). Variables (f : aT -> rT) (g : rT -> aT). @@ -419,10 +421,7 @@ End inj_can_sym_in_on. Arguments inj_can_sym_in_on {aT rT aD rD f g}. Arguments inj_can_sym_on {aT rT aD f g}. Arguments inj_can_sym_in {aT rT rD f g}. - -(*************************) -(* Mathcomp analysis now *) -(*************************) +(* /NB: these lemmas are in the recent versions of MathComp *) Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope classical_set_scope. @@ -680,6 +679,40 @@ Canonical linear_pointedType := PointedType {linear U -> V | GRing.Scale.op s_la (@GRing.null_fun_linear R U V s s_law). End Linear2. +(******************************************************************************) +Lemma addrfunE (T : pointedType) (K : ringType) (f g : T -> K) : + f + g = (fun x : T => f x + g x). +Proof. by []. Qed. + +Lemma opprfunE (T : pointedType) (K : ringType) (f : T -> K) : + - f = (fun x : T => - f x). +Proof. by []. Qed. + +Lemma mulrfunE (T : pointedType) (K : ringType) (f g : T -> K) : + f * g = (fun x : T => f x * g x). +Proof. by []. Qed. + +Lemma scalrfunE (T : pointedType) (K : ringType) (L : lmodType K) + k (f : T -> L) : + k *: f = (fun x : T => k *: f x). +Proof. by []. Qed. + +Lemma cstE (T T': Type) (x : T) : cst x = fun _: T' => x. +Proof. by []. Qed. + +Lemma exprfunE (T : pointedType) (K : ringType) (f : T -> K) n : + f ^+ n = (fun x => f x ^+ n). +Proof. +by elim: n => [|n ihn]; rewrite funeqE=> ?; [rewrite !expr0|rewrite !exprS ihn]. +Qed. + +Lemma compE (T1 T2 T3 : Type) (f : T1 -> T2) (g : T2 -> T3) : + g \o f = fun x => g (f x). +Proof. by []. Qed. + +Definition fctE := + (cstE, compE, opprfunE, addrfunE, mulrfunE, scalrfunE, exprfunE). + Module Filtered. (* Index a family of filters on a type, one for each element of the type *) diff --git a/theories/trigo.v b/theories/trigo.v new file mode 100644 index 000000000..82dbc23ac --- /dev/null +++ b/theories/trigo.v @@ -0,0 +1,1163 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum. +From mathcomp Require Import matrix interval rat. +Require Import boolp reals ereal. +Require Import nsatz_realtype. +Require Import classical_sets posnum topology normedtype landau sequences. +Require Import derive realfun exp. + +(******************************************************************************) +(* Theory of trigonometric functions *) +(* *) +(* This file provides the definitions of basic trigonometric functions and *) +(* develops their theories. *) +(* *) +(* periodic f T == f is a periodic function of period T *) +(* alternating f T == f is an alternating function of period T *) +(* sin_coeff x == the sequence of coefficients of sin x *) +(* sin x == the sine function, i.e., lim (series (sin_coeff x)) *) +(* sin_coeff' x == the sequence of odd coefficients of sin x *) +(* cos_coeff x == the sequence of coefficients of cos x *) +(* cos x == the cosine function, i.e., lim (series (cos_coeff x)) *) +(* cos_coeff' x == the sequence of even coefficients of cos x *) +(* pi == pi *) +(* tan x == the tangent function *) +(* acos x == the arccos function *) +(* asin x == the arcsin function *) +(* atan x == the arctangent function *) +(* *) +(* Acknowledgments: the proof of cos 2 < 0 is inspired from HOL-light, some *) +(* proofs of trigonometric relations are taken from *) +(* /~https://github.com/affeldt-aist/coq-robot. *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldNormedType.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +(* NB: backport to mathcomp in progress *) +Lemma sqrtrV (R : rcfType) (x : R) : 0 <= x -> Num.sqrt (x^-1) = (Num.sqrt x)^-1. +Proof. +move=> x_ge0. +case: (x =P 0) => [->|/eqP xD0]; first by rewrite invr0 sqrtr0 invr0. +rewrite -[LHS]mul1r -(mulVf (_ : Num.sqrt x != 0)); last first. + by rewrite sqrtr_eq0 -ltNge; case: ltrgt0P x_ge0 xD0. +by rewrite -mulrA -sqrtrM // divff // sqrtr1 mulr1. +Qed. + +Lemma eqr_div (R : numFieldType) (x y z t : R): + y != 0 -> t != 0 -> (x / y == z / t) = (x * t == z * y). +Proof. +move=> yD0 tD0. +rewrite -[x in RHS](divfK yD0) -[z in RHS](divfK tD0) mulrAC. +by apply/eqP/eqP=> [->//|xyty]; exact/(mulIf tD0)/(mulIf yD0). +Qed. + +Lemma big_nat_mul (R : zmodType) (f : R ^nat) (n k : nat) : + \sum_(0 <= i < n * k) f i = + \sum_(0 <= i < n) \sum_(i * k <= j < i.+1 * k) f j. +Proof. +elim: n => [|n ih]; first by rewrite mul0n 2!big_nil. +rewrite [in RHS]big_nat_recr//= -ih mulSn addnC [in LHS]/index_iota subn0 iotaD. +rewrite big_cat /= [in X in _ = X _]/index_iota subn0; congr (_ + _). +by rewrite add0n /index_iota (addnC _ k) addnK. +Qed. +(* /NB: backport to mathcomp in progress *) + +Lemma cvg_series_cvg_series_group (R : realFieldType) (f : R ^nat) k : + cvg (series f) -> (0 < k)%N -> + [series \sum_(n * k <= i < n.+1 * k) f i]_n --> lim (series f). +Proof. +move=> /cvg_ballP cf k0; apply/cvg_ballP => _/posnumP[e]. +have := cf _ (posnum_gt0 e); rewrite near_map => -[n _ nl]. +rewrite near_map; near=> m. +rewrite /ball /= [in X in `|_ - X|]/series [in X in `|_ - X|]/= -big_nat_mul. +have /nl : (n <= m * k)%N. + by near: m; exists n.+1 => //= p /ltnW /leq_trans /(_ (leq_pmulr _ k0)). +by rewrite /ball /= distrC. +Grab Existential Variables. all: end_near. Qed. + +Lemma lt_sum_lim_series (R : realFieldType) (f : R ^nat) n : cvg (series f) -> + (forall d, 0 < f (n + d.*2)%N + f (n + d.*2.+1)%N) -> + \sum_(0 <= i < n) f i < lim (series f). +Proof. +move=> /cvg_ballP cf fn. +have fn0 : 0 < f n + f n.+1 by have := fn 0%N; rewrite double0 addn0 addn1. +rewrite ltNge; apply: contraPN cf => ffn /(_ _ fn0). +rewrite near_map /ball /=. +have nf_ub N : \sum_(0 <= i < n.+2) f i <= \sum_(0 <= i < N.+1.*2 + n) f i. + elim: N => // N /le_trans ->//; rewrite -(addn1 (N.+1)) doubleD addnAC. + rewrite [in X in _ <= X]/index_iota subn0 iota_add big_cat. + rewrite -[in X in _ <= X + _](subn0 (N.+1.*2 + n)%N) ler_addl /= add0n. + by rewrite 2!big_cons big_nil addr0 -(addnC n) ltW// -addnS fn. +case=> N _ Nfn; have /Nfn/ltr_distlC_addr : (N.+1.*2 + n >= N)%N. + by rewrite doubleS -addn2 -addnn -2!addnA leq_addr. +rewrite addrA => ffnfn. +have : lim (series f) + f n + f n.+1 <= \sum_(0 <= i < N.+1.*2 + n) f i. + apply: (le_trans _ (nf_ub N)). + by do 2 rewrite big_nat_recr //=; by rewrite -2!addrA ler_add2r. +by move/(lt_le_trans ffnfn); rewrite ltxx. +Qed. + +Section periodic. +Variables U V : zmodType. +Implicit Type f : U -> V. + +Definition periodic f (T : U) := forall u, f (u + T) = f u. + +Lemma periodicn f (T : U) : periodic f T -> forall n a, f (a + T *+ n) = f a. +Proof. +by move=> fT; elim=> [|n ih] a;[rewrite mulr0n addr0|rewrite mulrS addrA ih fT]. +Qed. +End periodic. + +Section alternating. +Variables (U : zmodType) (V : ringType). +Implicit Type f : U -> V. + +Definition alternating f (T : U) := forall x, f (x + T) = - f x. + +Lemma alternatingn f (T : U) : alternating f T -> + forall n a, f (a + T *+ n) = (- 1) ^+ n * f a. +Proof. +move=> fT; elim => [a|n ih a]; first by rewrite mulr0n expr0 addr0 mul1r. +by rewrite mulrS addrA ih fT exprS mulrN mulN1r mulNr. +Qed. + +End alternating. + +Section CosSin. +Variable R : realType. +Implicit Types x y : R. + +Definition sin_coeff x := + [sequence (odd n)%:R * (-1) ^+ n.-1./2 * x ^+ n / n`!%:R]_n. + +Lemma sin_coeffE x : sin_coeff x = + (fun n => (fun n => (odd n)%:R * (-1) ^+ n.-1./2 * (n`!%:R)^-1) n * x ^+ n). +Proof. by apply/funext => i; rewrite /sin_coeff /= -!mulrA [_ / _]mulrC. Qed. + +Lemma sin_coeff_even n x : sin_coeff x n.*2 = 0. +Proof. by rewrite /sin_coeff /= odd_double /= !mul0r. Qed. + +Lemma is_cvg_series_sin_coeff x : cvg (series (sin_coeff x)). +Proof. +apply: normed_cvg. +apply: series_le_cvg; last exact: (@is_cvg_series_exp_coeff _ `|x|). +- by move=> n; rewrite normr_ge0. +- by move=> n; rewrite divr_ge0 ?exprn_ge0 // ler0n. +- move=> n /=; rewrite /exp_coeff /sin_coeff /=. + rewrite !normrM normfV !normr_nat !normrX normrN normr1 expr1n mulr1. + case: odd; first by rewrite mul1r. + by rewrite !mul0r divr_ge0 ?exprn_ge0 // ler0n. +Qed. + +Definition sin x : R := lim (series (sin_coeff x)). + +Lemma sinE : sin = fun x => + lim (pseries (fun n => (odd n)%:R * (-1) ^+ n.-1./2 * (n`!%:R)^-1) x). +Proof. by apply/funext => x; rewrite /pseries -sin_coeffE. Qed. + +Definition sin_coeff' x (n : nat) := (-1)^n * x ^+ n.*2.+1 / n.*2.+1`!%:R. + +Lemma sin_coeff'E x n : sin_coeff' x n = sin_coeff x n.*2.+1. +Proof. +by rewrite /sin_coeff' /sin_coeff /= odd_double mul1r -2!mulrA doubleK. +Qed. + +Lemma cvg_sin_coeff' x : series (sin_coeff' x) --> sin x. +Proof. +have /(@cvg_series_cvg_series_group _ _ 2) := @is_cvg_series_sin_coeff x. +move=> /(_ isT); apply: cvg_trans. +rewrite [X in _ --> series X](_ : _ = (fun n => sin_coeff x n.*2.+1)). + rewrite [X in series X --> _](_ : _ = (fun n => sin_coeff x n.*2.+1)) //. + by rewrite funeqE => n; exact: sin_coeff'E. +rewrite funeqE=> n; rewrite /= 2!muln2 big_nat_recl //= sin_coeff_even add0r. +by rewrite big_nat_recl // big_geq // addr0. +Qed. + +Lemma diffs_sin : + pseries_diffs (fun n => (odd n)%:R * (-1) ^+ n.-1./2 * (n`!%:R)^-1) = + (fun n => (~~(odd n))%:R * (-1) ^+ n./2 * (n`!%:R)^-1 : R). +Proof. +apply/funext => i; rewrite /pseries_diffs /= factS natrM invfM. +by rewrite [_.+1%:R * _]mulrC -!mulrA [_.+1%:R^-1 * _]mulrC mulfK. +Qed. + +Lemma series_sin_coeff0 n : series (sin_coeff 0) n.+1 = 0. +Proof. +rewrite /series /= big_nat_recl //= /sin_coeff /= expr0n divr1 !mulr1. +by rewrite big1 ?addr0 // => i _; rewrite expr0n !(mul0r, mulr0). +Qed. + +Lemma sin0 : sin 0 = 0. +Proof. +apply: lim_near_cst => //; near=> m; rewrite -[m]prednK; last by near: m. +rewrite -addn1 series_addn series_sin_coeff0 big_add1 big1 ?addr0//. +by move=> i _; rewrite /sin_coeff /= expr0n !(mulr0, mul0r). +Grab Existential Variables. all: end_near. Qed. + +Definition cos_coeff x := + [sequence (~~ odd n)%:R * (-1)^n./2 * x ^+ n / n`!%:R]_n. + +Lemma cos_coeff_odd n x : cos_coeff x n.*2.+1 = 0. +Proof. by rewrite /cos_coeff /= odd_double /= !mul0r. Qed. + +Lemma cos_coeff_2_0 : cos_coeff 2 0%N = 1 :> R. +Proof. by rewrite /cos_coeff /= mul1r expr0 mulr1 expr0z divff. Qed. + +Lemma cos_coeff_2_2 : cos_coeff 2 2%N = - 2%:R :> R. +Proof. +by rewrite /cos_coeff /= mul1r expr1z mulN1r expr2 mulNr -mulrA divff// mulr1. +Qed. + +Lemma cos_coeff_2_4 : cos_coeff 2 4 = 2%:R / 3%:R :> R. +Proof. +rewrite /cos_coeff /= mul1r -exprnP sqrrN expr1n mul1r 2!factS mulnCA mulnC. +by rewrite 3!exprS expr1 2!mulrA natrM -mulf_div -2!natrM divff// mul1r. +Qed. + +Lemma cos_coeffE x : + cos_coeff x = (fun n => (fun n => (~~(odd n))%:R * (-1) ^+ n./2 * + (n`!%:R)^-1) n * x ^+ n). +Proof. +by apply/funext => i; rewrite /cos_coeff /= -!mulrA [_ / _]mulrC. +Qed. + +Lemma is_cvg_series_cos_coeff x : cvg (series (cos_coeff x)). +Proof. +apply: normed_cvg. +apply: series_le_cvg; last exact: (@is_cvg_series_exp_coeff _ `|x|). +- by move=> n; rewrite normr_ge0. +- by move=> n; rewrite divr_ge0 ?exprn_ge0 // ler0n. +- move=> n /=. + rewrite /exp_coeff /cos_coeff /=. + rewrite !normrM normfV !normr_nat !normrX normrN normr1 expr1n mulr1. + case: odd; last by rewrite mul1r. + by rewrite !mul0r divr_ge0 ?exprn_ge0 // ler0n. +Qed. + +Definition cos x : R := lim (series (cos_coeff x)). + +Lemma cosE : cos = fun x => + lim (series (fun n => + (fun n => (~~(odd n))%:R * (-1)^+ n./2 * (n`!%:R)^-1) n + * x ^+ n)). +Proof. by apply/funext => x; rewrite -cos_coeffE. Qed. + +Definition cos_coeff' x (n : nat) := (-1)^n * x ^+ n.*2 / n.*2`!%:R. + +Lemma cos_coeff'E x n : cos_coeff' x n = cos_coeff x n.*2. +Proof. +rewrite /cos_coeff' /cos_coeff /= odd_double /= mul1r -2!mulrA; congr (_ * _). +by rewrite (half_bit_double n false). +Qed. + +Lemma cvg_cos_coeff' x : series (cos_coeff' x) --> cos x. +Proof. +have /(@cvg_series_cvg_series_group _ _ 2) := @is_cvg_series_cos_coeff x. +move=> /(_ isT); apply: cvg_trans. +rewrite [X in _ --> series X](_ : _ = (fun n => cos_coeff x n.*2)); last first. + rewrite funeqE=> n; rewrite /= 2!muln2 big_nat_recr //= cos_coeff_odd addr0. + by rewrite big_nat_recl//= /index_iota subnn big_nil addr0. +rewrite [X in series X --> _](_ : _ = (fun n => cos_coeff x n.*2)) //. +by rewrite funeqE => n; exact: cos_coeff'E. +Qed. + +Lemma diffs_cos : + pseries_diffs (fun n => (~~(odd n))%:R * (-1) ^+ n./2 * (n`!%:R)^-1) = + (fun n => - ((odd n)%:R * (-1) ^+ n.-1./2 * (n`!%:R)^-1): R). +Proof. +apply/funext => [] [|i] /=. + by rewrite /pseries_diffs /= !mul0r mulr0 oppr0. +rewrite /pseries_diffs /= negbK exprS mulN1r !(mulNr, mulrN). +rewrite factS natrM invfM. +by rewrite [_.+1%:R * _]mulrC -!mulrA [_.+1%:R^-1 * _]mulrC mulfK. +Qed. + +Lemma series_cos_coeff0 n : series (cos_coeff 0) n.+1 = 1. +Proof. +rewrite /series /= big_nat_recl //= /cos_coeff /= expr0n divr1 !mulr1. +by rewrite big1 ?addr0 // => i _; rewrite expr0n !(mul0r, mulr0). +Qed. + +Lemma cos0 : cos 0 = 1. +Proof. +apply: lim_near_cst => //; near=> m; rewrite -[m]prednK; last by near: m. +rewrite -addn1 series_addn series_cos_coeff0 big_add1 big1 ?addr0//. +by move=> i _; rewrite /cos_coeff /= expr0n !(mulr0, mul0r). +Grab Existential Variables. all: end_near. Qed. + +Global Instance is_derive_sin x : is_derive x 1 sin (cos x). +Proof. +rewrite sinE /=. +pose s : R^nat := fun n => (odd n)%:R * (-1) ^+ (n.-1)./2 / n`!%:R. +pose s1 n := pseries_diffs s n * x ^+ n. +rewrite cosE /= /pseries (_ : (fun _ => _) = s1); last first. + by apply/funext => i; rewrite /s1 diffs_sin. +apply: (@pseries_snd_diffs _ _ (`|x| + 1)); rewrite /pseries. +- by rewrite -sin_coeffE; apply: is_cvg_series_sin_coeff. +- rewrite (_ : (fun _ => _) = cos_coeff (`|x| + 1)). + exact: is_cvg_series_cos_coeff. + by apply/funext => i; rewrite diffs_sin cos_coeffE. +- rewrite /pseries (_ : (fun _ => _) = - sin_coeff (`|x| + 1)). + by rewrite is_cvg_seriesN; exact: is_cvg_series_sin_coeff. + by apply/funext => i; rewrite diffs_sin diffs_cos sin_coeffE !fctE !mulNr. +- by rewrite [X in _ < X]ger0_norm ?addr_ge0 // addrC -subr_gt0 addrK. +Qed. + +Lemma derivable_sin x : derivable sin x 1. +Proof. by apply: ex_derive; apply: is_derive_sin. Qed. + +Lemma continuous_sin : continuous sin. +Proof. +by move=> x; apply/differentiable_continuous/derivable1_diffP/derivable_sin. +Qed. + +Global Instance is_derive_cos x : is_derive x 1 cos (- (sin x)). +Proof. +rewrite cosE /=. +pose s : R^nat := fun n => (~~ odd n)%:R * (-1) ^+ n./2 / n`!%:R. +pose s1 n := pseries_diffs s n * x ^+ n. +rewrite sinE /= /pseries. +rewrite (_ : (fun _ => _) = - s1); last first. + by apply/funext => i; rewrite /s1 diffs_cos !fctE mulNr opprK. +rewrite lim_seriesN ?opprK; last first. + rewrite (_ : s1 = - sin_coeff x). + by rewrite is_cvg_seriesN; exact: is_cvg_series_sin_coeff. + by apply/funext => i; rewrite /s1 diffs_cos sin_coeffE !fctE mulNr. +apply: (@pseries_snd_diffs _ _ (`|x| + 1)). +- by rewrite /pseries -cos_coeffE; apply: is_cvg_series_cos_coeff. +- rewrite /pseries (_ : (fun _ => _) = - sin_coeff (`|x| + 1)). + by rewrite is_cvg_seriesN; exact: is_cvg_series_sin_coeff. + by apply/funext => i; rewrite diffs_cos sin_coeffE !fctE mulNr. +- rewrite /pseries (_ : (fun _=> _) = - cos_coeff (`|x| + 1)). + by rewrite is_cvg_seriesN; exact: is_cvg_series_cos_coeff. + apply/funext => i; rewrite diffs_cos -opprfunE. + by rewrite pseries_diffsN diffs_sin cos_coeffE !fctE mulNr. +- by rewrite [X in _ < X]ger0_norm ?addr_ge0 // addrC -subr_gt0 addrK. +Qed. + +Lemma derivable_cos x : derivable cos x 1. +Proof. by apply: ex_derive; apply: is_derive_cos. Qed. + +Lemma continuous_cos : continuous cos. +Proof. +by move=> x; exact/differentiable_continuous/derivable1_diffP/derivable_cos. +Qed. + +Lemma cos2Dsin2 x : (cos x) ^+ 2 + (sin x) ^+ 2 = 1. +Proof. +set v := LHS; pattern x in v; move: @v; set f := (X in let _ := X x in _) => /=. +apply: (@eq_trans _ _ (f 0)); last by rewrite /f sin0 cos0 expr1n expr0n addr0. +apply: is_derive_0_is_cst => {}x. +apply: trigger_derive; rewrite /GRing.scale /=. +by rewrite mulrN ![sin x * _]mulrC -opprD addrC subrr. +Qed. + +Lemma cos_max x : `| cos x | <= 1. +Proof. +rewrite -(expr_le1 (_ : 0 < 2)%nat) // -normrX ger0_norm ?exprn_even_ge0 //. +by rewrite -(cos2Dsin2 x) ler_addl ?sqr_ge0. +Qed. + +Lemma cos_geN1 x : -1 <= cos x. +Proof. by rewrite ler_oppl; have /ler_normlP[] := cos_max x. Qed. + +Lemma cos_le1 x : cos x <= 1. +Proof. by have /ler_normlP[] := cos_max x. Qed. + +Lemma sin_max x : `| sin x | <= 1. +Proof. +rewrite -(expr_le1 (_ : 0 < 2)%nat) // -normrX ger0_norm ?exprn_even_ge0 //. +by rewrite -(cos2Dsin2 x) ler_addr ?sqr_ge0. +Qed. + +Lemma sin_geN1 x : -1 <= sin x. +Proof. by rewrite ler_oppl; have /ler_normlP[] := sin_max x. Qed. + +Lemma sin_le1 x : sin x <= 1. +Proof. by have /ler_normlP[] := sin_max x. Qed. + +Fact sinD_cosD x y : + (sin (x + y) - (sin x * cos y + cos x * sin y)) ^+ 2 + + (cos (x + y) - (cos x * cos y - sin x * sin y)) ^+ 2 = 0. +Proof. +set v := LHS; pattern x in v; move: @v; set f := (X in let _ := X x in _) => /=. +apply: (@eq_trans _ _ (f 0)); last first. + by rewrite /f cos0 sin0 !(mul1r, mul0r, add0r, subr0, subrr, expr0n). +apply: is_derive_0_is_cst => {}x. +by apply: trigger_derive; rewrite /GRing.scale /=; nsatz. +Qed. + +Lemma sinD x y : sin (x + y) = sin x * cos y + cos x * sin y. +Proof. +have /eqP := sinD_cosD x y. +rewrite paddr_eq0 => [/andP[]||]; try exact: sqr_ge0. +by rewrite sqrf_eq0 subr_eq0 => /eqP. +Qed. + +Lemma cosD x y : cos (x + y) = cos x * cos y - sin x * sin y. +Proof. +have /eqP := sinD_cosD x y. +rewrite paddr_eq0 => [/andP[_]||]; try exact: sqr_ge0. +by rewrite sqrf_eq0 subr_eq0 => /eqP. +Qed. + +Lemma sin2cos2 x : sin x ^+ 2 = 1 - cos x ^+ 2. +Proof. by move/eqP: (cos2Dsin2 x); rewrite eq_sym addrC -subr_eq => /eqP. Qed. + +Lemma cos2sin2 x : cos x ^+ 2 = 1 - sin x ^+ 2. +Proof. by move/eqP: (cos2Dsin2 x); rewrite eq_sym -subr_eq => /eqP. Qed. + +Lemma sin_mulr2n x : sin (x *+ 2) = (cos x * sin x) *+ 2. +Proof. by rewrite mulr2n sinD mulrC -mulr2n. Qed. + +Lemma cos_mulr2n x : cos (x *+ 2) = cos x ^+2 *+ 2 - 1. +Proof. by rewrite mulr2n cosD -!expr2 sin2cos2 opprB addrA mulr2n. Qed. + +Fact sinN_cosN x : + (sin (- x) + sin x) ^+ 2 + (cos (- x) - cos x) ^+ 2 = 0. +Proof. +set v := LHS; pattern x in v; move: @v; set f := (X in let _ := X x in _) => /=. +apply: (@eq_trans _ _ (f 0)); last first. + by rewrite /f oppr0 cos0 sin0 !(addr0, subrr, expr0n). +apply: is_derive_0_is_cst => {}x. +by apply: trigger_derive; rewrite /GRing.scale /=; nsatz. +Qed. + +Lemma sinN x : sin (- x) = - sin x. +Proof. +have /eqP := sinN_cosN x. +rewrite paddr_eq0 => [/andP[]||]; try exact: sqr_ge0. +by rewrite sqrf_eq0 addr_eq0 => /eqP. +Qed. + +Lemma cosN x : cos (- x) = cos x. +Proof. +have /eqP := sinN_cosN x. +rewrite paddr_eq0 => [/andP[_]||]; try exact: sqr_ge0. +by rewrite sqrf_eq0 subr_eq0 => /eqP. +Qed. + +Lemma sin_sg x y : sin (Num.sg x * y) = Num.sg x * sin y. +Proof. by case: sgrP; rewrite ?mul1r ?mulN1r ?sinN // !mul0r sin0. Qed. + +Lemma cos_sg x y : x != 0 -> cos (Num.sg x * y) = cos y. +Proof. by case: sgrP; rewrite ?mul1r ?mulN1r ?cosN. Qed. + +Lemma cosB x y : cos (x - y) = cos x * cos y + sin x * sin y. +Proof. by rewrite cosD cosN sinN mulrN opprK. Qed. + +Lemma sinB x y : sin (x - y) = sin x * cos y - cos x * sin y. +Proof. by rewrite sinD cosN sinN mulrN. Qed. + +Lemma norm_cos_eq1 x : (`|cos x| == 1) = (sin x == 0). +Proof. +rewrite -sqrf_eq0 -sqrp_eq1 // -normrX ger0_norm ?exprn_even_ge0 //. +by rewrite [X in _ = (X == _)]sin2cos2 subr_eq0 eq_sym. +Qed. + +Lemma norm_sin_eq1 x : (`|sin x| == 1) = (cos x == 0). +Proof. +rewrite -sqrf_eq0 -sqrp_eq1 // -normrX ger0_norm ?exprn_even_ge0 //. +by rewrite [X in _ = (X == _)]cos2sin2 subr_eq0 eq_sym. +Qed. + +Lemma cos1sin0 x : `|cos x| = 1 -> sin x = 0. +Proof. by move/eqP; rewrite norm_cos_eq1 => /eqP. Qed. + +Lemma sin1cos0 x : `|sin x| = 1 -> cos x = 0. +Proof. by move/eqP; rewrite norm_sin_eq1 => /eqP. Qed. + +Lemma sin0cos1 x : sin x = 0 -> `|cos x| = 1. +Proof. by move/eqP; rewrite -norm_cos_eq1 => /eqP. Qed. + +Lemma cos_norm x : cos `|x| = cos x. +Proof. by case: (ler0P x); rewrite ?cosN. Qed. + +End CosSin. +Arguments sin {R}. +Arguments cos {R}. + +Section Pi. +Variable R : realType. +Implicit Types (x y : R) (n k : nat). + +Definition pi : R := get [set x | 0 <= x <= 2 /\ cos x = 0] *+ 2. + +Lemma pihalfE : pi / 2 = get [set x | 0 <= x <= 2 /\ cos x = 0]. +Proof. by rewrite /pi -(mulr_natr (get _)) -mulrA divff ?mulr1. Qed. + +Lemma cos2_lt0 : cos 2 < 0 :> R. +Proof. +rewrite -(opprK (cos _)) oppr_lt0; have /cvgN h := @cvg_cos_coeff' R 2. +rewrite -(cvg_lim (@Rhausdorff R) h). +apply: (@lt_trans _ _ (\sum_(0 <= i < 3) - cos_coeff' 2 i)). + do 3 rewrite big_nat_recl//; rewrite big_nil addr0 3!cos_coeff'E double0. + rewrite cos_coeff_2_0 cos_coeff_2_2 -muln2 cos_coeff_2_4 addrA -(opprD 1). + rewrite opprB -(@natrB _ 2 1)// subn1/= -[in X in X - _](@divff _ 3%:R)//. + by rewrite -mulrBl divr_gt0// -natrB. +rewrite -seriesN lt_sum_lim_series //. + by move/cvgP in h; by rewrite seriesN. +move=> d. +rewrite /cos_coeff' 2!exprzD_nat (exprSz _ d.*2) -[in (-1) ^ d.*2](muln2 d). +rewrite -(exprnP _ (d * 2)) (exprM (-1)) sqrr_sign 2!mulr1 -exprSzr. +rewrite (_ : 4 = 2 * 2)%N // -(exprnP _ (2 * 2)) (exprM (-1)) sqrr_sign. +rewrite mul1r [(-1) ^ 3](_ : _ = -1) ?mulN1r ?mulNr ?opprK; last first. + by rewrite -exprnP 2!exprS expr1 mulrN1 opprK mulr1. +rewrite subr_gt0. +rewrite addnS doubleS -[X in 2 ^+ X]addn2 exprD -mulrA ltr_pmul2l ?exprn_gt0//. +rewrite factS factS 2!natrM mulrA invfM !mulrA. +rewrite ltr_pdivr_mulr ?ltr0n ?fact_gt0// mulVf ?pnatr_eq0 ?gtn_eqF ?fact_gt0//. +rewrite ltr_pdivr_mulr ?mul1r //. +by rewrite expr2 -!natrM ltr_nat !mulSn !add2n mul0n !addnS. +Qed. + +Lemma cos_exists : exists2 pih : R, 0 <= pih <= 2 & cos pih = 0. +Proof. +have /IVT[]// : minr (cos 0) (cos 2) <= (0 : R) <= maxr (cos 0) (cos 2). + by rewrite /minr /maxr cos0 ltNge cos_le1/= ler01 (ltW cos2_lt0). +by move=> *; apply: continuous_cos. +by move=> pih /itvP pihI chpi_eq0; exists pih; rewrite ?pihI. +Qed. + +Lemma sin2_gt0 x : 0 < x < 2 -> 0 < sin x. +Proof. +move=> /andP[x_gt0 x_lt2]. +have sinx := @cvg_sin_coeff' _ x. +rewrite -(cvg_lim (@Rhausdorff R) sinx). +rewrite [X in X < _](_ : 0 = \sum_(0 <= i < 0) sin_coeff' x i :> R); last first. + by rewrite big_nil. +rewrite lt_sum_lim_series //; first by move/cvgP in sinx. +move=> d. +rewrite /sin_coeff' 2!exprzD_nat (exprSz _ d.*2) -[in (-1) ^ d.*2](muln2 d). +rewrite -(exprnP _ (d * 2)) (exprM (-1)) sqrr_sign 2!mulr1 -exprSzr. +rewrite !add0n!mul1r mulN1r -[d.*2.+1]addn1 doubleD -addSn exprD. +rewrite -(ffact_fact (leq_addl _ _)) addnK. +rewrite mulNr -!mulrA -mulrBr mulr_gt0 ?exprn_gt0 //. +set u := _.+1. +rewrite natrM invfM. +rewrite -[X in _ < X - _]mul1r !mulrA -mulrBl divr_gt0 //; last first. + by rewrite (ltr_nat _ 0) fact_gt0. +rewrite subr_gt0. +set v := _ ^_ _; rewrite -[X in _ < X](divff (_ : v%:R != 0)); last first. + by rewrite lt0r_neq0 // (ltr_nat _ 0) ffact_gt0 leq_addl. +rewrite ltr_pmul2r; last by rewrite invr_gt0 (ltr_nat _ 0) ffact_gt0 leq_addl. +rewrite {}/v !addnS addn0 !ffactnS ffactn0 muln1 /= natrM. +by rewrite (ltr_pmul (ltW _ ) (ltW _)) // (lt_le_trans x_lt2) // ler_nat. +Qed. + +Lemma cos_pihalf_uniq x y : + 0 <= x <= 2 -> cos x = 0 -> 0 <= y <= 2 -> cos y = 0 -> x = y. +Proof. +wlog xLy : x y / x <= y => [H xB cx0 yB cy0|]. + by case: (lerP x y) => [/H //| /ltW /H H1]; [exact|exact/esym/H1]. +move=> /andP[x_ge0 x_le2] cx0 /andP[y_ge0 y_le2] cy0. +case: (x =P y) => // /eqP xDy. +have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy. +have /(Rolle xLLs)[x1 _|x1 _|x1 x1I [_ x1D]] : cos x = cos y by rewrite cy0. +- exact: derivable_cos. +- exact: continuous_cos. +- have [_ /esym/eqP] := is_derive_cos x1; rewrite x1D oppr_eq0 => /eqP Hs. + suff : 0 < sin x1 by rewrite Hs ltxx. + apply/sin2_gt0/andP; split. + + by rewrite (le_lt_trans x_ge0)// (itvP x1I). + + by rewrite (lt_le_trans _ y_le2)// (itvP x1I). +Qed. + +Lemma pihalf_02_cos_pihalf : 0 <= pi / 2 <= 2 /\ cos (pi / 2) = 0. +Proof. +have [x ? ?] := cos_exists; rewrite pihalfE. +by case: xgetP => [_->[]//|/(_ x)/=]; tauto. +Qed. + +Lemma pihalf_02 : 0 < pi / 2 < 2. +Proof. +have [pih02 cpih] := pihalf_02_cos_pihalf. +rewrite 2!lt_neqAle andbCA -andbA pih02 andbT; apply/andP; split. + by apply/eqP => pih2; have := cos2_lt0; rewrite -pih2 cpih ltxx. +apply/eqP => pih0; have := @cos0 R. +by rewrite pih0 cpih; apply/eqP; rewrite eq_sym oner_eq0. +Qed. + +Lemma pi_gt0 : 0 < pi. +Proof. +by rewrite -[pi](divfK (_ : 2 != 0)) // mulr_gt0 //; case/andP: pihalf_02. +Qed. + +Lemma pi_ge0 : 0 <= pi. Proof. exact: (ltW pi_gt0). Qed. + +Lemma sin_gt0_pihalf x : 0 < x < pi / 2 -> 0 < sin x. +Proof. +move=> /andP[x_gt0 xLpi]. +apply: sin2_gt0; rewrite x_gt0 /=. +by apply: lt_trans xLpi _; have /andP[] := pihalf_02. +Qed. + +Lemma cos_gt0_pihalf x : -(pi / 2) < x < pi / 2 -> 0 < cos x. +Proof. +wlog : x / 0 <= x => [Hw|x_ge0]. + case: (leP 0 x) => [/Hw//| x_lt_0]. + rewrite -{-1}[x]opprK ltr_oppl andbC [-- _ < _]ltr_oppl cosN. + by apply: Hw => //; rewrite oppr_cp0 ltW. +move=> /andP[x_gt0 xLpi2]; case: (ler0P (cos x)) => // cx_le0. +have /IVT[]// : minr (cos 0) (cos x) <= 0 <= maxr (cos 0) (cos x). + by rewrite cos0 /minr /maxr !ifN ?cx_le0 //= -leNgt (le_trans cx_le0). +- by move=> *; apply: continuous_cos. +move=> x1 /itvP Hx1 cx1_eq0. +suff x1E : x1 = pi/2. + have : x1 < pi / 2 by apply: le_lt_trans xLpi2; rewrite Hx1. + by rewrite x1E ltxx. +have /andP[pi2_gt0 pi2L2] := pihalf_02. +apply: cos_pihalf_uniq=> //; last by case pihalf_02_cos_pihalf => _ ->. + by rewrite Hx1 ltW // (lt_trans _ pi2L2) // (le_lt_trans _ xLpi2) // Hx1. +by rewrite !ltW. +Qed. + +Lemma cos_pihalf : cos (pi / 2) = 0. Proof. exact: pihalf_02_cos_pihalf.2. Qed. + +Lemma sin_pihalf : sin (pi / 2) = 1. +Proof. +have := cos2Dsin2 (pi / 2); rewrite cos_pihalf expr0n add0r. +rewrite -[in X in _ = X -> _](expr1n _ 2%N) => /eqP; rewrite -subr_eq0 subr_sqr. +rewrite mulf_eq0=> /orP[|]; first by rewrite subr_eq0=> /eqP. +rewrite addr_eq0 => /eqP spi21. +by have := sin2_gt0 pihalf_02; rewrite spi21 ltr0N1. +Qed. + +Lemma cos_ge0_pihalf x : -(pi / 2) <= x <= pi / 2 -> 0 <= cos x. +Proof. +rewrite le_eqVlt; case: (_ =P x) => /= [<-|_]. + by rewrite cosN cos_pihalf. +rewrite le_eqVlt; case: (x =P _) => /= [->|_ H]; first by rewrite cos_pihalf. +by rewrite ltW //; apply: cos_gt0_pihalf. +Qed. + +Lemma cospi : cos pi = - 1. +Proof. +by rewrite /pi mulr2n cosD -pihalfE sin_pihalf mulr1 cos_pihalf mulr0 add0r. +Qed. + +Lemma sinpi : sin pi = 0. +Proof. +have := sinD (pi / 2) (pi / 2); rewrite cos_pihalf mulr0 mul0r. +by rewrite -mulrDl -mulr2n -mulr_natr -mulrA divff// mulr1 addr0. +Qed. + +Lemma cos2pi : cos (pi *+ 2) = 1. +Proof. by rewrite mulr2n cosD cospi sinpi !mulrN1 mulr0 subr0 opprK. Qed. + +Lemma sin2pi : sin (pi *+ 2) = 0. +Proof. by rewrite mulr2n sinD sinpi cospi !mulrN1 mulr0 oppr0 addr0. Qed. + +Lemma sinDpi : alternating sin pi. +Proof. by move=> a; rewrite sinD cospi mulrN1 sinpi mulr0 addr0. Qed. + +Lemma cosDpi : alternating cos pi. +Proof. by move=> a; rewrite cosD cospi mulrN1 sinpi mulr0 subr0. Qed. + +Lemma sinD2pi : periodic sin (pi *+ 2). +Proof. by move=> a; rewrite sinD cos2pi sin2pi mulr0 mulr1 addr0. Qed. + +Lemma cosD2pi : periodic cos (pi *+ 2). +Proof. by move=> a; rewrite cosD cos2pi mulr1 sin2pi mulr0 subr0. Qed. + +Lemma cosDpihalf a : cos (a + pi / 2) = - sin a. +Proof. by rewrite cosD cos_pihalf mulr0 add0r sin_pihalf mulr1. Qed. + +Lemma cosBpihalf a : cos (a - pi / 2) = sin a. +Proof. by rewrite cosB cos_pihalf mulr0 add0r sin_pihalf mulr1. Qed. + +Lemma sinDpihalf a : sin (a + pi / 2) = cos a. +Proof. by rewrite sinD cos_pihalf mulr0 add0r sin_pihalf mulr1. Qed. + +Lemma sinBpihalf a : sin (a - pi / 2) = - cos a. +Proof. by rewrite sinB cos_pihalf mulr0 add0r sin_pihalf mulr1. Qed. + +Lemma sin_ge0_pi x : 0 <= x <= pi -> 0 <= sin x. +Proof. +move=> xI; rewrite -cosBpihalf cos_ge0_pihalf //. +by rewrite ler_subr_addl subrr ler_sub_addr -mulr2n -[_ *+ 2]mulr_natr divfK. +Qed. + +Lemma sin_gt0_pi x : 0 < x < pi -> 0 < sin x. +Proof. +move=> xI; rewrite -cosBpihalf cos_gt0_pihalf //. +by rewrite ltr_subr_addl subrr ltr_sub_addr -mulr2n -[_ *+ 2]mulr_natr divfK. +Qed. + +Lemma ltr_cos : {in `[0, pi] &, {mono cos : x y /~ y < x}}. +Proof. +move=> x y; rewrite !in_itv/= le_eqVlt; case: eqP => [<- _|_] /=. + rewrite cos0 le_eqVlt; case: eqP => /= [<- _|_ /andP[y_gt0 gLpi]]. + by rewrite cos0 !ltxx. + rewrite y_gt0; apply/idP. + suff : cos y != 1 by case: ltrgtP (cos_le1 y). + rewrite -cos0 eq_sym; apply/eqP => /Rolle [||x1 _|x1 /itvP x1I [_ x1D]] //. + exact: continuous_cos. + case: (is_derive_cos x1) => _ /eqP; rewrite x1D eq_sym oppr_eq0 => /eqP s_eq0. + suff : 0 < sin x1 by rewrite s_eq0 ltxx. + by apply: sin_gt0_pi; rewrite x1I /= (lt_le_trans (_ : _ < y)) ?x1I // yI. +rewrite le_eqVlt; case: eqP => [-> _ /andP[y_ge0]|/= _ /andP[x_gt0 x_ltpi]] /=. + rewrite cospi le_eqVlt; case: eqP => /= [-> _|/eqP yDpi y_ltpi]. + by rewrite cospi ltxx. + by rewrite ltNge cos_geN1 ltNge ltW. +rewrite le_eqVlt; case: eqP => [<- _|_] /=. + rewrite cos0 [_ < 0]ltNge ltW //=. + by apply/idP/negP; rewrite -leNgt cos_le1. +rewrite le_eqVlt; case: eqP => /= [-> _ | _ /andP[y_gt0 y_ltpi]]. + rewrite cospi x_ltpi; apply/idP. + suff : cos x != -1 by case: ltrgtP (cos_geN1 x). + rewrite -cospi; apply/eqP => /Rolle [||x1 _|x1 /itvP x1I [_ x1D]] //. + exact: continuous_cos. + case: (is_derive_cos x1) => _ /eqP; rewrite x1D eq_sym oppr_eq0 => /eqP s_eq0. + suff : 0 < sin x1 by rewrite s_eq0 ltxx. + by apply: sin_gt0_pi; rewrite x1I /= (lt_le_trans (_ : _ < x)) ?x1I. +wlog xLy : x y x_gt0 x_ltpi y_gt0 y_ltpi / x <= y => [H | ]. + case: (lerP x y) => [/H //->//|yLx]. + by rewrite !ltNge ltW ?(ltW yLx) // H // ltW. +case: (x =P y) => [->| /eqP xDy]; first by rewrite ltxx. +have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy. +rewrite xLLs -subr_gt0 -opprB; rewrite -subr_gt0 in xLLs; apply/idP. +have [x1 _|z /itvP zI ->] := @MVT _ cos (-sin) _ _ xLy. + exact: continuous_cos. +rewrite -mulNr opprK mulr_gt0 //; apply: sin_gt0_pi. +by rewrite (lt_le_trans x_gt0) ?zI //= (le_lt_trans _ y_ltpi) ?zI. +Qed. + +Lemma ltr_sin : {in `[ (- (pi/2)), pi/2] &, {mono sin : x y / x < y}}. +Proof. +move=> x y /itvP xpi /itvP ypi; rewrite -[sin x]opprK ltr_oppl. +rewrite -!cosDpihalf -[x < y](ltr_add2r (pi /2)) ltr_cos// !in_itv/=. +- by rewrite -ler_subl_addr sub0r xpi/= [X in _ <= X]splitr ler_add2r xpi. +- by rewrite -ler_subl_addr sub0r ypi/= [X in _ <= X]splitr ler_add2r ypi. +Qed. + +Lemma cos_inj : {in `[0,pi] &, injective (@cos R)}. +Proof. +move=> x y x0pi y0pi xy; apply/eqP; rewrite eq_le; apply/andP; split. +- by have := ltr_cos y0pi x0pi; rewrite xy ltxx => /esym/negbT; rewrite -leNgt. +- by have := ltr_cos x0pi y0pi; rewrite xy ltxx => /esym/negbT; rewrite -leNgt. +Qed. + +Lemma sin_inj : {in `[(- (pi/2)), (pi/2)] &, injective sin}. +Proof. +move=> x y /itvP xpi /itvP ypi sinE; have : - sin x = - sin y by rewrite sinE. +rewrite -!cosDpihalf => /cos_inj h; apply/(addIr (pi/2))/h; rewrite !in_itv/=. +- by rewrite -ler_subl_addr sub0r xpi/= [X in _ <= X]splitr ler_add2r xpi. +- by rewrite -ler_subl_addr sub0r ypi/= [X in _ <= X]splitr ler_add2r ypi. +Qed. + +End Pi. + +Section Tan. +Variable R : realType. +Notation pi := (@pi R). + +Definition tan (x : R) := sin x / cos x. + +Lemma tan0 : tan 0 = 0 :> R. +Proof. by rewrite /tan sin0 cos0 mul0r. Qed. + +Lemma tanpi : tan pi = 0. +Proof. by rewrite /tan sinpi mul0r. Qed. + +Lemma tanN x : tan (- x) = - tan x. +Proof. by rewrite /tan sinN cosN mulNr. Qed. + +Lemma tanD x y : cos x != 0 -> cos y != 0 -> + tan (x + y) = (tan x + tan y) / (1 - tan x * tan y). +Proof. +move=> cxNZ cyNZ. +rewrite /tan sinD cosD !addf_div // [sin y * cos x]mulrC -!mulrA -invfM. +congr (_ / _). +rewrite mulrBr mulr1 !mulrA. +rewrite -[_ * _ * sin x]mulrA [cos x * (_ * _)]mulrC mulfK //. +by rewrite -[_ * _ * sin y]mulrA [cos y * (_ * _)]mulrC mulfK. +Qed. + +Lemma tan_mulr2n x : + cos x != 0 -> tan (x *+ 2) = tan x *+ 2 / (1 - tan x ^+ 2). +Proof. +move=> cxNZ. +rewrite /tan cos_mulr2n sin_mulr2n. +rewrite !mulr2n exprMn exprVn -[in RHS](divff (_ : 1 != 0)) //. +rewrite -mulNr !addf_div ?sqrf_eq0 //. +rewrite mul1r mulr1 -!mulrA -invfM -expr2; congr (_ / _). + by rewrite [cos x * _]mulrC. +rewrite mulrCA mulrA mulfK ?sqrf_eq0 // [X in _ = _ - X]sin2cos2. +by rewrite opprB addrA. +Qed. + +Lemma cos2_tan2 x : cos x != 0 -> (cos x) ^- 2 = 1 + (tan x) ^+ 2. +Proof. +move=> cosx. +rewrite /tan exprMn [X in _ = 1 + X * _]sin2cos2 mulrBl -exprMn divff //. +by rewrite expr1n addrCA subrr addr0 mul1r exprVn. +Qed. + +Lemma tan_pihalf : tan (pi / 2) = 0. +Proof. by rewrite /tan cos_pihalf invr0 mulr0. Qed. + +Lemma tan_piquarter : tan (pi / 4%:R) = 1. +Proof. +rewrite /tan -cosBpihalf (splitr (pi / 2)) opprD addrA -mulrA -invfM -natrM. +rewrite subrr sub0r cosN divff// gt_eqF// cos_gt0_pihalf//. +rewrite ltr_pmul2l ?pi_gt0// ltf_pinv ?qualifE// ltr_nat andbT. +by rewrite (@lt_trans _ _ 0)// ?oppr_lt0 ?divr_gt0 ?pi_gt0//. +Qed. + +Lemma tanDpi x : tan (x + pi) = tan x. +Proof. by rewrite /tan cosDpi sinDpi mulNr invrN mulrN opprK. Qed. + +Lemma continuous_tan x : cos x != 0 -> {for x, continuous tan}. +Proof. +move=> cxNZ. +apply: continuousM; first exact: continuous_sin. +exact/(continuousV cxNZ)/continuous_cos. +Qed. + +Lemma is_derive_tan x : + cos x != 0 -> is_derive x 1 tan ((cos x)^-2). +Proof. +move=> cxNZ; apply: trigger_derive. +rewrite /= ![_ *: - _]mulrN mulNr mulrN opprK [_^-1 *: _]mulVf //. +rewrite mulrCA -expr2 [X in _ * X + _ = _]sin2cos2. +by rewrite mulrBr mulr1 mulVf ?sqrf_eq0 // subrK. +Qed. + +Lemma derivable_tan x : cos x != 0 -> derivable tan x 1. +Proof. by move=> /is_derive_tan[]. Qed. + +Lemma ltr_tan : {in `](- (pi/2)), (pi/2)[ &, {mono tan : x y / x < y}}. +Proof. +move=> x y. +wlog xLy : x y / x <= y => [H | ] xB yB. + case: (lerP x y) => [/H //->//|yLx]. + by rewrite !ltNge ltW ?(ltW yLx) // H // ltW. +case: (x =P y) => [->| /eqP xDy]; first by rewrite ltxx. +have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy. +rewrite -subr_gt0 xLLs; rewrite -subr_gt0 in xLLs; apply/idP. +have [x1 /itvP x1I|z /itvP zI|] := @MVT _ tan (fun x => (cos x) ^-2) _ _ xLy. +- apply: is_derive_tan. + rewrite gt_eqF // cos_gt0_pihalf // (@lt_le_trans _ _ x) ?x1I ?(itvP xB)//=. + by rewrite (@le_lt_trans _ _ y) ?x1I ?(itvP yB). +- apply: continuous_tan. + rewrite gt_eqF // cos_gt0_pihalf // (@lt_le_trans _ _ x) ?zI ?(itvP xB)//=. + by rewrite (@le_lt_trans _ _ y) ?zI ?(itvP yB). +- move=> x1 /itvP x1I ->. + rewrite mulr_gt0 // invr_gt0 // exprn_gte0 // cos_gt0_pihalf //. + rewrite (@lt_le_trans _ _ x) ?x1I ?(itvP xB)//=. + by rewrite (@le_lt_trans _ _ y) ?x1I ?(itvP yB). +Qed. + +Lemma tan_inj : {in `](- (pi/2)), (pi/2)[ &, injective tan}. +Proof. +move=> x y xB yB tanE. +by case: (ltrgtP x y); rewrite // -ltr_tan ?tanE ?ltxx. +Qed. + +End Tan. +Arguments tan {R}. + +Hint Extern 0 (is_derive _ _ tan _) => + (eapply is_derive_tan; first by []) : typeclass_instances. + +Section Acos. +Variable R : realType. +Local Notation pi := (@pi R). + +Definition acos (x : R) := get [set y | 0 <= y <= pi /\ cos y = x]. + +Lemma acos_def x : + -1 <= x <= 1 -> 0 <= acos x <= pi /\ cos (acos x) = x. +Proof. +move=> xB; rewrite /acos; case: xgetP => //= He. +pose f y := cos y - x. +have /(IVT (@pi_ge0 _))[] // : minr (f 0) (f pi) <= 0 <= maxr (f 0) (f pi). + rewrite /f cos0 cospi /minr /maxr ltr_add2r -subr_lt0 opprK (_ : 1 + 1 = 2)//. + by rewrite ltrn0 subr_le0 subr_ge0. +- move=> y y0pi. + by apply: continuousB; [exact: continuous_cos|exact: cst_continuous]. +- rewrite /f => x1 /itvP x1I /eqP; rewrite subr_eq0 => /eqP cosx1E. + by case: (He x1); rewrite !x1I. +Qed. + +Lemma acos_ge0 x : -1 <= x <= 1 -> 0 <= acos x. +Proof. by move=> /acos_def[/andP[]]. Qed. + +Lemma acos_lepi x : -1 <= x <= 1 -> acos x <= pi. +Proof. by move=> /acos_def[/andP[]]. Qed. + +Lemma acosK : {in `[(-1),1], cancel acos cos}. +Proof. by move=> x; rewrite in_itv/==> /acos_def[/andP[]]. Qed. + +Lemma acos_gt0 x : -1 <= x < 1 -> 0 < acos x. +Proof. +move=> /andP[x_geN1 x_lt1]; move: (x_lt1). +have : 0 <= acos x by rewrite acos_ge0 // x_geN1 ltW. +have : cos (acos x) = x by rewrite acosK// in_itv/= x_geN1/= ltW. +by case: ltrgt0P => // ->; rewrite cos0 => ->; rewrite ltxx. +Qed. + +Lemma acos_ltpi x : -1 < x <= 1 -> acos x < pi. +Proof. +move=> /andP[x_gtN1 x_le1]; move: (x_gtN1). +have : acos x <= pi by rewrite acos_lepi // x_le1 ltW. +have : cos (acos x) = x by rewrite acosK// in_itv/= x_le1 ltW. +by case: (ltrgtP (acos x) pi) => // ->; rewrite cospi => ->; rewrite ltxx. +Qed. + +Lemma cosK : {in `[0, pi], cancel cos acos}. +Proof. +move=> x xB; apply: cos_inj => //; rewrite ?acosK//; last first. + by move: xB; rewrite !in_itv/= => /andP[? ?];rewrite cos_geN1 cos_le1. +move: xB; rewrite !in_itv/= => /andP[? ?]. +by rewrite acos_ge0 ?acos_lepi ?cos_geN1 ?cos_le1. +Qed. + +Lemma sin_acos x : -1 <= x <= 1 -> sin (acos x) = Num.sqrt (1 - x^+2). +Proof. +move=> xB. +rewrite -[LHS]ger0_norm; last by rewrite sin_ge0_pi // acos_ge0 ?acos_lepi. +by rewrite -sqrtr_sqr sin2cos2 acosK. +Qed. + +Lemma continuous_acos x : -1 < x < 1 -> {for x, continuous acos}. +Proof. +move=> /andP[x_gtN1 x_lt1]; rewrite -[x]acosK; first last. + by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB. +apply: nbhs_singleton (near_can_continuous _ _); last first. + by near=> z; apply: continuous_cos. +have /near_in_itv aI : acos x \in `]0, pi[. + suff : 0 < acos x < pi by []. + by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT. +near=> z; apply: cosK. +suff /itvP zI : z \in `]0, pi[ by have : 0 <= z <= pi by rewrite ltW ?zI. +by near: z. +Grab Existential Variables. all: end_near. Qed. + +Lemma is_derive1_acos (x : R) : + -1 < x < 1 -> is_derive x 1 acos (- (Num.sqrt (1 - x ^+ 2))^-1). +Proof. +move=> /andP[x_gtN1 x_lt1]; rewrite -sin_acos ?ltW // -invrN. +rewrite -{1}[x]acosK; last by have : -1 <= x <= 1 by rewrite ltW // ltW. +have /near_in_itv aI : acos x \in `]0, pi[. + suff : 0 < acos x < pi by []. + by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT. +apply: (@is_derive_inverse R cos). +- near=> z; apply: cosK. + suff /itvP zI : z \in `]0, pi[ by have : 0 <= z <= pi by rewrite ltW ?zI. + by near: z. +- by near=> z; apply: continuous_cos. +- rewrite oppr_eq0 sin_acos ?ltW // sqrtr_eq0 // -ltNge subr_gt0. + rewrite -real_normK ?qualifE; last by case: ltrgt0P. + by rewrite exprn_cp1 // ltr_norml x_gtN1. +Grab Existential Variables. all: end_near. Qed. + +End Acos. + +Hint Extern 0 (is_derive _ 1 (@acos _) _) => + (eapply is_derive1_acos; first by []) : typeclass_instances. + +Section Asin. +Variable R : realType. +Notation pi := (@pi R). + +Definition asin (x : R) := get [set y | -(pi / 2) <= y <= pi / 2 /\ sin y = x]. + +Lemma asin_def x : + -1 <= x <= 1 -> -(pi / 2) <= asin x <= pi / 2 /\ sin (asin x) = x. +Proof. +move=> xB; rewrite /asin; case: xgetP => //= He. +pose f y := sin y - x. +have /IVT[] // : + minr (f (-(pi/2))) (f (pi/2)) <= 0 <= maxr (f (-(pi/2))) (f (pi/2)). + rewrite /f sinN sin_pihalf /minr /maxr ltr_add2r -subr_gt0 opprK. + by rewrite (_ : 1 + 1 = 2)// ltr0n/= subr_le0 subr_ge0. +- by rewrite -subr_ge0 opprK -splitr pi_ge0. +- by move=> *; apply: continuousB; [exact: continuous_sin| + exact: cst_continuous]. +- rewrite /f => x1 /itvP x1I /eqP; rewrite subr_eq0 => /eqP sinx1E. + by case: (He x1); rewrite !x1I. +Qed. + +Lemma asin_geNpi2 x : -1 <= x <= 1 -> -(pi / 2) <= asin x. +Proof. by move=> /asin_def[/andP[]]. Qed. + +Lemma asin_lepi2 x : -1 <= x <= 1 -> asin x <= pi / 2. +Proof. by move=> /asin_def[/andP[]]. Qed. + +Lemma asinK : {in `[(-1),1], cancel asin sin}. +Proof. by move=> x; rewrite in_itv/= => /asin_def[/andP[]]. Qed. + +Lemma asin_ltpi2 x : -1 <= x < 1 -> asin x < pi/2. +Proof. +move=> /andP[x_geN1 x_lt1]; move: (x_lt1). +have : asin x <= pi / 2 by rewrite asin_lepi2 // x_geN1 ltW. +have : sin (asin x) = x by rewrite asinK// in_itv/= x_geN1 ltW. +case: (ltrgtP _ ((pi / 2))) => // ->. +by rewrite sin_pihalf => <-; rewrite ltxx. +Qed. + +Lemma asin_gtNpi2 x : -1 < x <= 1 -> - (pi / 2) < asin x. +Proof. +move=> /andP[x_gtN1 x_le1]; move: (x_gtN1). +have : - (pi / 2) <= asin x by rewrite asin_geNpi2 // x_le1 ltW. +have : sin (asin x) = x by rewrite asinK// in_itv/= x_le1 ltW. +by case: (ltrgtP (asin x)) => //->; rewrite sinN sin_pihalf => <-; rewrite ltxx. +Qed. + +Lemma sinK : {in `[(- (pi / 2)), pi / 2], cancel sin asin}. +Proof. +move=> x; rewrite !in_itv/= => xB ; apply: sin_inj => //; last first. + by rewrite asinK// in_itv/= sin_geN1 sin_le1. +by rewrite in_itv/= asin_geNpi2/= ?asin_lepi2 ?sin_geN1 ?sin_le1. +Qed. + +Lemma cos_asin x : -1 <= x <= 1 -> cos (asin x) = Num.sqrt (1 - x^+2). +Proof. +move=> xB; rewrite -[LHS]ger0_norm; first by rewrite -sqrtr_sqr cos2sin2 asinK. +by apply: cos_ge0_pihalf; rewrite asin_lepi2 // asin_geNpi2. +Qed. + +Lemma continuous_asin x : -1 < x < 1 -> {for x, continuous asin}. +Proof. +move=> /andP[x_gtN1 x_lt1]; rewrite -[x]asinK; first last. + by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB. +apply: nbhs_singleton (near_can_continuous _ _); last first. + by near=> z; apply: continuous_sin. +have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[. + suff : - (pi / 2) < asin x < pi / 2 by []. + by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW. +near=> z; apply: sinK. +suff /itvP zI : z \in `](-(pi/2)), (pi/2)[. + by have : - (pi / 2) <= z <= pi / 2 by rewrite ltW ?zI. +by near: z. +Grab Existential Variables. all: end_near. Qed. + +Lemma is_derive1_asin (x : R) : + -1 < x < 1 -> is_derive x 1 asin ((Num.sqrt (1 - x ^+ 2))^-1). +Proof. +move=> /andP[x_gtN1 x_lt1]; rewrite -cos_asin ?ltW //. +rewrite -{1}[x]asinK; last by have : -1 <= x <= 1 by rewrite ltW // ltW. +have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[. + suff : -(pi/2) < asin x < pi/2 by []. + by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW. +apply: (@is_derive_inverse R sin). +- near=> z; apply: sinK. + suff /itvP zI : z \in `](-(pi/2)), (pi/2)[. + by have : - (pi / 2) <= z <= pi / 2 by rewrite ltW ?zI. + by near: z. +- by near=> z; exact: continuous_sin. +- rewrite cos_asin ?ltW // sqrtr_eq0 // -ltNge subr_gt0. + rewrite -real_normK ?qualifE; last by case: ltrgt0P. + by rewrite exprn_cp1 // ltr_norml x_gtN1. +Grab Existential Variables. all: end_near. Qed. + +End Asin. + +Hint Extern 0 (is_derive _ 1 (@asin _) _) => + (eapply is_derive1_asin; first by []) : typeclass_instances. + +Section Atan. +Variable R : realType. +Notation pi := (@pi R). + +Definition atan (x : R) := + get [set y | -(pi / 2) < y < pi / 2 /\ tan y = x]. + +(* Did not see how to use ITV like in the other *) +Lemma atan_def x : -(pi / 2) < atan x < pi / 2 /\ tan (atan x) = x. +Proof. +rewrite /atan; case: xgetP => //= He. +pose x1 := Num.sqrt (1 + x^+ 2) ^-1. +have ox2_gt0 : 0 < 1 + x^2. + by apply: lt_le_trans (_ : 1 <= _); rewrite ?ler_addl ?sqr_ge0. +have ox2_ge0 : 0 <= 1 + x^2 by rewrite ltW. +have x1B : -1 <= x1 <= 1. + rewrite -ler_norml /x1 ger0_norm ?sqrtr_ge0 //. + rewrite -[X in _ <= X]sqrtr1 ler_psqrt ?qualifE ?invr_gte0 //=. + by rewrite invf_cp1 // ler_addl sqr_ge0. +case: (He (Num.sg x * acos x1)); split; last first. + case: (x =P 0) => [->|/eqP xD0]; first by rewrite /tan sgr0 mul0r sin0 mul0r. + rewrite /tan sin_sg cos_sg // acosK ?sin_acos //. + rewrite /x1 sqr_sqrtr ?invr_ge0 //. + rewrite -{1}[_^-1 in X in X / _ = _]mul1r. + rewrite -{1}[X in X - _](divff (_: 1 != 0)) //. + rewrite -mulNr addf_div ?lt0r_neq0 //. + rewrite mul1r mulr1 [X in X - 1]addrC addrK // sqrtrM ?sqr_ge0 //. + rewrite sqrtrV // invrK // mulrA divfK //; last by rewrite sqrtr_eq0 -ltNge. + by rewrite sqrtr_sqr mulr_sg_norm. +rewrite -ltr_norml normrM. +have pi2 : 0 < pi / 2 by rewrite divr_gt0 // pi_gt0. +case: (x =P 0) => [->|/eqP xD0]; first by rewrite sgr0 normr0 mul0r. +rewrite normr_sg xD0 mul1r ltr_norml. +rewrite (@lt_le_trans _ _ 0) ?acos_ge0 ?oppr_cp0 //=. +rewrite -ltr_cos ?in_itv/= ?acos_ge0/= ?acos_lepi//; last first. + by rewrite divr_ge0 ?pi_ge0//= ler_pdivr_mulr// ler_pmulr ?pi_gt0// ler1n. +by rewrite cos_pihalf acosK // ?sqrtr_gt0 ?invr_gt0. +Qed. + +Lemma atan_gtNpi2 x : - (pi / 2) < atan x. +Proof. by case: (atan_def x) => [] /andP[]. Qed. + +Lemma atan_ltpi2 x : atan x < pi / 2. +Proof. by case: (atan_def x) => [] /andP[]. Qed. + +Lemma atanK : cancel atan tan. +Proof. by move=> x; case: (atan_def x). Qed. + +Lemma tanK : {in `](- (pi / 2)), (pi / 2)[ , cancel tan atan}. +Proof. +move=> x xB; apply tan_inj => //; rewrite ?atanK//. +by rewrite in_itv/= atan_gtNpi2 atan_ltpi2. +Qed. + +Lemma continuous_atan x : {for x, continuous atan}. +Proof. +rewrite -[x]atanK. +have /near_in_itv aI : atan x \in `](-(pi / 2)), (pi / 2)[. + suff : - (pi / 2) < atan x < pi / 2 by []. + by rewrite atan_gtNpi2 atan_ltpi2. +apply: nbhs_singleton (near_can_continuous _ _); last first. + by near=> z; apply/continuous_tan/lt0r_neq0/cos_gt0_pihalf; near: z. +by near=> z; apply: tanK; near: z. +Grab Existential Variables. all: end_near. Qed. + +Lemma cos_atan x : cos (atan x) = (Num.sqrt (1 + x ^+ 2)) ^-1. +Proof. +have cos_gt0 : 0 < cos (atan x). + by apply: cos_gt0_pihalf; rewrite atan_gtNpi2 atan_ltpi2. +have cosD0 : cos (atan x) != 0 by apply: lt0r_neq0. +have /eqP : cos (atan x) ^+2 = (Num.sqrt (1 + x ^+ 2))^-2. + by rewrite -[LHS]invrK cos2_tan2 // atanK sqr_sqrtr // addr_ge0 // sqr_ge0. +rewrite -exprVn eqf_sqr => /orP[] /eqP // cosE. +move: cos_gt0; rewrite cosE ltNge; case/negP. +by rewrite oppr_le0 invr_ge0 sqrtr_ge0. +Qed. + +Global Instance is_derive1_atan (x : R) : is_derive x 1 atan (1 + x ^+ 2)^-1. +Proof. +rewrite -{1}[x]atanK. +have cosD0 : cos (atan x) != 0. + by apply/lt0r_neq0/cos_gt0_pihalf; rewrite atan_gtNpi2 atan_ltpi2. +have /near_in_itv aI : atan x \in `](-(pi/2)), (pi/2)[. + suff : - (pi / 2) < atan x < pi / 2 by []. + by rewrite atan_gtNpi2 atan_ltpi2. +apply: (@is_derive_inverse R tan). +- by near=> z; apply: tanK; near: z. +- by near=> z; apply/continuous_tan/lt0r_neq0/cos_gt0_pihalf; near: z. +- by rewrite -[X in 1 + X ^+ 2]atanK -cos2_tan2 //; exact: is_derive_tan. +by apply/lt0r_neq0/(@lt_le_trans _ _ 1) => //; rewrite ler_addl sqr_ge0. +Grab Existential Variables. all: end_near. Qed. + +End Atan. +