Theory Discrete_UCB_Step1

theory Discrete_UCB_Step1
  imports "MSc_Project_Discrete_Prop15_1"

begin

locale bandit_policy = bandit_problem +  prob_space  +
  fixes Ω :: "'b set"
    and ℱ :: "'b set set"
    and ω :: 'b
    and π :: "nat ⇒ 'b ⇒ 'a"
    and N_n :: "nat ⇒ 'a ⇒ 'b ⇒ nat"  
  assumes  measurable_policy: "∀t. π t ∈ measurable M (count_space A)"
    and N_n_def: "∀n a ω. N_n n a ω = card {t ∈ {0..<n}. π (t+1) ω = a}"
    and count_assm_pointwise: "∀n ω. (∑a ∈ A. real (N_n n a ω)) = real n" 
begin

lemma union_eq:
  fixes a :: 'a and n k :: nat 
  assumes "k ≤ n"
  shows "{t. t < n ∧ π (t+1) ω = a} = {t. t < k ∧ π (t+1) ω = a} ∪ {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
proof
  show "{t. t < n ∧ π (t+1) ω = a} ⊆ {t. t < k ∧ π (t+1) ω = a} ∪ {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
  proof
    fix x assume "x ∈ {t. t < n ∧ π (t+1) ω = a}"
    then have "x < n" and "π (x+1) ω = a" by auto
    then have "x < k ∨ k ≤ x" by auto
    thus "x ∈ {t. t < k ∧ π (t+1) ω = a} ∪ {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
      using ‹x < n› ‹π (x+1) ω = a› by auto
  qed
next
  show "{t. t < k ∧ π (t+1) ω = a} ∪ {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a} ⊆ {t. t < n ∧ π (t+1) ω = a}"
  proof
    fix x assume "x ∈ {t. t < k ∧ π (t+1) ω = a} ∪ {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
    then have "x < k ∧ π (x+1) ω = a ∨ (k ≤ x ∧ x < n ∧ π (x+1) ω = a)" by auto
    hence "x < n ∧ π (x+1) ω = a" using assms by auto
    thus "x ∈ {t. t < n ∧ π (t+1) ω = a}" by auto
  qed
qed

lemma cardinality_indic_eq:
  fixes I :: "nat ⇒ bool"
  assumes "finite {t. k ≤ t ∧ t < n}"
  shows "card {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ I t} = (∑ t = k..<n. if π (t+1) ω = a ∧ I t then 1 else 0)"
proof -
  have fin: "finite {t. k ≤ t ∧ t < n}" using assms by simp
  have sum_eq:
    "sum (indicator {t. π (t+1) ω = a ∧ I t}) {t. k ≤ t ∧ t < n} = card ({t. k ≤ t ∧ t < n} ∩ {t. π (t+1) ω = a ∧ I t})"
    by (rule sum_indicator_eq_card[OF fin])
  have sets_eq:
    "{t. k ≤ t ∧ t < n} ∩ {t. π (t+1) ω = a ∧ I t} = {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ I t}"
    by auto
  hence card_eq:
    "card ({t. k ≤ t ∧ t < n} ∩ {t. π (t+1) ω = a ∧ I t}) = card {t. k ≤ t ∧ t < n ∧ π(t+1) ω = a ∧ I t}"
    by simp
  have card_sum_eq:
    "sum (indicator {t. π (t+1) ω = a ∧ I t}) {t. k ≤ t ∧ t < n} = card {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ I t}"
    using sum_eq sets_eq by simp
  have ind_eq:
    "sum (indicator {t. π (t+1) ω = a ∧ I t}) {t. k ≤ t ∧ t < n} = sum (λt. of_bool (π (t+1) ω = a ∧ I t)) {t. k ≤ t ∧ t < n}"
    by (simp add: indicator_def)
  have bool_if_eq:
    "sum (λt. of_bool (π (t+1) ω = a ∧ I t)) {t. k ≤ t ∧ t < n} = sum (λt. if π (t+1) ω = a ∧ I t then 1 else 0) {t. k ≤ t ∧ t < n}"
    by (simp add: of_bool_def)
  have set_eq: "{t. k ≤ t ∧ t < n} = {k..} ∩ {..<n}" by auto
  have sum_set_eq:
    "sum (λt. if π (t+1) ω = a ∧ I t then 1 else 0) {t. k ≤ t ∧ t < n} = sum (λt. if π (t+1) ω = a ∧ I t then 1 else 0) ({k..} ∩ {..<n})"
    by (simp add: set_eq)
  have atLeastLessThan_eq:
    "sum (λt. if π (t+1) ω = a ∧ I t then 1 else 0) ({k..} ∩ {..<n}) = sum (λt. if π (t+1) ω = a ∧ I t then 1 else 0) (atLeastLessThan k n)"
    by (simp add: atLeastLessThan_def)
  have final_sum_eq:
    "sum (λt. if π (t+1) ω = a ∧ I t then 1 else 0) (atLeastLessThan k n) = (∑ t = k..<n. if π (t+1) ω = a ∧ I t then 1 else 0)"
    by simp
  show ?thesis
    apply (subst card_sum_eq[symmetric])
    apply (subst ind_eq)
    apply (subst bool_if_eq)
    apply (subst sum_set_eq)
    apply (subst atLeastLessThan_eq)
    apply (simp add: final_sum_eq)
    done
