(* 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 begin 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}i∈I. M' i) (λx. λi∈I. X i x) = (Π⇩_{M}i∈I. 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}i∈I. N' i) (λx. λi∈I. Y i x) = (Π⇩_{M}i∈I. distr M (N' i) (Y i))" by (intro indep_vars_iff_distr_eq_PiM rv assms) also have "(Π⇩_{M}i∈I. N' i) = (Π⇩_{M}i∈I. M' i)" by (intro PiM_cong) (simp_all add: N'_def) also have "(λx. λi∈I. Y i x) = (λx. λi∈I. X i x)" by (simp_all add: Y_def fun_eq_iff) also have "(Π⇩_{M}i∈I. distr M (N' i) (Y i)) = (Π⇩_{M}i∈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 "⋀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 (Pi⇩_{M}A M) (Pi⇩_{M}A M) (λx. restrict x A) = distr (Pi⇩_{M}A M) (Pi⇩_{M}A M) (λx. x)" by (intro distr_cong) (auto simp: restrict_def space_PiM PiE_def extensional_def Pi_def) also have "… = Pi⇩_{M}A M" by simp also have "… = Pi⇩_{M}A (λi. distr (Pi⇩_{M}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) 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 "⋀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) experiment fixes p :: real assumes p: "p ∈ {0..1}" begin 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 . qed 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 qed 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 . qed 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 . qed 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 . qed end end