Library Coqtail.Vec.Vec_prop

Library Coqtail.Vec.VecDep_def

Library Coqtail.Vec.Vec_def

Library Coqtail.Topology.Vectors

• Vector spaces

Library Coqtail.Topology.Topology

• Infinite Union
• Topological space
• Separation
• Sets properties
• Infinite_Union Properties
• Trivial topology
• Discrete topology

Library Coqtail.Topology.TFunctions

Library Coqtail.Topology.TContinuity

Library Coqtail.Topology.Sets

Library Coqtail.Topology.Metrics

• Topological space
• Metric Space
• Open sets
• Balls
• A metric space defines a topology
• A metric space is separated

Library Coqtail.Topology.Inner_product

Library Coqtail.Tactics.Ass_handling

Library Coqtail.Subseq.Subseq

Library Coqtail.Sets.My_Sets_facts

Library Coqtail.Sets.My_Finite_sets_facts

Library Coqtail.Sets.Cartesian_product

Library Coqtail.Sets.Cartesian_product_facts

Library Coqtail.Reals.Wallis

Library Coqtail.Reals.Triangular

Library Coqtail.Reals.Rzeta2

• Convergence of the 1/n² series
• Splitting series in odd and even terms
• Introduction of pi
• Sums indexed by relative integers (from -N to N)
• Introducing pi to bisums
• Double sums
• Rewriting double sums
• Rewriting An * An - Bn
• Bounding
• Bn converges to pi²/4
• Linking sums on nat and sums on Z
• Linking even terms of the 1/n² series to the series itself
• Final theorem

Library Coqtail.Reals.Rtrigo_facts

Library Coqtail.Reals.RTaylor

• • Taylor series of ln
• Taylor series of ln (1 - x)
• Taylor series of ln (1 + x)

Library Coqtail.Reals.Rtactic

Library Coqtail.Reals.RStirling

Library Coqtail.Reals.Rseries

Library Coqtail.Reals.Rseries.Rseries_usual

Library Coqtail.Reals.Rseries.Rseries_RiemannInt

• Generalized Chasles relation
• Link between series and integral

Library Coqtail.Reals.Rseries.Rseries_remainder_facts

Library Coqtail.Reals.Rseries.Rseries_pos_facts

• Properties about positive term series

Library Coqtail.Reals.Rseries.Rseries_facts

• Convergence and comparisons between sequences
• Summing Landau's relations when the series go to infinity
• Summing Landau's relations when the series converge

Library Coqtail.Reals.Rseries.Rseries_def

• Convergence of series
• Bounds
• Remainders of series

Library Coqtail.Reals.Rseries.Rseries_cv_facts

• Convergence facts
• Mertens' theorem
• Extensionnal equality compatibility

Library Coqtail.Reals.Rseries.Rseries_base_facts

Library Coqtail.Reals.Rsequence

Library Coqtail.Reals.Rsequence.Rsequence_usual_facts

• Convergence of usual sequences.
• Growth comparison.
• Things that don't have anything to do there...

Library Coqtail.Reals.Rsequence.Rsequence_tactics

• A tactic that constructs the limit of a sequence and the proof that this

Library Coqtail.Reals.Rsequence.Rsequence_tactics_reflection

Library Coqtail.Reals.Rsequence.Rsequence_sums_facts

• Rseq_sum properties
• Rseq_pps : compatibility with common operations.
• Rpser_abs, Rpser

Library Coqtail.Reals.Rsequence.Rsequence_subsequence

Library Coqtail.Reals.Rsequence.Rsequence_stdlib

Library Coqtail.Reals.Rsequence.Rsequence_ring

Library Coqtail.Reals.Rsequence.Rsequence_rewrite_facts

Library Coqtail.Reals.Rsequence.Rsequence_rel_facts

• Big-O, little-O and equivalence relations.
• Big-O and common operations.
• Little-O and common operations.
• Equivalence and common operations.
• Convergence and little-O.
• Divergence and little-O.
• Convergence and equivalence.

Library Coqtail.Reals.Rsequence.Rsequence_facts

