proposition: Lemma walk_to_corner_decomp m a b (A B : seq nat) : (size (hook_box_indices (a, b)) != 0)%N -> is_trace (a::A) (b::B) -> mu (walk_to_corner m.+1 (a, b)) (charfun (a :: A) (b :: B)) = ( mu (walk_to_corner m (a, head O B)) (charfun (a :: A) B) + mu (walk_to_corner m (head O A, b)) (charfun A (b :: B)) ) / (size (hook_box_indices (a, b)))%:Q.
proof: Proof. Proof using. move => Hs Ht. rewrite (walk_to_corner_simpl _ Hs) Mlet_simpl. rewrite mu_uniform_sum /=. congr (_ / _). rewrite /hook_box_indices big_cat /= !big_map /= addrC. congr (_ + _). - case (boolP (size B == 0%N)) => HB. + rewrite big1. * apply esym. apply: (mu_bool_negb0 _ (walk_to_corner_inv m a (head O B))) => [] [X Y] /=. apply/implyP => /and4P[_ SY _ _]. by move: SY; apply contra => /eqP[_ ->]. * move => i _; rewrite charfun_simplr. apply: (mu_bool_negb0 _ (walk_to_corner_inv m a i)) => [] [X Y] /=. apply/implyP => /and4P[_ SY _ _]. by move: SY; apply contra => /eqP[_ ->]. + rewrite (bigD1_seq (head O B) _ (iota_uniq _ _)) /=. * rewrite -{1}(@charfun_simplr b (a :: A) B) -[RHS]addr0. congr (_ + _). apply: big1 => i Hi. rewrite charfun_simplr. apply: (mu_bool_negb0 _ (walk_to_corner_inv m a i)) => [] [X Y] /=. apply/implyP => /and4P[_ _ _ SH]. move: Hi; apply contra => /eqP[_ <-]. by rewrite eq_sym. * have:= Ht => /and5P[_ _ _ HsortB _]. have Hb : (b < head 0 B)%N. by move: HsortB HB; case B => // b0 B' /= /andP[]. rewrite mem_iota (iota_hookE _ Hb) Hb /=. have Hh : (head O B \in b :: B). by move: HB; case B => // n l _; rewrite !inE eq_refl orbT. exact: (is_trace_in_in_shape Ht (mem_head _ _) Hh). - case (boolP (size A == O)) => HA. + rewrite big1. * apply esym. apply: (mu_bool_negb0 _ (walk_to_corner_inv m (head O A) b)) => [] [X Y] /=. apply /implyP => /andP[SX _]. by move: SX; apply contra => /eqP[-> _]. * move => i _; rewrite charfun_simpll. apply: (mu_bool_negb0 _ (walk_to_corner_inv m i b)) => [] [X Y] /=. apply /implyP => /andP[SX _]. by move: SX; apply contra => /eqP[-> _]. + rewrite (bigD1_seq (head O A) _ (iota_uniq _ _)) /=. * rewrite -{1}(@charfun_simpll a A (b :: B)) -[RHS]addr0. congr (_ + _). apply: big1 => i Hi. rewrite charfun_simpll. apply: (mu_bool_negb0 _ (walk_to_corner_inv m i b)) => [] [X Y] /=. apply /implyP => /and4P[_ _ HX _]. move: Hi; apply contra => /eqP[<- _]. by rewrite eq_sym. * have:= Ht => /and5P[_ _ HsortA _ _]. have Ha : (a < head 0 A)%N. by move: HsortA HA; case A => // a0 A' /= /andP[]. rewrite mem_iota (iota_hookE _ Ha) Ha /=. have Hh : (head O A \in a :: A). by move: HA; case A => // n l _; rewrite !inE eq_refl orbT. have:= is_trace_in_in_shape Ht Hh (mem_head _ _). case: p => /= part Hpart. by rewrite in_conj_part. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure