Inverse Trigonometric Functions
Definitions
We will now define arcsine, arccosine and arctangent as indefinite integrals and prove their main properties. We begin by proving that the appropriate indefinite integrals can be defined, then prove the main properties of the function.
Arccosine is defined in terms of arcsine by the relation ArcCos(x)=Pi[/]2-ArcSin(x).
Arcsine
Lemma ArcSin_def_lemma : Continuous ((⋅,⋅) [--]1 1) (( [-C-]1{-}FId{^}2) {!} [-C-] [--] (1 [/]2)).
Included.
Included.
Included.
Qed.
Lemma ArcSin_def_zero : (⋅,⋅) [--]1 1 0.
Definition ArcSin := ( [-S-]ArcSin_def_lemma) _ ArcSin_def_zero.
Lemma ArcSin_domain : forall x, [--]1 [<] x -> x [<] 1 -> Dom ArcSin x.
Lemma Continuous_ArcSin : Continuous ((⋅,⋅) [--]1 1) ArcSin.
Lemma Derivative_ArcSin : forall H,
Derivative ((⋅,⋅) [--]1 1) H ArcSin (( [-C-]1{-}FId{^}2) {!} [-C-] [--] (1 [/]2)).
Definition ArcCos := [-C-] (π [/]2) {-}ArcSin.
Lemma ArcCos_domain : forall x : IR, [--]1 [<] x -> x [<] 1 -> Dom ArcCos x.
Lemma Continuous_ArcCos : Continuous ((⋅,⋅) [--]1 1) ArcCos.
Lemma Derivative_ArcCos : forall H,
Derivative ((⋅,⋅) [--]1 1) H ArcCos {--} (( [-C-]1{-}FId{^}2) {!} [-C-] [--] (1 [/]2)).
Included.
Qed.
Lemma ArcTan_def_lemma : Continuous (-∞,+∞) {1/} ( [-C-]1{+}FId{^}2).
Included.
Qed.
Definition ArcTang := ( [-S-]ArcTan_def_lemma) 0 CI.
Lemma ArcTan_domain : forall x : IR, Dom ArcTang x.
Definition ArcTan (x : IR) := ArcTang x CI.
Lemma Continuous_ArcTan : Continuous (-∞,+∞) ArcTang.
Lemma Derivative_ArcTan : forall H, Derivative (-∞,+∞) H ArcTang {1/} ( [-C-]1{+}FId{^}2).
Lemma ArcTan_wd : forall x y, x[=]y -> ArcTan x [=] ArcTan y.
Section Inverses.
Composition properties
We now prove that this functions are in fact inverses to the corresponding trigonometric functions.
Sine and Arcsine
Lemma maps_Sin : maps_compacts_into ((⋅,⋅) [--] (π [/]2) (π [/]2)) ((⋅,⋅) [--]1 1) Sine.
Lemma ArcSin_Sin_inv : ≈ ((⋅,⋅) [--] (π [/]2) (π [/]2)) (ArcSin[o]Sine) FId.
Included.
Qed.
Lemma ArcSin_Sin : forall x, [--] (π [/]2) [<] x -> x [<] π [/]2 -> forall H, ArcSin (Sin x) H [=] x.
Lemma ArcSin_range : forall x Hx, [--] (π [/]2) [<] ArcSin x Hx and ArcSin x Hx [<] π [/]2.
Lemma Sin_ArcSin : forall (x : IR) Hx, x [=] Sin (ArcSin x Hx).
Lemma Sin_ArcSin_inv : ≈ ((⋅,⋅) [--]1 1) (Sine[o]ArcSin) FId.
Included.
Included.
Qed.
Lemma ArcSin_resp_leEq : forall x y,
[--]1 [<] x -> x [<=] y -> y [<] 1 -> forall Hx Hy, ArcSin x Hx [<=] ArcSin y Hy.
Lemma ArcCos_Cos : forall x, 0 [<] x -> x [<] π -> forall H, ArcCos (Cos x) H [=] x.
Lemma Cos_ArcCos : forall (x : IR) Hx, x [=] Cos (ArcCos x Hx).
Lemma ArcCos_Cos_inv : ≈ ((⋅,⋅) 0 π) (ArcCos[o]Cosine) FId.
Included.
Included.
Qed.
Lemma Cos_ArcCos_inv : ≈ ((⋅,⋅) [--]1 1) (Cosine[o]ArcCos) FId.
Included.
Qed.
Lemma ArcCos_resp_leEq : forall x y,
[--]1 [<] x -> x [<=] y -> y [<] 1 -> forall Hx Hy, ArcCos y Hy [<=] ArcCos x Hx.
Lemma maps_Tan : maps_compacts_into ((⋅,⋅) [--] (π [/]2) (π [/]2)) (-∞,+∞) Tang.
Included.
Qed.
Lemma ArcTan_Tan_inv : ≈ ((⋅,⋅) [--] (π [/]2) (π [/]2)) (ArcTang[o]Tang) FId.
Included.
Included.
Included.
Qed.
Lemma ArcTan_Tan : forall x, [--] (π [/]2) [<] x -> x [<] π [/]2 -> forall H, ArcTan (Tan x H) [=] x.
Lemma Tan_ilim : forall x, {y : IR | (⋅,⋅) [--] (π [/]2) (π [/]2) y | forall Hy, x [<=] Tan y Hy}.
Section ArcTan_Range.
Variable x : IR.
Lemma ArcTan_range : [--] (π [/]2) [<] ArcTan x and ArcTan x [<] π [/]2.
End ArcTan_Range.
Lemma Tan_ArcTan : forall (x : IR) Hx, x [=] Tan (ArcTan x) Hx.
Lemma Tan_ArcTan_inv : ≈ (-∞,+∞) (Tang[o]ArcTang) FId.
Included.
Included.
Qed.
End Inverses.