[STATEMENT]
lemma mix_pmf_partition:
  fixes p :: "'a pmf"
  assumes "y \<in> set_pmf p" "set_pmf p - {y} \<noteq> {}"
  obtains a q where "a \<in> {0<..<1}" "set_pmf q = set_pmf p - {y}"
    "p = mix_pmf a q (return_pmf y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
y \<in> set_pmf p
set_pmf p - {y} \<noteq> {}
[PROOF STEP]
obtain x where x: "x \<in> set_pmf p - {y}"
[PROOF STATE]
proof (prove)
using this:
y \<in> set_pmf p
set_pmf p - {y} \<noteq> {}

goal (1 subgoal):
 1. (\<And>x. x \<in> set_pmf p - {y} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set_pmf p - {y}

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define a where "a = 1 - pmf p y"
[PROOF STATE]
proof (state)
this:
a = 1 - pmf p y

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have a_n1:"a \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 1
[PROOF STEP]
by (simp add: a_def assms(1) pmf_eq_0_set_pmf)
[PROOF STATE]
proof (state)
this:
a \<noteq> 1

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "pmf p y \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf p y \<noteq> 1
[PROOF STEP]
using ex_certain_iff_singleton_support
[PROOF STATE]
proof (prove)
using this:
(\<exists>x. pmf ?p x = 1) = (card (set_pmf ?p) = 1)

goal (1 subgoal):
 1. pmf p y \<noteq> 1
[PROOF STEP]
by (metis (full_types)
        Diff_cancel assms(1) assms(2) card_1_singletonE singletonD)
[PROOF STATE]
proof (state)
this:
pmf p y \<noteq> 1

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence y: "pmf p y < 1"
[PROOF STATE]
proof (prove)
using this:
pmf p y \<noteq> 1

goal (1 subgoal):
 1. pmf p y < 1
[PROOF STEP]
using pmf_le_1[of p y]
[PROOF STATE]
proof (prove)
using this:
pmf p y \<noteq> 1
pmf p y \<le> 1

goal (1 subgoal):
 1. pmf p y < 1
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
using this:
pmf p y \<noteq> 1
pmf p y \<le> 1

goal (1 subgoal):
 1. pmf p y < 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
pmf p y < 1

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence a: "a > 0"
[PROOF STATE]
proof (prove)
using this:
pmf p y < 1

goal (1 subgoal):
 1. 0 < a
[PROOF STEP]
by (simp add: a_def)
[PROOF STATE]
proof (state)
this:
0 < a

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define q where "q = embed_pmf (\<lambda>z. if z = y then 0 else pmf p z / a)"
[PROOF STATE]
proof (state)
this:
q = embed_pmf (\<lambda>z. if z = y then 0 else pmf p z / a)

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have q: "pmf q z = (if z = y then 0 else pmf p z / a)" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf q z = (if z = y then 0 else pmf p z / a)
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (embed_pmf (\<lambda>z. if z = y then 0 else pmf p z / a)) z = (if z = y then 0 else pmf p z / a)
[PROOF STEP]
proof (rule pmf_embed_pmf)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
have "1 = (\<integral>\<^sup>+ x. ennreal (pmf p x) \<partial>count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = \<integral>\<^sup>+ x. ennreal (pmf p x) \<partial>count_space UNIV
[PROOF STEP]
by (rule nn_integral_pmf_eq_1 [symmetric])
[PROOF STATE]
proof (state)
this:
1 = \<integral>\<^sup>+ x. ennreal (pmf p x) \<partial>count_space UNIV

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 = \<integral>\<^sup>+ x. ennreal (pmf p x) \<partial>count_space UNIV

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
have "\<dots> = (\<integral>\<^sup>+ x. ennreal (pmf p x) * indicator {y} x +
                      ennreal (pmf p x) * indicator (-{y}) x \<partial>count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (pmf p x) \<partial>count_space UNIV = \<integral>\<^sup>+ x. ennreal (pmf p x) * indicator {y} x + ennreal (pmf p x) * indicator (- {y}) x \<partial>count_space UNIV
[PROOF STEP]
by (intro nn_integral_cong) (auto simp: indicator_def)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (pmf p x) \<partial>count_space UNIV = \<integral>\<^sup>+ x. ennreal (pmf p x) * indicator {y} x + ennreal (pmf p x) * indicator (- {y}) x \<partial>count_space UNIV

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (pmf p x) \<partial>count_space UNIV = \<integral>\<^sup>+ x. ennreal (pmf p x) * indicator {y} x + ennreal (pmf p x) * indicator (- {y}) x \<partial>count_space UNIV

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
have "\<dots> = (\<integral>\<^sup>+ x. ennreal (pmf p x) * indicator {y} x \<partial>count_space UNIV) +
                    (\<integral>\<^sup>+ x. ennreal (pmf p x) * indicator (-{y}) x \<partial>count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (pmf p x) * indicator {y} x + ennreal (pmf p x) * indicator (- {y}) x \<partial>count_space UNIV = (\<integral>\<^sup>+x\<in>{y}. ennreal (pmf p x)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV)
[PROOF STEP]
by (subst nn_integral_add) auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (pmf p x) * indicator {y} x + ennreal (pmf p x) * indicator (- {y}) x \<partial>count_space UNIV = (\<integral>\<^sup>+x\<in>{y}. ennreal (pmf p x)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (pmf p x) * indicator {y} x + ennreal (pmf p x) * indicator (- {y}) x \<partial>count_space UNIV = (\<integral>\<^sup>+x\<in>{y}. ennreal (pmf p x)\<partial>count_space UNIV) + (\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
have "(\<integral>\<^sup>+ x. ennreal (pmf p x) * indicator {y} x \<partial>count_space UNIV) = pmf p y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>{y}. ennreal (pmf p x)\<partial>count_space UNIV = ennreal (pmf p y)
[PROOF STEP]
by (subst nn_integral_indicator_finite) auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>{y}. ennreal (pmf p x)\<partial>count_space UNIV = ennreal (pmf p y)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>{y}. ennreal (pmf p x)\<partial>count_space UNIV = ennreal (pmf p y)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
have "ennreal (pmf p y) + (\<integral>\<^sup>+ x. ennreal (pmf p x) * indicator (-{y}) x \<partial>count_space UNIV)
                 - ennreal (pmf p y) = (\<integral>\<^sup>+ x. ennreal (pmf p x) * indicator (-{y}) x \<partial>count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (pmf p y) + (\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV) - ennreal (pmf p y) = \<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ennreal (pmf p y) + (\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV) - ennreal (pmf p y) = \<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal (pmf p y) + (\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV) - ennreal (pmf p y) = \<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
have "1 - ennreal (pmf p y) = ennreal (1 - pmf p y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - ennreal (pmf p y) = ennreal (1 - pmf p y)
[PROOF STEP]
by (subst ennreal_1 [symmetric], subst ennreal_minus) auto
[PROOF STATE]
proof (state)
this:
1 - ennreal (pmf p y) = ennreal (1 - pmf p y)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ennreal (1 - pmf p y) = \<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV
[PROOF STEP]
have eq: "(\<integral>\<^sup>+x\<in>-{y}. ennreal (pmf p x)\<partial>count_space UNIV) = 1 - pmf p y"
[PROOF STATE]
proof (prove)
using this:
ennreal (1 - pmf p y) = \<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV

goal (1 subgoal):
 1. \<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV = ennreal (1 - pmf p y)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV = ennreal (1 - pmf p y)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
have "(\<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV) =
            (\<integral>\<^sup>+ x. inverse a * (ennreal (pmf p x) * indicator (-{y}) x) \<partial>count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = \<integral>\<^sup>+ x. ennreal (inverse a) * (ennreal (pmf p x) * indicator (- {y}) x) \<partial>count_space UNIV
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
0 < a

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = \<integral>\<^sup>+ x. ennreal (inverse a) * (ennreal (pmf p x) * indicator (- {y}) x) \<partial>count_space UNIV
[PROOF STEP]
by (intro nn_integral_cong) (auto simp: divide_simps ennreal_mult' [symmetric])
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = \<integral>\<^sup>+ x. ennreal (inverse a) * (ennreal (pmf p x) * indicator (- {y}) x) \<partial>count_space UNIV

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = \<integral>\<^sup>+ x. ennreal (inverse a) * (ennreal (pmf p x) * indicator (- {y}) x) \<partial>count_space UNIV

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
have "\<dots> = inverse a * (\<integral>\<^sup>+ x\<in>-{y}. ennreal (pmf p x) \<partial>count_space UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (inverse a) * (ennreal (pmf p x) * indicator (- {y}) x) \<partial>count_space UNIV = ennreal (inverse a) * (\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV)
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
0 < a

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (inverse a) * (ennreal (pmf p x) * indicator (- {y}) x) \<partial>count_space UNIV = ennreal (inverse a) * (\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV)
[PROOF STEP]
by (subst nn_integral_cmult [symmetric]) (auto simp: ennreal_mult')
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (inverse a) * (ennreal (pmf p x) * indicator (- {y}) x) \<partial>count_space UNIV = ennreal (inverse a) * (\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (inverse a) * (ennreal (pmf p x) * indicator (- {y}) x) \<partial>count_space UNIV = ennreal (inverse a) * (\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
note eq
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV = ennreal (1 - pmf p y)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+x\<in>- {y}. ennreal (pmf p x)\<partial>count_space UNIV = ennreal (1 - pmf p y)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
have "ennreal (inverse a) * ennreal (1 - pmf p y) = ennreal ((1 - pmf p y) / a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (inverse a) * ennreal (1 - pmf p y) = ennreal ((1 - pmf p y) / a)
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
0 < a

goal (1 subgoal):
 1. ennreal (inverse a) * ennreal (1 - pmf p y) = ennreal ((1 - pmf p y) / a)
[PROOF STEP]
by (subst ennreal_mult' [symmetric]) (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
ennreal (inverse a) * ennreal (1 - pmf p y) = ennreal ((1 - pmf p y) / a)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal (inverse a) * ennreal (1 - pmf p y) = ennreal ((1 - pmf p y) / a)

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
have "(1 - pmf p y) / a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - pmf p y) / a = 1
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
pmf p y < 1

goal (1 subgoal):
 1. (1 - pmf p y) / a = 1
[PROOF STEP]
by (simp add: a_def)
[PROOF STATE]
proof (state)
this:
(1 - pmf p y) / a = 1

goal (2 subgoals):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
 2. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = ennreal 1
[PROOF STEP]
show "(\<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV) = 1"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = ennreal 1

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (if x = y then 0 else pmf p x / a) \<partial>count_space UNIV = 1

goal (1 subgoal):
 1. \<And>x. 0 \<le> (if x = y then 0 else pmf p x / a)
[PROOF STEP]
qed (insert a, auto)
[PROOF STATE]
proof (state)
this:
pmf q ?z = (if ?z = y then 0 else pmf p ?z / a)

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "mix_pmf (1 - pmf p y) q (return_pmf y) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf (1 - pmf p y) q (return_pmf y) = p
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
pmf p y < 1

goal (1 subgoal):
 1. mix_pmf (1 - pmf p y) q (return_pmf y) = p
[PROOF STEP]
by (intro pmf_eqI) (auto simp: q pmf_mix pmf_le_1 a_def)
[PROOF STATE]
proof (state)
this:
mix_pmf (1 - pmf p y) q (return_pmf y) = p

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mix_pmf (1 - pmf p y) q (return_pmf y) = p

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "set_pmf q = set_pmf p - {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf q = set_pmf p - {y}
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
pmf p y < 1

goal (1 subgoal):
 1. set_pmf q = set_pmf p - {y}
[PROOF STEP]
by (auto simp: q set_pmf_eq a_def)
[PROOF STATE]
proof (state)
this:
set_pmf q = set_pmf p - {y}

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf a q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mix_pmf (1 - pmf p y) q (return_pmf y) = p
set_pmf q = set_pmf p - {y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mix_pmf (1 - pmf p y) q (return_pmf y) = p
set_pmf q = set_pmf p - {y}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of "1 - pmf p y" q] y assms
[PROOF STATE]
proof (prove)
using this:
mix_pmf (1 - pmf p y) q (return_pmf y) = p
set_pmf q = set_pmf p - {y}
\<lbrakk>1 - pmf p y \<in> {0<..<1}; set_pmf q = set_pmf p - {y}; p = mix_pmf (1 - pmf p y) q (return_pmf y)\<rbrakk> \<Longrightarrow> thesis
pmf p y < 1
y \<in> set_pmf p
set_pmf p - {y} \<noteq> {}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto simp: set_pmf_eq)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmf_mix_induct [consumes 2, case_names degenerate mix]:
  assumes "finite A" "set_pmf p \<subseteq> A"
  assumes degenerate: "\<And>x. x \<in> A \<Longrightarrow> P (return_pmf x)"
  assumes mix:        "\<And>p a y. set_pmf p \<subseteq> A \<Longrightarrow> a \<in> {0<..<1} \<Longrightarrow> y \<in> A \<Longrightarrow>
                         P p \<Longrightarrow> P (mix_pmf a p (return_pmf y))"
  shows "P p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P p
[PROOF STEP]
have "finite (set_pmf p)" "set_pmf p \<noteq> {}" "set_pmf p \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf p) &&& set_pmf p \<noteq> {} &&& set_pmf p \<subseteq> A
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
finite A
set_pmf p \<subseteq> A

goal (1 subgoal):
 1. finite (set_pmf p) &&& set_pmf p \<noteq> {} &&& set_pmf p \<subseteq> A
[PROOF STEP]
by (auto simp: set_pmf_not_empty dest: finite_subset)
[PROOF STATE]
proof (state)
this:
finite (set_pmf p)
set_pmf p \<noteq> {}
set_pmf p \<subseteq> A

goal (1 subgoal):
 1. P p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf p)
set_pmf p \<noteq> {}
set_pmf p \<subseteq> A

goal (1 subgoal):
 1. P p
[PROOF STEP]
proof (induction "set_pmf p" arbitrary: p rule: finite_ne_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x p. \<lbrakk>{x} = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
 2. \<And>x F p. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>p. \<lbrakk>F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p; insert x F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
case (singleton x p)
[PROOF STATE]
proof (state)
this:
{x} = set_pmf p
set_pmf p \<subseteq> A

goal (2 subgoals):
 1. \<And>x p. \<lbrakk>{x} = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
 2. \<And>x F p. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>p. \<lbrakk>F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p; insert x F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
hence "p = return_pmf x"
[PROOF STATE]
proof (prove)
using this:
{x} = set_pmf p
set_pmf p \<subseteq> A

goal (1 subgoal):
 1. p = return_pmf x
[PROOF STEP]
using set_pmf_subset_singleton[of p x]
[PROOF STATE]
proof (prove)
using this:
{x} = set_pmf p
set_pmf p \<subseteq> A
(set_pmf p \<subseteq> {x}) = (p = return_pmf x)

goal (1 subgoal):
 1. p = return_pmf x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = return_pmf x

goal (2 subgoals):
 1. \<And>x p. \<lbrakk>{x} = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
 2. \<And>x F p. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>p. \<lbrakk>F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p; insert x F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
p = return_pmf x

goal (1 subgoal):
 1. P p
[PROOF STEP]
using singleton
[PROOF STATE]
proof (prove)
using this:
p = return_pmf x
{x} = set_pmf p
set_pmf p \<subseteq> A

goal (1 subgoal):
 1. P p
[PROOF STEP]
by (auto intro: degenerate)
[PROOF STATE]
proof (state)
this:
P p

goal (1 subgoal):
 1. \<And>x F p. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>p. \<lbrakk>F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p; insert x F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F p. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>p. \<lbrakk>F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p; insert x F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
case (insert x B p)
[PROOF STATE]
proof (state)
this:
finite B
B \<noteq> {}
x \<notin> B
\<lbrakk>B = set_pmf ?p; set_pmf ?p \<subseteq> A\<rbrakk> \<Longrightarrow> P ?p
insert x B = set_pmf p
set_pmf p \<subseteq> A

goal (1 subgoal):
 1. \<And>x F p. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>p. \<lbrakk>F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p; insert x F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
from insert.hyps
[PROOF STATE]
proof (chain)
picking this:
finite B
B \<noteq> {}
x \<notin> B
\<lbrakk>B = set_pmf ?p; set_pmf ?p \<subseteq> A\<rbrakk> \<Longrightarrow> P ?p
insert x B = set_pmf p
[PROOF STEP]
have "x \<in> set_pmf p" "set_pmf p - {x} \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
finite B
B \<noteq> {}
x \<notin> B
\<lbrakk>B = set_pmf ?p; set_pmf ?p \<subseteq> A\<rbrakk> \<Longrightarrow> P ?p
insert x B = set_pmf p

goal (1 subgoal):
 1. x \<in> set_pmf p &&& set_pmf p - {x} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set_pmf p
set_pmf p - {x} \<noteq> {}

goal (1 subgoal):
 1. \<And>x F p. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>p. \<lbrakk>F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p; insert x F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
from mix_pmf_partition[OF this]
[PROOF STATE]
proof (chain)
picking this:
(\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {x}; p = mix_pmf a q (return_pmf x)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain a q
      where decomp: "a \<in> {0<..<1}" "set_pmf q = set_pmf p - {x}"
        "p = mix_pmf a q (return_pmf x)"
[PROOF STATE]
proof (prove)
using this:
(\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {x}; p = mix_pmf a q (return_pmf x)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>a q. \<lbrakk>a \<in> {0<..<1}; set_pmf q = set_pmf p - {x}; p = mix_pmf a q (return_pmf x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> {0<..<1}
set_pmf q = set_pmf p - {x}
p = mix_pmf a q (return_pmf x)

goal (1 subgoal):
 1. \<And>x F p. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>p. \<lbrakk>F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p; insert x F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
have "P (mix_pmf a q (return_pmf x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (mix_pmf a q (return_pmf x))
[PROOF STEP]
using insert.prems decomp(1) insert.hyps
[PROOF STATE]
proof (prove)
using this:
set_pmf p \<subseteq> A
a \<in> {0<..<1}
finite B
B \<noteq> {}
x \<notin> B
\<lbrakk>B = set_pmf ?p; set_pmf ?p \<subseteq> A\<rbrakk> \<Longrightarrow> P ?p
insert x B = set_pmf p

goal (1 subgoal):
 1. P (mix_pmf a q (return_pmf x))
[PROOF STEP]
by (intro mix insert) (auto simp: decomp(2))
[PROOF STATE]
proof (state)
this:
P (mix_pmf a q (return_pmf x))

goal (1 subgoal):
 1. \<And>x F p. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<And>p. \<lbrakk>F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p; insert x F = set_pmf p; set_pmf p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
with decomp(3)
[PROOF STATE]
proof (chain)
picking this:
p = mix_pmf a q (return_pmf x)
P (mix_pmf a q (return_pmf x))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p = mix_pmf a q (return_pmf x)
P (mix_pmf a q (return_pmf x))

goal (1 subgoal):
 1. P p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmf_mix_induct' [consumes 2, case_names degenerate mix]:
  assumes "finite A" "set_pmf p \<subseteq> A"
  assumes degenerate: "\<And>x. x \<in> A \<Longrightarrow> P (return_pmf x)"
  assumes mix:        "\<And>p q a. set_pmf p \<subseteq> A \<Longrightarrow> set_pmf q \<subseteq> A \<Longrightarrow> a \<in> {0<..<1} \<Longrightarrow>
                         P p \<Longrightarrow> P q \<Longrightarrow> P (mix_pmf a p q)"
  shows "P p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
set_pmf p \<subseteq> A
?x \<in> A \<Longrightarrow> P (return_pmf ?x)
\<lbrakk>set_pmf ?p \<subseteq> A; set_pmf ?q \<subseteq> A; ?a \<in> {0<..<1}; P ?p; P ?q\<rbrakk> \<Longrightarrow> P (mix_pmf ?a ?p ?q)

goal (1 subgoal):
 1. P p
[PROOF STEP]
by (induct p rule: pmf_mix_induct)(auto)+


[STATEMENT]
lemma finite_sum_distribute_mix_pmf:
  assumes "finite (set_pmf (mix_pmf a p q))"
  assumes "finite (set_pmf p)"
  assumes "finite (set_pmf q)"
  shows "(\<Sum>i \<in> set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) i) = (\<Sum>i\<in>set_pmf p.  a * pmf p i) + (\<Sum>i\<in>set_pmf q. (1-a) * pmf q i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = (\<Sum>i\<in>set_pmf p. a * pmf p i) + (\<Sum>i\<in>set_pmf q. (1 - a) * pmf q i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = (\<Sum>i\<in>set_pmf p. a * pmf p i) + (\<Sum>i\<in>set_pmf q. (1 - a) * pmf q i)
[PROOF STEP]
have fst: "(\<Sum>i \<in> set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) i) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = 1
[PROOF STEP]
using sum_pmf_eq_1 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; set_pmf ?p \<subseteq> ?A\<rbrakk> \<Longrightarrow> sum (pmf ?p) ?A = 1
finite (set_pmf (mix_pmf a p q))
finite (set_pmf p)
finite (set_pmf q)

goal (1 subgoal):
 1. sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = 1

goal (1 subgoal):
 1. sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = (\<Sum>i\<in>set_pmf p. a * pmf p i) + (\<Sum>i\<in>set_pmf q. (1 - a) * pmf q i)
[PROOF STEP]
have "(\<Sum>i\<in>set_pmf p.  a * pmf p i) = a * (\<Sum>i\<in>set_pmf p. pmf p i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf p. a * pmf p i) = a * sum (pmf p) (set_pmf p)
[PROOF STEP]
by (simp add: sum_distrib_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf p. a * pmf p i) = a * sum (pmf p) (set_pmf p)

goal (1 subgoal):
 1. sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = (\<Sum>i\<in>set_pmf p. a * pmf p i) + (\<Sum>i\<in>set_pmf q. (1 - a) * pmf q i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf p. a * pmf p i) = a * sum (pmf p) (set_pmf p)

goal (1 subgoal):
 1. sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = (\<Sum>i\<in>set_pmf p. a * pmf p i) + (\<Sum>i\<in>set_pmf q. (1 - a) * pmf q i)
[PROOF STEP]
have "... = a * 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * sum (pmf p) (set_pmf p) = a * 1
[PROOF STEP]
using assms sum_pmf_eq_1
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf (mix_pmf a p q))
finite (set_pmf p)
finite (set_pmf q)
\<lbrakk>finite ?A; set_pmf ?p \<subseteq> ?A\<rbrakk> \<Longrightarrow> sum (pmf ?p) ?A = 1

goal (1 subgoal):
 1. a * sum (pmf p) (set_pmf p) = a * 1
[PROOF STEP]
by (simp add: sum_pmf_eq_1)
[PROOF STATE]
proof (state)
this:
a * sum (pmf p) (set_pmf p) = a * 1

goal (1 subgoal):
 1. sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = (\<Sum>i\<in>set_pmf p. a * pmf p i) + (\<Sum>i\<in>set_pmf q. (1 - a) * pmf q i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a * sum (pmf p) (set_pmf p) = a * 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a * sum (pmf p) (set_pmf p) = a * 1

goal (1 subgoal):
 1. sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = (\<Sum>i\<in>set_pmf p. a * pmf p i) + (\<Sum>i\<in>set_pmf q. (1 - a) * pmf q i)
[PROOF STEP]
by (metis fst add.assoc add_diff_cancel_left' add_uminus_conv_diff assms(3)
        mult.right_neutral order_refl sum_distrib_left sum_pmf_eq_1)
[PROOF STATE]
proof (state)
this:
sum (pmf (mix_pmf a p q)) (set_pmf (mix_pmf a p q)) = (\<Sum>i\<in>set_pmf p. a * pmf p i) + (\<Sum>i\<in>set_pmf q. (1 - a) * pmf q i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distribute_alpha_over_sum:
  shows "(\<Sum>i\<in>set_pmf T. a * pmf p i * f i) = a * (\<Sum>i\<in>set_pmf T. pmf p i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf T. a * pmf p i * f i) = a * (\<Sum>i\<in>set_pmf T. pmf p i * f i)
[PROOF STEP]
by (metis (mono_tags, lifting) semiring_normalization_rules(18) sum.cong sum_distrib_left)


[STATEMENT]
lemma sum_over_subset_pmf_support:
  assumes "finite T"
  assumes "set_pmf p \<subseteq> T"
  shows "(\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
consider (eq) "set_pmf p = T" | (sub) "set_pmf p \<subset> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_pmf p = T \<Longrightarrow> thesis; set_pmf p \<subset> T \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite T
set_pmf p \<subseteq> T

goal (1 subgoal):
 1. \<lbrakk>set_pmf p = T \<Longrightarrow> thesis; set_pmf p \<subset> T \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>set_pmf p = T \<Longrightarrow> ?thesis; set_pmf p \<subset> T \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>set_pmf p = T \<Longrightarrow> ?thesis; set_pmf p \<subset> T \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set_pmf p = T \<Longrightarrow> ?thesis; set_pmf p \<subset> T \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
case sub
[PROOF STATE]
proof (state)
this:
set_pmf p \<subset> T

goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
define A where "A = T - (set_pmf p)"
[PROOF STATE]
proof (state)
this:
A = T - set_pmf p

goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
have "finite (set_pmf p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf p)
[PROOF STEP]
using assms(1) assms(2) finite_subset
[PROOF STATE]
proof (prove)
using this:
finite T
set_pmf p \<subseteq> T
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (set_pmf p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set_pmf p)

goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (set_pmf p)

goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
have "finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A
[PROOF STEP]
using A_def assms(1)
[PROOF STATE]
proof (prove)
using this:
A = T - set_pmf p
finite T

goal (1 subgoal):
 1. finite A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite A

goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite A

goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
have "A \<inter> set_pmf p = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> set_pmf p = {}
[PROOF STEP]
using A_def assms(1)
[PROOF STATE]
proof (prove)
using this:
A = T - set_pmf p
finite T

goal (1 subgoal):
 1. A \<inter> set_pmf p = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A \<inter> set_pmf p = {}

goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (set_pmf p)
finite A
A \<inter> set_pmf p = {}
[PROOF STEP]
have *: "(\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i) + (\<Sum>i\<in>A. a * pmf p i * f i)"
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf p)
finite A
A \<inter> set_pmf p = {}

goal (1 subgoal):
 1. (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i) + (\<Sum>i\<in>A. a * pmf p i * f i)
[PROOF STEP]
using sum.union_disjoint
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf p)
finite A
A \<inter> set_pmf p = {}
\<lbrakk>finite ?A; finite ?B; ?A \<inter> ?B = {}\<rbrakk> \<Longrightarrow> sum ?g (?A \<union> ?B) = sum ?g ?A + sum ?g ?B

goal (1 subgoal):
 1. (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i) + (\<Sum>i\<in>A. a * pmf p i * f i)
[PROOF STEP]
by (metis (no_types) A_def Un_Diff_cancel2
          Un_absorb2 assms(2) inf.commute inf_sup_aci(5) sum.union_disjoint)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i) + (\<Sum>i\<in>A. a * pmf p i * f i)

goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
have "\<forall>e \<in> A. pmf p e = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>A. pmf p e = 0
[PROOF STEP]
by (simp add: A_def pmf_eq_0_set_pmf)
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>A. pmf p e = 0

goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
hence "(\<Sum>i\<in>A. a * pmf p i * f i) = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>A. pmf p e = 0

goal (1 subgoal):
 1. (\<Sum>i\<in>A. a * pmf p i * f i) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>A. a * pmf p i * f i) = 0

goal (2 subgoals):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
 2. set_pmf p \<subset> T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>A. a * pmf p i * f i) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>A. a * pmf p i * f i) = 0

goal (1 subgoal):
 1. (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
by (simp add: "*")
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)

goal (1 subgoal):
 1. set_pmf p = T \<Longrightarrow> (\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)
[PROOF STEP]
qed (auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>T. a * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. a * pmf p i * f i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expected_value_mix_pmf_distrib:
  assumes "finite (set_pmf p)"
    and "finite (set_pmf q)"
  assumes "a \<in> {0<..<1}"
  shows "measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1-a) * measure_pmf.expectation q f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have fn: "finite (set_pmf (mix_pmf a p q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf (mix_pmf a p q))
[PROOF STEP]
using mix_pmf_preserves_finite_support assms less_eq_real_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> {0..1}; finite (set_pmf ?p); finite (set_pmf ?q)\<rbrakk> \<Longrightarrow> finite (set_pmf (mix_pmf ?a ?p ?q))
finite (set_pmf p)
finite (set_pmf q)
a \<in> {0<..<1}
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

goal (1 subgoal):
 1. finite (set_pmf (mix_pmf a p q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set_pmf (mix_pmf a p q))

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have subsets: "set_pmf p \<subseteq> set_pmf (mix_pmf a p q)" "set_pmf q \<subseteq> set_pmf (mix_pmf a p q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_pmf p \<subseteq> set_pmf (mix_pmf a p q) &&& set_pmf q \<subseteq> set_pmf (mix_pmf a p q)
[PROOF STEP]
using assms assms set_pmf_mix
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf p)
finite (set_pmf q)
a \<in> {0<..<1}
finite (set_pmf p)
finite (set_pmf q)
a \<in> {0<..<1}
?a \<in> {0<..<1} \<Longrightarrow> set_pmf (mix_pmf ?a ?p ?q) = set_pmf ?p \<union> set_pmf ?q

goal (1 subgoal):
 1. set_pmf p \<subseteq> set_pmf (mix_pmf a p q) &&& set_pmf q \<subseteq> set_pmf (mix_pmf a p q)
[PROOF STEP]
by(fastforce)+
[PROOF STATE]
proof (state)
this:
set_pmf p \<subseteq> set_pmf (mix_pmf a p q)
set_pmf q \<subseteq> set_pmf (mix_pmf a p q)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have *: "(\<Sum>i \<in> set_pmf (mix_pmf a p q). a * pmf p i * f i) = a * (\<Sum>i \<in> set_pmf (mix_pmf a p q). pmf p i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i) = a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i)
[PROOF STEP]
by (metis (mono_tags, lifting) mult.assoc sum.cong sum_distrib_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i) = a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have **: "(\<Sum>i \<in> set_pmf (mix_pmf a p q). (1-a) * pmf q i * f i) = (1-a) * (\<Sum>i \<in> set_pmf (mix_pmf a p q). pmf q i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i) = (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i)
[PROOF STEP]
using distribute_alpha_over_sum[of "(1 - a)" q f "(mix_pmf a p q)"]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i) = (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i)

goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i) = (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i) = (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have ***: "measure_pmf.expectation (mix_pmf a p q) f = (\<Sum>i \<in> set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) i * f i)
[PROOF STEP]
by (metis fn pmf_integral_code_unfold pmf_integral_pmf_set_integral
        pmf_set_integral_code_alt_finite)
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (mix_pmf a p q) f = (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (mix_pmf a p q) f = (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have g: "... = (\<Sum>i \<in> set_pmf (mix_pmf a p q). (a * pmf p i + (1-a) * pmf q i) * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) i * f i) = (\<Sum>i\<in>set_pmf (mix_pmf a p q). (a * pmf p i + (1 - a) * pmf q i) * f i)
[PROOF STEP]
using pmf_mix[of a p q] assms(3)
[PROOF STATE]
proof (prove)
using this:
a \<in> {0..1} \<Longrightarrow> pmf (mix_pmf a p q) ?x = a * pmf p ?x + (1 - a) * pmf q ?x
a \<in> {0<..<1}

goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) i * f i) = (\<Sum>i\<in>set_pmf (mix_pmf a p q). (a * pmf p i + (1 - a) * pmf q i) * f i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) i * f i) = (\<Sum>i\<in>set_pmf (mix_pmf a p q). (a * pmf p i + (1 - a) * pmf q i) * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf (mix_pmf a p q) i * f i) = (\<Sum>i\<in>set_pmf (mix_pmf a p q). (a * pmf p i + (1 - a) * pmf q i) * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have ****: "... =  (\<Sum>i \<in> set_pmf (mix_pmf a p q). a * pmf p i * f i + (1-a) * pmf q i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). (a * pmf p i + (1 - a) * pmf q i) * f i) = (\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i + (1 - a) * pmf q i * f i)
[PROOF STEP]
by (simp add: mult.commute ring_class.ring_distribs(1))
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). (a * pmf p i + (1 - a) * pmf q i) * f i) = (\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i + (1 - a) * pmf q i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). (a * pmf p i + (1 - a) * pmf q i) * f i) = (\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i + (1 - a) * pmf q i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have f: "... = (\<Sum>i \<in> set_pmf (mix_pmf a p q). a * pmf p i * f i) + (\<Sum>i \<in> set_pmf (mix_pmf a p q). (1-a) * pmf q i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i + (1 - a) * pmf q i * f i) = (\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i) + (\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i)
[PROOF STEP]
by (simp add: sum.distrib)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i + (1 - a) * pmf q i * f i) = (\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i) + (\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i + (1 - a) * pmf q i * f i) = (\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i) + (\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have "... = a * (\<Sum>i \<in> set_pmf (mix_pmf a p q). pmf p i * f i) + (1-a) * (\<Sum>i \<in> set_pmf (mix_pmf a p q). pmf q i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i) + (\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i) = a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i)
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i) = a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i)
(\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i) = (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i)

goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i) + (\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i) = a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i) + (\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i) = a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). a * pmf p i * f i) + (\<Sum>i\<in>set_pmf (mix_pmf a p q). (1 - a) * pmf q i * f i) = a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have h: "... =  a * (\<Sum>i \<in> set_pmf p. pmf p i * f i) + (1-a) * (\<Sum>i \<in> set_pmf q. pmf q i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i)
[PROOF STEP]
have "(\<Sum>i \<in> set_pmf (mix_pmf a p q). pmf p i * f i) = (\<Sum>i \<in> set_pmf p. pmf p i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) = (\<Sum>i\<in>set_pmf p. pmf p i * f i)
[PROOF STEP]
using subsets sum_over_subset_pmf_support[of "(mix_pmf a p q)" p 1 f] fn
[PROOF STATE]
proof (prove)
using this:
set_pmf p \<subseteq> set_pmf (mix_pmf a p q)
set_pmf q \<subseteq> set_pmf (mix_pmf a p q)
\<lbrakk>finite (set_pmf (mix_pmf a p q)); set_pmf p \<subseteq> set_pmf (mix_pmf a p q)\<rbrakk> \<Longrightarrow> (\<Sum>i\<in>set_pmf (mix_pmf a p q). 1 * pmf p i * f i) = (\<Sum>i\<in>set_pmf p. 1 * pmf p i * f i)
finite (set_pmf (mix_pmf a p q))

goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) = (\<Sum>i\<in>set_pmf p. pmf p i * f i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) = (\<Sum>i\<in>set_pmf p. pmf p i * f i)

