All-rank harmonic rigidity #

↑↑((rootJointHarmonicActionUpperRootStructureCross n lam k) f S) = ∑ α : PositiveRoot r, if hα : α ∈ ↑↑S then ∑ β : PositiveRoot r, if hβ : β ∈ ↑↑S then 0 else if hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i then ∑ γ : PositiveRoot r, if _hγ : rootStructureConstant β γ α = 0 then 0 else (rootSwapExteriorHodgeSign S α β * rootStructureConstant β γ α) • (polarization r n (positiveRootFirst γ) (positiveRootSecond γ)) ↑↑(f (rootAdmissibleSwap lam S α β hα hβ hadm)) else 0 else 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge_eq_halves {r n k : ℕ} (lam : Fin (r + 1) → ℕ) :

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge✝ n lam k = MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionBracketMixed✝ n lam k + (weightedRootBracketCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedRootBracketCoboundary n lam (k + 1))

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge_eq_actionBracket_add_bracketAction {r n k : ℕ} (lam : Fin (r + 1) → ℕ) :

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge_add_offDiagonal_eq_zero_of_halves {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hupper : MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionBracketMixed✝ n lam k + rootJointHarmonicActionUpperRootStructureCross n lam (k + 1) = 0) (hlower : rootJointHarmonicBracketActionMixed n lam k + rootJointHarmonicActionLowerRootStructureCross n lam (k + 1) = 0) :

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge✝ n lam k + rootJointHarmonicActionHodgeOffDiagonal n lam (k + 1) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicPolynomialInclusion_actionBracketMixed_intertwines {r n k : ℕ} (lam : Fin (r + 1) → ℕ) :

rootJointHarmonicPolynomialInclusion n lam (k + 1) ∘ₗ MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionBracketMixed✝ n lam k = MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionBracketMixed✝ r n k ∘ₗ rootJointHarmonicPolynomialInclusion n lam (k + 1)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_output_eq_left_zero {r : ℕ} (α β : PositiveRoot r) :

rootStructureConstant α β α = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_root_pairs_eq_ordered_add_reverse {r : ℕ} {V : Type u_1} [AddCommGroup V] (F : PositiveRoot r → PositiveRoot r → V) (hzero : ∀ (α β : PositiveRoot r), ¬α < β → ¬β < α → F α β = 0) :

∑ α : PositiveRoot r, ∑ β : PositiveRoot r, F α β = ∑ α : PositiveRoot r, ∑ β : PositiveRoot r, if α < β then F α β + F β α else 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorActionCoboundary_bracket_eq_neg_upperStructure (r n : ℕ) :

fullRootExteriorActionCoboundary r n * fullRootExteriorBracket r n + fullRootExteriorBracket r n * fullRootExteriorActionCoboundary r n = -MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperRootStructureIncidence✝ r n

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperRootStructureIncidence_zeroExtension_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) :

(MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperRootStructureIncidence✝ r n) ((rootPolynomialChainZeroExtension r n k) ((rootJointHarmonicPolynomialInclusion n lam k) f)) ↑↑S = ↑↑((rootJointHarmonicActionUpperRootStructureCross n lam k) f S)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionBracketMixed_add_upperStructure_eq_zero {r n k : ℕ} (lam : Fin (r + 1) → ℕ) :

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionBracketMixed✝ n lam k + rootJointHarmonicActionUpperRootStructureCross n lam (k + 1) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootChevalleyEilenbergBoundary_comp_self_of_actionBracket (r n k : ℕ) (ha : rootActionBoundary r n k ∘ₗ rootActionBoundary r n (k + 1) + rootActionBoundary r n k ∘ₗ rootBracketBoundary r n (k + 1) + rootBracketBoundary r n k ∘ₗ rootActionBoundary r n (k + 1) = 0) (hb : rootBracketBoundary r n k ∘ₗ rootBracketBoundary r n (k + 1) = 0) :

