Basic.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.RowColumn.lineGroup line 13
Source documentation
Permutations preserving each fibre of a given line map.
Also declared: ComparatorChallenges/OccupiedOverlap.lean:182 (same declaration text).
```
def lineGroup {α β : Type*} (f : α → β) : Subgroup (Equiv.Perm α) where
…
```
abbrev OAI.RowColumn.Board line 23
Also declared: ComparatorChallenges/OccupiedOverlap.lean:192 (same declaration text).
abbrev OAI.RowColumn.rowGroup line 24
Also declared: ComparatorChallenges/OccupiedOverlap.lean:193 (same declaration text).
abbrev OAI.RowColumn.columnGroup line 26
Also declared: ComparatorChallenges/OccupiedOverlap.lean:195 (same declaration text).
def OAI.RowColumn.InHook line 30
Source documentation
Zero-based form of the manuscript's (h,h)-hook.
Also declared: ComparatorChallenges/OccupiedOverlap.lean:199 (same declaration text).
```
def InHook (a : YoungDiagram) (h : ℕ) : Prop :=
…
```
def OAI.RowColumn.Intertwines line 39
Source documentation
An actual equivariant inclusion, not an unspecified overlap matrix.
Also declared: ComparatorChallenges/OccupiedOverlap.lean:208 (same declaration text).
```
def Intertwines (ρ : Representation ℂ G V) (τ : Representation ℂ G W)
    (I : V →ₗ[ℂ] W) : Prop :=
…
```
def OAI.RowColumn.CompleteCopies line 46
Source documentation
All orthogonal multiplicity copies of one irreducible type. The completeness condition quantifies over genuine intertwiners, i.e. it is exactly the isotypic space condition.
Also declared: ComparatorChallenges/OccupiedOverlap.lean:215 (same declaration text).
```
def CompleteCopies (ρ : Representation ℂ G V) (τ : Representation ℂ G W)
    {u : ℕ} (I : Fin u → V →ₗᵢ[ℂ] W) : Prop :=
…
```

def OAI.RowColumn.allCopyOverlap line 56

Source documentation

The all-copy operator-overlap sum, with each squared operator norm.

Also declared: ComparatorChallenges/OccupiedOverlap.lean:225 (same declaration text).

def allCopyOverlap {V W X : Type*}
    [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]
    [NormedAddCommGroup W] [InnerProductSpace ℂ W] [FiniteDimensional ℂ W]
    [NormedAddCommGroup X] [InnerProductSpace ℂ X] [FiniteDimensional ℂ X]
    {u v : ℕ} (I : Fin u → V →ₗᵢ[ℂ] X) (J : Fin v → W →ₗᵢ[ℂ] X) : ℝ :=
…

abbrev OAI.RowColumn.OccupiedOverlapEndpoint line 68
Source documentation
Exact occupied-board main. Carriers are in orthonormal coordinates; arbitrary unitary irreducibles of the two actual line groups are quantified over (equivalently, the tuples of line partitions in the manuscript). Labelling e chooses the action of the Specht module on the occupied cells and forces |a| = |Ω|.
Also declared: ComparatorChallenges/OccupiedOverlap.lean:237 (same declaration text).
```
abbrev OccupiedOverlapEndpoint : Prop :=
…
```