The way that measurability of subtraction on ereals is proven in
Isabelle strongly suggests to me that it does not depend on any
particular choice of what ∞ - ∞ and -∞ - (-∞) are. I quickly checked it
by defining my own ereals and leaving it undefined, and all those proofs
still work fine.
In case you are interested in /how/ this is proven in Isabelle: You take
the following lemma:
lemma borel_measurable_ereal2:
fixes f g :: "'a ⇒ ereal"
assumes f: "f ∈ borel_measurable M"
assumes g: "g ∈ borel_measurable M"
assumes H: "(λx. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal
(g x)))) ∈ borel_measurable M"
"(λx. H (-∞) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M"
"(λx. H (∞) (ereal (real_of_ereal (g x)))) ∈ borel_measurable M"
"(λx. H (ereal (real_of_ereal (f x))) (-∞)) ∈ borel_measurable M"
"(λx. H (ereal (real_of_ereal (f x))) (∞)) ∈ borel_measurable M"
shows "(λx. H (f x) (g x)) ∈ borel_measurable M"
proof -
let ?G = "λy x. if g x = ∞ then H y ∞ else if g x = - ∞ then H y (-∞)
else H y (ereal (real_of_ereal (g x)))"
let ?F = "λx. if f x = ∞ then ?G ∞ x else if f x = - ∞ then ?G (-∞) x
else ?G (ereal (real_of_ereal (f x))) x"
{ fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule:
ereal2_cases) auto }
note * = this
from assms show ?thesis unfolding * by simp
qed
Then you note that the conversions between "real" and "ereal" (which are
called "ereal :: real ⇒ ereal" and "real_of_ereal :: ereal ⇒ real" in
Isabelle) are unconditionally Borel-measurable.
For the first one, that should be obvious. For the second one, note that
"real_of_ereal" is clearly a continuous map from "UNIV - {±∞} :: ereal"
to "UNIV :: real" and then still Borel-measurable on the entire Borel
space of ereal because there are only countable many (namely 2)
exceptional points.
I don't see why this kind of argument should not work in HOL4. This does
not even assume that "∞ - ∞ = -∞ - (-∞)" or anything of the sort. It
only assumes that "∞ - ∞" is some arbitrary but globally fixed value –
surely that is the case in HOL4's logic.
Manuel
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
