Hi Manuel,
many thanks for your hints. I can't fully understand Isabelle proofs, but I
think I got the idea. In HOL4 we have the following theorem for real-valued
borel measurable functions:
[in_borel_measurable_add] Theorem
⊢ ∀a f g h.
sigma_algebra a ∧ f ∈ borel_measurable a ∧
g ∈ borel_measurable a ∧ (∀x. x ∈ space a ⇒ h x = f x + g x) ⇒
h ∈ borel_measurable a
and a transition theorem from borel to Borel - the extreal-valued Borel
measurable set:
[IN_MEASURABLE_BOREL_IMP_BOREL] Theorem
⊢ ∀f m.
f ∈ borel_measurable (m_space m,measurable_sets m) ⇒
Normal ∘ f ∈ Borel_measurable (m_space m,measurable_sets m)
Thus, in theory, by considering a finite number of exceptional values
(infinities) it's possible to prove the previously mentioned lemma without
extra antecedents, no matter what's the actual value of the unspecified
terms. What I said before was based on the current proofs of
IN_MEASURABLE_BOREL_SUB in HOL4, which (indirectly) involves all 4 cases of
arithmetics of infinities.
I would say, this is still not inline with "real" mathematics, but the
situation is slightly better than (rudely) assuming any fixed value for
`PosInf + NegInf` a priori.
--Chun
On Mon, Jul 27, 2020 at 9:46 PM Manuel Eberl <ebe...@in.tum.de> wrote:
> 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
>
>
--
Chun Tian (binghe)
Fondazione Bruno Kessler (Italy)
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
