From 3a6036f2a7ba9aab4769394e42d75f91cf5ab6ca Mon Sep 17 00:00:00 2001 From: Laurence Rideau Date: Sat, 28 Sep 2024 16:30:26 +0900 Subject: [PATCH 1/3] initial commit --- theories/exercise6.v | 231 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 231 insertions(+) create mode 100644 theories/exercise6.v diff --git a/theories/exercise6.v b/theories/exercise6.v new file mode 100644 index 000000000..4831e122f --- /dev/null +++ b/theories/exercise6.v @@ -0,0 +1,231 @@ +From elpi Require Import elpi. +From HB Require Import structures. +From mathcomp Require Import all_ssreflect. +From mathcomp Require Import all_algebra. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** *** Exercices on polynomials +- Formalisation of the algebraic part of a + simple proof that PI is irrational described in: +- http://projecteuclid.org/download/pdf_1/euclid.bams/1183510788 +*) + +Section Algebraic_part. + +Open Scope ring_scope. +Import GRing.Theory Num.Theory. + +(** *** Parameters definitions: +- Let n na nb be natural numbers +- Suppose nb is a non zero nat: nb != 0 +- Define the corresponding rationals a , b +- Define pi as a/b. +*) +(* to complete for na nb*) +Variable n : nat. +(*D*)Variables na nb: nat. +Hypothesis nbne0: nb != 0%N. + +Definition a:rat := (Posz na)%:~R. +Definition b:rat := +(*D*)(Posz nb)%:~R. + +Definition pi := +(*D*)a / b. + +(** *** Definition of the polynomials: +- Look at the f definition: the factorial, the coercion nat :> R (as a Ring), etc... +- Define F:{poly rat} using bigop. +*) +Definition f :{poly rat} := + (n`!)%:R^-1 *: ('X^n * (a%:P - b*:'X)^+n). + +(*D*)Definition F :{poly rat} := \sum_(i < n.+1) (-1)^i *: f^`(2*i). + + +(** *** Prove that: +- b is non zero rational. +*) +(* Some intermediary simple theorems *) +Lemma bne0: b != 0. +(*D*)Proof. by rewrite intr_eq0. Qed. +(** *** Prove that: +- (a - bX) has a size of 2 +*) +Lemma P1_size: size (a%:P - b*:'X) = 2%N. +Proof. +(*D*)have hs: size (- (b *: 'X)) = 2%N. +(*D*) by rewrite size_opp size_scale ?bne0 // size_polyX. +(*D*)by rewrite addrC size_addl hs ?size_polyC //; case:(a!= 0). +Qed. + +(** *** Prove that: +- the lead_coef of (a - bX) is -b. +*) +Lemma P1_lead_coef: lead_coef (a%:P - b*:'X) = -b. +Proof. +(*D*)rewrite addrC lead_coefDl. +(*D*) by rewrite lead_coefN lead_coefZ lead_coefX mulr1. +(*D*)by rewrite size_opp size_scale ?bne0 // size_polyX size_polyC; case:(a!= 0). +Qed. + +(** *** Prove that: +- the size of (a-X)^n is n.+1 +*) +Lemma P_size : size ((a%:P - b*:'X)^+n) = n.+1. +(*D*)elim:n=>[| n0 Hn0]; first by rewrite expr0 size_polyC. +(*D*)rewrite exprS size_proper_mul. +(*D*) by rewrite P1_size /= Hn0. +(*D*)by rewrite lead_coef_exp P1_lead_coef -exprS expf_neq0 // oppr_eq0 bne0. +Qed. + +(* 2 useful lemmas for the Qint predicat. *) +Lemma int_Qint (z:int) : z%:~R \is a Qint. +Proof. by apply/QintP; exists z. Qed. + +Lemma nat_Qint (m:nat) : m%:R \is a Qint. +Proof. by apply/QintP; exists m. Qed. + +(** *** Prove that: +- Exponent and composition of polynomials combine: +*) +Lemma comp_poly_exprn: + forall (p q:{poly rat}) i, p^+i \Po q = (p \Po q) ^+i. +(*D*)move=> p q; elim=>[| i Hi]. +(*D*) by rewrite !expr0 comp_polyC. +(*D*)by rewrite !exprS comp_polyM Hi. +Qed. + + +(** *** Prove that: +- f's small coefficients are zero +*) +(* Let's begin the Niven proof *) +Lemma f_small_coef0 i: (i < n)%N -> f`_i = 0. +Proof. +(*D*)move=> iltn;rewrite /f coefZ. +(*D*)apply/eqP; rewrite mulf_eq0 invr_eq0 pnatr_eq0 eqn0Ngt (fact_gt0 n) /=. +(*D*)by rewrite coefXnM iltn. +Qed. + +(** *** Prove that: +- f/n! as integral coefficients +*) + +Lemma f_int i: (n`!)%:R * f`_i \is a Qint. +Proof. +(*D*)rewrite /f coefZ mulrA mulfV; last by rewrite pnatr_eq0 -lt0n (fact_gt0 n). +(*D*)rewrite mul1r; apply/polyOverP. +(*D*)rewrite rpredM ?rpredX ?polyOverX //. +(*D*)by rewrite rpredB ?polyOverC ?polyOverZ ?polyOverX // int_Qint. +Qed. + +(** *** Prove that: +the f^`(i) (x) have integral values for x = 0 +*) +Lemma derive_f_0_int: forall i, f^`(i).[0] \is a Qint. +Proof. +(*D*)move=> i. +(*D*)rewrite horner_coef0 coef_derivn addn0 binomial.ffactnn. +(*D*)case:(boolP (i . +(*D*) by rewrite mul0rn // int_Qint. +(*D*)rewrite -leqNgt. +(*D*)move/binomial.bin_fact <-. +(*D*)rewrite /f coefZ -mulrnAl -mulr_natr mulrC rpredM //; last first. +(*D*) rewrite mulnC !natrM !mulrA mulVf ?mul1r ?rpredM ?nat_Qint //. +(*D*) by rewrite pnatr_eq0 eqn0Ngt (fact_gt0 n). +(*D*)apply/polyOverP;rewrite rpredM // ?rpredX ?polyOverX //. +(*D*)by rewrite ?rpredB ?polyOverC ?polyOverZ ?polyOverX // int_Qint. +Qed. + +(** *** Deduce that: +F (0) has an integral value +*) + +Lemma F0_int : F.[0] \is a Qint. +Proof. +(*D*)rewrite /F horner_sum rpred_sum // => i _ ; rewrite !hornerE rpredM //. +(*D*) by rewrite -exprnP rpredX. +(*D*)by rewrite derive_f_0_int. +Qed. + +(** *** Then prove +- the symmetry argument f(x) = f(pi -x). +*) +Lemma pf_sym: f \Po (pi%:P -'X) = f. +Proof. +(*D*)rewrite /f comp_polyZ;congr (_ *:_). +(*D*)rewrite comp_polyM !comp_poly_exprn. +(*D*)rewrite comp_polyB comp_polyC !comp_polyZ !comp_polyX scalerBr /pi. +(*D*)have h1: b%:P * (a / b)%:P = a%:P. +(*D*) by rewrite polyCM mulrC -mulrA -polyCM mulVf ?bne0 // mulr1. +(*D*)suff->: (a%:P - (b *: (a / b)%:P - b *: 'X)) = b%:P * 'X. +(*D*) rewrite exprMn mulrA - exprMn [X in _ = X]mulrC. +(*D*) congr (_ *_); congr (_^+_). +(*D*) rewrite mulrC mulrBr; congr (_ -_)=>//. +(*D*) by rewrite mul_polyC. +(*D*)by rewrite -!mul_polyC h1 opprB addrA addrC addrA addNr add0r. +Qed. + +(** *** Prove +- the symmetry for the derivative +*) + +Lemma derivn_fpix i : + (f^`(i)\Po(pi%:P -'X))= (-1)^+i *: f^`(i). +Proof. +(*D*)elim:i ; first by rewrite /= expr0 scale1r pf_sym. +(*D*)move => i Hi. +(*D*)set fx := _ \Po _. +(*D*)rewrite derivnS exprS -scalerA -derivZ -Hi deriv_comp !derivE. +(*D*)by rewrite mulrBr mulr0 add0r mulr1 -derivnS /fx scaleN1r opprK. +Qed. + +(** *** Deduce that +- F(pi) is an integer +*) +Lemma FPi_int : F.[pi] \is a Qint. +Proof. +(*D*)rewrite /F horner_sum rpred_sum //. +(*D*)move=> i _ ; rewrite !hornerE rpredM //. +(*D*) by rewrite -exprnP rpredX. +(*D*)move:(derivn_fpix (2*i)). +(*D*)rewrite mulnC exprM sqrr_sign scale1r => <-. +(*D*)by rewrite horner_comp !hornerE subrr derive_f_0_int. +Qed. + + +(** *** if you have time +- you can prove the equality F^`(2) + F = f +- that is needed by the analytic part of the Niven proof +*) + +Lemma D2FDF : F^`(2) + F = f. +Proof. +(*D*)rewrite /F linear_sum /=. +(*D*)rewrite (eq_bigr (fun i:'I_n.+1 => (((-1)^i *: f^`(2 * i.+1)%N)))); last first. +(*D*) move=> i _ ;rewrite !derivZ; congr (_ *:_). +(*D*) rewrite -!derivnS;congr (_^`(_)). +(*D*) by rewrite mulnS addnC addn2. +(*D*)rewrite [X in _ + X]big_ord_recl muln0 derivn0. +(*D*)rewrite -exprnP expr0 scale1r (addrC f) addrA -[X in _ = X]add0r. +(*D*)congr (_ + _). +(*D*)rewrite big_ord_recr addrC addrA -big_split big1=>[| i _]. +(*D*) rewrite add0r /=; apply/eqP; rewrite scaler_eq0 -derivnS derivn_poly0. +(*D*) by rewrite eqxx orbT. +(*D*) suff ->: (size f) = (n + n.+1)%N by rewrite -plus_n_O leqnSn. +(*D*) rewrite /f size_scale; last first. +(*D*) by rewrite invr_neq0 // pnatr_eq0 -lt0n (fact_gt0 n). +(*D*) rewrite size_monicM ?monicXn //; last by rewrite -size_poly_eq0 P_size. +(*D*) by rewrite size_polyXn P_size. +(*D*)rewrite /bump /= -scalerDl. +(*D*)apply/eqP;rewrite scaler_eq0 /bump -exprnP add1n exprSr. +(*D*)by rewrite mulrN1 addrC subr_eq0 eqxx orTb. +Qed. + +End Algebraic_part. + From 6a5e34235d8e5134e51a667070c9abb99af34598 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 9 Oct 2024 08:56:01 +0900 Subject: [PATCH 2/3] complete Niven's proof --- theories/exercise6.v | 775 ++++++++++++++++++++++++++++++++----------- 1 file changed, 589 insertions(+), 186 deletions(-) diff --git a/theories/exercise6.v b/theories/exercise6.v index 4831e122f..ddccead5d 100644 --- a/theories/exercise6.v +++ b/theories/exercise6.v @@ -1,231 +1,634 @@ -From elpi Require Import elpi. -From HB Require Import structures. -From mathcomp Require Import all_ssreflect. -From mathcomp Require Import all_algebra. +From mathcomp Require Import all_ssreflect all_algebra archimedean. +From mathcomp Require Import finmap (*lra*). +Require Import mathcomp_extra boolp classical_sets functions. +Require Import cardinality fsbigop. +Require Import signed reals ereal topology normedtype sequences real_interval. +Require Import esum measure lebesgue_measure numfun realfun lebesgue_integral. +Require Import derive charge ftc trigo. + +(* Formalisation of a simple proof that PI is irrational described in: + http://projecteuclid.org/download/pdf_1/euclid.bams/1183510788 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -(** *** Exercices on polynomials -- Formalisation of the algebraic part of a - simple proof that PI is irrational described in: -- http://projecteuclid.org/download/pdf_1/euclid.bams/1183510788 -*) +Import Order.TTheory GRing.Theory Num.Theory. -Section Algebraic_part. +(* TODO: move to ssrnum? *) +Lemma prodr_ile1 {R : realDomainType} (s : seq R) : + (forall x, x \in s -> 0 <= x <= 1)%R -> (\prod_(j <- s) j <= 1)%R. +Proof. +elim: s => [_ | y s ih xs01]; rewrite ?big_nil// big_cons. +have /andP[y0 y1] : (0 <= y <= 1)%R by rewrite xs01// mem_head. +rewrite mulr_ile1 ?andbT//. + rewrite big_seq prodr_ge0// => x xs. + by have := xs01 x; rewrite inE xs orbT => /(_ _)/andP[]. +by rewrite ih// => e xs; rewrite xs01// in_cons xs orbT. +Qed. -Open Scope ring_scope. -Import GRing.Theory Num.Theory. +(* TODO: move to lebesgue_integral.v? *) +Section integral_fin_num_abs. +Local Open Scope ring_scope. +Context {d} {T : measurableType d} {R : realType}. +Variables (mu : {measure set T -> \bar R}) (D : set T). +Hypotheses (mD : measurable D). + +Lemma integral_fin_num_abs (f : T -> R) : measurable_fun D f -> + (\int[mu]_(x in D) `|(f x)%:E| < +oo)%E = + ((\int[mu]_(x in D) (f x)%:E)%E \is a fin_num). +Proof. +move=> mf; rewrite fin_num_abs; case H : LHS; apply/esym. +- by move: H => /abse_integralP ->//; exact/EFin_measurable_fun. +- apply: contraFF H => /abse_integralP; apply => //. + exact/EFin_measurable_fun. +Qed. -(** *** Parameters definitions: -- Let n na nb be natural numbers -- Suppose nb is a non zero nat: nb != 0 -- Define the corresponding rationals a , b -- Define pi as a/b. -*) -(* to complete for na nb*) -Variable n : nat. -(*D*)Variables na nb: nat. -Hypothesis nbne0: nb != 0%N. +End integral_fin_num_abs. + +(* TODO: move to lebesgue_integral.v *) +Section le_Rintegral. +Local Open Scope ring_scope. +Context {d} {T : measurableType d} {R : realType}. +Variables (mu : {measure set T -> \bar R}). +Variable (D : set T). +Hypotheses (mD : measurable D). +Variables f1 f2 : T -> R. +Local Open Scope ring_scope. +Hypotheses (mf1 : mu.-integrable D (EFin \o f1)) + (mf2 : mu.-integrable D (EFin \o f2)). + +Lemma le_Rintegral : (forall x, D x -> f1 x <= f2 x) -> + \int[mu]_(x in D) f1 x <= \int[mu]_(x in D) f2 x. +Proof. +move=> f12; rewrite /Rintegral fine_le//. +- rewrite -integral_fin_num_abs//; first by case/integrableP : mf1. + by apply/EFin_measurable_fun; case/integrableP : mf1. +- rewrite -integral_fin_num_abs//; first by case/integrableP : mf2. + by apply/EFin_measurable_fun; case/integrableP : mf2. +- by apply/le_integral => // x xD; rewrite lee_fin f12//; exact/set_mem. +Qed. -Definition a:rat := (Posz na)%:~R. -Definition b:rat := -(*D*)(Posz nb)%:~R. +End le_Rintegral. -Definition pi := -(*D*)a / b. - -(** *** Definition of the polynomials: -- Look at the f definition: the factorial, the coercion nat :> R (as a Ring), etc... -- Define F:{poly rat} using bigop. -*) -Definition f :{poly rat} := - (n`!)%:R^-1 *: ('X^n * (a%:P - b*:'X)^+n). - -(*D*)Definition F :{poly rat} := \sum_(i < n.+1) (-1)^i *: f^`(2*i). - - -(** *** Prove that: -- b is non zero rational. -*) -(* Some intermediary simple theorems *) -Lemma bne0: b != 0. -(*D*)Proof. by rewrite intr_eq0. Qed. -(** *** Prove that: -- (a - bX) has a size of 2 -*) -Lemma P1_size: size (a%:P - b*:'X) = 2%N. +(* TODO: move to lebesgue_integral.v *) +Lemma Rintegral_cst d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}%R) (D : set T) : (d.-measurable D)%classic -> + forall r, (\int[mu]_(x in D) (cst r) x = r * fine (mu D))%R. Proof. -(*D*)have hs: size (- (b *: 'X)) = 2%N. -(*D*) by rewrite size_opp size_scale ?bne0 // size_polyX. -(*D*)by rewrite addrC size_addl hs ?size_polyC //; case:(a!= 0). -Qed. - -(** *** Prove that: -- the lead_coef of (a - bX) is -b. -*) -Lemma P1_lead_coef: lead_coef (a%:P - b*:'X) = -b. -Proof. -(*D*)rewrite addrC lead_coefDl. -(*D*) by rewrite lead_coefN lead_coefZ lead_coefX mulr1. -(*D*)by rewrite size_opp size_scale ?bne0 // size_polyX size_polyC; case:(a!= 0). -Qed. - -(** *** Prove that: -- the size of (a-X)^n is n.+1 -*) -Lemma P_size : size ((a%:P - b*:'X)^+n) = n.+1. -(*D*)elim:n=>[| n0 Hn0]; first by rewrite expr0 size_polyC. -(*D*)rewrite exprS size_proper_mul. -(*D*) by rewrite P1_size /= Hn0. -(*D*)by rewrite lead_coef_exp P1_lead_coef -exprS expf_neq0 // oppr_eq0 bne0. -Qed. - -(* 2 useful lemmas for the Qint predicat. *) -Lemma int_Qint (z:int) : z%:~R \is a Qint. -Proof. by apply/QintP; exists z. Qed. - -Lemma nat_Qint (m:nat) : m%:R \is a Qint. -Proof. by apply/QintP; exists m. Qed. - -(** *** Prove that: -- Exponent and composition of polynomials combine: -*) -Lemma comp_poly_exprn: - forall (p q:{poly rat}) i, p^+i \Po q = (p \Po q) ^+i. -(*D*)move=> p q; elim=>[| i Hi]. -(*D*) by rewrite !expr0 comp_polyC. -(*D*)by rewrite !exprS comp_polyM Hi. +move=> mD r; rewrite /Rintegral/= integral_cst//. +have := leey (mu D); rewrite le_eqVlt => /predU1P[->/=|muy]; last first. + by rewrite fineM// ge0_fin_numE. +rewrite mulr_infty/=; have [_|r0|r0] := sgrP r. +- by rewrite mul0e/= mulr0. +- by rewrite mul1e/= mulr0. +- by rewrite mulN1e/= mulr0. Qed. +(* two useful lemmas for the Num.int predicate *) +Lemma int_int {R : archiNumDomainType} (z : int) : (z%:~R)%R \is a @Num.int R. +Proof. by []. Qed. + +Lemma nat_int {R : archiNumDomainType} (m : nat) : (m%:R)%R \is a @Num.int R. +Proof. by rewrite intrEge0. Qed. + +Import numFieldNormedType. + +(* connect MathComp's polynomials with analysis *) +Section derive_horner. +Variable (R : realFieldType). +Local Open Scope ring_scope. + +Lemma horner0_ext : horner (0 : {poly R}) = 0. +Proof. by apply/funext => y /=; rewrite horner0. Qed. + +Lemma hornerD_ext (p : {poly R}) r : + horner (p * 'X + r%:P) = horner (p * 'X) + horner (r%:P). +Proof. by apply/funext => y /=; rewrite !(hornerE,fctE). Qed. -(** *** Prove that: -- f's small coefficients are zero -*) -(* Let's begin the Niven proof *) -Lemma f_small_coef0 i: (i < n)%N -> f`_i = 0. +Lemma horner_scale_ext (p : {poly R}) : + horner (p * 'X) = (fun x => p.[x] * x)%R. +Proof. by apply/funext => y; rewrite !hornerE. Qed. + +Lemma hornerC_ext (r : R) : horner r%:P = cst r. +Proof. by apply/funext => y /=; rewrite !hornerE. Qed. + +Lemma derivable_horner (p : {poly R}) x : derivable (horner p) x 1. Proof. -(*D*)move=> iltn;rewrite /f coefZ. -(*D*)apply/eqP; rewrite mulf_eq0 invr_eq0 pnatr_eq0 eqn0Ngt (fact_gt0 n) /=. -(*D*)by rewrite coefXnM iltn. +elim/poly_ind: p => [|p r ih]; first by rewrite horner0_ext. +rewrite hornerD_ext; apply: derivableD. +- rewrite horner_scale_ext/=. + by apply: derivableM; [exact:ih|exact:derivable_id]. +- by rewrite hornerC_ext; exact: derivable_cst. Qed. -(** *** Prove that: -- f/n! as integral coefficients -*) +Lemma derivE (p : {poly R}) : horner (deriv p) = derive1 (horner p). +Proof. +apply/funext => x; elim/poly_ind: p => [|p r ih]. + by rewrite deriv0 hornerC horner0_ext derive1_cst. +rewrite derivD hornerD hornerD_ext. +rewrite derive1E deriveD//; [|exact: derivable_horner..]. +rewrite -!derive1E hornerC_ext derive1_cst addr0. +rewrite horner_scale_ext derive1E deriveM//; last exact: derivable_horner. +rewrite derive_id -derive1E -ih derivC horner0 addr0 derivM hornerD !hornerE. +rewrite derivX hornerE mulr1 addrC mulrC; congr +%R. +by rewrite /GRing.scale/= mulr1. +Qed. -Lemma f_int i: (n`!)%:R * f`_i \is a Qint. -Proof. -(*D*)rewrite /f coefZ mulrA mulfV; last by rewrite pnatr_eq0 -lt0n (fact_gt0 n). -(*D*)rewrite mul1r; apply/polyOverP. -(*D*)rewrite rpredM ?rpredX ?polyOverX //. -(*D*)by rewrite rpredB ?polyOverC ?polyOverZ ?polyOverX // int_Qint. +Global Instance is_derive_poly (p : {poly R}) (x : R) : + is_derive x (1:R) (horner p) p^`().[x]. +Proof. +by apply: DeriveDef; [exact: derivable_horner|rewrite derivE derive1E]. Qed. -(** *** Prove that: -the f^`(i) (x) have integral values for x = 0 -*) -Lemma derive_f_0_int: forall i, f^`(i).[0] \is a Qint. +End derive_horner. + +Local Open Scope classical_set_scope. + +Lemma cvg_poly {R : realType} (p : {poly R}) (a : R^o) : + (p.[x] @[x --> nbhs a] --> p.[a])%R. Proof. -(*D*)move=> i. -(*D*)rewrite horner_coef0 coef_derivn addn0 binomial.ffactnn. -(*D*)case:(boolP (i . -(*D*) by rewrite mul0rn // int_Qint. -(*D*)rewrite -leqNgt. -(*D*)move/binomial.bin_fact <-. -(*D*)rewrite /f coefZ -mulrnAl -mulr_natr mulrC rpredM //; last first. -(*D*) rewrite mulnC !natrM !mulrA mulVf ?mul1r ?rpredM ?nat_Qint //. -(*D*) by rewrite pnatr_eq0 eqn0Ngt (fact_gt0 n). -(*D*)apply/polyOverP;rewrite rpredM // ?rpredX ?polyOverX //. -(*D*)by rewrite ?rpredB ?polyOverC ?polyOverZ ?polyOverX // int_Qint. +apply/differentiable_continuous. +exact/derivable1_diffP/derivable_horner. Qed. -(** *** Deduce that: -F (0) has an integral value -*) +Lemma cvg_right_poly {R : realType} (p : {poly R}) a : + (p.[x] @[x --> a^'+] --> p.[a])%R. +Proof. +apply/cvg_at_right_filter/differentiable_continuous. +exact/derivable1_diffP/derivable_horner. +Qed. -Lemma F0_int : F.[0] \is a Qint. +Lemma cvg_left_poly {R : realType} (p : {poly R}) a : + (p.[x] @[x --> a^'-] --> p.[a])%R. Proof. -(*D*)rewrite /F horner_sum rpred_sum // => i _ ; rewrite !hornerE rpredM //. -(*D*) by rewrite -exprnP rpredX. -(*D*)by rewrite derive_f_0_int. +apply/cvg_at_left_filter/differentiable_continuous. +exact/derivable1_diffP/derivable_horner. Qed. -(** *** Then prove -- the symmetry argument f(x) = f(pi -x). -*) -Lemma pf_sym: f \Po (pi%:P -'X) = f. +Local Close Scope classical_set_scope. + +Lemma measurable_poly {R : realType} (p : {poly R}) (A : set R) : + measurable_fun A (horner p). Proof. -(*D*)rewrite /f comp_polyZ;congr (_ *:_). -(*D*)rewrite comp_polyM !comp_poly_exprn. -(*D*)rewrite comp_polyB comp_polyC !comp_polyZ !comp_polyX scalerBr /pi. -(*D*)have h1: b%:P * (a / b)%:P = a%:P. -(*D*) by rewrite polyCM mulrC -mulrA -polyCM mulVf ?bne0 // mulr1. -(*D*)suff->: (a%:P - (b *: (a / b)%:P - b *: 'X)) = b%:P * 'X. -(*D*) rewrite exprMn mulrA - exprMn [X in _ = X]mulrC. -(*D*) congr (_ *_); congr (_^+_). -(*D*) rewrite mulrC mulrBr; congr (_ -_)=>//. -(*D*) by rewrite mul_polyC. -(*D*)by rewrite -!mul_polyC h1 opprB addrA addrC addrA addNr add0r. +elim/poly_ind: p => [|p r ih]. + by rewrite horner0_ext; exact: measurable_cst. +rewrite hornerD_ext; apply: measurable_funD => //. + by rewrite horner_scale_ext; exact: measurable_funM. +by rewrite hornerC_ext; exact: measurable_cst. Qed. -(** *** Prove -- the symmetry for the derivative -*) +Section Algebraic_part. +Local Open Scope ring_scope. +Context {R : realType}. +Variables na nb n : nat. +Hypothesis nb0 : nb != 0%N. + +Definition a : R := (Posz na)%:~R. + +Definition b : R := (Posz nb)%:~R. -Lemma derivn_fpix i : - (f^`(i)\Po(pi%:P -'X))= (-1)^+i *: f^`(i). +Definition f : {poly R} := n`!%:R^-1 *: ('X^n * (a%:P - b*:'X)^+n). + +Definition F : {poly R} := \sum_(i < n.+1) (-1)^i *: f^`(i.*2). + +Let b0 : b != 0. +Proof. by rewrite intr_eq0. Qed. + +Let P1_size : size (a%:P - b *: 'X) = 2. +Proof. +have hs : size (- (b *: 'X)) = 2%N. + by rewrite size_opp (* TODO: size_opp -> sizeN *) size_scale ?b0// size_polyX. +by rewrite addrC size_addl hs ?size_polyC//; case: (a != 0). +Qed. + +Let P1_lead_coef : lead_coef (a%:P - b *: 'X) = - b. +Proof. +rewrite addrC lead_coefDl. + by rewrite lead_coefN lead_coefZ lead_coefX mulr1. +by rewrite size_opp size_scale ?b0// size_polyX size_polyC; case: (a != 0). +Qed. + +Let P_size : size ((a%:P - b*:'X) ^+ n) = n.+1. +Proof. +elim : n => [|n0 Hn0]; first by rewrite expr0 size_polyC oner_neq0. +rewrite exprS size_proper_mul; first by rewrite P1_size /= Hn0. +by rewrite lead_coef_exp P1_lead_coef -exprS expf_neq0 // oppr_eq0 b0. +Qed. + +Let comp_poly_exprn (p q : {poly R}) i : p ^+ i \Po q = (p \Po q) ^+ i. +Proof. +elim: i => [|i ih]; first by rewrite !expr0 comp_polyC. +by rewrite !exprS comp_polyM ih. +Qed. + +(* Let's begin Niven's proof... *) +Let f_int i : n`!%:R * f`_i \is a Num.int. Proof. -(*D*)elim:i ; first by rewrite /= expr0 scale1r pf_sym. -(*D*)move => i Hi. -(*D*)set fx := _ \Po _. -(*D*)rewrite derivnS exprS -scalerA -derivZ -Hi deriv_comp !derivE. -(*D*)by rewrite mulrBr mulr0 add0r mulr1 -derivnS /fx scaleN1r opprK. +rewrite /f coefZ mulrA divff ?mul1r ?pnatr_eq0 ?gtn_eqF ?fact_gt0//. +apply/polyOverP => /=; rewrite rpredM ?rpredX ?polyOverX//=. +by rewrite rpredB ?polyOverC ?polyOverZ ?polyOverX//= ?int_int. Qed. -(** *** Deduce that -- F(pi) is an integer -*) -Lemma FPi_int : F.[pi] \is a Qint. +Let f_small_coef0 i : (i < n)%N -> f`_i = 0. Proof. -(*D*)rewrite /F horner_sum rpred_sum //. -(*D*)move=> i _ ; rewrite !hornerE rpredM //. -(*D*) by rewrite -exprnP rpredX. -(*D*)move:(derivn_fpix (2*i)). -(*D*)rewrite mulnC exprM sqrr_sign scale1r => <-. -(*D*)by rewrite horner_comp !hornerE subrr derive_f_0_int. +move=> ni; rewrite /f coefZ; apply/eqP. +rewrite mulf_eq0 invr_eq0 pnatr_eq0 gtn_eqF ?fact_gt0//=. +by rewrite coefXnM ni. Qed. +Let derive_f_0_int i : f^`(i).[0] \is a Num.int. +Proof. +rewrite horner_coef0 coef_derivn addn0 ffactnn. +have [/f_small_coef0 ->|/bin_fact <-] := ltnP i n. + by rewrite mul0rn // int_Qint. +by rewrite mulnCA -mulr_natl natrM mulrAC rpredM ?f_int ?nat_int. +Qed. + +Lemma F0_int : F.[0] \is a Num.int. +Proof. +rewrite /F horner_sum rpred_sum //= => i _. +by rewrite !hornerE rpredM//= -exprnP rpredX// rpredN int_num1. +Qed. + +Definition pirat := a / b. + +Let pf_sym : f \Po (pirat%:P -'X) = f. +Proof. +rewrite /f comp_polyZ; congr *:%R. +rewrite comp_polyM !comp_poly_exprn comp_polyB comp_polyC !comp_polyZ. +rewrite !comp_polyX scalerBr. +have bap : b%:P * pirat%:P = a%:P. + by rewrite polyCM mulrC -mulrA -polyCM mulVf ?b0 // mulr1. +suff -> : a%:P - (b *: pirat%:P - b *: 'X) = b%:P * 'X. + rewrite exprMn mulrA mulrC; congr *%R. + rewrite -exprMn; congr (_ ^+ _). + rewrite mulrBl /pirat mul_polyC -bap (mulrC b%:P); congr (_ - _)%R. + by rewrite mul_polyC. + by rewrite mulrC mul_polyC. +by rewrite -mul_polyC bap opprB addrCA subrr addr0 mul_polyC. +Qed. + +Let derivn_fpix i : f^`(i) \Po (pirat%:P -'X) = (-1) ^+ i *: f^`(i). +Proof. +elim:i ; first by rewrite /= expr0 scale1r pf_sym. +move=> i Hi. +rewrite [in RHS]derivnS exprS mulN1r scaleNr -(derivZ ((-1) ^+ i)) -Hi. +by rewrite deriv_comp derivB derivX -derivnS derivC sub0r mulrN1 opprK. +Qed. -(** *** if you have time -- you can prove the equality F^`(2) + F = f -- that is needed by the analytic part of the Niven proof -*) +Lemma FPi_int : F.[pirat] \is a Num.int. +Proof. +rewrite /F horner_sum rpred_sum // => i _ ; rewrite !hornerE rpredM //=. + by rewrite -exprnP rpredX// (_ : -1 = (-1)%:~R)// intr_int. +move: (derivn_fpix i.*2). +rewrite -mul2n mulnC exprM sqrr_sign scale1r => <-. +by rewrite horner_comp !hornerE subrr derive_f_0_int. +Qed. +(* this is needed by the analytic part of the Niven proof *) Lemma D2FDF : F^`(2) + F = f. Proof. -(*D*)rewrite /F linear_sum /=. -(*D*)rewrite (eq_bigr (fun i:'I_n.+1 => (((-1)^i *: f^`(2 * i.+1)%N)))); last first. -(*D*) move=> i _ ;rewrite !derivZ; congr (_ *:_). -(*D*) rewrite -!derivnS;congr (_^`(_)). -(*D*) by rewrite mulnS addnC addn2. -(*D*)rewrite [X in _ + X]big_ord_recl muln0 derivn0. -(*D*)rewrite -exprnP expr0 scale1r (addrC f) addrA -[X in _ = X]add0r. -(*D*)congr (_ + _). -(*D*)rewrite big_ord_recr addrC addrA -big_split big1=>[| i _]. -(*D*) rewrite add0r /=; apply/eqP; rewrite scaler_eq0 -derivnS derivn_poly0. -(*D*) by rewrite eqxx orbT. -(*D*) suff ->: (size f) = (n + n.+1)%N by rewrite -plus_n_O leqnSn. -(*D*) rewrite /f size_scale; last first. -(*D*) by rewrite invr_neq0 // pnatr_eq0 -lt0n (fact_gt0 n). -(*D*) rewrite size_monicM ?monicXn //; last by rewrite -size_poly_eq0 P_size. -(*D*) by rewrite size_polyXn P_size. -(*D*)rewrite /bump /= -scalerDl. -(*D*)apply/eqP;rewrite scaler_eq0 /bump -exprnP add1n exprSr. -(*D*)by rewrite mulrN1 addrC subr_eq0 eqxx orTb. +rewrite /F linear_sum /=. +rewrite (eq_bigr (fun i : 'I_n.+1 => ((-1)^i *: f^`(i.+1.*2)%N))); last first. + by move=> i _ ;rewrite !derivZ. +rewrite [X in _ + X]big_ord_recl/=. +rewrite -exprnP expr0 scale1r (addrC f) addrA -[X in _ = X]add0r. +congr (_ + _). +rewrite big_ord_recr addrC addrA -big_split big1=>[| i _]. + rewrite add0r /=; apply/eqP; rewrite scaler_eq0 -derivnS derivn_poly0. + by rewrite deriv0 eqxx orbT. + suff -> : size f = (n + n.+1)%N by rewrite addnS addnn. + rewrite /f size_scale; last first. + by rewrite invr_neq0 // pnatr_eq0 -lt0n (fact_gt0 n). + rewrite size_monicM ?monicXn //; last by rewrite -size_poly_eq0 P_size. + by rewrite size_polyXn P_size. +rewrite /bump /= -scalerDl. +apply/eqP; rewrite scaler_eq0 /bump -exprnP add1n exprSr. +by rewrite mulrN1 addrC subr_eq0 eqxx orTb. Qed. End Algebraic_part. +Local Open Scope classical_set_scope. +Lemma exp_fact (R : realType) (r : R) : + (r ^+ n / n`!%:R @[n --> \oo] --> 0)%R. +Proof. +apply/cvg_series_cvg_0. +exact: is_cvg_series_exp_coeff. +Qed. + +Local Open Scope ring_scope. +(* NB: not used... *) +Lemma exp_fact_alternative (R : realType) (r : R) : + (r ^+ n / n`!%:R @[n --> \oo] --> 0)%R. +Proof. +apply: norm_cvg0. +apply/cvgrPdist_le => /= e e0; near=> k; rewrite sub0r normrN normr_id. +pose N := `|Num.ceil r|.+1%N. +rewrite normrM normfV (@ger0_norm _ k`!%:R)// normrX. +rewrite -{1}[k]/(k.+1.-1) -subn1 -prodr_const_nat fact_prod natr_prod. +rewrite [in X in X / _]/index_iota subn1/=; +rewrite -[in X in X / _](@subnKC N k); last by near: k; exists N. +rewrite iotaD big_cat/= -[_ :: _]/(index_iota 1 N.+1). +rewrite -[in X in _ / X](@subnKC N k)/=; last by near: k; exists N. +rewrite [in X in _ / X]/index_iota subn1. +rewrite iotaD big_cat/= -[_ :: _]/(index_iota 1 N.+1). +rewrite -mulf_div -prodfV -big_split/= -prodfV -big_split /=. +apply: (@le_trans _ _ (\prod_(1 <= i < N.+1) (`|r| / i%:R) * (`|r| / k%:R))). + rewrite ler_wpM2l//; first exact/prodr_ge0. + rewrite (_ : iota _ _ = iota (1 + N) (k - N).-1 ++ [:: k]); last first. + rewrite (_ : [:: k] = iota k 1)//. + rewrite [X in iota X 1](_ : _ = (1 + N) + (k - N).-1)%N; last first. + by rewrite add1n -subnS subnKC//; near: k; exists N.+1. + by rewrite -iotaD addn1 prednK// subn_gt0//; near: k; exists N.+1. + rewrite big_cat/= big_cons big_nil mulr1 ler_piMl//. + have /prodr_ile1 : forall z : R, + z \in [seq (`|r| / i%:R) | i <- iota (1 + N) (k - N).-1] -> + 0 <= z <= 1. + move=> _ /mapP[/= m] /[!mem_iota] /andP[Nk kN] ->; apply/andP; split => //. + rewrite ler_pdivrMr// ?mul1r//; last by rewrite ltr0n (leq_trans _ Nk). + rewrite (@le_trans _ _ N.+1%:R)//; last by rewrite ler_nat -addn1 addnC. + by rewrite /N (le_trans (abs_ceil_ge _))// ler_nat ltnS. + by rewrite big_map. +rewrite mulrA ler_pdivrMr//; last by rewrite ltr0n; near: k; exists 1%N. +by rewrite (mulrC e) -ler_pdivrMr//; near: k; exact: nbhs_infty_ger. +Unshelve. all: by end_near. Qed. + +Local Close Scope ring_scope. +Local Close Scope classical_set_scope. + +Section Analytic_part. +Local Open Scope ring_scope. +Context {R : realType}. +Let mu := @lebesgue_measure R. +Variable na nb : nat. +Hypothesis nb0 : nb != 0%N. + +Let pirat : R := pirat na nb. + +Let f := @f R na nb. + +(* NB: helper lemma, not elegant... *) +Let abx x : 0 < x < pirat -> 0 < a na - b nb * x. +Proof. +move=> /andP[x0]; rewrite subr_gt0. +rewrite /pirat /exercise6.pirat ltr_pdivlMr 1?mulrC//. +by rewrite /b ltr0n lt0n. +Qed. + +(* TODO: use the {in _, _} notation? *) +Let abx_ge0 x : 0 <= x <= pirat -> 0 <= a na - b nb * x. +Proof. +move=> /andP[x0 xpi]; rewrite subr_ge0. +rewrite -ler_pdivlMl//; last by rewrite /b ltr0n lt0n. +by rewrite mulrC. +Qed. + +Let fsin n := fun x : R => (f n).[x] * sin x. + +Let F := @F R na nb. + +Lemma fsin_antiderivative n : + derive1 (fun x => derive1 (horner (F n)) x * sin x - ((F n).[x]) * cos x) = + fsin n :> (R -> R). +Proof. +apply/funext => x/=. +rewrite derive1E/= deriveD//=; last first. + apply: derivableM; last exact: ex_derive. + by rewrite -derivE; exact: derivable_horner. +rewrite deriveM//; last by rewrite -derivE; exact: derivable_horner. +rewrite deriveN//= deriveM// !derive_val opprD -addrA addrC !addrA. +rewrite scalerN opprK -addrA [X in (_ + X = _)%R](_ : _ = 0%R); last first. + rewrite addrC derivE. + by apply/eqP; rewrite subr_eq0 [eqbLHS]mulrC. +rewrite addr0 -derive1E. +have := @D2FDF R na _ n nb0. +rewrite -/F derivSn /fsin -/f => <-. +rewrite -!derivE derivn1. +rewrite [X in (X + _ = _)%R](_ : _ = (F n)^`()^`().[x]%R * sin x)%R; last first. + by rewrite mulrC. +by rewrite -mulrDl hornerD. +Qed. + +Definition intfsin n := \int[mu]_(x in `[0, pi]) (fsin n x). + +Local Open Scope classical_set_scope. + +Let cfsin n (A : set R^o) : {within A, continuous (fsin n : R^o -> R^o)}. +Proof. +apply/continuous_subspaceT => /= x. +by apply: cvgM => /=; [exact: cvg_poly|exact: continuous_sin]. +Qed. + +Hypothesis piratE : pirat = pi. + +Lemma intfsinE n : intfsin n = (F n).[pi] + (F n).[0]. +Proof. +rewrite /intfsin /Rintegral. +set h := fun x => (derive1 (fun x => (F n).[x]) x * sin x - (F n).[x] * cos x). +rewrite (@continuous_FTC2 _ _ h). +- rewrite /h sin0 cospi cos0 sinpi !mulr0 !add0r mulr1 mulrN1 !opprK EFinN. + by rewrite oppeK -EFinD. +- by rewrite pi_gt0. +- exact: cfsin. +- split. + + move=> x x0pi. + by apply: derivableB => //; apply: derivableM => //; rewrite -derivE. + + apply: cvgB => //. + rewrite -!derivE. + apply: cvgM => //; first exact: cvg_right_poly. + by apply: (@cvg_at_right_filter R R^o); exact: continuous_sin. + apply: cvgM => //; first exact: cvg_right_poly. + by apply: (@cvg_at_right_filter R R^o); exact: continuous_cos. + + apply: cvgB => //. + apply: cvgM => //. + rewrite -derivE. + exact: cvg_left_poly. + by apply: (@cvg_at_left_filter R R^o); exact: continuous_sin. + apply: cvgM; first exact: cvg_left_poly. + by apply: (@cvg_at_left_filter R R^o); exact: continuous_cos. +- by move=> x x0pi; rewrite fsin_antiderivative. +Qed. + +Lemma intfsin_int n : intfsin n \is a Num.int. +Proof. by rewrite intfsinE rpredD ?F0_int -?piratE ?FPi_int. Qed. + +Let f0 x : (f 0).[x] = 1. +Proof. +by rewrite /f /exercise6.f fact0 !expr0 invr1 mulr1 !hornerE. +Qed. + +Lemma fsin_bounded n (x : R) : (0 < n)%N -> 0 < x < pi -> + 0 < fsin n x < (pi ^+ n * (a na) ^+ n) / n`!%:R. +Proof. +move=> n0 /andP[x0 xpi]. +have sinx0 : 0 < sin x by rewrite sin_gt0_pi// x0. +apply/andP; split. + rewrite mulr_gt0// /f !hornerE/= mulr_gt0//. + by rewrite mulr_gt0 ?invr_gt0 ?ltr0n ?fact_gt0// exprn_gt0. + by rewrite exprn_gt0// abx// x0 piratE. +rewrite /fsin !hornerE/= -2!mulrA mulrC ltr_pM2r ?invr_gt0 ?ltr0n ?fact_gt0//. +rewrite -!exprMn [in ltRHS]mulrC mulrA -exprMn. +have ? : 0 <= a na - b nb * x. + by rewrite abx_ge0 ?piratE// (ltW x0) ltW. +have H1 : x * (a na - b nb * x) < a na * pi. + rewrite [ltRHS]mulrC ltr_pM//; first exact/ltW. + by rewrite ltrBlDl //ltrDr mulr_gt0// lt0r /b pnatr_eq0 nb0/=. +have := sin_le1 x; rewrite le_eqVlt => /predU1P[x1|x1]. +- by rewrite x1 mulr1 ltrXn2r ?gtn_eqF// mulr_ge0//; exact/ltW. +- rewrite -[ltRHS]mulr1 ltr_pM//. + + by rewrite exprn_ge0// mulr_ge0//; exact/ltW. + + exact/ltW. + + by rewrite ltrXn2r ?gtn_eqF// mulr_ge0//; exact/ltW. +Qed. + +Lemma intsin : (\int[mu]_(x in `[0%R, pi]) (sin x)%:E = 2%:E)%E. +Proof. +rewrite (@continuous_FTC2 _ _ (- cos)) ?pi_gt0//. +- by rewrite /= !EFinN cos0 cospi !EFinN oppeK. +- exact/(@continuous_subspaceT R^o R^o)/continuous_sin. +- split. + + by move=> x x0pi; exact/derivableN/derivable_cos. + + by apply: cvgN; apply: cvg_at_right_filter; exact: continuous_cos. + + by apply: cvgN; apply: cvg_at_left_filter; exact: continuous_cos. + + by move=> x x0pi; rewrite derive1E deriveN// derive_val opprK. +Qed. + +Lemma integrable_fsin n : mu.-integrable `[0%R, pi] (EFin \o fsin n). +Proof. +apply: continuous_compact_integrable; first exact: segment_compact. +exact: cfsin. +Qed. + +Section fsin_small_ball. +Let m : R^o := pi / 2. +Let d : R := pi / 4. + +Lemma small_ballS : closed_ball m d `<=` `]0%R, pi[. +Proof. +move=> z; rewrite closed_ball_itv/=; last by rewrite divr_gt0// pi_gt0. +rewrite in_itv/= => /andP[mdz zmd]; rewrite in_itv/=; apply/andP; split. + rewrite (lt_le_trans _ mdz)// subr_gt0. + by rewrite ltr_pM2l// ?pi_gt0// ltf_pV2// ?posrE// ltr_nat. +rewrite (le_lt_trans zmd)// -mulrDr gtr_pMr// ?pi_gt0//. +by rewrite -ltrBrDl [X in _ < X - _](splitr 1) div1r addrK ltf_pV2 ?posrE// ltr_nat. +(* that would be immediate with lra... *) +Qed. + +Lemma min_fsin n : (0 < n)%N -> + exists2 r : R, 0 < r & forall x, x \in closed_ball m d -> r <= fsin n x. +Proof. +move=> n0; have mdmd : m - d <= m + d. + by rewrite lerBlDr -addrA lerDl -mulr2n mulrn_wge0// divr_ge0// pi_ge0. +have cf : {within `[m - d, m + d], continuous (fsin n : _ -> R^o)}. + exact: cfsin. +have [c cmd Hc] := @EVT_min R (fsin n) _ _ mdmd cf. +exists (fsin n c). + have /(_ _)/andP[]// := @fsin_bounded n c n0. + have := @small_ballS c; rewrite /=in_itv/=; apply. + by rewrite closed_ball_itv//= divr_gt0// pi_gt0. +move=> x /set_mem; rewrite closed_ball_itv//=; first exact: Hc. +by rewrite divr_gt0// pi_gt0. +Qed. + +End fsin_small_ball. + +Lemma intfsin_gt0 n : 0 < intfsin n. +Proof. +rewrite fine_gt0//; have [->|n0] := eqVneq n 0. + rewrite /fsin; under eq_integral do rewrite f0 mul1r. + by rewrite intsin ltry andbT. +have fsin_ge0 (x : R) : 0 <= x <= pi -> (0 <= (fsin n x)%:E)%E. + move=> /andP[x0 xpi]; rewrite lee_fin mulr_ge0//. + rewrite !hornerE mulr_ge0//=. + by rewrite mulr_ge0// exprn_ge0. + by rewrite exprn_ge0// abx_ge0// piratE x0. + by rewrite sin_ge0_pi// x0. +apply/andP; split. + rewrite -lt0n in n0. + have [r r0] := @min_fsin _ n0. + pose m : R^o := pi / 2; pose d : R := pi / 4 => rn. + apply: (@lt_le_trans _ _ (\int[mu]_(x in closed_ball m d) r%:E))%E. + rewrite integral_cst//=; last exact: measurable_closed_ball. + rewrite mule_gt0// lebesgue_measure_closed_ball//. + by rewrite lte_fin mulrn_wgt0// divr_gt0// pi_gt0. + by rewrite divr_ge0// pi_ge0. + apply: (@le_trans _ _ (\int[mu]_(x in (closed_ball m d)) (fsin n x)%:E))%E. + apply: ge0_le_integral => //=. + - exact: measurable_closed_ball. + - by move=> x _; rewrite lee_fin ltW. + - move=> x /small_ballS/= /[!in_itv]/= /andP[x0 xpi]. + by rewrite fsin_ge0// (ltW x0)/= ltW. + - case/integrableP : (integrable_fsin n) => + _. + apply: measurable_funS => // x ix. + exact: subset_itv_oo_cc (small_ballS ix). + - by move=> x /mem_set /rn; rewrite lee_fin. + apply: ge0_subset_integral => //=. + - exact: measurable_closed_ball. + - by case/integrableP : (integrable_fsin n). + - by move=> x ix; exact: subset_itv_oo_cc (small_ballS ix). +case/integrableP : (integrable_fsin n) => ? /=. +apply: le_lt_trans; apply: ge0_le_integral => //=. +- apply/EFin_measurable_fun => /=; apply/measurableT_comp => //. + exact/EFin_measurable_fun. +- by move=> x x0pi; rewrite lee_fin ler_norm. +Qed. + +Lemma intfsin_small (e : R) : 0 < e -> \forall n \near \oo, 0 < intfsin n < e. +Proof. +move=> e0; near=> n. +rewrite intfsin_gt0/=. +apply: (@le_lt_trans _ _ + (\int[mu]_(x in `[0, pi]) ((pi ^+ n * (a na) ^+ n) / n`!%:R))). + apply: le_Rintegral => //=. + - apply/continuous_compact_integrable; first exact: segment_compact. + exact: cfsin. + - apply/continuous_compact_integrable; first exact: segment_compact. + by apply/continuous_subspaceT => x; exact: cvg_cst. + - move=> x. + have ? : 0 <= pi ^+ n * a na ^+ n / n`!%:R :> R. + by rewrite mulr_ge0// mulr_ge0// exprn_ge0// pi_ge0. + rewrite in_itv/= => /andP[]. + rewrite le_eqVlt => /predU1P[<- _|x0]; first by rewrite /fsin sin0 !hornerE. + rewrite le_eqVlt => /predU1P[->|xpi]; first by rewrite /fsin sinpi mulr0. + have n0 : (0 < n)%N by near: n; exists 1%N. + have /(_ _)/andP[|//] := @fsin_bounded _ x n0. + + by rewrite x0. + + by move=> _ /ltW. +rewrite Rintegral_cst//= lebesgue_measure_itv/= lte_fin pi_gt0/=. +rewrite subr0 mulrAC -exprMn (mulrC _ pi) -mulrA. +near: n. +have : pi * (pi * a na) ^+ n / n`!%:R @[n --> \oo] --> (0:R^o). + rewrite -[X in _ --> X](mulr0 pi). + under eq_fun do rewrite -mulrA. + by apply: cvgMr; exact: exp_fact. +move/cvgrPdist_lt => /(_ e e0)[k _]H. +near=> n. +have {H} := H n. +rewrite sub0r normrN ger0_norm; last first. + by rewrite !mulr_ge0 ?pi_ge0// exprn_ge0// mulr_ge0// pi_ge0. +rewrite mulrA; apply. +by near: n; exists k. +Unshelve. all: by end_near. Qed. + +End Analytic_part. + +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. + +(* TODO: what's the predicate for rationality? could be more elegant *) +Lemma pi_is_irrationnal {R : realType} (a b : nat) : + b != 0 -> pi != a%:~R / b%:~R :> R. +Proof. +move=> b0; apply/negP => /eqP piratE. +have [N _] := intfsin_small b0 (esym piratE) (@ltr01 R). +near \oo => n. +have Nn : (N <= n)%N by near: n; exists N. +have := @intfsin_int R _ _ b0 (esym piratE) n. +rewrite intrEge0; last by rewrite ltW// intfsin_gt0. +move=> + /(_ n Nn). +move/natrP => [k] ->. +rewrite ltr0n ltrn1. +by case: k. +Unshelve. all: by end_near. Qed. From fe8a6a5c088427c4dc5cd034809268894da5e0b2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 18 Oct 2024 09:32:55 +0900 Subject: [PATCH 3/3] nitpicks --- theories/exercise6.v | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/theories/exercise6.v b/theories/exercise6.v index ddccead5d..68f7687e4 100644 --- a/theories/exercise6.v +++ b/theories/exercise6.v @@ -94,6 +94,8 @@ Proof. by rewrite intrEge0. Qed. Import numFieldNormedType. +Local Notation "f ^` ()" := (derive1 f) : classical_set_scope. + (* connect MathComp's polynomials with analysis *) Section derive_horner. Variable (R : realFieldType). @@ -122,7 +124,7 @@ rewrite hornerD_ext; apply: derivableD. - by rewrite hornerC_ext; exact: derivable_cst. Qed. -Lemma derivE (p : {poly R}) : horner (deriv p) = derive1 (horner p). +Lemma derivE (p : {poly R}) : horner (p^`()) = (horner p)^`()%classic. Proof. apply/funext => x; elim/poly_ind: p => [|p r ih]. by rewrite deriv0 hornerC horner0_ext derive1_cst. @@ -253,7 +255,7 @@ Qed. Definition pirat := a / b. -Let pf_sym : f \Po (pirat%:P -'X) = f. +Let pf_sym : f \Po (pirat%:P - 'X) = f. Proof. rewrite /f comp_polyZ; congr *:%R. rewrite comp_polyM !comp_poly_exprn comp_polyB comp_polyC !comp_polyZ. @@ -269,7 +271,7 @@ suff -> : a%:P - (b *: pirat%:P - b *: 'X) = b%:P * 'X. by rewrite -mul_polyC bap opprB addrCA subrr addr0 mul_polyC. Qed. -Let derivn_fpix i : f^`(i) \Po (pirat%:P -'X) = (-1) ^+ i *: f^`(i). +Let derivn_fpix i : f^`(i) \Po (pirat%:P - 'X) = (-1) ^+ i *: f^`(i). Proof. elim:i ; first by rewrite /= expr0 scale1r pf_sym. move=> i Hi. @@ -390,8 +392,8 @@ Let fsin n := fun x : R => (f n).[x] * sin x. Let F := @F R na nb. Lemma fsin_antiderivative n : - derive1 (fun x => derive1 (horner (F n)) x * sin x - ((F n).[x]) * cos x) = - fsin n :> (R -> R). + (fun x => (horner (F n))^`()%classic x * sin x - (F n).[x] * cos x)^`()%classic = + fsin n. Proof. apply/funext => x/=. rewrite derive1E/= deriveD//=; last first. @@ -421,8 +423,6 @@ apply/continuous_subspaceT => /= x. by apply: cvgM => /=; [exact: cvg_poly|exact: continuous_sin]. Qed. -Hypothesis piratE : pirat = pi. - Lemma intfsinE n : intfsin n = (F n).[pi] + (F n).[0]. Proof. rewrite /intfsin /Rintegral. @@ -451,6 +451,8 @@ rewrite (@continuous_FTC2 _ _ h). - by move=> x x0pi; rewrite fsin_antiderivative. Qed. +Hypothesis piratE : pirat = pi. + Lemma intfsin_int n : intfsin n \is a Num.int. Proof. by rewrite intfsinE rpredD ?F0_int -?piratE ?FPi_int. Qed. @@ -472,7 +474,7 @@ rewrite /fsin !hornerE/= -2!mulrA mulrC ltr_pM2r ?invr_gt0 ?ltr0n ?fact_gt0//. rewrite -!exprMn [in ltRHS]mulrC mulrA -exprMn. have ? : 0 <= a na - b nb * x. by rewrite abx_ge0 ?piratE// (ltW x0) ltW. -have H1 : x * (a na - b nb * x) < a na * pi. +have ? : x * (a na - b nb * x) < a na * pi. rewrite [ltRHS]mulrC ltr_pM//; first exact/ltW. by rewrite ltrBlDl //ltrDr mulr_gt0// lt0r /b pnatr_eq0 nb0/=. have := sin_le1 x; rewrite le_eqVlt => /predU1P[x1|x1]. @@ -619,7 +621,7 @@ Local Open Scope classical_set_scope. (* TODO: what's the predicate for rationality? could be more elegant *) Lemma pi_is_irrationnal {R : realType} (a b : nat) : - b != 0 -> pi != a%:~R / b%:~R :> R. + b != 0 -> pi != a%:R / b%:R :> R. Proof. move=> b0; apply/negP => /eqP piratE. have [N _] := intfsin_small b0 (esym piratE) (@ltr01 R).