Highest-weight identities #

Diamond relations, Lie irreducibility, and isotropic highest-weight constructions.

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowFirstAxisIntertwining.sum_powerset_erase_insert {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] (P : Finset α) (a : α) (ha : a ∈ P) (f : Finset α → M) :

∑ S ∈ P.powerset, f S = ∑ S ∈ (P.erase a).powerset, (f S + f (insert a S))

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondGapShift.shiftedRowGap_raiseWeight_of_ne {r : ℕ} (lam : Fin (r + 1) → ℕ) (target preceding raised : Fin (r + 1)) (htarget : target ≠ raised) (hpreceding : preceding ≠ raised) :

AllRankArbitraryRowBranchingOperator.shiftedRowGap (HigherChannel.raiseWeight lam raised) target preceding = AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target preceding

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondGapShift.shiftedRowGap_raiseWeight_later {r : ℕ} (lam : Fin (r + 1) → ℕ) (target raised preceding : Fin (r + 1)) (htarget : target < raised) (hpreceding : preceding < target) :

AllRankArbitraryRowBranchingOperator.shiftedRowGap (HigherChannel.raiseWeight lam raised) target preceding = AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target preceding

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondGapShift.shiftedRowGap_raiseWeight_preceding {r : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (hne : target ≠ raised) (hdom : lam target ≤ lam raised) :

AllRankArbitraryRowBranchingOperator.shiftedRowGap (HigherChannel.raiseWeight lam raised) target raised = AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target raised + 1

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondGapShift.polarizationPathCoefficient_raiseWeight_later {r : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (htarget : target < raised) (S : Finset (Fin (r + 1))) :

AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient (HigherChannel.raiseWeight lam raised) target S = AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target S

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondGapShift.arbitraryRowAxialRaise_raiseWeight_later {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (htarget : target < raised) (k : Fin n) :

AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise (HigherChannel.raiseWeight lam raised) target k = AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam target k

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondGapShift.polarizationPathCoefficient_raiseWeight_of_mem {r : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (htarget : target ≠ raised) (S : Finset (Fin (r + 1))) (hS : raised ∈ S) :

AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient (HigherChannel.raiseWeight lam raised) target S = AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target S

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondGapShift.polarizationPathCoefficient_raiseWeight_of_not_mem {r : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (hrow : raised < target) (hdom : lam target ≤ lam raised) (S : Finset (Fin (r + 1))) (hS : raised ∉ S) :

AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient (HigherChannel.raiseWeight lam raised) target S = AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target S - AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target (insert raised S)

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator_apply {r n : ℕ} (target : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (p : PolynomialSpace r n) :

(MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k S) p = MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart target S) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target])) p

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondOmittedRowOperator_apply {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) :

(MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondOmittedRowOperator✝ lam target raised k) p = ∑ S ∈ ((AllRankArbitraryRowBranchingOperator.precedingRows target).erase raised).powerset, AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target (insert raised S) • (MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart target S) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target])) p)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.arbitraryRowAxialRaise_raiseWeight_eq_sub_omitted {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (hrow : raised < target) (hdom : lam target ≤ lam raised) (k : Fin n) :

AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise (HigherChannel.raiseWeight lam raised) target k = AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam target k - MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondOmittedRowOperator✝ lam target raised k

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.arbitraryRowAxialRaise_sameAxis_diamond_iff_commutator {r n : ℕ} (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (hij : i < j) (hdom : lam j ≤ lam i) (k : Fin n) :

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamond.raiseWeight_raiseWeight_comm {r : ℕ} (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (hij : i ≠ j) :

HigherChannel.raiseWeight (HigherChannel.raiseWeight lam i) j = HigherChannel.raiseWeight (HigherChannel.raiseWeight lam j) i

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingAdjacentPathExchange.iteratedArbitraryRowAxialRaise_move_last_of_rowDiamond {r n : ℕ} (lam : Fin (r + 1) → ℕ) (rows : List (Fin (r + 1))) (row : Fin (r + 1)) (hdiamond : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingAdjacentPathExchange.DominantSameAxisRowDiamond✝ n row) (hrows : ∀ i ∈ rows, i < row) (hdom : ∀ (front : List (Fin (r + 1))), (∀ (i : Fin (r + 1)), List.count i front ≤ List.count i rows) → Antitone (ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight lam front)) (k : Fin n) (p : PolynomialSpace r n) :

(AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise (ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight lam rows) row k) ((ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise lam k rows) p) = (ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise (HigherChannel.raiseWeight lam row) k rows) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingAdjacentPathExchange.arbitraryRowPathWeight_adjacentReverseSuffix_antitone {r : ℕ} {low : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (hlow : HigherRepresentationGraph.Interlaces low mu) (row : Fin (r + 2)) (front : List (Fin (r + 2))) (hfront : ∀ (i : Fin (r + 2)), List.count i front ≤ List.count i (HigherYoungArbitraryRankAdjacentInterlacingSchedule.adjacentReverseSuffix low mu row)) :

Antitone (ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight (ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight (ThreeRowYoungBranching.appendZeroWeight mu) (HigherYoungArbitraryRankAdjacentInterlacingSchedule.adjacentReversePrefix low mu row)) front)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingAdjacentPathExchange.reverseInterlacingPolynomialSeed_adjacent_raise_of_rowDiamond {r n : ℕ} {low : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (hlow : HigherRepresentationGraph.Interlaces low mu) (row : Fin (r + 2)) (hdiamond : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingAdjacentPathExchange.DominantSameAxisRowDiamond✝ (n + 1) row) (p : ↥(HarmonicYoungSpace mu)) :

(AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise low row (Fin.last n)) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed low mu) p) = (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed (HigherChannel.raiseWeight low row) mu) p

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingAdjacentPathExchange.reverseInterlacingPolynomialSeed_adjacent_raise_of_diamond {r n : ℕ} (hdiamond : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingAdjacentPathExchange.DominantSameAxisDiamond✝ (r + 1) (n + 1)) {low : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (hlow : HigherRepresentationGraph.Interlaces low mu) (row : Fin (r + 2)) (p : ↥(HarmonicYoungSpace mu)) :

source

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

(projectedCoordinateRaise (HigherChannel.raiseWeight low row) low ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hlowGram) p) = MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinAdjacentProjectedCoefficient.canonicalAdjacentProjectedRaiseCoefficient✝ low mu row hlow hhigh hlowGram hhighGram • (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre (HigherChannel.raiseWeight low row) mu hhigh hhighGram) p

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinAdjacentProjectedCoefficient.canonicalAdjacentProjectedRaiseCoefficient_sq {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hlowGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (hhighGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherChannel.raiseWeight low row) mu hhigh) :

MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinAdjacentProjectedCoefficient.canonicalAdjacentProjectedRaiseCoefficient✝ low mu row hlow hhigh hlowGram hhighGram ^ 2 = (ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row)⁻¹ ^ 2 * AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram (HigherChannel.raiseWeight low row) mu hhigh hhighGram / AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram low mu hlow hlowGram

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinAdjacentProjectedCoefficient.canonicalAdjacentProjectedRaiseCoefficient_sq_iff_fischerGram {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hlowGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (hhighGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherChannel.raiseWeight low row) mu hhigh) :

MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinAdjacentProjectedCoefficient.canonicalAdjacentProjectedRaiseCoefficient✝ low mu row hlow hhigh hlowGram hhighGram ^ 2 = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * HigherChannel.plusProbability (n + 1) low mu row ↔ AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram (HigherChannel.raiseWeight low row) mu hhigh hhighGram = ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row ^ 2 * ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram low mu hlow hlowGram * HigherChannel.plusProbability (n + 1) low mu row

source

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

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual_apply {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (p : PolynomialSpace r n) :

(MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual✝ lam target raised k S) p = (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k (insert raised S)) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k) p) - (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k) ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k (insert raised S)) p) - AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target raised • ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k S) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k) p) - (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k) ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k S) p)) - (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k S) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k) p)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondFullCommutator.arbitraryRowAxialRaise_eq_paired_paths {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (hrow : raised < target) (k : Fin n) (p : PolynomialSpace r n) :

(AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam target k) p = ∑ S ∈ ((AllRankArbitraryRowBranchingOperator.precedingRows target).erase raised).powerset, AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target (insert raised S) • ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k (insert raised S)) p - AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target raised • (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k S) p)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondFullCommutator.arbitraryRowAxialRaise_commutator_sub_omitted_eq_sum_residual {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (hrow : raised < target) (k : Fin n) :

AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam target k ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam target k - MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondOmittedRowOperator✝ lam target raised k ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k = ∑ S ∈ ((AllRankArbitraryRowBranchingOperator.precedingRows target).erase raised).powerset, AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target (insert raised S) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual✝ lam target raised k S

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondFullCommutator.arbitraryRowAxialRaise_commutator_iff_sum_residual_eq_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (target raised : Fin (r + 1)) (hrow : raised < target) (k : Fin n) :

AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam target k ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam target k = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondOmittedRowOperator✝ lam target raised k ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam raised k ↔ ∑ S ∈ ((AllRankArbitraryRowBranchingOperator.precedingRows target).erase raised).powerset, AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam target (insert raised S) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual✝ lam target raised k S = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondGapDifference.shiftedRowGap_sub_shiftedRowGap {r : ℕ} (lam : Fin (r + 1) → ℕ) (a i j : Fin (r + 1)) (hai : a < i) (hij : i < j) (hji : lam j ≤ lam i) (hia : lam i ≤ lam a) :

AllRankArbitraryRowBranchingOperator.shiftedRowGap lam j a - AllRankArbitraryRowBranchingOperator.shiftedRowGap lam i a = AllRankArbitraryRowBranchingOperator.shiftedRowGap lam j i + 1

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondRootCommutator.polarization_axialCoordinate_mul_lowerPolarizationPath_sub {r n : ℕ} (a b start : Fin (r + 1)) (k : Fin n) (path : List (Fin (r + 1))) (p : PolynomialSpace r n) :

(polarization r n a b) (MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p) - MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) ((polarization r n a b) p) = (if b = start then MvPolynomial.X (variableIndex a k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p else 0) + MvPolynomial.X (variableIndex start k) * (ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator a b path) p

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondRootCommutator.axialCoordinateLowerPath_apply {r n : ℕ} (start : Fin (r + 1)) (k : Fin n) (path : List (Fin (r + 1))) (p : PolynomialSpace r n) :

(MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondRootCommutator.axialCoordinateLowerPath✝ start k path) p = MvPolynomial.X (variableIndex start k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondRootCommutator.polarization_arbitraryRowAxialRaise_commutator_sum {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row a b : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) :

(polarization r n a b) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) - (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) ((polarization r n a b) p) = ∑ S ∈ (AllRankArbitraryRowBranchingOperator.precedingRows row).powerset, AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient lam row S • ((if b = AllRankArbitraryRowBranchingOperator.polarizationPathStart row S then MvPolynomial.X (variableIndex a k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])) p else 0) + MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart row S) k) * (ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator a b ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])) p)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixRootCommute.upperPolarizationPathCommutator_eq_zero_of_avoids {r n : ℕ} (a b : Fin (r + 1)) (path : List (Fin (r + 1))) (ha : a ∉ path) (hb : b ∉ path) :

