Email Gateway (Aug 23 2022 at 09:25): Email Gateway (Aug 23 2022 at 09:25):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Dear HOL4 and Isabelle community,
the sole purpose of this email is to have your attention on a recent pull
request on HOL4:
https://github.com/HOL-Theorem-Prover/HOL/pull/845
where I was trying to formalize Fubini's theorem (in Lebesgue Integrals)
but was blocked somehow by HOL4's new arithmetic definitions of extended
reals (extreal), i.e. the addition/subtraction of infinities.
In short words, I feel that the statements of this classical result
(Fubini's theorem) by Guido Fubini (1879-1943) are not sufficient,
because its proof seems inevitably relied on the forbidden part of extreal
arithmetics. As a result, Fubini's theorem in its original statements has
been or (can be) formalized in Isabelle/HOL, Lean and Mizar, but not in
latest HOL4 where PosInf + NegInf is unspecified.
Thanks in advance for your opinions and comments!
Regards,
Chun Tian
Email Gateway (Aug 23 2022 at 09:25):From: Manuel Eberl <eberlm@in.tum.de>
Hello,
I find this a bit odd and I think that abstractly, there should be no
problem here.
Your assumptions include
(AE y::(Y,B,v). integrable (X,A,u) (λx. f (x,y)))
(AE x::(X,A,u). integrable (Y,B,v) (λy. f (x,y)))
And you say you need to add the assumptions
∀y. y ∈ Y ⇒ ∫⁺ (X,A,u) (λx. (abs ∘ f) (x,y)) ≠ +∞
∀x. x ∈ X ⇒ ∫⁺ (Y,B,v) (λy. (abs ∘ f) (x,y)) ≠ +∞
The former implies the "almost everywhere" form of the latter. So,
suppose X' and Y' are the subsets of X and Y where it doesn't hold, why
don't you just w.l.o.g. assume f to be zero on (X'×Y)∪(X×Y')? That does
not change the value of the integral – since both measures are
sigma-finite, and X' and Y' are null sets, (X'×Y)∪(X×Y') is also a null set.
Not saying that this is the easiest way to do it, but it should work.
In Isabelle, the situation is quite a bit different. Most of the heavy
lifting is done with non-negative integrals (nn_integral), which work on
extended non-negative reals, which are a much nicer algebraic structure
than "normal" extended reals.
The "normal" integral (lebesgue_integral) does not even return extended
reals, but normal reals, and is undefined (or rather always returns 0)
if the function is not integrable (i.e. if the nn_integral of the
absolute value is ∞).
If I recall correctly, results for lebesgue_integral usually follow
fairly easily from those of nn_integral. Especially because
integrability is just measurability + "nn_integral ≠ ∞" so the results
for nn_integral allow you to show integrability easily, and once you
have shown integrability, lebesgue_integral behaves fairly nicely.
(I've only contributed a little bit to this library, most of the work
was done by Johannes Hölzl, so the above is just my impression from
using and browsing the library)
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 09:25):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Hi Manuel,
please be noticed that
(AE y::(Y,B,v). integrable (X,A,u) (λx. f (x,y)))
(AE x::(X,A,u). integrable (Y,B,v) (λy. f (x,y)))
are conclusions of Fubini's theorem.
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. And actually the
measurability is the main problem:
[integrable_def] Definition
⊢ ∀m f.
integrable m f ⇔
f ∈ Borel_measurable (m_space m,measurable_sets m) ∧
∫⁺ m f⁺ ≠ +∞ ∧ ∫⁺ m f⁻ ≠ +∞
One may think that, if two functions f and g only differ at a null set
(i.e. they're a.e.-equivalent), and one of them, say f, is measurable, then
so is the other. But this is actually not true. In fact, this argument is
only true if the involved measure space is complete (i.e. all subsets of
null sets are null sets too). However their integrations are the same
(when they're integrable). See the following two theorems in HOL4:
[integral_cong_AE] Theorem
⊢ ∀m f g. measure_space m ∧ (AE x::m. f x = g x) ⇒ ∫ m f = ∫ m g
[integrable_eq_AE] Theorem
⊢ ∀m f g.
complete_measure_space m ∧ integrable m f ∧
(AE x::m. f x = g x) ⇒
integrable m g
To see a counterexample (of integrable_eq_AE when complete_measure_space
is replaced by just measure_space), see the following artificial example
given by Prof. Massimo Campanino (University of Bologna):
"I think I found an example using Cantor set C which has 0 Lebesque
measure. Let f and g both be equal to 1 on the complementary set of C. We
can decompose C as the union of two disjoint non-measurable sets C_1 and
C_2 using a modification of the standard example of non-measurable subset
of [0, 1]. Let f be equal to 0 ang g be equal to 1/3 on C_1 and to 2/3 on
C_2."
Regards,
Chun Tian
Email Gateway (Aug 23 2022 at 09:25):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 23 2022 at 09:25):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
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
Email Gateway (Aug 23 2022 at 09:25):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 23 2022 at 09:25):From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
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
Email Gateway (Aug 23 2022 at 09:26):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 23 2022 at 09:26):From: Manuel Eberl <eberlm@in.tum.de>
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
Last updated: Apr 18 2024 at 16:19 UTC