Fubini's Theorem and its variants in some models of extreals

[binghe]

Hi,

of all the PRs I submitted to HOL so far, this is the most special one (see below for the detailed story).

This PR continues the previous PR #822 and provide a formalization of Fubini's theorem [1, p.143] (or [2, p.126]) for product measure in Lebesgue integrals (as martingaleTheory.FUBINI). The original theorem statement (in HOL's notation) is the following:

      ∀X Y A B u v f.
            sigma_finite_measure_space (X,A,u) ∧
            sigma_finite_measure_space (Y,B,v) ∧
            f ∈ Borel_measurable ((X,A) × (Y,B)) ∧
            (∫⁺ ((X,A,u) × (Y,B,v)) (abs ∘ f) ≠ +∞ ∨
             ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. (abs ∘ f) (x,y))) ≠ +∞ ∨
             ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. (abs ∘ f) (x,y))) ≠ +∞) ⇒
            ∫⁺ ((X,A,u) × (Y,B,v)) (abs ∘ f) ≠ +∞ ∧
            ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. (abs ∘ f) (x,y))) ≠ +∞ ∧
            ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. (abs ∘ f) (x,y))) ≠ +∞ ∧
            integrable ((X,A,u) × (Y,B,v)) f ∧
            (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))) ∧
            integrable (X,A,u) (λx. ∫ (Y,B,v) (λy. f (x,y))) ∧
            integrable (Y,B,v) (λy. ∫ (X,A,u) (λx. f (x,y))) ∧
            ∫ ((X,A,u) × (Y,B,v)) f =
            ∫ (Y,B,v) (λy. ∫ (X,A,u) (λx. f (x,y))) ∧
            ∫ ((X,A,u) × (Y,B,v)) f =
            ∫ (X,A,u) (λx. ∫ (Y,B,v) (λy. f (x,y)))

Informally, let (X,A,u) and (Y,B,v) be σ-finite measure spaces, and let f :(Χ,Υ) -> extreal be (A B)-measurable. If at least one of the three integrals is finite, then all three integrals are finite, f is L1(u v)-integrable, and

1. x |-> f(x,y) is L1(u)-integrable for v-a.e. y IN Y
2. y |-> f(x,y) is L1(v)-integrable for u-a.e. x IN X
3. y |-> ∫ (X,A,u) (λx. f (x,y)) is L1(v)-integrable.
4. x |-> ∫ (Y,B,v) (λy. f (x,y)) is L1(u)-integrable.
5. ∫ ((X,A,u) × (Y,B,v)) f = ∫ (Y,B,v) (λy. ∫ (X,A,u) (λx. f (x,y))) = ∫ (X,A,u) (λx. ∫ (Y,B,v) (λy. f (x,y)))

Fubini's theorem is supposed to be an easy corollary of Tonelli's theorem, formalized in #822. However, after over a month's efforts, I found that this proof seems impossible, unless I added the following extra antecedents into the theorem:

1. ∀y. y ∈ Y ⇒ ∫⁺ (X,A,u) (λx. (abs ∘ f) (x,y)) ≠ +∞
2. ∀x. x ∈ X ⇒ ∫⁺ (Y,B,v) (λy. (abs ∘ f) (x,y)) ≠ +∞

The reason for the need of the above extra antecedents is that, in the following two lemmas of borelTheory and lebesgueTheory, HOL's current version needs extra antecedents to prevent PosInf - PosInf or PosInf + NegInf:

   [IN_MEASURABLE_BOREL_SUB]  Theorem      
      ⊢ ∀a f g h.
            sigma_algebra a ∧ f ∈ Borel_measurable a ∧
            g ∈ Borel_measurable a ∧
            (∀x. x ∈ space a ⇒ f x ≠ −∞ ∧ g x ≠ +∞ ∨ f x ≠ +∞ ∧ g x ≠ −∞) ∧
            (∀x. x ∈ space a ⇒ h x = f x − g x) ⇒
            h ∈ Borel_measurable a

   [integral_add_lemma]  Theorem      
      ⊢ ∀m f f1 f2.
            measure_space m ∧ integrable m f ∧ integrable m f1 ∧
            integrable m f2 ∧ (∀x. x ∈ m_space m ⇒ f x = f1 x − f2 x) ∧
            (∀x. x ∈ m_space m ⇒ 0 ≤ f1 x) ∧
            (∀x. x ∈ m_space m ⇒ 0 ≤ f2 x) ∧
            (∀x. x ∈ m_space m ⇒ f1 x ≠ +∞ ∨ f2 x ≠ +∞) ⇒
            ∫ m f = ∫⁺ m f1 − ∫⁺ m f2

