Session HOL-Multivariate_Analysis

Theories

• Indicator_Function
• Old_Datatype
• Nat_Bijection
• Countable
• Infinite_Set
• Countable_Set
• FuncSet
• L2_Norm
• Inner_Product
• Product_plus
• Product_Vector
• Euclidean_Space
• Linear_Algebra
• Sum_of_Squares
• Norm_Arith
• Topology_Euclidean_Space
• Convex
• Set_Algebras
• Convex_Euclidean_Space
• Path_Connected
• Brouwer_Fixpoint
• Phantom_Type
• Cardinality
• Numeral_Type
• Finite_Cartesian_Product
• Operator_Norm
• Countable_Complete_Lattices
• Order_Continuity
• Extended_Nat
• Liminf_Limsup
• Extended_Real
• Summation
• Uniform_Limit
• Bounded_Linear_Function
• Derivative
• Integration
• Cartesian_Euclidean_Space
• Fashoda
• Extended_Nonnegative_Real
• Extended_Real_Limits
• Permutations
• Determinants
• Product_Order
• Ordered_Euclidean_Space
• Bounded_Continuous_Function
• Weierstrass
• Nonpos_Ints
• Complex_Analysis_Basics
• Complex_Transcendental
• Cauchy_Integral_Thm
• Conformal_Mappings
• Generalised_Binomial_Theorem
• Integral_Test
• Harmonic_Numbers
• Periodic_Fun
• Gamma
• Multivariate_Analysis
• PolyRoots