qed

lemma ge_rewrite: "(x::real) ≥ y ⟹ y ≤ x" by simp

lemma Nn_expression:
  fixes a :: 'a and s :: "nat ⇒ real"
    and k :: nat and n :: nat
  assumes "a ∈ A"
    and "k ≤ n"
    and "0 < n"
    and "∀ t ∈ {0..n}. 0 < s t"
    and "∀t < n - 1.  s t ≤ s (t + 1)"  (* s non-decreasing *)
    and init_play_once: "∀ω. a ∈ A ⟶ N_n k a ω = 1"
    and finite_played_sets:
    "finite {t. t < n ∧ π (t+1) ω = a}"
    "finite {t. t < k ∧ π (t+1) ω = a}"
    "finite {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
  shows
    "(N_n n a ω) = 1 + (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) +
                      (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t then 1 else 0)"
proof -
  have Nn_def: "(N_n n a ω) = card {t. t < n ∧ π (t+1) ω = a}"
    by (simp add: N_n_def)

  have init_count: "1 ≤ card {t. t < k ∧ π (t+1) ω = a}"
  proof -
    have eq_card: "N_n k a ω = card {t. t < k ∧ π (t+1) ω = a}"
      by (simp add: N_n_def)
    moreover from init_play_once and ‹a ∈ A› have "1 ≤ N_n k a ω"
      by simp
    ultimately show ?thesis by simp
  qed

  have disj: "{t. t < k ∧ π (t+1) ω = a} ∩ {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a} = {}"
    by auto

  have union_eq_set:
    "{t. t < n ∧ π (t+1) ω = a} = {t. t < k ∧ π (t+1) ω = a} ∪ {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
    using union_eq assms by blast

  have finite1: "finite {t. t < k ∧ π (t+1) ω = a}" and finite2: "finite {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
    using finite_played_sets by auto

  have card_eq:
    "card {t. t < n ∧ π (t+1) ω = a} = card {t. t < k ∧ π (t+1) ω = a} + card {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
    using card_Un_disjoint[OF finite1 finite2 disj] union_eq_set by simp

  have eq_card_k: "card {t. t < k ∧ π (t+1) ω = a} = N_n k a ω"
    by (simp add: N_n_def)

  have card_k_eq_1: "card {t. t < k ∧ π (t+1) ω = a}  = 1"
    using init_play_once assms eq_card_k by simp

  have card_eq_1:
    "card {t. t < n ∧ π (t+1) ω = a} = 1 + card {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
    using card_eq eq_card_k card_k_eq_1 by simp

  have finite_lt: "finite {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ real (N_n t a ω) < s t}"
    using finite2 finite_subset by simp

  have finite_ge: "finite {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t}"
    using finite2 finite_subset by simp

  have card_eq_partition:
    "card {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a} =
     card {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ real (N_n t a ω) < s t} +
     card {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t}"
  proof -
    have union_eq_partition:
      "{t. k ≤ t ∧ t < n ∧ π (t+1) ω = a} =
       {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ real (N_n t a ω) < s t} ∪
       {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t}" by auto

    have disj_partition:
      "{t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ real (N_n t a ω) < s t} ∩
       {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t} = {}"
      by auto

    show ?thesis
      using card_Un_disjoint[OF finite_lt finite_ge disj_partition] union_eq_partition by simp
  qed

  have card_eq_sum_lt:
    "card {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ real (N_n t a ω) < s t} =
     (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0)"
    using cardinality_indic_eq by simp

  have card_eq_sum_ge:
    "card {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t} =
     (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t then 1 else 0)"
    using cardinality_indic_eq by simp

  have "(N_n n a ω) = card {t. t < n ∧ π (t+1) ω = a}"
    using N_n_def by simp

  also have "... = 1 +
    (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) +
    (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t then 1 else 0)"
    using card_eq_partition card_eq_1 card_eq_sum_lt card_eq_sum_ge by simp

  also have "... = 1 +
    (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) +
    (∑ t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)"
    using ge_rewrite by simp

  have rewrite_eq:" (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t then 1 else 0) =
       (∑ t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)"
    using sum.cong by simp

  ultimately have final_eq: "(N_n n a ω) = 1 + (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) +
                      (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t then 1 else 0) "
    by simp

  show "(N_n n a ω) = 1 + (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) +
                      (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) ≥ s t then 1 else 0)"
    apply (subst rewrite_eq)
    apply (subst final_eq)
    apply simp
    done

