Library p1_weierstrass

binomial coefficients, polynomials, continuity, Weierstrass' theorem through Bernstein's polynomials





first loading a few libraries

Require Import Setoid Morphisms.
Require Import List.
Import ListNotations Nat.
Arguments sub !n !m /.
Require Import Psatz Rbase Rfunctions Ranalysis.
Local Open Scope R_scope.

and defining a few helpers which are missing from the standard library
Lemma INR0: INR O = 0. Proof. reflexivity. Qed.
Definition INRS := S_INR.
Lemma INRpred n: (0<n)%natINR (pred n) = INR n - 1.
Proof. destruct n. lia. rewrite INRS. simpl. lra. Qed.
Opaque INR.
Lemma Rdiv1 x: x/1 = x.
Proof. field. Qed.
Ltac field_simpl := field_simplify; rewrite ?Rdiv1.

Instance Rle_PreOrder: PreOrder Rle.
Proof. constructor; cbv; intros; lra. Qed.
Instance Rlt_PreOrder: Transitive Rlt.
Proof. cbv; intros; lra. Qed.
Instance Rlt_Rle: subrelation Rlt Rle.
Proof. cbv. tauto. Qed.
Instance Rplus_Rle: Proper (Rle ==> Rle ==> Rle) Rplus.
Proof. repeat intro. lra. Qed.

first session: binomials coefficients

factorial


Fixpoint fact (n: nat) :=
  match n with
  | 0 ⇒ 1
  | S n'INR n × fact n'
  end.

Lemma fact_gt_0 n: fact n > 0.
Proof.
  induction n; simpl.
  - lra.
  - apply Rmult_gt_0_compat; trivial. apply lt_0_INR. lia.
Qed.

Lemma fact_neq_0 n: fact n ≠ 0.
Proof. pose (fact_gt_0 n). lra. Qed.

Ltac neq_0 := repeat split; solve [ apply not_O_INR; lia | apply fact_neq_0 ].

binomial coefficients


Definition C n p := fact n / (fact p × fact (n - p)).


Lemma Cnn: n, C n n = 1.
Proof.
  intro n. unfold C. replace (n-n)%nat with 0%nat by lia.
  simpl. field. neq_0.
Qed.

Lemma Cn0: n, C n 0 = 1.
Proof.
  intro n. unfold C. replace (n-0)%nat with n%nat by lia.
  simpl. field. neq_0.
Qed.

Lemma pascal1: n i, (in)%natC n i = C n (n - i).
Proof.
  intros n i H; unfold C.
  replace (n - (n - i))%nat with i by lia.
  field. neq_0.
Qed.

Lemma pascal2: n i,
    (in)%natC (S n) i = INR (S n) / INR (S n - i) × C n i.
Proof.
  intros n i H; unfold C.
  replace (S n - i)%nat with (S (n - i)) by lia.
  simpl. field; neq_0.
Qed.

Lemma pascal3: n i,
    (i < n)%natC n (S i) = INR (n - i) / INR (S i) × C n i.
Proof.
  intros n i H; unfold C.
  replace (n - i)%nat with (S (n - S i)) by lia.
  simpl. field; neq_0.
Qed.

Lemma pascal4: n i, C (S n) (S i) = INR (S n) / INR (S i) × C n i.
Proof. intros. unfold C. simpl. field. neq_0. Qed.

Lemma pascal: n i,
    (i < n)%natC (S n) (S i) = C n i + C n (S i).
Proof.
  intros.
  rewrite 2pascal3, pascal2 by lia.
  rewrite !minus_INR, !INRS by lia.
  field. pose (pos_INR i). apply lt_INR in H. lra.
Qed.

Lemma pascal4': n i, (0<n ∧ 0<i)%natINR i / INR n × C n i = C (pred n) (pred i).
Proof.
  intros.
  replace n with (S (pred n)) by lia.
  replace i with (S (pred i)) by lia.
  rewrite pascal4 at 1 by assumption.
  simpl. field; neq_0.
Qed.

finite sums


Fixpoint sum n f :=
  match n with
  | O ⇒ 0
  | S nsum n f + f n
  end.

Lemma sum0 f: sum 0 f = 0.
Proof. reflexivity. Qed.

