Documentation

YoungDiagram.Chromosome.Rank

def Chromosome.maxRank (c : Chromosome) :

Equations

c.maxRank = c.support.sup Gene.rank

Instances For

theorem Chromosome.maxRank_def {X : Chromosome} :

X.maxRank = X.support.sup Gene.rank

theorem Chromosome.maxRank_zero :

theorem Chromosome.le_maxRank {X : Chromosome} (g : Gene) :

g ∈ X.support → g.rank ≤ X.maxRank

theorem Chromosome.add_maxRank {X Y : Chromosome} :

(X + Y).maxRank = max X.maxRank Y.maxRank

theorem Chromosome.smul_maxRank {X : Chromosome} {n : ℕ} (hn : n ≠ 0) :

(n • X).maxRank = X.maxRank

theorem Chromosome.maxRank_ofRank {n : ℕ} {ε : GeneType} :

(Gene.ofRank n ε).maxRank = n

theorem Chromosome.maxRank_eq_zero {X : Chromosome} (h : X.maxRank = 0) :

X = 0

theorem Chromosome.maxRank_neg {X : Chromosome} :

(-X).maxRank = X.maxRank

theorem Chromosome.maxRank_prime_lt {X : Chromosome} (hX : X ≠ 0) :

(prime X).maxRank < X.maxRank

noncomputable def Chromosome.rank :

Chromosome →+ ℕ

Equations

Chromosome.rank = Finsupp.weight Gene.rank

Instances For

theorem Chromosome.rank_def {X : Chromosome} :

rank X = Finsupp.sum X fun (g : Gene) (count : ℕ) => count • g.rank

theorem Chromosome.rank_zero {X : Chromosome} (h : rank X = 0) :

X = 0

theorem Chromosome.rank_zero_iff {X : Chromosome} :

rank X = 0 ↔ X = 0

theorem Chromosome.rank_single {n : ℕ} {g : Gene} :

rank (Finsupp.single g n) = n • g.rank

theorem Chromosome.rank_sub_single {X : Chromosome} {g : Gene} (hg : 0 < X g) :

rank (X - Finsupp.single g 1) = rank X - g.rank

theorem Chromosome.rank_ofRank {n : ℕ} {ε : GeneType} :

rank (Gene.ofRank n ε) = n

theorem Chromosome.rank_neg {X : Chromosome} :

rank (-X) = rank X

theorem Chromosome.signature_sum_neg_eq_rank {X : Chromosome} :

signature X + signature (-X) = ↑(rank X)

theorem Chromosome.rank_one {X : Chromosome} (hrank : rank X = 1) :

∃ (ε : GeneType), X = Gene.ofRank 1 ε

theorem Chromosome.rank_of_prime {X : Chromosome} :

rank (prime X) = Finsupp.sum X fun (g : Gene) (m : ℕ) => m * (g.rank - 1)

theorem Chromosome.prime_rank_lt {X : Chromosome} (hne : X ≠ 0) :

rank (prime X) < rank X

theorem Chromosome.prime_iterate_rank_lt_of_ne_zero {X : Chromosome} {k : ℕ} (hk : 0 < k) (hne : (⇑prime)^[k] X ≠ 0) :

rank ((⇑prime)^[k] X) < rank X

theorem Chromosome.signature_sum_eq_rank {X : Chromosome} :

(signature X).1 + (signature X).2 = ↑(rank X)

theorem Chromosome.signature_eq_zero {X : Chromosome} (h : signature X = 0) :

X = 0

theorem Chromosome.maxRank_le_rank (X : Chromosome) :

X.maxRank ≤ rank X

theorem Chromosome.rank_eq_maxRank_single {X : Chromosome} (h : rank X = X.maxRank) (hpos : 0 < X.maxRank) :

∃ (g : Gene), g.rank = X.maxRank ∧ X = Finsupp.single g 1

theorem Chromosome.prime_iterate_zero_of_maxRank_le {X : Chromosome} {k : ℕ} (h : X.maxRank ≤ k) :

(⇑prime)^[k] X = 0