qed

lemma upper_bound_expression_contradiction:
  fixes a :: 'a and s :: "nat ⇒ real"
    and k :: nat and n :: nat
    and s_n_nat :: nat
  assumes "a ∈ A"
    and "k ≤ n"
    and "0 < n"
    and non_neg_s: "∀ t ∈ {0..n}. 0 < s t"
    and base_le: "s 0 ≤ s 1" 
    and non_dec: "∀t < n - 1. s t ≤ s (t + 1)"  (* s is non-decreasing *)
    and s_mono: "⋀t. k ≤ t ∧ t ≤ n ⟹ s t ≤ s n"
    and init_play_once: "∀ω. a ∈ A ⟶ N_n k a ω = 1"
    and finite_played_sets:
    "finite {t. t < n ∧ π (t+1) ω = a}"
    "finite {t. t < k ∧ π (t+1) ω = a}"
    "finite {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
    and xs_sorted_def: "xs = sorted_list_of_set {t ∈ {k..<n}. π (t+1) ω = a ∧ real (N_n t a ω) < s t}"
    and s_nat_def: "s_n_nat = nat (⌊s n⌋)"
    and len_bound_def: "s_n_nat < length xs" (* s_n_nat is an existing element *)
    and distinct_xs: "distinct xs"
    and gt_ineq: "length xs + 1 > ⌊s n⌋"
    and  N_n_increasing_with_plays:
    "∀ t t'. k ≤ t ∧ t < t' ∧ π (t+1) ω = a ∧ π (t'+1) ω = a ⟶ N_n t' a ω ≥ N_n t a ω + 1"
    and neg: "1 + real (∑ t=k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) > s n"
    and "t_hat ∈ set xs" 
    and " t_hat = xs ! s_n_nat"
    and " real (N_n t_hat a ω) ≥ real s_n_nat + 1"
    (* By construction of xs, and since t_hat is the s_n_nat-th element in xs,
     the count N_n t_hat a ω is at least s_n_nat + 1 *)
    (* The argument depends on repeated increments due to monotonicity *)

