Trunk#1

Open

spitters wants to merge 119 commits intorobbertkrebbers:masterfrom

spitters:trunk

Commits on Feb 3, 2012

Merge pull request #1 from 0x01/master
wires
committed

Commits on Apr 27, 2012

Commits on May 8, 2012

Changed UniformlyContinuous and Contraction into unbundled type classes. Bundling is expected to be done later, if necessary.
EvgenyMakarov
committed

Commits on May 11, 2012

Proved a lemma for the fixpoint theorem about the distance between x_n and x_{n+1}
EvgenyMakarov
committed

Commits on May 16, 2012

Proved a lemma needed to show that the sequence of approximations is a Cauchy sequence.
EvgenyMakarov
committed

Commits on May 21, 2012

Proved lemma dist_xm_xn'
EvgenyMakarov
committed

Commits on Jun 1, 2012

Defined complete metric spaces
EvgenyMakarov
committed

Commits on Jun 5, 2012

Defined complete metric space
EvgenyMakarov
committed

Commits on Jun 12, 2012

Proved theorems about limits and continuous functions, contractions
EvgenyMakarov
committed

Commits on Jun 21, 2012

Proved Banach fixpoint theorem
EvgenyMakarov
committed

Commits on Jun 25, 2012

Changed the definition of equality in a metric space and removed unnecessary axioms
EvgenyMakarov
committed

Commits on Jun 28, 2012

Added FromMetric2.v to define conversion from metric2.Metric to the metric space type class
EvgenyMakarov
committed

Commits on Jul 3, 2012

Commits on Jul 5, 2012

Proved that the completion of a metric space in the sense of Metric2.Complete is complete in the sense of type classes
EvgenyMakarov
committed

Commits on Aug 7, 2012

Started adapting Simpson integration to AR
EvgenyMakarov
committed

Commits on Aug 21, 2012

Now compiles with Coq 8.4
EvgenyMakarov
committed

Commits on Aug 22, 2012

Performed experiments with Simpson integration
EvgenyMakarov
committed

Commits on Sep 5, 2012

Experiments on Simpson integration
EvgenyMakarov
committed

Commits on Sep 11, 2012

Added Picard iteration
EvgenyMakarov
committed

Commits on Oct 2, 2012

Moved Banach Fixpoint theorem into BanachFixpoint.v. Added locally uniformly continuous functions to metric.v
EvgenyMakarov
committed

Commits on Oct 4, 2012

Proving approximation by Riemann sums in AbstractIntegration
EvgenyMakarov
committed

Commits on Oct 9, 2012

Proving Riemann approximation
EvgenyMakarov
committed

Commits on Oct 19, 2012

Proved completeness of the metric space of uniformly continuous functions. Started proving completeness of a closed ball.
EvgenyMakarov
committed

Commits on Oct 23, 2012

Proving corollaries of Riemann approximation
EvgenyMakarov
committed

Commits on Oct 26, 2012

Proved that a closed ball in a complete metric space is a complete metric subspace (FromMetric2.v)
EvgenyMakarov
committed

Commits on Oct 29, 2012

Moved lemmas about Q and Z into corresponding files
EvgenyMakarov
committed

Commits on Oct 30, 2012

Commits on Oct 31, 2012

Proving properties of Riemann sums
EvgenyMakarov
committed

Commits on Nov 1, 2012

Proved that uniformly continuous functions from R to R are determined by their values on rational numbers
EvgenyMakarov
committed

Commits on Nov 2, 2012

Proving that the sum of two integrable functions is integrable
EvgenyMakarov
committed

Commits on Nov 5, 2012

Update math-classes submodule.
EvgenyMakarov
committed

Commits on Nov 6, 2012

Proved that the sum of two locally uniformly continuous integrable functions is integrable
EvgenyMakarov
committed

Commits on Nov 7, 2012

Started adapting SimpleIntegration.v to metric.v instead of Classified.v
EvgenyMakarov
committed

Commits on Nov 8, 2012

Adapting SimpleIntegration.v to metric.v instead of Classified.v
EvgenyMakarov
committed

Commits on Nov 9, 2012

Finished adapting SimpleIntegration.v
EvgenyMakarov
committed

Commits on Nov 30, 2012

Defined Lipschitz and expressed Contraction through it
EvgenyMakarov
committed

Commits on Dec 4, 2012

Commits on Dec 5, 2012

Proving that integral of locally Lipschitz functions is locally Lipschitz
EvgenyMakarov
committed

Commits on Dec 7, 2012

Proving that integral is Lipschitz
EvgenyMakarov
committed

Commits on Dec 10, 2012

Proving that integral is Lipschitz
EvgenyMakarov
committed

Commits on Dec 11, 2012

Proved that the integral of a locally Lipschitz function is locally Lipschitz
EvgenyMakarov
committed

