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.
—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
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
