Library p1_weierstrass
binomial coefficients, polynomials, continuity, Weierstrass' theorem through Bernstein's polynomials
Require Import ssreflect. Require Import Setoid Morphisms. Require Import Arith Psatz. Require Import List. Import ListNotations Nat. Require Import Rbase Rfunctions Ranalysis.
Fixpoint fact n :=
match n with
| 0 ⇒ 1
| S n' ⇒ fact n' × n
end.
Lemma fact_neq0: ∀ n, fact n ≠ 0.
Proof. induction n; cbn; lia. Qed.
Fixpoint C n k :=
match n,k with
| _,0 ⇒ 1
| 0,_ ⇒ 0
| S n',S k' ⇒ C n' k' + C n' k
end.
Lemma Cn0: ∀ n, C n 0 = 1.
Proof. by destruct n. Qed.
Lemma Cn1: ∀ n, C n 1 = n.
Proof.
induction n; cbn; trivial.
by rewrite Cn0 IHn.
Qed.
Lemma Cn2: ∀ n, C n 2 × 2 = n × (n - 1).
Proof.
induction n; cbn; trivial.
rewrite Cn1.
transitivity (n×2 + C n 2 × 2). ring.
rewrite IHn. destruct n; cbn; lia.
Qed.
Lemma Czer': ∀ n k, n<k ↔ C n k = 0.
Proof.
induction n; cbn; intros [|k]; try lia.
rewrite eq_add_0 -2!IHn. lia.
Qed.
Lemma Czer: ∀ n k, n<k → C n k = 0.
Proof. apply Czer'. Qed.
Lemma Cpos: ∀ n k, k≤n → 0 < C n k.
Proof. intros n k. generalize (Czer' n k). lia. Qed.
Lemma Cnn: ∀ n, C n n = 1.
Proof.
induction n; cbn.
- reflexivity.
- rewrite IHn Czer; lia.
Qed.
Lemma factC: ∀ n k, k≤n → fact n = C n k × fact k × fact (n - k).
Proof.
induction n; intros [|k] H; cbn; try lia.
destruct (eq_nat_dec k n) as [<-|H'].
- rewrite Cnn. rewrite Czer. lia.
rewrite sub_diag. cbn. lia.
- transitivity ( C n k × fact k × fact (n-k) × S k
+ C n (S k) × fact (S k) × fact (n-S k) × (n - k)
).
rewrite -!IHn; lia.
set c := C n k.
set d := C n (S k).
replace (n-k) with (S (n-S k)) by lia.
cbn. ring.
Qed.
Corollary Cfact: ∀ n k, k≤n → C n k = fact n / (fact k × fact (n - k)).
Proof.
intros. rewrite (factC n k)//.
rewrite -mul_assoc div_mul//.
by rewrite -neq_mul_0; split; apply fact_neq0.
Qed.
Lemma Csym: ∀ n k, k ≤ n → C n k = C n (n - k).
Proof.
intros n k H.
apply mul_cancel_l with (fact k × fact (n - k)).
by rewrite -neq_mul_0; split; apply fact_neq0.
transitivity (fact n).
- rewrite (factC n k); lia.
- rewrite (factC n (n-k)). lia.
replace (n-(n-k)) with k; lia.
Qed.
Lemma Cpion: ∀ n k, C (S n) (S k) × S k = C n k × S n.
Proof.
intros n k. destruct (le_lt_dec k n) as [L|L].
- apply mul_cancel_l with (fact k × fact (n - k)).
by rewrite -neq_mul_0; split; apply fact_neq0.
transitivity (fact (S n)).
-- rewrite (factC (S n) (S k)). lia.
simpl. lia.
-- cbn. rewrite (factC n k); lia.
- rewrite !Czer; lia.
Qed.
Open Scope R_scope.
Global Instance Rle_rw: RewriteRelation Rle := {}.
Global Instance Rle_PreOrder: PreOrder Rle.
Proof. constructor; cbv; intros; lra. Qed.
Global Instance Rplus_Rle: Proper (Rle ==> Rle ==> Rle) Rplus.
Proof. repeat intro. lra. Qed.
Fixpoint sum n f :=
match n with
| O ⇒ 0
| S n ⇒ sum n f + f n
end.
Lemma sum0 f: sum 0 f = 0.
Proof. reflexivity. Qed.
Lemma sum1 f: sum 1 f = f 0%nat.
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 i ⇒ f (S i)).
Proof.
induction n as [|n IH].
- simpl; ring.
- rewrite sumS_last IH. simpl. ring.
Qed.
Lemma sum_last n f: (0<n)%nat → sum n f = sum (pred n) f + f (pred n).
Proof. destruct n. lia. reflexivity. Qed.
Lemma sum_first n f: (0<n)%nat → sum n f = f 0%nat + sum (pred n) (fun i ⇒ f (S i)).
Proof. destruct n. lia. intros _. apply sumS_first. Qed.
Lemma xsum n x f: x × sum n f = sum n (fun i ⇒ x × f i).
Proof.
induction n; simpl.
- ring.
- rewrite -IHn. ring.
Qed.
Lemma sum_plus n f g: sum n (fun i ⇒ f 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 i ⇒ f i - g i) = sum n f - sum n g.
Proof.
induction n; simpl.
- ring.
- rewrite IHn. ring.
Qed.
Lemma sum_rev n f: sum n f = sum n (fun i ⇒ f (n-S i)%nat).
Proof.
induction n. reflexivity.
rewrite sumS_last sumS_first IHn.
simpl. replace (n - 0)%nat with n by lia. ring.
Qed.
Lemma sum_eq n f g: (∀ i, (i<n)%nat → f i = g i) → sum n f = sum n g.
Proof.
intros H; induction n; simpl.
- reflexivity.
- rewrite H. lia. rewrite IHn//. intros. apply H. lia.
Qed.
Lemma sum_le n f g: (∀ i, (i<n)%nat → f i ≤ g i) → sum n f ≤ sum n g.
Proof.
intros H; induction n; simpl.
- reflexivity.
- rewrite H. lia. rewrite IHn. 2: reflexivity. intros. apply H. lia.
Qed.
Global Instance sum_pwr_eq n: Proper (pointwise_relation nat Logic.eq ==> Logic.eq) (sum n).
Proof. intros ???. apply sum_eq. intros ? _. apply H. Qed.
Global 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: nat → bool) n f:
sum n f =
sum n (fun i ⇒ if p i then f i else 0) +
sum n (fun i ⇒ if 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 i ⇒ Rabs (f i)).
Proof.
induction n; simpl.
- split_Rabs; lra.
- now rewrite Rabs_triang IHn.
Qed.
Arguments sum: simpl never.
Check INR.
Lemma INR0: INR O = 0. Proof. reflexivity. Qed.
Lemma INR1: INR 1 = 1. Proof. reflexivity. Qed.
Lemma INReq (n m: nat): n = m ↔ INR n = INR m.
Proof. split; auto using INR_eq. Qed.
Lemma INRle (n m: nat): (n ≤ m)%nat ↔ INR n ≤ INR m.
Proof. split; auto using INR_le, le_INR. Qed.
Lemma INRlt (n m: nat): (n < m)%nat ↔ INR n < INR m.
Proof. split. unfold Peano.lt. rewrite INRle S_INR. lra. apply INR_lt. Qed.
Definition NR := (INR0, INR1,S_INR,plus_INR,mult_INR,INReq,INRle,INRlt).
Lemma INRpred n: (0<n)%nat → INR (pred n) = INR n - 1.
Proof. destruct n. lia. rewrite S_INR/=. lra. Qed.
Arguments INR: simpl never.
Coercion INR: nat >-> R.
Check 4%nat + 3.14.
Set Printing Coercions.
Check 4%nat + 3.14.
Unset Printing Coercions.
Ltac neq_0 := repeat split; solve [ apply not_O_INR; lia ].
Goal ∀ n x y, (n>0)%nat → (x+y)/n = x/n + y/n.
Proof. intros. field. neq_0. Qed.
Lemma Rdiv0 n: 0 / n = 0.
Proof. unfold Rdiv. ring. Qed.
Lemma cancel_r x y z: y-x=z-x → y=z.
Proof. lra. Qed.
Proposition binomial: ∀ x y n,
(x + y) ^ n = sum (S n) (fun i ⇒ C n i × x ^ i × y ^ (n - i)).
Proof.
intros; induction n as [|n IH].
- rewrite sum1 Cn0 !NR /=. ring.
- rewrite sumS_last sumS_first /= !NR.
rewrite Cnn (Czer n (S n)). lia.
rewrite NR IH Rmult_plus_distr_r 2!xsum.
rewrite sumS_last sumS_first /=.
rewrite !Cn0 !Cnn sub_diag sub_0_r !NR.
apply cancel_r with (x^(S n)+y^(S n)). simpl. ring_simplify.
rewrite -sum_plus. apply sum_eq. intros.
rewrite !NR.
replace (n-i)%nat with (S (n-(S i))) by lia.
simpl. ring.
Qed.
Corollary binomial' x n: sum (S n) (fun k ⇒ C n k × x^k × (1-x)^(n-k)) = 1.
Proof.
rewrite -binomial.
replace (x+(1-x)) with 1 by ring. apply pow1.
Qed.
Corollary binomial'' x n: (0<n)%nat → sum n (fun k ⇒ C (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 i ⇒ C n i) = 2^n.
Proof.
intro. replace 2 with (1+1) by ring.
rewrite binomial. apply sum_eq. intros.
rewrite 2!pow1. ring.
Qed.
Corollary powk2n: ∀ n, sum (S n) (fun i ⇒ i × C n i) = n × 2^(n-1).
Proof.
intro. rewrite -pow2n. rewrite xsum.
destruct n. reflexivity.
rewrite sumS_first. rewrite NR. ring_simplify.
replace (S n - 1)%nat with n by lia.
apply sum_eq. intros i Hi.
rewrite Rmult_comm -NR Cpion !NR. ring.
Qed.
polynomials, continuity
polynomials
Definition poly := list R.
Fixpoint eval (P: poly) (x: R): R :=
match P with
| [] ⇒ 0
| a::Q ⇒ a + 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::P ⇒ pplus (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 /= IH. ring.
Qed.
Fixpoint pcomp (P Q: poly): poly :=
match P with
| [] ⇒ []
| a::P ⇒ pplus (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.
Fixpoint eval (P: poly) (x: R): R :=
match P with
| [] ⇒ 0
| a::Q ⇒ a + 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::P ⇒ pplus (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 /= IH. ring.
Qed.
Fixpoint pcomp (P Q: poly): poly :=
match P with
| [] ⇒ []
| a::P ⇒ pplus (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.
Definition is_poly (f: R → R) := ∃ 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 x ⇒ x).
Proof. ∃ pid. apply eval_id. Qed.
Lemma is_poly_xk k: is_poly (fun x ⇒ x^k).
Proof. ∃ (pxk k). apply eval_xk. Qed.
Lemma is_poly_plus f g: is_poly f → is_poly g → is_poly (fun x ⇒ f 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 f → is_poly (fun x ⇒ a × 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 f → is_poly g → is_poly (fun x ⇒ f 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 f → is_poly g → is_poly (fun x ⇒ f (g x)).
Proof.
intros (P&Pf) (Q&Qg). ∃ (pcomp P Q).
intro. now rewrite eval_comp Pf Qg.
Qed.
Global Instance is_poly_Proper: Proper (pointwise_relation R Logic.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<n → is_poly (f i))%nat → is_poly (fun x ⇒ sum n (fun i ⇒ f 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.
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 x ↔ continuity_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 x → continuous_at g x → continuous_at (fun y ⇒ f 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 Rmin_case.
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. lra.
rewrite 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 x → continuous_at g (f x) → continuous_at (fun y ⇒ g (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≤x → x/(x+1) ≤ 1.
Proof.
intro. apply (Rmult_le_reg_l (x+1)). lra.
field_simplify; lra.
Qed.
Goal ∀ a b c, a≤b → 0<=c → a×c ≤ b×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 x → continuous_at g x → continuous_at (fun y ⇒ f 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 Rmin_case. 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 Rmin_case. 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 Rmin_case.
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 2!Rabs_triang 3!Rabs_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. lra. apply Rmin_r.
rewrite Hdg. 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.
continuous_at f x ↔ continuity_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 x → continuous_at g x → continuous_at (fun y ⇒ f 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 Rmin_case.
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. lra.
rewrite 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 x → continuous_at g (f x) → continuous_at (fun y ⇒ g (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≤x → x/(x+1) ≤ 1.
Proof.
intro. apply (Rmult_le_reg_l (x+1)). lra.
field_simplify; lra.
Qed.
Goal ∀ a b c, a≤b → 0<=c → a×c ≤ b×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 x → continuous_at g x → continuous_at (fun y ⇒ f 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 Rmin_case. 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 Rmin_case. 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 Rmin_case.
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 2!Rabs_triang 3!Rabs_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. lra. apply Rmin_r.
rewrite Hdg. 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.
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 x ⇒ x^(n-k))).
apply is_poly_xk. apply is_poly_plus. apply is_poly_cst. apply is_poly_opp.
Qed.
Definition B n g := fun x ⇒ sum (S n) (fun k ⇒ g (k / 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.
Lemma Cpion': ∀ n i, (0<n ∧ 0<i)%nat → i / n × C n i = C (pred n) (pred i).
Proof.
intros [|n] [|i]; try (cbn; lia).
intros _. simpl pred.
have D: INR (S n) ≠ 0 by neq_0.
apply Rmult_eq_reg_r with (S n); trivial.
rewrite -NR -Cpion 4!NR. field.
now rewrite -NR.
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)%nat → B n (fun x ⇒ x) x = x.
Proof.
intros N. unfold B, b.
rewrite sumS_first NR Rdiv0. ring_simplify.
open_sum k Hk.
rewrite -2!Rmult_assoc Cpion'. 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''//. ring.
Qed.
Lemma Bx2 n x: (0<n)%nat → B n (fun x ⇒ x^2) x = x/n + x^2 × (n-1)/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 Cn0 Cnn 2!NR /=. field.
rewrite sumS_first NR Rdiv0. ring_simplify.
open_sum k Hk.
rewrite -2!Rmult_assoc.
replace (_^2 × _) with (S k / n × (S k / n × C n (S k))) by ring.
rewrite Cpion'. lia.
rewrite NR. replace (_/_) with (k/n + 1/n) by (field; neq_0).
rewrite 3!Rmult_plus_distr_r.
close_sum.
rewrite sum_plus.
rewrite sum_first. lia. rewrite NR Rdiv0. ring_simplify.
open_sum k Hk.
transitivity (((n - 1) / n × x^2) × (S k / pred n × C (pred n) (S k)) × x^k × (1-x)^(pred (pred n)-k)).
rewrite NR INRpred. lia.
replace (n-S(S k))%nat with (pred (pred n) - k)%nat by lia.
simpl. field. rewrite !NR in N. lra.
rewrite Cpion'. lia.
simpl pred.
rewrite 2!Rmult_assoc -(Rmult_assoc (C _ _)).
close_sum.
rewrite -xsum binomial''. lia.
open_sum k Hk.
transitivity (x/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.
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 < nup x.
Proof.
unfold nup.
destruct (archimed x) as [H H'].
destruct (up x) as [|z|z]; simpl in ×.
now rewrite NR.
now rewrite INR_IPR.
rewrite NR. unfold IZR in ×. pose proof (IPR_pos z). lra.
Qed.
Lemma C_pos n k: (k ≤ n)%nat → 0 < C n k.
Proof.
intro kn. apply Cpos, lt_INR in kn.
now rewrite NR in kn.
Qed.
Lemma b_pos n k x: (k ≤ n)%nat → 0≤x≤1 → 0 ≤ b n k x.
Proof.
intros kn H. unfold b. apply Rmult_le_pos. apply Rmult_le_pos.
apply Rlt_le, C_pos, kn.
apply pow_le, H.
apply pow_le. lra.
Qed.
Lemma Ikn k n: (k≤n)%nat → (0<n)%nat → 0≤k/n≤1.
Proof.
intros. pose proof (pos_INR k).
assert(k ≤ n) by now apply le_INR.
assert(0 < n) by now apply lt_0_INR.
split; apply Rmult_le_reg_l with 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 := match Rlt_dec x y with left _ ⇒ true | _ ⇒ false end.
Definition norm_inf a b f g e := ∀ x, a≤x≤b → Rabs (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 < d ≤ Rabs (x-y) → 1 ≤ ((x-y)/d)^2.
Proof.
intro H. rewrite <-Ratan.pow2_abs. apply pow_R1_Rle.
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. transitivity (1×1). 2: lra.
apply Rmult_le_compat; lra.
Qed.
we first prove the theorem on the interval 0;1, and we rely for
that on Heine's theorem, which is in the standard library.
we state it here with a form which is more convenient in the sequel.
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) ≤ d → Rabs (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.
Weierstrass' theorem, first on the interval 0;1
Theorem Weierstrass01 f:
(∀ x, 0≤x≤1 → continuous_at f x) →
∀ e, 0<e → ∃ p, is_poly p ∧ norm_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 x ⇒ Rabs (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 Hm.
assert(M': 0≤M) by apply Rabs_pos.
set (n := nup (4×M/(e×d^2))).
assert(N: 0<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) by now rewrite NR.
∃ (B n f). split. apply is_poly_B.
intros x Ix.
replace (f x - B n f x) with (sum (S n) (fun k ⇒ (f x - f (k/n)) × b n k x)); first last.
{ setoid_rewrite Rmult_minus_distr_r.
rewrite sum_minus. f_equal.
rewrite -xsum binomial'. lra. }
rewrite (split_sum (fun k ⇒ Rlt_bool (Rabs (x-k/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 k ⇒ e/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. apply b_pos; trivial; lia. reflexivity.
× intros _. rewrite Rabs_R0. apply Rmult_le_pos. lra. apply b_pos; trivial; lia.
× rewrite <-xsum. rewrite binomial'. lra.
- rewrite Rabs_sum.
transitivity (sum (S n) (fun k ⇒ 2×M*(((x-k/n)/d)^2 × b n k x))).
-- apply sum_le. intros k Hk. unfold Rlt_bool. case Rlt_dec.
× intros _. rewrite Rabs_R0. apply Rmult_le_pos. lra. apply Rmult_le_pos.
apply Ratan.pow2_ge_0. apply b_pos; trivial; lia.
× intro L. rewrite Rabs_mult -Rmult_assoc. apply Rmult_le_compat.
apply Rabs_pos. apply Rabs_pos. rewrite Rabs_triang.
rewrite Rabs_Ropp Hm//Hm. apply Ikn; lia.
erewrite <-Rmult_le_compat_l. 3: apply Weierstrass_aux1; lra. lra. lra.
rewrite Rabs_pos_eq. apply b_pos; trivial; lia. reflexivity.
--
transitivity (2 × M × ((x - x^2) / (n × d^2))). apply Req_le.
{ rewrite -xsum. f_equal.
open_sum k Hk.
transitivity
(1/d^2*(x^2×b n k x
+ -2×x*(k/n × b n k x)
+ (k/n)^2×b n k x)).
field. lra.
close_sum.
rewrite -xsum.
rewrite 2!sum_plus.
rewrite -2!xsum.
setoid_rewrite binomial'.
setoid_rewrite Bx. 2: assumption.
setoid_rewrite Bx2. 2: assumption.
field. lra.
}
apply Rmult_le_reg_l with (2×d^2×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))). lra.
erewrite Rmult_le_compat_l. 3: now apply Weierstrass_aux2.
lra. lra.
Qed.
then on an arbitrary interval a;b
Definition scale a b x := a + (b-a)*x.
Lemma scale01 a b x: a≤b → 0≤x≤1 → a≤scale a b x≤b.
Proof. intros. unfold scale; nra. Qed.
Definition unscale a b x := (x-a)/(b-a).
Lemma unscale01 a b x: a<b → a≤x≤b → 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<b → scale a b (unscale a b x) = x.
Proof. intro. unfold scale, unscale. field. lra. Qed.
Notation scale' f a b := (fun x ⇒ f (scale a b x)).
Notation unscale' f a b := (fun x ⇒ f (unscale a b x)).
Corollary Weierstrass f a b:
(∀ x, a≤x≤b → continuous_at f x) →
∀ e, 0<e → ∃ p, is_poly p ∧ norm_inf a b f p e.
Proof.
intros C e E.
destruct (Rlt_le_dec a b) as [AB|BA].
- destruct (fun C ⇒ Weierstrass01 (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.
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