Hi Chun,
Great work!!! I briefly went through the proof script and looks good to me.
However, there are few things that need be discussed before this PR that
are as follows:
1) The current version of the measure theory, which is still part of
HOL-sources, is formalized by taking a real-valued 'measure': ('a -> bool)
-> real ... whereas, you're working on the version having extreal-valued
'measure': ('a -> bool) -> extreal ... Do you have any plan to keep the
previous version?
2) My suggestion is to place the real-valued 'measure' theory somewhere in
HOL/examples and continue further development on extreal-valued 'measure'
theory.
3) I've also further extended the Qasim's measure theory by porting more
necessary defs/thms from Isabelle. I'd like to make them part of future
measure theory PRs.. Let me know if you have any suggestions regarding it...
Feel free to share your thoughts...
On Fri, Jan 4, 2019 at 11:01 AM Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> Hi all,
>
> after 4 months’ hard work (mostly using my spare time), among other
> things, finally I have (re)proved Carathéodory's extension theorem [6]
> under the new [0, +Inf] measure theory (from HVG [5]). This is the most
> general version based on semi-ring, also with uniqueness arguments:
>
> [CARATHEODORY_SEMIRING] Theorem
>
> ⊢ ∀m0.
> semiring (m_space m0,measurable_sets m0) ∧ premeasure m0 ⇒
> ∃m.
> measure_space 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)) ∧
> (sigma_finite m0 ⇒
> ∀m'.
> measure_space m' ∧ (m_space m' = m_space m) ∧
> (measurable_sets m' = measurable_sets m) ∧
> (∀s.
> s ∈ measurable_sets m0 ⇒
> (measure m' s = measure m0 s)) ⇒
> ∀s.
> s ∈ measurable_sets m' ⇒
> (measure m' s = measure m s))
>
> The original CARATHEODORY (back to Joe Hurd [1] and A. R. Coble [2]) now
> becomes an easy corollary (as any algebra is also semiring):
>
> [CARATHEODORY] Theorem
>
> ⊢ ∀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
>
> The new “src/probability/measureScript.sml” [3] (7737 lines), starting
> from line 3783 were all newly written by me. The formal proof of
> CARATHEODORY_SEMIRING strictly follows a newer textbook [4, p.38-43] with
> all gaps filled and small mistakes corrected. This single proof has 1600+
> lines of code...
>
> Before sending this huge PR to HOL official, I still need to merge a few
> other changes from HVG’s version into “src/probability/lebesgueScript.sml”
> and "“src/probability/probabilityScript.sml”, to make sure the PR doesn’t
> remove any existing theorem in these scripts. I also need to fix
> “examples/miller” under the new [0, +inf] measure theory as it needs
> CARATHEODORY to construct the discrete probability measure.
>
> Comments and suggestions are welcome.
>
> Regards,
>
> Chun Tian
> FBK and University of Trento, Italy
>
> [1] Hurd, J.: Formal verification of probabilistic algorithms. (2001).
> [2] Coble, A.R.: Anonymity, information, and machine-assisted proof,
> (2010).
> [3]
> https://github.com/binghe/HOL/blob/Probability-6/src/probability/measureScript.sml
> [4] Schilling, R.L.: Measures, Integrals and Martingales. Cambridge
> University Press (2005).
> [5] http://hvg.ece.concordia.ca/code/hol/DFT/index.php
> [6] https://en.wikipedia.org/wiki/Carathéodory%27s_extension_theorem
> <https://en.wikipedia.org/wiki/Carath%C3%A9odory%27s_extension_theorem>
>
> > Il giorno 11 ago 2018, alle ore 19:29, Waqar Ahmad <
> 12phdwah...@seecs.edu.pk> ha scritto:
> >
> > 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.
> >
> >
> >
> > --
> > 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/
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
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/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