• Results which need classical

Library Coqtail.Reals.Rsequence.Rsequence_def

• Morphism of functions on R to sequences.
• Extensionnal equality.
• Various properties.
• Convergence of sequences.
• Landau relations on sequences.
• Usual sequences.

Library Coqtail.Reals.Rsequence.Rsequence_cv_facts

• Convergence compatibility.
• Infinite convergence compatibility.
• Uniqueness of limit.
• Sandwich theorem.
• Limit of (non) negative terms
• Compatibility of Rle and interval with the limit

Library Coqtail.Reals.Rsequence.Rsequence_bound_facts

• Boundedness compatibility.

Library Coqtail.Reals.Rsequence.Rsequence_base_facts

• • Extensionnal equality.
• Extensional equality is an equivalence relation.
• Rseq_opp is involutive.
• Compatibility of extensional equality with convergence.
• Compatibility of extensional equality with Laudau relations.
  • Boundedness and subsequences
  • Partial sequences.
  • Asymptotic properties.
• Convergence is asymptotic.
• Landau relations are asymptotic.

Library Coqtail.Reals.Rpser

Library Coqtail.Reals.Rpser.Rpser_usual

• Definition of the null power series.
• Simplification when zipping with 0
• Definition of the constant power series.
• Definition of the identity
• Definition of the sum of x^k
• Definition of exp, cosine and sine
• About the derivatives of these functions
• Definition of arctan

Library Coqtail.Reals.Rpser.Rpser_taylor

• Comparison of Taylor development

Library Coqtail.Reals.Rpser.Rpser_sums

• Definition of weaksum_r
• Definition of sum_r
• Definition of sum

Library Coqtail.Reals.Rpser.Rpser_sums_facts