rootChevalleyEilenbergBoundary r n k ∘ₗ rootChevalleyEilenbergBoundary r n (k + 1) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential_comp_self_of_unweighted {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (h : rootChevalleyEilenbergBoundary r n k ∘ₗ rootChevalleyEilenbergBoundary r n (k + 1) = 0) :

weightedChevalleyEilenbergDifferential n lam k ∘ₗ weightedChevalleyEilenbergDifferential n lam (k + 1) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.fischerCore_injective_of_coercive_add_adjoint_squares {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] (cE : InnerProductSpace.Core ℝ E) (cF : InnerProductSpace.Core ℝ F) (cG : InnerProductSpace.Core ℝ G) (L : F →ₗ[ℝ ] F) (B : F →ₗ[ℝ ] E) (Bstar : E →ₗ[ℝ ] F) (C : G →ₗ[ℝ ] F) (Cstar : F →ₗ[ℝ ] G) (hBstar : ∀ (x : E) (y : F), inner ℝ (Bstar x) y = inner ℝ x (B y)) (hCstar : ∀ (x : F) (y : G), inner ℝ (Cstar x) y = inner ℝ x (C y)) (hL : ∀ (x : F), x ≠ 0 → 0 < inner ℝ x (L x)) :

Function.Injective ⇑(L + Bstar ∘ₗ B + C ∘ₗ Cstar)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_fischer_adjoint {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam (k + 1)) (q : RootJointHarmonicChain n lam k) :

inner ℝ ((weightedChevalleyEilenbergDifferential n lam k) p) q = inner ℝ p ((MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenbergCoboundary✝ n lam k) q)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_fischer_adjoint_reverse {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (q : RootJointHarmonicChain n lam k) (p : RootJointHarmonicChain n lam (k + 1)) :

inner ℝ ((MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenbergCoboundary✝ n lam k) q) p = inner ℝ q ((weightedChevalleyEilenbergDifferential n lam k) p)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketBoundary_fischer_adjoint_reverse {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (q : RootJointHarmonicChain n lam k) (p : RootJointHarmonicChain n lam (k + 1)) :

inner ℝ ((weightedRootBracketCoboundary n lam k) q) p = inner ℝ q ((weightedRootBracketBoundary n lam k) p)

source

e.range = d.ker

source

(weightedChevalleyEilenbergDifferential n lam (k + 1)).range = (weightedChevalleyEilenbergDifferential n lam k).ker

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonic_action_plus_mixed_hodge_eq_diagonal_of_cross_cancellation {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (haction : weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1) = rootJointHarmonicHodgeDiagonal n lam (k + 1) + rootJointHarmonicActionHodgeOffDiagonal n lam (k + 1)) (hmixed : MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge✝ n lam k + rootJointHarmonicActionHodgeOffDiagonal n lam (k + 1) = 0) :

weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1) + MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicFullMixedHodge✝ n lam k = rootJointHarmonicHodgeDiagonal n lam (k + 1)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_mixed_hodge_eq_diagonal_of_root_cross_halves {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (haction : weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1) = rootJointHarmonicHodgeDiagonal n lam (k + 1) + rootJointHarmonicActionHodgeOffDiagonal n lam (k + 1)) (hupper : MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionBracketMixed✝ n lam k + rootJointHarmonicActionUpperRootStructureCross n lam (k + 1) = 0) (hlower : rootJointHarmonicBracketActionMixed n lam k + rootJointHarmonicActionLowerRootStructureCross n lam (k + 1) = 0) :

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionBracketBoundary_mixed_comp_self_zero (r n k : ℕ) :

rootActionBoundary r n k ∘ₗ rootActionBoundary r n (k + 1) + rootActionBoundary r n k ∘ₗ rootBracketBoundary r n (k + 1) + rootBracketBoundary r n k ∘ₗ rootActionBoundary r n (k + 1) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracketBoundary_comp_self_zero (r n k : ℕ) :

rootBracketBoundary r n k ∘ₗ rootBracketBoundary r n (k + 1) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootChevalleyEilenbergBoundary_comp_self_zero (r n k : ℕ) :

rootChevalleyEilenbergBoundary r n k ∘ₗ rootChevalleyEilenbergBoundary r n (k + 1) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential_comp_self_zero {r n k : ℕ} (lam : Fin (r + 1) → ℕ) :

weightedChevalleyEilenbergDifferential n lam k ∘ₗ weightedChevalleyEilenbergDifferential n lam (k + 1) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_exact_of_hodge_root_identities {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (haction : weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1) = rootJointHarmonicHodgeDiagonal n lam (k + 1) + rootJointHarmonicActionHodgeOffDiagonal n lam (k + 1)) (hupper : MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionBracketMixed✝ n lam k + rootJointHarmonicActionUpperRootStructureCross n lam (k + 1) = 0) (hlower : rootJointHarmonicBracketActionMixed n lam k + rootJointHarmonicActionLowerRootStructureCross n lam (k + 1) = 0) :

(weightedChevalleyEilenbergDifferential n lam (k + 1)).range = (weightedChevalleyEilenbergDifferential n lam k).ker

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedChevalleyEilenberg_exact {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) :

(weightedChevalleyEilenbergDifferential n lam (k + 1)).range = (weightedChevalleyEilenbergDifferential n lam k).ker

source

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

HigherHierarchy.Weyl.dimension n lam = ↑(Module.finrank ℝ ↥(HarmonicYoungSpace lam))

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankFischerGramWeylRecurrence.loweredInternalYoungWeight_raiseWeight {r : ℕ} (low : Fin (r + 1) → ℕ) (row : Fin (r + 1)) :

HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight (HigherChannel.raiseWeight low row) row = low

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankFischerGramWeylRecurrence.finrank_raiseWeight_eq_finrank_mul_weylEdgeRatio {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (row : Fin (r + 1)) (hlow : HigherChannel.FiniteInterlacing n low mu) (hhigh : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight low row) mu) :

↑(Module.finrank ℝ ↥(HarmonicYoungSpace (HigherChannel.raiseWeight low row))) = ↑(Module.finrank ℝ ↥(HarmonicYoungSpace low)) * HigherChannel.weylEdgeRatio n low row

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankFischerGramWeylRecurrence.arbitraryRowRaiseTensorGramScalar_eq_lowerGram_mul_weylEdgeRatio {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (row : Fin (r + 1)) (hlow : HigherChannel.FiniteInterlacing n low mu) (hhigh : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight low row) mu) :

ArbitraryRowRaiseLowerTensorTrace.arbitraryRowRaiseTensorGramScalar (HigherChannel.raiseWeight low row) row = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * HigherChannel.weylEdgeRatio n low row

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose_X {m : ℕ} (i j : Fin m) :

(MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose✝ m) (MvPolynomial.X (i, j)) = MvPolynomial.X (j, i)

source

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

(MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose✝ m) ((MvPolynomial.pderiv (i, j)) p) = (MvPolynomial.pderiv (j, i)) ((MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose✝ m) p)

source

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

(MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose✝ m) ((HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) p) = (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) ((MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose✝ m) p)

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceExponentTranspose_apply {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (i j : Fin m) :

(MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceExponentTranspose✝ d) (i, j) = d (j, i)

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceExponentTranspose_transpose {m : ℕ} (d : Fin m × Fin m →₀ ℕ) :

MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceExponentTranspose✝ (MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceExponentTranspose✝ d) = d

source

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

MvPolynomial.coeff (MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceExponentTranspose✝ d) ((MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.sourceMatrixTranspose✝ m) p) = MvPolynomial.coeff d p

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankColumnHighestCoefficientDescent.exists_lowerTriangular_coeff_ne_zero_of_columnHighest {m : ℕ} (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix m) (hp : p ≠ 0) (hhighest : ∀ (i j : Fin m), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) p = 0) :

∃ (d : Fin m × Fin m →₀ ℕ), MvPolynomial.coeff d p ≠ 0 ∧ ∀ (i j : Fin m), i < j → d (i, j) = 0

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankTriangularMarginDominance.sourceMarginPrefix_succ {m : ℕ} (f : Fin m → ℕ) (i : Fin m) :

MetricCodes.Spherical.HigherYoungArbitraryRankTriangularMarginDominance.sourceMarginPrefix✝ f (↑i + 1) = MetricCodes.Spherical.HigherYoungArbitraryRankTriangularMarginDominance.sourceMarginPrefix✝ f ↑i + f i

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankTriangularMarginDominance.sourceMargins_eq_of_upper_and_lower {m : ℕ} (lam nu : Fin m → ℕ) (dUpper dLower : Fin m × Fin m →₀ ℕ) (hupper : ∀ (i j : Fin m), j < i → dUpper (i, j) = 0) (hlower : ∀ (i j : Fin m), i < j → dLower (i, j) = 0) (hupperRow : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree dUpper i = lam i) (hupperColumn : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree dUpper i = nu i) (hlowerRow : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceRowDegree dLower i = lam i) (hlowerColumn : ∀ (i : Fin m), HigherHarmonicYoung.BideterminantHighestLine.sourceColumnDegree dLower i = nu i) :

lam = nu

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnVariableWeight_weight {m : ℕ} (d : Fin m × Fin m →₀ ℕ) :

(Finsupp.weight (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnVariableWeight✝ m)) d = fun (j : Fin m) => BideterminantHighestLine.sourceColumnDegree d j

source

@[simp]

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

MvPolynomial.coeff d (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p) = if (fun (j : Fin m) => BideterminantHighestLine.sourceColumnDegree d j) = ν then MvPolynomial.coeff d p else 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent_ne_zero_of_coeff_ne_zero {m : ℕ} (p : BideterminantHighestLine.SourceMatrix m) (d : Fin m × Fin m →₀ ℕ) (hd : MvPolynomial.coeff d p ≠ 0) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ (fun (j : Fin m) => BideterminantHighestLine.sourceColumnDegree d j) p ≠ 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightCartan.sourceColumnRoot_self_columnWeightComponent {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (i : Fin m) :

(BideterminantHighestLine.sourceColumnRoot i i) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p) = ↑(ν i) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.sourceColumnDegree_add {m : ℕ} (d e : Fin m × Fin m →₀ ℕ) (column : Fin m) :

BideterminantHighestLine.sourceColumnDegree (d + e) column = BideterminantHighestLine.sourceColumnDegree d column + BideterminantHighestLine.sourceColumnDegree e column

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.sourceColumnDegree_single {m : ℕ} (row column target : Fin m) (degree : ℕ) :

BideterminantHighestLine.sourceColumnDegree (fun₀ | (row, column) => degree) target = if column = target then degree else 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.sourceColumnDegree_rowTransfer {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (source target column test : Fin m) (hoccupied : 0 < d (source, column)) :

BideterminantHighestLine.sourceColumnDegree ((d - fun₀ | (source, column) => 1) + fun₀ | (target, column) => 1) test = BideterminantHighestLine.sourceColumnDegree d test

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.columnWeightComponent_X_mul_pderiv_row {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (source target column : Fin m) :

MvPolynomial.X (target, column) * (MvPolynomial.pderiv (source, column)) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p) = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν (MvPolynomial.X (target, column) * (MvPolynomial.pderiv (source, column)) p)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.sourceRowRoot_columnWeightComponent {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (source target : Fin m) :

(BideterminantHighestLine.sourceRowRoot target source) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p) = MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν ((BideterminantHighestLine.sourceRowRoot target source) p)

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.columnWeightComponent_rowHighest {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hhighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceRowRoot i j) p = 0) (i j : Fin m) :

i < j → (BideterminantHighestLine.sourceRowRoot i j) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRowRoot.columnWeightComponent_rowCartan {m : ℕ} (ν lam : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hcartan : ∀ (i : Fin m), (BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) (i : Fin m) :

(BideterminantHighestLine.sourceRowRoot i i) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p) = ↑(lam i) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRootShift.columnWeight_shift_sub_single_add {m : ℕ} (d : Fin m × Fin m →₀ ℕ) (k i j : Fin m) (hd : d (k, i) ≠ 0) :

(fun (t : Fin m) => BideterminantHighestLine.sourceColumnDegree ((d - fun₀ | (k, i) => 1) + fun₀ | (k, j) => 1) t) + Pi.single i 1 = (fun (t : Fin m) => BideterminantHighestLine.sourceColumnDegree d t) + Pi.single j 1

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRootShift.coeff_sourceColumnRoot_columnWeightComponent {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (i j : Fin m) (hij : i ≠ j) (d : Fin m × Fin m →₀ ℕ) :

MvPolynomial.coeff d ((BideterminantHighestLine.sourceColumnRoot i j) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p)) = if ν + Pi.single i 1 = (fun (t : Fin m) => BideterminantHighestLine.sourceColumnDegree d t) + Pi.single j 1 then MvPolynomial.coeff d ((BideterminantHighestLine.sourceColumnRoot i j) p) else 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRootShift.columnWeightComponent_columnHighest {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (i j : Fin m) (hij : i < j) (hhighest : (BideterminantHighestLine.sourceColumnRoot i j) p = 0) :

(BideterminantHighestLine.sourceColumnRoot i j) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightRootShift.columnWeightComponent_columnHighest_all {m : ℕ} (ν : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hhighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceColumnRoot i j) p = 0) (i j : Fin m) (hij : i < j) :

(BideterminantHighestLine.sourceColumnRoot i j) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankColumnWeightProjection.columnWeightComponent✝ ν p) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankIsotropicSupportCartanWeight.exists_upperTriangular_coeff_ne_zero_of_rowHighest {m : ℕ} (p : BideterminantHighestLine.SourceMatrix m) (hp : p ≠ 0) (hhighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceRowRoot i j) p = 0) :

