1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/transc/Trigonometric".
19 (* $Id: Trigonometric.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
25 (*#* *The Trigonometric Functions
27 In this section, we explore the properties of the trigonometric functions which we previously defined.
34 (*#* First, we need a lemma on mappings. *)
36 inline cic:/CoRN/transc/Trigonometric/maps_translation.con.
43 Section Sine_and_Cosine.
46 (*#* Sine, cosine and tangent at [Zero]. *)
48 inline cic:/CoRN/transc/Trigonometric/Sin_zero.con.
50 inline cic:/CoRN/transc/Trigonometric/Cos_zero.con.
53 Hint Resolve Sin_zero Cos_zero: algebra.
60 inline cic:/CoRN/transc/Trigonometric/Tan_zero.con.
63 Transparent Sine Cosine.
67 Continuity of sine and cosine are trivial.
70 inline cic:/CoRN/transc/Trigonometric/Continuous_Sin.con.
72 inline cic:/CoRN/transc/Trigonometric/Continuous_Cos.con.
75 The rules for the derivative of the sine and cosine function; we begin by proving that their defining sequences can be expressed in terms of one another.
78 inline cic:/CoRN/transc/Trigonometric/cos_sin_seq.con.
80 inline cic:/CoRN/transc/Trigonometric/sin_cos_seq.con.
82 inline cic:/CoRN/transc/Trigonometric/Derivative_Sin.con.
84 inline cic:/CoRN/transc/Trigonometric/Derivative_Cos.con.
87 Hint Resolve Derivative_Sin Derivative_Cos: derivate.
91 Hint Resolve Continuous_Sin Continuous_Cos: continuous.
99 We now prove the rule for the sine and cosine of the sum. These rules
100 have to be proved first as functional equalities, which is why we also
101 state the results in a function form (which we won't do in other
104 %\begin{convention}% Let:
105 - [F := fun y => Sine[o] (FId{+} [-C-]y)];
106 - [G := fun y => (Sine{*} [-C-] (Cos y)) {+} (Cosine{*} [-C-] (Sin y))].
113 inline cic:/CoRN/transc/Trigonometric/F.con.
115 inline cic:/CoRN/transc/Trigonometric/G.con.
117 inline cic:/CoRN/transc/Trigonometric/F'.con.
119 inline cic:/CoRN/transc/Trigonometric/G'.con.
159 inline cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_lft.con.
193 inline cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_rht.con.
195 inline cic:/CoRN/transc/Trigonometric/Sin_plus_eq.con.
197 inline cic:/CoRN/transc/Trigonometric/Sin_plus_der_lft.con.
199 inline cic:/CoRN/transc/Trigonometric/Sin_plus_der_rht.con.
201 inline cic:/CoRN/transc/Trigonometric/Sin_plus_fun.con.
211 inline cic:/CoRN/transc/Trigonometric/Cos_plus_fun.con.