| author | immler |
| Mon, 26 Feb 2018 09:58:47 +0100 | |
| changeset 67728 | d97a28a006f9 |
| parent 67727 | ce3e87a51488 |
| child 67996 | 6a9d1b31a7c5 |
| 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 |
Lebesgue_Integral_Substitution |
|
66296
33a47f2d9edc
New theory of Equiintegrability / Continuity of the indefinite integral / improper integration
paulson <lp15@cam.ac.uk>
parents:
66277
diff
changeset
|
4 |
Improper_Integral |
|
63626
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 |
|
64289
42f28160bad9
HOL-Analysis: move Function Topology from AFP/Ergodict_Theory; HOL-Probability: move Essential Supremum from AFP/Lp
hoelzl
parents:
64006
diff
changeset
|
12 |
Function_Topology |
|
66277
512b0dc09061
HOL-Analysis: Infinite products
eberlm <eberlm@in.tum.de>
parents:
65040
diff
changeset
|
13 |
Infinite_Products |
|
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
66296
diff
changeset
|
14 |
Infinite_Set_Sum |
|
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
15 |
Weierstrass_Theorems |
|
63078
e49dc94eb624
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset
|
16 |
Polytope |
| 64846 | 17 |
Jordan_Curve |
|
65039
87972e6177bc
New theory about Winding Numbers
paulson <lp15@cam.ac.uk>
parents:
64846
diff
changeset
|
18 |
Winding_Numbers |
|
66826
0d60d2118544
Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.
paulson <lp15@cam.ac.uk>
parents:
66480
diff
changeset
|
19 |
Riemann_Mapping |
|
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
20 |
Poly_Roots |
|
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62049
diff
changeset
|
21 |
Conformal_Mappings |
|
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
66296
diff
changeset
|
22 |
FPS_Convergence |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61518
diff
changeset
|
23 |
Generalised_Binomial_Theorem |
|
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
24 |
Gamma_Function |
|
67278
c60e3d615b8c
Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
eberlm <eberlm@in.tum.de>
parents:
66826
diff
changeset
|
25 |
Ball_Volume |
|
67727
ce3e87a51488
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
immler
parents:
67278
diff
changeset
|
26 |
Lipschitz |
| 33175 | 27 |
begin |
28 |
||
29 |
end |