# 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