shows "(real (N_n t_hat a ω) ≥ ⌊s n⌋ + 1) ∧ (π (t_hat+1) ω = a ∧ (real (N_n t_hat a ω) < s t_hat))"

proof -
  have sn_nat_def:"s_n_nat = nat (⌊s n⌋)" by fact

  let ?I = "{t ∈ {k..<n}. π (t+1) ω = a ∧ real (N_n t a ω) < s t}"
  have sum_eq_card: "real (∑ t=k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) = real (card ?I)"
    using cardinality_indic_eq by simp

  have finI: "finite {t ∈ {k..<n}. π (t+1) ω = a ∧ real (N_n t a ω) < s t}"
  proof -
    have subset: "{t ∈ {k..<n}. π (t+1) ω = a ∧ real (N_n t a ω) < s t} ⊆ {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
      by auto
    moreover have "finite {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
      using finite_played_sets(3) .
    ultimately show ?thesis
      using finite_subset by blast
  qed


  have xs_props: "sorted xs" "distinct xs" "set xs = {t ∈ {k..<n}. π (t+1) ω = a ∧ real (N_n t a ω) < s t}"
    using List.linorder_class.set_sorted_list_of_set
    using finite_played_sets
    unfolding xs_sorted_def
    by auto


  have sum_eq_length:
    "(∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) = length xs"
  proof -
    let ?P = "λt. π (t+1) ω = a ∧ real (N_n t a ω) < s t"
    let ?I = "{t ∈ {k..<n}. ?P t}"

    have sum_card: "(∑ t = k..<n. if ?P t then 1 else 0) = card ?I"
      using cardinality_indic_eq by simp

    also have "... = card (set xs)"
      using xs_props(3) by simp

    also have "... = length xs"
      using xs_props(2) distinct_card by auto 

    finally show ?thesis .
  qed  

  have gt_ineq: "1 + real(length xs) > s n"
  proof -
    (* First show sum over indicator = length xs *)

    have eq1:"1 + (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) = 1 + length xs"
      using sum_eq_length by simp

    then have eq2: "real (1 + (∑ t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0)) = 1 + real ( length xs)"  
      by simp
        (* Use assumption neg to get strict inequality *)
    from neg have "¬ (1 + real (∑t=k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) ≤ s n)"
      by simp

    hence gt: "1 + real (∑ t=k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) > s n"
      by simp

(* Coerce nat to real for final goal *)
    then show ?thesis
      using eq1 eq2 neg gt by simp
  qed

  then have len_bound_assm: "s_n_nat < length xs"
    using len_bound_def assms
    by auto

  then have  distinct_xs: "distinct xs" (* distinct assumption already assumed in the global  scope*)
    using assms by simp

  then have  gt_ineq: "length xs + 1 > ⌊s n⌋"  (* ineq already assumed *)
    using assms by simp

  have part_1_glob: "π (t_hat +1 ) ω = a ∧ real (N_n t_hat a ω)  <  s t_hat"
  proof -
    have floor_le_sn: "⌊s n⌋ ≤ s n"
      using Archimedean_Field.of_int_floor_le by simp

    from gt_ineq have len_bound: "length xs + 1 > ⌊s n⌋"
      using len_bound_assm by simp

    have nat_expression_sn: "length xs ≥ nat (⌊s n⌋)"
    proof -
      from len_bound have "length xs ≥ nat (⌊s n⌋)"
        by (simp add: nat_less_iff)
      then show ?thesis .
    qed


    have sn_lt_len_plus_1: "⌊s n⌋ <  1 + real (length xs)"
      using gt_ineq by simp


    then have final_eq_glob:"π (t_hat+1) ω = a ∧ real (N_n t_hat a ω)  <  s t_hat"
    proof - 

      have π_eq: "π (t_hat+1) ω = a" 
        using assms xs_sorted_def by simp

      then have "π (t_hat +1) ω = a" using π_eq by simp

      then have intermid_eq: "k ≤ t_hat ∧ t_hat < n ∧ π (t_hat +1) ω = a ∧ real (N_n t_hat a ω) < s t_hat"
        using xs_sorted_def `t_hat ∈ set xs` by auto

      have fin_eq:"π (t_hat + 1) ω = a ∧ real (N_n t_hat a ω) < s t_hat"
        using intermid_eq
        by simp
      then show ?thesis by simp
    qed

    show ?thesis using  final_eq_glob by simp
  qed

