[isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis
Johannes Hölzl
hoelzl at in.tum.de
Mon Aug 8 15:45:31 CEST 2016
* 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
More information about the isabelle-dev
mailing list