Lemma sum1 f: sum 1 f = f O.
Proof. simpl. ring. Qed.

Lemma sumS_last n f: sum (S n) f = sum n f + f n.
Proof. reflexivity. Qed.

Lemma sumS_first n f: sum (S n) f = f 0%nat + sum n (fun if (S i)).
Proof.
  induction n as [|n IH].
  - simpl; ring.
  - rewrite sumS_last, IH. simpl. ring.
Qed.

Lemma sum_last n f: (0<n)%natsum n f = sum (pred n) f + f (pred n).
Proof. destruct n. lia. reflexivity. Qed.

Lemma sum_first n f: (0<n)%natsum n f = f 0%nat + sum (pred n) (fun if (S i)).
Proof. destruct n. lia. intros _. apply sumS_first. Qed.

Lemma sum_rev n f: sum n f = sum n (fun if (n-S i)%nat).
Proof.
  induction n. reflexivity.
  rewrite sumS_last, sumS_first, IHn.
  simpl. replace (n - 0)%nat with n. ring. lia.
Qed.

Lemma xsum n x f: x × sum n f = sum n (fun ix × f i).
Proof.
  induction n; simpl.
  - ring.
  - rewrite <-IHn. ring.
Qed.

Lemma sum_plus n f g: sum n (fun if i + g i) = sum n f + sum n g.
Proof.
  induction n; simpl.
  - ring.
  - rewrite IHn. ring.
Qed.

Lemma sum_minus n f g: sum n (fun if i - g i) = sum n f - sum n g.
Proof.
  induction n; simpl.
  - ring.
  - rewrite IHn. ring.
Qed.

Lemma sum_eq n f g: ( i, (i<n)%natf i = g i) → sum n f = sum n g.
Proof.
  intros H; induction n; simpl.
  - reflexivity.
  - rewrite H by lia. rewrite IHn. reflexivity. intros. apply H. lia.
Qed.

Lemma sum_le n f g: ( i, (i<n)%natf ig i) → sum n fsum n g.
Proof.
  intros H; induction n; simpl.
  - reflexivity.
  - rewrite H by lia. rewrite IHn. reflexivity. intros. apply H. lia.
Qed.

Instance sum_pwr_eq n: Proper (pointwise_relation nat eq ==> eq) (sum n).
Proof. intros ???. apply sum_eq. intros ? _. apply H. Qed.

Instance sum_pwr_le n: Proper (pointwise_relation nat Rle ==> Rle) (sum n).
Proof. intros ???. apply sum_le. intros ? _. apply H. Qed.

Lemma split_sum (p: natbool) n f:
  sum n f =
  sum n (fun iif p i then f i else 0) +
  sum n (fun iif p i then 0 else f i).
Proof.
  induction n; simpl.
  - ring.
  - rewrite IHn. case p; ring.
Qed.

Lemma Rabs_sum n f: Rabs (sum n f) ≤ sum n (fun iRabs (f i)).
Proof.
  induction n; simpl.
  - split_Rabs; lra.
  - now rewrite Rabs_triang, IHn.
Qed.

Opaque sum.

binomial equation


Lemma cancel_r x y z: y-x=z-xy=z.
Proof. lra. Qed.

Proposition binomial: x y n,
    (x + y) ^ n = sum (S n) (fun iC n i × x ^ i × y ^ (n - i)).
Proof.
  intros; induction n as [|n IH].
  - rewrite sum1, Cn0. simpl. ring.
  - rewrite sumS_last, sumS_first. simpl.
    rewrite IH, Rmult_plus_distr_r, 2xsum.
    rewrite sumS_last, sumS_first. simpl.
    rewrite 2Cn0, 2Cnn, minus_diag, <-minus_n_O. ring_simplify.
    apply cancel_r with (x^(S n)+y^(S n)). simpl. ring_simplify.
    rewrite <-sum_plus. apply sum_eq. intros.
    rewrite pascal by lia.
    replace (n-i)%nat with (S (n-(S i))) by lia.
    simpl. ring.
Qed.

Lemma binomial' x n: sum (S n) (fun kC n k × x^k × (1-x)^(n-k)) = 1.
Proof.
  rewrite <-binomial.
  replace (x+(1-x)) with 1 by ring. apply pow1.