ArbitraryRowMickelssonPathCommutator.upperPolarizationPathCommutator a b path = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixRootCommute.polarization_arbitraryRowAxialRaise_commutator_eq_zero_of_gt {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row a b : Fin (r + 1)) (ha : row < a) (hb : row < b) (k : Fin n) (p : PolynomialSpace r n) :

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixRootCommute.polarization_arbitraryRowAxialRaise_commute_of_gt {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row a b : Fin (r + 1)) (ha : row < a) (hb : row < b) (k : Fin n) (p : PolynomialSpace r n) :

(polarization r n a b) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) = (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) ((polarization r n a b) p)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixRootCommute.lowerPolarizationPath_arbitraryRowAxialRaise_commute_of_gt {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (path : List (Fin (r + 1))) (hpath : ∀ q ∈ path, row < q) (p : PolynomialSpace r n) :

(AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) = (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p)

source

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

(S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) = ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.precedingDiamondSubset✝ pivot S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.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) = ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.precedingDiamondSubset✝ pivot S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ pivot :: (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.succeedingDiamondSubset✝ pivot S).sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2

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) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k S = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.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) :

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

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) :

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

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) :

(MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot target k t) p = ∑ S ∈ (AllRankArbitraryRowBranchingOperator.precedingRows pivot).powerset, MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff✝ lam pivot t S • (MetricCodes.Spherical.HigherHarmonicYoung.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))) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.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) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.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) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff✝ lam pivot t S = -(AllRankArbitraryRowBranchingOperator.shiftedRowGap lam pivot a + t) * MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.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 : ℝ) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.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) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff✝ lam a.succ t (insert a.castSucc S) = -MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.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) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff✝ lam a.succ t S = (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam a.succ a.castSucc + t) * MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.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) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k (insert a.castSucc S) = MetricCodes.Spherical.HigherHarmonicYoung.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 : ℝ) :

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 = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.precedingDiamondSubset✝ pivot S ∪ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.succeedingDiamondSubset✝ pivot S

