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
> 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/
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