• Compatibility of Rpser with Rseq_prod (Mertens' theorem)
• Unfolding sums.
• Compatibility of weaksum_r with the common operations.
• Compatibility of sum_r with the common operations.
• Compatibility of sum with the common operations.

Library Coqtail.Reals.Rpser.Rpser_radius_facts

• Caracterization of the cv radius of the formal derivative

Library Coqtail.Reals.Rpser.Rpser_derivative

• Definition of the formal derivative
• The formal derivative is, inside the cv-disk, the actual derivative.
• Derivability / continuity of the sum when the cv disk as an infinite radius

Library Coqtail.Reals.Rpser.Rpser_derivative_facts

• An_nth_deriv is the general term of the nth derivative of sum An.

Library Coqtail.Reals.Rpser.Rpser_def

• Definitions

Library Coqtail.Reals.Rpser.Rpser_def_simpl

• • Simplification lemmas about the new concepts.
• gt_pser, gt_abs_pser
• An_deriv, An_nth_deriv

Library Coqtail.Reals.Rpser.Rpser_cv_facts

• Abel's lemma : convergence of the power serie inside the cv-disc
• D'Alembert's criterion

Library Coqtail.Reals.Rpser.Rpser_base_facts

• • Some lemmas manipulating the definitions.
• Extensionality of radiuses.
• Cv_radius_weak

Library Coqtail.Reals.Rpow_facts

Library Coqtail.Reals.RIVT

• Intermediate Value Theorem on an Interval and its corollary

Library Coqtail.Reals.Rintegral

• Real riemannian integrals
• Definition of the integral of f between a and b using Riemann_integrable
• Common results on integrals
• Continuous functions are integrable
• Chasles relation on integrals
• Compatibility of integrals with operations
• Inequalities involving integrals

Library Coqtail.Reals.Rintegral.Rintegral_usual

Library Coqtail.Reals.Rintegral.Rintegral_tactic

Library Coqtail.Reals.Rintegral.Riemann_integrable

Library Coqtail.Reals.RFsequence

• Morphism of functions on R -> R to sequences.
• Convergence of functions sequences.

Library Coqtail.Reals.RFsequence_facts

Library Coqtail.Reals.Rextensionality

• Extensionality of the common properties of functions.
• Extensionality of power serie related concepts.

Library Coqtail.Reals.Reirr

• Final result: e is irrational

Library Coqtail.Reals.Raxioms.Rdefinitions

Library Coqtail.Reals.Raxioms.Rcauchy

Library Coqtail.Reals.Raxioms.Rcauchy_lemmas

Library Coqtail.Reals.Raxioms.Raxioms

Library Coqtail.Reals.Ratan

• Definition of arctan as the reciprocal of tan
• Definition of arctan as the sum of a power series.

Library Coqtail.Reals.Ranalysis.Rinterval

• The definitions used in this file: middle, interval, Rball.
• middle's properties.
• interval's properties.
• dist properties

Library Coqtail.Reals.Ranalysis.Rfunction_facts

Library Coqtail.Reals.Ranalysis.Rfunction_def

Library Coqtail.Reals.Ranalysis.Rfunction_classes

Library Coqtail.Reals.Ranalysis.Rfunction_classes_usual

• Classification of common functions

Library Coqtail.Reals.Ranalysis.Rfunction_classes_facts

• Extensionality of the properties.
• Relations between the D and the C class.
• Basic Properties
• Compatibility of C, D with common operators
• Compatibility with derivation

Library Coqtail.Reals.Ranalysis.Rfunction_classes_def

• Being of Class D_n.
• Being of Class C_n

Library Coqtail.Reals.Ranalysis.Ranalysis_usual

• Derivability (thus continuity) of usual functions.
• Identity

Library Coqtail.Reals.Ranalysis.Ranalysis_MVT

Library Coqtail.Reals.Ranalysis.Ranalysis_monotonicity

Library Coqtail.Reals.Ranalysis.Ranalysis_facts

• Correcting stdlib's mistakes (generic derivable* proofs)
• Usual functions
• Relating variations to the value of the derivative

Library Coqtail.Reals.Ranalysis.Ranalysis_extend

Library Coqtail.Reals.Ranalysis.Ranalysis_derivability

• Extensionality of derivable*
• Unicity of the derivative
• In specific cases we can come back from the specific case to the one with no limitation.
• derivable implies continuous
• Compatibility of derivable*_in with common operations.

Library Coqtail.Reals.Ranalysis.Ranalysis_def

• (Re)defining the derivability predicate.
• Generic notions (injective, surjective, increasing, reciprocal, etc.)

Library Coqtail.Reals.Ranalysis.Ranalysis_def_simpl

• Example of dense domains
• Extensionality of growth_rate
• growth_rate is compatible with common operations.
• All the definitions using in are contravariant in their domain
• Extensionality of limit1_in

Library Coqtail.Reals.Ranalysis.Ranalysis_continuity

• Extensionality of continuity_pt_in
• How to relate the different notions of continuity.
• Simple compatibility results on continuity_in

Library Coqtail.Reals.Ranalysis.Ranalysis5

• Continuity of the reciprocal function
• Derivability of the reciprocal function
• Value of the derivative of the reciprocal function

Library Coqtail.Reals.Ranalysis.Nth_derivative_facts

• Simple equivalences
• nth_derive is not proof-sensible.
• Relation between nth_derive and derive.

Library Coqtail.Reals.Ranalysis.Nth_derivative_def

• Definition of the nth derivative

Library Coqtail.Reals.Logic.Runcountable

• R is uncountable.

Library Coqtail.Reals.Logic.Rmarkov

Library Coqtail.Reals.Hopital

Library Coqtail.Reals.Finite_Calculus.Definitions

Library Coqtail.Reals.Ediff.Vectorial_Cauchy

Library Coqtail.Reals.Ediff.realisation_by_stdlib

Library Coqtail.Reals.Ediff.integrales

Library Coqtail.Reals.Ediff.Evect

Library Coqtail.Reals.Dequa.Dequa_quote

• Quoting differential equations
• Test materials

Library Coqtail.Reals.Dequa.Dequa_facts

Library Coqtail.Reals.Dequa.Dequa_examples

Library Coqtail.Reals.Dequa.Dequa_def

Library Coqtail.Reals.Cauchy_lipschitz

Library Coqtail.mytheories.MyZ

Library Coqtail.mytheories.myReals.MyRIneq

Library Coqtail.mytheories.myReals.MyRfunctions

Library Coqtail.mytheories.myReals.MyReals

Library Coqtail.mytheories.myReals.MyR_dist

Library Coqtail.mytheories.myReals.MyRbasic_fun

• Rabs properties

Library Coqtail.mytheories.myReals.MyRbase

Library Coqtail.mytheories.myReals.MyNNR

Library Coqtail.mytheories.myReals.MyINR

Library Coqtail.mytheories.MyNeq

Library Coqtail.mytheories.MyNat

Library Coqtail.Monad.Option

Library Coqtail.Hierarchy.Vector_space_facts

Library Coqtail.Hierarchy.Type_class_instance

Library Coqtail.Hierarchy.Type_class_instance_beta

Library Coqtail.Hierarchy.Type_class_definition

Library Coqtail.Hierarchy.Type_class_definition_beta

Library Coqtail.Hierarchy.Commutative_ring_binomial

Library Coqtail.Graphs.definitions

Library Coqtail.Fresh.Reals.Rseq

Library Coqtail.Fresh.Reals.Rrealize

Library Coqtail.Fresh.Reals.Rorder

Library Coqtail.Fresh.Reals.Rimpl

• Archimedean
• Completeness

Library Coqtail.Fresh.Reals.Rimpl_template

Library Coqtail.Fresh.Reals.Rfun

Library Coqtail.Fresh.Reals.Repsilon

Library Coqtail.Fresh.Reals.Rconvenient

• Useful and basics results on <, ==,
• Setoid

Library Coqtail.Fresh.Reals.Raxiom

• Constructive ordered field
• Archimedean
• Completeness

Library Coqtail.Fresh.Reals.Rapprox

Library Coqtail.Fresh.Reals.Rabs

Library Coqtail.Fresh.Reals.IZR

Library Coqtail.Fresh.Inhabited.Monad

Library Coqtail.Fresh.Inhabited.InhabitedTactics

Library Coqtail.Fresh.Inhabited.Functions

Library Coqtail.Fresh.Inhabited.Examples

Library Coqtail.Fresh.Inhabited.Choice_facts

Library Coqtail.Complex.Ctacfield

• • Tactics ring and field in the Complex field

Library Coqtail.Complex.Cseries

• Convergence of series
• Bounds
• Remainders of series

Library Coqtail.Complex.Cseries_facts

Library Coqtail.Complex.Csequence

Library Coqtail.Complex.Csequence_facts

• Asymptotic properties.
• Convergence compatibilities

Library Coqtail.Complex.Csequence_def

• Morphism of functions on C to sequences.
• Various properties.
• Convergence of sequences.

Library Coqtail.Complex.Croot_n

• • Every positive real has a n root
  • Every complex has a n root

Library Coqtail.Complex.Cpser_facts

• Sum of the formal derivative
• Derivability of a power serie within its disc of convergence

Library Coqtail.Complex.Cpser_def

• Definitions

Library Coqtail.Complex.Cpser_base_facts

• Some lemmas manipulating the definitions

Library Coqtail.Complex.Cprop_base

• Decidability lemmas
• Good relations on Cre Cim
  • • Compatibility of functions with equalities (Hint database)
• IRC
• Addition
• Multiplication
• Opposite
• Opposite and multiplication
• Minus
• Inversion
• Power
• Injection from R to C
• Injection from N to C
• Cnorm
• INC/Cre/Cim
• Cneq results
• Compatibility of IRC and real/complex lemma
• Compatibility of Cconj with Cnorm_sqr
• Compatibility of pow and Cpow

Library Coqtail.Complex.Cpow

• Power definition on C

Library Coqtail.Complex.Cpow_plus

Library Coqtail.Complex.Cpolar

• • Every complex number has polar coordinate

Library Coqtail.Complex.Complex

Library Coqtail.Complex.Cnorm

• Cnorm comparisons to zero
• Properties of simple operators
• Triangle Inequality

Library Coqtail.Complex.Cmet

Library Coqtail.Complex.Cfunctions

• Finite sum of (nat -> C) sequences
  • • Finite sum properties

Library Coqtail.Complex.CFsequence

• Morphism of functions on R -> R to sequences.
• Convergence of functions sequences.

Library Coqtail.Complex.CFsequence_facts

Library Coqtail.Complex.Cexp

• Definition and manipulation of the general term of the power serie of the exponential
• This power serie has a radius of convergence that is infinite
• The exponential is its own derivative
  • Euler's Formula

Library Coqtail.Complex.Cderiv

Library Coqtail.Complex.Cdefinitions

• • Definition of C and basic operations over C
  • Basic definitions and notations
  • Injection from N to C
  • Injection from Z to C

Library Coqtail.Complex.Cbase

• Complex to real lemmas.
• Field Lemmas.
• R Vector Space Lemmas
• Other properties (Cconj)

Library Coqtail.Complex.Canalysis_diff

• differentiability -> continuity along an axis
• Main rules

Library Coqtail.Complex.Canalysis_deriv

• Equivalence of this definition with the one using limit concept
• derivability -> continuity
• derivability -> differentiability
• Main rules
• derivable_pt compatibility lemmas
• derivable compatibility lemmas
• fully differentiability -/-> derivability
• MVT (weak version : the strong one is false when f has complex values

Library Coqtail.Complex.Canalysis_def

• Definition of continuity as a limit
• Derivative's definition using Landau's kernel
• Differentiability

Library Coqtail.Complex.Canalysis_cont

Library Coqtail.Complex.Canalysis_basic_facts

• derivable_pt_lim
• derivable

Library Coqtail.Arith.Ztools

• Contains some useful lemmas not in stdlib and a tactic

Library Coqtail.Arith.Znumfacts

• Number theory : factorisation, computation of Bezout coefficients and modular inverse

Library Coqtail.Arith.Zeqm

• Results about eqm, congruence modulo some integer

Library Coqtail.Arith.PI

• Two proofs of n<m are equals

Library Coqtail.Arith.Ntools

• Iteration of a function over nat

Library Coqtail.Arith.Npow

• Definition of power over nat
• Simplification
• Compatibility with order

Library Coqtail.Arith.Nnewton

• Definition of a newton sum
• Newton sum theorem

Library Coqtail.Arith.Nminus

Library Coqtail.Arith.Nlittle_fermat

• Fermat's little theorem over nat
• Alternative formulation of Fermat's little theorem

Library Coqtail.Arith.Nle

• Additional properties on le

Library Coqtail.Arith.Nk_ind

• Definition of kth-successor and generalized AND hypothesis
• Properties of next_P_k and kth_S
• Inductions on nat

Library Coqtail.Arith.Ninductions

Library Coqtail.Arith.Nfinite_sum

• Definition of a finite sum on nat with an index starting from 0
• Properties of finite sum

Library Coqtail.Arith.Nfinite_prod

• Definition of a finite product on nat with an index starting from 0
• Properties of finite product

Library Coqtail.Arith.Ndiv

• Definitions
• Basic results on prime numbers
• Basic properties of divisibility
• Basic properties of quotient
• Properties of divisibility
• Properties of coprimes
• Gauss theorem
• Decidability of divisibility
• Greatest strict divisor
• Decidability of primality with greatest strict divisor
• Lowest strict divisor
• Decidability of primality with lowest strict divisor
• Gauss theorem (prime formulation)
• Compatibility of coprimality with multiplication
• Primality results
• Relation between lowest strict divisor and greatest strict divisor

Library Coqtail.Arith.Nbinomial

• Definition of a binomial coefficient using Pascal relation
• Properties of binomial coefficients

Library Coqtail.Arith.Natsets

• Basic operations and types

Library Coqtail.Arith.Modulo

Library Coqtail.Arith.Lagrange_four_square

Library Coqtail.Arith.Hurwitz_prop

Library Coqtail.Arith.Hurwitz_def