Theory Example_Coin_Toss

(*  Author:     Ata Keskin, TU München 
*)

theory Example_Coin_Toss
  imports Martingale "HOL-Probability.Stream_Space" "HOL-Probability.Probability_Mass_Function"
begin

section ‹Example: Coin Toss›

text ‹Consider a coin-tossing game, where the coin lands on heads with probability ‹p ∈ [0, 1]›. Assume that the gambler wins a fixed amount ‹c > 0› on a heads outcome 
      and loses the same amount ‹c› on a tails outcome. Let ‹(Xn)n∈ℕ› be a stochastic process, where ‹Xn› denotes the gambler's fortune after the ‹n›-th coin toss. 
      Then, we have the following three cases.›

text ‹1. If ‹p = 1/2›, it means the coin is fair and has an equal chance of landing heads or tails. 
      In this case, the gambler, on average, neither wins nor loses money over time. The expected value of the gambler's fortune stays the same over time. 
      Therefore, ‹(Xn)n∈ℕ› is a martingale.›
text ‹2. If ‹p ≥ 1/2› , it means the coin is biased in favor of heads. In this case, the gambler is more likely to win money on each bet. 
      Over time, the gambler's fortune tends to increase on average. 
      Therefore, ‹(Xn)n∈ℕ› is a submartingale.›

text ‹3. If ‹p ≤ 1/2› , it means the coin is biased in favor of tails. In this scenario, the gambler is more likely to lose money on each bet. 
      Over time, the gambler's fortune decreases on average. 
      Therefore, ‹(Xn)n∈ℕ› is a supermartingale.›

text ‹To formalize this example, we first consider a probability space consisting of infinite sequences of coin tosses.›

definition bernoulli_stream :: "real ⇒ (bool stream) measure" where
  "bernoulli_stream p = stream_space (measure_pmf (bernoulli_pmf p))"
                                  
lemma space_bernoulli_stream[simp]: "space (bernoulli_stream p) = UNIV" by (simp add: bernoulli_stream_def space_stream_space)

text ‹We define the fortune of the player at time term‹n› to be the number of heads minus number of tails.›

definition fortune :: "nat ⇒ bool stream ⇒ real" where
  "fortune n = (λs. ∑b ← stake (Suc n) s. if b then 1 else -1)"

definition toss :: "nat ⇒ bool stream ⇒ real" where
  "toss n = (λs. if snth s n then 1 else -1)"

lemma toss_indicator_def: "toss n = indicator {s. s !! n} - indicator {s. ¬ s !! n}"
  unfolding toss_def indicator_def by force

lemma range_toss: "range (toss n) = {-1, 1}"
proof -
  have "sconst True !! n" by simp
  moreover have "¬sconst False !! n" by simp
  ultimately have "∃x. x !! n" "∃x. ¬x !! n" by blast+
  thus ?thesis unfolding toss_def image_def by auto
qed

lemma vimage_toss: "toss n -` A = (if 1 ∈ A then {s. s !! n} else {}) ∪ (if -1 ∈ A then {s. ¬s !! n} else {})"
  unfolding vimage_def toss_def by auto

lemma fortune_Suc: "fortune (Suc n) s = fortune n s + toss (Suc n) s"
  by (induction n arbitrary: s) (simp add: fortune_def toss_def)+

lemma fortune_toss_sum: "fortune n s = (∑i ∈ {..n}. toss i s)"
  by (induction n arbitrary: s) (simp add: fortune_def toss_def, simp add: fortune_Suc)

lemma fortune_bound: "norm (fortune n s) ≤ Suc n" by (induction n) (force simp add: fortune_toss_sum toss_def)+

text ‹Our definition of term‹bernoulli_stream› constitutes a probability space.›

interpretation prob_space "bernoulli_stream p" unfolding bernoulli_stream_def by (simp add: measure_pmf.prob_space_axioms prob_space.prob_space_stream_space)

abbreviation "toss_filtration p ≡ nat_natural_filtration (bernoulli_stream p) toss"

text ‹The stochastic process term‹toss› is adapted to the filtration it generates.› 

interpretation toss: adapted_process "bernoulli_stream p" "toss_filtration p" 0 toss 
  by (intro adapted_process.intro stochastic_process.adapted_process_natural_filtration)
     (unfold_locales, auto simp add: toss_def bernoulli_stream_def)

interpretation bernoulli_stream_natural_filtration: nat_finite_filtered_measure "bernoulli_stream p" "toss_filtration p"
  by (simp add: nat_finite_filtered_measure_def toss.finite_filtered_measure_natural_filtration)

text ‹Similarly, the stochastic process term‹fortune› is adapted to the filtration generated by the tosses.›