goal (1 subgoal):
 1. a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) = (\<Sum>i\<in>set_pmf p. pmf p i * f i)

goal (1 subgoal):
 1. a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i)
[PROOF STEP]
have "(\<Sum>i \<in> set_pmf (mix_pmf a p q). pmf q i * f i) = (\<Sum>i \<in> set_pmf q. pmf q i * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = (\<Sum>i\<in>set_pmf q. pmf q i * f i)
[PROOF STEP]
using subsets sum_over_subset_pmf_support[of "(mix_pmf a p q)" q 1 f] fn
[PROOF STATE]
proof (prove)
using this:
set_pmf p \<subseteq> set_pmf (mix_pmf a p q)
set_pmf q \<subseteq> set_pmf (mix_pmf a p q)
\<lbrakk>finite (set_pmf (mix_pmf a p q)); set_pmf q \<subseteq> set_pmf (mix_pmf a p q)\<rbrakk> \<Longrightarrow> (\<Sum>i\<in>set_pmf (mix_pmf a p q). 1 * pmf q i * f i) = (\<Sum>i\<in>set_pmf q. 1 * pmf q i * f i)
finite (set_pmf (mix_pmf a p q))

goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = (\<Sum>i\<in>set_pmf q. pmf q i * f i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = (\<Sum>i\<in>set_pmf q. pmf q i * f i)

goal (1 subgoal):
 1. a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) = (\<Sum>i\<in>set_pmf p. pmf p i * f i)
