Session HOL-Analysis

Theories

• L2_Norm
• Inner_Product
• HOL-Library.Product_Plus
• Product_Vector
• Euclidean_Space
• HOL-Library.Infinite_Set
• Linear_Algebra
• Affine
• HOL-Library.Set_Algebras
• HOL-Library.FuncSet
• Convex
• HOL-Library.Cancellation
  • File ‹Cancellation/cancel.ML›
  • File ‹Cancellation/cancel_data.ML›
  • File ‹Cancellation/cancel_simprocs.ML›
• HOL-Library.Multiset
  • File ‹multiset_simprocs.ML›
• HOL-Library.Disjoint_Sets
• HOL-Combinatorics.Transposition
• HOL-Combinatorics.Permutations
• HOL-Library.Phantom_Type
• HOL-Library.Cardinality
• HOL-Library.Numeral_Type
• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• HOL-Library.Nat_Bijection
• HOL-Library.Countable
  • File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
• HOL-Library.Countable_Set
• Finite_Cartesian_Product
• Cartesian_Space
• Determinants
• HOL-Library.Set_Idioms
• Abstract_Topology
• FSigma
• Sum_Topology
• Elementary_Topology
• Abstract_Limits
• Continuum_Not_Denumerable
• HOL-Library.Indicator_Function
• HOL-Library.Equipollence
• Abstract_Topology_2
• Connected
• Function_Topology
• Product_Topology
• T1_Spaces
• Lindelof_Spaces
• Metric_Arith
  • File ‹metric_arith.ML›
• Elementary_Metric_Spaces
• Elementary_Normed_Spaces
• HOL-Library.Sum_of_Squares
  • File ‹Sum_of_Squares/positivstellensatz.ML›
  • File ‹Sum_of_Squares/positivstellensatz_tools.ML›
  • File ‹Sum_of_Squares/sum_of_squares.ML›
  • File ‹Sum_of_Squares/sos_wrapper.ML›
• Norm_Arith
  • File ‹normarith.ML›
• Topology_Euclidean_Space
• Line_Segment
• Convex_Euclidean_Space
• Starlike
• Path_Connected
• Locally
• Uncountable_Sets
• Homotopy
• Abstract_Euclidean_Space
• Abstract_Topological_Spaces
• Abstract_Metric_Spaces
• HOL-Library.Countable_Complete_Lattices
• HOL-Library.Order_Continuity
• HOL-Library.Extended_Nat
• HOL-Library.Liminf_Limsup
• HOL-Library.Extended_Real
• HOL-Library.Extended_Nonnegative_Real
• HOL-Library.Complex_Order
• Infinite_Sum
• HOL-Library.Product_Order
• Ordered_Euclidean_Space
• HOL-Computational_Algebra.Factorial_Ring
• HOL-Computational_Algebra.Euclidean_Algorithm
• HOL-Computational_Algebra.Primes
• Arcwise_Connected
• Urysohn
• Isolated
• Sparse_In
• Operator_Norm
• HOL-Library.Discrete
• Extended_Real_Limits
• Summation_Tests
• Uniform_Limit
• Bounded_Linear_Function
• Derivative
• Cartesian_Euclidean_Space
• HOL-Library.Nonpos_Ints
• Complex_Analysis_Basics
• HOL-Library.Periodic_Fun
• Complex_Transcendental
• Sigma_Algebra
• Measurable
  • File ‹measurable.ML›
• Measure_Space
• Borel_Space
• Nonnegative_Lebesgue_Integration
• Binary_Product_Measure
• Finite_Product_Measure
• Caratheodory
• Bochner_Integration
• Complete_Measure
• Regularity
• Lebesgue_Measure
• Tagged_Division
• Henstock_Kurzweil_Integration
• HOL-Library.BNF_Corec
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML›
  • File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML›
• HOL-Library.Landau_Symbols
• HOL-Real_Asymp.Lazy_Eval
  • File ‹lazy_eval.ML›
• HOL-Real_Asymp.Inst_Existentials
  • File ‹inst_existentials.ML›
• HOL-Real_Asymp.Eventuallize
• HOL-Real_Asymp.Multiseries_Expansion
  • File ‹asymptotic_basis.ML›
  • File ‹exp_log_expression.ML›
  • File ‹expansion_interface.ML›
  • File ‹multiseries_expansion.ML›
  • File ‹real_asymp.ML›
• HOL-Real_Asymp.Multiseries_Expansion_Bounds
  • File ‹multiseries_expansion_bounds.ML›
• HOL-Real_Asymp.Real_Asymp
  • File ‹real_asymp_diag.ML›
• Kronecker_Approximation_Theorem
• Weierstrass_Theorems
• Radon_Nikodym
• Set_Integral
• Homeomorphism
• Equivalence_Lebesgue_Henstock_Integration
• Harmonic_Numbers
• Gamma_Function
• Interval_Integral
• Lebesgue_Integral_Substitution
• Ball_Volume
• Integral_Test
• Improper_Integral
• Continuous_Extension
• Equivalence_Measurable_On_Borel
• Embed_Measure
• Brouwer_Fixpoint
• Fashoda_Theorem
• Cross3
• Bounded_Continuous_Function
• Infinite_Products
• Infinite_Set_Sum
• Polytope
• Retracts
• Further_Topology
• Jordan_Curve
• Poly_Roots
• Generalised_Binomial_Theorem
• Vitali_Covering_Theorem
• Change_Of_Vars
• Lipschitz
• Multivariate_Analysis
• Simplex_Content
• HOL-Computational_Algebra.Formal_Power_Series
• FPS_Convergence
• Smooth_Paths
• Function_Metric
• Analysis