As an example, we apply the strong law to the proportion of successes in an independent sequence
of coin flips with success probability \<open>p\<close>. We will show that proportion of successful coin
flips among the first \<open>n\<close> attempts almost surely converges to \<open>p\<close> as \<open>n \<rightarrow> \<infinity>\<close>.
\<close>
(* TODO: Move *)
lemma (in prob_space) indep_vars_iff_distr_eq_PiM':
fixes I :: "'i set" and X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b"
assumes "I \<noteq> {}"
assumes rv: "\<And>i. i \<in> I \<Longrightarrow> random_variable (M' i) (X i)"
shows "indep_vars M' X I \<longleftrightarrow>
distr M (\<Pi>\<^sub>M i\<in>I. M' i) (\<lambda>x. \<lambda>i\<in>I. X i x) = (\<Pi>\<^sub>M i\<in>I. distr M (M' i) (X i))"
proof -
from assms obtain j where j: "j \<in> I"
by auto
define N' where "N' = (\<lambda>i. if i \<in> I then M' i else M' j)"
define Y where "Y = (\<lambda>i. if i \<in> I then X i else X j)"
have rv: "random_variable (N' i) (Y i)" for i
using j by (auto simp: N'_def Y_def intro: assms)
have "indep_vars M' X I = indep_vars N' Y I"
by (intro indep_vars_cong) (auto simp: N'_def Y_def)
also have "\<dots> \<longleftrightarrow> distr M (\<Pi>\<^sub>M i\<in>I. N' i) (\<lambda>x. \<lambda>i\<in>I. Y i x) = (\<Pi>\<^sub>M i\<in>I. distr M (N' i) (Y i))"
by (intro indep_vars_iff_distr_eq_PiM rv assms)
also have "(\<Pi>\<^sub>M i\<in>I. N' i) = (\<Pi>\<^sub>M i\<in>I. M' i)"
by (intro PiM_cong) (simp_all add: N'_def)
also have "(\<lambda>x. \<lambda>i\<in>I. Y i x) = (\<lambda>x. \<lambda>i\<in>I. X i x)"
by (simp_all add: Y_def fun_eq_iff)
also have "(\<Pi>\<^sub>M i\<in>I. distr M (N' i) (Y i)) = (\<Pi>\<^sub>M i\<in>I. distr M (M' i) (X i))"
by (intro PiM_cong distr_cong) (simp_all add: N'_def Y_def)
finally show ?thesis .
qed
(* TODO: Move *)
lemma indep_vars_PiM_components:
assumes "\<And>i. i \<in> A \<Longrightarrow> prob_space (M i)"
shows "prob_space.indep_vars (PiM A M) M (\<lambda>i f. f i) A"
proof (cases "A = {}")
case False
have "distr (Pi\<^sub>M A M) (Pi\<^sub>M A M) (\<lambda>x. restrict x A) = distr (Pi\<^sub>M A M) (Pi\<^sub>M A M) (\<lambda>x. x)"
by (intro distr_cong) (auto simp: restrict_def space_PiM PiE_def extensional_def Pi_def)
also have "\<dots> = Pi\<^sub>M A M"
by simp
also have "\<dots> = Pi\<^sub>M A (\<lambda>i. distr (Pi\<^sub>M A M) (M i) (\<lambda>f. f i))"
by (intro PiM_cong refl, subst distr_PiM_component) (auto simp: assms)
finally show ?thesis
by (subst prob_space.indep_vars_iff_distr_eq_PiM') (simp_all add: prob_space_PiM assms False)
next
case True
interpret prob_space "PiM A M"
by (intro prob_space_PiM assms)
show ?thesis
unfolding indep_vars_def indep_sets_def by (auto simp: True)
qed
(* TODO: Move *)
lemma indep_vars_PiM_components':
assumes "\<And>i. i \<in> A \<Longrightarrow> prob_space (M i)"
assumes "\<And>i. i \<in> A \<Longrightarrow> g i \<in> M i \<rightarrow>\<^sub>M N i"
shows "prob_space.indep_vars (PiM A M) N (\<lambda>i f. g i (f i)) A"
by (rule prob_space.indep_vars_compose2[OF prob_space_PiM indep_vars_PiM_components])
(use assms in simp_all)
(* TODO: Move *)
lemma integrable_bernoulli_pmf [intro]:
fixes f :: "bool \<Rightarrow> 'a :: {banach, second_countable_topology}"
shows "integrable (bernoulli_pmf p) f"
by (rule integrable_measure_pmf_finite) auto
(* TODO: Move *)
lemma expectation_bernoulli_pmf:
fixes f :: "bool \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes p: "p \<in> {0..1}"
shows "measure_pmf.expectation (bernoulli_pmf p) f = p *\<^sub>R f True + (1 - p) *\<^sub>R f False"
using p by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
experiment
fixes p :: real
assumes p: "p \<in> {0..1}"
begin
definition M :: "(nat \<Rightarrow> bool) measure"