Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] looking for some measure.union_inter theorem

Email Gateway (Aug 19 2022 at 09:17):

From: Henri DEBRAT <Henri.Debrat@loria.fr>
Hi all,

I am trying to demonstrate the following probability lemma (prob being defined as a measure in a prob_space according to the Probability library) :
"⋀ A B. finite A ⟹ finite B ⟹ prob (A ∪ B) + prob (A ∩ B) = prob A + prob B"

The closer theorem I could discover in the Isabelle/HOL library is Finite_Set.folding_image_simple.union_inter.

Si I am trying this:

have "⋀ A B. finite A ⟹ finite B ⟹ prob (A ∪ B) + prob (A ∩ B) = prob A + prob B"
proof -
fix A B::"(nat×'proc ⇒ bool) set"
assume A:"finite A" and B:"finite B"
show "prob (A ∪ B) + prob (A ∩ B) = prob A + prob B"
proof (intro folding_image_simple.union_inter [OF _ A B, of "op +" "0::real" "λω. prob {ω}" prob], default)

There, it output I should now demonstrate that:

⋀A. finite A ⟹ prob A = fold_image op + (λω. prob {ω}) 0 A

I feel a little lost from this point, as I do not understand why f(A) + 0 = f(A) for any peculiar function f ! As far a I know, this is part of the addition definition.

Any clue ?

Thanks in advance.
H.

Email Gateway (Aug 19 2022 at 09:17):

From: Henri DEBRAT <Henri.Debrat@loria.fr>

I feel a little lost from this point, as I do not understand why f(A) + 0 = f(A) for any peculiar function f ! As far a I know, this is part of the addition definition.

I meant "I do not understand why f(A) + 0 = f(A) SHOULD BE PROVED for any peculiar function f ", of course...

Email Gateway (Aug 19 2022 at 09:17):

From: Stephan Merz <Stephan.Merz@loria.fr>
Hi Henri,

while not a direct answer to your proof attempt, I believe that the lemma you are trying to prove is a simple consequence of existing lemmas:

prob(A \<union> B)
= prob((A - (A \<inter> B)) \<union> B) [by simple set theory]
= prob(A - (A \<inter> B)) + prob(B) [by lemma finite_measure_Union]
= (prob(A) - prob(A \<inter< B)) + prob(B) [by lemma finite_measure_Diff]

Hope this helps,

Stephan

Email Gateway (Aug 19 2022 at 09:17):

From: Johannes Hölzl <hoelzl@in.tum.de>
As Stephan Merz already mentioned this is better done with
finite_measure_Union and finite_measure_Diff in the prob_space locale.

fold_image (op +) is used to define setsum and setprod, so it is easier
to just use setsum. The rules you need are setsum_Un_Int and
measure_eq_setsum_singleton. But my experience is, that staying as long
as possible in the probability theory setting (i.e. use prob on sets) is
usually easier.

I hope this helps,
Johannes

Last updated: Apr 26 2024 at 08:19 UTC