| Bernstein
| Formalization of an efficient representation of multivariate Bernstein polynomials. Includes strategies
and the tool Grizzly for solving global optimization problems.
| details |
|
|---|
| complex§
| Complex numbers
| details |
|
|---|
| complex_alt§
| Alternative version of complex numbers
| details |
|
|---|
| complex_integration§
| Complex integration
| details |
|
|---|
| co_structures§
| Sequences of countable length defined as coalgebra datatypes
| details |
|
|---|
| digraphs
| Directed graphs: circuits, maximal subtrees, paths, dags
| details |
|
|---|
| exact_real_arith§
| Exact real arithmetic including trig functions
| details |
|
|---|
| extended_nnreal§
| Extended non-negative reals
| details |
|
|---|
| fault_tolerance§
| Fault tolerance protocols
| details |
|
|---|
| float§
| Floating point numbers and arithmetic
| details |
|
|---|
| graphs
| Graph theory: connectedness, walks, trees, Menger's Theorem
| details |
|
|---|
| group
| Group theory | details |
|
|---|
| ints
| Integer division, gcd, mod, prime factorization, min, max
| details |
|
|---|
| interval_arith
| Interval arithmetic and numerical approximations
|
details |
|
|---|
| lebesgue§
| Lebesgue integral with connection to Riemann Integral
| details |
|
|---|
| linear_algebra§
| Linear algebra
| details |
|
|---|
| lnexp§
| Logarithm, exponential and hyperbolic functions
| details |
|
|---|
| lnexp_fnd§
| Foundational definitions of logarithm, exponential and hyperbolic functions
| details |
|
|---|
| measure_integration§
| Sigma algebras, measures, Fubini-Tonelli Lemmas
| details |
|
|---|
| metric_space§
| Domains with a distance metric, continuity and uniform continuity
| details |
|
|---|
| numbers§
| Elementary number theory
| details |
|
|---|
| orders§
| abstract orders, lattices, fixedpoints
| details |
|
|---|
| power§
| Generalized Power function (without ln/exp)
| details |
|
|---|
| probability§
| Probability theory
| details |
|
|---|
| reals§
| Summations, sup, inf, sqrt over the reals, abs lemmas
| details |
|
|---|
| scott§
| Scott topology
| details |
|
|---|
| series§
| Power series, comparison test, ratio test, Taylor's theorem
| details |
|
|---|
| sets_aux
| Powersets, orders, cardinality over infinite sets
| details |
|
|---|
| sigma_set§
| Summations over countably infinite sets
| details |
|
|---|
| structures§
| Bounded arrays, finite sequences and bags
| details |
|
|---|
| topology§
| Continuity, homeomorphisms, connected and compact spaces,
Borel sets/functions
| details |
|
|---|
| trig§
| Trigonometry: definitions, identities, approximations
| details |
|
|---|
| trig_fnd§
| Foundational development of trigonometry: proofs of trig axioms
| details |
|
|---|
| TRS§
| Term rewrite systems and Robinson unification algorithm
| details |
|
|---|
| TU_games§
| Cooperative TU-games
| details |
|
|---|
| vect_analysis§
| Limits, continuity, and derivatives of vector functions
| details |
|
|---|
| vectors§
| Basic properties of vectors
| details |
|
|---|
| while§
| Semantics for the programming language "while"
| details |
|
|---|