Highest-weight identities #

(S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) = ((precedingDiamondSubset pivot S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ (succeedingDiamondSubset pivot S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.sort_insert_eq_preceding_cons_succeeding {r : ℕ} (pivot : Fin (r + 1)) (S : Finset (Fin (r + 1))) (hpivot : pivot ∉ S) :

((insert pivot S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) = ((precedingDiamondSubset pivot S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ pivot :: (succeedingDiamondSubset pivot S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.omittedDiamondPrefix {r n : ℕ} (target : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (front : List (Fin (r + 1))) (next : Fin (r + 1)) :

PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n

The axial lowering-path prefix with the pivot omitted.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.insertedDiamondPrefix {r n : ℕ} (target pivot : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (front : List (Fin (r + 1))) (next : Fin (r + 1)) :

PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n

The axial lowering-path prefix with the pivot inserted, followed by its connecting polarization.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.diamondPathOperator_eq_omittedPrefix_comp_suffix {r n : ℕ} (target : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (front : List (Fin (r + 1))) (next : Fin (r + 1)) (tail : List (Fin (r + 1))) (hsplit : (S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target] = front ++ next :: tail) :

ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator target k S = omittedDiamondPrefix target k S front next ∘ₗ AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (next :: tail)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.diamondPathOperator_eq_insertedPrefix_comp_suffix {r n : ℕ} (target pivot : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (front : List (Fin (r + 1))) (next : Fin (r + 1)) (tail : List (Fin (r + 1))) (hsplit : ((insert pivot S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target] = front ++ pivot :: next :: tail) :

ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator target k (insert pivot S) = insertedDiamondPrefix target pivot k S front next ∘ₗ AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (next :: tail)

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.diamondPrefixResidual {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target pivot : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (front : List (Fin (r + 1))) (next : Fin (r + 1)) :

PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n

The commutator residual comparing the inserted and omitted diamond prefixes.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.diamondPairResidual_eq_prefix_comp_suffix {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target pivot : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (front : List (Fin (r + 1))) (next : Fin (r + 1)) (tail : List (Fin (r + 1))) (homit : (S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target] = front ++ next :: tail) (hinsert : ((insert pivot S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target] = front ++ pivot :: next :: tail) (hnext : pivot < next) (htail : ∀ a ∈ tail, pivot < a) :

ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual lam target pivot k S = diamondPrefixResidual lam target pivot k S front next ∘ₗ AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (next :: tail)

source

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff {r : ℕ} (lam : Fin (r + 1) → ℕ) (pivot : Fin (r + 1)) (t : ℝ) (S : Finset (Fin (r + 1))) :

ℝ

The signed product of spectrally shifted row gaps outside the selected path subset.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator {r n : ℕ} (lam : Fin (r + 1) → ℕ) (pivot target : Fin (r + 1)) (k : Fin n) (t : ℝ) :

PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n

The sum of diamond path operators weighted by their spectrally shifted coefficients.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator_apply {r n : ℕ} (lam : Fin (r + 1) → ℕ) (pivot target : Fin (r + 1)) (k : Fin n) (t : ℝ) (p : PolynomialSpace r n) :

(spectralPathOperator lam pivot target k t) p = ∑ S ∈ (AllRankArbitraryRowBranchingOperator.precedingRows pivot).powerset, spectralPathCoeff lam pivot t S • (ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator target k S) p

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff_zero {r : ℕ} (lam : Fin (r + 1) → ℕ) (pivot : Fin (r + 1)) (S : Finset (Fin (r + 1))) :

spectralPathCoeff lam pivot 0 S = AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam pivot S

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator_self_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (pivot : Fin (r + 1)) (k : Fin n) :

spectralPathOperator lam pivot pivot k 0 = AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff_insert {r : ℕ} (lam : Fin (r + 1) → ℕ) (pivot a : Fin (r + 1)) (t : ℝ) (S : Finset (Fin (r + 1))) (ha : a < pivot) (haS : a ∉ S) :

spectralPathCoeff lam pivot t S = -(AllRankArbitraryRowBranchingOperator.shiftedRowGap lam pivot a + t) * spectralPathCoeff lam pivot t (insert a S)

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator_zero_pivot {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target : Fin (r + 1)) (k : Fin n) (t : ℝ) :

spectralPathOperator lam 0 target k t = LinearMap.mulLeft ℝ (MvPolynomial.X (variableIndex target k))

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.shiftedRowGap_succ_eq_add_predecessor {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (a : Fin r) (b : Fin (r + 1)) (hb : b < a.castSucc) :

AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.succ b = AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.castSucc b + AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.succ a.castSucc + 1

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff_succ_insert_predecessor {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (a : Fin r) (t : ℝ) (S : Finset (Fin (r + 1))) (hS : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows a.castSucc) :

spectralPathCoeff lam a.succ t (insert a.castSucc S) = -spectralPathCoeff lam a.castSucc (t + AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.succ a.castSucc + 1) S

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff_succ_of_preceding {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (a : Fin r) (t : ℝ) (S : Finset (Fin (r + 1))) (hS : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows a.castSucc) :

spectralPathCoeff lam a.succ t S = (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.succ a.castSucc + t) * spectralPathCoeff lam a.castSucc (t + AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.succ a.castSucc + 1) S

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.diamondPathOperator_insert_predecessor {r n : ℕ} (a : Fin r) (target : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (hS : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows a.castSucc) :

ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator target k (insert a.castSucc S) = ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator a.castSucc k S ∘ₗ polarization r n target a.castSucc

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator_succ {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (a : Fin r) (target : Fin (r + 1)) (k : Fin n) (t : ℝ) :

spectralPathOperator lam a.succ target k t = (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.succ a.castSucc + t) • spectralPathOperator lam a.castSucc target k (t + AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.succ a.castSucc + 1) - spectralPathOperator lam a.castSucc a.castSucc k (t + AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.succ a.castSucc + 1) ∘ₗ polarization r n target a.castSucc

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSubset_eq_preceding_union_succeeding {r : ℕ} (pivot : Fin (r + 1)) (S : Finset (Fin (r + 1))) (hpivot : pivot ∉ S) :

S = ArbitraryRowSameAxisDiamondResidualSuffixPartition.precedingDiamondSubset pivot S ∪ ArbitraryRowSameAxisDiamondResidualSuffixPartition.succeedingDiamondSubset pivot S

source

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows {r : ℕ} (target pivot : Fin (r + 1)) :

Finset (Fin (r + 1))

The rows strictly between the pivot and the target.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.mem_diamondSucceedingRows {r : ℕ} (target pivot a : Fin (r + 1)) :

a ∈ diamondSucceedingRows target pivot ↔ a < target ∧ pivot < a

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondOmittedRows_eq_preceding_union_succeeding {r : ℕ} (target pivot : Fin (r + 1)) (hpivot : pivot < target) (S : Finset (Fin (r + 1))) :

AllRankArbitraryRowBranchingOperator.precedingRows target \ insert pivot S = AllRankArbitraryRowBranchingOperator.precedingRows pivot \ ArbitraryRowSameAxisDiamondResidualSuffixPartition.precedingDiamondSubset pivot S ∪ diamondSucceedingRows target pivot \ ArbitraryRowSameAxisDiamondResidualSuffixPartition.succeedingDiamondSubset pivot S

source

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.upperDiamondPathCoefficient {r : ℕ} (lam : Fin (r + 1) → ℕ) (target pivot : Fin (r + 1)) (S : Finset (Fin (r + 1))) :

ℝ

The signed product of row gaps contributed by the upper part of a diamond path.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.shiftedRowGap_target_eq_pivot_add_spectralShift {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (target pivot a : Fin (r + 1)) (hpivot : pivot < target) (ha : a < pivot) :

AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target a = AllRankArbitraryRowBranchingOperator.shiftedRowGap lam pivot a + (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target pivot + 1)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.polarizationPathCoefficient_insert_pivot_factor {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (target pivot : Fin (r + 1)) (hpivot : pivot < target) (S : Finset (Fin (r + 1))) (hS : pivot ∉ S) :

AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target (insert pivot S) = -upperDiamondPathCoefficient lam target pivot S * ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff lam pivot (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target pivot + 1) (ArbitraryRowSameAxisDiamondResidualSuffixPartition.precedingDiamondSubset pivot S)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.sum_powerset_disjoint_union {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] (lower upper : Finset α) (hdisjoint : Disjoint lower upper) (f : Finset α → M) :

∑ S ∈ (lower ∪ upper).powerset, f S = ∑ U ∈ upper.powerset, ∑ L ∈ lower.powerset, f (L ∪ U)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.precedingRows_erase_pivot_eq_union {r : ℕ} (target pivot : Fin (r + 1)) (hpivot : pivot < target) :

(AllRankArbitraryRowBranchingOperator.precedingRows target).erase pivot = AllRankArbitraryRowBranchingOperator.precedingRows pivot ∪ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.precedingRows_disjoint_diamondSucceedingRows {r : ℕ} (target pivot : Fin (r + 1)) :

Disjoint (AllRankArbitraryRowBranchingOperator.precedingRows pivot) (ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.precedingDiamondSubset_union {r : ℕ} (target pivot : Fin (r + 1)) (L U : Finset (Fin (r + 1))) (hL : L ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (hU : U ⊆ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot) :

ArbitraryRowSameAxisDiamondResidualSuffixPartition.precedingDiamondSubset pivot (L ∪ U) = L

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.succeedingDiamondSubset_union {r : ℕ} (target pivot : Fin (r + 1)) (L U : Finset (Fin (r + 1))) (hL : L ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (hU : U ⊆ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot) :

ArbitraryRowSameAxisDiamondResidualSuffixPartition.succeedingDiamondSubset pivot (L ∪ U) = U

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.pivot_not_mem_preceding_union_succeeding {r : ℕ} (target pivot : Fin (r + 1)) (L U : Finset (Fin (r + 1))) (hL : L ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (hU : U ⊆ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot) :

pivot ∉ L ∪ U

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.polarizationPathCoefficient_insert_union_factor {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (target pivot : Fin (r + 1)) (hpivot : pivot < target) (L U : Finset (Fin (r + 1))) (hL : L ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (hU : U ⊆ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot) :

AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target (insert pivot (L ∪ U)) = -ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.upperDiamondPathCoefficient lam target pivot U * ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff lam pivot (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target pivot + 1) L

source

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.diamondUpperSuffixNext {r : ℕ} (target : Fin (r + 1)) (U : Finset (Fin (r + 1))) :

Fin (r + 1)

The first row in the sorted upper suffix, with the target appended as a final row.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.diamondUpperSuffixNext target U = ((U.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target]).headD target

Instances For

source

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.diamondUpperSuffixTail {r : ℕ} (target : Fin (r + 1)) (U : Finset (Fin (r + 1))) :

List (Fin (r + 1))

The remaining rows after removing the first row of the upper diamond suffix.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.diamondUpperSuffixTail target U = ((U.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target]).tail

Instances For

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.upperDiamondSuffix_eq_next_cons_tail {r : ℕ} (target : Fin (r + 1)) (U : Finset (Fin (r + 1))) :

(U.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target] = diamondUpperSuffixNext target U :: diamondUpperSuffixTail target U

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.polarizationPathStart_union_eq_lower_next {r : ℕ} (target pivot next : Fin (r + 1)) (L U : Finset (Fin (r + 1))) (tail : List (Fin (r + 1))) (hL : L ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (hU : U ⊆ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot) (hupper : (U.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target] = next :: tail) :

AllRankArbitraryRowBranchingOperator.polarizationPathStart target (L ∪ U) = AllRankArbitraryRowBranchingOperator.polarizationPathStart next L

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.polarizationPathStart_insert_union_eq_lower_pivot {r : ℕ} (target pivot : Fin (r + 1)) (L U : Finset (Fin (r + 1))) (hL : L ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (hU : U ⊆ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot) :

AllRankArbitraryRowBranchingOperator.polarizationPathStart target (insert pivot (L ∪ U)) = AllRankArbitraryRowBranchingOperator.polarizationPathStart pivot L

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.omittedDiamondPrefix_union_eq_lowerPath {r n : ℕ} (target pivot next : Fin (r + 1)) (k : Fin n) (L U : Finset (Fin (r + 1))) (tail : List (Fin (r + 1))) (hL : L ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (hU : U ⊆ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot) (hupper : (U.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target] = next :: tail) :

ArbitraryRowSameAxisDiamondResidualSuffixPartition.omittedDiamondPrefix target k (L ∪ U) (L.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) next = ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator next k L

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.insertedDiamondPrefix_union_eq_lowerPath_comp_root {r n : ℕ} (target pivot next : Fin (r + 1)) (k : Fin n) (L U : Finset (Fin (r + 1))) (hL : L ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (hU : U ⊆ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot) :

ArbitraryRowSameAxisDiamondResidualSuffixPartition.insertedDiamondPrefix target pivot k (L ∪ U) (L.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) next = ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator pivot k L ∘ₗ polarization r n next pivot

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.localSpectralDiamondResidual {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target pivot next : Fin (r + 1)) (k : Fin n) (L : Finset (Fin (r + 1))) :

PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n

The local commutator residual for a diamond prefix ending at the next suffix row.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.spectralDiamondPrefixResidual {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target pivot next : Fin (r + 1)) (k : Fin n) :

PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n

The spectral-path commutator residual associated with a diamond prefix and its next row.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.spectralDiamondResidualTransform {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target pivot next : Fin (r + 1)) (k : Fin n) :

(PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n) × (PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n) →ₗ[ℝ ] PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n

The linear transformation combining diagonal and off-diagonal operators into a diamond residual.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.spectralDiamondResidualTransform_apply {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target pivot next : Fin (r + 1)) (k : Fin n) (A B : PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n) :

(spectralDiamondResidualTransform lam target pivot next k) (A, B) = (A ∘ₗ polarization r n next pivot) ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ A ∘ₗ polarization r n next pivot - AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target pivot • (B ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ B) - B ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.sum_spectralLocalDiamondResidual_eq_spectralPrefix {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target pivot next : Fin (r + 1)) (k : Fin n) :

∑ L ∈ (AllRankArbitraryRowBranchingOperator.precedingRows pivot).powerset, ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff lam pivot (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target pivot + 1) L • localSpectralDiamondResidual lam target pivot next k L = spectralDiamondPrefixResidual lam target pivot next k

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.diamondPairResidual_union_eq_local_comp_suffix {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target pivot next : Fin (r + 1)) (hpivot : pivot < target) (k : Fin n) (L U : Finset (Fin (r + 1))) (tail : List (Fin (r + 1))) (hL : L ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (hU : U ⊆ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot) (hupper : (U.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target] = next :: tail) :

ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual lam target pivot k (L ∪ U) = localSpectralDiamondResidual lam target pivot next k L ∘ₗ AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (next :: tail)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.sum_weightedDiamondPairResidual_eq_sum_upper_lower {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (target pivot : Fin (r + 1)) (hpivot : pivot < target) (k : Fin n) :

∑ S ∈ ((AllRankArbitraryRowBranchingOperator.precedingRows target).erase pivot).powerset, AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target (insert pivot S) • ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual lam target pivot k S = -∑ U ∈ (ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot).powerset, ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.upperDiamondPathCoefficient lam target pivot U • ∑ L ∈ (AllRankArbitraryRowBranchingOperator.precedingRows pivot).powerset, ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff lam pivot (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target pivot + 1) L • ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual lam target pivot k (L ∪ U)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.pivot_lt_diamondUpperSuffixNext {r : ℕ} (target pivot : Fin (r + 1)) (hpivot : pivot < target) (U : Finset (Fin (r + 1))) (hU : U ⊆ ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot) :

pivot < diamondUpperSuffixNext target U

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.sum_weightedDiamondPairResidual_eq_sum_spectralPrefix_suffix {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (target pivot : Fin (r + 1)) (hpivot : pivot < target) (k : Fin n) :

∑ S ∈ ((AllRankArbitraryRowBranchingOperator.precedingRows target).erase pivot).powerset, AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target (insert pivot S) • ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual lam target pivot k S = -∑ U ∈ (ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows target pivot).powerset, ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.upperDiamondPathCoefficient lam target pivot U • spectralDiamondPrefixResidual lam target pivot (diamondUpperSuffixNext target U) k ∘ₗ AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((U.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target])

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRootTransport.upperPolarizationPathCommutator_append_pivot {r n : ℕ} (pivot target : Fin (r + 1)) (hpt : pivot < target) (front : List (Fin (r + 1))) (hnon : front ≠ []) (hfront : ∀ a ∈ front, a < pivot) :

ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator target pivot (front ++ [pivot]) = AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (front ++ [target])

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRootTransport.polarization_diamondPathOperator_pivot_sub {r n : ℕ} (pivot target : Fin (r + 1)) (hpt : pivot < target) (k : Fin n) (S : Finset (Fin (r + 1))) (hS : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (p : PolynomialSpace r n) :

(polarization r n target pivot) ((ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator pivot k S) p) - (ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator pivot k S) ((polarization r n target pivot) p) = (ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator target k S) p

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRootTransport.upperPolarizationPathCommutator_later_target_eq_zero {r n : ℕ} (pivot rootTarget target : Fin (r + 1)) (hroot : pivot < rootTarget) (htarget : pivot < target) (front : List (Fin (r + 1))) (hfront : ∀ a ∈ front, a < pivot) :

ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator rootTarget pivot (front ++ [target]) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRootTransport.polarization_diamondPathOperator_later_target_sub_eq_zero {r n : ℕ} (pivot rootTarget target : Fin (r + 1)) (hroot : pivot < rootTarget) (htarget : pivot < target) (k : Fin n) (S : Finset (Fin (r + 1))) (hS : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows pivot) (p : PolynomialSpace r n) :

(polarization r n rootTarget pivot) ((ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator target k S) p) - (ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator target k S) ((polarization r n rootTarget pivot) p) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRootTransport.polarization_spectralPathOperator_later_target_sub_eq_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (pivot rootTarget target : Fin (r + 1)) (hroot : pivot < rootTarget) (htarget : pivot < target) (k : Fin n) (t : ℝ) (p : PolynomialSpace r n) :

(polarization r n rootTarget pivot) ((ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k t) p) - (ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k t) ((polarization r n rootTarget pivot) p) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRootTransport.polarization_comp_spectralPathOperator_later_target_commute {r n : ℕ} (lam : Fin (r + 1) → ℕ) (pivot rootTarget target : Fin (r + 1)) (hroot : pivot < rootTarget) (htarget : pivot < target) (k : Fin n) (t : ℝ) :

polarization r n rootTarget pivot ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k t = ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k t ∘ₗ polarization r n rootTarget pivot

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRootTransport.polarization_spectralPathOperator_self_sub {r n : ℕ} (lam : Fin (r + 1) → ℕ) (pivot target : Fin (r + 1)) (hpt : pivot < target) (k : Fin n) (t : ℝ) (p : PolynomialSpace r n) :

(polarization r n target pivot) ((ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot pivot k t) p) - (ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot pivot k t) ((polarization r n target pivot) p) = (ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k t) p

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRootTransport.polarization_comp_spectralPathOperator_self_sub {r n : ℕ} (lam : Fin (r + 1) → ℕ) (pivot target : Fin (r + 1)) (hpt : pivot < target) (k : Fin n) (t : ℝ) :

polarization r n target pivot ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot pivot k t - ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot pivot k t ∘ₗ polarization r n target pivot = ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k t

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRootTransport.polarization_comp_arbitraryRowAxialRaise_sub {r n : ℕ} (lam : Fin (r + 1) → ℕ) (pivot target : Fin (r + 1)) (hpt : pivot < target) (k : Fin n) :

polarization r n target pivot ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ polarization r n target pivot = ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondUniversalPluckerCancellation.spectralBooleanPrefixResidual_eq_zero_of_rtt {r n : ℕ} (A B C D E : PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n) (h : ℝ) (hcomm : A ∘ₗ B = B ∘ₗ A) (hroot : E ∘ₗ B - B ∘ₗ E = D) (hrtt : (h + 1) • (C ∘ₗ B - B ∘ₗ C) = A ∘ₗ D - B ∘ₗ C) :

(A ∘ₗ E) ∘ₗ B - B ∘ₗ A ∘ₗ E - h • (C ∘ₗ B - B ∘ₗ C) - C ∘ₗ B = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondUniversalPluckerCancellation.spectralPathPrefixResidual_eq_zero_of_rtt {r n : ℕ} (lam : Fin (r + 1) → ℕ) (pivot next : Fin (r + 1)) (hpivot : pivot < next) (k : Fin n) (h : ℝ) (hcomm : ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot pivot k (h + 1) ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k = AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot pivot k (h + 1)) (hrtt : (h + 1) • (ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot next k (h + 1) ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot next k (h + 1)) = ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot pivot k (h + 1) ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot next k 0 - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot next k (h + 1)) :

(ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot pivot k (h + 1) ∘ₗ polarization r n next pivot) ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot pivot k (h + 1) ∘ₗ polarization r n next pivot - h • (ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot next k (h + 1) ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot next k (h + 1)) - ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot next k (h + 1) ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralAbstractRTT.spectralStep_rtt {r n : ℕ} (A B C D E F S T : PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n) (x y : ℝ) (hAB : A * B = B * A) (hSB : S * B - B * S = D) (hTA : T * A - A * T = E) (hTB : T * B - B * T = F) (hSF : S * F = F * S) (hTC : T * C = C * T) (hTD : T * D = D * T) (hST : S * T = T * S) (hcross : (x - y) • (C * F - F * C) = E * D - F * C) (hCB : (x - y) • (C * B - B * C) = A * D - B * C) (hAF : (x - y) • (A * F - F * A) = E * B - F * A) (hEB : (x - y) • (E * B - B * E) = A * F - B * E) :

(x - y) • ((x • C - A * S) * (y • F - B * T) - (y • F - B * T) * (x • C - A * S)) = (x • E - A * T) * (y • D - B * S) - (y • F - B * T) * (x • C - A * S)

source

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralAbstractSelfCommute.spectralStep_same_target_commute {r n : ℕ} (A B C D R : PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n) (x y : ℝ) (hAB : A * B = B * A) (hCD : C * D = D * C) (hRA : R * A - A * R = C) (hRB : R * B - B * R = D) (hRC : R * C = C * R) (hRD : R * D = D * R) (hcross : (x - y) • (C * B - B * C) = A * D - B * C) :

(x • C - A * R) * (y • D - B * R) = (y • D - B * R) * (x • C - A * R)

source

ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam a.succ target k u ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam a.succ target k v = ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam a.succ target k v ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam a.succ target k u

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRTT.spectralPathOperator_zero_pivot_rtt {r n : ℕ} (lam : Fin (r + 1) → ℕ) (s t : Fin (r + 1)) (k : Fin n) (u v : ℝ) :

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRTT.spectralPathOperator_zero_pivot_same_target_commute {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target : Fin (r + 1)) (k : Fin n) (u v : ℝ) :

ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam 0 target k u ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam 0 target k v = ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam 0 target k v ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam 0 target k u

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRTT.spectralPathOperator_rtt_and_same_target_commute {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (pivot : Fin (r + 1)) :

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRTT.spectralPathOperator_rtt {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (pivot s t : Fin (r + 1)) (hs : pivot ≤ s) (ht : pivot ≤ t) (k : Fin n) (u v : ℝ) :

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralRTT.spectralPathOperator_same_target_commute {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (pivot target : Fin (r + 1)) (htarget : pivot ≤ target) (k : Fin n) (u v : ℝ) :

ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k u ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k v = ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k v ∘ₗ ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator lam pivot target k u

source

ArbitraryRowSameAxisDiamondSuffixSummation.spectralDiamondPrefixResidual lam target pivot next k = 0

source

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralSuffixClosure.sum_weightedDiamondPairResidual_eq_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (target pivot : Fin (r + 1)) (hpivot : pivot < target) (k : Fin n) :

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralSuffixClosure.arbitraryRowAxialRaise_sameAxis_commutator {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (pivot target : Fin (r + 1)) (hpivot : pivot < target) (k : Fin n) :

AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam target k ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam target k = ArbitraryRowSameAxisDiamondPathCommutator.diamondOmittedRowOperator lam target pivot k ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralSuffixClosure.arbitraryRowAxialRaise_sameAxis_diamond {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (i j : Fin (r + 1)) (hij : i < j) (k : Fin n) (p : PolynomialSpace r n) :

(AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise (HigherChannel.raiseWeight lam i) j k) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam i k) p) = (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise (HigherChannel.raiseWeight lam j) i k) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam j k) p)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxActualForward.boxAxis_succ_val_eq_basisFun (n : ℕ) :

↑(HigherYoungAllRankActualBoxInstantiation.boxAxis (n + 1) ⋯) = (EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxActualForward.dominantSameAxisDiamond_allRows (r n : ℕ) :

ArbitraryRankInterlacingAdjacentPathExchange.DominantSameAxisDiamond r n

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxActualForward.projectedCoordinateRaise_canonicalGelfandTsetlinFibre_eq_of_adjacentSignature {r n : ℕ} (low high : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hrow : high = HigherChannel.raiseWeight low row) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces high mu) (hdom : Antitone low) (hlowGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (hhighGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram high mu hhigh) (hexchange : ∀ (p : ↥(HarmonicYoungSpace mu)), (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise low row (Fin.last n)) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed low mu) p) - (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed high mu) p ∈ youngGramRadialIdeal (r + 1) (n + 1)) (p : ↥(HarmonicYoungSpace mu)) :

(projectedCoordinateRaise high low ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hlowGram) p) = AllRankGelfandTsetlinAdjacentFibrePhase.adjacentNormalizedAxisCoefficient (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram low mu hlow hlowGram) (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram high mu hhigh hhighGram) (ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row)⁻¹ • (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre high mu hhigh hhighGram) p

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxActualForward.canonicalAdjacentProjectedRaiseCoefficient_sq_of_adjacentSignature {r n : ℕ} (low high : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hrow : high = HigherChannel.raiseWeight low row) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces high mu) (hlowGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (hhighGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram high mu hhigh) (hgram : AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram high mu hhigh hhighGram = ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row ^ 2 * ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar high row * AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram low mu hlow hlowGram * HigherChannel.plusProbability (n + 1) low mu row) :

AllRankGelfandTsetlinAdjacentFibrePhase.adjacentNormalizedAxisCoefficient (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram low mu hlow hlowGram) (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram high mu hhigh hhighGram) (ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row)⁻¹ ^ 2 = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar high row * HigherChannel.plusProbability (n + 1) low mu row

source

structure MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxActualForward.CanonicalBoxForwardPolynomialData {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) i) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) :

Prop

Data encoding the canonical box forward polynomial construction.

path_exchange (p : ↥(HarmonicYoungSpace (HigherHierarchy.Weyl.flooredWeight b (n + 1)))) : (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row (Fin.last n)) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) (HigherHierarchy.Weyl.flooredWeight b (n + 1))) p) - (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed (HigherYoungActualGraphAssembly.boxSignature a (n + 1) high) (HigherHierarchy.Weyl.flooredWeight b (n + 1))) p ∈ youngGramRadialIdeal (r + 1) (n + 1)
fischer_recurrence : AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) high) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯ ⋯ = ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row ^ 2 * ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherYoungActualGraphAssembly.boxSignature a (n + 1) high) row * AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯ ⋯ * HigherChannel.plusProbability (n + 1) (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) row

Instances For

source

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxActualForward.CanonicalBoxAdjacentFischerRecurrence {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) i) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) :

Prop

The canonical box adjacent fischer recurrence used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxActualForward.canonicalBoxGenuineForwardAxisData {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) i) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) (D : CanonicalBoxForwardPolynomialData a b hstable hgram low high row hrow) :

HigherYoungArbitraryRowLoweringProjectedAxisWitness.GenuineLoweringFibreAxisData a b (HigherYoungAllRankActualBoxInstantiation.boxAxis (n + 1) ⋯) (AllRankGelfandTsetlinCanonicalFibre.canonicalBoxGelfandTsetlinFibre a b hstable hgram) low high row ⋯

The canonical box genuine forward axis data used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxActualForward.canonicalBoxForwardPolynomialData_pathExchange_of_diamond {r m n : ℕ} (hdiamond : ArbitraryRankInterlacingAdjacentPathExchange.DominantSameAxisDiamond (r + 1) (n + 1)) (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) (p : ↥(HarmonicYoungSpace (HigherHierarchy.Weyl.flooredWeight b (n + 1)))) :

(AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row (Fin.last n)) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) (HigherHierarchy.Weyl.flooredWeight b (n + 1))) p) - (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed (HigherYoungActualGraphAssembly.boxSignature a (n + 1) high) (HigherHierarchy.Weyl.flooredWeight b (n + 1))) p ∈ youngGramRadialIdeal (r + 1) (n + 1)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxActualForward.canonicalBoxForwardPolynomialData_pathExchange_allRows {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) (p : ↥(HarmonicYoungSpace (HigherHierarchy.Weyl.flooredWeight b (n + 1)))) :

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxActualForward.canonicalBoxForwardPolynomialData_of_recurrence {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) i) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) (hrecurrence : CanonicalBoxAdjacentFischerRecurrence a b hstable hgram low high row) :

CanonicalBoxForwardPolynomialData a b hstable hgram low high row hrow

source

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (m : ℕ) :

Type

The source matrix used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m = MvPolynomial (Fin m × Fin m) ℂ

Instances For

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot {m : ℕ} (i j : Fin m) :

Derivation ℂ (SourceMatrix m) (SourceMatrix m)

The source row root used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j = ∑ k : Fin m, MvPolynomial.X (i, k) • MvPolynomial.pderiv (j, k)

Instances For

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot {m : ℕ} (i j : Fin m) :

Derivation ℂ (SourceMatrix m) (SourceMatrix m)

The source column root used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j = ∑ k : Fin m, MvPolynomial.X (k, i) • MvPolynomial.pderiv (k, j)

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot_apply {m : ℕ} (i j : Fin m) (p : SourceMatrix m) :

(sourceRowRoot i j) p = ∑ k : Fin m, MvPolynomial.X (i, k) * (MvPolynomial.pderiv (j, k)) p

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot_apply {m : ℕ} (i j : Fin m) (p : SourceMatrix m) :

(sourceColumnRoot i j) p = ∑ k : Fin m, MvPolynomial.X (k, i) * (MvPolynomial.pderiv (k, j)) p

source

def MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i : Fin m) :

ℕ

The source row degree used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree d i = ∑ j : Fin m, d (i, j)

Instances For

source

def MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (j : Fin m) :

ℕ

The source column degree used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree d j = ∑ i : Fin m, d (i, j)

Instances For

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.coeff_sourceRowRoot_self {m : ℕ} (p : SourceMatrix m) (i : Fin m) (d : Fin m × Fin m →₀ ℕ) :

((sourceRowRoot i i) p).coeff d = sourceRowDegree d i • p.coeff d

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.coeff_sourceColumnRoot_self {m : ℕ} (p : SourceMatrix m) (i : Fin m) (d : Fin m × Fin m →₀ ℕ) :

((sourceColumnRoot i i) p).coeff d = sourceColumnDegree d i • p.coeff d

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree_eq_of_coeff_ne_zero {m : ℕ} (p : SourceMatrix m) (lam : Fin m → ℕ) (hp : ∀ (i : Fin m), (sourceRowRoot i i) p = ↑(lam i) • p) (d : Fin m × Fin m →₀ ℕ) (hd : p.coeff d ≠ 0) (i : Fin m) :

sourceRowDegree d i = lam i

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree_eq_of_coeff_ne_zero {m : ℕ} (p : SourceMatrix m) (lam : Fin m → ℕ) (hp : ∀ (i : Fin m), (sourceColumnRoot i i) p = ↑(lam i) • p) (d : Fin m × Fin m →₀ ℕ) (hd : p.coeff d ≠ 0) (i : Fin m) :

sourceColumnDegree d i = lam i

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.coeff_X_mul_pderiv_ne {σ : Type u_1} (p : MvPolynomial σ ℂ) (a b : σ) (hab : a ≠ b) (d : σ →₀ ℕ) :

(MvPolynomial.X a * (MvPolynomial.pderiv b) p).coeff d = if d a = 0 then 0 else (d b + 1) • p.coeff (d - Finsupp.single a 1 + Finsupp.single b 1)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot_X {m : ℕ} (i j a b : Fin m) :

(sourceRowRoot i j) (MvPolynomial.X (a, b)) = if j = a then MvPolynomial.X (i, b) else 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot_X {m : ℕ} (i j a b : Fin m) :

(sourceColumnRoot i j) (MvPolynomial.X (a, b)) = if j = b then MvPolynomial.X (a, i) else 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot_sourceLeadingMinor_self {r : ℕ} (i k : Fin (r + 1)) :

(sourceRowRoot i i) (DeterminantVectors.sourceLeadingMinor k) = if i ≤ k then DeterminantVectors.sourceLeadingMinor k else 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot_sourceLeadingMinor_self {r : ℕ} (i k : Fin (r + 1)) :

(sourceColumnRoot i i) (DeterminantVectors.sourceLeadingMinor k) = if i ≤ k then DeterminantVectors.sourceLeadingMinor k else 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot_sourceLeadingMinor_upper {r : ℕ} (i j : Fin (r + 1)) (hij : i < j) (k : Fin (r + 1)) :

(sourceRowRoot i j) (DeterminantVectors.sourceLeadingMinor k) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot_sourceHighestWeightPolynomial_self {r : ℕ} (e : Fin (r + 1) → ℕ) (i : Fin (r + 1)) :

(sourceRowRoot i i) (DeterminantVectors.sourceHighestWeightPolynomial e) = ↑(DeterminantVectors.determinantWeight e i) • DeterminantVectors.sourceHighestWeightPolynomial e

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot_sourceHighestWeightPolynomial_self {r : ℕ} (e : Fin (r + 1) → ℕ) (i : Fin (r + 1)) :

(sourceColumnRoot i i) (DeterminantVectors.sourceHighestWeightPolynomial e) = ↑(DeterminantVectors.determinantWeight e i) • DeterminantVectors.sourceHighestWeightPolynomial e

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot_sourceHighestWeightPolynomial_upper {r : ℕ} (e : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (hij : i < j) :

(sourceRowRoot i j) (DeterminantVectors.sourceHighestWeightPolynomial e) = 0

source

def MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceDiagonalEvaluation {m : ℕ} :

Fin m × Fin m → ℂ

The identity-matrix assignment to the source polynomial variables.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceDiagonalEvaluation z = if z.1 = z.2 then 1 else 0

Instances For

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.eval_sourceLeadingMinor {r : ℕ} (k : Fin (r + 1)) :

(MvPolynomial.eval sourceDiagonalEvaluation) (DeterminantVectors.sourceLeadingMinor k) = 1

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.eval_sourceHighestWeightPolynomial {r : ℕ} (e : Fin (r + 1) → ℕ) :

(MvPolynomial.eval sourceDiagonalEvaluation) (DeterminantVectors.sourceHighestWeightPolynomial e) = 1

source

noncomputable def MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialComplexification {r n : ℕ} :

HigherHarmonicYoung.PolynomialSpace r n →ₗ[ℝ ] MvPolynomial (Fin ((r + 1) * n)) ℂ

The polynomial complexification used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialComplexification = { toFun := ⇑(MvPolynomial.map Complex.ofRealHom), map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialComplexification_apply {r n : ℕ} (p : HigherHarmonicYoung.PolynomialSpace r n) :

polynomialComplexification p = (MvPolynomial.map Complex.ofRealHom) p

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialRealPart_complexification {r n : ℕ} (p : HigherHarmonicYoung.PolynomialSpace r n) :

HigherHarmonicYoung.polynomialRealPart (polynomialComplexification p) = p

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialImaginaryPart_complexification {r n : ℕ} (p : HigherHarmonicYoung.PolynomialSpace r n) :

HigherHarmonicYoung.polynomialImaginaryPart (polynomialComplexification p) = 0

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialRealPart_complex_smul {r n : ℕ} (c : ℂ) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

HigherHarmonicYoung.polynomialRealPart (c • p) = c.re • HigherHarmonicYoung.polynomialRealPart p - c.im • HigherHarmonicYoung.polynomialImaginaryPart p

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialImaginaryPart_complex_smul {r n : ℕ} (c : ℂ) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

HigherHarmonicYoung.polynomialImaginaryPart (c • p) = c.re • HigherHarmonicYoung.polynomialImaginaryPart p + c.im • HigherHarmonicYoung.polynomialRealPart p

source

noncomputable def MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialComplexSpan {r n : ℕ} (W : Submodule ℝ (HigherHarmonicYoung.PolynomialSpace r n)) :

Submodule ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The polynomial complex span used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialComplexSpan W = Submodule.span ℂ (⇑MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialComplexification '' ↑W)

Instances For

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.realPart_imaginaryPart_mem_of_mem_polynomialComplexSpan {r n : ℕ} (W : Submodule ℝ (HigherHarmonicYoung.PolynomialSpace r n)) (z : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hz : z ∈ polynomialComplexSpan W) :

HigherHarmonicYoung.polynomialRealPart z ∈ W ∧ HigherHarmonicYoung.polynomialImaginaryPart z ∈ W

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialComplexSpan_inf_eq_bot_of_inf_eq_bot {r n : ℕ} (W U : Submodule ℝ (HigherHarmonicYoung.PolynomialSpace r n)) (hdisjoint : W ⊓ U = ⊥) :

polynomialComplexSpan W ⊓ polynomialComplexSpan U = ⊥

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.polynomialComplexSpan_ne_bot_of_ne_bot {r n : ℕ} (W : Submodule ℝ (HigherHarmonicYoung.PolynomialSpace r n)) (hW : W ≠ ⊥) :

polynomialComplexSpan W ≠ ⊥

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.complexSpan_invariant {V : Type u_1} {Z : Type u_2} {I : Type u_3} [AddCommGroup V] [Module ℝ V] [AddCommGroup Z] [Module ℂ Z] [Module ℝ Z] (e : V →ₗ[ℝ ] Z) (R : I → V →ₗ[ℝ ] V) (RC : I → Z →ₗ[ℂ ] Z) (hcomm : ∀ (i : I) (v : V), (RC i) (e v) = e ((R i) v)) (W : Submodule ℝ V) (hW : ∀ (i : I), ∀ v ∈ W, (R i) v ∈ W) (i : I) (z : Z) (hz : z ∈ Submodule.span ℂ (⇑e '' ↑W)) :

(RC i) z ∈ Submodule.span ℂ (⇑e '' ↑W)

source

noncomputable def MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.complexAmbientCoordinateDerivation {r n : ℕ} (a b : Fin n) :

Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The complex ambient coordinate derivation used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.complexAmbientCoordinateDerivation_apply {r n : ℕ} (a b : Fin n) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(complexAmbientCoordinateDerivation a b) p = ∑ i : Fin (r + 1), MvPolynomial.X (HigherHarmonicYoung.variableIndex i a) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i b)) p

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.complexAmbientCoordinateDerivation_complexification {r n : ℕ} (a b : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r n) :

(complexAmbientCoordinateDerivation a b) (polynomialComplexification p) = polynomialComplexification ((HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation a b) p)

source

noncomputable def MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.complexAmbientRotation {r n : ℕ} (a b : Fin n) :

Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The complex ambient rotation used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.complexAmbientRotation_complexification {r n : ℕ} (a b : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r n) :

(complexAmbientRotation a b) (polynomialComplexification p) = polynomialComplexification ((HigherHarmonicYoung.MixedSignature.ambientRotation a b) p)

source

noncomputable def MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.youngRealPolynomialImage {r n : ℕ} (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

Submodule ℝ (HigherHarmonicYoung.PolynomialSpace r n)

The young real polynomial image used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.youngRealPolynomialImage lam W = Submodule.map (MetricCodes.Spherical.HigherHarmonicYoung.harmonicYoungSubmodule lam).subtype W

Instances For

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.youngRealPolynomialImage_le {r n : ℕ} (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

youngRealPolynomialImage lam W ≤ HigherHarmonicYoung.harmonicYoungSubmodule lam

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.youngRealPolynomialImage_ne_bot_of_ne_bot {r n : ℕ} (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : W ≠ ⊥) :

youngRealPolynomialImage lam W ≠ ⊥

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.youngRealPolynomialImage_inf_orthogonal_eq_bot {r n : ℕ} (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

youngRealPolynomialImage lam W ⊓ youngRealPolynomialImage lam Wᗮ = ⊥

source

noncomputable def MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

Submodule ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The young complex polynomial span used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) :

Submodule ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The full young complex polynomial span used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan_le_full {r n : ℕ} (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

youngComplexPolynomialSpan lam W ≤ fullYoungComplexPolynomialSpan lam

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan_ne_bot_of_ne_bot {r n : ℕ} (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : W ≠ ⊥) :

youngComplexPolynomialSpan lam W ≠ ⊥

source

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan_inf_orthogonal_eq_bot {r n : ℕ} (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

youngComplexPolynomialSpan lam W ⊓ youngComplexPolynomialSpan lam Wᗮ = ⊥

source

def MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.rootOperatorWord {K : Type u_1} {V : Type u_2} {I : Type u_3} [Semiring K] [AddCommMonoid V] [Module K V] (E : I → V →ₗ[K] V) :

List I → V →ₗ[K] V

The root operator word used in the spherical-code argument.

Equations

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.rootOperatorWord_nil {K : Type u_1} {V : Type u_2} {I : Type u_3} [Semiring K] [AddCommMonoid V] [Module K V] (E : I → V →ₗ[K] V) :

rootOperatorWord E [] = LinearMap.id

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungTwoRowLieIrreducibility.rootOperatorWord_cons_apply {K : Type u_1} {V : Type u_2} {I : Type u_3} [Semiring K] [AddCommMonoid V] [Module K V] (E : I → V →ₗ[K] V) (i : I) (w : List I) (v : V) :

(rootOperatorWord E (i :: w)) v = (rootOperatorWord E w) ((E i) v)

source

theorem MetricCodes.Spherical.HigherYoungCyclicHighestSchur.commute_rootOperatorWord {K : Type u_1} {V : Type u_2} {I : Type u_3} [Semiring K] [AddCommMonoid V] [Module K V] (R : I → V →ₗ[K] V) (A : V →ₗ[K] V) (hcomm : ∀ (i : I), A ∘ₗ R i = R i ∘ₗ A) (w : List I) :

A ∘ₗ HigherYoungTwoRowLieIrreducibility.rootOperatorWord R w = HigherYoungTwoRowLieIrreducibility.rootOperatorWord R w ∘ₗ A

source

def MetricCodes.Spherical.HigherYoungCyclicHighestSchur.operatorWordSpan {K : Type u_1} {V : Type u_2} {I : Type u_3} [Semiring K] [AddCommMonoid V] [Module K V] (R : I → V →ₗ[K] V) (v : V) :

Submodule K V

The operator word span used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def MetricCodes.Spherical.HigherYoungCyclicHighestSchur.operatorWordPairSpan {K : Type u_1} {V : Type u_2} {I : Type u_3} [Semiring K] [AddCommMonoid V] [Module K V] (R : I → V →ₗ[K] V) (v w : V) :

Submodule K V

The sum of the operator-word cyclic submodules generated by two vectors.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherYoungCyclicHighestSchur.eq_smul_id_of_cyclic_eigenpair {K : Type u_1} {V : Type u_2} {I : Type u_3} [CommRing K] [AddCommGroup V] [Module K V] (R : I → V →ₗ[K] V) (A : V →ₗ[K] V) (hcomm : ∀ (i : I), A ∘ₗ R i = R i ∘ₗ A) (v w : V) (c : K) (hv : A v = c • v) (hw : A w = c • w) (hcyclic : operatorWordPairSpan R v w = ⊤) :

A = c • LinearMap.id

source

theorem MetricCodes.Spherical.HigherYoungCyclicHighestSchur.complex_eigenpair_im_eq_zero_of_symmetric {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A : V →ₗ[ℝ ] V) (hA : A.IsSymmetric) (v w : V) (a b : ℝ) (hv : A v = a • v - b • w) (hw : A w = b • v + a • w) (hne : v ≠ 0 ∨ w ≠ 0) :

b = 0

source

theorem MetricCodes.Spherical.HigherYoungCyclicHighestSchur.symmetric_eq_smul_id_of_complex_cyclic_eigenvector {V : Type u_1} {I : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (R : I → V →ₗ[ℝ ] V) (A : V →ₗ[ℝ ] V) (hA : A.IsSymmetric) (hcomm : ∀ (i : I), A ∘ₗ R i = R i ∘ₗ A) (v w : V) (c : ℂ) (hv : A v = c.re • v - c.im • w) (hw : A w = c.im • v + c.re • w) (hne : v ≠ 0 ∨ w ≠ 0) (hcyclic : operatorWordPairSpan R v w = ⊤) :

A = c.re • LinearMap.id

source

noncomputable def MetricCodes.Spherical.HigherYoungCyclicHighestSchur.dominantHighestRealVector {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

↥(HigherHarmonicYoung.HarmonicYoungSpace lam)

The dominant highest real vector used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def MetricCodes.Spherical.HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

↥(HigherHarmonicYoung.HarmonicYoungSpace lam)

The dominant highest imaginary vector used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherYoungCyclicHighestSchur.dominantHighestRealVector_ne_zero_or_imaginary_ne_zero {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

dominantHighestRealVector hn lam hdom ≠ 0 ∨ dominantHighestImaginaryVector hn lam hdom ≠ 0

source

noncomputable def MetricCodes.Spherical.HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)

The dominant highest rotation word span used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherYoungCyclicHighestSchur.youngSymmetricRotationIntertwiner_eq_smul_id_of_dominantCyclicHighest {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hA : A.IsSymmetric) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) (c : ℂ) (hreal : A (dominantHighestRealVector hn lam hdom) = c.re • dominantHighestRealVector hn lam hdom - c.im • dominantHighestImaginaryVector hn lam hdom) (himaginary : A (dominantHighestImaginaryVector hn lam hdom) = c.im • dominantHighestRealVector hn lam hdom + c.re • dominantHighestImaginaryVector hn lam hdom) (hcyclic : dominantHighestRotationWordSpan hn lam hdom = ⊤) :

A = c.re • LinearMap.id

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaisingSchurTraceGram.youngClebschRaise_scalar_eq_lower_dimension_ratio {r n : ℕ} (high low : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), high i = ∑ i : Fin (r + 1), low i + 1) (row : Fin (r + 1)) (raisingGram loweringGram : ℝ) (hraise : LinearMap.adjoint (youngClebschRaise high low hdeg row) ∘ₗ youngClebschRaise high low hdeg row = raisingGram • LinearMap.id) (hlower : LinearMap.adjoint (youngClebschLower low high hdeg row) ∘ₗ youngClebschLower low high hdeg row = loweringGram • LinearMap.id) (hlow : 0 < Module.finrank ℝ ↥(HarmonicYoungSpace low)) :

raisingGram = loweringGram * ↑(Module.finrank ℝ ↥(HarmonicYoungSpace high)) / ↑(Module.finrank ℝ ↥(HarmonicYoungSpace low))

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaisingSchurTraceGram.youngClebschRaise_gram_rotation_intertwine {r n : ℕ} (high low : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), high i = ∑ i : Fin (r + 1), low i + 1) (row : Fin (r + 1)) (a b : Fin n) :

(LinearMap.adjoint (youngClebschRaise high low hdeg row) ∘ₗ youngClebschRaise high low hdeg row) ∘ₗ MixedSignature.youngAmbientRotation low a b = MixedSignature.youngAmbientRotation low a b ∘ₗ LinearMap.adjoint (youngClebschRaise high low hdeg row) ∘ₗ youngClebschRaise high low hdeg row

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaisingSchurTraceGram.youngClebschRaise_gram_scalar_of_dominantCyclicHighest {r n : ℕ} (high low : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), high i = ∑ i : Fin (r + 1), low i + 1) (row : Fin (r + 1)) (hn : 2 * (r + 1) ≤ n) (hdom : Antitone low) (c : ℂ) (hreal : (LinearMap.adjoint (youngClebschRaise high low hdeg row) ∘ₗ youngClebschRaise high low hdeg row) (HigherYoungCyclicHighestSchur.dominantHighestRealVector hn low hdom) = c.re • HigherYoungCyclicHighestSchur.dominantHighestRealVector hn low hdom - c.im • HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn low hdom) (himaginary : (LinearMap.adjoint (youngClebschRaise high low hdeg row) ∘ₗ youngClebschRaise high low hdeg row) (HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn low hdom) = c.im • HigherYoungCyclicHighestSchur.dominantHighestRealVector hn low hdom + c.re • HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn low hdom) (hcyclic : HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan hn low hdom = ⊤) :

LinearMap.adjoint (youngClebschRaise high low hdeg row) ∘ₗ youngClebschRaise high low hdeg row = c.re • LinearMap.id

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaisingSchurTraceGram.arbitraryRowRaisingGramScalar {r n : ℕ} (high : Fin (r + 1) → ℕ) (row : Fin (r + 1)) :

ℝ

The arbitrary row raising gram scalar used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

inner ℝ ((youngClebschRaise high (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) ⋯ row) p) ((youngClebschRaise high (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) ⋯ row) q) = arbitraryRowRaisingGramScalar high row * inner ℝ p q

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.rowDerivation_nullSubstitution_sourceRowRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) (q : BideterminantHighestLine.SourceMatrix (r + 1)) :

(DeterminantVectors.rowDerivation i j) ((nullSubstitution h) q) = (nullSubstitution h) ((BideterminantHighestLine.sourceRowRoot i j) q)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientPositiveRoot_nullSubstitution_sourceColumnRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) (q : BideterminantHighestLine.SourceMatrix (r + 1)) :

(DeterminantVectors.ambientPositiveRoot h i j) ((nullSubstitution h) q) = 2 • (nullSubstitution h) ((BideterminantHighestLine.sourceColumnRoot i j) q)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientCartan_nullSubstitution_sourceColumnRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i : Fin (r + 1)) (q : BideterminantHighestLine.SourceMatrix (r + 1)) :

(DeterminantVectors.ambientCartan h i) ((nullSubstitution h) q) = 2 • (nullSubstitution h) ((BideterminantHighestLine.sourceColumnRoot i i) q)

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.sourceMatrixHighestSubmodule {r : ℕ} (lam : Fin (r + 1) → ℕ) :

Submodule ℂ (BideterminantHighestLine.SourceMatrix (r + 1))

The source matrix highest submodule used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.mem_sourceMatrixHighestSubmodule {r : ℕ} (lam : Fin (r + 1) → ℕ) (q : BideterminantHighestLine.SourceMatrix (r + 1)) :

q ∈ sourceMatrixHighestSubmodule lam ↔ (∀ (i : Fin (r + 1)), (BideterminantHighestLine.sourceRowRoot i i) q = ↑(lam i) • q) ∧ (∀ (i : Fin (r + 1)), (BideterminantHighestLine.sourceColumnRoot i i) q = ↑(lam i) • q) ∧ ∀ (i j : Fin (r + 1)), i < j → (BideterminantHighestLine.sourceRowRoot i j) q = 0

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) :

Submodule ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The ambient isotropic highest submodule used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.mem_ambientIsotropicHighestSubmodule {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

f ∈ ambientIsotropicHighestSubmodule h lam ↔ (∃ (q : BideterminantHighestLine.SourceMatrix (r + 1)), (nullSubstitution h) q = f) ∧ (∀ (i : Fin (r + 1)), (DeterminantVectors.rowDerivation i i) f = ↑(lam i) • f) ∧ (∀ (i : Fin (r + 1)), (DeterminantVectors.ambientCartan h i) f = ↑(2 * lam i) • f) ∧ ∀ (i j : Fin (r + 1)), i < j → (DeterminantVectors.rowDerivation i j) f = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.sourceRowRoot_eigen_of_ambient {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i : Fin (r + 1)) (q : BideterminantHighestLine.SourceMatrix (r + 1)) (c : ℂ) (heigen : (DeterminantVectors.rowDerivation i i) ((nullSubstitution h) q) = c • (nullSubstitution h) q) :

(BideterminantHighestLine.sourceRowRoot i i) q = c • q

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.sourceColumnRoot_eigen_of_ambient {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i : Fin (r + 1)) (q : BideterminantHighestLine.SourceMatrix (r + 1)) (k : ℕ) (heigen : (DeterminantVectors.ambientCartan h i) ((nullSubstitution h) q) = ↑(2 * k) • (nullSubstitution h) q) :

(BideterminantHighestLine.sourceColumnRoot i i) q = ↑k • q

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule_eq_map_source {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) :

ambientIsotropicHighestSubmodule h lam = Submodule.map (nullSubstitution h).toLinearMap (sourceMatrixHighestSubmodule lam)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.finrank_ambientIsotropicHighestSubmodule_eq_source {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) :

Module.finrank ℂ ↥(ambientIsotropicHighestSubmodule h lam) = Module.finrank ℂ ↥(sourceMatrixHighestSubmodule lam)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.sourceHighestWeightPolynomial_mem_sourceMatrixHighestSubmodule {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

DeterminantVectors.sourceHighestWeightPolynomial (DeterminantVectors.signatureExponent lam) ∈ sourceMatrixHighestSubmodule lam

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.sourceHighestWeightPolynomial_ne_zero {r : ℕ} (lam : Fin (r + 1) → ℕ) :

DeterminantVectors.sourceHighestWeightPolynomial (DeterminantVectors.signatureExponent lam) ≠ 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule_eq_span_iff_source_finrank {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

ambientIsotropicHighestSubmodule h lam = ℂ ∙ DeterminantVectors.highestWeightPolynomial h (DeterminantVectors.signatureExponent lam) ↔ Module.finrank ℂ ↥(sourceMatrixHighestSubmodule lam) = 1

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceHighestKernel.sourceColumnRoot_sourceLeadingMinor_upper {r : ℕ} (i j : Fin (r + 1)) (hij : i < j) (k : Fin (r + 1)) :

(HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) (HigherHarmonicYoung.DeterminantVectors.sourceLeadingMinor k) = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceHighestKernel.sourceColumnRoot_sourceHighestWeightPolynomial_upper {r : ℕ} (e : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (hij : i < j) :

(HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) (HigherHarmonicYoung.DeterminantVectors.sourceHighestWeightPolynomial e) = 0

source

noncomputable def MetricCodes.Spherical.HigherYoungAllRankSourceHighestKernel.sourceHighestKernel {r : ℕ} (lam : Fin (r + 1) → ℕ) :

Submodule ℂ (HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1))

The simultaneous source row and column highest-weight equations for the weight lam.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceHighestKernel.mem_sourceHighestKernel {r : ℕ} (lam : Fin (r + 1) → ℕ) (q : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)) :

q ∈ sourceHighestKernel lam ↔ (∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i i) q = ↑(lam i) • q) ∧ (∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i i) q = ↑(lam i) • q) ∧ (∀ (i j : Fin (r + 1)), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) q = 0) ∧ ∀ (i j : Fin (r + 1)), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) q = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceHighestKernel.sourceHighestWeightPolynomial_mem_sourceHighestKernel {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

HigherHarmonicYoung.DeterminantVectors.sourceHighestWeightPolynomial (HigherHarmonicYoung.DeterminantVectors.signatureExponent lam) ∈ sourceHighestKernel lam

source

noncomputable def MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent {m : ℕ} (lam : Fin m → ℕ) :

Fin m × Fin m →₀ ℕ

The exponent vector supported on diagonal entries, with diagonal multiplicities prescribed by lam.

Equations

MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent lam = ∑ i : Fin m, Finsupp.single (i, i) (lam i)

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent_apply {m : ℕ} (lam : Fin m → ℕ) (i j : Fin m) :

(sourceDiagonalExponent lam) (i, j) = if i = j then lam i else 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.rowWeightedEntry_le_columnWeightedEntry {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (hbelow : ∀ (i j : Fin m), j < i → d (i, j) = 0) (i j : Fin m) :

↑i * d (i, j) ≤ ↑j * d (i, j)

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.rowWeightedMass_eq_columnWeightedMass {m : ℕ} (lam : Fin m → ℕ) (d : Fin m × Fin m →₀ ℕ) (hrow : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree d i = lam i) (hcolumn : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree d i = lam i) :

∑ i : Fin m, ∑ j : Fin m, ↑i * d (i, j) = ∑ i : Fin m, ∑ j : Fin m, ↑j * d (i, j)

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.rowWeightedEntry_eq_columnWeightedEntry_of_balance {m : ℕ} (lam : Fin m → ℕ) (d : Fin m × Fin m →₀ ℕ) (hrow : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree d i = lam i) (hcolumn : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree d i = lam i) (hbelow : ∀ (i j : Fin m), j < i → d (i, j) = 0) (i j : Fin m) :

↑i * d (i, j) = ↑j * d (i, j)

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceExponent_above_eq_zero_of_diagonalBalance {m : ℕ} (lam : Fin m → ℕ) (d : Fin m × Fin m →₀ ℕ) (hrow : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree d i = lam i) (hcolumn : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree d i = lam i) (hbelow : ∀ (i j : Fin m), j < i → d (i, j) = 0) (i j : Fin m) (hij : i < j) :

d (i, j) = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceExponent_offDiagonal_eq_zero_of_diagonalBalance {m : ℕ} (lam : Fin m → ℕ) (d : Fin m × Fin m →₀ ℕ) (hrow : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree d i = lam i) (hcolumn : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree d i = lam i) (hbelow : ∀ (i j : Fin m), j < i → d (i, j) = 0) (i j : Fin m) (hij : i ≠ j) :

d (i, j) = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceExponent_diagonal_eq_of_diagonalBalance {m : ℕ} (lam : Fin m → ℕ) (d : Fin m × Fin m →₀ ℕ) (hrow : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree d i = lam i) (hcolumn : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree d i = lam i) (hbelow : ∀ (i j : Fin m), j < i → d (i, j) = 0) (i : Fin m) :

d (i, i) = lam i

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceExponent_eq_diagonal_of_upperTriangular {m : ℕ} (lam : Fin m → ℕ) (d : Fin m × Fin m →₀ ℕ) (hrow : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree d i = lam i) (hcolumn : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree d i = lam i) (hbelow : ∀ (i j : Fin m), j < i → d (i, j) = 0) :

d = sourceDiagonalExponent lam

source

def MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.belowDiagonalWeight {m : ℕ} (z : Fin m × Fin m) :

ℕ

The row-minus-column offset, truncated to zero on and above the diagonal.

Equations

MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.belowDiagonalWeight z = ↑z.1 - ↑z.2

Instances For

source

def MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.belowDiagonalMass {m : ℕ} (d : Fin m × Fin m →₀ ℕ) :

ℕ

The below diagonal mass used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.belowDiagonalMass_add_single {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (z : Fin m × Fin m) (k : ℕ) :

belowDiagonalMass (d + Finsupp.single z k) = belowDiagonalMass d + belowDiagonalWeight z * k

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.belowDiagonalMass_sub_single_add {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (z : Fin m × Fin m) (hz : 0 < d z) :

belowDiagonalMass (d - Finsupp.single z 1) + belowDiagonalWeight z = belowDiagonalMass d

source

noncomputable def MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootTargetExponent {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j : Fin m) :

Fin m × Fin m →₀ ℕ

Move one exponent unit from the lower-triangular entry (j, i) to the diagonal entry (i, i).

Equations

MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootTargetExponent d i j = d - Finsupp.single (j, i) 1 + Finsupp.single (i, i) 1

Instances For

source

noncomputable def MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootSourceExponent {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j k : Fin m) :

Fin m × Fin m →₀ ℕ

The upper-root source exponent obtained by moving one unit between rows of the target exponent.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootSourceExponent_self {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j : Fin m) (hij : i < j) (hpositive : 0 < d (j, i)) :

upperRootSourceExponent d i j i = d

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootTarget_coefficient_eq_zero {m : ℕ} (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m) (i j : Fin m) (hij : i < j) (d : Fin m × Fin m →₀ ℕ) (hhighest : (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) p = 0) :

(∑ k : Fin m, if (upperRootTargetExponent d i j) (i, k) = 0 then 0 else ((upperRootTargetExponent d i j) (j, k) + 1) • p.coeff (upperRootSourceExponent d i j k)) = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.belowDiagonalMass_upperRootTarget_add {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j : Fin m) (hpositive : 0 < d (j, i)) :

belowDiagonalMass (upperRootTargetExponent d i j) + (↑j - ↑i) = belowDiagonalMass d

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.belowDiagonalMass_upperRootSource_lt {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j k : Fin m) (hij : i < j) (hik : i < k) (hpositive : 0 < d (j, i)) (htarget : 0 < (upperRootTargetExponent d i j) (i, k)) :

belowDiagonalMass (upperRootSourceExponent d i j k) < belowDiagonalMass d

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootTargetExponent_diagonal {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j : Fin m) (hij : i < j) :

(upperRootTargetExponent d i j) (i, i) = d (i, i) + 1

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootTargetExponent_below_add_one {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j : Fin m) (hij : i < j) (hpositive : 0 < d (j, i)) :

(upperRootTargetExponent d i j) (j, i) + 1 = d (j, i)

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootTargetExponent_earlierRow_of_ne {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j k : Fin m) (hij : i < j) (hki : k ≠ i) :

(upperRootTargetExponent d i j) (i, k) = d (i, k)

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootTargetExponent_eq_zero_of_earlierColumn {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j k : Fin m) (hij : i < j) (hki : k < i) (hminimal : ∀ (a b : Fin m), b < i → b < a → d (a, b) = 0) :

(upperRootTargetExponent d i j) (i, k) = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.coeff_eq_zero_of_minimalBelowColumn {m : ℕ} (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m) (d : Fin m × Fin m →₀ ℕ) (i j : Fin m) (hij : i < j) (hpositive : 0 < d (j, i)) (hminimal : ∀ (a b : Fin m), b < i → b < a → d (a, b) = 0) (hhighest : (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) p = 0) (hinduction : ∀ (e : Fin m × Fin m →₀ ℕ), belowDiagonalMass e < belowDiagonalMass d → p.coeff e = 0) :

p.coeff d = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.exists_minimalBelowColumn_of_mass_pos {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (hmass : 0 < belowDiagonalMass d) :

∃ (i : Fin m) (j : Fin m), i < j ∧ 0 < d (j, i) ∧ ∀ (a b : Fin m), b < i → b < a → d (a, b) = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.eq_zero_of_upperRoots_of_massZero_coeff {m : ℕ} (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m) (hhighest : ∀ (i j : Fin m), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) p = 0) (hzero : ∀ (d : Fin m × Fin m →₀ ℕ), belowDiagonalMass d = 0 → p.coeff d = 0) :

p = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.belowDiagonal_entry_eq_zero_of_mass_eq_zero {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (hmass : belowDiagonalMass d = 0) (i j : Fin m) (hji : j < i) :

d (i, j) = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.sourceHighest_eq_zero_of_diagonalCoeff_eq_zero {r : ℕ} (lam : Fin (r + 1) → ℕ) (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)) (hrow : ∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) (hcolumn : ∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i i) p = ↑(lam i) • p) (hhighest : ∀ (i j : Fin (r + 1)), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) p = 0) (hdiagonal : p.coeff (HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent lam) = 0) :

p = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.sourceHighest_eq_of_diagonalCoeff_eq {r : ℕ} (lam : Fin (r + 1) → ℕ) (p q : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)) (hrowp : ∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) (hcolumnp : ∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i i) p = ↑(lam i) • p) (hhighestp : ∀ (i j : Fin (r + 1)), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) p = 0) (hrowq : ∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i i) q = ↑(lam i) • q) (hcolumnq : ∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i i) q = ↑(lam i) • q) (hhighestq : ∀ (i j : Fin (r + 1)), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) q = 0) (hdiagonal : p.coeff (HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent lam) = q.coeff (HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent lam)) :

p = q

source

theorem MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.sourceHighestWeightPolynomial_diagonal_coeff_ne_zero {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

(HigherHarmonicYoung.DeterminantVectors.sourceHighestWeightPolynomial (HigherHarmonicYoung.DeterminantVectors.signatureExponent lam)).coeff (HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent lam) ≠ 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankIsotropicHighestMultiplicityOne.sourceMatrixHighestSubmodule_eq_span {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

HigherHarmonicYoung.IsotropicAmbientHighestLine.sourceMatrixHighestSubmodule lam = ℂ ∙ HigherHarmonicYoung.DeterminantVectors.sourceHighestWeightPolynomial (HigherHarmonicYoung.DeterminantVectors.signatureExponent lam)

source

theorem MetricCodes.Spherical.HigherYoungAllRankIsotropicHighestMultiplicityOne.finrank_sourceMatrixHighestSubmodule {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

Module.finrank ℂ ↥(HigherHarmonicYoung.IsotropicAmbientHighestLine.sourceMatrixHighestSubmodule lam) = 1

source

theorem MetricCodes.Spherical.HigherYoungAllRankIsotropicHighestMultiplicityOne.ambientIsotropicHighestSubmodule_eq_determinant_span {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule h lam = ℂ ∙ HigherHarmonicYoung.DeterminantVectors.highestWeightPolynomial h (HigherHarmonicYoung.DeterminantVectors.signatureExponent lam)

source

theorem MetricCodes.Spherical.HigherYoungAllRankIsotropicHighestMultiplicityOne.finrank_ambientIsotropicHighestSubmodule {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

Module.finrank ℂ ↥(HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule h lam) = 1

source

theorem MetricCodes.Spherical.HigherYoungAllRankIsotropicHighestMultiplicityOne.ambientIsotropicHighest_eq_diagonal_smul {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule h lam) :

f = (MvPolynomial.eval HigherHarmonicYoung.DeterminantVectors.diagonalEvaluation) f • HigherHarmonicYoung.DeterminantVectors.highestWeightPolynomial h (HigherHarmonicYoung.DeterminantVectors.signatureExponent lam)

source

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℕ) (hdom : Antitone mu) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) :

MvPolynomial (Fin ((r + 1) * n)) ℂ

The young endomorphism highest polynomial used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.polynomialRealPart_youngEndomorphismHighestPolynomial {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℕ) (hdom : Antitone mu) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) :

HigherHarmonicYoung.polynomialRealPart (youngEndomorphismHighestPolynomial hn mu hdom A) = ↑(A (HigherYoungCyclicHighestSchur.dominantHighestRealVector hn mu hdom))

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.polynomialImaginaryPart_youngEndomorphismHighestPolynomial {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℕ) (hdom : Antitone mu) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) :

HigherHarmonicYoung.polynomialImaginaryPart (youngEndomorphismHighestPolynomial hn mu hdom A) = ↑(A (HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn mu hdom))

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphism_dominantHighest_eigenpair {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℕ) (hdom : Antitone mu) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) (hhighest : youngEndomorphismHighestPolynomial hn mu hdom A ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn mu) :

∃ (c : ℂ), A (HigherYoungCyclicHighestSchur.dominantHighestRealVector hn mu hdom) = c.re • HigherYoungCyclicHighestSchur.dominantHighestRealVector hn mu hdom - c.im • HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn mu hdom ∧ A (HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn mu hdom) = c.im • HigherYoungCyclicHighestSchur.dominantHighestRealVector hn mu hdom + c.re • HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn mu hdom

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaiseLowerTensorTrace.arbitraryRowRaiseTensorGramScalar {r n : ℕ} (high : Fin (r + 1) → ℕ) (row : Fin (r + 1)) :

ℝ

The arbitrary row raise tensor gram scalar used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaiseLowerTensorTrace.arbitraryRowRaiseTensorGramScalar_pos {r n : ℕ} (high : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hn : 2 * (r + 1) ≤ n) (hrow : 0 < high row) (hdomhigh : Antitone high) (hdomlow : Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row)) (hstrict : ∀ (j : Fin (r + 1)), ↑j = ↑row + 1 → high j < high row) :

0 < arbitraryRowRaiseTensorGramScalar high row

source

theorem MetricCodes.Spherical.HigherYoungAmbientCartanIsotropicEigenvalues.pderiv_even_conjugateIsotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p i j : Fin (r + 1)) :

(MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) (HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j) = if a = i ∧ p = j then 1 else 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientCartanIsotropicEigenvalues.pderiv_odd_conjugateIsotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p i j : Fin (r + 1)) :

(MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) (HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j) = if a = i ∧ p = j then -MvPolynomial.C Complex.I else 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientCartanIsotropicEigenvalues.ambientCartan_conjugateIsotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p i j : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) (HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j) = if p = j then -2 • HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j else 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientCartanIsotropicEigenvalues.ambientCartan_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = 0

source

noncomputable def MetricCodes.Spherical.HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan {r n : ℕ} (h : 2 * (r + 1) ≤ n) :

Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The total ambient cartan used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h = ∑ p : Fin (r + 1), MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientCartan h p

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(totalAmbientCartan h) f = ∑ p : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) f

source

theorem MetricCodes.Spherical.HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) :

(totalAmbientCartan h) (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h i j) = 2 • HigherHarmonicYoung.DeterminantVectors.isotropicVariable h i j

source

theorem MetricCodes.Spherical.HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan_conjugateIsotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) :

(totalAmbientCartan h) (HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j) = -2 • HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j

source

theorem MetricCodes.Spherical.HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(totalAmbientCartan h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.complexAmbientRotation_apply {r n : ℕ} (a b : Fin n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a b) f = ∑ i : Fin (r + 1), (MvPolynomial.X (HigherHarmonicYoung.variableIndex i a) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i b)) f - MvPolynomial.X (HigherHarmonicYoung.variableIndex i b) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i a)) f)

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.complexAmbientRotation_youngComplexPolynomialSpan_mem {r n : ℕ} (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) W) (a b : Fin n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W) :

(HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a b) f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.ambientPositiveRoot_eq_complexRotations {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) :

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.ambientPositiveRoot_youngComplexPolynomialSpan_mem {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) W) (p q : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W) :

(HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.ambientSumPositiveRoot_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.ambientSumPositiveRoot_eq_complexRotations {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) :

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.ambientSumPositiveRoot_youngComplexPolynomialSpan_mem {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) W) (p q : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W) :

(HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.ambientShortPositiveRoot_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) (t : Fin n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.ambientShortPositiveRoot_eq_complexRotations {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) (t : Fin n) :

HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t = HigherYoungTwoRowLieIrreducibility.complexAmbientRotation (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p) t + Complex.I • HigherYoungTwoRowLieIrreducibility.complexAmbientRotation (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p) t

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.ambientShortPositiveRoot_youngComplexPolynomialSpan_mem {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) W) (p : Fin (r + 1)) (t : Fin n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W) :

(HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootRotationDecomposition.ambientCartan_youngComplexPolynomialSpan_mem {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) W) (p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W) :

(HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W

source

noncomputable def MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.weightedPolynomialFiltration {σ : Type u_1} (weight : σ → ℕ) (k : ℕ) :

Submodule ℂ (MvPolynomial σ ℂ)

The polynomial submodule supported on monomials of weighted degree at most k.

Equations

MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.weightedPolynomialFiltration weight k = MvPolynomial.restrictSupport ℂ {d : σ →₀ ℕ | (Finsupp.weight weight) d ≤ k}

Instances For

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.mem_weightedPolynomialFiltration {σ : Type u_1} (weight : σ → ℕ) (k : ℕ) (p : MvPolynomial σ ℂ) :

p ∈ weightedPolynomialFiltration weight k ↔ ∀ (d : σ →₀ ℕ), p.coeff d ≠ 0 → (Finsupp.weight weight) d ≤ k

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.monomial_mem_weightedPolynomialFiltration {σ : Type u_1} (weight : σ → ℕ) (d : σ →₀ ℕ) (c : ℂ) :

(MvPolynomial.monomial d) c ∈ weightedPolynomialFiltration weight ((Finsupp.weight weight) d)

source

noncomputable def MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.strictWeightedPolynomialFiltration {σ : Type u_1} (weight : σ → ℕ) (k : ℕ) :

Submodule ℂ (MvPolynomial σ ℂ)

The polynomial submodule supported on monomials of weighted degree strictly below k.

Equations

MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.strictWeightedPolynomialFiltration weight k = MvPolynomial.restrictSupport ℂ {d : σ →₀ ℕ | (Finsupp.weight weight) d + 1 ≤ k}

Instances For

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.mem_strictWeightedPolynomialFiltration {σ : Type u_1} (weight : σ → ℕ) (k : ℕ) (p : MvPolynomial σ ℂ) :

p ∈ strictWeightedPolynomialFiltration weight k ↔ ∀ (d : σ →₀ ℕ), p.coeff d ≠ 0 → (Finsupp.weight weight) d + 1 ≤ k

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.strictWeightedPolynomialFiltration_mono {σ : Type u_1} (weight : σ → ℕ) {k l : ℕ} (h : k ≤ l) :

strictWeightedPolynomialFiltration weight k ≤ strictWeightedPolynomialFiltration weight l

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.mul_mem_strictWeightedPolynomialFiltration {σ : Type u_1} (weight : σ → ℕ) {k l : ℕ} {p q : MvPolynomial σ ℂ} (hp : p ∈ weightedPolynomialFiltration weight k) (hq : q ∈ strictWeightedPolynomialFiltration weight l) :

p * q ∈ strictWeightedPolynomialFiltration weight (k + l)

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.derivation_mem_strictWeightedPolynomialFiltration {σ : Type u_1} (weight : σ → ℕ) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (hD : ∀ (i : σ) (e : σ →₀ ℕ), (D (MvPolynomial.X i)).coeff e ≠ 0 → (Finsupp.weight weight) e + 1 ≤ weight i) {k : ℕ} {p : MvPolynomial σ ℂ} (hp : p ∈ weightedPolynomialFiltration weight k) :

D p ∈ strictWeightedPolynomialFiltration weight k

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.derivation_eq_zero_of_mem_weightedPolynomialFiltration_zero {σ : Type u_1} (weight : σ → ℕ) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (hD : ∀ (i : σ) (e : σ →₀ ℕ), (D (MvPolynomial.X i)).coeff e ≠ 0 → (Finsupp.weight weight) e + 1 ≤ weight i) {p : MvPolynomial σ ℂ} (hp : p ∈ weightedPolynomialFiltration weight 0) :

D p = 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.strictWeightedPolynomialFiltration_le_weighted_pred {σ : Type u_1} (weight : σ → ℕ) (k : ℕ) :

strictWeightedPolynomialFiltration weight (k + 1) ≤ weightedPolynomialFiltration weight k

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.derivation_mem_weightedPolynomialFiltration_succ {σ : Type u_1} (weight : σ → ℕ) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (hD : ∀ (i : σ) (e : σ →₀ ℕ), (D (MvPolynomial.X i)).coeff e ≠ 0 → (Finsupp.weight weight) e + 1 ≤ weight i) {k : ℕ} {p : MvPolynomial σ ℂ} (hp : p ∈ weightedPolynomialFiltration weight (k + 1)) :

D p ∈ weightedPolynomialFiltration weight k

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.triangular_rootOperatorWord_eq_zero_of_length_gt {σ : Type u_1} {J : Type u_2} (weight : σ → ℕ) (D : J → Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (hD : ∀ (j : J) (i : σ) (e : σ →₀ ℕ), ((D j) (MvPolynomial.X i)).coeff e ≠ 0 → (Finsupp.weight weight) e + 1 ≤ weight i) (word : List J) {k : ℕ} {p : MvPolynomial σ ℂ} (hp : p ∈ weightedPolynomialFiltration weight k) (hlen : k < word.length) :

(HigherYoungTwoRowLieIrreducibility.rootOperatorWord (fun (j : J) => ↑(D j)) word) p = 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.finsupp_weight_le_degree_mul {σ : Type u_1} (weight : σ → ℕ) (bound : ℕ) (hweight : ∀ (i : σ), weight i ≤ bound) (d : σ →₀ ℕ) :

(Finsupp.weight weight) d ≤ Finsupp.degree d * bound

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.homogeneous_mem_weightedPolynomialFiltration {σ : Type u_1} (weight : σ → ℕ) (bound m : ℕ) (hweight : ∀ (i : σ), weight i ≤ bound) {p : MvPolynomial σ ℂ} (hp : p.IsHomogeneous m) :

p ∈ weightedPolynomialFiltration weight (m * bound)

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.triangular_rootOperatorWord_eq_zero_of_isHomogeneous {σ : Type u_1} {J : Type u_2} (weight : σ → ℕ) (bound : ℕ) (hweight : ∀ (i : σ), weight i ≤ bound) (D : J → Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (hD : ∀ (j : J) (i : σ) (e : σ →₀ ℕ), ((D j) (MvPolynomial.X i)).coeff e ≠ 0 → (Finsupp.weight weight) e + 1 ≤ weight i) {m : ℕ} {p : MvPolynomial σ ℂ} (hp : p.IsHomogeneous m) (word : List J) (hlen : m * bound < word.length) :

(HigherYoungTwoRowLieIrreducibility.rootOperatorWord (fun (j : J) => ↑(D j)) word) p = 0

source

def MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.ambientPairIndex {r n : ℕ} (a : Fin n) (ha : ↑a < 2 * (r + 1)) :

Fin (r + 1)

The ambient pair index used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.ambientPairIndex a ha = ⟨↑a / 2, ⋯⟩

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.ambientPairIndex_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a : Fin (r + 1)) :

ambientPairIndex (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h a) ⋯ = a

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.ambientPairIndex_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a : Fin (r + 1)) :

ambientPairIndex (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h a) ⋯ = a

source

noncomputable def MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateGenerator {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin ((r + 1) * n)) :

MvPolynomial (Fin ((r + 1) * n)) ℂ

The isotropic coordinate generator used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateGenerator_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) :

