math-comp / analysis Goto Github PK

View Code? Open in Web Editor NEW

190.0 19.0 41.0 9.79 MB

Mathematical Components compliant Analysis Library

License: Other

Coq 99.07% Makefile 0.16% Python 0.13% Shell 0.47% Nix 0.12% sed 0.02% Emacs Lisp 0.01%

coq mathcomp ssreflect analysis

analysis's Introduction

Analysis library compatible with Mathematical Components

$Docker CI$

This repository contains an experimental library for real analysis for the Coq proof-assistant and using the Mathematical Components library.

Building and installation instructions

The easiest way to install the latest released version of Analysis library compatible with Mathematical Components is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-analysis

To instead build and install manually, do:

git clone https://github.com/math-comp/analysis.git
cd analysis
make   # or make -j <number-of-cores-on-your-machine> 
make install

About the stability of this library

Changes are documented systematically in CHANGELOG.md and CHANGELOG_UNRELEASED.md.

We bump the minor part of the version number for breaking changes.

We use deprecation warnings to help transitioning to new versions.

We try to preserve backward compatibility as best as we can.

Documentation

Each file is documented in its header (documentation for the last version, using coq2html).

Overview presentation: Classical Analysis with Coq (2018)

See also "Related publication(s)" above.

Other work using MathComp-Analysis:

Mathematical structures

MathComp-Analysis adds mathematical structures on top of MathComp's ones. The following inheritance diagram displays the resulting hierarchy as of version 1.1.0 (excluding most MathComp structures). The structures introduced by MathComp-Analysis are highlighted. (See topology.v, normedtype.v, reals.v, measure.v.)

Hierarchies of functions

Functions	Functions with a finite image	Measures	Kernels

(see `functions.v`)	(see `cardinality.v`, `lebesgue_integral.v`)	(see `measure.v`, `charge.v`)	(see `kernel.v`)

Development information

Detailed requirements and installation procedure

Developping with nix

Contributing

Previous work reused at the time of the first releases

This library was inspired by the Coquelicot library by Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. topology.v and normedtype.v contained a reimplementation of file Hierarchy.v from the library Coquelicot.

The instantiation of the mathematical structures of the Mathematical Components library with the real numbers of the standard Coq library used a well-known file (Rstruct.v) from the CoqApprox library (with modifications from various authors).

Our proof of Zorn's Lemma in classical_sets.v (NB: new filename) is a reimplementation of the one by Daniel Schepler (https://github.com/coq-community/zorns-lemma); we also took inspiration from his work on topology (https://github.com/coq-community/topology) for parts of topology.v.

ORIGINAL_FILES.md gives more details about the files in the first releases.

Acknowledgments

Many thanks to various contributors

analysis's People

Contributors

Stargazers

Watchers

analysis's Issues

Backport Enrico's inline "!!" refining for the have tactic to mathcomp?

analysis/posnum.v

Line 20 in 1566e32

Notation "!! x" := (ltac:(refine x)) (at level 100, only parsing).

Have comap : A -> B -> set (set B) -> set (set A)

And define weak and sup filteredType, compare with weak and sup topology.
And define the prod as the sup of the two comaps of π₁ and π₂.
Credit @johoelzl for the idea.

Instantiate the hierarchy on row vectors

This work was done for Coquelicot's hierarchy in https://github.com/drouhling/LaSalle/blob/master/vect.v and should be adapted to the new hierarchy to remove the Admitted in

analysis/derive.v

Line 174 in e2d3d4c

Section jacobian_tentative.

Maybe move the instantiations to the corresponding sections in hierarchy.v?

Move things from coq-alternate-reals/src subdir to root dir

Which bigenough?

This is a minor issue but with "From mathcomp Require Import bigenough" Coq might
load the bigenough from real-closed if it is installed. Of course this is ok as long as both
are in sync and real-closed properly updated but what about "Require Import mathcomp.bigenough.bigenough"?

analysis/altreals/realseq.v

Line 7 in 3643e6e

From mathcomp Require Import all_ssreflect all_algebra bigenough.

Could we have a nix upgrade documentation somewhere? (@amahboubi)

a doc on

upgrading the local nix shell (shell.nix) on analysis?
or upgrading the package definitions (mathcomp/extra.nix) on nixpkgs?

Originally posted by @CohenCyril in #147 (comment)

Set up a continuous integration

Travis?
ci/circleci?
other?

Put littleo_linear0 in 0

analysis/derive.v

Line 320 in b6aa8eb

Lemma littleo_linear0 (V' W' : normedModType R) (f : {linear V' -> W'})

As it is, this theorem is seldom rewritable from left to right, I'd rather have this theorem with x = 0 and provide lemmas to bring any o_x to o_0 instead.

Reserve Notations first

Factor out format and levels in new notations using Reserved Notations

Solve slowdown in derive

TODO (alternatives):

Lock the definition of diffusing a module type :

analysis/derive.v

Lines 46 to 48 in 99d2078

 Definition diff (F : filter_on V) (_ : phantom (set (set V)) F) (f : V -> W) := 

 (get (fun (df : {linear V -> W}) => continuous df /\ forall x, 

 f x = f (lim F) + df (x - lim F) +o_(x \near F) (x - lim F))).

Use canonical structures instead of typeclasses for automatic derive

naming of flim_add

analysis/hierarchy.v

Line 1490 in aa351f3

Lemma flim_add : continuous (fun z : V * V => z.1 + z.2).

Is that a good name? With that name, I was rather expecting a lemma such as
Lemma lim_add (F : filter_on X) (f g : X -> Y) (a b : Y) :
f @ F --> a -> g @ F --> b -> (f + g) @ F --> a + b.
(no prod, following flim_const).

merge bigmaxr lemmas into master?

Is it possible to merge this section about bigop's and max into master?

analysis/normedtype.v

