Pi irrational

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

_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

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.

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

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.

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,22 +1037,22 @@ 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 : _ -> _).
 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.

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) => //.

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.