From 4e298f709a437af5e0384e67618318053ecf1f60 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 9 Oct 2024 08:56:01 +0900 Subject: [PATCH] complete Niven's proof --- CHANGELOG_UNRELEASED.md | 28 +++ _CoqProject | 1 + classical/mathcomp_extra.v | 15 ++ theories/Make | 1 + theories/all_analysis.v | 1 + theories/derive.v | 69 +++++- theories/exercise6.v | 231 ------------------- theories/lebesgue_integral.v | 52 ++++- theories/normedtype.v | 3 + theories/pi_irrational.v | 433 +++++++++++++++++++++++++++++++++++ 10 files changed, 588 insertions(+), 246 deletions(-) delete mode 100644 theories/exercise6.v create mode 100644 theories/pi_irrational.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 67bb43c3b..5ab0033e1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -6,6 +6,34 @@ ### Changed +- in `mathcomp_extra.v`: + + lemmas `prodr_ile1`, `nat_int` + +- in `normedtype.v`: + + lemma `scaler1` + +- in `derive.v`: + + lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`, + `derivable_horner`, `derivE`, `continuous_horner` + + instance `is_derive_poly` + +- in `lebesgue_integral.v`: + + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral` + +- new file `pi_irrational.v`: + + lemmas `measurable_poly` + + definition `rational` + + module `pi_irrational` + + lemma `pi_irrationnal` + +### Changed + +- in `lebesgue_integrale.v` + + change implicits of `measurable_funP` + +- in `derive.v`: + + put the notation ``` ^`() ``` and ``` ^`( _ ) ``` in scope `classical_set_scope` + ### Renamed ### Generalized diff --git a/_CoqProject b/_CoqProject index bf4dcb863..a8b38635c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -89,6 +89,7 @@ theories/probability.v theories/convex.v theories/charge.v theories/kernel.v +theories/pi_irrational.v theories/showcase/summability.v analysis_stdlib/Rstruct_topology.v analysis_stdlib/showcase/uniform_bigO.v diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index f7c05dd23..7f5eeb3af 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -501,6 +501,9 @@ End floor_ceil. #[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to `ceil_gt_int`")] Notation ceil_lt_int := ceil_gt_int (only parsing). +Lemma nat_int {R : archiNumDomainType} n : n%:R \is a @Num.int R. +Proof. by rewrite Num.Theory.intrEge0. Qed. + Section bijection_forall. Lemma bij_forall A B (f : A -> B) (P : B -> Prop) : @@ -573,3 +576,15 @@ by apply: contraNeq (disjF _ _ iK jK) _; rewrite -fsetI_eq0 eqFij fsetIid. Qed. End FsetPartitions. + +(* 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. diff --git a/theories/Make b/theories/Make index de272b231..35f6699fb 100644 --- a/theories/Make +++ b/theories/Make @@ -56,5 +56,6 @@ lebesgue_stieltjes_measure.v convex.v charge.v kernel.v +pi_irrational.v all_analysis.v showcase/summability.v diff --git a/theories/all_analysis.v b/theories/all_analysis.v index 99bdb7e9d..3eb98668d 100644 --- a/theories/all_analysis.v +++ b/theories/all_analysis.v @@ -23,3 +23,4 @@ From mathcomp Require Export lebesgue_stieltjes_measure. From mathcomp Require Export convex. From mathcomp Require Export charge. From mathcomp Require Export kernel. +From mathcomp Require Export pi_irrational. diff --git a/theories/derive.v b/theories/derive.v index c368957b0..f1c1fd31d 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -3,7 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import reals signed topology prodnormedzmodule tvs. -From mathcomp Require Import normedtype landau forms. +From mathcomp Require Import normedtype landau forms poly. (**md**************************************************************************) (* # Differentiation *) @@ -389,8 +389,8 @@ Proof. exact: iterSr. Qed. End DifferentialR2. -Notation "f ^` ()" := (derive1 f). -Notation "f ^` ( n )" := (derive1n n f). +Notation "f ^` ()" := (derive1 f) : classical_set_scope. +Notation "f ^` ( n )" := (derive1n n f) : classical_set_scope. Section DifferentialR3. Variable R : numFieldType. @@ -1037,8 +1037,8 @@ Qed. Lemma deriv1E f x : derivable f x 1 -> 'd f x = ( *:%R^~ (f^`() x)) :> (R -> U). Proof. -pose d (h : R) := h *: f^`() x. -move=> df; have lin_scal : linear d by move=> ???; rewrite /d scalerDl scalerA. +pose d (h : R) := h *: (f^`() x)%classic. +move=> df; have lin_scal : linear d by move=> ? ? ?; rewrite /d scalerDl scalerA. pose scallM := GRing.isLinear.Build _ _ _ _ _ lin_scal. pose scalL : {linear _ -> _} := HB.pack d scallM. rewrite -/d -[d]/(scalL : _ -> _). @@ -1046,13 +1046,13 @@ by apply: diff_unique; [apply: scalel_continuous|apply: der1]. Qed. Lemma diff1E f x : - differentiable f x -> 'd f x = (fun h => h *: f^`() x) :> (R -> U). + differentiable f x -> 'd f x = (fun h => h *: f^`()%classic x) :> (R -> U). Proof. pose d (h : R) := h *: 'd f x 1. move=> df; have lin_scal : linear d by move=> ? ? ?; rewrite /d scalerDl scalerA. pose scallM := GRing.isLinear.Build _ _ _ _ _ lin_scal. pose scalL : {linear _ -> _} := HB.pack d scallM. -have -> : (fun h => h *: f^`() x) = scalL by rewrite derive1E'. +have -> : (fun h => h *: f^`()%classic x) = scalL by rewrite derive1E'. apply: diff_unique; first exact: scalel_continuous. apply/eqaddoE; have /diff_locally -> := df; congr (_ + _ + _). by rewrite funeqE => h /=; rewrite -{1}[h]mulr1 linearZ. @@ -1635,7 +1635,7 @@ Qed. Lemma derive1_comp (R : realFieldType) (f g : R -> R) x : derivable f x 1 -> derivable g (f x) 1 -> - (g \o f)^`() x = g^`() (f x) * f^`() x. + (g \o f)^`() x = g^`()%classic (f x) * f^`()%classic x. Proof. move=> /derivable1_diffP df /derivable1_diffP dg. rewrite derive1E'; last exact/differentiable_comp. @@ -1647,3 +1647,56 @@ Qed. Lemma trigger_derive (R : realType) (f : R -> R) x x1 y1 : is_derive x (1 : R) f x1 -> x1 = y1 -> is_derive x 1 f y1. Proof. by move=> Hi <-. Qed. + +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. + +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. +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. + +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. +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. +by rewrite derivX hornerE mulr1 addrC mulrC scaler1. +Qed. + +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. + +Lemma continuous_horner (p : {poly R}) : continuous (horner p). +Proof. +move=> /= x; apply/differentiable_continuous. +exact/derivable1_diffP/derivable_horner. +Qed. + +End derive_horner. diff --git a/theories/exercise6.v b/theories/exercise6.v deleted file mode 100644 index 4831e122f..000000000 --- a/theories/exercise6.v +++ /dev/null @@ -1,231 +0,0 @@ -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. - diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 3ac62afdf..5c9855232 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3683,6 +3683,18 @@ move: foo; rewrite integralE/= -fin_num_abs fin_numB => /andP[fpoo fnoo]. by rewrite lte_add_pinfty// ltey_eq ?fpoo ?fnoo. Qed. +Lemma integral_fin_num_abs d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (D : set T) (f : T -> R) : + measurable D -> 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=> mD mf; rewrite fin_num_abs; case H : LHS; apply/esym. +- by move: H => /abse_integralP ->//; exact/measurable_EFinP. +- apply: contraFF H => /abse_integralP; apply => //. + exact/measurable_EFinP. +Qed. + Section integral_patch. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) @@ -4642,6 +4654,32 @@ Qed. Lemma Rintegral_set0 f : \int[mu]_(x in set0) f x = 0. Proof. by rewrite /Rintegral integral_set0. Qed. +Lemma Rintegral_cst D : d.-measurable D -> + forall r, \int[mu]_(x in D) (cst r) x = r * fine (mu D). +Proof. +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. + +Lemma le_Rintegral D f1 f2 : measurable D -> + mu.-integrable D (EFin \o f1) -> + mu.-integrable D (EFin \o f2) -> + (forall x, D x -> f1 x <= f2 x) -> + \int[mu]_(x in D) f1 x <= \int[mu]_(x in D) f2 x. +Proof. +move=> mD mf1 mf2 f12; rewrite /Rintegral fine_le//. +- rewrite -integral_fin_num_abs//; first by case/integrableP : mf1. + by apply/measurable_EFinP; case/integrableP : mf1. +- rewrite -integral_fin_num_abs//; first by case/integrableP : mf2. + by apply/measurable_EFinP; case/integrableP : mf2. +- by apply/le_integral => // x xD; rewrite lee_fin f12//; exact/set_mem. +Qed. + End Rintegral. Section ae_ge0_le_integral. @@ -5973,7 +6011,7 @@ Qed. Lemma lebesgue_differentiation_continuous (f : R -> rT^o) (A : set R) (x : R) : open A -> mu.-integrable A (EFin \o f) -> {for x, continuous f} -> A x -> - (fun r => 1 / (r *+ 2) * \int[mu]_(z in ball x r) f z) @ 0^'+ --> + (fun r => (r *+ 2)^-1 * \int[mu]_(z in ball x r) f z) @ 0^'+ --> (f x : R^o). Proof. have ball_itvr r : 0 < r -> `[x - r, x + r] `\` ball x r = [set x + r; x - r]. @@ -6004,10 +6042,10 @@ have -> : \int[mu]_(z in ball x r) f z = \int[mu]_(z in `[x - r, x + r]) f z. - by apply/measurableU; exact: measurable_set1. - exact: (integrableS mA). - by rewrite measureU0//; exact: lebesgue_measure_set1. -have r20 : 0 <= 1 / (r *+ 2) by rewrite ?divr_ge0 // mulrn_wge0. -have -> : f x = 1 / (r *+ 2) * \int[mu]_(z in `[x - r, x + r]) cst (f x) z. - rewrite /Rintegral /= integral_cst /= ?ritv // mulrC mul1r. - by rewrite -mulrA divff ?mulr1//; apply: lt0r_neq0; rewrite mulrn_wgt0. +have r20 : 0 <= (r *+ 2)^-1 by rewrite invr_ge0 mulrn_wge0. +have -> : f x = (r *+ 2)^-1 * \int[mu]_(z in `[x - r, x + r]) cst (f x) z. + rewrite Rintegral_cst// ritv//= mulrA mulrAC mulVf ?mul1r//. + by apply: lt0r_neq0; rewrite mulrn_wgt0. have intRf : mu.-integrable `[x - r, x + r] (EFin \o f). exact: (@integrableS _ _ _ mu _ _ _ _ _ xrA intf). rewrite /= -mulrBr -fineB; first last. @@ -6021,7 +6059,7 @@ have int_fx : mu.-integrable `[x - r, x + r] (fun z => (f z - f x)%:E). under [fun z => (f z - _)%:E]eq_fun => ? do rewrite EFinB. rewrite integrableB// continuous_compact_integrable// => ?. exact: cvg_cst. -rewrite normrM [ `|_/_| ]ger0_norm // -fine_abse //; first last. +rewrite normrM ger0_norm // -fine_abse //; first last. by rewrite integral_fune_fin_num. suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <= (r *+ 2 * eps)%:E)%E. @@ -6031,7 +6069,7 @@ suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <= - by rewrite abse_fin_num integral_fune_fin_num. - by rewrite integral_fune_fin_num// integrable_abse. - by case/integrableP : int_fx. - rewrite div1r ler_pdivrMl ?mulrn_wgt0 // -[_ * _]/(fine (_%:E)). + rewrite ler_pdivrMl ?mulrn_wgt0 // -[_ * _]/(fine (_%:E)). by rewrite fine_le// integral_fune_fin_num// integrable_abse. apply: le_trans. - apply: (@integral_le_bound _ _ _ _ _ (fun z => (f z - f x)%:E) eps%:E) => //. diff --git a/theories/normedtype.v b/theories/normedtype.v index c8ffba17b..b87600267 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -986,6 +986,9 @@ Module Exports. Export numFieldTopology.Exports. HB.reexport. End Exports. End numFieldNormedType. Import numFieldNormedType.Exports. +Lemma scaler1 {R : numFieldType} h : h%:A = h :> R. +Proof. by rewrite /GRing.scale/= mulr1. Qed. + Lemma limf_esup_dnbhsN {R : realType} (f : R -> \bar R) (a : R) : limf_esup f a^' = limf_esup (fun x => f (- x)%R) (- a)%R^'. Proof. diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v new file mode 100644 index 000000000..d070d0b31 --- /dev/null +++ b/theories/pi_irrational.v @@ -0,0 +1,433 @@ +From mathcomp Require Import all_ssreflect all_algebra archimedean finmap. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop signed reals ereal topology. +From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun lebesgue_integral. +From mathcomp Require Import derive charge ftc trigo. + +(**md**************************************************************************) +(* # Formalisation of A simple proof that pi is irrational by Ivan Niven *) +(* *) +(* Reference: *) +(* - http://projecteuclid.org/download/pdf_1/euclid.bams/1183510788 *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Theory. +Import numFieldNormedType.Exports. + +(* TODO: move *) +Lemma measurable_poly {R : realType} (p : {poly R}) (A : set R) : + measurable_fun A (horner p). +Proof. +apply/measurable_funTS; apply: continuous_measurable_fun. +exact/continuous_horner. +Qed. + +(* TODO: move somewhere to classical *) +Definition rational {R : realType} (x : R) := exists m n, x = (m%:R / n%:R)%R. + +Module pi_irrational. +Local Open Scope ring_scope. + +Lemma exp_fact (R : realType) (r : R) : + (r ^+ n / n`!%:R @[n --> \oo] --> 0)%classic. +Proof. +by apply/cvg_series_cvg_0; exact: is_cvg_series_exp_coeff. +Qed. + +Section algebraic_part. +Context {R : realType}. +Variables na nb n : nat. +Hypothesis nb0 : nb != 0%N. + +Definition a : R := na%:R. + +Definition b : R := nb%:R. + +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 pnatr_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 f_int i : n`!%:R * f`_i \is a Num.int. +Proof. +rewrite /f coefZ mulrA divff ?mul1r ?pnatr_eq0 ?gtn_eqF ?fact_gt0//. +apply/polyOverP => /=; rewrite rpredM ?rpredX ?polyOverX//=. +by rewrite rpredB ?polyOverC ?polyOverZ ?polyOverX//= nat_int. +Qed. + +Let f_small_coef0 i : (i < n)%N -> f`_i = 0. +Proof. +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. + +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. + +Lemma D2FDF : F^`(2) + F = f. +Proof. +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. + +Section analytic_part. +Context {R : realType}. +Let mu := @lebesgue_measure R. +Variable na nb : nat. +Hypothesis nb0 : nb != 0%N. + +Let pirat : R := pirat na nb. + +Let a : R := a na. + +Let b : R := b nb. + +Let f := @f R na nb. + +Let abx_gt0 x : 0 < x < pirat -> 0 < a - b * x. +Proof. +move=> /andP[x0]; rewrite subr_gt0. +rewrite /pirat /pirat ltr_pdivlMr 1?mulrC//. +by rewrite ltr0n lt0n. +Qed. + +Let abx_ge0 x : 0 <= x <= pirat -> 0 <= a - b * 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. + +Let fsin_antiderivative n : + (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. + 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) : {within A, continuous (fsin n)}. +Proof. +apply/continuous_subspaceT => /= x. +by apply: cvgM => /=; [exact: continuous_horner|exact: continuous_sin]. +Qed. + +Goal forall (p : {poly R}) c, p.[x] @[x --> c^'+] --> p.[c]. +by move=> p c; apply: cvg_at_right_filter; exact: continuous_horner. +Qed. + +Let 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=> [x x0pi| |]. + + by apply: derivableB => //; apply: derivableM => //; rewrite -derivE. + + apply: cvgB. + by rewrite -derivE; apply: cvgM => //; apply: cvg_at_right_filter; + [exact: continuous_horner|exact: continuous_sin]. + by apply: cvgM => //; apply: cvg_at_right_filter; + [exact: continuous_horner|exact: continuous_cos]. + + apply: cvgB => //. + by rewrite -derivE; apply: cvgM => //; apply: cvg_at_left_filter; + [exact: continuous_horner|exact: continuous_sin]. + by apply: cvgM => //; apply: cvg_at_left_filter; + [exact: continuous_horner|exact: continuous_cos]. +- 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. + +Let f0 x : (f 0).[x] = 1. +Proof. by rewrite /f /pi_irrational.f fact0 !expr0 invr1 mulr1 !hornerE. Qed. + +Let fsin_bounded n (x : R) : (0 < n)%N -> 0 < x < pi -> + 0 < fsin n x < (pi ^+ n * a ^+ 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_gt0// 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 - b * x by rewrite abx_ge0 ?piratE// (ltW x0) ltW. +have ? : x * (a - b * x) < a * 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. + +Let 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/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. + +Let integrable_fsin n : mu.-integrable `[0%R, pi] (EFin \o fsin n). +Proof. +apply: continuous_compact_integrable; first exact: segment_compact. +exact: cfsin. +Qed. + +Let small_ballS (m : R := pi / 2) (d := pi / 4) : + 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. + +Let min_fsin (m : R := pi / 2) (d := pi / 4) 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)}. + 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. + +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 := 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/measurable_EFinP => /=; apply/measurableT_comp => //. + exact/measurable_EFinP. +- 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 ^+ n) / n`!%:R))). + apply: le_Rintegral => //=. + - apply/continuous_compact_integrable; first exact: segment_compact. + by apply/continuous_subspaceT => x; exact: cvg_cst. + - move=> x. + have ? : 0 <= pi ^+ n * a ^+ 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) ^+ n / n`!%:R @[n --> \oo] --> (0:R). + 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. + +End pi_irrational. + +Lemma pi_irrationnal {R : realType} : ~ rational (pi : R). +Proof. +move=> [a [b]]; have [->|b0 piratE] := eqVneq b O. + by rewrite invr0 mulr0; apply/eqP; rewrite gt_eqF// pi_gt0. +have [N _] := pi_irrational.intfsin_small b0 (esym piratE) (@ltr01 R). +near \oo%classic => n. +have Nn : (N <= n)%N by near: n; exists N. +have := @pi_irrational.intfsin_int R _ _ b0 (esym piratE) n. +rewrite intrEge0; last by rewrite ltW// pi_irrational.intfsin_gt0. +move=> + /(_ n Nn). +move/natrP => [k] ->. +rewrite ltr0n ltrn1. +by case: k. +Unshelve. all: by end_near. Qed.