Library Combi.HookFormula.hook: A proof of the Hook-Lenght formula
A proof of the Hook-Lenght formula
- [FRT] -- J. S. Frame, G. de B. Robinson and R. M. Thrall,
The hook graphs of the symmetric group, Canad. J. Math. 6 (1954), 316-324.
- [GNW] -- Greene, C., Nijenhuis, A. and Wilf, H. S., A probabilistic proof of a formula for the number of Young tableaux of a given shape, Adv. in Math. 31 (1979), 104–109.
- corner_box sh (r, c) == (r, c) are the coordinate of a corner of sh
- arm_length sh (r, c) == the arm length of sh of the box (r, c)
- leg_length sh (r, c) == the leg length of sh of the box (r, c)
- hook_length sh (r, c) == the hook length of sh of the box (r, c)
- in_hook (r, c) (k, l) == the box (k, l) is in the hook of the box (r, c)
- hook_box_indices (r, c) == a sequence of indexes for boxes in the hook of (r, c): leg boxes are inl k, arm boxes are inr
- hook_box (r, c) n == the coordinate of the box of index n
- hook_boxes (r, c) == sequence of the boxes in the hool of (r, c)
- is_trace p A B == the trace of a trial path in the partition p, that is
the pair of the vertical and horizontal projection (see GNW).
Specifically A and B are two non-empty strictly increasing
sequences of naturals ending at a corner of p.
- trace_seq last == all stricly increasing sequences ending by last
- enum_trace Alpha Beta == all trace ending at (Alpha, Beta)
- walk_to_corner m (i, j) == the probabilistic distribution of traces of a hook path of length at most m starting at (i, j)
- choose_corner p == the probalistic distribution of a trace starting at
a uniformly chosen box
- starts_at (r, c) t == the trace t starts as (r, c)
- starts_at (r, c) t == the trace t ends as (r, c)
- RHSL3 p a b A B == the right hand side of Lemma 3 for a path starting at (a, b) with projections A and B
- RHSL3_trace p t == the right hand side of Lemma 3 for trace t in p
- hook_length_prod sh == the product of the hook length of sh
Theorem HookLengthFormula (p : intpart) :
#|{:stdtabsh p}| = (sumn p)`! %/ (hook_length_prod p).
Require Import Misc Ccpo.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssrint div rat ssralg ssrnum.
Require Import tools subseq partition Yamanouchi stdtab Qmeasure.
Set Implicit Arguments.
Import GRing.Theory.
Import Num.Theory.
#[local] Open Scope nat_scope.
Lemma card_yama_rec (p : intpart) :
p != empty_intpart ->
#|{:yameval p}| =
\sum_(i <- rem_corners p) #|{:yameval (decr_nth_intpart p i)}|.
Lemma card_yama0 : #|{:yameval empty_intpart}| = 1.
Lemma card_yam_stdtabE (p : intpart) :
#|{:yameval p}| = #|{:stdtabsh p}|.
#[local] Open Scope ring_scope.
Lemma card_stdtabsh_rat_rec (F : intpart -> rat) :
F empty_intpart = 1 ->
( forall p : intpart,
p != empty_intpart ->
F p = \sum_(i <- rem_corners p) F (decr_nth_intpart p i) ) ->
forall p : intpart, F p = #|{:stdtabsh p}|%:Q.
Close Scope ring_scope.
p != empty_intpart ->
#|{:yameval p}| =
\sum_(i <- rem_corners p) #|{:yameval (decr_nth_intpart p i)}|.
Lemma card_yama0 : #|{:yameval empty_intpart}| = 1.
Lemma card_yam_stdtabE (p : intpart) :
#|{:yameval p}| = #|{:stdtabsh p}|.
#[local] Open Scope ring_scope.
Lemma card_stdtabsh_rat_rec (F : intpart -> rat) :
F empty_intpart = 1 ->
( forall p : intpart,
p != empty_intpart ->
F p = \sum_(i <- rem_corners p) F (decr_nth_intpart p i) ) ->
forall p : intpart, F p = #|{:stdtabsh p}|%:Q.
Close Scope ring_scope.
Definition corner_box sh rc :=
is_rem_corner sh rc.1 && (rc.2 == (nth 0 sh rc.1).-1).
Lemma corner_box_in_part sh rc :
corner_box sh rc -> in_shape sh rc.
Lemma corner_box_conj_part sh u v :
is_part sh -> corner_box sh (u, v) -> corner_box (conj_part sh) (v, u).
Arm Leg and Hook lengths
Definition arm_length sh rc := ((nth 0 sh rc.1) - rc.2).-1.
Definition leg_length sh rc := (arm_length (conj_part sh) (rc.2, rc.1)).
Definition hook_length sh rc := (arm_length sh rc + leg_length sh rc).+1.
The hook length product
Definition hook_length_prod sh := (\prod_(b : box_in sh) hook_length sh b)%N.
#[local] Notation HLF sh := (((sumn sh)`!)%:Q / (hook_length_prod sh)%:Q)%R.
Lemma hook_length_geq1 sh rc : hook_length sh rc >= 1.
#[local] Hint Resolve hook_length_geq1 : core.
Lemma hook_length_conj_part sh r c :
is_part sh -> hook_length (conj_part sh) (r, c) = hook_length sh (c, r).
Lemma arm_length_ler sh r c j :
is_part sh -> r < j -> in_shape sh (j, c) ->
arm_length sh (j, c) <= arm_length sh (r, c).
Lemma arm_length_ltl sh r c j :
is_part sh -> c < j -> in_shape sh (r, j) ->
arm_length sh (r, j) < arm_length sh (r, c).
Lemma leg_length_ltr sh r c j :
is_part sh -> r < j -> in_shape sh (j, c) ->
leg_length sh (j, c) < leg_length sh (r, c).
Lemma leg_length_lel sh r c j :
is_part sh -> c < j -> in_shape sh (r, j) ->
leg_length sh (r, j) <= leg_length sh (r, c).
Lemma hook_length_ltl sh r c j :
is_part sh -> c < j -> in_shape sh (r, j) ->
hook_length sh (r, j) < hook_length sh (r, c).
Lemma hook_length_ltr sh r c j :
is_part sh -> r < j -> in_shape sh (j, c) ->
hook_length sh (j, c) < hook_length sh (r, c).
Lemma hook_length1_corner sh rc :
is_part sh -> in_shape sh rc ->
hook_length sh rc = 1 -> corner_box sh rc.
Lemma corner_arm_length0 sh rc :
is_part sh -> corner_box sh rc -> arm_length sh rc = 0.
Lemma corner_leg_length0 sh rc :
is_part sh -> corner_box sh rc -> leg_length sh rc = 0.
Lemma corner_hook_length1 sh rc :
is_part sh -> corner_box sh rc -> hook_length sh rc = 1.
Lemma arm_length_corner_box sh r c u v :
is_part sh ->
r <= u -> c <= v -> corner_box sh (u, v) ->
arm_length sh (r, c) = arm_length sh (u, c) + arm_length sh (r, v).
Lemma leg_length_corner_box sh r c u v :
is_part sh ->
r <= u -> c <= v -> corner_box sh (u, v) ->
leg_length sh (r, c) = leg_length sh (u, c) + leg_length sh (r, v).
Lemma hook_length_corner_box sh r c u v :
is_part sh -> r <= u -> c <= v -> corner_box sh (u, v) ->
hook_length sh (r, c) = hook_length sh (u, c) + hook_length sh (r, v) - 1.
Lemma arm_length_incr_nth_row sh r c :
in_shape sh (r, c) ->
arm_length (incr_nth sh r) (r, c) = (arm_length sh (r, c)).+1.
Lemma arm_length_incr_nth_nrow sh r c i :
i != r -> arm_length (incr_nth sh i) (r, c) = arm_length sh (r, c).
Lemma hook_length_incr_nth_row sh r c :
is_part sh -> is_add_corner sh r -> in_shape sh (r, c) ->
hook_length (incr_nth sh r) (r, c) = (hook_length sh (r, c)).+1.
Lemma hook_length_incr_nth_col sh r i :
is_part sh -> is_add_corner sh r ->
in_shape sh (i, (nth 0 sh r)) ->
hook_length (incr_nth sh r) (i, nth 0 sh r)
= (hook_length sh (i, nth 0 sh r)).+1.
Lemma hook_length_incr_nth sh i r c :
is_part sh -> is_add_corner sh i ->
in_shape sh (r, c) ->
i != r -> nth 0 sh i != c ->
hook_length (incr_nth sh i) (r, c) = hook_length sh (r, c).
Open Scope ring_scope.
Lemma hook_length_pred sh rc :
(hook_length sh rc)%:~R - 1 = ((hook_length sh rc).-1)%:~R :> rat.
Lemma prod_hook_length_quot_row p Alpha Beta :
is_part p -> corner_box p (Alpha, Beta) ->
\prod_(i <- enum_box_in (decr_nth p Alpha) | i.1 == Alpha)
( (hook_length p i)%:Q /
(hook_length (decr_nth p Alpha) i)%:Q ) =
\prod_(0 <= j < Beta) (1 + ((hook_length p (Alpha, j))%:Q - 1)^-1).
Close Scope ring_scope.
Section FindCorner.
Variable p : intpart.
Implicit Types (r c k l : nat) (rc kl : nat * nat).
#[local] Notation HLF sh := (((sumn sh)`!)%:Q / (hook_length_prod sh)%:Q)%R.
Lemma hook_length_geq1 sh rc : hook_length sh rc >= 1.
#[local] Hint Resolve hook_length_geq1 : core.
Lemma hook_length_conj_part sh r c :
is_part sh -> hook_length (conj_part sh) (r, c) = hook_length sh (c, r).
Lemma arm_length_ler sh r c j :
is_part sh -> r < j -> in_shape sh (j, c) ->
arm_length sh (j, c) <= arm_length sh (r, c).
Lemma arm_length_ltl sh r c j :
is_part sh -> c < j -> in_shape sh (r, j) ->
arm_length sh (r, j) < arm_length sh (r, c).
Lemma leg_length_ltr sh r c j :
is_part sh -> r < j -> in_shape sh (j, c) ->
leg_length sh (j, c) < leg_length sh (r, c).
Lemma leg_length_lel sh r c j :
is_part sh -> c < j -> in_shape sh (r, j) ->
leg_length sh (r, j) <= leg_length sh (r, c).
Lemma hook_length_ltl sh r c j :
is_part sh -> c < j -> in_shape sh (r, j) ->
hook_length sh (r, j) < hook_length sh (r, c).
Lemma hook_length_ltr sh r c j :
is_part sh -> r < j -> in_shape sh (j, c) ->
hook_length sh (j, c) < hook_length sh (r, c).
Lemma hook_length1_corner sh rc :
is_part sh -> in_shape sh rc ->
hook_length sh rc = 1 -> corner_box sh rc.
Lemma corner_arm_length0 sh rc :
is_part sh -> corner_box sh rc -> arm_length sh rc = 0.
Lemma corner_leg_length0 sh rc :
is_part sh -> corner_box sh rc -> leg_length sh rc = 0.
Lemma corner_hook_length1 sh rc :
is_part sh -> corner_box sh rc -> hook_length sh rc = 1.
Lemma arm_length_corner_box sh r c u v :
is_part sh ->
r <= u -> c <= v -> corner_box sh (u, v) ->
arm_length sh (r, c) = arm_length sh (u, c) + arm_length sh (r, v).
Lemma leg_length_corner_box sh r c u v :
is_part sh ->
r <= u -> c <= v -> corner_box sh (u, v) ->
leg_length sh (r, c) = leg_length sh (u, c) + leg_length sh (r, v).
Lemma hook_length_corner_box sh r c u v :
is_part sh -> r <= u -> c <= v -> corner_box sh (u, v) ->
hook_length sh (r, c) = hook_length sh (u, c) + hook_length sh (r, v) - 1.
Lemma arm_length_incr_nth_row sh r c :
in_shape sh (r, c) ->
arm_length (incr_nth sh r) (r, c) = (arm_length sh (r, c)).+1.
Lemma arm_length_incr_nth_nrow sh r c i :
i != r -> arm_length (incr_nth sh i) (r, c) = arm_length sh (r, c).
Lemma hook_length_incr_nth_row sh r c :
is_part sh -> is_add_corner sh r -> in_shape sh (r, c) ->
hook_length (incr_nth sh r) (r, c) = (hook_length sh (r, c)).+1.
Lemma hook_length_incr_nth_col sh r i :
is_part sh -> is_add_corner sh r ->
in_shape sh (i, (nth 0 sh r)) ->
hook_length (incr_nth sh r) (i, nth 0 sh r)
= (hook_length sh (i, nth 0 sh r)).+1.
Lemma hook_length_incr_nth sh i r c :
is_part sh -> is_add_corner sh i ->
in_shape sh (r, c) ->
i != r -> nth 0 sh i != c ->
hook_length (incr_nth sh i) (r, c) = hook_length sh (r, c).
Open Scope ring_scope.
Lemma hook_length_pred sh rc :
(hook_length sh rc)%:~R - 1 = ((hook_length sh rc).-1)%:~R :> rat.
Lemma prod_hook_length_quot_row p Alpha Beta :
is_part p -> corner_box p (Alpha, Beta) ->
\prod_(i <- enum_box_in (decr_nth p Alpha) | i.1 == Alpha)
( (hook_length p i)%:Q /
(hook_length (decr_nth p Alpha) i)%:Q ) =
\prod_(0 <= j < Beta) (1 + ((hook_length p (Alpha, j))%:Q - 1)^-1).
Close Scope ring_scope.
Section FindCorner.
Variable p : intpart.
Implicit Types (r c k l : nat) (rc kl : nat * nat).
#[local] Notation conj := (conj_part p).
Definition in_hook rc kl :=
let: (r, c) := rc in let: (k, l) := kl in
((r == k) && (c < l < nth 0 p r)) ||
((c == l) && (r < k < nth 0 conj c)).
Lemma in_hook_shape rc kl :
in_shape p rc -> in_hook rc kl -> in_shape p kl.
Definition hook_box_indices rc : seq (nat+nat) :=
[seq inl k | k <- iota rc.1.+1 ((nth 0 conj rc.2).-1 - rc.1)] ++
[seq inr k | k <- iota rc.2.+1 ((nth 0 p rc.1).-1 - rc.2)].
Definition hook_box rc n : nat * nat :=
match n with inl k => (k,rc.2) | inr k => (rc.1,k) end.
Definition hook_boxes rc := [seq hook_box rc n | n <- hook_box_indices rc].
Lemma size_hook_box_indices rc :
size (hook_box_indices rc) = (hook_length p rc).-1.
#[local] Lemma ltnPred a b : a < b -> (a <= b.-1).
#[local] Lemma iota_hookE a b c : a < b -> b < a.+1 + (c.-1 - a) = (b < c).
Lemma in_hook_boxesP rc kl : (kl \in hook_boxes rc) = (in_hook rc kl).
Lemma hook_boxes_empty rc :
in_shape p rc -> hook_boxes rc = [::] -> corner_box p rc.
Definition is_trace (A B : seq nat) :=
[&& (A != [::]), (B != [::]),
sorted ltn A, sorted ltn B &
corner_box p (last 0 A, last 0 B) ].
Lemma is_trace_tll a A B : A != [::] -> is_trace (a :: A) B -> is_trace A B.
Lemma is_trace_tlr b A B : B != [::] -> is_trace A (b :: B) -> is_trace A B.
Lemma is_trace_lastr (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> is_trace (a :: A) [:: last b B].
Lemma is_trace_lastl (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> is_trace [:: last a A] (b :: B).
Lemma sorted_in_leq_last A a : sorted ltn A -> a \in A -> a <= last 0 A.
Lemma sorted_leq_last A a : sorted ltn (a :: A) -> a <= last a A.
Lemma is_trace_in_in_shape (A B : seq nat) : is_trace A B ->
forall a b, a \in A -> b \in B -> in_shape p (a, b).
Lemma is_trace_in_shape (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> in_shape p (a, b).
Lemma trace_size_arm_length (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> size B <= arm_length p (a, b).
Lemma trace_size_leg_length (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> size A <= leg_length p (a, b).
Lemma size_tracer (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> size B < hook_length p (a, b).
Lemma size_tracel (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> size A < hook_length p (a, b).
Lemma is_trace_corner_nil (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) ->
(size (hook_box_indices (a, b)) == 0) = (A == [::]) && (B == [::]).
Lemma hook_length_last_rectangle (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) ->
hook_length p (a, b)
= hook_length p (last a A, b) + hook_length p (a, (last b B)) - 1.
Definition trace_seq (last : nat) : seq (seq nat) :=
[seq rcons tr last | tr : subseqs (iota 0 last)].
Definition enum_trace (Alpha Beta : nat) : seq ((seq nat) * (seq nat)) :=
[seq (A, B) | A <- trace_seq Alpha, B <- trace_seq Beta].
Lemma trace_seq_uniq l : uniq (trace_seq l).
Lemma enum_trace_uniq (Alpha Beta : nat) : uniq (enum_trace Alpha Beta).
Lemma trace_corner_box (Alpha Beta : nat) :
corner_box p (Alpha, Beta) ->
forall A B, A \in trace_seq Alpha -> B \in trace_seq Beta -> is_trace A B.
Lemma trace_seqlP (A B : seq nat) :
is_trace A B -> A \in trace_seq (last 0 A).
Lemma trace_seqrP (A B : seq nat) :
is_trace A B -> B \in trace_seq (last 0 B).
Lemma enum_traceP (Alpha Beta : nat) :
corner_box p (Alpha, Beta) ->
forall A B,
(A, B) \in enum_trace Alpha Beta =
[&& (is_trace A B), (last 0 A == Alpha) & (last 0 B == Beta)].
[&& (A != [::]), (B != [::]),
sorted ltn A, sorted ltn B &
corner_box p (last 0 A, last 0 B) ].
Lemma is_trace_tll a A B : A != [::] -> is_trace (a :: A) B -> is_trace A B.
Lemma is_trace_tlr b A B : B != [::] -> is_trace A (b :: B) -> is_trace A B.
Lemma is_trace_lastr (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> is_trace (a :: A) [:: last b B].
Lemma is_trace_lastl (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> is_trace [:: last a A] (b :: B).
Lemma sorted_in_leq_last A a : sorted ltn A -> a \in A -> a <= last 0 A.
Lemma sorted_leq_last A a : sorted ltn (a :: A) -> a <= last a A.
Lemma is_trace_in_in_shape (A B : seq nat) : is_trace A B ->
forall a b, a \in A -> b \in B -> in_shape p (a, b).
Lemma is_trace_in_shape (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> in_shape p (a, b).
Lemma trace_size_arm_length (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> size B <= arm_length p (a, b).
Lemma trace_size_leg_length (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> size A <= leg_length p (a, b).
Lemma size_tracer (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> size B < hook_length p (a, b).
Lemma size_tracel (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) -> size A < hook_length p (a, b).
Lemma is_trace_corner_nil (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) ->
(size (hook_box_indices (a, b)) == 0) = (A == [::]) && (B == [::]).
Lemma hook_length_last_rectangle (a b : nat) (A B : seq nat) :
is_trace (a :: A) (b :: B) ->
hook_length p (a, b)
= hook_length p (last a A, b) + hook_length p (a, (last b B)) - 1.
Definition trace_seq (last : nat) : seq (seq nat) :=
[seq rcons tr last | tr : subseqs (iota 0 last)].
Definition enum_trace (Alpha Beta : nat) : seq ((seq nat) * (seq nat)) :=
[seq (A, B) | A <- trace_seq Alpha, B <- trace_seq Beta].
Lemma trace_seq_uniq l : uniq (trace_seq l).
Lemma enum_trace_uniq (Alpha Beta : nat) : uniq (enum_trace Alpha Beta).
Lemma trace_corner_box (Alpha Beta : nat) :
corner_box p (Alpha, Beta) ->
forall A B, A \in trace_seq Alpha -> B \in trace_seq Beta -> is_trace A B.
Lemma trace_seqlP (A B : seq nat) :
is_trace A B -> A \in trace_seq (last 0 A).
Lemma trace_seqrP (A B : seq nat) :
is_trace A B -> B \in trace_seq (last 0 B).
Lemma enum_traceP (Alpha Beta : nat) :
corner_box p (Alpha, Beta) ->
forall A B,
(A, B) \in enum_trace Alpha Beta =
[&& (is_trace A B), (last 0 A == Alpha) & (last 0 B == Beta)].
Fixpoint walk_to_corner_rec (m : nat) (i j : nat) : distr (seq nat * seq nat) :=
if m is m'.+1 then
let s := hook_box_indices (i, j) in
(if size s is _.+1
then Mlet (Uniform (unif_def (inl 0%N) s))
(fun n => match n with
| inl k => Mlet (walk_to_corner_rec m' k j) (fun X => Munit (i::X.1, X.2))
| inr k => Mlet (walk_to_corner_rec m' i k) (fun X => Munit (X.1, j::X.2))
end)
else Munit ([::i],[::j]))
else Munit ([::i],[::j]).
Definition walk_to_corner m ij := walk_to_corner_rec m ij.1 ij.2.
Lemma walk_to_corner0_simpl r c :
walk_to_corner 0 (r, c) = Munit ([:: r], [:: c]).
Lemma walk_to_corner_end_simpl m r c :
size (hook_box_indices (r, c)) = 0 ->
walk_to_corner m (r, c) = Munit ([:: r], [:: c]).
Lemma walk_to_corner_simpl m r c :
forall (Hs : (size (hook_box_indices (r, c)) != 0)),
walk_to_corner m.+1 (r, c) =
Mlet (Uniform (mkunif (hook_box_indices (r, c)) Hs))
(fun n => match n with
| inl k => Mlet (walk_to_corner m (k, c)) (fun X => Munit (r::X.1, X.2))
| inr k => Mlet (walk_to_corner m (r, k)) (fun X => Munit (X.1, c::X.2))
end).
Open Scope ring_scope.
Lemma walk_to_corner_inv m r c :
mu (walk_to_corner m (r, c))
(fun HS => [&& size HS.1 != 0, size HS.2 != 0,
head 0 HS.1 == r& head 0 HS.2 == c]%N%:Q)
= 1.
#[local] Definition charfun A B := fun x : seq nat * seq nat => (x == (A, B))%:Q.
Lemma walk_to_corner_emptyl m rc (A B : seq nat) :
(A == [::])%B -> mu (walk_to_corner m rc) (charfun A B) = 0.
Lemma walk_to_corner_emptyr m rc (A B : seq nat) :
(B == [::])%B -> mu (walk_to_corner m rc) (charfun A B) = 0.
Lemma charfun_simpll a A B :
(fun x => charfun (a :: A) B (a :: x.1, x.2)) == charfun A B.
Lemma charfun_simplr b A B :
(fun x => charfun A (b :: B) (x.1, b :: x.2)) == charfun A B.
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.
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.
Right hand size formula of Lemma 3.
Definition RHSL3 (a b : nat) (A B : seq nat) : rat :=
\prod_(i <- belast a A) (1 / ((hook_length p (i, last b (b :: B)))%:Q - 1)) *
\prod_(j <- belast b B) (1 / ((hook_length p (last a (a :: A), j))%:Q - 1)).
Lemma Lemma3 m a b (A B : seq nat) :
(size A + size B <= m)%N -> is_trace (a :: A) (b :: B) ->
mu (walk_to_corner m (a, b)) (charfun (a :: A) (b :: B)) = RHSL3 a b A B.
\prod_(i <- belast a A) (1 / ((hook_length p (i, last b (b :: B)))%:Q - 1)) *
\prod_(j <- belast b B) (1 / ((hook_length p (last a (a :: A), j))%:Q - 1)).
Lemma Lemma3 m a b (A B : seq nat) :
(size A + size B <= m)%N -> is_trace (a :: A) (b :: B) ->
mu (walk_to_corner m (a, b)) (charfun (a :: A) (b :: B)) = RHSL3 a b A B.
Choose a box in p
Definition choose_corner : distr ((seq nat) * (seq nat)) :=
Mlet (Random (sumn p).-1)
(fun n => let (r, c) := (reshape_index p n, reshape_offset p n) in
walk_to_corner (hook_length p (r, c)).-1 (r, c)).
Section EndsAt.
Definition starts_at rc t := (head O t.1 == rc.1) && (head O t.2 == rc.2).
Definition ends_at rc t := (last O t.1 == rc.1) && (last O t.2 == rc.2).
Definition RHSL3_trace t :=
(RHSL3 (head O t.1) (head O t.2) (behead t.1) (behead t.2)).
Variable (Alpha Beta : nat).
Hypothesis Hcorn : corner_box p (Alpha, Beta).
Lemma sumnpSPE : (sumn p).-1.+1 = sumn p.
Lemma reshape_index_walk_to i (r := reshape_index p i) (c := reshape_offset p i) :
(i < sumn p)%N ->
mu (walk_to_corner (hook_length p (r, c)).-1 (r, c))
(fun pair => (ends_at (Alpha, Beta) pair)%:Q) =
\sum_(X <- enum_trace Alpha Beta | starts_at (r, c) X) RHSL3_trace X.
Lemma prob_choose_corner_ends_at :
mu choose_corner (fun pair => (ends_at (Alpha, Beta) pair)%:Q) =
1 / (sumn p)%:Q * \sum_(X <- enum_trace Alpha Beta) RHSL3_trace X.
End EndsAt.
Section Formula.
Variable T : countType.
Variable R : comRingType.
Variable alpha : T -> R.
Lemma expand_prod_add1_seq (S : seq T) :
uniq S ->
\prod_(i <- S) (1 + alpha i) = \sum_(s : subseqs S) \prod_(i <- s) alpha i.
End Formula.
Section Theorem2.
Variable (Alpha Beta : nat).
Hypothesis Hcorn : corner_box p (Alpha, Beta).
Let p' := decr_nth p Alpha.
Fact Hcrn : is_rem_corner p Alpha.
Hint Resolve Hcrn : core.
Fact Hp : incr_nth p' Alpha = p.
Fact Hpart' : is_part p'.
Let Hpartc' : is_part (conj_part p') := is_part_conj Hpart'.
Hint Resolve Hpart' Hpartc' : core.
Fact HBeta : Beta = (nth O p Alpha).-1.
Fact HBeta' : Beta = (nth O p' Alpha).
Lemma Formula1 :
(hook_length_prod p)%:Q / (hook_length_prod p')%:Q =
( \prod_(0 <= i < Alpha) (1 + ((hook_length p (i, Beta) )%:Q - 1)^-1) ) *
( \prod_(0 <= j < Beta) (1 + ((hook_length p (Alpha, j))%:Q - 1)^-1) ).
Lemma SimpleCalculation :
\sum_(X <- enum_trace Alpha Beta) RHSL3_trace X =
(hook_length_prod p)%:Q / (hook_length_prod p')%:Q.
Theorem Theorem2 :
mu choose_corner (fun pair => (ends_at (Alpha, Beta) pair)%:Q) =
(HLF p') / (HLF p).
End Theorem2.
Open Scope ring_scope.
Lemma ends_at_rem_cornerE :
(fun X : seq nat * seq nat =>
\sum_(i0 <- rem_corners p) (ends_at (i0, (nth O p i0).-1) X)%:Q)
== (fun X => (corner_box p (last O X.1, last O X.2))%:Q).
Corollary Corollary4 :
p != empty_intpart ->
\sum_(i <- rem_corners p) (HLF (decr_nth p i)) / (HLF p) = 1.
Corollary Corollary4_eq :
p != empty_intpart ->
\sum_(i <- rem_corners p) (HLF (decr_nth_intpart p i)) = HLF p.
End FindCorner.
Theorem HookLengthFormula_rat (p : intpart) :
( (#|{:stdtabsh p}|)%:Q = HLF p )%R.
Lemma hook_length_prod_non0 (p : intpart) : (hook_length_prod p) != 0.
Lemma hook_length_prod_nat (p : intpart) :
#|{:stdtabsh p}| * (hook_length_prod p) = (sumn p)`!.
Lemma hook_length_prod_div (p : intpart) : (hook_length_prod p) %| (sumn p)`!.
Theorem HookLengthFormula (p : intpart) :
#|{:stdtabsh p}| = (sumn p)`! %/ (hook_length_prod p).
Variable T : countType.
Variable R : comRingType.
Variable alpha : T -> R.
Lemma expand_prod_add1_seq (S : seq T) :
uniq S ->
\prod_(i <- S) (1 + alpha i) = \sum_(s : subseqs S) \prod_(i <- s) alpha i.
End Formula.
Section Theorem2.
Variable (Alpha Beta : nat).
Hypothesis Hcorn : corner_box p (Alpha, Beta).
Let p' := decr_nth p Alpha.
Fact Hcrn : is_rem_corner p Alpha.
Hint Resolve Hcrn : core.
Fact Hp : incr_nth p' Alpha = p.
Fact Hpart' : is_part p'.
Let Hpartc' : is_part (conj_part p') := is_part_conj Hpart'.
Hint Resolve Hpart' Hpartc' : core.
Fact HBeta : Beta = (nth O p Alpha).-1.
Fact HBeta' : Beta = (nth O p' Alpha).
Lemma Formula1 :
(hook_length_prod p)%:Q / (hook_length_prod p')%:Q =
( \prod_(0 <= i < Alpha) (1 + ((hook_length p (i, Beta) )%:Q - 1)^-1) ) *
( \prod_(0 <= j < Beta) (1 + ((hook_length p (Alpha, j))%:Q - 1)^-1) ).
Lemma SimpleCalculation :
\sum_(X <- enum_trace Alpha Beta) RHSL3_trace X =
(hook_length_prod p)%:Q / (hook_length_prod p')%:Q.
Theorem Theorem2 :
mu choose_corner (fun pair => (ends_at (Alpha, Beta) pair)%:Q) =
(HLF p') / (HLF p).
End Theorem2.
Open Scope ring_scope.
Lemma ends_at_rem_cornerE :
(fun X : seq nat * seq nat =>
\sum_(i0 <- rem_corners p) (ends_at (i0, (nth O p i0).-1) X)%:Q)
== (fun X => (corner_box p (last O X.1, last O X.2))%:Q).
Corollary Corollary4 :
p != empty_intpart ->
\sum_(i <- rem_corners p) (HLF (decr_nth p i)) / (HLF p) = 1.
Corollary Corollary4_eq :
p != empty_intpart ->
\sum_(i <- rem_corners p) (HLF (decr_nth_intpart p i)) = HLF p.
End FindCorner.
Theorem HookLengthFormula_rat (p : intpart) :
( (#|{:stdtabsh p}|)%:Q = HLF p )%R.
Lemma hook_length_prod_non0 (p : intpart) : (hook_length_prod p) != 0.
Lemma hook_length_prod_nat (p : intpart) :
#|{:stdtabsh p}| * (hook_length_prod p) = (sumn p)`!.
Lemma hook_length_prod_div (p : intpart) : (hook_length_prod p) %| (sumn p)`!.
Theorem HookLengthFormula (p : intpart) :
#|{:stdtabsh p}| = (sumn p)`! %/ (hook_length_prod p).