(*this should hold as we now have verified 
but is in fact impossible as arm a must have played at least 1 +⌊s n⌋ times, let's continue exploring
*)


  have floor_le_sn: "⌊s n⌋ ≤ s n"
    using Archimedean_Field.of_int_floor_le by simp

  have one_plus_length_gt_floor: "1 + real (length xs) > s n"
    using `1 + real (length xs) > s n` .

  have floor_less_length_plus_one: "real (nat (⌊s n⌋)) < 1 + real (length xs)"
    using one_plus_length_gt_floor floor_le_sn
    by linarith

  from gt_ineq have len_result: "length xs  > ⌊s n⌋ - 1" by simp
  then have "length xs ≥ nat (⌊s n⌋)" by (simp add: nat_less_iff)
  hence t_hat_in_set:"t_hat ∈ set xs"
    using assms distinct_xs len_bound_assm by auto

(* Since t_hat ∈ xs and xs ⊆ {k..<n}, we have k ≤ t_hat < n, so t_hat ≤ n *)
  have t_hat_le_n: "t_hat + 1 ≤ n"
    using xs_sorted_def t_hat_in_set by auto

(* Then by monotonicity: *)
  have k_le_t_hat: "k ≤ t_hat"
    using xs_sorted_def t_hat_in_set by auto

  have s_t_hat_le_s_n: "s t_hat ≤ s n"
    using s_mono[of t_hat] 
    using xs_sorted_def t_hat_in_set by auto


  have "real (N_n t_hat a ω) ≥ real s_n_nat + 1"
    using assms by simp

  have final_result: "real (N_n t_hat a ω) ≥ ⌊s n⌋ + 1"
    using ‹real (N_n t_hat a ω) ≥ real (s_n_nat) + 1›
    by (simp add: sn_nat_def )


  show ?thesis using final_result and part_1_glob by auto

qed


(* We have identified an element t_hat ∈ xs such that t_hat is the element at position s_n_nat
   in the sorted list xs. This corresponds to the floor index of s n in the sorted set of indices
   where arm a was played and the count N_n(t, a, ω) is less than s(t).

   In simpler terms:

   Since there are at least ⌊s n⌋ + 1 such times in xs,
  N_t_hat_a ≥ 1 +⌊s n⌋ . *)


lemma Nn_upper_bound:
  fixes a :: 'a and s :: "nat ⇒ real"
    and k :: nat and n :: nat
  assumes asm: "real(1 + (∑t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0)) ≤ s n"
    and a_in_A: "a ∈ A"
    and k_le_n: "k ≤ n"
    and n_pos: "0 < n"
    and s_pos: "∀ t ∈ {0..n}. 0 < s t"
    and s_nondec: "∀ t < n - 1. s t ≤ s (t + 1)"
    and init_play_once: "∀ω. a ∈ A ⟶ N_n k a ω = 1"
    and finite_played_sets_1: "finite {t. t < n ∧ π (t+1) ω = a}"
    and finite_played_sets_2: "finite {t. t < k ∧ π (t+1) ω = a}"
    and finite_played_sets_3: "finite {t. k ≤ t ∧ t < n ∧ π (t+1) ω = a}"
  shows "real(N_n n a ω) ≤ s n + real((∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0))"
proof -
  have expr_nat: "N_n n a ω =
    1 + (∑t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) +
        (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)"
    using Nn_expression[OF a_in_A k_le_n n_pos s_pos s_nondec init_play_once
        finite_played_sets_1 finite_played_sets_2 finite_played_sets_3]
    by simp

  from asm have bound:"real(1 + (∑t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0)) ≤ s n" by simp

  have "real (N_n n a ω) = real ( 1 + (∑t = k..<n. if π (t+1) ω = a ∧ real (N_n t a ω) < s t then 1 else 0) +
        (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0))"
    using expr_nat by simp

  also have "... ≤ s n + real ( (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0))"
    using assms
    by simp

  then show ?thesis
    using expr_nat asm
    by simp
qed


theorem ENn_upper_bound:
  assumes
    a_in_A: "a ∈ A"
    and k_le_n: "k ≤ n"
    and n_pos: "0 < n"
    and s_pos: "∀t ∈ {0..n}. 0 < s t"
    and s_nondec: "∀t < n. s t ≤ s (t + 1)"
    and init_play_once: "∀ω. a ∈ A ⟶ N_n k a ω = 1"
    and integrable_Nn: "integrable M (λω. real (N_n n a ω))"
    and integrable_rhs_sum: "integrable M (λω. s n + (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0))"
    and integrable_s: "integrable M (λω. s n)"
    and integrable_indicator_sum: "integrable M (λω. ∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)"
    and linearity: "integral⇧L M (λω. s n + (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)) = 
                 integral⇧L M (λω. s n) + integral⇧L M (λω. ∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)"
    and pointwise_bound: "real (N_n n a ω) ≤ s n + (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)"
    and mono_intgrl: " integral⇧L M (λω. real (N_n n a ω)) ≤ integral⇧L M (λω. s n + (∑t = k..<n. 
if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0))"
  shows
    "expectation (λω. real (N_n n a ω)) ≤ 
     s n + expectation (λω. (∑t = k..<n.  if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0))"
proof -
  let ?f = "λω. real (N_n n a ω)"
  let ?g = "λω. s n + (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)"
  let ?g1 = "λω. s n"
  let ?g2 = "λω. (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)"
  have pointwise_le: " ?f ω ≤ ?g ω"
    using pointwise_bound .

  have intg_f: "integrable M ?f" using integrable_Nn .
  have intg_g: "integrable M ?g" using integrable_rhs_sum .
  then have eq_f:"integral⇧L M ?f = expectation (?f)"
    using prob_space by simp
  then have eq_g: "integral⇧L M ?g = expectation (?g)"
    by simp

  then have sub_eqg1:"integral⇧L M ?g1 = expectation (λω. s n)"
    by simp
  then have sub_eqg2:"integral⇧L M ?g2 = expectation(λω. (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0))"
    by simp


  have "real (N_n n a ω) ≤ s n + (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)"
    using assms by simp 

  have const_measure: "Sigma_Algebra.measure M (space M) = 1"
    using prob_space Probability_Measure.prob_space.prob_space by blast

  have exp_sn: "expectation (λω. s n) = s n"
  proof -
    have "expectation (λω. s n) = integral⇧L M (λω. s n)"
      by simp
    also have "... = s n"
      using prob_space by (simp add: prob_space.prob_space)
    then show ?thesis .
  qed

  have rhs_expr:
    "integral⇧L M ?g =  integral⇧L M (λω. s n) + integral⇧L M (λω. ∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0)"
    using linearity by auto

  then have rhs_expr: 
    "expectation (?g) = expectation (λω. s n) + expectation (λω. (∑t = k..<n. if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0))"
    by simp

  also have final_eq: "expectation (?g) = s n + expectation (λω. (∑t = k..<n.  if π (t+1) ω = a ∧ s t ≤ real (N_n t a ω) then 1 else 0))"
    using rhs_expr exp_sn
    by simp

  have glob_final_eq:"expectation (?f) ≤ expectation (?g)"
    using assms intg_f intg_g pointwise_le mono_intgrl
    by auto


  thus ?thesis
    using glob_final_eq final_eq by simp
qed

end
end