More on Power Series
We will now formally define an operator that defines a function as the sum of some series given a number sequence. Along with it, we will prove some important properties of these entities.
Variable J : interval.
Variable x0 : IR.
Hypothesis Hx0 : J x0.
Variable a : N -> IR.
Definition FPowerSeries (n : N) := a n{**} (FId{-} [-C-]x0) {^}n.
The most important convergence criterium specifically for power series
is the Dirichlet criterium.
Hypothesis Ha : {r : IR | {H : 0 [<] r | {N : N | forall n, N <= n ->
AbsIR (a (S n)) [<=] (1[/] r[//]pos_ap_zero _ _ H) [*]AbsIR (a n)}}}.
Let r := ProjT1 Ha.
Let Hr := ProjT1 (ProjT2 Ha).
Lemma Dirichlet_crit : fun_series_abs_convergent_IR ((⋅,⋅) (x0[-]r) (x0[+]r)) FPowerSeries.
When defining a function using its Taylor series as a motivation, the following operator can be of use.
This function is also continuous and has a good convergence ratio.
Lemma FPowerSeries'_cont : forall n, Continuous (-∞,+∞) (FPowerSeries' n).
Lemma included_FPowerSeries' : forall n P, ⊆ P (Dom (FPowerSeries' n)).
Hypothesis Ha' : {N : N | {c : IR | 0 [<] c |
forall n, N <= n -> AbsIR (a (S n)) [<=] c[*]AbsIR (a n)}}.
Lemma FPowerSeries'_conv' : fun_series_abs_convergent_IR (-∞,+∞) FPowerSeries'.
Lemma FPowerSeries'_conv : fun_series_convergent_IR (-∞,+∞) FPowerSeries'.
End Power_Series.
Section More_on_PowerSeries.
Let F and G be the power series defined
respectively by a and by fun n => (a (S n)).
Variable x0 : IR.
Variable a : N -> IR.
Variable J : interval.
Hypothesis Hf : fun_series_convergent_IR J F.
Hypothesis Hf' : fun_series_abs_convergent_IR J F.
Hypothesis Hg : fun_series_convergent_IR J G.
We get a comparison test for power series.
Lemma FPowerSeries'_comp : forall b, (forall n, AbsIR (b n) [<=] a n) ->
fun_series_convergent_IR J (FPowerSeries' x0 b).
And a rule for differentiation.
Lemma Derivative_FPowerSeries1' : forall H, Derivative J H (∑'∞ Hf) (∑'∞ Hg).
End More_on_PowerSeries.
Section Definitions.
Function definitions through power series
We now define the exponential, sine and cosine functions as power series, and prove their convergence. Tangent is defined as the quotient of sine over cosine.
Definition Exp_ps := FPowerSeries' 0 (fun n : N => 1).
Definition sin_seq : N -> IR.
Defined.
Definition sin_ps := FPowerSeries' 0 sin_seq.
Definition cos_seq : N -> IR.
Defined.
Definition cos_ps := FPowerSeries' 0 cos_seq.
Lemma Exp_conv' : fun_series_abs_convergent_IR (-∞,+∞) Exp_ps.
Lemma Exp_conv : fun_series_convergent_IR (-∞,+∞) Exp_ps.
Lemma sin_conv : fun_series_convergent_IR (-∞,+∞) sin_ps.
Lemma cos_conv : fun_series_convergent_IR (-∞,+∞) cos_ps.
Definition Expon := ∑'∞ Exp_conv.
Definition Sine := ∑'∞ sin_conv.
Definition Cosine := ∑'∞ cos_conv.
Definition Tang := Sine{/}Cosine.
Some auxiliary domain results.
Lemma Exp_domain : forall x : IR, Dom Expon x.
Lemma sin_domain : forall x : IR, Dom Sine x.
Lemma cos_domain : forall x : IR, Dom Cosine x.
Lemma included_Exp : forall P, ⊆ P (Dom Expon).
Lemma included_Sin : forall P, ⊆ P (Dom Sine).
Lemma included_Cos : forall P, ⊆ P (Dom Cosine).
Definition of the logarithm.
Lemma log_defn_lemma : Continuous ((⋅,+∞) 0) {1/}FId.
Included.
Qed.
Definition Logarithm := ( [-S-]log_defn_lemma) 1 (pos_one IR).
End Definitions.
As most of these functions are total, it makes sense to treat them as setoid functions on the reals. In the case of logarithm and tangent, this is not possible; however, we still define some abbreviations for aesthetical reasons.
Definition Exp : CSetoid_un_op IR.
Defined.
Definition Sin : CSetoid_un_op IR.
Defined.
Definition Cos : CSetoid_un_op IR.
Defined.
Definition Log x (Hx : 0 [<] x) := Logarithm x Hx.
Definition Tan x Hx := Tang x Hx.