Then I recall in the old days (<= K13), when PosInf + NegInf = PosInf - PosInf = PosInf were allowed, the above two lemmas didn't have the extra antecedents, namely: (∀x. x ∈ space a ⇒ f x ≠ −∞ ∧ g x ≠ +∞ ∨ f x ≠ +∞ ∧ g x ≠ −∞) or (∀x. x ∈ m_space m ⇒ f1 x ≠ +∞ ∨ f2 x ≠ +∞). So I tried the following experiments in a separated theory file (examples/probability/fubiniScript.sml):

First of all, since the value of PosInf + NegInf = PosInf - PosInf = NegInf - NegInf is unspecified in current HOL's extrealTheory, thus assuming any (unique) value shouldn't cause any inconsistency in HOL, and for each value we assumed, we may call it a (non-standard) model of extended reals. The following five models were initially defined:

   [extreal_model1_def]  Definition      
      ⊢ extreal_model1 ⇔
        +∞ + −∞ = +∞ ∧ −∞ + +∞ = +∞ ∧ +∞ − +∞ = +∞ ∧ −∞ − −∞ = +∞
   
   [extreal_model2_def]  Definition      
      ⊢ extreal_model2 ⇔
        +∞ + −∞ = −∞ ∧ −∞ + +∞ = −∞ ∧ +∞ − +∞ = −∞ ∧ −∞ − −∞ = −∞
   
   [extreal_model3_def]  Definition      
      ⊢ extreal_model3 ⇔
        +∞ + −∞ = 0 ∧ −∞ + +∞ = 0 ∧ +∞ − +∞ = 0 ∧ −∞ − −∞ = 0
   
   [extreal_model4_def]  Definition      
      ⊢ ∀r.
            extreal_model4 r ⇔
            +∞ + −∞ = Normal r ∧ −∞ + +∞ = Normal r ∧ +∞ − +∞ = Normal r ∧
            −∞ − −∞ = Normal r
   
   [extreal_model5_def]  Definition      
      ⊢ ∀z.
            extreal_model5 z ⇔
            +∞ + −∞ = z ∧ −∞ + +∞ = z ∧ +∞ − +∞ = z ∧ −∞ − −∞ = z

Model 1 corresponds to HOL version <= K13, Isabelle, and Lean. Model 2 is the dual version of Model 1 where I let PosInf + NegInf = NegInf. Model 3 is the one adopted in Mizar's MML (xxreal3.mm) where PosInf + NegInf = 0. Model 4 is a parametrized generalization of Model 3 such that PosInf + NegInf = Normal r for any real value r. Finally, Model 5 is a combined version of all previous models such that PosInf + NegInf etc. is assigned to any extreal value including PosInf and NegInf.