isotropicCoordinateGenerator h (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) = HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateGenerator_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) :

isotropicCoordinateGenerator h (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p)) = HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateGenerator_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

isotropicCoordinateGenerator h (HigherHarmonicYoung.variableIndex a t) = MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)

source

noncomputable def MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.inverseIsotropicCoordinateGenerator {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin ((r + 1) * n)) :

MvPolynomial (Fin ((r + 1) * n)) ℂ

The polynomial substitution expressing an original coordinate in the inverse isotropic coordinates.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

source

@[simp]

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.inverseIsotropicCoordinateGenerator_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

inverseIsotropicCoordinateGenerator h (HigherHarmonicYoung.variableIndex a t) = MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)

source

noncomputable def MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateHom {r n : ℕ} (h : 2 * (r + 1) ≤ n) :

MvPolynomial (Fin ((r + 1) * n)) ℂ →ₐ[ℂ ] MvPolynomial (Fin ((r + 1) * n)) ℂ

The algebra map substituting the isotropic coordinate generators.

Equations

MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateHom h = MvPolynomial.aeval (MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateGenerator h)

Instances For

source

noncomputable def MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.inverseIsotropicCoordinateHom {r n : ℕ} (h : 2 * (r + 1) ≤ n) :

MvPolynomial (Fin ((r + 1) * n)) ℂ →ₐ[ℂ ] MvPolynomial (Fin ((r + 1) * n)) ℂ

