The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.
Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.
abbreviation OAI.Thorp.Position line 14
abbrev Position (d : ℕ) := Fin d → Bool
definition OAI.Thorp.Block.perm line 20
def perm (p : I → Equiv.Perm β) : Equiv.Perm (I × β) where toFun x := (x.1, p x.1 x.2) invFun x := (x.1, (p x.1)⁻¹ x.2) left_inv x := by simp right_inv x := by simp
definition OAI.Thorp.Block.hom line 26
def hom : (I → Equiv.Perm β) →* Equiv.Perm (I × β) where toFun := perm map_one' := by ext ⟨i,b⟩ <;> rfl map_mul' p q := by ext ⟨i,b⟩ <;> rfl
definition OAI.Thorp.Block.embedding line 31
def embedding (e : α ≃ I × β) : (I → Equiv.Perm β) →* Equiv.Perm α := (e.symm.permCongrHom).toMonoidHom.comp hom
definition OAI.Thorp.Fourier.integrated line 41
def integrated (ρ : Representation ℂ G V) (f : G → ℂ) : Module.End ℂ V := ∑ g, f g • ρ g
abbreviation OAI.Thorp.Young.Cells line 48
abbrev Cells (D : YoungDiagram) := {p : ℕ × ℕ // p ∈ D.cells}
definition OAI.Thorp.Young.rowCellsEquiv line 50
def rowCellsEquiv (D : YoungDiagram) : Cells D ≃ (i : Fin (D.colLen 0)) × Fin (D.rowLen i) where toFun x := ⟨⟨x.val.1, YoungDiagram.mem_iff_lt_colLen.mp (D.up_left_mem le_rfl (Nat.zero_le _) x.property)⟩, ⟨x.val.2, YoungDiagram.mem_iff_lt_rowLen.mp x.property⟩⟩ invFun x := ⟨(x.1, x.2), YoungDiagram.mem_iff_lt_rowLen.mpr x.2.isLt⟩ left_inv x := rfl right_inv x := by cases x; rfl
definition OAI.Thorp.Young.ofPartition line 57
def ofPartition {n : ℕ} (p : Nat.Partition n) : YoungDiagram := YoungDiagram.ofRowLens (p.parts.sort (· ≥ ·)) (Multiset.pairwise_sort _ _).sortedGE
definition OAI.Thorp.Young.longest line 60
def longest (D : YoungDiagram) : ℕ := max (D.rowLen 0) (D.colLen 0)
definition OAI.Thorp.Specht.cyclic line 69
def cyclic (ρ : Representation ℂ G E) (e : E) : Subrepresentation ρ where
Show the remaining 12 lines
toSubmodule := Submodule.span ℂ (Set.range fun g => ρ g e) apply_mem_toSubmodule g := by intro v hv induction hv using Submodule.span_induction with | mem v hv => obtain ⟨h, rfl⟩ := hv exact Submodule.subset_span ⟨g * h, by simp⟩ | zero => simp | add x y hx hy ihx ihy => simpa using (Submodule.span ℂ (Set.range fun h => ρ h e)).add_mem ihx ihy | smul a x hx ih => simpa using (Submodule.span ℂ (Set.range fun h => ρ h e)).smul_mem a ih
definition OAI.Thorp.Specht.PermutationSpace.rep line 87
def rep : Representation ℂ G (EuclideanSpace ℂ X) where
Show the remaining 10 lines
toFun g := { toFun v := WithLp.toLp 2 (fun x => v (g⁻¹ • x)) map_add' := by intro v w; rfl map_smul' := by intro a v; rfl } map_one' := by ext v x; simp map_mul' := by intro g h ext v x change v ((g * h)⁻¹ • x) = v (h⁻¹ • g⁻¹ • x) simp [mul_smul]
definition OAI.Thorp.Specht.PermutationSpace.alternator line 101
def alternator (ι : H →* G) (χ : H →* ℂ) : Module.End ℂ (EuclideanSpace ℂ X) := ∑ h, χ h • rep (ι h)
definition OAI.Thorp.Specht.Tabloid line 108
def Tabloid (r : α → ℕ) := {f : α → ℕ // ∃ g : Equiv.Perm α, f = r ∘ g}
definition OAI.Thorp.Specht.baseTabloid line 130
def baseTabloid (r : α → ℕ) : Tabloid r := ⟨r, 1, by funext x; rfl⟩
definition OAI.Thorp.Specht.fiberGroup line 132
def fiberGroup (c : α → ℕ) : Subgroup (Equiv.Perm α) where carrier := {g | ∀ x, c (g x) = c x} one_mem' := by intro x; rfl mul_mem' := by intro g h hg hh x; exact (hg (h x)).trans (hh x) inv_mem' := by intro g hg x have hh := hg (g⁻¹ x) change c (g (g.symm x)) = c (g.symm x) at hh rw [g.apply_symm_apply] at hh exact hh.symm
definition OAI.Thorp.Specht.complexSign line 143
def complexSign : Equiv.Perm α →* ℂ where toFun g := ((Equiv.Perm.sign g : ℤˣ) : ℤ) map_one' := by simp map_mul' := by intro g h; simp
definition OAI.Thorp.Specht.tableauRow line 150
def tableauRow (x : α) : ℕ := (t x).val.1
definition OAI.Thorp.Specht.tableauCol line 152
def tableauCol (x : α) : ℕ := (t x).val.2
definition OAI.Thorp.Specht.tabloidRep line 154
def tabloidRep : Representation ℂ (Equiv.Perm α) (EuclideanSpace ℂ (Tabloid (tableauRow D t))) := PermutationSpace.rep
definition OAI.Thorp.Specht.columnAlternator line 157
def columnAlternator : Module.End ℂ (EuclideanSpace ℂ (Tabloid (tableauRow D t))) := PermutationSpace.alternator (fiberGroup (tableauCol D t)).subtype (complexSign.comp (fiberGroup (tableauCol D t)).subtype)
definition OAI.Thorp.Specht.polytabloid line 161
def polytabloid : EuclideanSpace ℂ (Tabloid (tableauRow D t)) := columnAlternator D t (EuclideanSpace.single (baseTabloid (tableauRow D t)) (1 : ℂ))
definition OAI.Thorp.Specht.module line 164
def module : Subrepresentation (tabloidRep D t) := cyclic (tabloidRep D t) (polytabloid D t)
abbreviation OAI.Thorp.Specht.Shape line 166
abbrev Shape (α : Type uα) [Fintype α] := Nat.Partition (Fintype.card α)
definition OAI.Thorp.Specht.canonicalTableau line 168
def canonicalTableau (p : Shape α) : α ≃ Thorp.Young.Cells (Thorp.Young.ofPartition p) := by
Show the remaining 13 lines
have card_cells_eq_sum (D : YoungDiagram) : Fintype.card (Thorp.Young.Cells D) = D.rowLens.sum := by rw [Fintype.card_congr (Thorp.Young.rowCellsEquiv D), Fintype.card_sigma] simp only [Fintype.card_fin, YoungDiagram.rowLens] rw [← List.sum_toFinset _ List.nodup_range, List.toFinset_range, Finset.sum_range] have rowLens_ofPartition {n : ℕ} (p : Nat.Partition n) : (Thorp.Young.ofPartition p).rowLens = p.parts.sort (· ≥ ·) := by apply YoungDiagram.rowLens_ofRowLens_eq_self intro x hx exact p.parts_pos ((Multiset.mem_sort _).mp hx) have card_ofPartition {n : ℕ} (p : Nat.Partition n) : Fintype.card (Thorp.Young.Cells (Thorp.Young.ofPartition p)) = n := by rw [card_cells_eq_sum, rowLens_ofPartition] simpa only [← Multiset.sum_coe, Multiset.sort_eq] using p.parts_sum exact Fintype.equivOfCardEq (card_ofPartition p).symm
7 more definitions are reached the same way; the full file lists them.