What I have proven is the following: under whatever parameter in Model 5, the original Fubini's theorem holds without any extra antecedents: (the main difficulty is to prove IN_MEASURABLE_BOREL_SUB and integral_add_lemma under Model 1~4)

   [FUBINI__model5]  Theorem      
      ⊢ ∀z.
            extreal_model5 z ⇒
            ∀X Y A B u v f.
                sigma_finite_measure_space (X,A,u) ∧
                sigma_finite_measure_space (Y,B,v) ∧
                f ∈ Borel_measurable ((X,A) × (Y,B)) ∧
                (∫⁺ ((X,A,u) × (Y,B,v)) (abs ∘ f) ≠ +∞ ∨
                 ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. (abs ∘ f) (x,y))) ≠ +∞ ∨
                 ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. (abs ∘ f) (x,y))) ≠ +∞) ⇒
                ∫⁺ ((X,A,u) × (Y,B,v)) (abs ∘ f) ≠ +∞ ∧
                ∫⁺ (Y,B,v) (λy. ∫⁺ (X,A,u) (λx. (abs ∘ f) (x,y))) ≠ +∞ ∧
                ∫⁺ (X,A,u) (λx. ∫⁺ (Y,B,v) (λy. (abs ∘ f) (x,y))) ≠ +∞ ∧
                integrable ((X,A,u) × (Y,B,v)) f ∧
                (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))) ∧
                integrable (X,A,u) (λx. ∫ (Y,B,v) (λy. f (x,y))) ∧
                integrable (Y,B,v) (λy. ∫ (X,A,u) (λx. f (x,y))) ∧
                ∫ ((X,A,u) × (Y,B,v)) f =
                ∫ (Y,B,v) (λy. ∫ (X,A,u) (λx. f (x,y))) ∧
                ∫ ((X,A,u) × (Y,B,v)) f =
                ∫ (X,A,u) (λx. ∫ (Y,B,v) (λy. f (x,y)))

My conclusion is the following:

1. It's possible that Fubini's theorem in the pure mathematical sense is wrong, i.e. without some extra antecedents the forbidden extreal arithmetics like PosInf - PosInf is inevitable. But I'm not 100% sure for this, until I got confirmed by my probability professor.

2. Fubini's theorem is already formalized in Mizar (see mesfun13). And it's possible to formalize Fubini's theorem in its original statements In Isabelle/HOL and Lean. But I'd say all these work will be based on special models of extreal arithmetics where PosInf + NegInf, etc. has a determined value.

3. The well-accepted opinions that PosInf + NegInf = PosInf and x / 0 = 0 are "harmless" (and especially handy) in formal mathematics, needs to be reconsidered.

Regards,

Chun Tian

[1] Schilling, R.L.: Measures, Integrals and Martingales (2nd Edition). Cambridge University Press (2017).
[2] Schilling, R.L.: Measures, Integrals and Martingales. Cambridge University Press (2005).

[mn200]

My uninformed opinion is that, given option 5's validity, option 3 is the nicest: who wouldn't want x - x = 0 and
x - y = x + -y to be as true as possible?

I don't understand your third point. I'm not sure that anyone claims you can just pick anything you want in situations like this and have it be harmless. Instead, we can pick certain values with care, and thereby avoid some annoying side conditions, making things “handy”. I'd say your work here is strong support for this!

[mn200]

But do feel free to write to the HOL, Isabelle and/or Lean mailing lists and invite other opinions...

[binghe]

