author | hoelzl |
Mon, 08 Aug 2016 14:13:14 +0200 | |
changeset 63627 | 6ddb43c6b711 |
parent 63626 | src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy@44ce6b524ff3 |
child 63968 | 4359400adfe7 |
permissions | -rw-r--r-- |
63627 | 1 |
theory Analysis |
59453
4736ff5a41d8
moved bcontfun from AFP/Ordinary_Differential_Equations
hoelzl
parents:
56370
diff
changeset
|
2 |
imports |
63626
44ce6b524ff3
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
hoelzl
parents:
63594
diff
changeset
|
3 |
Regularity |
44ce6b524ff3
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
hoelzl
parents:
63594
diff
changeset
|
4 |
Lebesgue_Integral_Substitution |
44ce6b524ff3
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
hoelzl
parents:
63594
diff
changeset
|
5 |
Embed_Measure |
44ce6b524ff3
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
hoelzl
parents:
63594
diff
changeset
|
6 |
Complete_Measure |
44ce6b524ff3
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
hoelzl
parents:
63594
diff
changeset
|
7 |
Radon_Nikodym |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
8 |
Fashoda_Theorem |
59453
4736ff5a41d8
moved bcontfun from AFP/Ordinary_Differential_Equations
hoelzl
parents:
56370
diff
changeset
|
9 |
Determinants |
63129 | 10 |
Homeomorphism |
59453
4736ff5a41d8
moved bcontfun from AFP/Ordinary_Differential_Equations
hoelzl
parents:
56370
diff
changeset
|
11 |
Bounded_Continuous_Function |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
12 |
Weierstrass_Theorems |
63078
e49dc94eb624
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset
|
13 |
Polytope |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
14 |
Poly_Roots |
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62049
diff
changeset
|
15 |
Conformal_Mappings |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61518
diff
changeset
|
16 |
Generalised_Binomial_Theorem |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
17 |
Gamma_Function |
33175 | 18 |
begin |
19 |
||
20 |
end |