Qed.

Lemma binomial'' x n: (0<n)%natsum n (fun kC (pred n) k × x^k × (1-x)^(pred n-k)) = 1.
Proof.
  intro. replace n with (S (pred n)) by lia. apply binomial'.
Qed.

Corollary pow2n: n, sum (S n) (fun iC n i) = 2^n.
Proof.
  intro. replace 2 with (1+1) by ring.
  rewrite binomial. apply sum_eq. intros.
  rewrite 2pow1. ring.
Qed.

Corollary powk2n: n, sum (S n) (fun iINR i × C n i) = INR n × 2^(n-1).
Proof.
  intro. rewrite <-pow2n. rewrite xsum.
  destruct n. reflexivity.
  rewrite sumS_first. rewrite INR0. ring_simplify.
  replace (S n - 1)%nat with n by lia.
  apply sum_eq. intros i Hi.
  rewrite pascal4, 2INRS. field. pose proof (pos_INR i); lra.
Qed.

second session: polynomials, continuity

polynomials

we represent polynomials by their list of coefficients a;b;c represents a+bX+cX^2 note that we do *not* impose that the last coefficient must be non-zero.
Definition poly := list R.
Fixpoint eval (P: poly) (x: R): R :=
  match P with
  | [] ⇒ 0
  | a::Qa + x × eval Q x
  end.

Definition pcst a: poly := [a].
Lemma eval_cst a x: eval (pcst a) x = a.
Proof. simpl. ring. Qed.

Definition pid: poly := [0;1].
Lemma eval_id x: eval pid x = x.
Proof. simpl. ring. Qed.

Fixpoint pxk (k: nat): poly :=
  match k with
  | O ⇒ [1]
  | S k ⇒ 0::pxk k
  end.
Lemma eval_xk k x: eval (pxk k) x = x^k.
Proof. induction k as [|k IH]; simpl; rewrite ?IH; ring. Qed.

Fixpoint pplus (P Q: poly): poly :=
  match P,Q with
  | [],R | R,[] ⇒ R
  | a::P,b::Q ⇒ (a+b)::pplus P Q
  end.
Arguments pplus !P !Q /.
Lemma eval_plus: P Q x, eval (pplus P Q) x = eval P x + eval Q x.
Proof. induction P as [|a P IH]; intros [|b Q] x; simpl; rewrite ?IH; ring. Qed.

Definition pscal a (P: poly): poly := List.map (Rmult a) P.
Lemma eval_scal a P x: eval (pscal a P) x = a × eval P x.
Proof. induction P as [|b P IH]; simpl; rewrite ?IH; ring. Qed.

Fixpoint pmult (P Q: poly): poly :=
  match P with
  | [] ⇒ []
  | a::Ppplus (pscal a Q) (0::pmult P Q)
  end.
Lemma eval_mult: P Q x, eval (pmult P Q) x = eval P x × eval Q x.
Proof.
  induction P as [|a P IH]; intros Q x; simpl. ring.
  rewrite eval_plus, eval_scal. simpl. rewrite IH. ring.
Qed.

Fixpoint pcomp (P Q: poly): poly :=
  match P with
  | [] ⇒ []
  | a::Ppplus (pcst a) (pmult (pcomp P Q) Q)
  end.
Lemma eval_comp: P Q x, eval (pcomp P Q) x = eval P (eval Q x).
Proof.
  induction P as [|a P IH]; intros Q x; simpl. reflexivity.
  rewrite eval_plus, eval_cst, eval_mult, IH. ring.
Qed.

isolating polynomials amongst arbitrary functions (boilerplate)


Definition is_poly (f: RR) := P: poly, x, eval P x = f x.

Lemma is_poly_cst a: is_poly (fun _a).
Proof. (pcst a). apply eval_cst. Qed.

Lemma is_poly_id: is_poly (fun xx).
Proof. pid. apply eval_id. Qed.

Lemma is_poly_xk k: is_poly (fun xx^k).
Proof. (pxk k). apply eval_xk. Qed.