∃ (d : Fin m × Fin m →₀ ℕ), MvPolynomial.coeff d p ≠ 0 ∧ ∀ (i j : Fin m), j < i → d (i, j) = 0

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankIsotropicSupportCartanWeight.source_rowWeight_eq_columnWeight_of_biHighest {m : ℕ} (lam nu : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hp : p ≠ 0) (hrow : ∀ (i : Fin m), (BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) (hcolumn : ∀ (i : Fin m), (BideterminantHighestLine.sourceColumnRoot i i) p = ↑(nu i) • p) (hrowHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceRowRoot i j) p = 0) (hcolumnHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceColumnRoot i j) p = 0) :

lam = nu

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankIsotropicSupportCartanWeight.sourceColumnDegree_eq_rowWeight_of_coeff_ne_zero_of_biHighest {m : ℕ} (lam : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hrow : ∀ (i : Fin m), (BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) (hrowHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceRowRoot i j) p = 0) (hcolumnHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceColumnRoot i j) p = 0) (d : Fin m × Fin m →₀ ℕ) (hd : MvPolynomial.coeff d p ≠ 0) :

(fun (i : Fin m) => BideterminantHighestLine.sourceColumnDegree d i) = lam

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankIsotropicSupportCartanWeight.sourceColumnRoot_self_eq_rowWeight_of_biHighest {m : ℕ} (lam : Fin m → ℕ) (p : BideterminantHighestLine.SourceMatrix m) (hrow : ∀ (i : Fin m), (BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) (hrowHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceRowRoot i j) p = 0) (hcolumnHighest : ∀ (i j : Fin m), i < j → (BideterminantHighestLine.sourceColumnRoot i j) p = 0) (i : Fin m) :