Some extra work (irrelevant to Fubini's theorem) in this PR include the following theorem in borelTheory (any continuous function is measurable from (real-value) borel to itself), ported from HVG Concordia's normal_rvTheory:

   [in_measurable_borel_continuous_on]  Theorem      
      ⊢ ∀f. f continuous_on 𝕌(:real) ⇒ f ∈ borel_measurable borel

Other changes are just moving of definitions to their more appropriated places, e.g. sigma_finite_measure_space_def (to measureTheory) and binary_def (to util_probTheory).

[binghe]

My uninformed opinion is that, given option 5's validity, option 3 is the nicest: who wouldn't want x - x = 0 and
x - y = x + -y to be as true as possible?

In fact, in all models we can formally prove x - y = x + -y, simply because in all these models the 4 expressions (PosInf + NegInf = NegInf + PosInf = PosInf - PosInf = NegInf - NegInf) are assigned to the same value: (and -NegInf = PosInf is always true due to the unique definition of extreal_ainv)

   [extreal_sub_add__model1]  Theorem      
      ⊢ extreal_model1 ⇒ ∀x y. x − y = x + -y
   
   [extreal_sub_add__model2]  Theorem      
      ⊢ extreal_model2 ⇒ ∀x y. x − y = x + -y
   
   [extreal_sub_add__model3]  Theorem      
      ⊢ extreal_model3 ⇒ ∀x y. x − y = x + -y
   
   [extreal_sub_add__model4]  Theorem      
      ⊢ ∀r. extreal_model4 r ⇒ ∀x y. x − y = x + -y

The actual problem of Model 3 (Mizar) (and also Model 4) is that, associativity doesn't hold. For example, consider 1 = 0 + 1 = (PosInf + NegInf) + 1 = PosInf + (NegInf + 1) = PosInf + NegInf = 0 in Model 3, while the special elegance of Model 1 (Isabelle, Lean and old HOL) and also Model 2, is that both commutativity and associativity for extreals hold:

   [add_comm__model1]  Theorem      
      ⊢ extreal_model1 ⇒ ∀x y. x + y = y + x
   
   [add_comm__model2]  Theorem      
      ⊢ extreal_model2 ⇒ ∀x y. x + y = y + x
   
   [add_comm__model3]  Theorem      
      ⊢ extreal_model3 ⇒ ∀x y. x + y = y + x
   
   [add_comm__model4]  Theorem      
      ⊢ ∀r. extreal_model4 r ⇒ ∀x y. x + y = y + x

   [add_assoc__model1]  Theorem      
      ⊢ extreal_model1 ⇒ ∀x y z. x + (y + z) = x + y + z
   
   [add_assoc__model2]  Theorem      
      ⊢ extreal_model2 ⇒ ∀x y z. x + (y + z) = x + y + z

[mn200]

Clearly "uninformed" was right!

Anyway, given the above as motivation, I think it would be quite reasonable to follow the herd and revert to the old model.

[binghe]

Clearly "uninformed" was right!

Anyway, given the above as motivation, I think it would be quite reasonable to follow the herd and revert to the old model.

Model 1 and 2 are equivalently "good" () but I still think there's no reason to assign PosInf + NegInf to PosInf instead of NegInf, as mathematically none of these is true. My whole opinion here is that, having these non-standard definitions it's possible to have "false positive", i.e. having verified a wrong non-trivial statement although the logic itself is consistent.

But, reverting to the old model is very easy: we can just revert the definitions of extreal_add and extreal_sub and the rest of HOL-Probability still builds without any problem. I personally don't like this idea, but if you insist I have to follow. However, I hope that we can make this choice is easily switchable one, say, by the configuration option before building HOL ...

[mn200]

I don't insist at all. It “would be reasonable” to do it; and indeed, the validity of the theorems is demonstration of that. As the author of the theorems, I'm happy to let you make the final call.

[binghe]

I don't insist at all. It “would be reasonable” to do it; and indeed, the validity of the theorems is demonstration of that. As the author of the theorems, I'm happy to let you make the final call.

Well... thanks. I hope to keep the current extreal arithmetic definitions, although this means many proofs become more difficult than those in other theorem provers. And think the good side: our proofs can be easily ported to Mizar or Isabelle, where extra assumptions on extreal arithmetics were used.

As for the additional antecedents in the present version of Fubini's theorem, I found that it doesn't cause any problem in my own application in probability theory, where the extra requirements are indeed satisfied. There are two possible but divergent future developments:

1. A better (formal) proof of Fubini's theorem will be found, and even in HOL's current setting the original statement can be proved. Then all models/opinions of extreals are again "equivalent".
2. The original statement of Fubini's theorem is confirmed by real mathematicians as "not sufficient". Then HOL's my formalization will be the only "correct one", who knows ...

[binghe]

A small correction about Lean. Lean's mathlib actually hasn't defined + and - for extended reals, below are some comments I found in their related file:

In Isabelle they define + - * and / (making junk choices for things like -∞ + ∞)
and then prove whatever bits of the ordered ring/field axioms still hold. They
also do some limits stuff (liminf/limsup etc).
See https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Extended_Real.html

[ahmedwaqar]

The arithmetic of infinity is tricky and also paradoxical in nature. I'm not sure what was the thought when Mhamdi was defining the extreal_add_def. I remembered once having a similar discussion to define extread_add as a total function and assign PosInf + NegInf to some meaningful value so to make proofs easier or unload some extra assumptions. It's actually a famous Ross-Littlewood Paradox, which states that subtracting infinitely many times from infinity returns different results depending upon how you subtract it.

See some interesting pointers to that and attached file:

http://www.suitcaseofdreams.net/Wizard_Mermaid.htm

https://en.wikipedia.org/wiki/Ross%E2%80%93Littlewood_paradox

Infinity ch. 3.pdf

[binghe]

Hi Michael, please hold this PR, I think I've got a new idea to prove the original Fubini's theorem without extra antecedents.

[binghe]

Hi Michael, please hold this PR, I think I've got a new idea to prove the original Fubini's theorem without extra antecedents.

Hmmm ... I was thinking that, if the value of PosInf + NegInf has only three cases (PosInf, NegInf and Normal r), in theory I can do a case analysis and prove each case separately. This is still not inline with the actual mathematics but is logically correct.

However, the problem is that I don't have just PosInf + NegInf, but also NegInf + PosInf, PosInf - PosInf and NegInf - NegInf, thus the total number of cases are 3^4 = 81, and none of them leads to any inconsistency! My work in that fubiniTheory only proved Fubini's theorem under 3 of 81 cases, the cases where at least add_comm and extreal_sub_add hold. In all other cases the proof is still impossible.

Thus I hope the present PR can be merged if there's no problem except for the math statements of Fubini's theorem. As I mentioned already, the extra antecedents do not block my future plan (Law of Large Numbers for I.I.D. r.v.'s).

[binghe]

The arithmetic of infinity is tricky and also paradoxical in nature. I'm not sure what was the thought when Mhamdi was defining the extreal_add_def.

But I do like his new definition because it really makes senses. Without having those "forbidden" arithmetics unspecified, the proof engineers have to "be careful" but now (with the present definitions) the proof cannot complete - this is inline with the whole idea of formal verification.

[mn200]

Of course, I'm happy to take any updates to this if you end up deciding that there is a better way of getting the "right" statement of Fubini's theorem.

[binghe]

Thanks for merging the PR.

Yesterday I got a chance to ask some questions on the Slack of CICM 2020, to Mario Carneiro, current Lean mathlib and (former) Metamath proof engineer. It turns out that Metamath and Mizar both choose PosInf + NegInf = 0 [1] (they are aware of the inconvenience of associativity [2]) More importantly, he said that, when the time comes, Lean will follow in the same way.

Thus there's actually no "herd", only Isabelle and HOL4 (old) choose PosInf + NegInf = PosInf, while Mizar/Metamath (and future Lean mathlib) choose PosInf + NegInf = 0. On the other hand, it seems that not every theorem prover has the ability to leave it completely unspecified (and we can).

P. S. I got some new hints from Manuel Eberl of Isabelle as you may have also seen. The difficulty is that, some connections between borel and Borel are missing in our code base. I will try to resolve this problem and see if the extra antecedents in IN_MEASURABLE_BOREL_SUB and integral_add_lemma can be removed in a better proof without using too much extreal arithmetics.

--Chun

[1] http://us.metamath.org/mpeuni/pnfaddmnf.html
[2] http://us.metamath.org/mpeuni/xaddass.html

[binghe]

Updates: today I finally finished the following two improved version of IN_MEASURABLE_BOREL_ADD and IN_MEASURABLE_BOREL_SUB within the current definition of extreals in HOL4:

   [IN_MEASURABLE_BOREL_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

   [IN_MEASURABLE_BOREL_SUB']  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

In comparison with the existing corresponding theorems, now there's no restrictions on unspecified arithmetics between PosInf and NegInf. In another words, by tedious case analysis in the proofs of the above two new theorems, I have successfully proven that, under whatever choices on those "unspecified" arithmetics (e.g. PosInf + NegInf), these two theorems still hold! This resolve one of the two blocking issues in proving the "correct" Fubini's theorem.

I'll submit a new PR once the existing PR #850 get merged (the proof of the above two new theorems depends on the new definition of Borel in that PR.)

Regards,

Chun Tian