Commits on Dec 17, 2012

Commits on Dec 18, 2012

Commits on Dec 21, 2012

Picard iterations
EvgenyMakarov
committed

Commits on Dec 24, 2012

Defined product metric space with supremum norm
EvgenyMakarov
committed

Commits on Dec 27, 2012

Proved that the composition if uniformly continuous functions is uniformly continuous
EvgenyMakarov
committed

Commits on Dec 29, 2012

Ran 'git add math-classes'
EvgenyMakarov
committed

Commits on Jan 1, 2013

Changed Map to Func
EvgenyMakarov
committed

Commits on Jan 16, 2013

Started defining Picard operator
EvgenyMakarov
committed

Commits on Jan 17, 2013

Moved the new code about Picard iterations into Picard.v
EvgenyMakarov
committed

Commits on Jan 18, 2013

Started proving that the function to which Picard operator is applied is Lipschitz
EvgenyMakarov
committed

Commits on Jan 22, 2013

.
EvgenyMakarov
committed

Commits on Jan 24, 2013

Proved some facts about Lipschitz functions
EvgenyMakarov
committed

Commits on Jan 25, 2013

Changed type class arguments of some functions and theorems (e.g., diag_lip and compose_lip) to avoid requiring MetricSpaceClass when not necessary. Now they require MetricSpaceBall or ExtMetricSpa…
EvgenyMakarov
committed

Commits on Jan 29, 2013

Commits on Jan 30, 2013

Proving that extend is Lipschitz
EvgenyMakarov
committed

Commits on Jan 31, 2013

Proved that extension of a Lipschitz function is Lipschitz
EvgenyMakarov
committed

Commits on Feb 2, 2013

Proved that the result of the Picard operators is Lipschitz
EvgenyMakarov
committed

Commits on Feb 4, 2013

Proved that the image of the image of the Picard operator lies in the required segment
EvgenyMakarov
committed

Commits on Feb 5, 2013

.
EvgenyMakarov
committed

Commits on Feb 7, 2013

Commits on Feb 11, 2013

Made BanachFixpoint.v compile
EvgenyMakarov
committed

Commits on Feb 12, 2013

.
EvgenyMakarov
committed

Commits on Feb 13, 2013

.
EvgenyMakarov
committed

Commits on Feb 14, 2013

.
EvgenyMakarov
committed

Commits on Feb 16, 2013

Commits on Feb 17, 2013

Proved that Picard operator is a contraction
EvgenyMakarov
committed

Commits on Feb 18, 2013

Proved that Picard operator has a fixpoint
EvgenyMakarov
committed

Commits on Feb 22, 2013

Proved some lemmas
EvgenyMakarov
committed

Commits on Feb 26, 2013

.
EvgenyMakarov
committed

Commits on Mar 20, 2013

Proved that unformly continuous functions are closed under addition and negation
EvgenyMakarov
committed

Commits on Apr 2, 2013

Proved several lemmas
EvgenyMakarov
committed

Commits on Apr 5, 2013

Proved all lemmas outside of Picard.v
EvgenyMakarov
committed

Commits on Apr 16, 2013

Made AbstractIntegration.v require SimpleIntegration.v instead of the other way around. SimpleIntegration.v defines integral for uniformly comtinuous functions; AbstractIntegration.v proves propert…
EvgenyMakarov
committed

Commits on Apr 19, 2013

Proved that the integral of a sum equals the sum of integrals
EvgenyMakarov
committed

Commits on Apr 20, 2013

Proved lemmas needed for computational example
EvgenyMakarov
committed

Commits on Apr 22, 2013

Did computational experiments
EvgenyMakarov
committed

Commits on Apr 28, 2013

Removed all admit's. Proved that Picard iterations converge to the solution of an integral equation.
EvgenyMakarov
committed

Commits on May 10, 2013

Commented out computations that take too long in Picard.v
EvgenyMakarov
committed

Commits on Jul 1, 2013

merging
Bas Spitters
committed

Commits on Apr 3, 2014

Updating the math-classes submodule
Bas Spitters
committed
Now works ith 8.4pl4
Bas Spitters
committed

Commits on Apr 4, 2014

Updating description
Bas Spitters
committed

Commits on May 23, 2014

Small changes in example
Bas Spitters
committed

Commits on Jun 2, 2014

Removing html files here, as they are now on:
Bas Spitters
committed

Commits on Aug 25, 2014

Adding .aux .native
spitters
committed

Commits on Aug 26, 2014

Commits on Aug 27, 2014

In the process of making compile with trunk
spitters
committed

Commits on Aug 29, 2014

Making compile with trunk
spitters
committed

Commits on Sep 1, 2014

Commits on Sep 2, 2014

Commits on Sep 18, 2014

Commits on Sep 25, 2014