The algebra map substituting the inverse isotropic coordinate generators.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateHom_X {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin ((r + 1) * n)) :

(isotropicCoordinateHom h) (MvPolynomial.X v) = isotropicCoordinateGenerator h v

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.inverseIsotropicCoordinateHom_X {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin ((r + 1) * n)) :

(inverseIsotropicCoordinateHom h) (MvPolynomial.X v) = inverseIsotropicCoordinateGenerator h v

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropic_inverse_even_identity {V : Type u_1} [AddCommGroup V] [Module ℂ V] (x y : V) :

2⁻¹ • (x + Complex.I • y + (x - Complex.I • y)) = x

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropic_inverse_odd_identity {V : Type u_1} [AddCommGroup V] [Module ℂ V] (x y : V) :

-(Complex.I / 2) • (x + Complex.I • y) + (Complex.I / 2) • (x - Complex.I • y) = y

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropic_forward_even_identity {V : Type u_1} [AddCommGroup V] [Module ℂ V] (x y : V) :

2⁻¹ • (x + y) + Complex.I • (-(Complex.I / 2) • x + (Complex.I / 2) • y) = x

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropic_forward_odd_identity {V : Type u_1} [AddCommGroup V] [Module ℂ V] (x y : V) :

2⁻¹ • (x + y) - Complex.I • (-(Complex.I / 2) • x + (Complex.I / 2) • y) = y

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateHom_comp_inverse {r n : ℕ} (h : 2 * (r + 1) ≤ n) :