(BideterminantHighestLine.sourceColumnRoot i i) p = ↑(lam i) • p

source

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanRowEquations.rowDerivation_polynomialComplexification {r n : ℕ} (i j : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) :

(HigherHarmonicYoung.DeterminantVectors.rowDerivation i j) (HigherYoungTwoRowLieIrreducibility.polynomialComplexification p) = HigherYoungTwoRowLieIrreducibility.polynomialComplexification ((HigherHarmonicYoung.polarization r n i j) p)

source

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanRowEquations.rowDerivation_self_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (i : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.rowDerivation i i) f = ↑(lam i) • f

source

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanRowEquations.rowDerivation_upper_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (i j : Fin (r + 1)) (hij : i < j) :

(HigherHarmonicYoung.DeterminantVectors.rowDerivation i j) f = 0

source

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanTraceFree.complexTraceOperator_polynomialComplexification {r n : ℕ} (i j : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) :

HigherHarmonicYoung.complexTraceOperator i j (HigherYoungTwoRowLieIrreducibility.polynomialComplexification p) = HigherYoungTwoRowLieIrreducibility.polynomialComplexification ((HigherHarmonicYoung.traceOperator r n i j) p)

source

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanTraceFree.complexTraceOperator_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (i j : Fin (r + 1)) :

HigherHarmonicYoung.complexTraceOperator i j f = 0

source

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanHomogeneity.isHomogeneous_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) :

f.IsHomogeneous (∑ i : Fin (r + 1), lam i)

source

theorem MetricCodes.Spherical.HigherYoungOrthogonalPositiveRootKernelIsotropicSupport.exists_nullSubstitution_of_mem_fullYoungComplexPolynomialSpan_maximalCartan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hcartan : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) f = ↑(2 * ∑ i : Fin (r + 1), lam i) • f) :

∃ (q : MvPolynomial (Fin (r + 1) × Fin (r + 1)) ℂ), (HigherHarmonicYoung.nullSubstitution h) q = f

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.sourceColumnRoot_upper_of_positiveRootKernel {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) ((HigherHarmonicYoung.nullSubstitution hn) p) = 0) (i j : Fin (r + 1)) (hij : i < j) :

(HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) p = 0

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.sourceRowRoot_self_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)) (hp : (HigherHarmonicYoung.nullSubstitution hn) p ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (i : Fin (r + 1)) :

(HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.sourceRowRoot_upper_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)) (hp : (HigherHarmonicYoung.nullSubstitution hn) p ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (i j : Fin (r + 1)) (hij : i < j) :

(HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) p = 0

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.mem_ambientIsotropicHighestSubmodule_of_isotropic_positiveRootKernel {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hsupport : ∃ (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)), (HigherHarmonicYoung.nullSubstitution hn) p = f) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) f = 0) (hsourceCartan : ∀ (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)), (∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i i) p = ↑(lam i) • p) → (∀ (i j : Fin (r + 1)), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceRowRoot i j) p = 0) → (∀ (i j : Fin (r + 1)), i < j → (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i j) p = 0) → ∀ (i : Fin (r + 1)), (HigherHarmonicYoung.BideterminantHighestLine.sourceColumnRoot i i) p = ↑(lam i) • p) :

f ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.mem_ambientIsotropicHighestSubmodule_of_positiveRootKernel_and_support {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hsupport : ∃ (p : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)), (HigherHarmonicYoung.nullSubstitution hn) p = f) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) f = 0) :

f ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankHarmonicHoweHighestRigidity.mem_ambientIsotropicHighestSubmodule_of_positiveRootKernel_maximalCartan {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) f = 0) (hcartan : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan hn) f = ↑(2 * ∑ i : Fin (r + 1), lam i) • f) :

f ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler_apply {r n : ℕ} (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler✝ f = ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a a) f

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler_of_rowCartan {r n : ℕ} (lam : Fin (r + 1) → ℕ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hrow : ∀ (a : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a a) f = ↑(lam a) • f) :

MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler✝ f = ↑(∑ a : Fin (r + 1), lam a) • f

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler_X {r n : ℕ} (a : Fin (r + 1)) (t : Fin n) :

MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler✝ (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)

source

@[simp]

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

(MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect✝ h) f = ∑ a : Fin (r + 1), ∑ p : Fin (r + 1), HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicDerivative_X_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p b q : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) (MvPolynomial.X (HigherHarmonicYoung.variableIndex b (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h q))) = if a = b ∧ p = q then 1 else 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicDerivative_X_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p b q : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) (MvPolynomial.X (HigherHarmonicYoung.variableIndex b (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h q))) = if a = b ∧ p = q then MvPolynomial.C Complex.I else 0

source

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

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

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect_apply {r n : ℕ} (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect✝ f = ∑ a : Fin (r + 1), ∑ t : Fin n with 2 * (r + 1) ≤ ↑t, MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f

source

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

(MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect✝ h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) = HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p

source

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

(MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect✝ h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) = HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p * MvPolynomial.C Complex.I

source

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

(MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect✝ h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect_X {r n : ℕ} (a : Fin (r + 1)) (t : Fin n) :

MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect✝ (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = if 2 * (r + 1) ≤ ↑t then MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) else 0

source

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

(HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) = HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p - HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p

source

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

(HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) = -Complex.I • (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p + HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a p)

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect_eq_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hanti : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) :

(MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect✝ h) f = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect_eq_zero {r n : ℕ} (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hunused : ∀ (a : Fin (r + 1)) (t : Fin n), 2 * (r + 1) ≤ ↑t → (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f = 0) :

MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect✝ f = 0

source

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

2 • MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalYoungRowEuler✝ - HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h = 2 • MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.antiholomorphicEulerDefect✝ h + 2 • MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.unusedCoordinateEulerDefect✝

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestCartanEulerIdentity.totalAmbientCartan_eq_maximal_of_rowCartan_antiholomorphic_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hrow : ∀ (a : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a a) f = ↑(lam a) • f) (hanti : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) (hunused : ∀ (a : Fin (r + 1)) (t : Fin n), 2 * (r + 1) ≤ ↑t → (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f = 0) :

(HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) f = ↑(2 * ∑ a : Fin (r + 1), lam a) • f

source

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

(Matrix.of fun (a p : Fin (r + 1)) => HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p).det ≠ 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestUnusedDerivativeVanishing.isotropicMatrix_transpose_mulVec_injective {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin (r + 1) → MvPolynomial (Fin ((r + 1) * n)) ℂ) (hv : (Matrix.of fun (a p : Fin (r + 1)) => HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p).transpose.mulVec v = 0) :

v = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestUnusedDerivativeVanishing.isotropicMatrix_unusedDerivative_eq_zero_of_shortRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hantiholomorphic : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) (t : Fin n) (hshort : ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) f = 0) (p : Fin (r + 1)) :

∑ a : Fin (r + 1), HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestUnusedDerivativeVanishing.unused_pderiv_eq_zero_of_antiholomorphic_and_shortRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hantiholomorphic : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) (hshort : ∀ (p : Fin (r + 1)) (t : Fin n), 2 * (r + 1) ≤ ↑t → (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) f = 0) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestUnusedDerivativeVanishing.unused_pderiv_eq_zero_of_antiholomorphic_and_positiveRootKernel {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hantiholomorphic : ∀ (a p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) (hroot : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f = 0

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.mem_unusedAmbientCoordinates {r n : ℕ} (t : Fin n) :

t ∈ MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝ ↔ 2 * (r + 1) ≤ ↑t

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.shortRoot_unusedDerivative {r n : ℕ} (h : 2 * (r + 1) ≤ n) (b p : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.shortRoot_unusedDerivative_sum {r n : ℕ} (h : 2 * (r + 1) ≤ n) (b p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

∑ t ∈ MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝, (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) f) = ∑ t ∈ MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝, ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) f) - MvPolynomial.X (HigherHarmonicYoung.variableIndex a t) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)) - MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝.card • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.shortRoot_unusedDerivative_sum_eq_card_smul_of_rootKernel {r n : ℕ} (h : 2 * (r + 1) ≤ n) (b p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroot : ∀ (t : Fin n), 2 * (r + 1) ≤ ↑t → (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot h p t) f = 0) :

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h a p) f = (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) f - MvPolynomial.C Complex.I * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) f

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.antiholomorphicDerivative_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p))) f + MvPolynomial.C Complex.I * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))) f

source

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

Disjoint (Finset.image (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h) Finset.univ) (Finset.image (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h) Finset.univ)

source

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

{t : Fin n | ↑t < 2 * (r + 1)} = Finset.image (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h) Finset.univ ∪ Finset.image (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h) Finset.univ

source

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.sum_occupied_eq_even_odd {r n : ℕ} {A : Type u_1} [AddCommMonoid A] (h : 2 * (r + 1) ≤ n) (g : Fin n → A) :

∑ t : Fin n with ↑t < 2 * (r + 1), g t = ∑ p : Fin (r + 1), (g (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p) + g (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p))

source

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.sum_univ_eq_even_odd_add_unused {r n : ℕ} {A : Type u_1} [AddCommMonoid A] (h : 2 * (r + 1) ≤ n) (g : Fin n → A) :

∑ t : Fin n, g t = ∑ p : Fin (r + 1), (g (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p) + g (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p)) + ∑ t ∈ MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝, g t

source

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.occupiedMixedTrace_eq_holomorphic_antiholomorphic {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

source

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.complexTraceOperator_eq_isotropicDerivative_add_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

HigherHarmonicYoung.complexTraceOperator a b f = 2⁻¹ • ∑ p : Fin (r + 1), ((MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h a p) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f) + (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b p) f)) + ∑ t ∈ MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝, (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) f)

source

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.unusedMixedHessian_eq_neg_isotropicDerivative_of_traceFree {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (htrace : HigherHarmonicYoung.complexTraceOperator a b f = 0) :

∑ t ∈ MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝, (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) f) = -(2⁻¹ • ∑ p : Fin (r + 1), ((MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h a p) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f) + (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b p) f)))