Lines 980 to 1223 in 19d922d

 Section Bigmaxr. 

 Variable (R : realDomainType). 

 Lemma bigmaxr_mkcond I r (P : pred I) (F : I -> R) x : 

 \big[maxr/x]_(i <- r | P i) F i = 

 \big[maxr/x]_(i <- r) (if P i then F i else x). 

 Proof. 

 rewrite unlock; elim: r x => //= i r ihr x. 

 case P; rewrite ihr // maxr_r //; elim: r {ihr} => //= j r ihr. 

 by rewrite ler_maxr ihr orbT. 

 Qed. 

 Lemma bigminr_maxr I r (P : pred I) (F : I -> R) x : 

 \big[minr/x]_(i <- r | P i) F i = - \big[maxr/- x]_(i <- r | P i) - F i. 

 Proof. 

 by elim/big_rec2: _ => [|i y _ _ ->]; rewrite ?oppr_max opprK. 

 Qed. 

 Lemma bigminr_mkcond I r (P : pred I) (F : I -> R) x : 

 \big[minr/x]_(i <- r | P i) F i = 

 \big[minr/x]_(i <- r) (if P i then F i else x). 

 Proof. 

 rewrite !bigminr_maxr bigmaxr_mkcond; congr (- _). 

 by apply: eq_bigr => i _; case P. 

 Qed. 

 Lemma bigmaxr_split I r (P : pred I) (F1 F2 : I -> R) x : 

 \big[maxr/x]_(i <- r | P i) (maxr (F1 i) (F2 i)) = 

 maxr (\big[maxr/x]_(i <- r | P i) F1 i) (\big[maxr/x]_(i <- r | P i) F2 i). 

 Proof. 

 by elim/big_rec3: _ => [|i y z _ _ ->]; rewrite ?maxrr // maxrCA -!maxrA maxrCA. 

 Qed. 

 Lemma bigminr_split I r (P : pred I) (F1 F2 : I -> R) x : 

 \big[minr/x]_(i <- r | P i) (minr (F1 i) (F2 i)) = 

 minr (\big[minr/x]_(i <- r | P i) F1 i) (\big[minr/x]_(i <- r | P i) F2 i). 

 Proof. 

 rewrite !bigminr_maxr -oppr_max -bigmaxr_split; congr (- _). 

 by apply: eq_bigr => i _; rewrite oppr_min. 

 Qed. 

 Lemma filter_andb I r (a P : pred I) : 

 [seq i <- r | P i && a i] = [seq i <- [seq j <- r | P j] | a i]. 

 Proof. by elim: r => //= i r ->; case P. Qed. 

 Lemma bigmaxr_idl I r (P : pred I) (F : I -> R) x : 

 \big[maxr/x]_(i <- r | P i) F i = maxr x (\big[maxr/x]_(i <- r | P i) F i). 

 Proof. 

 rewrite -big_filter; elim: [seq i <- r | P i] => [|i l ihl]. 

 by rewrite big_nil maxrr. 

 by rewrite big_cons maxrCA -ihl. 

 Qed. 

 Lemma bigminr_idl I r (P : pred I) (F : I -> R) x : 

 \big[minr/x]_(i <- r | P i) F i = minr x (\big[minr/x]_(i <- r | P i) F i). 

 Proof. by rewrite !bigminr_maxr {1}bigmaxr_idl oppr_max opprK. Qed. 

 Lemma bigmaxrID I r (a P : pred I) (F : I -> R) x : 

 \big[maxr/x]_(i <- r | P i) F i = 

 maxr (\big[maxr/x]_(i <- r | P i && a i) F i) 

 (\big[maxr/x]_(i <- r | P i && ~~ a i) F i). 

 Proof. 

 rewrite -!(big_filter _ (fun _ => _ && _)) !filter_andb !big_filter. 

 rewrite ![in RHS](bigmaxr_mkcond _ _ F) !big_filter -bigmaxr_split. 

 have eqmax : forall i, P i -> 

 maxr (if a i then F i else x) (if ~~ a i then F i else x) = maxr (F i) x. 

 by move=> i _; case: (a i) => //=; rewrite maxrC. 

 rewrite [RHS](eq_bigr _ eqmax) -!(big_filter _ P). 

 elim: [seq j <- r | P j] => [|j l ihl]; first by rewrite !big_nil. 

 by rewrite !big_cons -maxrA -bigmaxr_idl ihl. 

 Qed. 

 Lemma bigminrID I r (a P : pred I) (F : I -> R) x : 

 \big[minr/x]_(i <- r | P i) F i = 

 minr (\big[minr/x]_(i <- r | P i && a i) F i) 

 (\big[minr/x]_(i <- r | P i && ~~ a i) F i). 

 Proof. by rewrite !bigminr_maxr -oppr_max -bigmaxrID. Qed. 

 Lemma bigmaxr_seq1 I (i : I) (F : I -> R) x : 

 \big[maxr/x]_(j <- [:: i]) F j = maxr (F i) x. 

 Proof. by rewrite unlock /=. Qed. 

 Lemma bigminr_seq1 I (i : I) (F : I -> R) x : 

 \big[minr/x]_(j <- [:: i]) F j = minr (F i) x. 

 Proof. by rewrite unlock /=. Qed. 

 Lemma bigmaxr_pred1_eq (I : finType) (i : I) (F : I -> R) x : 

 \big[maxr/x]_(j | j == i) F j = maxr (F i) x. 

 Proof. by rewrite -big_filter filter_index_enum enum1 bigmaxr_seq1. Qed. 

 Lemma bigminr_pred1_eq (I : finType) (i : I) (F : I -> R) x : 

 \big[minr/x]_(j | j == i) F j = minr (F i) x. 

 Proof. by rewrite bigminr_maxr bigmaxr_pred1_eq oppr_max !opprK. Qed. 

 Lemma bigmaxr_pred1 (I : finType) i (P : pred I) (F : I -> R) x : 

 P =1 pred1 i -> \big[maxr/x]_(j | P j) F j = maxr (F i) x. 

 Proof. by move/(eq_bigl _ _)->; apply: bigmaxr_pred1_eq. Qed. 

 Lemma bigminr_pred1 (I : finType) i (P : pred I) (F : I -> R) x : 

 P =1 pred1 i -> \big[minr/x]_(j | P j) F j = minr (F i) x. 

 Proof. by move/(eq_bigl _ _)->; apply: bigminr_pred1_eq. Qed. 

 Lemma bigmaxrD1 (I : finType) j (P : pred I) (F : I -> R) x : 

 P j -> \big[maxr/x]_(i | P i) F i 

 = maxr (F j) (\big[maxr/x]_(i | P i && (i != j)) F i). 

 Proof. 

 move=> Pj; rewrite (bigmaxrID _ (pred1 j)) [in RHS]bigmaxr_idl maxrA. 

 by congr maxr; apply: bigmaxr_pred1 => i; rewrite /= andbC; case: eqP => //->. 

 Qed. 

 Lemma bigminrD1 (I : finType) j (P : pred I) (F : I -> R) x : 

 P j -> \big[minr/x]_(i | P i) F i 

 = minr (F j) (\big[minr/x]_(i | P i && (i != j)) F i). 

 Proof. 

 by move=> Pj; rewrite !bigminr_maxr (bigmaxrD1 _ _ Pj) oppr_max opprK. 

 Qed. 

 Lemma ler_bigmaxr_cond (I : finType) (P : pred I) (F : I -> R) x i0 : 

 P i0 -> F i0 <= \big[maxr/x]_(i | P i) F i. 

 Proof. by move=> Pi0; rewrite (bigmaxrD1 _ _ Pi0) ler_maxr lerr. Qed. 

 Lemma bigminr_ler_cond (I : finType) (P : pred I) (F : I -> R) x i0 : 

 P i0 -> \big[minr/x]_(i | P i) F i <= F i0. 

 Proof. by move=> Pi0; rewrite (bigminrD1 _ _ Pi0) ler_minl lerr. Qed. 

 Lemma ler_bigmaxr (I : finType) (F : I -> R) (i0 : I) x : 

 F i0 <= \big[maxr/x]_i F i. 

 Proof. exact: ler_bigmaxr_cond. Qed. 

 Lemma bigminr_ler (I : finType) (F : I -> R) (i0 : I) x : 

 \big[minr/x]_i F i <= F i0. 

 Proof. exact: bigminr_ler_cond. Qed. 

 Lemma bigmaxr_lerP (I : finType) (P : pred I) m (F : I -> R) x : 

 reflect (x <= m /\ forall i, P i -> F i <= m) 

 (\big[maxr/x]_(i | P i) F i <= m). 

 Proof. 

 apply: (iffP idP) => [|[lexm leFm]]; last first. 

 by elim/big_ind: _ => // ??; rewrite ler_maxl =>->. 

 rewrite bigmaxr_idl ler_maxl => /andP[-> leFm]; split=> // i Pi. 

 by apply: ler_trans leFm; apply: ler_bigmaxr_cond. 

 Qed. 

 Lemma bigminr_gerP (I : finType) (P : pred I) m (F : I -> R) x : 

 reflect (m <= x /\ forall i, P i -> m <= F i) 

 (m <= \big[minr/x]_(i | P i) F i). 

 Proof. 

 rewrite bigminr_maxr ler_oppr; apply: (iffP idP). 

 by move=> /bigmaxr_lerP [? lemF]; split=> [|??]; rewrite -ler_opp2 ?lemF. 

 by move=> [? lemF]; apply/bigmaxr_lerP; split=> [|??]; rewrite ler_opp2 ?lemF. 

 Qed. 

 Lemma bigmaxr_sup (I : finType) i0 (P : pred I) m (F : I -> R) x : 

 P i0 -> m <= F i0 -> m <= \big[maxr/x]_(i | P i) F i. 

 Proof. by move=> Pi0 ?; apply: ler_trans (ler_bigmaxr_cond _ _ Pi0). Qed. 

 Lemma bigminr_inf (I : finType) i0 (P : pred I) m (F : I -> R) x : 

 P i0 -> F i0 <= m -> \big[minr/x]_(i | P i) F i <= m. 

 Proof. by move=> Pi0 ?; apply: ler_trans (bigminr_ler_cond _ _ Pi0) _. Qed. 

 Lemma bigmaxr_ltrP (I : finType) (P : pred I) m (F : I -> R) x : 

 reflect (x < m /\ forall i, P i -> F i < m) 

 (\big[maxr/x]_(i | P i) F i < m). 

 Proof. 

 apply: (iffP idP) => [|[ltxm ltFm]]; last first. 

 by elim/big_ind: _ => // ??; rewrite ltr_maxl =>->. 

 rewrite bigmaxr_idl ltr_maxl => /andP[-> ltFm]; split=> // i Pi. 

 by apply: ler_lt_trans ltFm; apply: ler_bigmaxr_cond. 

 Qed. 

 Lemma bigminr_gtrP (I : finType) (P : pred I) m (F : I -> R) x : 

 reflect (m < x /\ forall i, P i -> m < F i) 

 (m < \big[minr/x]_(i | P i) F i). 

 Proof. 

 rewrite bigminr_maxr ltr_oppr; apply: (iffP idP). 

 by move=> /bigmaxr_ltrP [? ltmF]; split=> [|??]; rewrite -ltr_opp2 ?ltmF. 

 by move=> [? ltmF]; apply/bigmaxr_ltrP; split=> [|??]; rewrite ltr_opp2 ?ltmF. 

 Qed. 

 Lemma bigmaxr_gerP (I : finType) (P : pred I) m (F : I -> R) x : 

 reflect (m <= x \/ exists2 i, P i & m <= F i) 

 (m <= \big[maxr/x]_(i | P i) F i). 

 Proof. 

 apply: (iffP idP) => [|[lemx|[i Pi lemFi]]]; last 2 first. 

 - by rewrite bigmaxr_idl ler_maxr lemx. 

 - by rewrite (bigmaxrD1 _ _ Pi) ler_maxr lemFi. 

 rewrite lerNgt => /bigmaxr_ltrP /asboolPn. 

 rewrite asbool_and negb_and => /orP [/asboolPn/negP|/existsp_asboolPn [i]]. 

 by rewrite -lerNgt; left. 

 by move=> /asboolPn/imply_asboolPn [Pi /negP]; rewrite -lerNgt; right; exists i. 

 Qed. 

 Lemma bigminr_lerP (I : finType) (P : pred I) m (F : I -> R) x : 

 reflect (x <= m \/ exists2 i, P i & F i <= m) 

 (\big[minr/x]_(i | P i) F i <= m). 

 Proof. 

 rewrite bigminr_maxr ler_oppl; apply: (iffP idP). 

 by move=> /bigmaxr_gerP [?|[i ??]]; [left|right; exists i => //]; 

 rewrite -ler_opp2. 

 by move=> [?|[i ??]]; apply/bigmaxr_gerP; [left|right; exists i => //]; 

 rewrite ler_opp2. 

 Qed. 

 Lemma bigmaxr_gtrP (I : finType) (P : pred I) m (F : I -> R) x : 

 reflect (m < x \/ exists2 i, P i & m < F i) 

 (m < \big[maxr/x]_(i | P i) F i). 

 Proof. 

 apply: (iffP idP) => [|[ltmx|[i Pi ltmFi]]]; last 2 first. 

 - by rewrite bigmaxr_idl ltr_maxr ltmx. 

 - by rewrite (bigmaxrD1 _ _ Pi) ltr_maxr ltmFi. 

 rewrite ltrNge => /bigmaxr_lerP /asboolPn. 

 rewrite asbool_and negb_and => /orP [/asboolPn/negP|/existsp_asboolPn [i]]. 

 by rewrite -ltrNge; left. 

 by move=> /asboolPn/imply_asboolPn [Pi /negP]; rewrite -ltrNge; right; exists i. 

 Qed. 

 Lemma bigminr_ltrP (I : finType) (P : pred I) m (F : I -> R) x : 

 reflect (x < m \/ exists2 i, P i & F i < m) 

 (\big[minr/x]_(i | P i) F i < m). 

 Proof. 

 rewrite bigminr_maxr ltr_oppl; apply: (iffP idP). 

 by move=> /bigmaxr_gtrP [?|[i ??]]; [left|right; exists i => //]; 

 rewrite -ltr_opp2. 

 by move=> [?|[i ??]]; apply/bigmaxr_gtrP; [left|right; exists i => //]; 

 rewrite ltr_opp2. 

 Qed. 

 End Bigmaxr. 

 Arguments bigmaxr_mkcond {R I r}. 

 Arguments bigmaxrID {R I r}. 

 Arguments bigmaxr_pred1 {R I} i {P F}. 

 Arguments bigmaxrD1 {R I} j {P F}. 

 Arguments ler_bigmaxr_cond {R I P F}. 

 Arguments ler_bigmaxr {R I F}. 

 Arguments bigmaxr_sup {R I} i0 {P m F}. 

 Arguments bigminr_mkcond {R I r}. 

 Arguments bigminrID {R I r}. 

 Arguments bigminr_pred1 {R I} i {P F}. 

 Arguments bigminrD1 {R I} j {P F}. 

 Arguments bigminr_ler_cond {R I P F}. 

 Arguments bigminr_ler {R I F}. 

 Arguments bigminr_inf {R I} i0 {P m F}.

I ask because I have a use for it in another branch.

Have notations for deriving and derivability

Provide and document derivation notations such as:

f^`(n), f^`() and f^`N(n) (as in poly.v) for derivation onR (and when available, on C)
'D(A -> V) for the type of derviable functions from domain A to a normed module type V
'D^n(A -> V) for n times derivable (so that 'D^1 = 'D)
'C^n_(A -> V) (I believe 'C^0 = 'C in the literature, but I advocate for not providing a notation without explicit n)

Bonus question: should the last 3 be types or sets ?

Merge coq-alternate-reals in there

The library https://github.com/strub/coq-alternate-reals or its (slight) fork (https://github.com/CohenCyril/coq-alternate-reals) should be merged in there, and the external dependency should be removed.

Linear and littleo of id is zero.

analysis/derive.v

Line 337 in aaaad64

[o_ (0 : V) id of f] = cst 0.

I am afraid this is difficult to use too... Maybe f =o id -> f = cst 0 is better?

The make install target fails when using opam 2

I'm using opam 2, and the make install target fails, I suspect due to the sandboxing feature. I'm not sure how to solve this exactly, but the other mathcomp packages installed fine, so...

The log

 make -f Makefile.coq install
make[1]: Entering directory '/home/armael/.opam/current/.opam-switch/build/coq-mathcomp-analysis.dev'
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot change permissions of '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis/': No such file or directory
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
install: cannot create directory '/home/armael/.opam/current/lib/coq/user-contrib/mathcomp/analysis': Read-only file system
make[1]: *** [Makefile.coq:471: install] Error 1
make[1]: Leaving directory '/home/armael/.opam/current/.opam-switch/build/coq-mathcomp-analysis.dev'

Prepare opam package for 0.1.0 and push to the coq opam archive

Document derive

analysis/derive.v

Line 1 in abb66fa

Remove min and max in MVT

analysis/derive.v

Line 1361 in 931af1c

let l := minr a b in let r := maxr a b in

Show a relation between locally and locally'

Use it to extend this result

analysis/derive.v

Line 193 in 86bc251

Lemma derivable_locally (f : V -> W) a v :

to locally 0 (not just locally' 0)

Have a spec lemma for big0

I think there should be spec lemma for bigO to avoid these patterns:
have /bigOFP [_/posnumP[c1] kOg] := bigOP [bigO of k]

Remove this lemma about derivative and replace.

analysis/derive.v

Line 135 in e2d3d4c

derivative1 f a = lim ((fun x => ('d_a f x) / x) @ (0 : R^o)).

'd_a f x / x although valid is a non canonical way for getting the coefficient of a linear map (no need to take a limit by the way, it is supposed to be constant). The canonical way is to first take the Jacobian (using lin1_mx) and in dimension 1 (since R^o is), just take the only coefficient: jacobian f 0 0.

derivative1 f a = 'J_a f 0 0

Find a better name for this.

analysis/set.v

Line 309 in 3404704

Definition is_prop {A} (X : set A) := forall x y, X x -> X y -> x = y.

Fix 'the_* landau notation to improve readability

Make the notation f = g +o_e stable (e.g. by putting a definition)

analysis/landau.v

Line 199 in 1566e32

Notation "f = g '+o_' F h" :=
Remove the "'the" tag which makes things unreadable

analysis/landau.v

Line 135 in 1566e32

Definition the_tag : unit := tt.

...

Not sure why this lemma is exported

analysis/derive.v

Line 318 in aaaad64

Lemma littleo_linear_id (V W : normedModType R) (f : {linear V -> W}) :

Shouldn't it be a part of littleo_linear0?

opam package does not build with latest mathcomp-finmap

Trying to install the library using the opam package currently does not work, because of finmap it seems (it works if I pin finmap 1.0.0 instead of using finmap dev).

The log:

make -f Makefile.coq
make[1] : on entre dans le répertoire « /home/armael/.opam/current/.opam-switch/build/coq-mathcomp-analysis.dev »
COQDEP VFILES
COQC altreals/xfinmap.v
COQC boolp.v
COQC forms.v
COQC reals.v
COQC classical_sets.v
File "./altreals/xfinmap.v", line 83, characters 30-31:
Error:
In environment
R : Type
idx : R
op : Monoid.com_law 1
T : choiceType
s : seq T
P : ?T
F : ?T0
The term "s" has type "seq T" while it is expected to have type "unit".

make[2]: *** [Makefile.coq:657: altreals/xfinmap.vo] Error 1

Provide a shorter symbol?

analysis/topology.v

Line 33 in 3404704

(* Filtered.source Y Z == structure that records types X such *)

Refactor norm and absolute value

In order to perform a good refactoring, one should first amend ssrnum to decorrelate norm and order, which cascades to integrating github.com/math-comp/finmap/order.v into mathcomp...

Rework landau's documentation and naming convention

This is related to #101. [NB(rei): PR which has been merged]

[NB(rei): partially addressed by PR #216 ]

Since we force user to use the equational notations by removing the defintions, we should be very clear on how to use this library. In particular the documentation should:

~~detail how to state a lemma using the notations, e.g. should I use f =O_F g or f = [O_F g of h]?~~
list all the possibilities to prove such relations, with the important steps, e.g. apply: eqoE is not to be forgotten, filter reasoning is possible but thought of as a last resort…
clarify anything that can confuse the user about the notations, e.g.:
- what is the difference between f =o_F g and f = o_F g?
- ~~why does f =O_ (0 : U) g work but not f =O_(0 : U) g, while f =O_F g does work?~~
what are the naming conventions. I believe this library should be used as bigop: since it is hard and tedious to search lemmas using notations, we should have a clear naming convention so that it is easy to find a lemma by its name.

Rstruct should export R?

Replace Filter by pfilter_on

Try to substitute canonical structures for typeclasses everywhere, so that we only use CS instead of TC...
(And maybe put in filteredType the axiom that canonical sets of sets must actually be filters)

Add closed sets to topological mixin

This issue was opened at the end of a discussion (at least with @CohenCyril) where we felt the need for an inclusion of closed sets as a field of the topological mixin, instead of defining them from closures afterwards.

This was a long time ago, so I don't remember the arguments in favor of this.

Warnings.

What about adding this in the _CoqProject file ?

  -arg -w
  -arg -parsing

I'm a bit fed up with all these warnings.

conflicting notation

This notation conflicts with the syntax for intro patterns (as in => [[...][...]]).
(That is why it sits in the middle of the file despite being a Reserved.)

analysis/hierarchy.v

Line 1269 in 3be1810

Reserved Notation "`|[ x ]|" (at level 0, x at level 99, format "`|[ x ]|").

Factor cauchy_eqP through cauch_entouragesP

analysis/hierarchy.v

Line 1001 in 7fc7e74

Lemma cauchy_exP (T : uniformType) (F : set (set T)) : Filter F ->

Document equiv.

analysis/equiv.v

Line 1 in abb66fa

Also, merge with Landau ?

Cut hierarchy in two parts : topology and uniform

Cut here:

analysis/hierarchy.v

Line 1413 in e2d3d4c

Module Uniform.
Name what happens before topology.v
Name what happens after uniform.v? pseudometric.v? normedtype.v? (help wanted)
Put

analysis/hierarchy.v

Line 2092 in e2d3d4c

Section Closed.

(Closed, Compact, Tychonof and Covers) in topology.v

Reserved Notations should come first.

analysis/landau.v

Line 160 in 061ff77

Reserved Notation "{o_ F f }" (at level 0, F at level 0, format "{o_ F f }").

Reserved Notations should be after Require Imports and headers but before the first definition.

The notations near and locally are too unstable.

Redo filters in mem_pred style.
PR soon!

Shouldn't a normed module be of dimension at least 1?

Indeed, otherwise locally' is not proper.
Other issues? One way or another?

Merge Rbar and ereal

Merge this with with ereal when issue #1 is solved

analysis/Rbar.v

Line 42 in 1566e32

Inductive Rbar := | Finite of R | p_infty | m_infty.

Quotients without ChoiceType?

Is my understanding correct that @CohenCyril constructs quotients over ChoiceType to be able to work with Leibniz equality in a constructive context?

When using classical logic, this does not seem necessary, as the usual construction we considers elements of the quotient as equivalence classes. With classical logic these are maps A->2, by functional extensionality, these have the right equality.

Am I overlooking something?
This construction would avoid requiring ChoiceTypes in a number of places.

Add typeclasses for differentiation and derivation

As in https://github.com/drouhling/LaSalle/blob/e52704b3d373d4a65b3794aa33033c27df1a312b/coquelicotComplements.v#L336

Put Zorn in set.v

analysis/hierarchy.v

Line 2354 in e2d3d4c

Lemma Zorn T (R : T -> T -> Prop) :

and put pointed type in set.v as well

Move structures about functions out of landau.v

move

analysis/landau.v

Lines 285 to 331 in 8768257

 Section function_space. 

 Definition cst {T T' : Type} (x : T') : T -> T' := fun=> x. 

 Program Definition fct_zmodMixin (T : Type) (M : zmodType) := 

 @ZmodMixin (T -> M) \0 (fun f x => - f x) (fun f g => f \+ g) _ _ _ _. 

 Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite addrA. Qed. 

 Next Obligation. by move=> f g; rewrite funeqE=> x /=; rewrite addrC. Qed. 

 Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite add0r. Qed. 

 Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite addNr. Qed. 

 Canonical fct_zmodType T (M : zmodType) := ZmodType (T -> M) (fct_zmodMixin T M). 

 Program Definition fct_ringMixin (T : pointedType) (M : ringType) := 

 @RingMixin [zmodType of T -> M] (cst 1) (fun f g x => f x * g x) 

 _ _ _ _ _ _. 

 Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrA. Qed. 

 Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite mul1r. Qed. 

 Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite mulr1. Qed. 

 Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrDl. Qed. 

 Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrDr. Qed. 

 Next Obligation. 

 by apply/eqP; rewrite funeqE => /(_ point) /eqP; rewrite oner_eq0. 

 Qed. 

 Canonical fct_ringType (T : pointedType) (M : ringType) := 

 RingType (T -> M) (fct_ringMixin T M). 

 Program Canonical fct_comRingType (T : pointedType) (M : comRingType) := 

 ComRingType (T -> M) _. 

 Next Obligation. by move=> f g; rewrite funeqE => x; rewrite mulrC. Qed. 

 Program Definition fct_lmodMixin (U : Type) (R : ringType) (V : lmodType R) 

 := @LmodMixin R [zmodType of U -> V] (fun k f => k \*: f) _ _ _ _. 

 Next Obligation. rewrite funeqE => x; exact: scalerA. Qed. 

 Next Obligation. by move=> f; rewrite funeqE => x /=; rewrite scale1r. Qed. 

 Next Obligation. by move=> f g h; rewrite funeqE => x /=; rewrite scalerDr. Qed. 

 Next Obligation. by move=> f g; rewrite funeqE => x /=; rewrite scalerDl. Qed. 

 Canonical fct_lmodType U (R : ringType) (V : lmodType R) := 

 LmodType _ (U -> V) (fct_lmodMixin U V). 

 Lemma fct_sumE (T : Type) (M : zmodType) n (f : 'I_n -> T -> M) (x : T) : 

 (\sum_(i < n) f i) x = \sum_(i < n) f i x. 

 Proof. 

 elim: n f => [|n H] f; 

 by rewrite !(big_ord0,big_ord_recr) //= -[LHS]/(_ x + _ x) H. 

 Qed. 

 End function_space.

at the top of topology.v?

Looks subsumed by `littleo_center0`

analysis/derive.v

Line 346 in aaaad64

Lemma littleo_center (V W : normedModType R) (f : V -> W) (x : V) :

Put differential, derivative and jacobian outside landau

analysis/landau.v

Line 937 in 1566e32

Section Differential.

Forms library?

Where is the 'forms' library imported by derive in the diff branch?

analysis/derive.v

Line 4 in 6b36593

From mathcomp Require Import ssralg ssrnum fintype matrix forms.

Prepare a opam dev package

Document hierarchy

analysis/hierarchy.v

Line 1 in abb66fa

	Definition diff (F : filter_on V) (_ : phantom (set (set V)) F) (f : V -> W) :=
	(get (fun (df : {linear V -> W}) => continuous df /\ forall x,
	f x = f (lim F) + df (x - lim F) +o_(x \near F) (x - lim F))).

	Section Bigmaxr.

	Variable (R : realDomainType).

	Lemma bigmaxr_mkcond I r (P : pred I) (F : I -> R) x :
	\big[maxr/x]_(i <- r \| P i) F i =
	\big[maxr/x]_(i <- r) (if P i then F i else x).
	Proof.
	rewrite unlock; elim: r x => //= i r ihr x.
	case P; rewrite ihr // maxr_r //; elim: r {ihr} => //= j r ihr.
	by rewrite ler_maxr ihr orbT.
	Qed.

	Lemma bigminr_maxr I r (P : pred I) (F : I -> R) x :
	\big[minr/x]_(i <- r \| P i) F i = - \big[maxr/- x]_(i <- r \| P i) - F i.
	Proof.
	by elim/big_rec2: _ => [\|i y _ _ ->]; rewrite ?oppr_max opprK.
	Qed.

	Lemma bigminr_mkcond I r (P : pred I) (F : I -> R) x :
	\big[minr/x]_(i <- r \| P i) F i =
	\big[minr/x]_(i <- r) (if P i then F i else x).
	Proof.
	rewrite !bigminr_maxr bigmaxr_mkcond; congr (- _).
	by apply: eq_bigr => i _; case P.
	Qed.

	Lemma bigmaxr_split I r (P : pred I) (F1 F2 : I -> R) x :
	\big[maxr/x]_(i <- r \| P i) (maxr (F1 i) (F2 i)) =
	maxr (\big[maxr/x]_(i <- r \| P i) F1 i) (\big[maxr/x]_(i <- r \| P i) F2 i).
	Proof.
	by elim/big_rec3: _ => [\|i y z _ _ ->]; rewrite ?maxrr // maxrCA -!maxrA maxrCA.
	Qed.

	Lemma bigminr_split I r (P : pred I) (F1 F2 : I -> R) x :
	\big[minr/x]_(i <- r \| P i) (minr (F1 i) (F2 i)) =
	minr (\big[minr/x]_(i <- r \| P i) F1 i) (\big[minr/x]_(i <- r \| P i) F2 i).
	Proof.
	rewrite !bigminr_maxr -oppr_max -bigmaxr_split; congr (- _).
	by apply: eq_bigr => i _; rewrite oppr_min.
	Qed.

	Lemma filter_andb I r (a P : pred I) :
	[seq i <- r \| P i && a i] = [seq i <- [seq j <- r \| P j] \| a i].
	Proof. by elim: r => //= i r ->; case P. Qed.

	Lemma bigmaxr_idl I r (P : pred I) (F : I -> R) x :
	\big[maxr/x]_(i <- r \| P i) F i = maxr x (\big[maxr/x]_(i <- r \| P i) F i).
	Proof.
	rewrite -big_filter; elim: [seq i <- r \| P i] => [\|i l ihl].
	by rewrite big_nil maxrr.
	by rewrite big_cons maxrCA -ihl.
	Qed.

	Lemma bigminr_idl I r (P : pred I) (F : I -> R) x :
	\big[minr/x]_(i <- r \| P i) F i = minr x (\big[minr/x]_(i <- r \| P i) F i).
	Proof. by rewrite !bigminr_maxr {1}bigmaxr_idl oppr_max opprK. Qed.

	Lemma bigmaxrID I r (a P : pred I) (F : I -> R) x :
	\big[maxr/x]_(i <- r \| P i) F i =
	maxr (\big[maxr/x]_(i <- r \| P i && a i) F i)
	(\big[maxr/x]_(i <- r \| P i && ~~ a i) F i).
	Proof.
	rewrite -!(big_filter _ (fun _ => _ && _)) !filter_andb !big_filter.
	rewrite ![in RHS](bigmaxr_mkcond _ _ F) !big_filter -bigmaxr_split.
	have eqmax : forall i, P i ->
	maxr (if a i then F i else x) (if ~~ a i then F i else x) = maxr (F i) x.
	by move=> i _; case: (a i) => //=; rewrite maxrC.
	rewrite [RHS](eq_bigr _ eqmax) -!(big_filter _ P).
	elim: [seq j <- r \| P j] => [\|j l ihl]; first by rewrite !big_nil.
	by rewrite !big_cons -maxrA -bigmaxr_idl ihl.
	Qed.

	Lemma bigminrID I r (a P : pred I) (F : I -> R) x :
	\big[minr/x]_(i <- r \| P i) F i =
	minr (\big[minr/x]_(i <- r \| P i && a i) F i)
	(\big[minr/x]_(i <- r \| P i && ~~ a i) F i).
	Proof. by rewrite !bigminr_maxr -oppr_max -bigmaxrID. Qed.

	Lemma bigmaxr_seq1 I (i : I) (F : I -> R) x :
	\big[maxr/x]_(j <- [:: i]) F j = maxr (F i) x.
	Proof. by rewrite unlock /=. Qed.

	Lemma bigminr_seq1 I (i : I) (F : I -> R) x :
	\big[minr/x]_(j <- [:: i]) F j = minr (F i) x.
	Proof. by rewrite unlock /=. Qed.

	Lemma bigmaxr_pred1_eq (I : finType) (i : I) (F : I -> R) x :
	\big[maxr/x]_(j \| j == i) F j = maxr (F i) x.
	Proof. by rewrite -big_filter filter_index_enum enum1 bigmaxr_seq1. Qed.

	Lemma bigminr_pred1_eq (I : finType) (i : I) (F : I -> R) x :
	\big[minr/x]_(j \| j == i) F j = minr (F i) x.
	Proof. by rewrite bigminr_maxr bigmaxr_pred1_eq oppr_max !opprK. Qed.

	Lemma bigmaxr_pred1 (I : finType) i (P : pred I) (F : I -> R) x :
	P =1 pred1 i -> \big[maxr/x]_(j \| P j) F j = maxr (F i) x.
	Proof. by move/(eq_bigl _ _)->; apply: bigmaxr_pred1_eq. Qed.

	Lemma bigminr_pred1 (I : finType) i (P : pred I) (F : I -> R) x :
	P =1 pred1 i -> \big[minr/x]_(j \| P j) F j = minr (F i) x.
	Proof. by move/(eq_bigl _ _)->; apply: bigminr_pred1_eq. Qed.

	Lemma bigmaxrD1 (I : finType) j (P : pred I) (F : I -> R) x :
	P j -> \big[maxr/x]_(i \| P i) F i
	= maxr (F j) (\big[maxr/x]_(i \| P i && (i != j)) F i).
	Proof.
	move=> Pj; rewrite (bigmaxrID _ (pred1 j)) [in RHS]bigmaxr_idl maxrA.
	by congr maxr; apply: bigmaxr_pred1 => i; rewrite /= andbC; case: eqP => //->.
	Qed.

	Lemma bigminrD1 (I : finType) j (P : pred I) (F : I -> R) x :
	P j -> \big[minr/x]_(i \| P i) F i
	= minr (F j) (\big[minr/x]_(i \| P i && (i != j)) F i).
	Proof.
	by move=> Pj; rewrite !bigminr_maxr (bigmaxrD1 _ _ Pj) oppr_max opprK.
	Qed.

	Lemma ler_bigmaxr_cond (I : finType) (P : pred I) (F : I -> R) x i0 :
	P i0 -> F i0 <= \big[maxr/x]_(i \| P i) F i.
	Proof. by move=> Pi0; rewrite (bigmaxrD1 _ _ Pi0) ler_maxr lerr. Qed.

	Lemma bigminr_ler_cond (I : finType) (P : pred I) (F : I -> R) x i0 :
	P i0 -> \big[minr/x]_(i \| P i) F i <= F i0.
	Proof. by move=> Pi0; rewrite (bigminrD1 _ _ Pi0) ler_minl lerr. Qed.

	Lemma ler_bigmaxr (I : finType) (F : I -> R) (i0 : I) x :
	F i0 <= \big[maxr/x]_i F i.
	Proof. exact: ler_bigmaxr_cond. Qed.

	Lemma bigminr_ler (I : finType) (F : I -> R) (i0 : I) x :
	\big[minr/x]_i F i <= F i0.
	Proof. exact: bigminr_ler_cond. Qed.

	Lemma bigmaxr_lerP (I : finType) (P : pred I) m (F : I -> R) x :
	reflect (x <= m /\ forall i, P i -> F i <= m)
	(\big[maxr/x]_(i \| P i) F i <= m).
	Proof.
	apply: (iffP idP) => [\|[lexm leFm]]; last first.
	by elim/big_ind: _ => // ??; rewrite ler_maxl =>->.
	rewrite bigmaxr_idl ler_maxl => /andP[-> leFm]; split=> // i Pi.
	by apply: ler_trans leFm; apply: ler_bigmaxr_cond.
	Qed.

	Lemma bigminr_gerP (I : finType) (P : pred I) m (F : I -> R) x :
	reflect (m <= x /\ forall i, P i -> m <= F i)
	(m <= \big[minr/x]_(i \| P i) F i).
	Proof.
	rewrite bigminr_maxr ler_oppr; apply: (iffP idP).
	by move=> /bigmaxr_lerP [? lemF]; split=> [\|??]; rewrite -ler_opp2 ?lemF.
	by move=> [? lemF]; apply/bigmaxr_lerP; split=> [\|??]; rewrite ler_opp2 ?lemF.
	Qed.

	Lemma bigmaxr_sup (I : finType) i0 (P : pred I) m (F : I -> R) x :
	P i0 -> m <= F i0 -> m <= \big[maxr/x]_(i \| P i) F i.
	Proof. by move=> Pi0 ?; apply: ler_trans (ler_bigmaxr_cond _ _ Pi0). Qed.

	Lemma bigminr_inf (I : finType) i0 (P : pred I) m (F : I -> R) x :
	P i0 -> F i0 <= m -> \big[minr/x]_(i \| P i) F i <= m.
	Proof. by move=> Pi0 ?; apply: ler_trans (bigminr_ler_cond _ _ Pi0) _. Qed.

	Lemma bigmaxr_ltrP (I : finType) (P : pred I) m (F : I -> R) x :
	reflect (x < m /\ forall i, P i -> F i < m)
	(\big[maxr/x]_(i \| P i) F i < m).
	Proof.
	apply: (iffP idP) => [\|[ltxm ltFm]]; last first.
	by elim/big_ind: _ => // ??; rewrite ltr_maxl =>->.
	rewrite bigmaxr_idl ltr_maxl => /andP[-> ltFm]; split=> // i Pi.
	by apply: ler_lt_trans ltFm; apply: ler_bigmaxr_cond.
	Qed.

	Lemma bigminr_gtrP (I : finType) (P : pred I) m (F : I -> R) x :
	reflect (m < x /\ forall i, P i -> m < F i)
	(m < \big[minr/x]_(i \| P i) F i).
	Proof.
	rewrite bigminr_maxr ltr_oppr; apply: (iffP idP).
	by move=> /bigmaxr_ltrP [? ltmF]; split=> [\|??]; rewrite -ltr_opp2 ?ltmF.
	by move=> [? ltmF]; apply/bigmaxr_ltrP; split=> [\|??]; rewrite ltr_opp2 ?ltmF.
	Qed.

	Lemma bigmaxr_gerP (I : finType) (P : pred I) m (F : I -> R) x :
	reflect (m <= x \/ exists2 i, P i & m <= F i)
	(m <= \big[maxr/x]_(i \| P i) F i).
	Proof.
	apply: (iffP idP) => [\|[lemx\|[i Pi lemFi]]]; last 2 first.
	- by rewrite bigmaxr_idl ler_maxr lemx.
	- by rewrite (bigmaxrD1 _ _ Pi) ler_maxr lemFi.
	rewrite lerNgt => /bigmaxr_ltrP /asboolPn.
	rewrite asbool_and negb_and => /orP [/asboolPn/negP\|/existsp_asboolPn [i]].
	by rewrite -lerNgt; left.
	by move=> /asboolPn/imply_asboolPn [Pi /negP]; rewrite -lerNgt; right; exists i.
	Qed.

	Lemma bigminr_lerP (I : finType) (P : pred I) m (F : I -> R) x :
	reflect (x <= m \/ exists2 i, P i & F i <= m)
	(\big[minr/x]_(i \| P i) F i <= m).
	Proof.
	rewrite bigminr_maxr ler_oppl; apply: (iffP idP).
	by move=> /bigmaxr_gerP [?\|[i ??]]; [left\|right; exists i => //];
	rewrite -ler_opp2.
	by move=> [?\|[i ??]]; apply/bigmaxr_gerP; [left\|right; exists i => //];
	rewrite ler_opp2.
	Qed.

	Lemma bigmaxr_gtrP (I : finType) (P : pred I) m (F : I -> R) x :
	reflect (m < x \/ exists2 i, P i & m < F i)
	(m < \big[maxr/x]_(i \| P i) F i).
	Proof.
	apply: (iffP idP) => [\|[ltmx\|[i Pi ltmFi]]]; last 2 first.
	- by rewrite bigmaxr_idl ltr_maxr ltmx.
	- by rewrite (bigmaxrD1 _ _ Pi) ltr_maxr ltmFi.
	rewrite ltrNge => /bigmaxr_lerP /asboolPn.
	rewrite asbool_and negb_and => /orP [/asboolPn/negP\|/existsp_asboolPn [i]].
	by rewrite -ltrNge; left.
	by move=> /asboolPn/imply_asboolPn [Pi /negP]; rewrite -ltrNge; right; exists i.
	Qed.

	Lemma bigminr_ltrP (I : finType) (P : pred I) m (F : I -> R) x :
	reflect (x < m \/ exists2 i, P i & F i < m)
	(\big[minr/x]_(i \| P i) F i < m).
	Proof.
	rewrite bigminr_maxr ltr_oppl; apply: (iffP idP).
	by move=> /bigmaxr_gtrP [?\|[i ??]]; [left\|right; exists i => //];
	rewrite -ltr_opp2.
	by move=> [?\|[i ??]]; apply/bigmaxr_gtrP; [left\|right; exists i => //];
	rewrite ltr_opp2.
	Qed.

	End Bigmaxr.

	Arguments bigmaxr_mkcond {R I r}.
	Arguments bigmaxrID {R I r}.
	Arguments bigmaxr_pred1 {R I} i {P F}.
	Arguments bigmaxrD1 {R I} j {P F}.
	Arguments ler_bigmaxr_cond {R I P F}.
	Arguments ler_bigmaxr {R I F}.
	Arguments bigmaxr_sup {R I} i0 {P m F}.
	Arguments bigminr_mkcond {R I r}.
	Arguments bigminrID {R I r}.
	Arguments bigminr_pred1 {R I} i {P F}.
	Arguments bigminrD1 {R I} j {P F}.
	Arguments bigminr_ler_cond {R I P F}.
	Arguments bigminr_ler {R I F}.
	Arguments bigminr_inf {R I} i0 {P m F}.

	Section function_space.

	Definition cst {T T' : Type} (x : T') : T -> T' := fun=> x.

	Program Definition fct_zmodMixin (T : Type) (M : zmodType) :=
	@ZmodMixin (T -> M) \0 (fun f x => - f x) (fun f g => f \+ g) _ _ _ _.
	Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite addrA. Qed.
	Next Obligation. by move=> f g; rewrite funeqE=> x /=; rewrite addrC. Qed.
	Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite add0r. Qed.
	Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite addNr. Qed.
	Canonical fct_zmodType T (M : zmodType) := ZmodType (T -> M) (fct_zmodMixin T M).

	Program Definition fct_ringMixin (T : pointedType) (M : ringType) :=
	@RingMixin [zmodType of T -> M] (cst 1) (fun f g x => f x * g x)
	_ _ _ _ _ _.
	Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrA. Qed.
	Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite mul1r. Qed.
	Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite mulr1. Qed.
	Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrDl. Qed.
	Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrDr. Qed.
	Next Obligation.
	by apply/eqP; rewrite funeqE => /(_ point) /eqP; rewrite oner_eq0.
	Qed.
	Canonical fct_ringType (T : pointedType) (M : ringType) :=
	RingType (T -> M) (fct_ringMixin T M).

	Program Canonical fct_comRingType (T : pointedType) (M : comRingType) :=
	ComRingType (T -> M) _.
	Next Obligation. by move=> f g; rewrite funeqE => x; rewrite mulrC. Qed.

	Program Definition fct_lmodMixin (U : Type) (R : ringType) (V : lmodType R)
	:= @LmodMixin R [zmodType of U -> V] (fun k f => k \*: f) _ _ _ _.
	Next Obligation. rewrite funeqE => x; exact: scalerA. Qed.
	Next Obligation. by move=> f; rewrite funeqE => x /=; rewrite scale1r. Qed.
	Next Obligation. by move=> f g h; rewrite funeqE => x /=; rewrite scalerDr. Qed.
	Next Obligation. by move=> f g; rewrite funeqE => x /=; rewrite scalerDl. Qed.
	Canonical fct_lmodType U (R : ringType) (V : lmodType R) :=
	LmodType _ (U -> V) (fct_lmodMixin U V).

	Lemma fct_sumE (T : Type) (M : zmodType) n (f : 'I_n -> T -> M) (x : T) :
	(\sum_(i < n) f i) x = \sum_(i < n) f i x.
	Proof.
	elim: n f => [\|n H] f;
	by rewrite !(big_ord0,big_ord_recr) //= -[LHS]/(_ x + _ x) H.
	Qed.

	End function_space.

math-comp / analysis Goto Github PK

analysis's Introduction

Analysis library compatible with Mathematical Components

Meta

Building and installation instructions

About the stability of this library

Documentation

Mathematical structures

Hierarchies of functions

Development information

Previous work reused at the time of the first releases

Acknowledgments

analysis's People

Contributors

Stargazers

Watchers

Forkers

analysis's Issues

Recommend Projects

Recommend Topics

Recommend Org