Lemma is_poly_plus f g: is_poly fis_poly gis_poly (fun xf x + g x).
Proof.
  intros (P&Pf) (Q&Qg). (pplus P Q).
  intro. now rewrite eval_plus, Pf, Qg.
Qed.

Lemma is_poly_scal f a: is_poly fis_poly (fun xa × f x).
Proof.
  intros (P&Pf). (pscal a P).
  intro. now rewrite eval_scal, Pf.
Qed.

Lemma is_poly_opp: is_poly Ropp.
Proof.
   (pscal (-1) pid).
  intro. simpl. ring.
Qed.

Lemma is_poly_mult f g: is_poly fis_poly gis_poly (fun xf x × g x).
Proof.
  intros (P&Pf) (Q&Qg). (pmult P Q).
  intro. now rewrite eval_mult, Pf, Qg.
Qed.

Lemma is_poly_comp f g: is_poly fis_poly gis_poly (fun xf (g x)).
Proof.
  intros (P&Pf) (Q&Qg). (pcomp P Q).
  intro. now rewrite eval_comp, Pf, Qg.
Qed.

Instance is_poly_Proper: Proper (pointwise_relation R eq ==> Basics.impl) is_poly.
Proof. intros f g H. unfold is_poly. now setoid_rewrite H. Qed.

Lemma is_poly_sum n f:
  ( i, i<nis_poly (f i))%natis_poly (fun xsum n (fun if i x)).
Proof.
  induction n; intro H.
  - setoid_rewrite sum0. apply is_poly_cst.
  - setoid_rewrite sumS_last. apply is_poly_plus.
    apply IHn. intros. apply H. lia.
    apply H. lia.
Qed.

continuity


Definition continuous_at f x :=
   e, 0<e d, 0<d y, Rabs(y-x)<=dRabs(f y-f x)<=e.

we prove that this definition is equivalent to the one in the standard library (the one above is slightly easier to work with)
Lemma continuous_at_standard f x:
  continuous_at f xcontinuity_pt f x.
Proof.
  split; intros H e He.
  - destruct (H (e/2)) as (d&D&Hd). lra.
     d. split. assumption.
    simpl dist; unfold R_dist.
    intros y [_ ?]. specialize (Hd y). lra.
  - destruct (H e) as (d&D&Hd). assumption.
    simpl dist in Hd; unfold R_dist in Hd.
     (d/2). split. lra.
    intros y Hy. destruct (Req_dec x y) as [-> | N]. split_Rabs; lra.
    apply Rlt_le. apply Hd. split. now split. lra.
Qed.

Lemma continuous_id x: continuous_at id x.
Proof.
  intros e He. e. split. assumption.
  now intros y ?.
Qed.

Lemma continuous_cst a x: continuous_at (fun _a) x.
Proof.
  intros e He. 1. split. lra.
  intros y D. split_Rabs; lra.
Qed.

Lemma continuous_plus f g x:
  continuous_at f xcontinuous_at g xcontinuous_at (fun yf y + g y) x.
Proof.
  intros F G e He.
  destruct (F (e/2)) as (df&Df&Hdf). lra.
  destruct (G (e/2)) as (dg&Dg&Hdg). lra.
   (Rmin df dg). split. now apply P_Rmin.
  intros y D.
  pose proof (conj (Rmin_l df dg) (Rmin_r df dg)).
  replace (_-_) with ((f y-f x) + (g y-g x)) by ring.
  rewrite Rabs_triang, Hdf, Hdg; lra.
Qed.

Lemma continuous_Rabs x: continuous_at Rabs x.
Proof.
  intros e He. e. split. assumption.
  intros y D. split_Rabs; lra.
Qed.

Lemma continuous_comp f g x:
  continuous_at f xcontinuous_at g (f x) → continuous_at (fun yg (f y)) x.
Proof.
  intros F G e E.
  specialize (G e E) as (d&D&Hg).
  specialize (F d D) as (d'&D'&Hf).
   d'. split. assumption.
  intros y L. apply Hg, Hf, L.
Qed.

Lemma x_div_1x x: 0<=xx/(x+1) ≤ 1.
Proof.
  intro. apply (Rmult_le_reg_l (x+1)). lra.
  field_simpl. lra. lra.
Qed.


