Hi,
> 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
