![[Jenkins]](/jenkins/static/51af4dc4/images/svgs/logo.svg){kind=logo}
Summary
- rename HOL-Multivariate_Analysis to HOL-Analysis.
- move measure theory from HOL-Probability to HOL-Multivariate_Analysis
| The file was added | src/HOL/Analysis/Analysis.thy |
| The file was added | src/HOL/Analysis/Binary_Product_Measure.thy |
| The file was added | src/HOL/Analysis/Bochner_Integration.thy |
| The file was added | src/HOL/Analysis/Borel_Space.thy |
| The file was added | src/HOL/Analysis/Bounded_Continuous_Function.thy |
| The file was added | src/HOL/Analysis/Bounded_Linear_Function.thy |
| The file was added | src/HOL/Analysis/Brouwer_Fixpoint.thy |
| The file was added | src/HOL/Analysis/Caratheodory.thy |
| The file was added | src/HOL/Analysis/Cartesian_Euclidean_Space.thy |
| The file was added | src/HOL/Analysis/Cauchy_Integral_Theorem.thy |
| The file was added | src/HOL/Analysis/Complete_Measure.thy |
| The file was added | src/HOL/Analysis/Complex_Analysis_Basics.thy |
| The file was added | src/HOL/Analysis/Complex_Transcendental.thy |
| The file was added | src/HOL/Analysis/Conformal_Mappings.thy |
| The file was added | src/HOL/Analysis/Continuous_Extension.thy |
| The file was added | src/HOL/Analysis/Convex_Euclidean_Space.thy |
| The file was added | src/HOL/Analysis/Derivative.thy |
| The file was added | src/HOL/Analysis/Determinants.thy |
| The file was added | src/HOL/Analysis/Embed_Measure.thy |
| The file was added | src/HOL/Analysis/Euclidean_Space.thy |
| The file was added | src/HOL/Analysis/Extended_Real_Limits.thy |
| The file was added | src/HOL/Analysis/Fashoda_Theorem.thy |
| The file was added | src/HOL/Analysis/Finite_Cartesian_Product.thy |
| The file was added | src/HOL/Analysis/Finite_Product_Measure.thy |
| The file was added | src/HOL/Analysis/Gamma_Function.thy |
| The file was added | src/HOL/Analysis/Generalised_Binomial_Theorem.thy |
| The file was added | src/HOL/Analysis/Harmonic_Numbers.thy |
| The file was added | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy |
| The file was added | src/HOL/Analysis/Homeomorphism.thy |
| The file was added | src/HOL/Analysis/Integral_Test.thy |
| The file was added | src/HOL/Analysis/Interval_Integral.thy |
| The file was added | src/HOL/Analysis/L2_Norm.thy |
| The file was added | src/HOL/Analysis/Lebesgue_Integral_Substitution.thy |
| The file was added | src/HOL/Analysis/Lebesgue_Measure.thy |
| The file was added | src/HOL/Analysis/Linear_Algebra.thy |
| The file was added | src/HOL/Analysis/Measurable.thy |
| The file was added | src/HOL/Analysis/Measure_Space.thy |
| The file was added | src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy |
| The file was added | src/HOL/Analysis/Norm_Arith.thy |
| The file was added | src/HOL/Analysis/Operator_Norm.thy |
| The file was added | src/HOL/Analysis/Ordered_Euclidean_Space.thy |
| The file was added | src/HOL/Analysis/Path_Connected.thy |
| The file was added | src/HOL/Analysis/Poly_Roots.thy |
| The file was added | src/HOL/Analysis/Polytope.thy |
| The file was added | src/HOL/Analysis/Radon_Nikodym.thy |
| The file was added | src/HOL/Analysis/Regularity.thy |
| The file was added | src/HOL/Analysis/Set_Integral.thy |
| The file was added | src/HOL/Analysis/Sigma_Algebra.thy |
| The file was added | src/HOL/Analysis/Summation_Tests.thy |
| The file was added | src/HOL/Analysis/Topology_Euclidean_Space.thy |
| The file was added | src/HOL/Analysis/Uniform_Limit.thy |
| The file was added | src/HOL/Analysis/Weierstrass_Theorems.thy |
| The file was added | src/HOL/Analysis/document/root.tex |
| The file was added | src/HOL/Analysis/ex/Approximations.thy |
| The file was added | src/HOL/Analysis/measurable.ML |
| The file was added | src/HOL/Analysis/normarith.ML |
| The file was modified | NEWS (diff) |
| The file was modified | src/HOL/Deriv.thy (diff) |
| The file was modified | src/HOL/Library/Extended_Real.thy (diff) |
| The file was modified | src/HOL/Probability/Discrete_Topology.thy (diff) |
| The file was modified | src/HOL/Probability/Probability_Measure.thy (diff) |
| The file was modified | src/HOL/ROOT (diff) |
| The file was modified | src/HOL/ex/Gauge_Integration.thy (diff) |
| The file was removed | src/HOL/Multivariate_Analysis/Binary_Product_Measure.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Bochner_Integration.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Borel_Space.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Caratheodory.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Cauchy_Integral_Theorem.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Complete_Measure.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Complex_Transcendental.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Conformal_Mappings.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Continuous_Extension.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Derivative.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Determinants.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Embed_Measure.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Euclidean_Space.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Fashoda_Theorem.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Finite_Product_Measure.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Gamma_Function.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Henstock_Kurzweil_Integration.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Homeomorphism.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Integral_Test.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Interval_Integral.thy |
| The file was removed | src/HOL/Multivariate_Analysis/L2_Norm.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Lebesgue_Integral_Substitution.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Lebesgue_Measure.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Linear_Algebra.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Measurable.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Measure_Space.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Nonnegative_Lebesgue_Integration.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Norm_Arith.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Operator_Norm.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Path_Connected.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Poly_Roots.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Polytope.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Radon_Nikodym.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Regularity.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Set_Integral.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Sigma_Algebra.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Summation_Tests.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Uniform_Limit.thy |
| The file was removed | src/HOL/Multivariate_Analysis/Weierstrass_Theorems.thy |
| The file was removed | src/HOL/Multivariate_Analysis/document/root.tex |
| The file was removed | src/HOL/Multivariate_Analysis/ex/Approximations.thy |
| The file was removed | src/HOL/Multivariate_Analysis/measurable.ML |
| The file was removed | src/HOL/Multivariate_Analysis/normarith.ML |
| The file was added | src/HOL/Multivariate_Analysis/Binary_Product_Measure.thy |
| The file was added | src/HOL/Multivariate_Analysis/Bochner_Integration.thy |
| The file was added | src/HOL/Multivariate_Analysis/Borel_Space.thy |
| The file was added | src/HOL/Multivariate_Analysis/Caratheodory.thy |
| The file was added | src/HOL/Multivariate_Analysis/Complete_Measure.thy |
| The file was added | src/HOL/Multivariate_Analysis/Embed_Measure.thy |
| The file was added | src/HOL/Multivariate_Analysis/Finite_Product_Measure.thy |
| The file was added | src/HOL/Multivariate_Analysis/Interval_Integral.thy |
| The file was added | src/HOL/Multivariate_Analysis/Lebesgue_Integral_Substitution.thy |
| The file was added | src/HOL/Multivariate_Analysis/Lebesgue_Measure.thy |
| The file was added | src/HOL/Multivariate_Analysis/Measurable.thy |
| The file was added | src/HOL/Multivariate_Analysis/Measure_Space.thy |
| The file was added | src/HOL/Multivariate_Analysis/Nonnegative_Lebesgue_Integration.thy |
| The file was added | src/HOL/Multivariate_Analysis/Radon_Nikodym.thy |
| The file was added | src/HOL/Multivariate_Analysis/Regularity.thy |
| The file was added | src/HOL/Multivariate_Analysis/Set_Integral.thy |
| The file was added | src/HOL/Multivariate_Analysis/Sigma_Algebra.thy |
| The file was added | src/HOL/Multivariate_Analysis/measurable.ML |
| The file was modified | src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy (diff) |
| The file was modified | src/HOL/Probability/Characteristic_Functions.thy (diff) |
| The file was modified | src/HOL/Probability/Giry_Monad.thy (diff) |
| The file was modified | src/HOL/Probability/Independent_Family.thy (diff) |
| The file was modified | src/HOL/Probability/Infinite_Product_Measure.thy (diff) |
| The file was modified | src/HOL/Probability/Information.thy (diff) |
| The file was modified | src/HOL/Probability/Probability.thy (diff) |
| The file was modified | src/HOL/Probability/Probability_Measure.thy (diff) |
| The file was modified | src/HOL/Probability/Projective_Family.thy (diff) |
| The file was modified | src/HOL/Probability/Projective_Limit.thy (diff) |
| The file was modified | src/HOL/Probability/SPMF.thy (diff) |
| The file was removed | src/HOL/Probability/Binary_Product_Measure.thy |
| The file was removed | src/HOL/Probability/Bochner_Integration.thy |
| The file was removed | src/HOL/Probability/Borel_Space.thy |
| The file was removed | src/HOL/Probability/Caratheodory.thy |
| The file was removed | src/HOL/Probability/Complete_Measure.thy |
| The file was removed | src/HOL/Probability/Embed_Measure.thy |
| The file was removed | src/HOL/Probability/Finite_Product_Measure.thy |
| The file was removed | src/HOL/Probability/Interval_Integral.thy |
| The file was removed | src/HOL/Probability/Lebesgue_Integral_Substitution.thy |
| The file was removed | src/HOL/Probability/Lebesgue_Measure.thy |
| The file was removed | src/HOL/Probability/Measurable.thy |
| The file was removed | src/HOL/Probability/Measure_Space.thy |
| The file was removed | src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy |
| The file was removed | src/HOL/Probability/Radon_Nikodym.thy |
| The file was removed | src/HOL/Probability/Regularity.thy |
| The file was removed | src/HOL/Probability/Set_Integral.thy |
| The file was removed | src/HOL/Probability/Sigma_Algebra.thy |
| The file was removed | src/HOL/Probability/measurable.ML |