(isotropicCoordinateHom h).comp (inverseIsotropicCoordinateHom h) = AlgHom.id ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ)

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.inverseIsotropicCoordinateHom_comp {r n : ℕ} (h : 2 * (r + 1) ≤ n) :

(inverseIsotropicCoordinateHom h).comp (isotropicCoordinateHom h) = AlgHom.id ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ)

source

noncomputable def MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv {r n : ℕ} (h : 2 * (r + 1) ≤ n) :

MvPolynomial (Fin ((r + 1) * n)) ℂ ≃ₐ[ℂ ] MvPolynomial (Fin ((r + 1) * n)) ℂ

The isotropic coordinate equiv used in the spherical-code argument.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv_X {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin ((r + 1) * n)) :

(isotropicCoordinateEquiv h) (MvPolynomial.X v) = isotropicCoordinateGenerator h v

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv_X_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) :

(isotropicCoordinateEquiv h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) = HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv_X_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) :

(isotropicCoordinateEquiv h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) = HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p

source

theorem MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(isotropicCoordinateEquiv h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)

source

theorem MetricCodes.Spherical.HigherYoungAmbientPositiveRootGeneratorAction.antiholomorphicDerivative_conjugateIsotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p i j : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) (HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j) = if a = i ∧ p = j then 2 else 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientPositiveRootGeneratorAction.ambientPositiveRoot_conjugateIsotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q i j : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) (HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j) = if p = j then -2 • HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i q else 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientPositiveRootGeneratorAction.ambientSumPositiveRoot_conjugateIsotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q i j : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) (HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j) = (if q = j then 2 • HigherHarmonicYoung.DeterminantVectors.isotropicVariable h i p else 0) - if p = j then 2 • HigherHarmonicYoung.DeterminantVectors.isotropicVariable h i q else 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientPositiveRootUnusedGeneratorAction.pderiv_even_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p i : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i t)) = 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientPositiveRootUnusedGeneratorAction.pderiv_odd_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p i : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i t)) = 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientPositiveRootUnusedGeneratorAction.pderiv_unused_conjugateIsotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a i j : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) (HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j) = 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientPositiveRootUnusedGeneratorAction.ambientPositiveRoot_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q i : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i t)) = 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientPositiveRootUnusedGeneratorAction.ambientSumPositiveRoot_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q i : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i t)) = 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientPositiveRootUnusedGeneratorAction.ambientShortPositiveRoot_conjugateIsotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p i j : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) (HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h i j) = if p = j then -2 • MvPolynomial.X (HigherHarmonicYoung.variableIndex i t) else 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientPositiveRootUnusedGeneratorAction.ambientShortPositiveRoot_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p i : Fin (r + 1)) (t u : Fin n) (hu : 2 * (r + 1) ≤ ↑u) :

(HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i u)) = if t = u then HigherHarmonicYoung.DeterminantVectors.isotropicVariable h i p else 0

source

theorem MetricCodes.Spherical.HigherYoungIsotropicCoordinateHomogeneity.inverseIsotropicCoordinateGenerator_isHomogeneous {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin ((r + 1) * n)) :

(HigherYoungAmbientRootNilpotence.inverseIsotropicCoordinateGenerator h v).IsHomogeneous 1

source

theorem MetricCodes.Spherical.HigherYoungIsotropicCoordinateHomogeneity.isotropicCoordinateEquiv_symm_isHomogeneous {r n m : ℕ} (h : 2 * (r + 1) ≤ n) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hp : p.IsHomogeneous m) :

((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h).symm p).IsHomogeneous m

Documentation

LeanPool.MetricCodes.HighestWeights

Highest-weight identities #