source

theorem MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.unusedMixedHessian_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (a b : Fin (r + 1)) :

∑ t ∈ MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝, (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a t)) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b t)) f) = -(2⁻¹ • ∑ p : Fin (r + 1), ((MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h a p) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f) + (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b p) f)))

source

theorem MetricCodes.Spherical.HigherYoungAllRankAntiHolomorphicRootCommutators.complex_pderiv_commute {N : ℕ} (i j : Fin N) (f : MvPolynomial (Fin N) ℂ) :

(MvPolynomial.pderiv i) ((MvPolynomial.pderiv j) f) = (MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) f)

source

theorem MetricCodes.Spherical.HigherYoungAllRankAntiHolomorphicRootCommutators.pderiv_rowDerivation {r n : ℕ} (a i j : Fin (r + 1)) (k : Fin n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a k)) ((HigherHarmonicYoung.DeterminantVectors.rowDerivation i j) f) = (if a = i then (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex j k)) f else 0) + (HigherHarmonicYoung.DeterminantVectors.rowDerivation i j) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a k)) f)

source

theorem MetricCodes.Spherical.HigherYoungAllRankAntiHolomorphicRootCommutators.rowDerivation_antiholomorphicDerivative_commutator {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b c p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h c p) f) - (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h c p) ((HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) f) = if a = c then -(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f else 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankAntiHolomorphicRootCommutators.rowDerivation_antiholomorphicDerivative_matching {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f) - (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) f) = -(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

source

theorem MetricCodes.Spherical.HigherYoungAllRankShortRootAntiHolomorphicMixedTraceCancellation.occupiedRowEuler_eq_isotropicDerivatives {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b q : Fin (r + 1)) (g : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h q)) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h q))) g + MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h q)) * (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h q))) g = 2⁻¹ • (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a q * (MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b q) g + HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable h a q * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) g)

source

theorem MetricCodes.Spherical.HigherYoungAllRankShortRootAntiHolomorphicMixedTraceCancellation.rowDerivation_eq_isotropicDerivatives_add_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a b : Fin (r + 1)) (g : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicRootEnergyTraceRowCancellation.shortRoot_mixedRemainder_eq_neg_rowDerivation_add_isotropic_traces {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (b p : Fin (r + 1)) :

source

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

(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f) = (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)

source

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

(HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b s) f) - (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b s) ((HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) f) = if s = q then 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f else 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientDifferenceRootAntiHolomorphicDerivativeCommutator.ambientPositiveRoot_antiholomorphicDerivative_of_rootKernel {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q b : Fin (r + 1)) (_hpq : p ≠ q) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : (HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) f = 0) :

(HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f) = 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

source

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

(MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h a p) (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h i j) = if a = i ∧ p = j then 2 else 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.complexPolynomial_pderiv_commute {ι : Type u_1} (i j : ι) (f : MvPolynomial ι ℂ) :

(MvPolynomial.pderiv i) ((MvPolynomial.pderiv j) f) = (MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) f)

source

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

(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) ((MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b q) f) = (MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)

source

@[simp]

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

HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p p = 0

source

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

(HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f = ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a p * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a q) f - HigherHarmonicYoung.DeterminantVectors.isotropicVariable h a q * (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f)

source

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

(HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) ((MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b s) f) - (MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b s) ((HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f) = (if s = q then 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f else 0) - if s = p then 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f else 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.ambientSumPositiveRoot_holomorphicDerivative_commutator {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q b : Fin (r + 1)) (hpq : p ≠ q) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) ((MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b q) f) - (MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b q) ((HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f) = 2 • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

source

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootHolomorphicDerivativeCommutator.ambientSumPositiveRoot_holomorphicDerivative_of_rootKernel {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q b : Fin (r + 1)) (hpq : p ≠ q) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f = 0) :

source

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

HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q = -HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h q p

source

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootAllHighestHolomorphicEvaluation.ambientSumPositiveRoot_eq_zero_of_all_positive_root_highest {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (p q : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) f = 0

source

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootAllHighestHolomorphicEvaluation.ambientSumPositiveRoot_holomorphicDerivative_of_all_positive_root_highest {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (p q b : Fin (r + 1)) :

source

theorem MetricCodes.Spherical.HigherYoungAmbientSumRootAllHighestHolomorphicEvaluation.sum_ambientSumPositiveRoot_holomorphicDerivative_of_all_positive_root_highest {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (p b : Fin (r + 1)) :

∑ q : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot h p q) ((MetricCodes.Spherical.HigherYoungIsotropicComplexTraceDecomposition.holomorphicDerivative✝ h b q) f) = ↑(2 * r) • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

source

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

MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝.card = n - 2 * (r + 1)

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.two_le_card_unusedAmbientCoordinates {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) :

2 ≤ MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝.card

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.triangularResidual_eq_rowTail_add_columnTail {r : ℕ} (b p : Fin (r + 1)) :

2 * (r + 1) - 2 - ↑b - ↑p = r - ↑b + (r - ↑p)

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient_eq_tails {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) :

MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient✝ n lam mu b p = MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝.card + lam b + mu p + (r - ↑b) + (r - ↑p)

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.two_le_harmonicHighestTriangularCoefficient {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) :

2 ≤ MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient✝ n lam mu b p

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient_ne_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) :

MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient✝ n lam mu b p ≠ 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient_complex_ne_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) :

↑(MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient✝ n lam mu b p) ≠ 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestTriangularScalarBookkeeping.sum_ite_lt_scalar {r : ℕ} (b : Fin (r + 1)) (c : ℂ) :

(∑ a : Fin (r + 1), if a < b then c else 0) = ↑↑b * c

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestTriangularScalarBookkeeping.sum_ite_gt_scalar {r : ℕ} (p : Fin (r + 1)) (c : ℂ) :

