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 *********************)
19 (* $Id: Trigonometric.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
21 include "transc/TaylorSeries.ma".
23 (*#* *The Trigonometric Functions
25 In this section, we explore the properties of the trigonometric functions which we previously defined.
32 (*#* First, we need a lemma on mappings. *)
34 inline procedural "cic:/CoRN/transc/Trigonometric/maps_translation.con" as lemma.
41 Section Sine_and_Cosine
44 (*#* Sine, cosine and tangent at [Zero]. *)
46 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_zero.con" as lemma.
48 inline procedural "cic:/CoRN/transc/Trigonometric/Cos_zero.con" as lemma.
51 Hint Resolve Sin_zero Cos_zero: algebra.
58 inline procedural "cic:/CoRN/transc/Trigonometric/Tan_zero.con" as lemma.
61 Transparent Sine Cosine.
65 Continuity of sine and cosine are trivial.
68 inline procedural "cic:/CoRN/transc/Trigonometric/Continuous_Sin.con" as lemma.
70 inline procedural "cic:/CoRN/transc/Trigonometric/Continuous_Cos.con" as lemma.
73 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.
76 inline procedural "cic:/CoRN/transc/Trigonometric/cos_sin_seq.con" as lemma.
78 inline procedural "cic:/CoRN/transc/Trigonometric/sin_cos_seq.con" as lemma.
80 inline procedural "cic:/CoRN/transc/Trigonometric/Derivative_Sin.con" as lemma.
82 inline procedural "cic:/CoRN/transc/Trigonometric/Derivative_Cos.con" as lemma.
85 Hint Resolve Derivative_Sin Derivative_Cos: derivate.
89 Hint Resolve Continuous_Sin Continuous_Cos: continuous.
97 We now prove the rule for the sine and cosine of the sum. These rules
98 have to be proved first as functional equalities, which is why we also
99 state the results in a function form (which we won't do in other
102 %\begin{convention}% Let:
103 - [F := fun y => Sine[o] (FId{+} [-C-]y)];
104 - [G := fun y => (Sine{*} [-C-] (Cos y)) {+} (Cosine{*} [-C-] (Sin y))].
111 inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
113 inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
115 inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/F'.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
117 inline procedural "cic:/CoRN/transc/Trigonometric/Sine_and_Cosine/Sine_of_Sum/G'.con" "Sine_and_Cosine__Sine_of_Sum__" as definition.
157 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_lft.con" as lemma.
191 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_Taylor_bnd_rht.con" as lemma.
193 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_eq.con" as lemma.
195 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_der_lft.con" as lemma.
197 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_der_rht.con" as lemma.
199 inline procedural "cic:/CoRN/transc/Trigonometric/Sin_plus_fun.con" as lemma.
209 inline procedural "cic:/CoRN/transc/Trigonometric/Cos_plus_fun.con" as lemma.