Goal a b c, ab → 0<=ca×cb×c.
Proof.
  intros a b c H C.
  erewrite Rmult_le_compat_r. 2: apply C. 2: apply H.
  reflexivity.
Qed.

Lemma continuous_mult f g x:
  continuous_at f xcontinuous_at g xcontinuous_at (fun yf y × g y) x.
Proof.
  intros F G e He.
  set (ef := (Rmin (e/(3*(Rabs (g x) + 1))) (sqrt (e/3)))).
  destruct (F ef) as (df&Df&Hdf).
   apply P_Rmin. apply Rdiv_lt_0_compat. assumption. split_Rabs; lra.
   apply sqrt_lt_R0. apply Rdiv_lt_0_compat. assumption. lra.
  set (eg := (Rmin (e/(3*(Rabs (f x) + 1))) (sqrt (e/3)))).
  destruct (G eg) as (dg&Dg&Hdg).
   apply P_Rmin. apply Rdiv_lt_0_compat. assumption. split_Rabs; lra.
   apply sqrt_lt_R0. apply Rdiv_lt_0_compat. assumption. lra.
   (Rmin df dg). split. now apply P_Rmin.
  intros y D.
  pose proof (conj (Rmin_l df dg) (Rmin_r df dg)).
  replace (_-_) with ((f y-f x) × g x + (g y-g x) × f x + (f y-f x)*(g y-g x)) by ring.
  rewrite 2Rabs_triang, 3Rabs_mult.
  replace e with (e/3 + e/3 + e/3) by lra.
  apply Rplus_le_compat. apply Rplus_le_compat.
  - erewrite Rmult_le_compat_r. 2: apply Rabs_pos. 2: apply Hdf; lra.
    erewrite Rmult_le_compat_r. 2: apply Rabs_pos. 2: apply Rmin_l.
    transitivity ((Rabs (g x))/(Rabs (g x)+1)*(e/3)). apply Req_le. field. split_Rabs; lra.
    erewrite Rmult_le_compat_r. 2: lra. 2: apply x_div_1x. apply Req_le. ring. apply Rabs_pos.
  - erewrite Rmult_le_compat_r. 2: apply Rabs_pos. 2: apply Hdg; lra.
    erewrite Rmult_le_compat_r. 2: apply Rabs_pos. 2: apply Rmin_l.
    transitivity ((Rabs (f x))/(Rabs (f x)+1)*(e/3)). apply Req_le. field. split_Rabs; lra.
    erewrite Rmult_le_compat_r. 2: lra. 2: apply x_div_1x. apply Req_le. ring. apply Rabs_pos.
  - etransitivity. apply Rmult_le_compat. apply Rabs_pos. apply Rabs_pos.
    rewrite Hdf by lra. apply Rmin_r.
    rewrite Hdg by lra. apply Rmin_r.
    apply Req_le, sqrt_sqrt. lra.
Qed.

Lemma poly_continuous P x: continuous_at (eval P) x.
Proof.
  induction P as [|a P IH]; simpl.
  - apply continuous_cst.
  - apply continuous_plus. apply continuous_cst.
    apply continuous_mult. apply continuous_id. apply IH.
Qed.

third session: Weierstrass' theorem, via Bernstein's polynomials

Bernstein's polynomials


Definition b n k x := C n k × x^k × (1-x)^(n-k).

Lemma is_poly_b k n: is_poly (b n k).
Proof.
  apply is_poly_mult. apply is_poly_scal. apply is_poly_xk.
  apply (is_poly_comp (fun xx^(n-k))).
  apply is_poly_xk. apply is_poly_plus. apply is_poly_cst. apply is_poly_opp.
Qed.

Definition B n g x := sum (S n) (fun kg(INR k / INR n) × b n k x).

Lemma is_poly_B n g: is_poly (B n g).
Proof.
  apply is_poly_sum. intros k _.
  apply is_poly_mult. apply is_poly_cst. apply is_poly_b.
Qed.

Lemma B1 n x: B n (fun _ ⇒ 1) x = 1.
Proof.
  unfold B, b. setoid_rewrite Rmult_1_l. apply binomial'.
Qed.

Ltac open_sum i Hi := erewrite sum_eq; swap 1 2; [intros i Hi|].
Ltac close_sum := reflexivity.