(∑ q : Fin (r + 1), if p < q then c else 0) = ↑(r - ↑p) * c

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestTriangularScalarBookkeeping.sum_rowHighest_scalar {r : ℕ} (lam : Fin (r + 1) → ℕ) (b : Fin (r + 1)) :

(∑ a : Fin (r + 1), if a < b then -1 else if a = b then ↑(lam b) - 1 else 0) = ↑(lam b) - 1 - ↑↑b

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestTriangularScalarBookkeeping.sum_differenceHighest_scalar {r : ℕ} (mu : Fin (r + 1) → ℕ) (p : Fin (r + 1)) :

(∑ q : Fin (r + 1), if q < p then 0 else if q = p then ↑(2 * mu p) + 2 else 2) = ↑(2 * mu p) + 2 + 2 * ↑(r - ↑p)

source

theorem MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestTriangularScalarBookkeeping.harmonicHighestTriangularCoefficient_complex_eq {r n : ℕ} (lam mu : Fin (r + 1) → ℕ) (b p : Fin (r + 1)) :

↑(MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootCoercivity.harmonicHighestTriangularCoefficient✝ n lam mu b p) = ↑MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝.card + (↑(lam b) - 1 - ↑↑b) + 2⁻¹ * (↑(2 * mu p) + 2 + 2 * ↑(r - ↑p) + 2 * ↑r)

source

theorem MetricCodes.Spherical.HigherYoungAllRankAntiHolomorphicTriangularSums.rowDerivation_antiholomorphic_sum_of_later_rows {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (b p : Fin (r + 1)) (hrowLater : ∀ (a : Fin (r + 1)), b < a → (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f = 0) :

∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f) = (↑(lam b) - 1 - ↑↑b) • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

source

theorem MetricCodes.Spherical.HigherYoungAllRankActualHighestCasimirRigidity.ambientPositiveRoot_antiholomorphic_sum_of_earlier_columns {r n : ℕ} (h : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℕ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (hcartan : ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) f = ↑(2 * mu p) • f) (b p : Fin (r + 1)) (hcolEarlier : ∀ q < p, (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f = 0) :

∑ q : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f) = (↑(2 * mu p) + 2 + 2 * ↑(r - ↑p)) • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f

source

theorem MetricCodes.Spherical.HigherYoungFiniteDescendingAscendingInduction.fin_descending_ascending_induction {m : ℕ} {P : Fin m → Fin m → Prop} (hstep : ∀ (b p : Fin m), (∀ (a : Fin m), b < a → ∀ (q : Fin m), P a q) → (∀ q < p, P b q) → P b p) (b p : Fin m) :

P b p

source

theorem MetricCodes.Spherical.HigherYoungAllRankActualHighestAntiHolomorphicRecurrence.harmonicHighestRoot_antiholomorphic_operator_recurrence {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (b p : Fin (r + 1)) :

↑(MetricCodes.Spherical.HigherYoungAllRankHarmonicHighestRootEnergyIdentity.unusedAmbientCoordinates✝.card + r) • (HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f + ∑ a : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.rowDerivation a b) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h a p) f) + 2⁻¹ • ∑ q : Fin (r + 1), (HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p q) ((HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b q) f) = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankActualHighestAntiHolomorphicRecurrence.antiholomorphicDerivative_eq_zero_of_positiveRootKernel_nonnegativeCartan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (hstable : 2 * (r + 1) + 2 ≤ n) (lam mu : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hroots : ∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f = 0) (hcartan : ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) f = ↑(2 * mu p) • f) (b p : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative h b p) f = 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.complexAmbientCoordinateDerivation_X {r n : ℕ} (a b : Fin n) (i : Fin (r + 1)) (k : Fin n) :

(HigherYoungTwoRowLieIrreducibility.complexAmbientCoordinateDerivation a b) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i k)) = if b = k then MvPolynomial.X (HigherHarmonicYoung.variableIndex i a) else 0

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.complexAmbientRotation_X {r n : ℕ} (a b : Fin n) (i : Fin (r + 1)) (k : Fin n) :

(HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a b) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i k)) = (if b = k then MvPolynomial.X (HigherHarmonicYoung.variableIndex i a) else 0) - if a = k then MvPolynomial.X (HigherHarmonicYoung.variableIndex i b) else 0

source

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.complexAmbientRotation_commutator_same_right {r n : ℕ} (a b t : Fin n) (hab : a ≠ b) (hat : a ≠ t) (hbt : b ≠ t) :

⁅HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a t, HigherYoungTwoRowLieIrreducibility.complexAmbientRotation b t⁆ = HigherYoungTwoRowLieIrreducibility.complexAmbientRotation b a