source

@[simp]

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

a ∈ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.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 \ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.precedingDiamondSubset✝ pivot S ∪ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot \ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.succeedingDiamondSubset✝ pivot S

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) = -MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.upperDiamondPathCoefficient✝ lam target pivot S * MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff✝ lam pivot (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target pivot + 1) (MetricCodes.Spherical.HigherHarmonicYoung.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 ∪ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot

source

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

Disjoint (AllRankArbitraryRowBranchingOperator.precedingRows pivot) (MetricCodes.Spherical.HigherHarmonicYoung.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 ⊆ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot) :

MetricCodes.Spherical.HigherHarmonicYoung.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 ⊆ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot) :

MetricCodes.Spherical.HigherHarmonicYoung.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 ⊆ MetricCodes.Spherical.HigherHarmonicYoung.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 ⊆ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot) :

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

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] = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.diamondUpperSuffixNext✝ target U :: MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.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 ⊆ MetricCodes.Spherical.HigherHarmonicYoung.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 ⊆ MetricCodes.Spherical.HigherHarmonicYoung.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 ⊆ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot) (hupper : (U.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target] = next :: tail) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondResidualSuffixPartition.omittedDiamondPrefix✝ target k (L ∪ U) (L.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) next = MetricCodes.Spherical.HigherHarmonicYoung.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 ⊆ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot) :

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

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) :

(MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.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, MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff✝ lam pivot (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target pivot + 1) L • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.localSpectralDiamondResidual✝ lam target pivot next k L = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.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 ⊆ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot) (hupper : (U.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [target] = next :: tail) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual✝ lam target pivot k (L ∪ U) = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.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) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual✝ lam target pivot k S = -∑ U ∈ (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot).powerset, MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.upperDiamondPathCoefficient✝ lam target pivot U • ∑ L ∈ (AllRankArbitraryRowBranchingOperator.precedingRows pivot).powerset, MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathCoeff✝ lam pivot (AllRankArbitraryRowBranchingOperator.shiftedRowGap lam target pivot + 1) L • MetricCodes.Spherical.HigherHarmonicYoung.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 ⊆ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot) :

pivot < MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.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) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondFullCommutator.diamondPairResidual✝ lam target pivot k S = -∑ U ∈ (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.diamondSucceedingRows✝ target pivot).powerset, MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixCoefficientFactor.upperDiamondPathCoefficient✝ lam target pivot U • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.spectralDiamondPrefixResidual✝ lam target pivot (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSuffixSummation.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) ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ pivot k S) p) - (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ pivot k S) ((polarization r n target pivot) p) = (MetricCodes.Spherical.HigherHarmonicYoung.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) ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondPathCommutator.diamondPathOperator✝ target k S) p) - (MetricCodes.Spherical.HigherHarmonicYoung.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) ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot target k t) p) - (MetricCodes.Spherical.HigherHarmonicYoung.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 ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot target k t = MetricCodes.Spherical.HigherHarmonicYoung.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) ((MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot pivot k t) p) - (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot pivot k t) ((polarization r n target pivot) p) = (MetricCodes.Spherical.HigherHarmonicYoung.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 ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot pivot k t - MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot pivot k t ∘ₗ polarization r n target pivot = MetricCodes.Spherical.HigherHarmonicYoung.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 = MetricCodes.Spherical.HigherHarmonicYoung.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 : MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot pivot k (h + 1) ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k = AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot pivot k (h + 1)) (hrtt : (h + 1) • (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot next k (h + 1) ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot next k (h + 1)) = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot pivot k (h + 1) ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot next k 0 - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot next k (h + 1)) :

(MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot pivot k (h + 1) ∘ₗ polarization r n next pivot) ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot pivot k (h + 1) ∘ₗ polarization r n next pivot - h • (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot next k (h + 1) ∘ₗ AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k - AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam pivot k ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot next k (h + 1)) - MetricCodes.Spherical.HigherHarmonicYoung.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

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam a.succ target k u ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam a.succ target k v = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam a.succ target k v ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.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 : ℝ) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam 0 target k u ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam 0 target k v = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam 0 target k v ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.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 : ℝ) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot target k u ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot target k v = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot target k v ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisDiamondSpectralPath.spectralPathOperator✝ lam pivot target k u

source

MetricCodes.Spherical.HigherHarmonicYoung.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 = MetricCodes.Spherical.HigherHarmonicYoung.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 : ℕ) :

