The Trigonometric Functions
In this section, we explore the properties of the trigonometric functions which we previously defined.
First, we need a lemma on mappings.
Lemma maps_translation : forall y, maps_compacts_into (-∞,+∞) (-∞,+∞) (FId{+} [-C-]y).
End Lemmas.
Section Sine_and_Cosine.
Sine, cosine and tangent at 0.
Lemma Sin_zero : Sin 0 [=] 0.
Lemma Cos_zero : Cos 0 [=] 1.
Lemma Tan_zero : forall H, Tan 0 H [=] 0.
Continuity of sine and cosine are trivial.
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.
Lemma cos_sin_seq : forall n : N, cos_seq n [=] sin_seq (S n).
Lemma sin_cos_seq : forall n : N, sin_seq n [=] [--] (cos_seq (S n)).
Lemma Derivative_Sin : forall H, Derivative (-∞,+∞) H Sine Cosine.
Lemma Derivative_Cos : forall H, Derivative (-∞,+∞) H Cosine {--}Sine.
Section Sine_of_Sum.
We now prove the rule for the sine and cosine of the sum. These rules
have to be proved first as functional equalities, which is why we also
state the results in a function form (which we won't do in other
situations).
Let:
Let:
- F := fun y => Sine[o] (FId{+} [-C-]y);
- G := fun y => (Sine{*} [-C-] (Cos y)) {+} (Cosine{*} [-C-] (Sin y)).
Lemma Sin_plus_Taylor_bnd_lft : forall y : IR, Taylor_bnd (F' y).
Included.
Qed.
Lemma Sin_plus_Taylor_bnd_rht : forall y : IR, Taylor_bnd (G' y).
Lemma Sin_plus_eq : forall y n HaF HaG, F' y n 0 HaF [=] G' y n 0 HaG.
Lemma Sin_plus_der_lft : forall y n, Derivative_n n (-∞,+∞) CI (F y) (F' y n).
Lemma Sin_plus_der_rht : forall y n, Derivative_n n (-∞,+∞) CI (G y) (G' y n).
Lemma Sin_plus_fun : forall y : IR, ≈ (-∞,+∞) (F y) (G y).
End Sine_of_Sum.
Lemma Cos_plus_fun : forall y, ≈ (-∞,+∞) (Cosine[o]FId{+} [-C-]y) (Cosine{*} [-C-] (Cos y) {-}Sine{*} [-C-] (Sin y)).
End Sine_and_Cosine.