[isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

[Johannes Hölzl]

* 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