Lemma Bx n x: (0<n)%natB n (fun xx) x = x.
Proof.
  intros N. unfold B, b.
  rewrite sumS_first, INR0. unfold Rdiv at 1. ring_simplify.
  open_sum k Hk.
    rewrite <-2Rmult_assoc, pascal4' by lia.
    transitivity (x*(C (pred n) k × x^k × (1-x)^(pred n-k))).
    replace (n - S k)%nat with (pred n - k)%nat by lia.
    simpl. ring.
  close_sum.
  rewrite <-xsum, binomial'' by lia. ring.
Qed.

Lemma Bx2 n x: (0<n)%natB n (fun xx^2) x = x/INR n + x^2 × (INR n-1)/INR n.
Proof.
  intro N'. assert (C: (n=1 ∨ 1<n)%nat) by lia.
  destruct C as [->|N]; clear N'; unfold B, b.
  rewrite sumS_first, sum1, INRS, INR0, Cn0, Cnn. simpl. field.
  rewrite sumS_first, INR0. unfold Rdiv at 1. ring_simplify.
  open_sum k Hk.
    rewrite <-2Rmult_assoc.
    replace (_^2 × _) with (INR (S k) / INR n × (INR (S k) / INR n × C n (S k))) by ring.
    rewrite pascal4' by lia.
    rewrite INRS. replace (_/_) with (INR k/INR n + 1/INR n) by (field; neq_0).
    rewrite 3Rmult_plus_distr_r.
  close_sum.
  rewrite sum_plus.
  rewrite sum_first, INR0 by lia. unfold Rdiv at 1. ring_simplify.
  open_sum k Hk.
    transitivity (((INR n - 1) / INR n × x^2) × ((INR (S k)) / INR (pred n) × C (pred n) (S k)) × x^k × (1-x)^(pred (pred n)-k)).
    rewrite INRpred, INRS by lia.
    replace (n-S(S k))%nat with (pred (pred n) - k)%nat by lia.
    simpl. field. assert (1<INR n) by (apply lt_1_INR; lia). lra.
    rewrite pascal4' by lia.
    simpl pred.
    rewrite 2Rmult_assoc, <-(Rmult_assoc (C _ _)).
  close_sum.
  rewrite <-xsum, binomial'' by lia.
  open_sum k Hk.
    transitivity (x/INR n × (C (pred n) k × x^k × (1-x)^(pred n-k))).
    replace (pred n-k)%nat with (n-S k)%nat by lia.
    simpl. field. neq_0.
  close_sum.
  rewrite <-xsum,binomial'' by lia.
  field. neq_0.
Qed.

Weierstrass' theorem: polynomials are dense in C(a,b)


Definition nup (x: R) := Z.to_nat (up x).

Lemma IPR_pos p: 0<IPR p.
Proof.
  assert(H: q, 0<IPR_2 q).
  induction q; simpl; nra.
  destruct p; unfold IPR; try specialize (H p); lra.
Qed.

