[STATEMENT]
lemma expectation_add_pair_pmf:
  fixes f :: "'a \<Rightarrow> 'c::{banach, second_countable_topology}"
  assumes "finite (set_pmf p)" and "finite (set_pmf q)"
  shows "measure_pmf.expectation (pair_pmf p q) (\<lambda>(x,y). f x + g y) =
           measure_pmf.expectation p f + measure_pmf.expectation q g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "measure_pmf.expectation (pair_pmf p q) (\<lambda>(x,y). f x + g y) =
          measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z))
[PROOF STEP]
by (simp add: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z))

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z))

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "\<dots> = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) +
                  measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z)) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) + measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z))
[PROOF STEP]
by (intro Bochner_Integration.integral_add integrable_measure_pmf_finite) (auto intro: assms)
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z)) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) + measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z))

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z)) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) + measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z))

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) =
               measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) = measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) = measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) = measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "map_pmf fst (pair_pmf p q) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf fst (pair_pmf p q) = p
[PROOF STEP]
by (rule map_fst_pair_pmf)
[PROOF STATE]
proof (state)
this:
map_pmf fst (pair_pmf p q) = p

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_pmf fst (pair_pmf p q) = p

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z)) =
               measure_pmf.expectation (map_pmf snd (pair_pmf p q)) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z)) = measure_pmf.expectation (map_pmf snd (pair_pmf p q)) g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z)) = measure_pmf.expectation (map_pmf snd (pair_pmf p q)) g

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z)) = measure_pmf.expectation (map_pmf snd (pair_pmf p q)) g

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "map_pmf snd (pair_pmf p q) = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf snd (pair_pmf p q) = q
[PROOF STEP]
by (rule map_snd_pair_pmf)
[PROOF STATE]
proof (state)
this:
map_pmf snd (pair_pmf p q) = q

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>a. case a of (x, y) \<Rightarrow> f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>a. case a of (x, y) \<Rightarrow> f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g

goal:
No subgoals!
[PROOF STEP]
qed