Hi,

## Advertising

> I have a question about the new version of measureTheory > (measure_hvgScript.sml): why the Carathéodory's extension theorem > (CARATHEODORY), with all related definitions and lemmas, are removed? > > [CARATHEODORY] > |- ∀m0. > algebra (m_space m0,measurable_sets m0) ∧ positive m0 ∧ > countably_additive m0 ⇒ > ∃m. > (∀s. s ∈ measurable_sets m0 ⇒ (measure m s = measure m0 > s)) ∧ > ((m_space m,measurable_sets m) = > sigma (m_space m0) (measurable_sets m0)) ∧ measure_space m > > This is a fundamental result in measure theory. It is one way of arriving > at the concept of Lebesgue measure. Without it, how did you manage to > define the Lebesgue measure on all Borel sets? (sorry, I’ve lost in the > long lebesgue_measure_hvgScript.sml to find out by myself) > > P. S. If the goal is to just merge the latest version of measureTheory > into HOL4, we cannot loose CARATHEODORY, as it’s needed by other work > (e.g.. HOL’s "examples/miller/prob/probScript.sml”). I’m trying to fix its > old proofs using under the new extrealTheory, it seems that each proof is a > bit harder to prove, but essentially there’s no difficulty at al, > CARATHEODORY must still hold. > > I'm not sure why the original authors removed CARATHEODORY properties in measure_hvg.sml (maybe its not needed at that time). However, Lebesgue measure (in lebesgue_measure_hvgScript.sml) is formalized using Gauge integral that has been ported from HOL-Light (Multivariate Calculus formalized by J. Horrison). You can find the details of this project from this link http://hvg.ece.concordia.ca/projects/prob-it/pr7.html Let me know if you need any help regarding it. > —Chun > > > Il giorno 10 ago 2018, alle ore 00:20, Waqar Ahmad < > 12phdwah...@seecs.edu.pk> ha scritto: > > > > Hi, > > > > I appreciate the changes that you are making but I'm still not sure that > why are you re-proving the existing properties that are present in the > latest version [1]. For instance, EXTREAL_SUM_IMAGE_INSERT is already > existed in [1] in different forms: > > > > extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY (THEOREM) > > ------------------------------------------------------ > > |- !f s. > > FINITE s ==> > > !e. > > (!x. x IN e INSERT s ==> f x <> NegInf) \/ > > (!x. x IN e INSERT s ==> f x <> PosInf) ==> > > (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e)) > > > > > > extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY_NEG (THEOREM) > > ---------------------------------------------------------- > > |- !f s. > > FINITE s ==> > > !e. > > (!x. x IN e INSERT s ==> f x <> NegInf) ==> > > (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e)) > > > > > > extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY_POS (THEOREM) > > ---------------------------------------------------------- > > |- !f s. > > FINITE s ==> > > !e. > > (!x. x IN e INSERT s ==> f x <> PosInf) ==> > > (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e)) > > > > You can simply merge the latest extrealTheory (extreal_hvgTheory) with > the HOL sources and that will be it? > > > > > > [1] http://hvg.ece.concordia.ca/code/hol/DFT/index.php > > > > -- Waqar Ahmad, Ph.D. Post Doc at Hardware Verification Group (HVG) Department of Electrical and Computer Engineering Concordia University, QC, Canada Web: http://save.seecs.nust.edu.pk/waqar-ahmad/

------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot

_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info