Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem
El 28/07/20 a las 4:35, Manuel Eberl escribió: > Well, if you want to do it the "proper" way, you need a logic with an > explicit notion of undefinedness. In HOL4 one can use the option types. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem
On 28/07/2020 11:20, Chun Tian (binghe) wrote: > 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. Well, if you want to do it the "proper" way, you need a logic with an explicit notion of undefinedness. Or some form of dependent types, perhaps. But I think even in Coq and Lean they often go for the "let's pick a convenient dummy result" approach as opposed to the "let's restrict the function's input to a subtype" approach when it comes to questions like "what is the integral of a non-integrable function". (I don't have any hard data for that, just from anecdotes I recall from talking to people, but I'm sure someone will contradict me if the above is wrong.) In Isabelle/HOL, the current consensus seems to be that convenient dummy values are the best way to go. We've yet to encounter a situation where they are a problem (and I for one do not think there is one) and they make life much easier. For instance, if you define something like "ln x = (THE y. x = exp y)", the ln of all non-positive numbers is completely unspecified. If you add a "if x ≤ 0 then undefined else …", it's still unspecified, but you at least know that "ln x1 = ln x2" for any non-positive numbers x1, x2. That might sound silly to you, but the nice thing is that this allows you to prove that ln is measurable on the reals, whereas the other thing does not. Of course, you could do all the maths you can do with that definition also with the previous one, but things just become a lot messier because you then have to talk about measurability on a subspace and some of the automation will probably not work anymore etc. So why not make your life a bit easier? All in all, I think this fixation on defining things the "proper" way is unnecessary. But don't get me wrong, I totally understand where it is coming from, and I do think it is a legitimate view. Manuel ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem
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 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
Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem
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
Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem
Not that easy, or just impossible. However, if f and g are positive and negative parts of the same function (h), then the theorem indeed holds without any extra antecedents: [IN_MEASURABLE_BOREL_PLUS_MINUS] Theorem ⊢ ∀a f. f ∈ Borel_measurable a ⇔ f⁺ ∈ Borel_measurable a ∧ f⁻ ∈ Borel_measurable a My previous idea actually doesn't work. The problem is that, not only ∞ + -∞, but also the other three cases (-∞ + ∞, ∞ - ∞, -∞ - -∞) will also involve when you actually try to prove that proposition, and these four cases have in total 3^4 possible value combinations, none leads to any inconsistency. --Chun On Mon, Jul 27, 2020 at 5:51 PM Manuel Eberl wrote: > In any case, all I said in my last email was that you should be able to > easily prove > > ⊢ ∀a f g h. sigma_algebra a ∧ f ∈ Borel_measurable a ∧ g ∈ > Borel_measurable a ⇒ (λx. f x − g x) ∈ Borel_measurable a > > no matter what ∞ + -∞ is defined as (including undefined, which is just > some globally fixed value in HOL). But perhaps that is the same > realisation that you also had in your last email. > > 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
Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem
On 27/07/2020 11:38, Chun Tian (binghe) wrote:
> If f and g are both measurable functions, then {x | f x = g x /\ x IN
> m_space m} (abbrev: {f = g}) must be a measurable set. However, if you
> have just f a measurable function, and {f = g} a measurable set, then it
> is NOT true that g is a measurable set, UNLESS m is a complete measure
> space.
I don't understand that statement at all. Did you mean "it is NOT true
that g is a measurable function"? If yes, then, well, of course not,
since {f = g} could be the empty set (which is certainly measurable) and
then obviously the measurability of f does not tell you anything about
g. Not sure why you are bringing this up.
In any case, all I said in my last email was that you should be able to
easily prove
⊢ ∀a f g h. sigma_algebra a ∧ f ∈ Borel_measurable a ∧ g ∈
Borel_measurable a ⇒ (λx. f x − g x) ∈ Borel_measurable a
no matter what ∞ + -∞ is defined as (including undefined, which is just
some globally fixed value in HOL). But perhaps that is the same
realisation that you also had in your last email.
Manuel
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem
Hi,
If f and g are both measurable functions, then {x | f x = g x /\ x IN
m_space m} (abbrev: {f = g}) must be a measurable set. However, if you have
just f a measurable function, and {f = g} a measurable set, then it is NOT
true that g is a measurable set, UNLESS m is a complete measure space.
But actually I just got a new idea to resolve my problem:
Although the value of `PosInf + NegInf`, etc. are not specified (in latest
HOL4), but if I let `x = PosInf + NegInf` in a proof, and then do a case
analysis on `x`, there must be only three possibilities: x = PosInf, x =
NegInf, x = Normal r, where r is an arbitrary normal real number. But I
do have proven the involved theorems under all these 3 cases (with very
different proofs, sometimes), thus in theory I also have a proof when
`PosInf + NegInf` is unspecified!
What I have just benefited from logic is that the same logical term cannot
equal to different values in the same proof.
Regards,
Chun Tian
On Mon, Jul 27, 2020 at 4:28 PM Manuel Eberl wrote:
> On 27/07/2020 10:04, Chun Tian (binghe) wrote:
> > are conclusions of Fubini's theorem.
>
> Oops, okay, sorry!
>
> > Furthermore, the definition of integrability, besides the finiteness of
> > nn_integral (pos_fn_integral in HOL4) of the positive and negative parts,
> > also includes the measurability of the involved functions.
>
> Perhaps the problem is simply that your measurability theorem for
> subtraction on extreals is too weak. I would be very surprised if it
> were not possible to prove that subtraction of extreals is measurable
> with no preconditions.
>
> After all, there are only finitely many problematic points and you can
> treat those separately. Testing for equality is measurable, constant
> functions are measurable, "if-then-else" is measurable – so a function
> that is measurable with finitely many exceptions should also be measurable.
>
> At the end of the day, pretty much everything you can write down without
> doing something crazy (like choice operators) is Borel-measurable.
>
> 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
