[STATEMENT]
lemma  bernoulli_stream_element_prob_rec':
  fixes x
  assumes "M = bernoulli_stream p"
and "0 \<le> p" and "p \<le> 1"
  shows "\<And> n. measure M {w\<in> space M. (stake (Suc n) w = stake (Suc n) x)} =
    (measure M {w\<in> space M. (stake n w = stake n x)} * prob_component p x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
have "ennreal (measure M {w\<in> space M. (stake (Suc n) w = stake (Suc n) x)}) =
    emeasure M {w\<in> space M. (stake (Suc n) w = stake (Suc n) x)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x}
[PROOF STEP]
by (metis (no_types, lifting) assms(1) bernoulli_stream_def emeasure_eq_ennreal_measure
        emeasure_space ennreal_top_neq_one neq_top_trans prob_space.emeasure_space_1
        prob_space.prob_space_stream_space prob_space_measure_pmf)
[PROOF STATE]
proof (state)
this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x}

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x}

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
have "... = (emeasure M {w\<in> space M. (stake n w = stake n x)} * prob_component p x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x} = emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n)
[PROOF STEP]
using bernoulli_stream_element_prob_rec assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M = bernoulli_stream ?p; 0 \<le> ?p; ?p \<le> 1\<rbrakk> \<Longrightarrow> emeasure ?M {w \<in> space ?M. stake (Suc ?n) w = stake (Suc ?n) ?x} = emeasure ?M {w \<in> space ?M. stake ?n w = stake ?n ?x} * ennreal (prob_component ?p ?x ?n)
M = bernoulli_stream p
0 \<le> p
p \<le> 1

goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x} = emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x} = emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n)

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x} = emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n)

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
have "... = (measure M {w\<in> space M. (stake n w = stake n x)} * prob_component p x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
have "prob_space M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space M
[PROOF STEP]
using assms(1) bernoulli_stream_def prob_space.prob_space_stream_space prob_space_measure_pmf
[PROOF STATE]
proof (prove)
using this:
M = bernoulli_stream p
bernoulli_stream ?p = stream_space (measure_pmf (bernoulli_pmf ?p))
prob_space ?M \<Longrightarrow> prob_space (stream_space ?M)
prob_space (measure_pmf ?p)

goal (1 subgoal):
 1. prob_space M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prob_space M

goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prob_space M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prob_space M

goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
by (simp add: ennreal_mult'' finite_measure.emeasure_eq_measure mult.commute prob_space_def)
[PROOF STATE]
proof (state)
this:
emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
have "ennreal (measure M {w\<in> space M. (stake (Suc n) w = stake (Suc n) x)}) =
    (measure M {w\<in> space M. (stake n w = stake n x)} * prob_component p x n)"
[PROOF STATE]
proof (prove)
using this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)

goal (1 subgoal):
 1. ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
thus "measure M {w\<in> space M. (stake (Suc n) w = stake (Suc n) x)} =
    (measure M {w\<in> space M. (stake n w = stake n x)} * prob_component p x n)"
[PROOF STATE]
proof (prove)
using this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)

goal (1 subgoal):
 1. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
using assms prob_component_def
[PROOF STATE]
proof (prove)
using this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
M = bernoulli_stream p
0 \<le> p
p \<le> 1
prob_component ?p ?w ?n = (if ?w !! ?n then ?p else 1 - ?p)

goal (1 subgoal):
 1. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n

goal:
No subgoals!
[PROOF STEP]
qed