Hook bounds on induction and Kronecker multiplicities

Deligne 1.10 and 1.12, character side: if the induction multiplicity [λ : μ, ν] is nonzero and λ contains the cell (p + r, q + s), then μ contains (p, q) or ν contains (r, s); and the Kronecker analogue at (pr + qs, ps + qr). Both by evaluation: the Schur specialisation of λ at the corresponding super power sum vanishes, every term of the bilinear splitting is a natural number, so every term vanishes; hook positivity makes the two specialisation factors nonzero, killing the multiplicity.

theorem RS.eq_zero_of_sum_nat_eq_zero {ι : Type u_1} {s : Finset ι} {f : ι → ℂ} (h : ∀ i ∈ s, ∃ (m : ℕ), f i = ↑m) (h0 : ∑ i ∈ s, f i = 0) (i : ι) : i ∈ s → f i = 0

A finite sum of natural values vanishing termwise: if every summand is a natural number and the sum is zero, each summand is zero.

theorem RS.indMult_eq_zero_of_cells {a b : ℕ} (lam : Shape (a + b)) (μ : Shape a) (ν : Shape b) {p q r s : ℕ} (hμ : (p, q) ∉ ↑μ) (hν : (r, s) ∉ ↑ν) (hlam : (p + r, q + s) ∈ ↑lam) : indMult lam μ ν = 0

Deligne 1.10, character side: an induction multiplicity dies against the fat hook — if λ contains (p + r, q + s) while μ avoids (p, q) and ν avoids (r, s), then [λ : μ, ν] = 0.

theorem RS.cell_of_indMult_ne_zero {a b : ℕ} (lam : Shape (a + b)) (μ : Shape a) (ν : Shape b) {p q r s : ℕ} (h : indMult lam μ ν ≠ 0) (hlam : (p + r, q + s) ∈ ↑lam) : (p, q) ∈ ↑μ ∨ (r, s) ∈ ↑ν

Deligne 1.10 in its positive form: a nonzero induction multiplicity pushes a fat-hook cell of λ into μ or ν.

theorem RS.kronMult_eq_zero_of_cells {n : ℕ} (lam μ ν : Shape n) {p q r s : ℕ} (hμ : (p, q) ∉ ↑μ) (hν : (r, s) ∉ ↑ν) (hlam : (p * r + q * s, p * s + q * r) ∈ ↑lam) : kronMult lam μ ν = 0

Deligne 1.12, character side: a Kronecker multiplicity dies against the product hook.

theorem RS.cell_of_kronMult_ne_zero {n : ℕ} (lam μ ν : Shape n) {p q r s : ℕ} (h : kronMult lam μ ν ≠ 0) (hlam : (p * r + q * s, p * s + q * r) ∈ ↑lam) : (p, q) ∈ ↑μ ∨ (r, s) ∈ ↑ν

Deligne 1.12 in its positive form.