(\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = (\<Sum>i\<in>set_pmf q. pmf q i * f i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) = (\<Sum>i\<in>set_pmf p. pmf p i * f i)
(\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = (\<Sum>i\<in>set_pmf q. pmf q i * f i)

goal (1 subgoal):
 1. a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i)
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf (mix_pmf a p q). pmf q i * f i) = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
measure_pmf.expectation (mix_pmf a p q) f = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
measure_pmf.expectation (mix_pmf a p q) f = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i)

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i) \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have "(\<Sum>i\<in>set_pmf q. pmf q i * f i) = measure_pmf.expectation q f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf q. pmf q i * f i) = measure_pmf.expectation q f
[PROOF STEP]
by (metis (full_types) assms(2) pmf_integral_code_unfold pmf_integral_pmf_set_integral pmf_set_integral_code_alt_finite)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf q. pmf q i * f i) = measure_pmf.expectation q f

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i) \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf q. pmf q i * f i) = measure_pmf.expectation q f

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i) \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have "(\<Sum>i\<in>set_pmf p. pmf p i * f i) = measure_pmf.expectation p f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>set_pmf p. pmf p i * f i) = measure_pmf.expectation p f
[PROOF STEP]
by (metis (full_types) assms(1) pmf_integral_code_unfold pmf_integral_pmf_set_integral pmf_set_integral_code_alt_finite)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>set_pmf p. pmf p i * f i) = measure_pmf.expectation p f

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * (\<Sum>i\<in>set_pmf p. pmf p i * f i) + (1 - a) * (\<Sum>i\<in>set_pmf q. pmf q i * f i) \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<in>set_pmf q. pmf q i * f i) = measure_pmf.expectation q f
(\<Sum>i\<in>set_pmf p. pmf p i * f i) = measure_pmf.expectation p f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>set_pmf q. pmf q i * f i) = measure_pmf.expectation q f
(\<Sum>i\<in>set_pmf p. pmf p i * f i) = measure_pmf.expectation p f

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
by (simp add: "*" "**" "***" "****" f g h)
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expected_value_mix_pmf:
  assumes "finite (set_pmf p)"
    and "finite (set_pmf q)"
  assumes "a \<in> {0..1}"
  shows "measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1-a) * measure_pmf.expectation q f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
consider (0) "a = 0" | (b) "a \<in> {0<..<1}" | (1) "a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = 0 \<Longrightarrow> thesis; a \<in> {0<..<1} \<Longrightarrow> thesis; a = 1 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms(3) less_eq_real_def
[PROOF STATE]
proof (prove)
using this:
a \<in> {0..1}
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

goal (1 subgoal):
 1. \<lbrakk>a = 0 \<Longrightarrow> thesis; a \<in> {0<..<1} \<Longrightarrow> thesis; a = 1 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>a = 0 \<Longrightarrow> ?thesis; a \<in> {0<..<1} \<Longrightarrow> ?thesis; a = 1 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a = 0 \<Longrightarrow> ?thesis; a \<in> {0<..<1} \<Longrightarrow> ?thesis; a = 1 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a = 0 \<Longrightarrow> ?thesis; a \<in> {0<..<1} \<Longrightarrow> ?thesis; a = 1 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. a = 0 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 2. a \<in> {0<..<1} \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 3. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
a = 0

goal (3 subgoals):
 1. a = 0 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 2. a \<in> {0<..<1} \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 3. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have "(mix_pmf a p q) = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf a p q = q
[PROOF STEP]
using 0 pmf_mix_0
[PROOF STATE]
proof (prove)
using this:
a = 0
mix_pmf 0 ?p ?q = ?q

