proposition: Lemma mu_walk_to_corner_is_trace rc m : in_shape p rc -> ((hook_length p rc) <= m.+1)%N -> mu (walk_to_corner m rc) (fun X => (is_trace X.1 X.2)%:Q) = 1.
proof: Proof. Proof using. elim: m rc => [| m IHm] [r c] Hrc /= Hal. have {}Hal : hook_length p (r, c) = 1%N. by move: Hal; rewrite /hook_length ltnS leqn0 => /eqP ->. by rewrite /is_trace hook_length1_corner. case H : (hook_length p (r, c)).-1 => [/= | n]. rewrite walk_to_corner_end_simpl // ?size_hook_box_indices //. rewrite Munit_simpl /= /is_trace /=. by rewrite hook_length1_corner // /hook_length H. have Hsz : size (hook_box_indices (r, c)) != 0%N. by rewrite size_hook_box_indices H. rewrite (walk_to_corner_simpl _ Hsz) Mlet_simpl mu_uniform_sum. have : upoints (unif_def (inl O) (hook_box_indices (r, c))) = (hook_box_indices (r, c)). rewrite /unif_def. move: H; rewrite -size_hook_box_indices. by case: (hook_box_indices (r, c)). rewrite -weight1_size /weight; rat_to_ring. rewrite [X in (_ / X)](eq_bigl predT) //=. set num := (X in (X / _)); set den := (X in (_ / X)). suff -> : num = den. rewrite divff // {num}/den. rewrite big_const_seq count_predT size_hook_box_indices H iter_addr addr0. by rewrite pnatr_eq0. rewrite {}/num {}/den. apply eq_big_seq => /= i. rewrite mem_cat => /orP[] /mapP[j]; rewrite mem_iota => /andP/=[H1 H2] ->{i}; move: H2; rewrite (iota_hookE _ H1) Mlet_simpl. - rewrite -/(in_shape _ (_, _)) -(in_conj_part (intpartP p)) => Hj. have Hlen : (hook_length p (j, c) <= m.+1)%N. rewrite -ltnS; apply: (leq_trans _ Hal). exact: hook_length_ltr. rewrite -[RHS](IHm _ Hj Hlen). rewrite (mu_pos_cond _ (walk_to_corner_inv m j c)); first last. by move=> [A B]; apply/andP; split; [exact: mu_bool_0le | exact: mu_bool_le1]. rewrite [RHS](mu_pos_cond _ (walk_to_corner_inv m j c)); first last. by move=> [A B]; case: (is_trace _ _). apply Mstable_eq => [] [A B] /=. do 2 (case: eqP => /=; first by rewrite !mul0r). do 2 (case: eqP => /=; last by rewrite !mul0r). rewrite !mul1r /is_trace /=. case: A B => [// | a0 A] [// | b0 B] /= _ -> _ _. by rewrite H1. - rewrite -/(in_shape _ (_, _)) => Hj. have Hlen : (hook_length p (r, j) <= m.+1)%N. rewrite -ltnS; apply: (leq_trans _ Hal). exact: hook_length_ltl. rewrite -[RHS](IHm _ Hj Hlen). rewrite (mu_pos_cond _ (walk_to_corner_inv m r j)); first last. by move=> [A B]; apply/andP; split; [exact: mu_bool_0le | exact: mu_bool_le1]. rewrite [RHS](mu_pos_cond _ (walk_to_corner_inv m r j)); first last. by move=> [A B]; case: (is_trace _ _). apply Mstable_eq => [] [A B]. do 2 (case: eqP => /=; first by rewrite !mul0r). do 2 (case: eqP => /=; last by rewrite !mul0r). rewrite !mul1r /is_trace /=. case: A B => [// | a0 A] [// | b0 B] /= -> _ _ _. by rewrite H1. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure