author | Manuel Eberl <eberlm@in.tum.de> |
Sat, 30 Nov 2019 13:47:33 +0100 | |
changeset 71189 | 954ee5acaae0 |
parent 70694 | ae37b8fbf023 |
child 71191 | 6695aeae8ec9 |
permissions | -rw-r--r-- |
63627 | 1 |
theory Analysis |
69676 | 2 |
imports |
3 |
(* Linear Algebra *) |
|
4 |
Convex |
|
5 |
Determinants |
|
6 |
(* Topology *) |
|
7 |
Connected |
|
69874 | 8 |
Abstract_Limits |
69994
cf7150ab1075
more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.
paulson <lp15@cam.ac.uk>
parents:
69945
diff
changeset
|
9 |
Abstract_Euclidean_Space |
69676 | 10 |
(* Functional Analysis *) |
11 |
Elementary_Normed_Spaces |
|
12 |
Norm_Arith |
|
13 |
(* Vector Analysis *) |
|
14 |
Convex_Euclidean_Space |
|
15 |
(* Measure and Integration Theory *) |
|
16 |
Ball_Volume |
|
17 |
Integral_Test |
|
18 |
Improper_Integral |
|
70694
ae37b8fbf023
New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
paulson <lp15@cam.ac.uk>
parents:
70621
diff
changeset
|
19 |
Equivalence_Measurable_On_Borel |
69676 | 20 |
(* Unsorted *) |
63626
44ce6b524ff3
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
hoelzl
parents:
63594
diff
changeset
|
21 |
Lebesgue_Integral_Substitution |
44ce6b524ff3
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
hoelzl
parents:
63594
diff
changeset
|
22 |
Embed_Measure |
44ce6b524ff3
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
hoelzl
parents:
63594
diff
changeset
|
23 |
Complete_Measure |
44ce6b524ff3
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
hoelzl
parents:
63594
diff
changeset
|
24 |
Radon_Nikodym |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
25 |
Fashoda_Theorem |
59453
4736ff5a41d8
moved bcontfun from AFP/Ordinary_Differential_Equations
hoelzl
parents:
56370
diff
changeset
|
26 |
Determinants |
68465
e699ca8e22b7
New material in support of quaternions
paulson <lp15@cam.ac.uk>
parents:
68000
diff
changeset
|
27 |
Cross3 |
63129 | 28 |
Homeomorphism |
59453
4736ff5a41d8
moved bcontfun from AFP/Ordinary_Differential_Equations
hoelzl
parents:
56370
diff
changeset
|
29 |
Bounded_Continuous_Function |
69144
f13b82281715
new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
paulson <lp15@cam.ac.uk>
parents:
68625
diff
changeset
|
30 |
Abstract_Topology |
69922
4a9167f377b0
new material about topology, etc.; also fixes for yesterday's
paulson <lp15@cam.ac.uk>
parents:
69874
diff
changeset
|
31 |
Product_Topology |
70178
4900351361b0
Lindelöf spaces and supporting material
paulson <lp15@cam.ac.uk>
parents:
70089
diff
changeset
|
32 |
Lindelof_Spaces |
66277
512b0dc09061
HOL-Analysis: Infinite products
eberlm <eberlm@in.tum.de>
parents:
65040
diff
changeset
|
33 |
Infinite_Products |
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
66296
diff
changeset
|
34 |
Infinite_Set_Sum |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
35 |
Weierstrass_Theorems |
63078
e49dc94eb624
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
paulson <lp15@cam.ac.uk>
parents:
62408
diff
changeset
|
36 |
Polytope |
64846 | 37 |
Jordan_Curve |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
38 |
Poly_Roots |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61518
diff
changeset
|
39 |
Generalised_Binomial_Theorem |
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63129
diff
changeset
|
40 |
Gamma_Function |
68000
40b790c5a11d
Oops! Change_Of_Vars was not being imported to Analysis!
paulson <lp15@cam.ac.uk>
parents:
67996
diff
changeset
|
41 |
Change_Of_Vars |
70621
1afcfb7fdff4
entry point for analysis without integration theory
immler
parents:
70178
diff
changeset
|
42 |
Multivariate_Analysis |
68625
2ec84498f562
HOL-Analysis: Volume of a simplex, Heron's theorem
Manuel Eberl <eberlm@in.tum.de>
parents:
68465
diff
changeset
|
43 |
Simplex_Content |
71189
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
70694
diff
changeset
|
44 |
FPS_Convergence |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
70694
diff
changeset
|
45 |
Smooth_Paths |
33175 | 46 |
begin |
47 |
||
48 |
end |