source

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.ambientShortPositiveRoot_negative_commutator {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

⁅HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot hn p t, MetricCodes.Spherical.HigherYoungAllRankShortNegativeRootNilpotence.ambientShortNegativeRoot✝ hn p t⁆ = HigherHarmonicYoung.DeterminantVectors.ambientCartan hn p

source

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.ambientShortPositiveRoot_youngComplexPair {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1)) (t : Fin n) (u v : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

source

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.ambientShortNegativeRoot_youngComplexPair {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1)) (t : Fin n) (u v : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

source

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.shortRootYoungPair_inner_adjoint {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1)) (t : Fin n) (u v x y : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

source

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.shortRootHighest_signedWeight_nonnegative {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hfzero : f ≠ 0) (p : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) (hroot : (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot hn p t) f = 0) (mu : ℤ) (hcartan : (HigherHarmonicYoung.DeterminantVectors.ambientCartan hn p) f = (2 * ↑mu) • f) :

0 ≤ mu

source

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.positiveRootHighest_signedWeight_nonnegative {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (hstrict : 2 * (r + 1) < n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (hfzero : f ≠ 0) (mu : Fin (r + 1) → ℤ) (hroot : ∀ (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn alpha) f = 0) (hcartan : ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientCartan hn p) f = (2 * ↑(mu p)) • f) (p : Fin (r + 1)) :

0 ≤ mu p

source

theorem MetricCodes.Spherical.HigherYoungAllRankHighestShortRootWeightNonnegative.positiveRootHighest_exists_naturalCartanEigenvalues {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (hstrict : 2 * (r + 1) < n) (lam : Fin (r + 1) → ℕ) {f : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (mu : Fin (r + 1) → ℤ) (hroot : ∀ (alpha : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn alpha) f = 0) (hcartan : ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientCartan hn p) f = (2 * ↑(mu p)) • f) :

∃ (nu : Fin (r + 1) → ℕ), ∀ (p : Fin (r + 1)), (HigherHarmonicYoung.DeterminantVectors.ambientCartan hn p) f = ↑(2 * nu p) • f

source

@[simp]

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

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight✝ (variableIndex a (DeterminantVectors.evenCoordinate h p)) = Pi.single p 1

source

@[simp]

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

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight✝ (variableIndex a (DeterminantVectors.oddCoordinate h p)) = Pi.single p (-1)

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight_unused {r n : ℕ} (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight✝ (variableIndex a t) = 0

source

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.coeff_isotropicInverse_ambientSignedWeightComponent {r n : ℕ} (h : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℤ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : Fin ((r + 1) * n) →₀ ℕ) :

MvPolynomial.coeff d ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h).symm (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent✝ h mu f)) = if (Finsupp.weight MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight✝) d = mu then MvPolynomial.coeff d ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h).symm f) else 0

source

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

(HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) (HigherYoungAmbientRootNilpotence.isotropicCoordinateGenerator h v) = (2 * ↑(MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight✝ v p)) • HigherYoungAmbientRootNilpotence.isotropicCoordinateGenerator h v

source

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation_X {ι : Type u_1} {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) (i : ι) :

(MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation✝ w p) (MvPolynomial.X i) = (2 * ↑(w i p)) • MvPolynomial.X i

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation_eq_sum {ι : Type u_1} [Fintype ι] {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) :

MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation✝ w p = ∑ i : ι, (2 * ↑(w i p)) • MvPolynomial.X i • MvPolynomial.pderiv i

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation_apply {ι : Type u_1} [Fintype ι] {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) (q : MvPolynomial ι ℂ) :

(MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation✝ w p) q = ∑ i : ι, (2 * ↑(w i p)) • (MvPolynomial.X i * (MvPolynomial.pderiv i) q)

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedWeight_apply {ι : Type u_1} [Fintype ι] {m : ℕ} (w : ι → Fin m → ℤ) (d : ι →₀ ℕ) (p : Fin m) :

(Finsupp.weight w) d p = ∑ i : ι, ↑(d i) * w i p

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.coeff_signedDiagonalDerivation {ι : Type u_1} [Finite ι] {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) (q : MvPolynomial ι ℂ) (d : ι →₀ ℕ) :

MvPolynomial.coeff d ((MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation✝ w p) q) = 2 * ↑((Finsupp.weight w) d p) * MvPolynomial.coeff d q

source

theorem MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonal_weightedHomogeneousComponent {ι : Type u_1} [Finite ι] {m : ℕ} (w : ι → Fin m → ℤ) (p : Fin m) (mu : Fin m → ℤ) (q : MvPolynomial ι ℂ) :

(MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation✝ w p) ((MvPolynomial.weightedHomogeneousComponent w mu) q) = (2 * ↑(mu p)) • (MvPolynomial.weightedHomogeneousComponent w mu) q

source

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

HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation (HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) (HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) = MetricCodes.Spherical.HigherYoungArbitraryRankSignedDiagonalDerivation.signedDiagonalDerivation✝ MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedVariableWeight✝ p

source

theorem MetricCodes.Spherical.HigherYoungAllRankActualSignedWeightCartanEigen.ambientCartan_ambientSignedWeightComponent {r n : ℕ} (h : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℤ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (p : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.ambientCartan h p) (MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent✝ h mu f) = (2 * ↑(mu p)) • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent✝ h mu f

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightYoungPreservation.youngComplexPolynomialSpan_top_eq_full {r n : ℕ} (lam : Fin (r + 1) → ℕ) :

HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam ⊤ = HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam

source

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightYoungPreservation.ambientCartan_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) :

(DeterminantVectors.ambientCartan h p) f ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam

source

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightYoungPreservation.ambientSignedWeightSupport {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

Finset (Fin (r + 1) → ℤ)

The ambient signed weight support 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.ArbitraryRankAmbientSignedWeightYoungPreservation.ambientSignedWeightComponent_eq_zero_of_not_mem_support {r n : ℕ} (h : 2 * (r + 1) ≤ n) (mu : Fin (r + 1) → ℤ) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hmu : mu ∉ ambientSignedWeightSupport h f) :

MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent✝ h mu f = 0

source

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

∑ mu ∈ ambientSignedWeightSupport h f, MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankAmbientSignedWeightProjection.ambientSignedWeightComponent✝ h mu f = f

source

theorem MetricCodes.Spherical.HigherYoungFiniteJointWeightProjectorInvariant.jointEigenComponent_mem_of_invariant_sum {K : Type u_1} {V : Type u_2} {α : Type u_3} {ι : Type u_4} [Field K] [AddCommGroup V] [Module K V] (T : ι → V →ₗ[K] V) (W : Submodule K V) (hW : ∀ (i : ι), ∀ x ∈ W, (T i) x ∈ W) (S : Finset α) (v : α → V) (eigen : α → ι → K) (heigen : ∀ a ∈ S, ∀ (i : ι), (T i) (v a) = eigen a i • v a) (hseparated : ∀ a ∈ S, ∀ b ∈ S, a ≠ b → ∃ (i : ι), eigen a i ≠ eigen b i) (hsum : ∑ a ∈ S, v a ∈ W) (a : α) (ha : a ∈ S) :

v a ∈ W

source