proof of L'Hopital rule

CHANGELOG.md

@@ -1,6 +1,121 @@
 # Changelog
 
-Latest releases: [[1.7.0] - 2024-11-22](#170---2024-11-22) and [[1.6.0] - 2024-10-25](#160---2024-10-25)
+Latest releases: [[1.8.0] - 2024-12-19](#180---2024-12-19), [[1.7.0] - 2024-11-22](#170---2024-11-22) and [[1.6.0] - 2024-10-25](#160---2024-10-25)
+
+## [1.8.0] - 2024-12-19
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + lemma `partition_disjoint_bigfcup`
+
+- in `constructive_ereal.v`:
+  + notations `\prod` in scope ereal_scope
+  + lemmas `prode_ge0`, `prode_fin_num`
+
+- in `num_topology.v`:
+  + lemma `in_continuous_mksetP`
+
+- in `normedtype.v`:
+  + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP`
+
+- in file `realfun.v`:
+  + lemma `cvg_nbhsP`
+
+- in `measure.v`:
+  + lemma `countable_bigcupT_measurable`
+  + definition `discrete_measurable`
+  + lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU`
+
+- in `lebesgue_measure.v`:
+  + lemma `measurable_indicP`
+  + lemma `measurable_powRr`
+
+- in `lebesgue_integral.v`:
+  + definition `dyadic_approx` (was `Let A`)
+  + definition `integer_approx` (was `Let B`)
+  + lemma `measurable_sum`
+  + lemma `integrable_indic`
+  + lemmas `integrable_pushforward`, `integral_pushforward`
+  + lemma `integral_measure_add`
+
+- in `probability.v`:
+  + lemma `expectation_def`
+  + notation `'M_`
+  + lemma `integral_distribution` (existing lemma `integral_distribution` has been renamed)
+
+### Changed
+
+- in `lebesgue_integrale.v`
+  + change implicits of `measurable_funP`
+
+### Renamed
+
+- in `classical_sets.v`:
+  + `preimage_itv_o_infty` -> `preimage_itvoy`
+  + `preimage_itv_c_infty` -> `preimage_itvcy`
+  + `preimage_itv_infty_o` -> `preimage_itvNyo`
+  + `preimage_itv_infty_c` -> `preimage_itvNyc`
+
+- in `constructive_ereal.v`:
+  + `maxeMr` -> `maxe_pMr`
+  + `maxeMl` -> `maxe_pMl`
+  + `mineMr` -> `mine_pMr`
+  + `mineMl` -> `mine_pMl`
+
+- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v`
+
+- in `lebesgue_measure.v`:
+  + `measurable_fun_indic` -> `measurable_indic`
+  + `emeasurable_fun_sum` -> `emeasurable_sum`
+  + `emeasurable_fun_fsum` -> `emeasurable_fsum`
+  + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
+
+- in `probability.v`:
+  + `expectationM` -> `expectationZl`
+  + `integral_distribution` -> `ge0_integral_distribution`
+
+### Generalized
+
+- in `sequences.v`:
+  + lemmas `cvg_restrict`, `cvg_centern`, `cvg_shiftn cvg_shiftS`
+
+- in `lebesgue_integral.v`:
+  + lemma `measurable_sfunP`
+
+- in `probability.v`:
+  + definition `random_variable`
+  + lemmas `notin_range_measure`, `probability_range`
+  + definition `distribution`
+  + lemma `probability_distribution`, `integral_distribution`
+  + mixin `MeasurableFun_isDiscrete`
+  + structure `discreteMeasurableFun`
+  + definition `discrete_random_variable`
+  + lemma `dRV_dom_enum`
+  + definitions `dRV_dom`, `dRV_enum`, `enum_prob`
+  + lemmas `distribution_dRV`, `sum_enum_prob`
+
+### Deprecated
+
+- in file `lebesgue_integral.v`:
+  + lemma `approximation`
+
+### Removed
+
+- in `constructive_ereal.v`
+  + notation `lee_opp` (deprecated since 0.6.5)
+  + notation `lte_opp` (deprecated since 0.6.5)
+
+- in `measure.v`:
+  + `dynkin_setI_bigsetI` (use `big_ind` instead)
+
+- in `lebesgue_measurable.v`:
+  + notation `measurable_fun_power_pos` (deprecated since 0.6.3)
+  + notation `measurable_power_pos` (deprecated since 0.6.4)
+
+- in `lebesgue_integral.v`:
+  + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
+  + notation `measurable_fun_indic` (deprecation since 0.6.3)
 
 ## [1.7.0] - 2024-11-22
 

CHANGELOG_UNRELEASED.md

@@ -4,107 +4,82 @@
 
 ### Added
 
-- in `num_topology.v`:
-  + lemma `in_continuous_mksetP`
+- in `mathcomp_extra.v`:
+  + lemmas `prodr_ile1`, `nat_int`
 
 - in `normedtype.v`:
-  + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP`
+  + lemma `scaler1`
 
-- in `mathcomp_extra.v`:
-  + lemma `partition_disjoint_bigfcup`
-- in `lebesgue_measure.v`:
-  + lemma `measurable_indicP`
+- 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`:
-  + definition `dyadic_approx` (was `Let A`)
-  + definition `integer_approx` (was `Let B`)
-  + lemma `measurable_sum`
-  + lemma `integrable_indic`
-
-- in `constructive_ereal.v`:
-  + notations `\prod` in scope ereal_scope
-  + lemmas `prode_ge0`, `prode_fin_num`
-- in `probability.v`:
-  + lemma `expectation_def`
-  + notation `'M_`
+  + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral`
 
-- in `lebesgue_integral.v`:
-  + lemmas `integrable_pushforward`, `integral_pushforward`
-  + lemma `integral_measure_add`
+- new file `pi_irrational.v`:
+  + lemmas `measurable_poly`
+  + definition `rational`
+  + module `pi_irrational`
+  + lemma `pi_irrationnal`
+
+- in `numfun.v`
+  + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp`
 
-- in `probability.v`
-  + lemma `integral_distribution` (existsing lemma `integral_distribution` has been renamed)
+- in `classical_sets.v`:
+  + lemmas `xsectionE`, `ysectionE`
 
-- in file `realfun.v`:
-  + lemma `cvg_nbhsP`
+- in `derive.v`:
+  + lemmas `differentiable_subr_neq0`, `cauchy_MVT`,
+    `lhopital_right`, `lhopital_left`
 
 ### Changed
 
 - in `lebesgue_integrale.v`
   + change implicits of `measurable_funP`
-
-### Renamed
 
-- in `lebesgue_measure.v`:
-  + `measurable_fun_indic` -> `measurable_indic`
-  + `emeasurable_fun_sum` -> `emeasurable_sum`
-  + `emeasurable_fun_fsum` -> `emeasurable_fsum`
-  + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
-- in `probability.v`:
-  + `expectationM` -> `expectationZl`
+- in `derive.v`:
+  + put the notation ``` ^`() ``` and ``` ^`( _ ) ``` in scope `classical_set_scope`
 
-- in `classical_sets.v`:
-  + `preimage_itv_o_infty` -> `preimage_itvoy`
-  + `preimage_itv_c_infty` -> `preimage_itvcy`
-  + `preimage_itv_infty_o` -> `preimage_itvNyo`
-  + `preimage_itv_infty_c` -> `preimage_itvNyc`
+- in `numfun.v`
+  + lock `funepos`, `funeneg`
 
-- in `constructive_ereal.v`:
-  + `maxeMr` -> `maxe_pMr`
-  + `maxeMl` -> `maxe_pMl`
-  + `mineMr` -> `mine_pMr`
-  + `mineMl` -> `mine_pMl`
+- moved from `lebesgue_integral.v` to `measure.v` and generalized
+  + lemmas `measurable_xsection`, `measurable_ysection`
 
-- in `probability.v`:
-  + `integral_distribution` -> `ge0_integral_distribution`
+### Renamed
 
-- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v`
+- in `measure.v`
+  + `preimage_class` -> `preimage_set_system`
+  + `image_class` -> `image_set_system`
+  + `preimage_classes` -> `g_sigma_preimageU`
+  + `preimage_class_measurable_fun` -> `preimage_set_system_measurable_fun`
+  + `sigma_algebra_preimage_class` -> `sigma_algebra_preimage`
+  + `sigma_algebra_image_class` -> `sigma_algebra_image`
+  + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE`
+  + `preimage_classes_comp` -> `g_sigma_preimageU_comp`
 
 ### Generalized
 
-- in `sequences.v`:
-  + lemmas `cvg_restrict`, `cvg_centern`, `cvg_shiftn cvg_shiftS`
-
-- in `probability.v`:
-  + definition `random_variable`
-  + lemmas `notin_range_measure`, `probability_range`
-  + definition `distribution`
-  + lemma `probability_distribution`, `integral_distribution`
-  + mixin `MeasurableFun_isDiscrete`
-  + structure `discreteMeasurableFun`
-  + definition `discrete_random_variable`
-  + lemma `dRV_dom_enum`
-  + definitions `dRV_dom`, `dRV_enum`, `enum_prob`
-  + lemmas `distribution_dRV`, `sum_enum_prob`
-
-- in `lebesgue_integral.v`:
-  + lemma `measurable_sfunP`
-
+- in `sequences.v`,
+  + generalized indexing from zero-based ones (`0 <= k < n` and `k <oo`)
+    to `m <= k < n` and `m <= k <oo`
+    * lemmas `nondecreasing_series`, `ereal_nondecreasing_series`,
+             `eseries_mkcondl`, `eseries_mkcondr`, `eq_eseriesl`,
+	     `nneseries_lim_ge`, `adde_def_nneseries`,
+	     `nneseriesD`, `nneseries_sum_nat`, `nneseries_sum`,
+  + lemmas `nneseries_ge0`, `is_cvg_nneseries_cond`, `is_cvg_npeseries_cond`,
+    `is_cvg_nneseries`, `is_cvg_npeseries`, `nneseries_ge0`, `npeseries_le0`,
+    `lee_nneseries`
+
 ### Deprecated
 
-- in file `lebesgue_integral.v`:
-  + lemma `approximation`
-
 ### Removed
 
-- in `lebesgue_integral.v`:
-  + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
-  + notation `measurable_fun_indic` (deprecation since 0.6.3)
-- in `constructive_ereal.v`
-  + notation `lee_opp` (deprecated since 0.6.5)
-  + notation `lte_opp` (deprecated since 0.6.5)
-- in `measure.v`:
-  + `dynkin_setI_bigsetI` (use `big_ind` instead)
+- in `sequences.v`:
+  + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`,
+    `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0)
 
 ### Infrastructure
 

INSTALL.md

@@ -48,7 +48,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.1.7.0
+$ opam install coq-mathcomp-analysis.1.8.0
 ```
 4. Everytime you want to work in this same context, you need to type
 ```

README.md

@@ -88,7 +88,7 @@ We try to preserve backward compatibility as best as we can.
 
 Each file is documented in its header in ASCII.
 
-[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_7_0/index.html) (using a fork of [`coq2html`](https://github.com/xavierleroy/coq2html)).
+[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_8_0/index.html) (using a fork of [`coq2html`](https://github.com/xavierleroy/coq2html)).
 It includes inheritance diagrams for the mathematical structures that MathComp-Analysis adds on top of MathComp's ones.
 
 Overview presentations:

_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/classical_sets.v

@@ -2602,6 +2602,7 @@ Proof.
 by apply: qcanon; elim/eqPchoice; elim/choicePpointed => [[T F]|T];
    [left; exists (Empty.Pack F) | right; exists T].
 Qed.
+
 Lemma Ppointed : quasi_canonical Type pointedType.
 Proof.
 by apply: qcanon; elim/Peq; elim/eqPpointed => [[T F]|T];
@@ -3262,11 +3263,17 @@ Proof. by apply/idP/idP => [|]; [rewrite inE|rewrite /ysection !inE /= inE]. Qed
 Lemma ysectionP x y A : ysection A y x <-> A (x, y).
 Proof. by rewrite /ysection/= inE. Qed.
 
+Lemma xsectionE A x : xsection A x = (fun y => (x, y)) @^-1` A.
+Proof. by apply/seteqP; split => [y|y] /xsectionP. Qed.
+
+Lemma ysectionE A y : ysection A y = (fun x => (x, y)) @^-1` A.
+Proof. by apply/seteqP; split => [x|x] /ysectionP. Qed.
+
 Lemma xsection0 x : xsection set0 x = set0.
-Proof. by rewrite predeqE /xsection => y; split => //=; rewrite inE. Qed.
+Proof. by rewrite xsectionE preimage_set0. Qed.
 
 Lemma ysection0 y : ysection set0 y = set0.
-Proof. by rewrite predeqE /ysection => x; split => //=; rewrite inE. Qed.
+Proof. by rewrite ysectionE preimage_set0. Qed.
 
 Lemma in_xsectionX X1 X2 x : x \in X1 -> xsection (X1 `*` X2) x = X2.
 Proof.

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.

reals_stdlib/Rstruct.v

@@ -25,7 +25,7 @@ liability. See the COPYING file for more details.
 (* # Compatibility with the real numbers of Coq                               *)
 (******************************************************************************)
 
-From Coq Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
+From Coq Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
 From Coq Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
 From Coq Require Import Rtrigo1 Reals.
 From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.

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.