## Library Coqtail.Vec.Vec_prop

## Library Coqtail.Vec.VecDep_def

## Library Coqtail.Vec.Vec_def

## Library Coqtail.Topology.Vectors

## 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

## Library Coqtail.Reals.Rtactic

## Library Coqtail.Reals.RStirling

## Library Coqtail.Reals.Rseries

## Library Coqtail.Reals.Rseries.Rseries_usual

## Library Coqtail.Reals.Rseries.Rseries_RiemannInt

## Library Coqtail.Reals.Rseries.Rseries_remainder_facts

## Library Coqtail.Reals.Rseries.Rseries_pos_facts

## 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

## Library Coqtail.Reals.Rseries.Rseries_cv_facts

## Library Coqtail.Reals.Rseries.Rseries_base_facts

## Library Coqtail.Reals.Rsequence

## Library Coqtail.Reals.Rsequence.Rsequence_usual_facts

## Library Coqtail.Reals.Rsequence.Rsequence_tactics

## Library Coqtail.Reals.Rsequence.Rsequence_tactics_reflection

## Library Coqtail.Reals.Rsequence.Rsequence_sums_facts

## 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

## 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

## Library Coqtail.Reals.Rsequence.Rsequence_base_facts

- Extensional equality is an equivalence relation.
- Rseq_opp is involutive.
- Compatibility of extensional equality with convergence.
- Compatibility of extensional equality with Laudau relations.
- 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

## Library Coqtail.Reals.Rpser.Rpser_sums

## 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

## 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

## Library Coqtail.Reals.Rpser.Rpser_def

## Library Coqtail.Reals.Rpser.Rpser_def_simpl

## Library Coqtail.Reals.Rpser.Rpser_cv_facts

## Library Coqtail.Reals.Rpser.Rpser_base_facts

## Library Coqtail.Reals.Rpow_facts

## Library Coqtail.Reals.RIVT

## 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

## 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

## 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

## 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

## 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

## Library Coqtail.Reals.Ranalysis.Ranalysis_usual

## 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

## Library Coqtail.Reals.Ranalysis.Nth_derivative_def

## Library Coqtail.Reals.Logic.Runcountable

## 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

## 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

## 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

## Library Coqtail.Fresh.Reals.Rimpl_template

## Library Coqtail.Fresh.Reals.Rfun

## Library Coqtail.Fresh.Reals.Repsilon

## Library Coqtail.Fresh.Reals.Rconvenient

## Library Coqtail.Fresh.Reals.Raxiom

## 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

## Library Coqtail.Complex.Cseries

## Library Coqtail.Complex.Cseries_facts

## Library Coqtail.Complex.Csequence

## Library Coqtail.Complex.Csequence_facts

## Library Coqtail.Complex.Csequence_def

## Library Coqtail.Complex.Croot_n

## Library Coqtail.Complex.Cpser_facts

## Library Coqtail.Complex.Cpser_def

## Library Coqtail.Complex.Cpser_base_facts

## Library Coqtail.Complex.Cprop_base

- Decidability lemmas
- Good relations on Cre Cim
- 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

## Library Coqtail.Complex.Cpow_plus

## Library Coqtail.Complex.Cpolar

## Library Coqtail.Complex.Complex

## Library Coqtail.Complex.Cnorm

## Library Coqtail.Complex.Cmet

## Library Coqtail.Complex.Cfunctions

## Library Coqtail.Complex.CFsequence

## 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

## Library Coqtail.Complex.Cderiv

## Library Coqtail.Complex.Cdefinitions

## Library Coqtail.Complex.Cbase

## Library Coqtail.Complex.Canalysis_diff

## 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

## Library Coqtail.Complex.Canalysis_cont

## Library Coqtail.Complex.Canalysis_basic_facts

## Library Coqtail.Arith.Ztools

## Library Coqtail.Arith.Znumfacts

## Library Coqtail.Arith.Zeqm

## Library Coqtail.Arith.PI

## Library Coqtail.Arith.Ntools

## Library Coqtail.Arith.Npow

## Library Coqtail.Arith.Nnewton

## Library Coqtail.Arith.Nminus

## Library Coqtail.Arith.Nlittle_fermat

## Library Coqtail.Arith.Nle

## 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

## Library Coqtail.Arith.Nfinite_prod

## 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

## Library Coqtail.Arith.Natsets

## Library Coqtail.Arith.Modulo

## Library Coqtail.Arith.Lagrange_four_square

## Library Coqtail.Arith.Hurwitz_prop

## Library Coqtail.Arith.Hurwitz_def

This page has been generated by coqdoc

This page has been generated by coqdoc