CoRN.transc.PowerSeries

Require Export FTC.

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.

Section Power_Series.

General results

Let J : interval and x0 : IR be a point of J. Let a : nat → IR.

Variable J : interval.
Variable x0 : IR.
Hypothesis Hx0 : J x0.

Variable a : nat → IR.

Definition FPowerSeries (n : nat) := 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 : nat | ∀ 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 (olor (x0 [-]r) (x0 [+]r)) FPowerSeries.
Proof.
fold r in (value of Hr).
red in |- *; intros.
red in |- *; intros.
apply fun_ratio_test_conv.
  intro.
  unfold FPowerSeries in |- *; Contin.
elim (ProjT2 (ProjT2 Ha)); intros N HN.
∃ N.
cut {z : IR | [0] [<] z and z [<] r | ∀ x : IR, Compact Hab x → AbsIR (x [-]x0) [<=] z}.
  intro H.
  elim H; intros z Hz.
  elim Hz; clear Hz; intros H0z Hzr Hz.
  clear H.
  ∃ (([1][/] r [//]pos_ap_zero _ _ Hr ) [*]z).
   apply shift_mult_less with (pos_ap_zero _ _ H0z).
    assumption.
   apply recip_resp_less; assumption.
  split.
   apply less_leEq; apply mult_resp_pos.
    apply recip_resp_pos; assumption.
   assumption.
  intros.
  astepl (AbsIR (FPowerSeries (S n) x (ProjIR1 Hx'))).
  apply leEq_wdl with (AbsIR (a (S n)) [*]AbsIR (x[-]x0) [*]AbsIR ((x[-]x0 ) [^]n)).
   apply leEq_wdr with (([1][/] r [//]pos_ap_zero _ _ Hr ) [*]z[*]AbsIR (a n) [*] AbsIR ((x[-]x0 ) [^]n)).
    apply mult_resp_leEq_rht.
     2: apply AbsIR_nonneg.
    rstepr (([1][/] r [//]pos_ap_zero _ _ Hr ) [*]AbsIR (a n) [*]z).
    apply mult_resp_leEq_both; try apply AbsIR_nonneg.
     apply HN; assumption.
    apply Hz; auto.
   rstepl (([1][/] r [//]pos_ap_zero _ _ Hr ) [*]z[*](AbsIR (a n) [*]AbsIR ((x[-]x0 ) [^]n))).
   apply mult_wdr.
   astepr (AbsIR (FPowerSeries n x (ProjIR1 Hx))).
   simpl in |- *; apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
  simpl in |- ×.
  apply eq_symmetric_unfolded; eapply eq_transitive_unfolded.
   apply AbsIR_resp_mult.
  apply eq_transitive_unfolded with (AbsIR (a (S n)) [*](AbsIR ((x[-]x0 ) [^]n) [*]AbsIR (x[-]x0))).
   apply mult_wdr; apply AbsIR_resp_mult.
  simpl in |- *; rational.
clear HN.
cut ((∀ x : IR, Compact Hab x → a0 [<=] x ) ∧
   (∀ x : IR, Compact Hab x → x [<=] b)); intros.
  inversion_clear H.
  ∃ (Max (Max (b[-]x0) (x0 [-]a0)) (r [/]TwoNZ)).
   repeat split.
    eapply less_leEq_trans.
     2: apply rht_leEq_Max.
    apply pos_div_two; auto.
   repeat apply Max_less.
     apply shift_minus_less'.
     elim (Hinc _ (compact_inc_rht _ _ Hab)); auto.
    apply shift_minus_less; apply shift_less_plus'; elim (Hinc _ (compact_inc_lft _ _ Hab)); auto.
   apply pos_div_two'; auto.
  intros.
  simpl in |- *; unfold ABSIR in |- *; apply Max_leEq.
   apply leEq_transitive with (b[-]x0).
    apply minus_resp_leEq; apply H1; auto.
   eapply leEq_transitive.
    2: apply lft_leEq_Max.
   apply lft_leEq_Max.
  apply leEq_transitive with (x0 [-]a0).
   rstepr ([--](a0[-]x0 )); apply inv_resp_leEq.
   apply minus_resp_leEq; apply H0; auto.
  eapply leEq_transitive.
   2: apply lft_leEq_Max.
  apply rht_leEq_Max.
split; intros x H; elim H; auto.
Qed.

When defining a function using its Taylor series as a motivation, the following operator can be of use.

Definition FPowerSeries' n := (a n [/] _[//]nring_fac_ap_zero _ n ) {**} (FId {-} [-C -]x0 ) {^}n.

This function is also continuous and has a good convergence ratio.

Lemma FPowerSeries'_cont : ∀ n, Continuous realline (FPowerSeries' n).
Proof.
intros; unfold FPowerSeries' in |- ×.
Contin.
Qed.

Lemma included_FPowerSeries' : ∀ n P, included P (Dom (FPowerSeries' n)).
Proof.
repeat split.
Qed.

Hypothesis Ha' : {N : nat | {c : IR | [0] [<] c |
  ∀ n, N ≤ n → AbsIR (a (S n)) [<=] c[*]AbsIR (a n)}}.

Lemma FPowerSeries'_conv' : fun_series_abs_convergent_IR realline FPowerSeries'.
Proof.
clear Hr r Ha.
red in |- *; intros.
red in |- *; intros.
apply fun_ratio_test_conv.
  intro.
  unfold FPowerSeries' in |- *; Contin.
elim Ha'; intros N HN.
elim HN; intros c H H0.
clear HN Ha'.
elim (Archimedes (Max (Max b x0 [-]Min a0 x0) [1][*]Two [*]c)); intros y Hy.
∃ (max N y); ∃ (Half:IR); repeat split.
   unfold Half in |- ×.
   apply pos_div_two'; apply pos_one.
  apply less_leEq; apply pos_half.
intros x H1; intros.
astepl (AbsIR (FPowerSeries' (S n) x (ProjIR1 Hx'))).
astepr (Half [*]AbsIR (FPowerSeries' n x (ProjIR1 Hx))).
simpl in |- ×.
eapply leEq_wdl.
  2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
apply leEq_wdl with ((AbsIR (a (S n)) [/] _[//]nring_fac_ap_zero _ (S n)) [*]
   (AbsIR ((x[-]x0 ) [^]n) [*]AbsIR (x[-]x0))).
  2: apply mult_wd.
   2: apply eq_transitive_unfolded with (AbsIR (a (S n)) [/] _[//]
     AbsIR_resp_ap_zero _ (nring_fac_ap_zero _ (S n))).
    3: apply eq_symmetric_unfolded; apply AbsIR_division.
   2: apply div_wd; algebra.
   2: apply eq_symmetric_unfolded; apply AbsIR_eq_x; apply nring_nonneg.
  2: apply eq_symmetric_unfolded; eapply eq_transitive_unfolded.
   2: apply AbsIR_resp_mult.
  2: apply mult_wd; apply AbsIR_wd; simpl in |- *; algebra.
apply leEq_wdr with ([1] [/]TwoNZ [*](AbsIR (a n) [/] _[//]nring_fac_ap_zero _ n) [*]
   AbsIR ((x[-]x0 ) [^]n)).
  2: apply eq_symmetric_unfolded; eapply eq_transitive_unfolded.
   3: apply mult_assoc_unfolded.
  2: apply mult_wdr.
  2: eapply eq_transitive_unfolded.
   2: apply AbsIR_resp_mult.
  2: apply mult_wdl; simpl in |- *; algebra.
  2: apply eq_transitive_unfolded
    with (AbsIR (a n) [/] _[//]AbsIR_resp_ap_zero _ (nring_fac_ap_zero _ n)).
   2: apply AbsIR_division.
  2: apply div_wd; algebra.
  2: apply AbsIR_eq_x; apply nring_nonneg.
rstepl (AbsIR (a (S n)) [*]AbsIR (x[-]x0) [*]AbsIR ((x[-]x0 ) [^]n) [/] _[//]
   nring_fac_ap_zero _ (S n)).
apply shift_div_leEq.
  apply pos_nring_fac.
rstepr ([1] [/]TwoNZ [*] (AbsIR (a n) [*]nring (fact (S n)) [/] _[//]nring_fac_ap_zero _ n) [*]
   AbsIR ((x[-]x0 ) [^]n)).
apply leEq_wdr with ([1] [/]TwoNZ [*](AbsIR (a n) [*]nring (S n)) [*]AbsIR ((x[-]x0 ) [^]n)).
  2: apply mult_wdl; apply mult_wdr.
  2: rstepr (AbsIR (a n) [*](nring (fact (S n)) [/] _[//]nring_fac_ap_zero _ n)).
  2: apply mult_wdr.
  2: astepr (nring (S n × fact n) [/] _[//]nring_fac_ap_zero IR n).
  2: astepr (nring (S n) [*]nring (fact n) [/] _[//]nring_fac_ap_zero IR n); rational.
rstepr ([1] [/]TwoNZ [*]nring (S n) [*]AbsIR (a n) [*]AbsIR ((x[-]x0 ) [^]n)).
apply mult_resp_leEq_rht.
  2: apply AbsIR_nonneg.
apply leEq_transitive with (AbsIR (a (S n)) [*]AbsIR (Max b x0 [-]Min a0 x0)).
  apply mult_resp_leEq_lft.
   cut (Min a0 x0 [<=] Max b x0). intro H3.
    apply compact_elements with H3.
     inversion_clear H1; split.
      apply leEq_transitive with a0; auto; apply Min_leEq_lft.
     apply leEq_transitive with b; auto; apply lft_leEq_Max.
    split.
     apply Min_leEq_rht.
    apply rht_leEq_Max.
   apply leEq_transitive with x0.
    apply Min_leEq_rht.
   apply rht_leEq_Max.
  apply AbsIR_nonneg.
apply leEq_transitive with (AbsIR (a (S n)) [*]Max (Max b x0 [-]Min a0 x0) [1]).
  apply mult_resp_leEq_lft.
   2: apply AbsIR_nonneg.
  eapply leEq_wdl.
   apply lft_leEq_Max.
  apply eq_symmetric_unfolded; apply AbsIR_eq_x.
  apply shift_leEq_minus; astepl (Min a0 x0).
  apply leEq_transitive with x0.
   apply Min_leEq_rht.
  apply rht_leEq_Max.
apply shift_mult_leEq with (max_one_ap_zero (Max b x0 [-]Min a0 x0)).
  apply pos_max_one.
apply leEq_transitive with (c[*]AbsIR (a n)).
  apply H0.
  apply le_trans with (max N y); auto; apply le_max_l.
apply shift_leEq_div.
  apply pos_max_one.
rstepl (c[*]Max (Max b x0 [-]Min a0 x0) [1][*]AbsIR (a n)).
apply mult_resp_leEq_rht.
  2: apply AbsIR_nonneg.
rstepr (nring (R:=IR) (S n) [/]TwoNZ); apply shift_leEq_div.
  apply pos_two.
apply less_leEq; apply leEq_less_trans with (nring (R:=IR) y).
  eapply leEq_wdl.
   apply Hy.
  rational.
apply nring_less.
red in |- ×.
cut (y ≤ n); intros; auto with arith.
apply le_trans with (max N y); auto with arith.
Qed.

Lemma FPowerSeries'_conv : fun_series_convergent_IR realline FPowerSeries'.
Proof.
apply abs_imp_conv_IR.
  apply FPowerSeries'_cont.
apply FPowerSeries'_conv'.
Qed.

End Power_Series.

Hint Resolve FPowerSeries'_cont: continuous.

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 : nat → 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 : ∀ b, (∀ n, AbsIR (b n) [<=] a n) →
fun_series_convergent_IR J (FPowerSeries' x0 b).
Proof.
intros.
apply fun_comparison_IR with (fun n : nat ⇒ FAbs (FPowerSeries' x0 a n)).
   intros n.
   apply Included_imp_Continuous with realline;[Contin | auto with *].
  auto.
intros.
apply leEq_wdr with (AbsIR (FPowerSeries' x0 a n x (ProjIR1 Hx'))).
  2: apply eq_symmetric_unfolded; apply FAbs_char.
simpl in |- ×.
eapply leEq_wdr.
  2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
eapply leEq_wdl.
  2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
apply mult_resp_leEq_rht.
  2: apply AbsIR_nonneg.
eapply leEq_wdr.
  2: apply eq_symmetric_unfolded; apply AbsIR_division
    with (y__ := AbsIR_resp_ap_zero _ (nring_fac_ap_zero IR n)).
eapply leEq_wdl.
  2: apply eq_symmetric_unfolded; apply AbsIR_division
    with (y__ := AbsIR_resp_ap_zero _ (nring_fac_ap_zero IR n)).
apply div_resp_leEq.
  eapply less_leEq_trans.
   apply (pos_nring_fac IR n).
  apply leEq_AbsIR.
apply leEq_transitive with (a n); [ auto | apply leEq_AbsIR ].
Qed.

And a rule for differentiation.

Lemma Derivative_FPowerSeries1' : ∀ H, Derivative J H (FSeries_Sum Hf) (FSeries_Sum Hg).
Proof.
intro.
eapply Derivative_wdr.
  apply Feq_symmetric; apply (insert_series_sum _ _ Hg).
apply Derivative_FSeries.
intro; case n; clear n; intros.
  simpl in |- ×.
  apply Derivative_wdl with (Fconst (S:=IR) (a 0)).
   FEQ.
  Deriv.
simpl in |- ×.
Opaque nring fact.
unfold F, G, FPowerSeries' in |- *; simpl in |- ×.
Derivative_Help.
apply eq_imp_Feq.
   apply included_FScalMult; apply included_FScalMult.
   apply included_FMult; Included.
  apply included_FScalMult; Included.
intros; simpl in |- ×.
set (y := nexp _ n (x[-]x0)) in ×.
rstepl (a (S n) [*]y[*](nring (S n) [/] _[//]nring_fac_ap_zero _ (S n))).
rstepr (a (S n) [*]y[*] (nring (S n) [/] _[//]
   mult_resp_ap_zero _ _ _ (pos_ap_zero _ _ (pos_nring_S _ n)) (nring_fac_ap_zero _ n))).
apply mult_wdr.
apply div_wd; algebra.
Step_final (nring (R:=IR) (S n × fact n)).
Qed.

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 : nat ⇒ [1]).

Definition sin_seq : nat → IR.
Proof.
intro n; elim (even_or_odd_plus n); intros k Hk; inversion_clear Hk.
  apply ZeroR.
apply ([--]OneR [^]k).
Defined.

Definition sin_ps := FPowerSeries' [0] sin_seq.

Definition cos_seq : nat → IR.
Proof.
intro n; elim (even_or_odd_plus n); intros k Hk; inversion_clear Hk.
  apply ([--]OneR [^]k).
apply ZeroR.
Defined.

Definition cos_ps := FPowerSeries' [0] cos_seq.

Lemma Exp_conv' : fun_series_abs_convergent_IR realline Exp_ps.
Proof.
unfold Exp_ps in |- ×.
apply FPowerSeries'_conv'.
∃ 0; ∃ OneR.
  apply pos_one.
intros; apply eq_imp_leEq; algebra.
Qed.

Lemma Exp_conv : fun_series_convergent_IR realline Exp_ps.
Proof.
unfold Exp_ps in |- ×.
apply FPowerSeries'_conv.
∃ 0; ∃ OneR.
  apply pos_one.
intros; apply eq_imp_leEq; algebra.
Qed.

Lemma sin_conv : fun_series_convergent_IR realline sin_ps.
Proof.
unfold sin_ps in |- *; apply FPowerSeries'_comp with (fun n : nat ⇒ OneR).
  apply Exp_conv'.
intros; unfold sin_seq in |- ×.
elim even_or_odd_plus; intros k Hk; simpl in |- ×.
elim Hk; simpl in |- *; intro.
  eapply leEq_wdl; [ apply less_leEq; apply pos_one | apply eq_symmetric_unfolded; apply AbsIRz_isz ].
apply eq_imp_leEq.
elim (even_odd_dec k); intro.
  apply eq_transitive_unfolded with (AbsIR [1]).
   apply AbsIR_wd; astepl ([--]OneR [^]k); apply inv_one_even_nexp; auto.
  apply AbsIR_eq_x; apply less_leEq; apply pos_one.
apply eq_transitive_unfolded with (AbsIR [--][1]).
  apply AbsIR_wd; astepl ([--]OneR [^]k); apply inv_one_odd_nexp; auto.
astepr ([--][--]OneR); apply AbsIR_eq_inv_x; apply less_leEq.
astepr ([--]ZeroR); apply inv_resp_less; apply pos_one.
Qed.

Lemma cos_conv : fun_series_convergent_IR realline cos_ps.
Proof.
unfold cos_ps in |- *; apply FPowerSeries'_comp with (fun n : nat ⇒ OneR).
  apply Exp_conv'.
intros; unfold cos_seq in |- ×.
elim even_or_odd_plus; intros k Hk; simpl in |- ×.
elim Hk; simpl in |- *; intro.
  apply eq_imp_leEq.
  elim (even_odd_dec k); intro.
   apply eq_transitive_unfolded with (AbsIR [1]).
    apply AbsIR_wd; astepl ([--]OneR [^]k); apply inv_one_even_nexp; auto.
   apply AbsIR_eq_x; apply less_leEq; apply pos_one.
  apply eq_transitive_unfolded with (AbsIR [--][1]).
   apply AbsIR_wd; astepl ([--]OneR [^]k); apply inv_one_odd_nexp; auto.
  astepr ([--][--]OneR); apply AbsIR_eq_inv_x; apply less_leEq.
  astepr ([--]ZeroR); apply inv_resp_less; apply pos_one.
eapply leEq_wdl; [ apply less_leEq; apply pos_one | apply eq_symmetric_unfolded; apply AbsIRz_isz ].
Qed.

Definition Expon := FSeries_Sum Exp_conv.

Definition Sine := FSeries_Sum sin_conv.

Definition Cosine := FSeries_Sum cos_conv.

Definition Tang := Sine {/}Cosine.

Some auxiliary domain results.

Lemma Exp_domain : ∀ x : IR, Dom Expon x.
Proof.
intros; simpl in |- *; auto.
Qed.

Lemma sin_domain : ∀ x : IR, Dom Sine x.
Proof.
intros; simpl in |- *; auto.
Qed.

Lemma cos_domain : ∀ x : IR, Dom Cosine x.
Proof.
intros; simpl in |- *; auto.
Qed.

Lemma included_Exp : ∀ P, included P (Dom Expon).
Proof.
intro; simpl in |- *; Included.
Qed.

Lemma included_Sin : ∀ P, included P (Dom Sine).
Proof.
intro; simpl in |- *; Included.
Qed.

Lemma included_Cos : ∀ P, included P (Dom Cosine).
Proof.
intro; simpl in |- *; Included.
Qed.

Definition of the logarithm.

Lemma log_defn_lemma : Continuous (openl [0]) {1/}FId.
Proof.
apply Continuous_recip.
  apply Continuous_id.
intros a b Hab H.
split.
  Included.
assert (H0 : [0] [<] a). apply H; apply compact_inc_lft.
  ∃ a.
  auto.
intros y Hy H1; inversion_clear H1.
apply leEq_transitive with y.
  auto.
apply leEq_AbsIR.
Qed.

Definition Logarithm := ( [-S -]log_defn_lemma) [1] (pos_one IR).

End Definitions.

Hint Resolve included_Exp included_Sin included_Cos: included.

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.
Proof.
red in |- ×.
apply Build_CSetoid_fun with (fun x : IR ⇒ Expon x I).
intros x y H.
exact (pfstrx _ _ _ _ _ _ H).
Defined.

Definition Sin : CSetoid_un_op IR.
Proof.
red in |- ×.
apply Build_CSetoid_fun with (fun x : IR ⇒ Sine x I).
intros x y H.
exact (pfstrx _ _ _ _ _ _ H).
Defined.

Definition Cos : CSetoid_un_op IR.
Proof.
red in |- ×.
apply Build_CSetoid_fun with (fun x : IR ⇒ Cosine x I).
intros x y H.
exact (pfstrx _ _ _ _ _ _ H).
Defined.

Definition Log x (Hx : [0] [<] x) := Logarithm x Hx.

Definition Tan x Hx := Tang x Hx.