interpretation fortune: adapted_process "bernoulli_stream p" "toss_filtration p" 0 fortune 
proof -
  show "adapted_process (bernoulli_stream p) (toss_filtration p) 0 fortune"
  unfolding fortune_toss_sum   
  by (intro toss.partial_sum_adapted[folded atMost_atLeast0]) intro_locales
qed

lemma integrable_toss: "integrable (bernoulli_stream p) (toss n)" 
  using toss.random_variable
  by (intro Bochner_Integration.integrable_bound[OF integrable_const[of _ "1 :: real"]]) (auto simp add: toss_def)

lemma integrable_fortune: "integrable (bernoulli_stream p) (fortune n)" using fortune_bound 
  by (intro Bochner_Integration.integrable_bound[OF integrable_const[of _ "Suc n"] fortune.random_variable]) auto

text ‹We provide the following lemma to explicitly calculate the probability of events in this probability space.›

lemma measure_bernoulli_stream_snth_pred:
  assumes "0 ≤ p" and "p ≤ 1" and "finite J" 
  shows "prob p {w ∈ space (bernoulli_stream p). ∀j∈J. P j = w !! j} = p ^ card (J ∩ Collect P) * (1 - p) ^ (card (J - Collect P))"
proof -
  let ?PiE = "(ΠE i∈J. if P i then {True} else {False})"
  have "product_prob_space (λ_. measure_pmf (bernoulli_pmf p))" by unfold_locales

  hence *: "to_stream -` {s. ∀i∈J. P i = s !! i} = {s. ∀i∈J. P i = s i}" using assms by (simp add: to_stream_def)
  also have "... = prod_emb UNIV (λ_. measure_pmf (bernoulli_pmf p)) J ?PiE"
  proof -
    {
      fix s assume "(∀i∈J. P i = s i)"
      hence "(∀i∈J. P i = s i) = (s ∈ prod_emb UNIV (λ_. measure_pmf (bernoulli_pmf p)) J ?PiE)" 
        by (subst prod_emb_iff[of s]) (smt (verit, best) not_def assms(3) id_def PiE_eq_singleton UNIV_I extensional_UNIV insert_iff singletonD space_measure_pmf)
    }
    moreover
    {
      fix s assume "¬(∀i∈J. P i = s i)"
      then obtain i where "i ∈ J" "P i ≠ s i" by blast
      hence "(∀i∈J. P i = s i) = (s ∈ prod_emb UNIV (λ_. measure_pmf (bernoulli_pmf p)) J ?PiE)"
        by (simp add: restrict_def prod_emb_iff[of s]) (smt (verit, ccfv_SIG) PiE_mem assms(3) id_def insert_iff singleton_iff)
    }
    ultimately show ?thesis by auto
  qed
  finally have inteq: "(to_stream -` {s. ∀i∈J. P i = s !! i}) = prod_emb UNIV (λ_. measure_pmf (bernoulli_pmf p)) J ?PiE" .
  let ?M = "(PiM UNIV (λ_. measure_pmf (bernoulli_pmf p)))"
  have "emeasure (bernoulli_stream p) {s ∈ space (bernoulli_stream p). ∀i∈J. P i = s !! i} = emeasure ?M (to_stream -` {s. ∀i∈J. P i  = s !! i})"
    using assms emeasure_distr[of "to_stream" ?M "(vimage_algebra (streams (space (measure_pmf (bernoulli_pmf p)))) (!!) ?M)" "{s. ∀i∈J. P i = s !! i}", symmetric] measurable_to_stream[of "(measure_pmf (bernoulli_pmf p))"]
    by (simp only: bernoulli_stream_def stream_space_def *, simp add: space_PiM ) (smt (verit, best) emeasure_notin_sets in_vimage_algebra inf_top.right_neutral sets_distr vimage_Collect)
  also have "... = emeasure ?M (prod_emb UNIV (λ_. measure_pmf (bernoulli_pmf p)) J ?PiE)" using inteq by (simp add: space_PiM)
  also have "... = (∏i∈J. emeasure (measure_pmf (bernoulli_pmf p)) (if P i then {True} else {False}))" 
    by (subst emeasure_PiM_emb) (auto simp add: prob_space_measure_pmf assms(3))
  also have "... = (∏i∈J ∩ Collect P. ennreal p) * (∏i∈J - Collect P. ennreal (1 - p))"
    unfolding emeasure_pmf_single[of "bernoulli_pmf p" True, unfolded pmf_bernoulli_True[OF assms(1,2)], symmetric]
              emeasure_pmf_single[of "bernoulli_pmf p" False, unfolded pmf_bernoulli_False[OF assms(1,2)], symmetric]
    by (simp add: prod.Int_Diff[OF assms(3), of _ "Collect P"])
  also have "... = p ^ card (J ∩ Collect P) * (1 - p) ^ card (J - Collect P)" using assms by (simp add: prod_ennreal ennreal_mult' ennreal_power)
  finally show ?thesis using assms by (intro measure_eq_emeasure_eq_ennreal) auto
qed

lemma 
  assumes "0 ≤ p" and "p ≤ 1"
  shows measure_bernoulli_stream_snth: "prob p {w ∈ space (bernoulli_stream p). w !! i} = p"
    and measure_bernoulli_stream_neg_snth: "prob p {w ∈ space (bernoulli_stream p). ¬w !! i} = 1 - p"
  using measure_bernoulli_stream_snth_pred[OF assms, of "{i}" "λx. True"]
        measure_bernoulli_stream_snth_pred[OF assms, of "{i}" "λx. False"] by auto

text ‹Now we can express the expected value of a single coin toss.›

lemma integral_toss:
  assumes "0 ≤ p" "p ≤ 1"
  shows "expectation p (toss n) = 2 * p - 1"
proof -
  have [simp]:"{s. s !! n} ∈ events p" using measurable_snth[THEN measurable_sets, of "{True}" "measure_pmf (bernoulli_pmf p)" n, folded bernoulli_stream_def]
    by (simp add: vimage_def)
  have "expectation p (toss n) = Bochner_Integration.simple_bochner_integral (bernoulli_stream p) (toss n)"
    using toss.random_variable[of n, THEN measurable_sets]
    by (intro simple_bochner_integrable_eq_integral[symmetric] simple_bochner_integrable.intros) (auto simp add: toss_def simple_function_def image_def)
  also have "... = p - prob p {s. ¬ s !! n}" unfolding simple_bochner_integral_def using measure_bernoulli_stream_snth[OF assms]
    by (simp add: range_toss, simp add: toss_def)
  also have "... = p - (1 - prob p {s. s !! n})" by (subst prob_compl[symmetric], auto simp add: Collect_neg_eq Compl_eq_Diff_UNIV)
  finally show ?thesis using measure_bernoulli_stream_snth[OF assms] by simp
qed

text ‹Now, we show that the tosses are independent from one another.›

lemma indep_vars_toss:
  assumes "0 ≤ p" "p ≤ 1"
  shows "indep_vars p (λ_. borel) toss {0..}"
proof (subst indep_vars_def, intro conjI indep_sets_sigma)
  {
    fix A J assume asm: "J ≠ {}" "finite J" "∀j∈J. A j ∈ {toss j -` A ∩ space (bernoulli_stream p) |A. A ∈ borel}"
    hence "∀j∈J. ∃B ∈ borel. A j = toss j -` B ∩ space (bernoulli_stream p)" by auto
    then obtain B where B_is: "A j = toss j -` B j ∩ space (bernoulli_stream p)" "B j ∈ borel" if "j ∈ J" for j by metis

    have "prob p (⋂ (A ` J)) = (∏j∈J. prob p (A j))"
    proof cases
      text ‹We consider the case where there is a zero probability event.›
      assume "∃j ∈ J. 1 ∉ B j ∧ -1 ∉ B j"
      then obtain j where j_is: "j ∈ J" "1 ∉ B j" "-1 ∉ B j" by blast
      hence A_j_empty: "A j = {}" using B_is by (force simp add: toss_def vimage_def)
      hence "⋂ (A ` J) = {}" using j_is by blast
      moreover have "prob p (A j) = 0" using A_j_empty by simp
      ultimately show ?thesis using j_is asm(2) by auto
    next
      text ‹We now assume all events have positive probability.›
      assume "¬(∃j ∈ J. 1 ∉ B j ∧ -1 ∉ B j)"
      hence *: "1 ∈ B j ∨ -1 ∈ B j" if "j ∈ J" for j using that by blast


      define J' where [simp]: "J' = {j ∈ J. (1 ∈ B j) ⟷ (-1 ∉ B j)}"
      hence "toss j w ∈ B j ⟷ (1 ∈ B j) = w !! j" if "j ∈ J'" for w j using that unfolding toss_def by simp
      hence "(⋂ (A ` J')) = {w ∈ space (bernoulli_stream p). ∀j∈J'. (1 ∈ B j) = w !! j}" using B_is by force
      hence prob_J': "prob p (⋂ (A ` J')) = p ^ card (J' ∩ {j. 1 ∈ B j}) * (1 - p) ^ card (J' - {j. 1 ∈ B j})" 
        using measure_bernoulli_stream_snth_pred[OF assms finite_subset[OF _ asm(2)], of J' "λj. 1 ∈ B j"] by auto
      
      text ‹The index set term‹J'› consists of the indices of all non-trivial events.›
      
      have A_j_True: "A j = {w ∈ space (bernoulli_stream p). w !! j}" if "j ∈ J' ∩ {j. 1 ∈ B j}" for j
        using that by (auto simp add: toss_def B_is(1) split: if_splits) 

      have A_j_False: "A j = {w ∈ space (bernoulli_stream p). ¬w !! j}" if "j ∈ J' - {j. 1 ∈ B j}" for j 
        using that B_is by (auto simp add: toss_def) 
      
      have A_j_top: "A j = space (bernoulli_stream p)" if "j ∈ J - J'" for j using that * by (auto simp add: B_is toss_def)
      hence "⋂ (A ` J) = ⋂ (A ` J')" by auto
      hence "prob p (⋂ (A ` J)) = prob p (⋂ (A ` J'))" by presburger
      also have "... = (∏j∈J' ∩ {j. 1 ∈ B j}. prob p (A j)) * (∏j∈J' - {j. 1 ∈ B j}. prob p (A j))" 
        by (simp only: prob_J' A_j_True A_j_False measure_bernoulli_stream_snth[OF assms] measure_bernoulli_stream_neg_snth[OF assms] cong: prod.cong) simp
      also have "... = (∏j∈J'. prob p (A j))" using asm(2) by (intro prod.Int_Diff[symmetric]) auto
      also have "... = (∏j∈J'. prob p (A j)) * (∏j∈J - J'. prob p (A j))" using A_j_top prob_space by simp
      also have "... = (∏j∈J. prob p (A j))" using asm(2) by (metis (no_types, lifting) J'_def mem_Collect_eq mult.commute prod.subset_diff subsetI)
      finally show ?thesis .
    qed
  }
  thus "indep_sets p (λi. {toss i -` A ∩ space (bernoulli_stream p) |A. A ∈ sets borel}) {0..}" using measurable_sets[OF toss.random_variable]
  by (intro indep_setsI subsetI) fastforce
qed (simp, intro Int_stableI, simp, metis sets.Int vimage_Int)

text ‹The fortune of a player is a martingale (resp. sub- or supermartingale) with respect to the filtration generated by the coin tosses.›

theorem fortune_martingale:
  assumes "p = 1/2"
  shows "martingale (bernoulli_stream p) (toss_filtration p) 0 fortune"
  using cond_exp_indep[OF bernoulli_stream_natural_filtration.subalg indep_set_natural_filtration integrable_toss, OF zero_order(1) lessI indep_vars_toss, of p] 
        integral_toss assms
    by (intro bernoulli_stream_natural_filtration.martingale_of_cond_exp_diff_Suc_eq_zero integrable_fortune fortune.adapted_process_axioms) (force simp add: fortune_toss_sum)

theorem fortune_submartingale:
  assumes "1/2 ≤ p" "p ≤ 1"
  shows "submartingale (bernoulli_stream p) (toss_filtration p) 0 fortune"
proof (intro bernoulli_stream_natural_filtration.submartingale_of_cond_exp_diff_Suc_nonneg integrable_fortune fortune.adapted_process_axioms)
  fix n
  show "AE ξ in bernoulli_stream p. 0 ≤ cond_exp (bernoulli_stream p) (toss_filtration p n) (λξ. fortune (Suc n) ξ - fortune n ξ) ξ"
    using cond_exp_indep[OF bernoulli_stream_natural_filtration.subalg indep_set_natural_filtration integrable_toss, OF zero_order(1) lessI indep_vars_toss, of p n] 
          integral_toss[of p "Suc n"] assms
    by (force simp add: fortune_toss_sum)
qed

theorem fortune_supermartingale:
  assumes "0 ≤ p" "p ≤ 1/2" 
  shows "supermartingale (bernoulli_stream p) (toss_filtration p) 0 fortune"
proof (intro bernoulli_stream_natural_filtration.supermartingale_of_cond_exp_diff_Suc_le_zero integrable_fortune fortune.adapted_process_axioms)
  fix n
  show "AE ξ in bernoulli_stream p. 0 ≥ cond_exp (bernoulli_stream p) (toss_filtration p n) (λξ. fortune (Suc n) ξ - fortune n ξ) ξ"
    using cond_exp_indep[OF bernoulli_stream_natural_filtration.subalg indep_set_natural_filtration integrable_toss, OF zero_order(1) lessI indep_vars_toss, of p n] 
          integral_toss[of p "Suc n"] assms
    by (force simp add: fortune_toss_sum)
qed

end