MetricCodes.Spherical.HigherHarmonicYoung.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 : MetricCodes.Spherical.HigherHarmonicYoung.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 →₀ ℕ) :

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

source

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

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

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 : MvPolynomial.coeff d p ≠ 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 : MvPolynomial.coeff d p ≠ 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.coeff d (MvPolynomial.X a * (MvPolynomial.pderiv b) p) = if d a = 0 then 0 else (d b + 1) • MvPolynomial.coeff (d - Finsupp.single a 1 + Finsupp.single b 1) p

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

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

(MvPolynomial.eval MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.sourceDiagonalEvaluation✝) (DeterminantVectors.sourceLeadingMinor k) = 1

source

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

(MvPolynomial.eval MetricCodes.Spherical.HigherHarmonicYoung.BideterminantHighestLine.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

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 : MetricCodes.Spherical.HigherYoungCyclicHighestSchur.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 : MetricCodes.Spherical.HigherYoungCyclicHighestSchur.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

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

q ∈ MetricCodes.Spherical.HigherYoungAllRankSourceHighestKernel.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) ∈ MetricCodes.Spherical.HigherYoungAllRankSourceHighestKernel.sourceHighestKernel✝ lam

source

@[simp]

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

(MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.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 = MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent✝ lam

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 + MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.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) + MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.belowDiagonalWeight✝ z = belowDiagonalMass d

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)) :

MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.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 (MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootTargetExponent✝ d i j) (i, k) = 0 then 0 else ((MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootTargetExponent✝ d i j) (j, k) + 1) • MvPolynomial.coeff (MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootSourceExponent✝ d i j k) p) = 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 (MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.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 < (MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.upperRootTargetExponent✝ d i j) (i, k)) :

belowDiagonalMass (MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.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) :

(MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.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)) :

(MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.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) :

(MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.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) :

(MetricCodes.Spherical.HigherYoungAllRankSourceCoefficientStraightening.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 → MvPolynomial.coeff e p = 0) :

MvPolynomial.coeff d p = 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 → MvPolynomial.coeff d p = 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 : MvPolynomial.coeff (MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent✝ lam) p = 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 : MvPolynomial.coeff (MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent✝ lam) p = MvPolynomial.coeff (MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent✝ lam) q) :

p = q

source

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

MvPolynomial.coeff (MetricCodes.Spherical.HigherYoungAllRankSourceDiagonalBalance.sourceDiagonalExponent✝ lam) (HigherHarmonicYoung.DeterminantVectors.sourceHighestWeightPolynomial (HigherHarmonicYoung.DeterminantVectors.signatureExponent 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

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

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

source

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

(MvPolynomial.monomial d) c ∈ MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.weightedPolynomialFiltration✝ weight ((Finsupp.weight weight) d)

source

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

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

source

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

MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.strictWeightedPolynomialFiltration✝ weight k ≤ MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.strictWeightedPolynomialFiltration✝ weight l

source

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

p * q ∈ MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.strictWeightedPolynomialFiltration✝ weight (k + l)

source

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

D p ∈ MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.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 : σ →₀ ℕ), MvPolynomial.coeff e (D (MvPolynomial.X i)) ≠ 0 → (Finsupp.weight weight) e + 1 ≤ weight i) {p : MvPolynomial σ ℂ} (hp : p ∈ MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.weightedPolynomialFiltration✝ weight 0) :

D p = 0

source

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

MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.strictWeightedPolynomialFiltration✝ weight (k + 1) ≤ MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.weightedPolynomialFiltration✝ weight k

source

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

D p ∈ MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.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 : σ →₀ ℕ), MvPolynomial.coeff e ((D j) (MvPolynomial.X i)) ≠ 0 → (Finsupp.weight weight) e + 1 ≤ weight i) (word : List J) {k : ℕ} {p : MvPolynomial σ ℂ} (hp : p ∈ MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.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 ∈ MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.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 : σ →₀ ℕ), MvPolynomial.coeff e ((D j) (MvPolynomial.X i)) ≠ 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

@[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) :

MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.inverseIsotropicCoordinateGenerator✝ h (HigherHarmonicYoung.variableIndex a t) = MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)

source

@[simp]

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

(MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.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)) :

(MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.inverseIsotropicCoordinateHom✝ h) (MvPolynomial.X v) = MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.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) :

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

source

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

(MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.inverseIsotropicCoordinateHom✝ h).comp (MetricCodes.Spherical.HigherYoungAmbientRootNilpotence.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)) :

(MetricCodes.Spherical.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 #