goal (1 subgoal):
 1. mix_pmf a p q = q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mix_pmf a p q = q

goal (3 subgoals):
 1. a = 0 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 2. a \<in> {0<..<1} \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 3. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have "measure_pmf.expectation q f = (1-a) * measure_pmf.expectation q f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation q f = (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
by (simp add: 0)
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation q f = (1 - a) * measure_pmf.expectation q f

goal (3 subgoals):
 1. a = 0 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 2. a \<in> {0<..<1} \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 3. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
a = 0

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f

goal (2 subgoals):
 1. a \<in> {0<..<1} \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 2. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> {0<..<1} \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 2. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
case b
[PROOF STATE]
proof (state)
this:
a \<in> {0<..<1}

goal (2 subgoals):
 1. a \<in> {0<..<1} \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
 2. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
using assms(1) assms(2) b expected_value_mix_pmf_distrib
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf p)
finite (set_pmf q)
a \<in> {0<..<1}
\<lbrakk>finite (set_pmf ?p); finite (set_pmf ?q); ?a \<in> {0<..<1}\<rbrakk> \<Longrightarrow> measure_pmf.expectation (mix_pmf ?a ?p ?q) ?f = ?a * measure_pmf.expectation ?p ?f + (1 - ?a) * measure_pmf.expectation ?q ?f

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f

goal (1 subgoal):
 1. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
a = 1

goal (1 subgoal):
 1. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
have "(mix_pmf a p q) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf a p q = p
[PROOF STEP]
using 1 pmf_mix_0
[PROOF STATE]
proof (prove)
using this:
a = 1
mix_pmf 0 ?p ?q = ?q

goal (1 subgoal):
 1. mix_pmf a p q = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mix_pmf a p q = p

goal (1 subgoal):
 1. a = 1 \<Longrightarrow> measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mix_pmf a p q = p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mix_pmf a p q = p

goal (1 subgoal):
 1. measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f
[PROOF STEP]
by (simp add: "1")
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (mix_pmf a p q) f = a * measure_pmf.expectation p f + (1 - a) * measure_pmf.expectation q f

goal:
No subgoals!
[PROOF STEP]
qed