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 <ebe...@in.tum.de> 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
