* Renamed session HOL-Multivariate_Analysis to HOL-Analysis. * Moved measure theory from HOL-Probability to HOL-Analysis. When importing HOL-Analysis some theorems need additional name spaces prefixes due to name clashes. INCOMPATIBILITY.
The incompatibility is obviously due to the renaming, but we also have currently two integrals which share now some theorem names. The problem is that one integral does not subsume the other: * The /Bochner/ integral is defined on arbitrary measures, but restricted to be absolutely integrable, i.e. when a function is integrable than also its norm is integrable. * The /Henstock-Kurzweil/ integral is restricted to Euclidean spaces (and the Lebesgue measure on it), but it is not restricted to absolutely integrable functions. My idea would be to rename both integrals into something like: has_bc_integral, bc_integrable, bc_integral, has_hk_integral, hk_integrable, hk_integral and consequently rename the integral theorems. Currently the measure theory is based on the stuff in the former Multivariate_Analysis. My plan is to integrate it further down and then replace some old stuff by more generic definitions/proofs from measure theory. There are currently further restrictions where we are not sure how to solve them: * Dominated convergence is very general on the Bochner integral it works for integrals into Banach spaces, while for the HK integral it is currently only proven for Euclidean spaces. * We require dominated convergence to prove that both integrals are equal. Hence currently equality is only proven for Euclidean spaces. * FTC for the Bochner integral is derived from FTC for the HK integral. Hence FTC for the Bochner integral is only available for Euclidean spaces. - Johannes _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev