Theory Laws_of_Large_Numbers_Example

   File:     Laws_of_Large_Numbers.thy
   Author:   Manuel Eberl, TU München
subsection ‹Example›
theory Laws_of_Large_Numbers_Example
  imports Laws_of_Large_Numbers

text ‹
  As an example, we apply the strong law to the proportion of successes in an independent sequence
  of coin flips with success probability p›. We will show that proportion of successful coin
  flips among the first n› attempts almost surely converges to p› as n → ∞›.

(* TODO: Move *)
lemma (in prob_space) indep_vars_iff_distr_eq_PiM':
  fixes I :: "'i set" and X :: "'i  'a  'b"
  assumes "I  {}"
  assumes rv: "i. i  I  random_variable (M' i) (X i)"
  shows "indep_vars M' X I 
           distr M (ΠM iI. M' i) (λx. λiI. X i x) = (ΠM iI. distr M (M' i) (X i))"
proof -
  from assms obtain j where j: "j  I"
    by auto
  define N' where "N' = (λi. if i  I then M' i else M' j)"
  define Y where "Y = (λi. if i  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 "  distr M (ΠM iI. N' i) (λx. λiI. Y i x) = (ΠM iI. distr M (N' i) (Y i))"
    by (intro indep_vars_iff_distr_eq_PiM rv assms)
  also have "(ΠM iI. N' i) = (ΠM iI. M' i)"
    by (intro PiM_cong) (simp_all add: N'_def)
  also have "(λx. λiI. Y i x) = (λx. λiI. X i x)"
    by (simp_all add: Y_def fun_eq_iff)
  also have "(ΠM iI. distr M (N' i) (Y i)) = (ΠM iI. distr M (M' i) (X i))"
    by (intro PiM_cong distr_cong) (simp_all add: N'_def Y_def)
  finally show ?thesis .

(* TODO: Move *)
lemma indep_vars_PiM_components:
  assumes "i. i  A  prob_space (M i)"
  shows   "prob_space.indep_vars (PiM A M) M (λi f. f i) A"
proof (cases "A = {}")
  case False
  have "distr (PiM A M) (PiM A M) (λx. restrict x A) = distr (PiM A M) (PiM A M) (λx. x)"
    by (intro distr_cong) (auto simp: restrict_def space_PiM PiE_def extensional_def Pi_def)
  also have " = PiM A M"
    by simp
  also have " = PiM A (λi. distr (PiM A M) (M i) (λ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)
  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)

(* TODO: Move *)
lemma indep_vars_PiM_components':
  assumes "i. i  A  prob_space (M i)"
  assumes "i. i  A  g i  M i M N i"
  shows   "prob_space.indep_vars (PiM A M) N (λ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  '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  'a :: {banach, second_countable_topology}"
  assumes p: "p  {0..1}"
  shows   "measure_pmf.expectation (bernoulli_pmf p) f = p *R f True + (1 - p) *R f False"
  using p by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)

  fixes p :: real
  assumes p: "p  {0..1}"

definition M :: "(nat  bool) measure"
  where "M = (ΠM i(UNIV :: nat set). measure_pmf (bernoulli_pmf p))"

definition X :: "nat  (nat  bool)  real"
  where "X = (λi f. if f i then 1 else 0)"

interpretation prob_space M
  unfolding M_def by (intro prob_space_PiM measure_pmf.prob_space_axioms)

lemma random_variable_component: "random_variable (count_space UNIV) (λf. f i)"
  unfolding X_def M_def by measurable

lemma random_variable_X [measurable]: "random_variable borel (X i)"
  unfolding X_def M_def by measurable

lemma distr_M_component: "distr M (count_space UNIV) (λf. f i) = measure_pmf (bernoulli_pmf p)"
proof -
  have "distr M (count_space UNIV) (λf. f i) = distr M (measure_pmf (bernoulli_pmf p)) (λf. f i)"
    by (rule distr_cong) auto
  also have " = measure_pmf (bernoulli_pmf p)"
    unfolding M_def by (subst distr_PiM_component) (simp_all add: measure_pmf.prob_space_axioms)
  finally show ?thesis .

lemma distr_M_X:
  "distr M borel (X i) = distr (measure_pmf (bernoulli_pmf p)) borel (λb. if b then 1 else 0)"
proof -
  have "distr M borel (X i) = distr (distr M (count_space UNIV) (λf. f i)) 
                                    borel (λb. if b then 1 else 0 :: real)"
    by (subst distr_distr) (auto simp: M_def X_def o_def)
  also note distr_M_component[of i]
  finally show ?thesis
    by simp

lemma X_has_expectation: "integrable M (X 0)"
proof -
  have "integrable (bernoulli_pmf p) (λb. if b then 1 else 0 :: real)"
    by auto
  also have "measure_pmf (bernoulli_pmf p) = distr M (count_space UNIV) (λf. f 0)"
    by (simp add: distr_M_component)
  also have "integrable  (λb. if b then 1 else 0 :: real) = integrable M (X 0)"
    unfolding X_def using random_variable_component by (subst integrable_distr_eq) auto
  finally show ?thesis .

lemma indep: "indep_vars (λ_. borel) X UNIV"
  unfolding M_def X_def
  by (rule indep_vars_PiM_components') (simp_all add: measure_pmf.prob_space_axioms)

lemma expectation_X: "expectation (X i) = p"
proof -
  have "expectation (X i) =
        lebesgue_integral (distr M (count_space UNIV) (λf. f i)) (λb. if b then 1 else 0 :: real)"
    by (subst integral_distr) (simp_all add: random_variable_component X_def)
  also have "distr M (count_space UNIV) (λx. x i) = measure_pmf (bernoulli_pmf p)"
    by (rule distr_M_component)
  also have "measure_pmf.expectation (bernoulli_pmf p) (λb. if b then 1 else 0 :: real) = p"
    using p by (subst integral_bernoulli_pmf) auto
  finally show ?thesis .

theorem "AE f in M. (λn. card {i. i < n  f i} / n)  p"
proof -
  have "AE f in M. (λn. (i<n. X i f) / real n)  expectation (X 0)"
    by (rule strong_law_of_large_numbers_iid)
       (use indep X_has_expectation in simp_all add: distr_M_X)
  also have "expectation (X 0) = p"
    by (simp add: expectation_X)
  also have "(λx n. i<n. X i x) = (λx n. i{i{..<n}. x i}. 1)"
    by (intro ext sum.mono_neutral_cong_right) (auto simp: X_def)
  also have " = (λx n. real (card {i. i < n  x i}))"
    by simp
  finally show ?thesis .