Lemma nup_above x: x < INR (nup x).
Proof.
  unfold nup.
  destruct (archimed x) as [H H'].
  destruct (up x) as [|z|z]; simpl in ×.
  now rewrite INR0.
  now rewrite INR_IPR.
  rewrite INR0. unfold IZR in ×. pose proof (IPR_pos z). lra.
Qed.

Lemma C_pos n k: 0 < C n k.
Proof.
  apply Rdiv_lt_0_compat. apply fact_gt_0.
  pose proof (fact_gt_0 k).
  pose proof (fact_gt_0 (n-k)).
  nra.
Qed.

Lemma b_pos n k x: 0<=x<=1 → 0 ≤ b n k x.
Proof.
  intro H. unfold b. apply Rmult_le_pos. apply Rmult_le_pos.
  apply Rlt_le, C_pos.
  apply pow_le, H.
  apply pow_le. lra.
Qed.

Lemma Ikn k n: (kn)%nat → (0<n)%nat → 0<=INR k/INR n<=1.
Proof.
  intros. pose proof (pos_INR k).
  assert(INR kINR n) by now apply le_INR.
  assert(0 < INR n) by now apply lt_0_INR.
  split; apply Rmult_le_reg_l with (INR n). assumption.
  ring_simplify. replace (_ × _) with (INR k). assumption. field. neq_0. assumption.
  ring_simplify. replace (_ × _) with (INR k). assumption. field. neq_0.
Qed.

Definition Rlt_bool x y := if Rlt_dec x y then true else false.

Definition norm_inf a b f g e := x, axbRabs (f x - g x) ≤ e.

Lemma Rdiv_ge0 a b: 0 ≤ a → 0 < b → 0 ≤ a / b.
Proof.
  intros. assert (0 < /b) by now apply Rinv_0_lt_compat. nra.
Qed.

Lemma Weierstrass_aux1 d x y: 0 < dRabs (x-y) → 1 ≤ ((x-y)/d)^2.
Proof.
  intro H. rewrite <-Ratan.pow2_abs. apply pow_R1_Rle.
  unfold Rdiv. rewrite Rabs_mult. apply Rmult_le_reg_l with d. tauto.
  replace (Rabs (/d)) with (/d).
  field_simplify. split_Rabs; lra. lra.
  symmetry; apply Rabs_pos_eq.
  apply proj1, Rinv_0_lt_compat in H. lra.
Qed.

Lemma Weierstrass_aux2 x: 0 ≤ x ≤ 1 → x*(1-x) ≤ 1.
Proof.
  intro H. replace 1 with (1*1) at 2 by ring.
  apply Rmult_le_compat; lra.
Qed.

Theorem Heine01 f:
  ( x, 0<=x<=1 → continuous_at f x) →
   e, 0<e d, 0<d x y, 0<=x<=1 → 0<=y<=1 → Rabs (x-y) ≤ dRabs (f x - f y) ≤ e.
Proof.
  intros F e E.
  assert(UC: uniform_continuity f (fun x ⇒ 0<=x<=1)).
   apply Heine. apply compact_P3. intros. apply continuous_at_standard. now apply F.
  specialize (UC (mkposreal _ E)) as ((d&D)&Hd). simpl in Hd.
   (d/2). split. lra.
  intros x y. specialize (Hd x y). lra.
Qed.

first on the interval 0;1

Theorem Weierstrass01 f:
  ( x, 0<=x<=1 → continuous_at f x) →
   e, 0<e p, is_poly pnorm_inf 0 1 f p e.
Proof.
  intros F e E.
  destruct (Heine01 _ F (e/2)) as (d&D&Hd). lra.
  destruct (continuity_ab_maj (fun xRabs (f x)) 0 1) as (m&Hm&Im). lra.
   intros x Hx. apply continuous_at_standard.
   apply (continuous_comp f Rabs). now apply F. apply continuous_Rabs.
  clear F.
  set(M:=Rabs (f m)) in ×.
  assert(M': 0<=M) by (unfold M; clear; split_Rabs; lra).
  set (n := nup (4*M/(e×d^2))).
  assert(N: 0<INR n).
   eapply Rle_lt_trans. 2: apply nup_above.
   apply Rdiv_ge0. lra.
   apply Rmult_lt_0_compat. assumption. nra.
  assert(N': (0<n)%nat).
   apply INR_lt. now rewrite INR0.
   (B n f). split. apply is_poly_B.
  intros x Ix. unfold B.
  replace (f x) with (f x × 1) by lra.
  rewrite <-(binomial' x n), xsum, <-sum_minus.
  open_sum k Hk.
    transitivity ((f x - f (INR k / INR n))* b n k x). unfold b. ring.
  close_sum.
  rewrite (split_sum (fun kRlt_bool (Rabs (x - INR k / INR n)) d)).
  rewrite Rabs_triang.
  replace e with (e/2 + e/2) by field.
  apply Rplus_le_compat.
  - rewrite Rabs_sum.
    transitivity (sum (S n) (fun ke/2 × b n k x)). apply sum_le.
    intros k Hk. unfold Rlt_bool. case Rlt_dec.
    × intro H. rewrite Rabs_mult. apply Rmult_le_compat.
      apply Rabs_pos. apply Rabs_pos. apply Hd; trivial. apply Ikn; lia. lra.
      rewrite Rabs_pos_eq. reflexivity. now apply b_pos.
    × intros _. rewrite Rabs_R0. apply Rmult_le_pos. lra. now apply b_pos.
    × rewrite <-xsum. unfold b. rewrite binomial'. lra.
  - rewrite Rabs_sum.
    transitivity (sum (S n) (fun k ⇒ 2*M*(((x-INR k/INR n)/d)^2 × b n k x))).
    -- apply sum_le. intros k Hk. unfold Rlt_bool. case Rlt_dec; swap 1 2.
    × intro L. rewrite Rabs_mult, <-Rmult_assoc. apply Rmult_le_compat.
      apply Rabs_pos. apply Rabs_pos. unfold Rminus at 1. rewrite Rabs_triang.
      rewrite Rabs_Ropp, 2Hm. apply Rnot_lt_le in L.
      erewrite <-Rmult_le_compat_l. 3: now apply Weierstrass_aux1.
      now ring_simplify. lra.
      apply Ikn; lia. assumption.
      rewrite Rabs_pos_eq. reflexivity. now apply b_pos.
    × intros _. rewrite Rabs_R0, <-Rmult_assoc. apply Rmult_le_pos. apply Rmult_le_pos.
      lra. apply Ratan.pow2_ge_0. now apply b_pos.
    --
      
      rewrite <-xsum.
      open_sum k Hk.
        transitivity
          (1/d^2*(x^2*b n k x
                    + -2*x*(INR k/INR n × b n k x)
                    + (INR k/INR n)^2*b n k x)).
        field. lra.
      close_sum.
      rewrite <-xsum.
      rewrite 2sum_plus.
      rewrite <-2xsum.
      setoid_rewrite binomial'.
      setoid_rewrite Bx. 2: assumption.
      setoid_rewrite Bx2. 2: assumption.
      field_simplify. 2: lra.
      apply Rmult_le_reg_l with (2*d^2*INR n).
       apply Rmult_lt_0_compat; nra.       field_simplify. 2: lra.
      etransitivity; swap 1 2.
       apply Rmult_le_compat_r. lra.
       apply Rmult_le_compat_l. nra.
      apply Rlt_le, nup_above.
      field_simplify. 2: lra.
      transitivity (4*M*(x*(1-x))). now ring_simplify.
      erewrite Rmult_le_compat_l. 3: now apply Weierstrass_aux2.
      now ring_simplify. lra.
Qed.

then on an arbitrary interval a;b

Definition scale a b x := a + (b-a)*x.
Lemma scale01 a b x: ab → 0<=x<=1 → ascale a b xb.
Proof. intros. unfold scale; nra. Qed.

Definition unscale a b x := (x-a)/(b-a).
Lemma unscale01 a b x: a<baxb → 0<=unscale a b x<=1.
Proof.
  intros. unfold unscale.
  split; apply Rmult_le_reg_l with (b-a); field_simplify; lra.
Qed.

Lemma scale_unscale a b x: a<bscale a b (unscale a b x) = x.
Proof. intro. unfold scale, unscale. field. lra. Qed.

Notation scale' f a b := (fun xf (scale a b x)).
Notation unscale' f a b := (fun xf (unscale a b x)).

Corollary Weierstrass f a b:
  ( x, axbcontinuous_at f x) →
   e, 0<e p, is_poly pnorm_inf a b f p e.
Proof.
  intros C e E.
  destruct (Rlt_le_dec a b) as [AB|BA].
  - destruct (fun CWeierstrass01 (scale' f a b) C e E) as (p&P&N).
     intros x X. apply continuous_comp.
     apply continuous_plus. apply continuous_cst. apply continuous_mult. apply continuous_cst. apply continuous_id.
     apply C. apply scale01; lra.
     (unscale' p a b). split.
     apply is_poly_comp. assumption. apply is_poly_mult. apply is_poly_plus. apply is_poly_id. apply is_poly_cst. apply is_poly_cst.
    intros x X.
    specialize (N (unscale a b x)).
    simpl in N. rewrite scale_unscale in N by assumption.
    apply N. now apply unscale01.
  - (fun _f a). split. apply is_poly_cst.
    intros x X. replace x with a by lra. split_Rabs; lra.
Qed.

This page has been generated by coqdoc