Weyl and root-complex identities

Euler groupings, orthogonal denominator formulas, and all-rank Weyl evaluations.

theorem MetricCodes.Spherical.HigherYoungRootFamilyEulerGrouping.sum_card_grade_eq_signed_subtype_sum {α : Type u_1} [Fintype α] (P : Finset α → Prop) [DecidablePred P] (F : Finset α → ℤ) : ∑ k ∈ Finset.range (Fintype.card α + 1), (-1) ^ k * ∑ S : { S : Finset α // S.card = k ∧ P S }, F ↑S = ∑ S : Finset α, (-1) ^ S.card * if P S then F S else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootExteriorEulerCharacteristic_eq_rootFamilyEulerCharacteristic {r n : ℕ} (lam : Fin (r + 1) → ℕ) : rootExteriorEulerCharacteristic n lam = rootFamilyEulerCharacteristic n lam

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorRootEdgeAdjoint {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) : JointHarmonicWeightSpace n (rootWedgeWeight lam T) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleInsert lam T α hα hadm))

The adjoint root operator along an admissible wedge insertion, with its weight spaces identified.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorRootEdgeAdjoint_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) (q : JointHarmonicWeightSpace n (rootWedgeWeight lam T)) : ↑↑((weightedExteriorRootEdgeAdjoint n lam T α hα hadm) q) = (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑q

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorRootEdge_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleInsert lam T α hα hadm))) : ↑↑((weightedExteriorRootEdge n lam T α hα hadm) p) = (polarization r n (positiveRootSecond α) (positiveRootFirst α)) ↑↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorRootEdge_fischer_adjoint {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleInsert lam T α hα hadm))) (q : JointHarmonicWeightSpace n (rootWedgeWeight lam T)) : inner ℝ ((weightedExteriorRootEdge n lam T α hα hadm) p) q = inner ℝ p ((weightedExteriorRootEdgeAdjoint n lam T α hα hadm) q)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorRootEdgeAdjointAt {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) (S : AdmissibleRootWedge lam (k + 1)) (hS : rootAdmissibleInsert lam T α hα hadm = S) : JointHarmonicWeightSpace n (rootWedgeWeight lam T) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

Transport the adjoint insertion-edge operator to a specified equal target wedge.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionCoboundary {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam k →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)

The weighted exterior action coboundary used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionCoboundary_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (q : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam (k + 1)) : (weightedExteriorActionCoboundary n lam k) q S = ∑ T : AdmissibleRootWedge lam k, ∑ α : PositiveRoot r, if hα : α ∈ ↑↑T then 0 else if hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i then if hS : rootAdmissibleInsert lam T α hα hadm = S then realExteriorRootSign (insert α ↑↑T) α • (weightedExteriorRootEdgeAdjointAt n lam T α hα hadm S hS) (q T) else 0 else 0

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleErase {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (α : PositiveRoot r) (hα : α ∈ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i) : AdmissibleRootWedge lam k

Erase a root from an admissible wedge when the resulting signed weight remains nonnegative.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleErase lam S α hα hadm = ⟨⟨(↑↑S).erase α, ⋯⟩, hadm⟩

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleErase_val {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (α : PositiveRoot r) (hα : α ∈ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i) : ↑↑(rootAdmissibleErase lam S α hα hadm) = (↑↑S).erase α

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_mem_of_eq {r k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) (S : AdmissibleRootWedge lam (k + 1)) (hS : rootAdmissibleInsert lam T α hα hadm = S) : α ∈ ↑↑S

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_erase_nonneg_of_eq {r k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) (S : AdmissibleRootWedge lam (k + 1)) (hS : rootAdmissibleInsert lam T α hα hadm = S) (i : Fin (r + 1)) : 0 ≤ signedRootWeight lam ((↑↑S).erase α) i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_eq_iff_erase {r k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) (S : AdmissibleRootWedge lam (k + 1)) (hαS : α ∈ ↑↑S) (herase : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i) : rootAdmissibleInsert lam T α hα hadm = S ↔ T = rootAdmissibleErase lam S α hαS herase

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorRootEdgeAdjointAt_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) (S : AdmissibleRootWedge lam (k + 1)) (hS : rootAdmissibleInsert lam T α hα hadm = S) (q : JointHarmonicWeightSpace n (rootWedgeWeight lam T)) : ↑↑((weightedExteriorRootEdgeAdjointAt n lam T α hα hadm S hS) q) = (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑q

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorRootEdgeAdjointErase {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (α : PositiveRoot r) (hα : α ∈ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i) : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleErase lam S α hα hadm)) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

The adjoint insertion-edge operator viewed from the wedge with one root erased back to the original wedge.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorRootEdgeAdjointErase_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (α : PositiveRoot r) (hα : α ∈ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i) (q : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleErase lam S α hα hadm))) : ↑↑((weightedExteriorRootEdgeAdjointErase n lam S α hα hadm) q) = (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑q

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionCoboundary_apply_erase {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (q : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam (k + 1)) : (weightedExteriorActionCoboundary n lam k) q S = ∑ α : PositiveRoot r, if hα : α ∈ ↑↑S then if hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i then realExteriorRootSign (↑↑S) α • (weightedExteriorRootEdgeAdjointErase n lam S α hα hadm) (q (rootAdmissibleErase lam S α hα hadm)) else 0 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionDifferential_fischer_adjoint {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam (k + 1)) (q : RootJointHarmonicChain n lam k) : inner ℝ ((weightedExteriorActionDifferential n lam k) p) q = inner ℝ p ((weightedExteriorActionCoboundary n lam k) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionCoboundary_apply_erase_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (q : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam (k + 1)) : ↑↑((weightedExteriorActionCoboundary n lam k) q S) = ∑ α : PositiveRoot r, if hα : α ∈ ↑↑S then if hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i then realExteriorRootSign (↑↑S) α • (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑(q (rootAdmissibleErase lam S α hα hadm)) else 0 else 0

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activeAdmissibleRootWedge {r : ℕ} (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) : AdmissibleRootWedge lam 1

The admissible singleton wedge associated with an active positive root.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activeAdmissibleRootWedge lam α = ⟨MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeSingleton ↑α, ⋯⟩

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activeAdmissibleRootWedge_val {r : ℕ} (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) : ↑↑(activeAdmissibleRootWedge lam α) = {↑α}

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicDegreeZeroEquiv_coe {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam 0) : ↑↑((rootJointHarmonicDegreeZeroEquiv n lam) p) = ↑↑(p (emptyAdmissibleRootWedge lam))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionCoboundary_degreeZero_active_coe {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam 0) (α : ActivePositiveRoot lam) : ↑↑((weightedExteriorActionCoboundary n lam 0) p (activeAdmissibleRootWedge lam α)) = (polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ↑↑((rootJointHarmonicDegreeZeroEquiv n lam) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionCoboundary_degreeZero_eq_zero_iff {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam 0) : (weightedExteriorActionCoboundary n lam 0) p = 0 ↔ (rootDegreeZeroPositiveCochain n lam) p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.ker_weightedExteriorActionCoboundary_degreeZero {r n : ℕ} (lam : Fin (r + 1) → ℕ) : (weightedExteriorActionCoboundary n lam 0).ker = (rootDegreeZeroPositiveCochain n lam).ker

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroPositiveCochain_finrank_ker_add_finrank_ce_range {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Module.finrank ℝ ↥(rootDegreeZeroPositiveCochain n lam).ker + Module.finrank ℝ ↥(weightedChevalleyEilenbergDifferential n lam 0).range = Module.finrank ℝ (RootJointHarmonicChain n lam 0)

def MetricCodes.Spherical.HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient (n : ℕ) (k : ℤ) : ℤ

The orthogonal complete symmetric coefficient used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n k = if 0 ≤ k then ↑((n + k.toNat - 1).choose k.toNat) else 0

def MetricCodes.Spherical.HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Matrix (Fin (r + 1)) (Fin (r + 1)) ℤ

The orthogonal jacobi trudi matrix used in the spherical-code argument.

Equations

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

def MetricCodes.Spherical.HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ℤ

The orthogonal jacobi trudi dimension used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n lam = (MetricCodes.Spherical.HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).det

@[simp]

theorem MetricCodes.Spherical.HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient_nat (n k : ℕ) : orthogonalCompleteSymmetricCoefficient n ↑k = ↑((n + k - 1).choose k)

@[simp]

theorem MetricCodes.Spherical.HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient_of_neg (n : ℕ) {k : ℤ} (hk : k < 0) : orthogonalCompleteSymmetricCoefficient n k = 0

noncomputable def MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.weylTargetExponent {r : ℕ} (lam : Fin (r + 1) → ℕ) : Fin (r + 1) →₀ ℕ

The exponent vector lam i + r - i used for the target Weyl coefficient.

Equations

• MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.weylTargetExponent lam = Finsupp.equivFunOnFinite.symm fun (i : Fin (r + 1)) => lam i + r - ↑i

@[simp]

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.weylTargetExponent_apply {r : ℕ} (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : (weylTargetExponent lam) i = lam i + r - ↑i

noncomputable def MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.reversePermutationExponent {r : ℕ} (σ : Equiv.Perm (Fin (r + 1))) : Fin (r + 1) →₀ ℕ

The reversed staircase exponent vector permuted by σ.

Equations

• MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.reversePermutationExponent σ = Finsupp.equivFunOnFinite.symm fun (i : Fin (r + 1)) => r - ↑(σ i)

@[simp]

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.reversePermutationExponent_apply {r : ℕ} (σ : Equiv.Perm (Fin (r + 1))) (i : Fin (r + 1)) : (reversePermutationExponent σ) i = r - ↑(σ i)

noncomputable def MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.boundedExponent {r B : ℕ} (d : Fin (r + 1) → Fin (B + 1)) : Fin (r + 1) →₀ ℕ

Convert bounded finite coordinates to a finitely supported natural exponent vector.

Equations

• MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.boundedExponent d = Finsupp.equivFunOnFinite.symm fun (i : Fin (r + 1)) => ↑(d i)

@[simp]

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.boundedExponent_apply {r B : ℕ} (d : Fin (r + 1) → Fin (B + 1)) (i : Fin (r + 1)) : (boundedExponent d) i = ↑(d i)

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.boundedExponent_injective {r B : ℕ} : Function.Injective boundedExponent

noncomputable def MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.ambientBinomialPolynomial {r : ℕ} (n B : ℕ) : MvPolynomial (Fin (r + 1)) ℤ

The polynomial of coordinatewise bounded exponents with coefficients given by products of ambient binomial dimensions.

Equations

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

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.coeff_ambientBinomialPolynomial_of_le {r n B : ℕ} (m : Fin (r + 1) →₀ ℕ) (hm : ∀ (i : Fin (r + 1)), m i ≤ B) : (ambientBinomialPolynomial n B).coeff m = ∏ i : Fin (r + 1), ↑((n + m i - 1).choose (m i))

noncomputable def MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramPairExponent {r : ℕ} (z : HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.UpperGramPair r) : Fin (r + 1) →₀ ℕ

The row-degree exponent vector of one Gram pair, counting each of its two coordinates.

Equations

• MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramPairExponent z = (fun₀ | (↑z).1 => 1) + fun₀ | (↑z).2 => 1

@[simp]

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramPairExponent_apply {r : ℕ} (z : HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.UpperGramPair r) (i : Fin (r + 1)) : (gramPairExponent z) i = HigherHarmonicYoung.gramPairRowDegree z i

noncomputable def MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramFamilyExponent {r : ℕ} (s : Finset (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.UpperGramPair r)) : Fin (r + 1) →₀ ℕ

The sum of the row-degree exponent vectors of a finite family of Gram pairs.

Equations

• MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramFamilyExponent s = ∑ z ∈ s, MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramPairExponent z

@[simp]

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramFamilyExponent_apply {r : ℕ} (s : Finset (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.UpperGramPair r)) (i : Fin (r + 1)) : (gramFamilyExponent s) i = HigherHarmonicYoung.gramFamilyRowDegree s i

noncomputable def MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramEquationPolynomial (r : ℕ) : MvPolynomial (Fin (r + 1)) ℤ

The product of 1 - Xᵢ * Xⱼ over the upper Gram pairs.

Equations

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

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramPairMonomial {r : ℕ} (z : HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.UpperGramPair r) : MvPolynomial.X (↑z).1 * MvPolynomial.X (↑z).2 = (MvPolynomial.monomial (gramPairExponent z)) 1

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramFamilyMonomial {r : ℕ} (s : Finset (HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.UpperGramPair r)) : ∏ z ∈ s, MvPolynomial.X (↑z).1 * MvPolynomial.X (↑z).2 = (MvPolynomial.monomial (gramFamilyExponent s)) 1

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.gramEquationPolynomial_eq_sum (r : ℕ) : gramEquationPolynomial r = ∑ s ∈ Finset.univ.powerset, (MvPolynomial.monomial (gramFamilyExponent s)) ((-1) ^ s.card)

theorem MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.coeff_ambientBinomialPolynomial_mul_gramEquationPolynomial {r n B : ℕ} (m : Fin (r + 1) →₀ ℕ) (hm : ∀ (i : Fin (r + 1)), m i ≤ B) : (ambientBinomialPolynomial n B * gramEquationPolynomial r).coeff m = HigherHarmonicYoung.fullGramKoszulCoefficient n fun (i : Fin (r + 1)) => m i

noncomputable def MetricCodes.Spherical.HigherWeylReversedAlternantCoefficient.reversedWeylPolynomial (r : ℕ) : MvPolynomial (Fin (r + 1)) ℤ

The determinant alternant whose columns have powers in descending order from r to zero.

Equations

• MetricCodes.Spherical.HigherWeylReversedAlternantCoefficient.reversedWeylPolynomial r = (Matrix.of fun (i j : Fin (r + 1)) => MvPolynomial.X i ^ (r - ↑j)).det

theorem MetricCodes.Spherical.HigherWeylReversedAlternantCoefficient.reversePermutationMonomial {r : ℕ} (σ : Equiv.Perm (Fin (r + 1))) : ∏ i : Fin (r + 1), MvPolynomial.X i ^ (r - ↑(σ i)) = (MvPolynomial.monomial (HigherWeylGramAlternantCoefficient.reversePermutationExponent σ)) 1

theorem MetricCodes.Spherical.HigherWeylReversedAlternantCoefficient.reversedWeylPolynomial_eq_sum (r : ℕ) : reversedWeylPolynomial r = ∑ σ : Equiv.Perm (Fin (r + 1)), (MvPolynomial.monomial (HigherWeylGramAlternantCoefficient.reversePermutationExponent σ)) ↑(Equiv.Perm.sign σ)

theorem MetricCodes.Spherical.HigherWeylReversedAlternantCoefficient.reversePermutationExponent_le_weylTargetExponent_iff {r : ℕ} (lam : Fin (r + 1) → ℕ) (σ : Equiv.Perm (Fin (r + 1))) : HigherWeylGramAlternantCoefficient.reversePermutationExponent σ ≤ HigherWeylGramAlternantCoefficient.weylTargetExponent lam ↔ ∀ (i : Fin (r + 1)), 0 ≤ HigherHarmonicYoung.weylShift lam σ i

theorem MetricCodes.Spherical.HigherWeylReversedAlternantCoefficient.weylTargetExponent_sub_reversePermutationExponent_apply {r : ℕ} (lam : Fin (r + 1) → ℕ) (σ : Equiv.Perm (Fin (r + 1))) (hσ : HigherWeylGramAlternantCoefficient.reversePermutationExponent σ ≤ HigherWeylGramAlternantCoefficient.weylTargetExponent lam) (i : Fin (r + 1)) : (HigherWeylGramAlternantCoefficient.weylTargetExponent lam - HigherWeylGramAlternantCoefficient.reversePermutationExponent σ) i = (HigherHarmonicYoung.weylShift lam σ i).toNat

theorem MetricCodes.Spherical.HigherWeylReversedAlternantCoefficient.coeff_ambient_mul_gram_mul_reversedWeylPolynomial {r n B : ℕ} (lam : Fin (r + 1) → ℕ) (hB : ∀ (i : Fin (r + 1)), (HigherWeylGramAlternantCoefficient.weylTargetExponent lam) i ≤ B) : (HigherWeylGramAlternantCoefficient.ambientBinomialPolynomial n B * HigherWeylGramAlternantCoefficient.gramEquationPolynomial r * reversedWeylPolynomial r).coeff (HigherWeylGramAlternantCoefficient.weylTargetExponent lam) = HigherHarmonicYoung.alternatingGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherWeylQuadraticDeterminantCoefficient.coeff_ambientBinomialPolynomial_mul_monomial {r n B : ℕ} (m s : Fin (r + 1) →₀ ℕ) (hm : ∀ (i : Fin (r + 1)), m i ≤ B) : (HigherWeylGramAlternantCoefficient.ambientBinomialPolynomial n B * (MvPolynomial.monomial s) 1).coeff m = ∏ i : Fin (r + 1), HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑(m i) - ↑(s i))

theorem MetricCodes.Spherical.HigherWeylQuadraticDeterminantCoefficient.weylTargetExponent_sub_lowPower {r : ℕ} (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) : ↑((HigherWeylGramAlternantCoefficient.weylTargetExponent lam) i) - ↑(r - ↑j) = ↑(lam i) - ↑↑i + ↑↑j

theorem MetricCodes.Spherical.HigherWeylQuadraticDeterminantCoefficient.weylTargetExponent_sub_highPower {r : ℕ} (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) : ↑((HigherWeylGramAlternantCoefficient.weylTargetExponent lam) i) - ↑(r + ↑j + 2) = ↑(lam i) - ↑↑i - ↑↑j - 2

theorem MetricCodes.Spherical.HigherWeylQuadraticDeterminantCoefficient.coeff_ambientBinomialPolynomial_mul_axisDifferenceProduct {r n B : ℕ} (m : Fin (r + 1) →₀ ℕ) (hm : ∀ (i : Fin (r + 1)), m i ≤ B) (a b : Fin (r + 1) → ℕ) : (HigherWeylGramAlternantCoefficient.ambientBinomialPolynomial n B * ∏ i : Fin (r + 1), (MvPolynomial.X i ^ a i - MvPolynomial.X i ^ b i)).coeff m = ∏ i : Fin (r + 1), (HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑(m i) - ↑(a i)) - HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑(m i) - ↑(b i)))

theorem MetricCodes.Spherical.HigherWeylQuadraticDeterminantCoefficient.coeff_ambientBinomialPolynomial_mul_det_separable {r n B : ℕ} (m : Fin (r + 1) →₀ ℕ) (a b : Fin (r + 1) → Fin (r + 1) → ℕ) (hm : ∀ (i : Fin (r + 1)), m i ≤ B) : (HigherWeylGramAlternantCoefficient.ambientBinomialPolynomial n B * (Matrix.of fun (i j : Fin (r + 1)) => MvPolynomial.X i ^ a i j - MvPolynomial.X i ^ b i j).det).coeff m = (Matrix.of fun (i j : Fin (r + 1)) => HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑(m i) - ↑(a i j)) - HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑(m i) - ↑(b i j))).det

theorem MetricCodes.Spherical.HigherWeylQuadraticDeterminantCoefficient.coeff_ambientBinomialPolynomial_mul_orthogonalDenominator {r n B : ℕ} (lam : Fin (r + 1) → ℕ) (hB : ∀ (i : Fin (r + 1)), (HigherWeylGramAlternantCoefficient.weylTargetExponent lam) i ≤ B) : (HigherWeylGramAlternantCoefficient.ambientBinomialPolynomial n B * (Matrix.of fun (i j : Fin (r + 1)) => MvPolynomial.X i ^ (r - ↑j) - MvPolynomial.X i ^ (r + ↑j + 2)).det).coeff (HigherWeylGramAlternantCoefficient.weylTargetExponent lam) = HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n lam

theorem MetricCodes.Spherical.HigherWeylQuadraticDeterminantCoefficient.gramEquationPolynomial_eq_upperPairProduct (r : ℕ) : HigherWeylGramAlternantCoefficient.gramEquationPolynomial r = ∏ i : Fin (r + 1), ∏ j ≥ i, (1 - MvPolynomial.X i * MvPolynomial.X j)

theorem MetricCodes.Spherical.HigherWeylGramOrthogonalJacobiTrudi.alternatingGramKoszulCoefficient_eq_orthogonalJacobiTrudiDimension {r n : ℕ} (lam : Fin (r + 1) → ℕ) : HigherHarmonicYoung.alternatingGramKoszulCoefficient n lam = HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n lam

def MetricCodes.Spherical.HigherWeylGeneralRowNormalization.risingFactorProduct (M q : ℕ) : ℝ

The product of the q consecutive factors starting at M + 1, viewed as a real number.

Equations

• MetricCodes.Spherical.HigherWeylGeneralRowNormalization.risingFactorProduct M q = ∏ a ∈ Finset.range q, ↑(M + a + 1)

theorem MetricCodes.Spherical.HigherWeylGeneralRowNormalization.risingFactorProduct_eq_ascFactorial (M q : ℕ) : risingFactorProduct M q = ↑((M + 1).ascFactorial q)

theorem MetricCodes.Spherical.HigherWeylGeneralRowNormalization.risingFactorProduct_pos (M q : ℕ) : 0 < risingFactorProduct M q

theorem MetricCodes.Spherical.HigherWeylGeneralRowNormalization.factorial_mul_risingFactorProduct (M q : ℕ) : ↑M.factorial * risingFactorProduct M q = ↑(M + q).factorial

theorem MetricCodes.Spherical.HigherWeylGeneralRowNormalization.normalized_choose_rising (M k t q : ℕ) (ht : t ≤ q) : ↑((M + k + q).choose (k + t)) / risingFactorProduct (M + k) q / (↑((M + q).choose t) / risingFactorProduct M q) = ↑((M + k).choose k) / ↑((k + t).choose k)

theorem MetricCodes.Spherical.HigherWeylGeneralRowNormalization.normalized_choose_rising_with_linear (M k t q : ℕ) (ht : t ≤ q) (a b : ℝ) (hb : b ≠ 0) : ↑((M + k + q).choose (k + t)) * a / risingFactorProduct (M + k) q / (↑((M + q).choose t) * b / risingFactorProduct M q) = a / b * (↑((M + k).choose k) / ↑((k + t).choose k))

noncomputable def MetricCodes.Spherical.HigherWeylGeneralRowFactor.orthogonalRowScale {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : ℝ

The orthogonal row normalization combining its complete-symmetric coefficient, linear factor, and rising-factor denominator.

Equations

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

theorem MetricCodes.Spherical.HigherWeylGeneralRowFactor.baselineLinear_ne_zero {r n : ℕ} (hn : 2 * r + 4 ≤ n) (i : Fin (r + 1)) : ↑n - 2 * ↑(↑i + 1) ≠ 0

theorem MetricCodes.Spherical.HigherWeylGeneralRowFactor.orthogonalRowScale_div_zero_eq_rowFactor {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : orthogonalRowScale n lam i / orthogonalRowScale n (fun (x : Fin (r + 1)) => 0) i = HigherHierarchy.Weyl.rowFactor n lam i

theorem MetricCodes.Spherical.HigherWeylDescendingRowFactors.descendingFactorProduct_eq_risingFactorProduct (M q : ℕ) : ∏ a ∈ Finset.range q, (↑(M + q) - ↑a) = HigherWeylGeneralRowNormalization.risingFactorProduct M q

theorem MetricCodes.Spherical.HigherWeylDescendingRowFactors.descendingRowFactors_eq_risingFactorProduct {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : ∏ a ∈ Finset.range (2 * r + 2), (↑n + ↑(lam i) - ↑↑i + ↑r - 1 - ↑a) = HigherWeylGeneralRowNormalization.risingFactorProduct (HigherHierarchy.Weyl.tailLength n r i + lam i) (2 * r + 2)

theorem MetricCodes.Spherical.HigherWeylShiftedSquarePairNormalization.shifted_square_pair_ratio_eq_pairFactor {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) {i j : Fin (r + 1)} (hij : i < j) : ((↑(lam i) - ↑↑i) * (↑(lam i) - ↑↑i + ↑n - 2) - (↑(lam j) - ↑↑j) * (↑(lam j) - ↑↑j + ↑n - 2)) / (-↑↑i * (-↑↑i + ↑n - 2) - -↑↑j * (-↑↑j + ↑n - 2)) = HigherHierarchy.Weyl.pairFactor n lam i j

noncomputable def MetricCodes.Spherical.HigherWeylAllRankCommonInvariantPolynomial.commonInvariantPolynomial (n : ℝ) (r k : ℕ) : Polynomial ℝ

The monic product of k shifted linear factors in the common quadratic invariant.

Equations

• MetricCodes.Spherical.HigherWeylAllRankCommonInvariantPolynomial.commonInvariantPolynomial n r k = ∏ q ∈ Finset.range k, (Polynomial.X + Polynomial.C ((↑r - ↑q) * (n - ↑r - 2 + ↑q)))

theorem MetricCodes.Spherical.HigherWeylAllRankCommonInvariantPolynomial.commonInvariantPolynomial_natDegree (n : ℝ) (r k : ℕ) : (commonInvariantPolynomial n r k).natDegree = k

theorem MetricCodes.Spherical.HigherWeylAllRankCommonInvariantPolynomial.commonInvariantPolynomial_eval (n z : ℝ) (r k : ℕ) : Polynomial.eval (z * (z + n - 2)) (commonInvariantPolynomial n r k) = (∏ q ∈ Finset.range k, (z + ↑r - ↑q)) * ∏ q ∈ Finset.range k, (n + z - ↑r - 2 + ↑q)

theorem MetricCodes.Spherical.HigherWeylAllRankCommonInvariantPolynomial.commonInvariantPolynomial_mul_natDegree_le (n : ℝ) (r j : ℕ) (hj : j ≤ r) (p : Polynomial ℝ) (hp : p.natDegree ≤ j) : (commonInvariantPolynomial n r (r - j) * p).natDegree ≤ r

def MetricCodes.Spherical.HigherWeylMiddleProductClosedForm.middleProducts (n z : ℝ) : ℕ → ℝ × ℝ

The paired middle products generated by successively adjoining the two outer factors in each component.

Equations

• One or more equations did not get rendered due to their size.
• MetricCodes.Spherical.HigherWeylMiddleProductClosedForm.middleProducts n z 0 = ((n + z - 2) * (n + z - 1), (z - 1) * z)

def MetricCodes.Spherical.HigherWeylMiddleProductClosedForm.centeredProduct (x : ℝ) (j : ℕ) : ℝ

The product of consecutive factors from x + j down to x - j - 1.

Equations

• MetricCodes.Spherical.HigherWeylMiddleProductClosedForm.centeredProduct x j = ∏ s ∈ Finset.range (2 * j + 2), (x + ↑j - ↑s)

@[simp]

theorem MetricCodes.Spherical.HigherWeylMiddleProductClosedForm.centeredProduct_zero (x : ℝ) : centeredProduct x 0 = (x - 1) * x

theorem MetricCodes.Spherical.HigherWeylMiddleProductClosedForm.centeredProduct_succ (x : ℝ) (j : ℕ) : centeredProduct x (j + 1) = centeredProduct x j * ((x - ↑j - 2) * (x + ↑j + 1))

theorem MetricCodes.Spherical.HigherWeylMiddleProductClosedForm.middleProducts_fst_eq_centeredProduct (n z : ℝ) (j : ℕ) : (middleProducts n z j).1 = centeredProduct (n + z - 1) j

theorem MetricCodes.Spherical.HigherWeylMiddleProductClosedForm.middleProducts_snd_eq_centeredProduct (n z : ℝ) (j : ℕ) : (middleProducts n z j).2 = centeredProduct z j

theorem MetricCodes.Spherical.HigherWeylMiddleProductClosedForm.middleProducts_fst_eq_prod (n z : ℝ) (j : ℕ) : (middleProducts n z j).1 = ∏ s ∈ Finset.range (2 * j + 2), (n + z + ↑j - 1 - ↑s)

theorem MetricCodes.Spherical.HigherWeylMiddleProductClosedForm.middleProducts_snd_eq_prod (n z : ℝ) (j : ℕ) : (middleProducts n z j).2 = ∏ s ∈ Finset.range (2 * j + 2), (z + ↑j - ↑s)

theorem MetricCodes.Spherical.HigherWeylAllRankReflectedPrefixSuffixFactor.prod_prefix_suffix_sub_factor {R : Type u_1} [CommRing R] (f d : ℕ → R) (k m : ℕ) : (∏ q ∈ Finset.range k, f q) * ∏ q ∈ Finset.range (m + k), d (k + q) - (∏ q ∈ Finset.range (k + m), f q) * ∏ q ∈ Finset.range k, d (k + m + q) = ((∏ q ∈ Finset.range k, f q) * ∏ q ∈ Finset.range k, d (k + m + q)) * (∏ q ∈ Finset.range m, d (k + q) - ∏ q ∈ Finset.range m, f (k + q))

theorem MetricCodes.Spherical.HigherWeylAllRankReflectedPrefixSuffixFactor.orthogonal_reflected_prefix_suffix_factor (n z : ℝ) (r j : ℕ) (hj : j ≤ r) : (∏ q ∈ Finset.range (r - j), (z + ↑r - ↑q)) * ∏ q ∈ Finset.range (2 * r + 2 - (r - j)), (n + z + ↑r - 1 - ↑(r - j + q)) - (∏ q ∈ Finset.range (r + j + 2), (z + ↑r - ↑q)) * ∏ q ∈ Finset.range (2 * r + 2 - (r + j + 2)), (n + z + ↑r - 1 - ↑(r + j + 2 + q)) = ((∏ q ∈ Finset.range (r - j), (z + ↑r - ↑q)) * ∏ q ∈ Finset.range (r - j), (n + z - ↑r - 2 + ↑q)) * (∏ q ∈ Finset.range (2 * j + 2), (n + z + ↑j - 1 - ↑q) - ∏ q ∈ Finset.range (2 * j + 2), (z + ↑j - ↑q))

theorem MetricCodes.Spherical.HigherWeylAllRankReflectedPrefixSuffixFactor.orthogonal_reflected_prefix_suffix_eq_invariant_middle (n z : ℝ) (r j : ℕ) (hj : j ≤ r) : (∏ q ∈ Finset.range (r - j), (z + ↑r - ↑q)) * ∏ q ∈ Finset.range (2 * r + 2 - (r - j)), (n + z + ↑r - 1 - ↑(r - j + q)) - (∏ q ∈ Finset.range (r + j + 2), (z + ↑r - ↑q)) * ∏ q ∈ Finset.range (2 * r + 2 - (r + j + 2)), (n + z + ↑r - 1 - ↑(r + j + 2 + q)) = Polynomial.eval (z * (z + n - 2)) (HigherWeylAllRankCommonInvariantPolynomial.commonInvariantPolynomial n r (r - j)) * ((HigherWeylMiddleProductClosedForm.middleProducts n z j).1 - (HigherWeylMiddleProductClosedForm.middleProducts n z j).2)

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalCompleteSymmetricCoefficient_succ {n : ℕ} (hn : 0 < n) (k : ℤ) : (k + 1) * HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (k + 1) = (↑n + k) * HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n k

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalCompleteSymmetricCoefficient_descend {n : ℕ} (hn : 0 < n) (z : ℤ) (r k : ℕ) : (∏ q ∈ Finset.range k, (↑n + z + ↑r - 1 - ↑q)) * HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (z + ↑r - ↑k) = (∏ q ∈ Finset.range k, (z + ↑r - ↑q)) * HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (z + ↑r)

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalCompleteSymmetricCoefficient_descend_commonDenominator {n : ℕ} (hn : 0 < n) (z : ℤ) (r L k : ℕ) (hk : k ≤ L) : (∏ q ∈ Finset.range L, (↑n + z + ↑r - 1 - ↑q)) * HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (z + ↑r - ↑k) = (HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (z + ↑r) * ∏ q ∈ Finset.range k, (z + ↑r - ↑q)) * ∏ q ∈ Finset.range (L - k), (↑n + z + ↑r - 1 - ↑(k + q))

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalCompleteSymmetricCoefficient_descend_commonDenominator_sub {n : ℕ} (hn : 0 < n) (z : ℤ) (r L k₁ k₂ : ℕ) (hk₁ : k₁ ≤ L) (hk₂ : k₂ ≤ L) : (∏ q ∈ Finset.range L, (↑n + z + ↑r - 1 - ↑q)) * (HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (z + ↑r - ↑k₁) - HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (z + ↑r - ↑k₂)) = HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (z + ↑r) * ((∏ q ∈ Finset.range k₁, (z + ↑r - ↑q)) * ∏ q ∈ Finset.range (L - k₁), (↑n + z + ↑r - 1 - ↑(k₁ + q)) - (∏ q ∈ Finset.range k₂, (z + ↑r - ↑q)) * ∏ q ∈ Finset.range (L - k₂), (↑n + z + ↑r - 1 - ↑(k₂ + q)))

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalCompleteSymmetricCoefficient_reflected_commonDenominator {n : ℕ} (hn : 0 < n) (z : ℤ) (r j : ℕ) (hj : j ≤ r) : (∏ q ∈ Finset.range (2 * r + 2), (↑n + z + ↑r - 1 - ↑q)) * (HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (z + ↑j) - HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (z - ↑j - 2)) = HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (z + ↑r) * ((∏ q ∈ Finset.range (r - j), (z + ↑r - ↑q)) * ∏ q ∈ Finset.range (2 * r + 2 - (r - j)), (↑n + z + ↑r - 1 - ↑(r - j + q)) - (∏ q ∈ Finset.range (r + j + 2), (z + ↑r - ↑q)) * ∏ q ∈ Finset.range (2 * r + 2 - (r + j + 2)), (↑n + z + ↑r - 1 - ↑(r + j + 2 + q)))

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalJacobiTrudiDimension_zero {r n : ℕ} : (HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n fun (x : Fin (r + 1)) => 0) = 1

def MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.middlePolynomials (n : ℝ) : ℕ → Polynomial ℝ × Polynomial ℝ

The recursively coupled pair of polynomials used to express the middle-product sum and difference.

Equations

• One or more equations did not get rendered due to their size.
• MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.middlePolynomials n 0 = (Polynomial.C (n - 1), Polynomial.C 2 * Polynomial.X + Polynomial.C ((n - 2) * (n - 1)))

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.middleProducts_sub_add (n z : ℝ) (j : ℕ) : (HigherWeylMiddleProductClosedForm.middleProducts n z j).1 - (HigherWeylMiddleProductClosedForm.middleProducts n z j).2 = (2 * z + n - 2) * Polynomial.eval (z * (z + n - 2)) (middlePolynomials n j).1 ∧ (HigherWeylMiddleProductClosedForm.middleProducts n z j).1 + (HigherWeylMiddleProductClosedForm.middleProducts n z j).2 = Polynomial.eval (z * (z + n - 2)) (middlePolynomials n j).2

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.middlePolynomials_natDegree (n : ℝ) (j : ℕ) : (middlePolynomials n j).1.natDegree ≤ j ∧ (middlePolynomials n j).2.natDegree ≤ j + 1

noncomputable def MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalColumnPolynomial (n : ℝ) (r : ℕ) (j : Fin (r + 1)) : Polynomial ℝ

The column polynomial formed from the common invariant factor and the first middle polynomial.

Equations

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

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalColumnPolynomial_natDegree_le (n : ℝ) (r : ℕ) (j : Fin (r + 1)) : (orthogonalColumnPolynomial n r j).natDegree ≤ r

def MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.shiftedSquare {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : ℝ

The quadratic invariant z * (z + n - 2) at the shifted row weight z = lam i - i.

Equations

• MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.shiftedSquare n lam i = (↑(lam i) - ↑↑i) * (↑(lam i) - ↑↑i + ↑n - 2)

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.eval_matrixOfPolynomials_fixedRank {r : ℕ} (v : Fin (r + 1) → ℝ) (p : Fin (r + 1) → Polynomial ℝ) (hdegree : ∀ (j : Fin (r + 1)), (p j).natDegree ≤ r) : (Matrix.of fun (i j : Fin (r + 1)) => Polynomial.eval (v i) (p j)) = Matrix.vandermonde v * Matrix.of fun (i j : Fin (r + 1)) => (p j).coeff ↑i

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.det_shiftedSquare_evaluation_div_zero_of_degree_le {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1) → Polynomial ℝ) (hdegree : ∀ (j : Fin (r + 1)), (p j).natDegree ≤ r) (hzero : (Matrix.det fun (i j : Fin (r + 1)) => Polynomial.eval (shiftedSquare n (fun (x : Fin (r + 1)) => 0) i) (p j)) ≠ 0) : ((Matrix.det fun (i j : Fin (r + 1)) => Polynomial.eval (shiftedSquare n lam i) (p j)) / Matrix.det fun (i j : Fin (r + 1)) => Polynomial.eval (shiftedSquare n (fun (x : Fin (r + 1)) => 0) i) (p j)) = ∏ i : Fin (r + 1), ∏ j > i, HigherHierarchy.Weyl.pairFactor n lam i j

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.det_rowScaled_polynomial_evaluation {r : ℕ} (scale T : Fin (r + 1) → ℝ) (p : Fin (r + 1) → Polynomial ℝ) : (Matrix.det fun (i j : Fin (r + 1)) => scale i * Polynomial.eval (T i) (p j)) = (∏ i : Fin (r + 1), scale i) * Matrix.det fun (i j : Fin (r + 1)) => Polynomial.eval (T i) (p j)

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.polynomial_evaluation_det_ne_zero_of_rowScaled {r : ℕ} (scale T : Fin (r + 1) → ℝ) (p : Fin (r + 1) → Polynomial ℝ) (hdet : (Matrix.det fun (i j : Fin (r + 1)) => scale i * Polynomial.eval (T i) (p j)) ≠ 0) : (Matrix.det fun (i j : Fin (r + 1)) => Polynomial.eval (T i) (p j)) ≠ 0

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.det_rowScaled_shiftedSquare_evaluation_eq {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1) → Polynomial ℝ) (hdegree : ∀ (j : Fin (r + 1)), (p j).natDegree ≤ r) (scale scaleZero : Fin (r + 1) → ℝ) (hscaleZero : ∀ (i : Fin (r + 1)), scaleZero i ≠ 0) (hzero : (Matrix.det fun (i j : Fin (r + 1)) => scaleZero i * Polynomial.eval (shiftedSquare n (fun (x : Fin (r + 1)) => 0) i) (p j)) = 1) : (Matrix.det fun (i j : Fin (r + 1)) => scale i * Polynomial.eval (shiftedSquare n lam i) (p j)) = ((∏ i : Fin (r + 1), scale i) / ∏ i : Fin (r + 1), scaleZero i) * ∏ i : Fin (r + 1), ∏ j > i, HigherHierarchy.Weyl.pairFactor n lam i j

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.pairProduct_Ioi_eq_conditional {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ∏ i : Fin (r + 1), ∏ j > i, HigherHierarchy.Weyl.pairFactor n lam i j = ∏ i : Fin (r + 1), ∏ j : Fin (r + 1), if i < j then HigherHierarchy.Weyl.pairFactor n lam i j else 1

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.rowRatio_mul_pairProduct_eq_weyl_dimension {r n : ℕ} (lam : Fin (r + 1) → ℕ) (scale scaleZero : Fin (r + 1) → ℝ) (hrow : ∀ (i : Fin (r + 1)), scale i / scaleZero i = HigherHierarchy.Weyl.rowFactor n lam i) : ((∏ i : Fin (r + 1), scale i) / ∏ i : Fin (r + 1), scaleZero i) * ∏ i : Fin (r + 1), ∏ j > i, HigherHierarchy.Weyl.pairFactor n lam i j = HigherHierarchy.Weyl.dimension n lam

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalRowScale_zero_ne_zero {r n : ℕ} (hn : 2 * r + 4 ≤ n) (i : Fin (r + 1)) : HigherWeylGeneralRowFactor.orthogonalRowScale n (fun (x : Fin (r + 1)) => 0) i ≠ 0

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalJacobiTrudiDimension_eq_weyl_of_row_evaluation {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (p : Fin (r + 1) → Polynomial ℝ) (hdegree : ∀ (j : Fin (r + 1)), (p j).natDegree ≤ r) (hentry : ∀ (i j : Fin (r + 1)), ↑(HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam i j) = HigherWeylGeneralRowFactor.orthogonalRowScale n lam i * Polynomial.eval (shiftedSquare n lam i) (p j)) (hentryZero : ∀ (i j : Fin (r + 1)), ↑(HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n (fun (x : Fin (r + 1)) => 0) i j) = HigherWeylGeneralRowFactor.orthogonalRowScale n (fun (x : Fin (r + 1)) => 0) i * Polynomial.eval (shiftedSquare n (fun (x : Fin (r + 1)) => 0) i) (p j)) : ↑(HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n lam) = HigherHierarchy.Weyl.dimension n lam

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalJacobiTrudiMatrix_reflected_commonDenominator_real {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) : (∏ q ∈ Finset.range (2 * r + 2), (↑n + ↑(lam i) - ↑↑i + ↑r - 1 - ↑q)) * ↑(HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam i j) = ↑(HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n ↑(lam i + HigherHierarchy.Weyl.rowTail i)) * ((∏ q ∈ Finset.range (r - ↑j), (↑(lam i) - ↑↑i + ↑r - ↑q)) * ∏ q ∈ Finset.range (2 * r + 2 - (r - ↑j)), (↑n + ↑(lam i) - ↑↑i + ↑r - 1 - ↑(r - ↑j + q)) - (∏ q ∈ Finset.range (r + ↑j + 2), (↑(lam i) - ↑↑i + ↑r - ↑q)) * ∏ q ∈ Finset.range (2 * r + 2 - (r + ↑j + 2)), (↑n + ↑(lam i) - ↑↑i + ↑r - 1 - ↑(r + ↑j + 2 + q)))

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalJacobiTrudiMatrix_entry_of_factored_transport {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (hfact : (∏ a ∈ Finset.range (2 * r + 2), (↑n + ↑(lam i) - ↑↑i + ↑r - 1 - ↑a)) * ↑(HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam i j) = ↑(HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n ↑(lam i + HigherHierarchy.Weyl.rowTail i)) * (2 * ↑(lam i) + ↑n - 2 * ↑(↑i + 1)) * Polynomial.eval (shiftedSquare n lam i) (HigherWeylAllRankCommonInvariantPolynomial.commonInvariantPolynomial (↑n) r (r - ↑j) * (middlePolynomials ↑n ↑j).1)) : ↑(HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam i j) = HigherWeylGeneralRowFactor.orthogonalRowScale n lam i * Polynomial.eval (shiftedSquare n lam i) (HigherWeylAllRankCommonInvariantPolynomial.commonInvariantPolynomial (↑n) r (r - ↑j) * (middlePolynomials ↑n ↑j).1)

def MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalReflectedBracket (n z : ℝ) (r j : ℕ) : ℝ

The difference of the two reflected factorial products in an orthogonal determinant entry.

Equations

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

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalReflectedBracket_eq_commonPolynomial (n z : ℝ) (r j : ℕ) (hj : j ≤ r) : orthogonalReflectedBracket n z r j = Polynomial.eval (z * (z + n - 2)) (HigherWeylAllRankCommonInvariantPolynomial.commonInvariantPolynomial n r (r - j)) * ((HigherWeylMiddleProductClosedForm.middleProducts n z j).1 - (HigherWeylMiddleProductClosedForm.middleProducts n z j).2)

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalJacobiTrudiMatrix_entry_of_real_transport {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (htransport : (∏ a ∈ Finset.range (2 * r + 2), (↑n + ↑(lam i) - ↑↑i + ↑r - 1 - ↑a)) * ↑(HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam i j) = ↑(HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n ↑(lam i + HigherHierarchy.Weyl.rowTail i)) * orthogonalReflectedBracket (↑n) (↑(lam i) - ↑↑i) r ↑j) : ↑(HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam i j) = HigherWeylGeneralRowFactor.orthogonalRowScale n lam i * Polynomial.eval (shiftedSquare n lam i) (HigherWeylAllRankCommonInvariantPolynomial.commonInvariantPolynomial (↑n) r (r - ↑j) * (middlePolynomials ↑n ↑j).1)

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalJacobiTrudiMatrix_entry_eq_rowScale_columnPolynomial {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) : ↑(HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam i j) = HigherWeylGeneralRowFactor.orthogonalRowScale n lam i * Polynomial.eval (shiftedSquare n lam i) (orthogonalColumnPolynomial (↑n) r j)

theorem MetricCodes.Spherical.HigherWeylAllRankJacobiTrudiWeylEvaluation.orthogonalJacobiTrudiDimension_eq_weyl {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) : ↑(HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n lam) = HigherHierarchy.Weyl.dimension n lam

theorem MetricCodes.Spherical.HigherWeylAllRankAlternatingCharacter.weyl_dimension_eq_alternatingGramKoszulCoefficient {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) : HigherHierarchy.Weyl.dimension n lam = ↑(HigherHarmonicYoung.alternatingGramKoszulCoefficient n lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.weyl_dimension_eq_finrank_harmonicYoung_of_rootExact {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (d : (k : ℕ) → UniversalBGGRootComplex.RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] UniversalBGGRootComplex.RootJointHarmonicChain n lam k) (hexact : ∀ k < Fintype.card (UniversalBGGRootComplex.PositiveRoot r), (d (k + 1)).range = (d k).ker) (hzero : Module.finrank ℝ ↥(UniversalBGGRootComplex.rootDegreeZeroPositiveCochain n lam).ker + Module.finrank ℝ ↥(d 0).range = Module.finrank ℝ (UniversalBGGRootComplex.RootJointHarmonicChain n lam 0)) : HigherHierarchy.Weyl.dimension n lam = ↑(Module.finrank ℝ ↥(HarmonicYoungSpace lam))

theorem MetricCodes.Spherical.HigherHarmonicYoung.weyl_dimension_eq_finrank_harmonicYoung_of_chevalleyExact {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hexact : ∀ k < Fintype.card (UniversalBGGRootComplex.PositiveRoot r), (UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential n lam (k + 1)).range = (UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential n lam k).ker) (hzero : Module.finrank ℝ ↥(UniversalBGGRootComplex.rootDegreeZeroPositiveCochain n lam).ker + Module.finrank ℝ ↥(UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential n lam 0).range = Module.finrank ℝ (UniversalBGGRootComplex.RootJointHarmonicChain n lam 0)) : HigherHierarchy.Weyl.dimension n lam = ↑(Module.finrank ℝ ↥(HarmonicYoungSpace lam))

theorem MetricCodes.Spherical.HigherHarmonicYoung.weyl_dimension_eq_finrank_harmonicYoung_of_chevalleyExactness {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hexact : ∀ k < Fintype.card (UniversalBGGRootComplex.PositiveRoot r), (UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential n lam (k + 1)).range = (UniversalBGGRootComplex.weightedChevalleyEilenbergDifferential n lam k).ker) : HigherHierarchy.Weyl.dimension n lam = ↑(Module.finrank ℝ ↥(HarmonicYoungSpace lam))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionDifferential_apply_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam (k + 1)) (T : AdmissibleRootWedge lam k) : ↑↑((weightedExteriorActionDifferential n lam k) p T) = ∑ α : PositiveRoot r, if hα : α ∈ ↑↑T then 0 else if hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i then realExteriorRootSign (insert α ↑↑T) α • (polarization r n (positiveRootSecond α) (positiveRootFirst α)) ↑↑(p (rootAdmissibleInsert lam T α hα hadm)) else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootUpperOperator {r : ℕ} (n : ℕ) (α : PositiveRoot r) : PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The positive root upper operator used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootUpperOperator_apply {r n : ℕ} (α : PositiveRoot r) (p : PolynomialSpace r n) : (positiveRootUpperOperator n α) p = (polarization r n (positiveRootFirst α) (positiveRootSecond α)) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootUpper_lower_commutator_apply {r n : ℕ} (α β : PositiveRoot r) (p : PolynomialSpace r n) : (positiveRootUpperOperator n α) ((positiveRootOperator n β) p) - (positiveRootOperator n β) ((positiveRootUpperOperator n α) p) = (if positiveRootSecond α = positiveRootSecond β then (polarization r n (positiveRootFirst α) (positiveRootFirst β)) p else 0) - if positiveRootFirst β = positiveRootFirst α then (polarization r n (positiveRootSecond β) (positiveRootSecond α)) p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootUpper_lower_commutator {r n : ℕ} (α β : PositiveRoot r) : positiveRootUpperOperator n α ∘ₗ positiveRootOperator n β - positiveRootOperator n β ∘ₗ positiveRootUpperOperator n α = (if positiveRootSecond α = positiveRootSecond β then polarization r n (positiveRootFirst α) (positiveRootFirst β) else 0) - if positiveRootFirst β = positiveRootFirst α then polarization r n (positiveRootSecond β) (positiveRootSecond α) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRoot_sum_sub_smul {r : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℝ V] (f g : PositiveRoot r → ℝ) (v : PositiveRoot r → V) : ∑ γ : PositiveRoot r, (f γ - g γ) • v γ = ∑ γ : PositiveRoot r, f γ • v γ - ∑ γ : PositiveRoot r, g γ • v γ

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_upper_cross {r : ℕ} (α β γ : PositiveRoot r) : rootStructureConstant β γ α = (if positiveRootSecond α = positiveRootSecond β ∧ ↑γ = (positiveRootFirst α, positiveRootFirst β) then 1 else 0) - if positiveRootFirst α = positiveRootFirst β ∧ ↑γ = (positiveRootSecond β, positiveRootSecond α) then 1 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_lower_cross {r : ℕ} (α β γ : PositiveRoot r) : rootStructureConstant α γ β = (if positiveRootSecond α = positiveRootSecond β ∧ ↑γ = (positiveRootFirst β, positiveRootFirst α) then 1 else 0) - if positiveRootFirst α = positiveRootFirst β ∧ ↑γ = (positiveRootSecond α, positiveRootSecond β) then 1 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_positiveRootUpperOperator_eq_polarization_of_pair {r n : ℕ} (i j : Fin (r + 1)) : ∑ γ : PositiveRoot r, (if ↑γ = (i, j) then 1 else 0) • positiveRootUpperOperator n γ = if i < j then polarization r n i j else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_positiveRootOperator_eq_polarization_of_pair {r n : ℕ} (i j : Fin (r + 1)) : ∑ γ : PositiveRoot r, (if ↑γ = (i, j) then 1 else 0) • positiveRootOperator n γ = if i < j then polarization r n j i else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_upper_cross_sum {r n : ℕ} (α β : PositiveRoot r) : ∑ γ : PositiveRoot r, rootStructureConstant β γ α • positiveRootUpperOperator n γ = (if positiveRootSecond α = positiveRootSecond β ∧ positiveRootFirst α < positiveRootFirst β then polarization r n (positiveRootFirst α) (positiveRootFirst β) else 0) - if positiveRootFirst α = positiveRootFirst β ∧ positiveRootSecond β < positiveRootSecond α then polarization r n (positiveRootSecond β) (positiveRootSecond α) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_lower_cross_sum {r n : ℕ} (α β : PositiveRoot r) : ∑ γ : PositiveRoot r, rootStructureConstant α γ β • positiveRootOperator n γ = (if positiveRootSecond α = positiveRootSecond β ∧ positiveRootFirst β < positiveRootFirst α then polarization r n (positiveRootFirst α) (positiveRootFirst β) else 0) - if positiveRootFirst α = positiveRootFirst β ∧ positiveRootSecond α < positiveRootSecond β then polarization r n (positiveRootSecond β) (positiveRootSecond α) else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootCartanOperator {r : ℕ} (n : ℕ) (α : PositiveRoot r) : PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The difference of the diagonal row-polarization operators at the endpoints of a positive root.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootUpper_lower_commutator_eq_cartan_add_bracket {r n : ℕ} (α β : PositiveRoot r) : positiveRootUpperOperator n α ∘ₗ positiveRootOperator n β - positiveRootOperator n β ∘ₗ positiveRootUpperOperator n α = (if α = β then positiveRootCartanOperator n α else 0) + ∑ γ : PositiveRoot r, rootStructureConstant β γ α • positiveRootUpperOperator n γ + ∑ γ : PositiveRoot r, rootStructureConstant α γ β • positiveRootOperator n γ

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleSwap {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) : AdmissibleRootWedge lam k

The root admissible swap used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleSwap lam S α β hα hβ hadm = ⟨⟨insert β ((↑↑S).erase α), ⋯⟩, hadm⟩

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight_admissibleSwap {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (i : Fin (r + 1)) : signedRootWeight lam (↑↑(rootAdmissibleSwap lam S α β hα hβ hadm)) i = signedRootWeight lam (↑↑S) i - rootCharge α i + rootCharge β i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleSwap_upper_charge {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β γ : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hstructure : rootStructureConstant β γ α ≠ 0) (i : Fin (r + 1)) : ↑(rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm) i) + rootCharge γ i = ↑(rootWedgeWeight lam S i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleSwap_lower_charge {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β γ : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hstructure : rootStructureConstant α γ β ≠ 0) (i : Fin (r + 1)) : ↑(rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm) i) - rootCharge γ i = ↑(rootWedgeWeight lam S i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleSwap_upper_second_pos {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β γ : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hstructure : rootStructureConstant β γ α ≠ 0) : 0 < rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm) (positiveRootSecond γ)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleSwap_lower_first_pos {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β γ : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hstructure : rootStructureConstant α γ β ≠ 0) : 0 < rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm) (positiveRootFirst γ)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionCoboundary_differential_apply_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) : ↑↑((weightedExteriorActionCoboundary n lam k) ((weightedExteriorActionDifferential n lam k) f) S) = ∑ α : PositiveRoot r, if hα : α ∈ ↑↑S then if herase : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i then ∑ β : PositiveRoot r, if hβ : β ∈ ↑↑(rootAdmissibleErase lam S α hα herase) then 0 else if hins : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ↑↑(rootAdmissibleErase lam S α hα herase)) i then (realExteriorRootSign (↑↑S) α * realExteriorRootSign (insert β ↑↑(rootAdmissibleErase lam S α hα herase)) β) • (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ((polarization r n (positiveRootSecond β) (positiveRootFirst β)) ↑↑(f (rootAdmissibleInsert lam (rootAdmissibleErase lam S α hα herase) β hβ hins))) else 0 else 0 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionDifferential_coboundary_apply_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) : ↑↑((weightedExteriorActionDifferential n lam (k + 1)) ((weightedExteriorActionCoboundary n lam (k + 1)) f) S) = ∑ β : PositiveRoot r, if hβ : β ∈ ↑↑S then 0 else if hins : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ↑↑S) i then ∑ α : PositiveRoot r, if hα : α ∈ ↑↑(rootAdmissibleInsert lam S β hβ hins) then if herase : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑(rootAdmissibleInsert lam S β hβ hins)).erase α) i then (realExteriorRootSign (insert β ↑↑S) β * realExteriorRootSign (↑↑(rootAdmissibleInsert lam S β hβ hins)) α) • (polarization r n (positiveRootSecond β) (positiveRootFirst β)) ((polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑(f (rootAdmissibleErase lam (rootAdmissibleInsert lam S β hβ hins) α hα herase))) else 0 else 0 else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionCoboundaryDifferentialIncidence {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) (α β : PositiveRoot r) : PolynomialSpace r n

The signed polynomial-action term obtained by erasing α and inserting β, or zero when either step is inadmissible.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionDifferentialCoboundaryIncidence {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) (β α : PositiveRoot r) : PolynomialSpace r n

The signed polynomial-action term obtained by inserting β and erasing α, or zero when either step is inadmissible.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionCoboundary_differential_apply_coe_eq_incidence_sum {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) : ↑↑((weightedExteriorActionCoboundary n lam k) ((weightedExteriorActionDifferential n lam k) f) S) = ∑ α : PositiveRoot r, ∑ β : PositiveRoot r, rootPolynomialActionCoboundaryDifferentialIncidence lam f S α β

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionDifferential_coboundary_apply_coe_eq_incidence_sum {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) : ↑↑((weightedExteriorActionDifferential n lam (k + 1)) ((weightedExteriorActionCoboundary n lam (k + 1)) f) S) = ∑ β : PositiveRoot r, ∑ α : PositiveRoot r, rootPolynomialActionDifferentialCoboundaryIncidence lam f S β α

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_rootIncidence_eq_diagonal_add_offDiagonal {ι : Type u_1} {M : Type u_2} [Fintype ι] [DecidableEq ι] [AddCommMonoid M] (F : ι → ι → M) : ∑ a : ι, ∑ b : ι, F a b = ∑ a : ι, F a a + ∑ a : ι, ∑ b : ι, if a = b then 0 else F a b

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_rootIncidence_pair_eq_diagonal_add_offDiagonal {ι : Type u_1} {M : Type u_2} [Fintype ι] [DecidableEq ι] [AddCommMonoid M] (F G : ι → ι → M) : ∑ a : ι, ∑ b : ι, F a b + ∑ b : ι, ∑ a : ι, G b a = ∑ a : ι, (F a a + G a a) + ∑ a : ι, ∑ b : ι, if a = b then 0 else F a b + G b a

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionHodgeDiagonalIncidence {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) : PolynomialSpace r n

The sum of the equal-root incidence terms in the polynomial-action Hodge operator.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionHodgeOffDiagonalIncidence {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) : PolynomialSpace r n

The sum of the distinct-root incidence terms in the polynomial-action Hodge operator.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionHodge_apply_coe_eq_diagonal_add_offDiagonal {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) : ↑↑((weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1)) f S) = rootPolynomialActionHodgeDiagonalIncidence lam f S + rootPolynomialActionHodgeOffDiagonalIncidence lam f S

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activeRootRaisedWeight_cast {r : ℕ} (μ : Fin (r + 1) → ℕ) (γ : ActivePositiveRoot μ) (i : Fin (r + 1)) : ↑(activeRootRaisedWeight μ γ i) = ↑(μ i) + rootCharge (↑γ) i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSwapUpperStructureEdge_weight {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β γ : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hstructure : rootStructureConstant β γ α ≠ 0) : activeRootRaisedWeight (rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm)) ⟨γ, ⋯⟩ = rootWedgeWeight lam S

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSwapLowerStructureEdge_weight {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β γ : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hstructure : rootStructureConstant α γ β ≠ 0) : lowerRootWeight (rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm)) γ = rootWedgeWeight lam S

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSwapUpperStructureEdge {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β γ : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hstructure : rootStructureConstant β γ α ≠ 0) : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm)) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

The root swap upper structure edge used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSwapLowerStructureEdge {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β γ : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hstructure : rootStructureConstant α γ β ≠ 0) : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm)) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

The lowering root operator from a swapped wedge's weight space back to the original weight space, using a nonzero structure constant.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSwapUpperStructureEdge_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β γ : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hstructure : rootStructureConstant β γ α ≠ 0) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm))) : ↑↑((rootSwapUpperStructureEdge n lam S α β γ hα hβ hadm hstructure) p) = (polarization r n (positiveRootFirst γ) (positiveRootSecond γ)) ↑↑p

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSwapLowerStructureEdge_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α β γ : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hstructure : rootStructureConstant α γ β ≠ 0) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm))) : ↑↑((rootSwapLowerStructureEdge n lam S α β γ hα hβ hadm hstructure) p) = (polarization r n (positiveRootSecond γ) (positiveRootFirst γ)) ↑↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_mul_rootCharge {r : ℕ} (u : Fin (r + 1) → ℤ) (α : PositiveRoot r) : ∑ i : Fin (r + 1), u i * rootCharge α i = u (positiveRootFirst α) - u (positiveRootSecond α)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_mul_rootFamilyCharge {r : ℕ} (u : Fin (r + 1) → ℤ) (S : Finset (PositiveRoot r)) : ∑ i : Fin (r + 1), u i * rootFamilyCharge S i = ∑ α ∈ S, (u (positiveRootFirst α) - u (positiveRootSecond α))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exists_rootFamilyCharge_ne_zero_of_nonempty {r : ℕ} (S : Finset (PositiveRoot r)) (hS : S.Nonempty) : ∃ (i : Fin (r + 1)), rootFamilyCharge S i ≠ 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_signedRootWeight_root_difference {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : Finset (PositiveRoot r)) : ∑ α ∈ S, (signedRootWeight lam S (positiveRootFirst α) - signedRootWeight lam S (positiveRootSecond α)) = ∑ α ∈ S, (↑(lam (positiveRootFirst α)) - ↑(lam (positiveRootSecond α))) + ∑ i : Fin (r + 1), rootFamilyCharge S i * rootFamilyCharge S i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exists_signedRootWeight_descending_of_antitone {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (S : Finset (PositiveRoot r)) (hS : S.Nonempty) : ∃ α ∈ S, signedRootWeight lam S (positiveRootSecond α) < signedRootWeight lam S (positiveRootFirst α)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exists_rootWedgeWeight_descending_of_antitone {r k : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hk : 0 < k) (S : AdmissibleRootWedge lam k) : ∃ α ∈ ↑↑S, rootWedgeWeight lam S (positiveRootSecond α) < rootWedgeWeight lam S (positiveRootFirst α)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedPositiveRootOperator_fischer_energy_gap {r n : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) (p : JointHarmonicWeightSpace n μ) : inner ℝ ((weightedPositiveRootOperator n μ α hμ) p) ((weightedPositiveRootOperator n μ α hμ) p) = SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑p) ((polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑p) + (↑(μ (positiveRootFirst α)) - ↑(μ (positiveRootSecond α))) * inner ℝ p p

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedPositiveRootOperator_fischer_energy_ge_gap {r n : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) (p : JointHarmonicWeightSpace n μ) : (↑(μ (positiveRootFirst α)) - ↑(μ (positiveRootSecond α))) * inner ℝ p p ≤ inner ℝ ((weightedPositiveRootOperator n μ α hμ) p) ((weightedPositiveRootOperator n μ α hμ) p)

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.IncludedDescendingPositiveRoot {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) : Type

Roots included in the wedge whose first endpoint has strictly larger weight than their second endpoint.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedDescendingPositiveRoot_nonempty_of_antitone {r k : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hk : 0 < k) (S : AdmissibleRootWedge lam k) : Nonempty (IncludedDescendingPositiveRoot lam S)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedDescendingPositiveRoot_first_pos {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : IncludedDescendingPositiveRoot lam S) : 0 < rootWedgeWeight lam S (positiveRootFirst ↑α)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedDescendingPositiveRootOperator {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : IncludedDescendingPositiveRoot lam S) : JointHarmonicWeightSpace n (rootWedgeWeight lam S) →ₗ[ℝ] JointHarmonicWeightSpace n (lowerRootWeight (rootWedgeWeight lam S) ↑α)

The weighted lowering operator for an included root with strictly descending endpoint weights.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedDescendingPositiveRootOperatorStar {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : IncludedDescendingPositiveRoot lam S) : JointHarmonicWeightSpace n (lowerRootWeight (rootWedgeWeight lam S) ↑α) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

The Fischer adjoint of the lowering operator for an included root with descending endpoint weights.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedDescendingPositiveRoot_fischer_adjoint {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : IncludedDescendingPositiveRoot lam S) (p : JointHarmonicWeightSpace n (lowerRootWeight (rootWedgeWeight lam S) ↑α)) (q : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : inner ℝ ((includedDescendingPositiveRootOperatorStar n lam S α) p) q = inner ℝ p ((includedDescendingPositiveRootOperator n lam S α) q)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedDescendingPositiveRootFischerLaplacian {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) : JointHarmonicWeightSpace n (rootWedgeWeight lam S) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

The finite Fischer root Laplacian summed over the included roots with descending endpoint weights.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedDescendingPositiveRootFischerLaplacian_energy {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : inner ℝ p ((includedDescendingPositiveRootFischerLaplacian n lam S) p) = ∑ α : IncludedDescendingPositiveRoot lam S, inner ℝ ((includedDescendingPositiveRootOperator n lam S α) p) ((includedDescendingPositiveRootOperator n lam S α) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedDescendingPositiveRootFischerLaplacian_energy_ge_self {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : IncludedDescendingPositiveRoot lam S) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : inner ℝ p p ≤ inner ℝ p ((includedDescendingPositiveRootFischerLaplacian n lam S) p)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicIncludedDescendingFischerLaplacian {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam k →ₗ[ℝ] RootJointHarmonicChain n lam k

The root joint harmonic included descending fischer laplacian used in the spherical-code argument.

Equations

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

@[simp]

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicIncludedDescendingFischerLaplacian_energy_ge_self {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hk : 0 < k) (f : RootJointHarmonicChain n lam k) : inner ℝ f f ≤ inner ℝ f ((rootJointHarmonicIncludedDescendingFischerLaplacian n lam k) f)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicIncludedDescendingFischerLaplacian_energy_pos {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hk : 0 < k) (f : RootJointHarmonicChain n lam k) (hf : f ≠ 0) : 0 < inner ℝ f ((rootJointHarmonicIncludedDescendingFischerLaplacian n lam k) f)

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.IncludedNondescendingPositiveRoot {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) : Type

Included roots whose first endpoint has positive weight no larger than the second endpoint's weight.

Equations

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

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.ExcludedActivePositiveRoot {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) : Type

Roots absent from the wedge whose second endpoint has positive weight.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedNondescendingPositiveRootOperator {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : IncludedNondescendingPositiveRoot lam S) : JointHarmonicWeightSpace n (rootWedgeWeight lam S) →ₗ[ℝ] JointHarmonicWeightSpace n (lowerRootWeight (rootWedgeWeight lam S) ↑α)

The weighted lowering operator for an included root with positive, nondescending endpoint weights.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedNondescendingPositiveRootOperatorStar {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : IncludedNondescendingPositiveRoot lam S) : JointHarmonicWeightSpace n (lowerRootWeight (rootWedgeWeight lam S) ↑α) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

The Fischer adjoint of the lowering operator for an included root with nondescending endpoint weights.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedNondescendingPositiveRoot_fischer_adjoint {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : IncludedNondescendingPositiveRoot lam S) (p : JointHarmonicWeightSpace n (lowerRootWeight (rootWedgeWeight lam S) ↑α)) (q : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : inner ℝ ((includedNondescendingPositiveRootOperatorStar n lam S α) p) q = inner ℝ p ((includedNondescendingPositiveRootOperator n lam S α) q)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedNondescendingPositiveRootFischerLaplacian {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) : JointHarmonicWeightSpace n (rootWedgeWeight lam S) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

The finite Fischer root Laplacian summed over the included roots with nondescending endpoint weights.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.excludedActivePositiveRootOperator {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : ExcludedActivePositiveRoot lam S) : JointHarmonicWeightSpace n (rootWedgeWeight lam S) →ₗ[ℝ] JointHarmonicWeightSpace n (activeRootRaisedWeight (rootWedgeWeight lam S) ⟨↑α, ⋯⟩)

The active raising operator for a root absent from the wedge.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.excludedActivePositiveRootOperatorStar {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : ExcludedActivePositiveRoot lam S) : JointHarmonicWeightSpace n (activeRootRaisedWeight (rootWedgeWeight lam S) ⟨↑α, ⋯⟩) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

The Fischer adjoint lowering operator for an active root absent from the wedge.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.excludedActivePositiveRoot_fischer_adjoint {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (α : ExcludedActivePositiveRoot lam S) (p : JointHarmonicWeightSpace n (activeRootRaisedWeight (rootWedgeWeight lam S) ⟨↑α, ⋯⟩)) (q : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : inner ℝ ((excludedActivePositiveRootOperatorStar n lam S α) p) q = inner ℝ p ((excludedActivePositiveRootOperator n lam S α) q)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.excludedActivePositiveRootFischerLaplacian {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) : JointHarmonicWeightSpace n (rootWedgeWeight lam S) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

The finite Fischer root Laplacian summed over active roots absent from the wedge.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicHodgeDiagonal {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam k →ₗ[ℝ] RootJointHarmonicChain n lam k

The root joint harmonic hodge diagonal used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicHodgeDiagonal_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) : (rootJointHarmonicHodgeDiagonal n lam k) f S = (includedDescendingPositiveRootFischerLaplacian n lam S) (f S) + (includedNondescendingPositiveRootFischerLaplacian n lam S) (f S) + (excludedActivePositiveRootFischerLaplacian n lam S) (f S)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedNondescendingPositiveRootFischerLaplacian_energy {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : inner ℝ p ((includedNondescendingPositiveRootFischerLaplacian n lam S) p) = ∑ α : IncludedNondescendingPositiveRoot lam S, inner ℝ ((includedNondescendingPositiveRootOperator n lam S α) p) ((includedNondescendingPositiveRootOperator n lam S α) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedNondescendingPositiveRootFischerLaplacian_energy_nonneg {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : 0 ≤ inner ℝ p ((includedNondescendingPositiveRootFischerLaplacian n lam S) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.excludedActivePositiveRootFischerLaplacian_energy {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : inner ℝ p ((excludedActivePositiveRootFischerLaplacian n lam S) p) = ∑ α : ExcludedActivePositiveRoot lam S, inner ℝ ((excludedActivePositiveRootOperator n lam S α) p) ((excludedActivePositiveRootOperator n lam S α) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.excludedActivePositiveRootFischerLaplacian_energy_nonneg {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : 0 ≤ inner ℝ p ((excludedActivePositiveRootFischerLaplacian n lam S) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicHodgeDiagonal_energy_ge_included {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) : inner ℝ f ((rootJointHarmonicIncludedDescendingFischerLaplacian n lam k) f) ≤ inner ℝ f ((rootJointHarmonicHodgeDiagonal n lam k) f)

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSwapExteriorHodgeSign {r k : ℕ} {lam : Fin (r + 1) → ℕ} (S : AdmissibleRootWedge lam k) (α β : PositiveRoot r) : ℝ

The root swap exterior hodge sign used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionUpperRootStructureCross {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam k →ₗ[ℝ] RootJointHarmonicChain n lam k

The root joint harmonic action upper root structure cross used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionLowerRootStructureCross {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam k →ₗ[ℝ] RootJointHarmonicChain n lam k

The root joint harmonic action lower root structure cross used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionHodgeOffDiagonal {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam k →ₗ[ℝ] RootJointHarmonicChain n lam k

The root joint harmonic action hodge off diagonal used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionUpperRootStructureCross_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) : (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 β γ α) • (rootSwapUpperStructureEdge n lam S α β γ hα hβ hadm hγ) (f (rootAdmissibleSwap lam S α β hα hβ hadm)) else 0 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionLowerRootStructureCross_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) : (rootJointHarmonicActionLowerRootStructureCross 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 α γ β) • (rootSwapLowerStructureEdge n lam S α β γ hα hβ hadm hγ) (f (rootAdmissibleSwap lam S α β hα hβ hadm)) else 0 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedDescendingPositiveRootFischerLaplacian_apply_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : ↑↑((includedDescendingPositiveRootFischerLaplacian n lam S) p) = ∑ α : IncludedDescendingPositiveRoot lam S, (polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ((polarization r n (positiveRootSecond ↑α) (positiveRootFirst ↑α)) ↑↑p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.includedNondescendingPositiveRootFischerLaplacian_apply_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : ↑↑((includedNondescendingPositiveRootFischerLaplacian n lam S) p) = ∑ α : IncludedNondescendingPositiveRoot lam S, (polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ((polarization r n (positiveRootSecond ↑α) (positiveRootFirst ↑α)) ↑↑p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.excludedActivePositiveRootFischerLaplacian_apply_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : ↑↑((excludedActivePositiveRootFischerLaplacian n lam S) p) = ∑ α : ExcludedActivePositiveRoot lam S, (polarization r n (positiveRootSecond ↑α) (positiveRootFirst ↑α)) ((polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ↑↑p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicHodgeDiagonal_apply_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) : ↑↑((rootJointHarmonicHodgeDiagonal n lam k) f S) = ∑ α : IncludedDescendingPositiveRoot lam S, (polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ((polarization r n (positiveRootSecond ↑α) (positiveRootFirst ↑α)) ↑↑(f S)) + ∑ α : IncludedNondescendingPositiveRoot lam S, (polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ((polarization r n (positiveRootSecond ↑α) (positiveRootFirst ↑α)) ↑↑(f S)) + ∑ α : ExcludedActivePositiveRoot lam S, (polarization r n (positiveRootSecond ↑α) (positiveRootFirst ↑α)) ((polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ↑↑(f S))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_rootSubtype_eq_indicator {ι : Type u_1} {M : Type u_2} [Fintype ι] [AddCommMonoid M] (P : ι → Prop) [DecidablePred P] (F : ι → M) : ∑ a : { a : ι // P a }, F ↑a = ∑ a : ι, if P a then F a else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialIncludedActionHodgeDiagonal_eq_subtype_sums {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : (∑ α : PositiveRoot r, if α ∈ ↑↑S then if 0 < rootWedgeWeight lam S (positiveRootFirst α) then (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ((polarization r n (positiveRootSecond α) (positiveRootFirst α)) ↑↑p) else 0 else 0) = ∑ α : IncludedDescendingPositiveRoot lam S, (polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ((polarization r n (positiveRootSecond ↑α) (positiveRootFirst ↑α)) ↑↑p) + ∑ α : IncludedNondescendingPositiveRoot lam S, (polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ((polarization r n (positiveRootSecond ↑α) (positiveRootFirst ↑α)) ↑↑p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialExcludedActionHodgeDiagonal_eq_subtype_sum {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) : (∑ α : PositiveRoot r, if α ∈ ↑↑S then 0 else if 0 < rootWedgeWeight lam S (positiveRootSecond α) then (polarization r n (positiveRootSecond α) (positiveRootFirst α)) ((polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑p) else 0) = ∑ α : ExcludedActivePositiveRoot lam S, (polarization r n (positiveRootSecond ↑α) (positiveRootFirst ↑α)) ((polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ↑↑p)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicPolynomialInclusion {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam k →ₗ[ℝ] RootPolynomialChain r n k

The root joint harmonic polynomial inclusion used in the spherical-code argument.

Equations

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

@[simp]

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicPolynomialInclusion_injective {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : Function.Injective ⇑(rootJointHarmonicPolynomialInclusion n lam k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOperator_eq_zero_of_inadmissible_target {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (T : RootWedge r k) (hT : ¬∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (↑T) i) (α : PositiveRoot r) (hα : α ∉ ↑T) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑T) i) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam ⟨rootWedgeInsert T α hα, hadm⟩)) : (positiveRootOperator n α) ↑↑p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicPolynomialInclusion_action_intertwines {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : rootJointHarmonicPolynomialInclusion n lam k ∘ₗ weightedExteriorActionDifferential n lam k = rootActionBoundary r n k ∘ₗ rootJointHarmonicPolynomialInclusion n lam (k + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicPolynomialInclusion_bracket_intertwines {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : rootJointHarmonicPolynomialInclusion n lam k ∘ₗ weightedRootBracketBoundary n lam k = rootBracketBoundary r n k ∘ₗ rootJointHarmonicPolynomialInclusion n lam (k + 1)

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

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOrderCode {r : ℕ} (α : PositiveRoot r) : Fin ((r + 1) * (r + 1))

The positive root order code used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOrderCode α = finProdFinEquiv ↑α

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.sum_offDiagonal_eq_sum_orderedPairs {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [DecidableEq ι] [LinearOrder κ] [AddCommMonoid M] (key : ι → κ) (hkey : Function.Injective key) (F : ι → ι → M) : (∑ a : ι, ∑ b : ι, if a = b then 0 else F a b) = ∑ a : ι, ∑ b : ι, if key a < key b then F a b + F b a else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.realExteriorRootSign_mul_self {ι : Type u_1} [LinearOrder ι] (S : Finset ι) (a : ι) : realExteriorRootSign S a * realExteriorRootSign S a = 1

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootContraction {ι : Type u_1} [LinearOrder ι] (M : Type u_3) [AddCommGroup M] [Module ℝ M] (a : ι) : Module.End ℝ (Finset ι → M)

The actual exterior root contraction used in the spherical-code argument.

Equations

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

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootCreation {ι : Type u_1} [LinearOrder ι] (M : Type u_3) [AddCommGroup M] [Module ℝ M] (a : ι) : Module.End ℝ (Finset ι → M)

The actual exterior root creation used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootContraction_apply {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] (a : ι) (f : Finset ι → M) (S : Finset ι) : (actualExteriorRootContraction M a) f S = if a ∈ S then 0 else realExteriorRootSign (insert a S) a • f (insert a S)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootCreation_apply {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] (a : ι) (f : Finset ι → M) (S : Finset ι) : (actualExteriorRootCreation M a) f S = if a ∈ S then realExteriorRootSign S a • f (S.erase a) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.realExteriorRootSign_insert_insert_anticommute {ι : Type u_1} [LinearOrder ι] (S : Finset ι) (a b : ι) (ha : a ∉ S) (hb : b ∉ S) (hab : a ≠ b) : realExteriorRootSign (insert a S) a * realExteriorRootSign (insert b (insert a S)) b = -(realExteriorRootSign (insert b S) b * realExteriorRootSign (insert a (insert b S)) a)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.realExteriorRootSign_insert_erase_anticommute {ι : Type u_1} [LinearOrder ι] (S : Finset ι) (a b : ι) (ha : a ∉ S) (hb : b ∈ S) (hab : a ≠ b) : realExteriorRootSign (insert a S) a * realExteriorRootSign (insert a S) b = -(realExteriorRootSign S b * realExteriorRootSign (insert a (S.erase b)) a)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootContraction_anticommute {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] (a b : ι) : actualExteriorRootContraction M a * actualExteriorRootContraction M b + actualExteriorRootContraction M b * actualExteriorRootContraction M a = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootContraction_creation_anticommute {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] (a b : ι) : actualExteriorRootContraction M a * actualExteriorRootCreation M b + actualExteriorRootCreation M b * actualExteriorRootContraction M a = if a = b then 1 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleErase_nonnegative_iff_first_pos {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (α : PositiveRoot r) (hα : α ∈ ↑↑S) : (∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i) ↔ 0 < rootWedgeWeight lam S (positiveRootFirst α)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_nonnegative_iff_second_pos {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (β : PositiveRoot r) (hβ : β ∉ ↑↑S) : (∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ↑↑S) i) ↔ 0 < rootWedgeWeight lam S (positiveRootSecond β)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSwapExteriorActionPathSigns_anticommute {r : ℕ} (S : Finset (PositiveRoot r)) (α β : PositiveRoot r) (hα : α ∈ S) (hβ : β ∉ S) : realExteriorRootSign (insert β S) β * realExteriorRootSign (insert β S) α = -(realExteriorRootSign S α * realExteriorRootSign (insert β (S.erase α)) β)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSwap_twoActionPaths_eq_signed_commutator {r n : ℕ} (S : Finset (PositiveRoot r)) (α β : PositiveRoot r) (hα : α ∈ S) (hβ : β ∉ S) (p : PolynomialSpace r n) : (realExteriorRootSign S α * realExteriorRootSign (insert β (S.erase α)) β) • (positiveRootUpperOperator n α) ((positiveRootOperator n β) p) + (realExteriorRootSign (insert β S) β * realExteriorRootSign (insert β S) α) • (positiveRootOperator n β) ((positiveRootUpperOperator n α) p) = (realExteriorRootSign S α * realExteriorRootSign (insert β (S.erase α)) β) • (positiveRootUpperOperator n α ∘ₗ positiveRootOperator n β - positiveRootOperator n β ∘ₗ positiveRootUpperOperator n α) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootSwap_twoActionPaths_eq_signed_structureRoots {r n : ℕ} (S : Finset (PositiveRoot r)) (α β : PositiveRoot r) (hα : α ∈ S) (hβ : β ∉ S) (p : PolynomialSpace r n) : (realExteriorRootSign S α * realExteriorRootSign (insert β (S.erase α)) β) • (positiveRootUpperOperator n α) ((positiveRootOperator n β) p) + (realExteriorRootSign (insert β S) β * realExteriorRootSign (insert β S) α) • (positiveRootOperator n β) ((positiveRootUpperOperator n α) p) = (realExteriorRootSign S α * realExteriorRootSign (insert β (S.erase α)) β) • ((∑ γ : PositiveRoot r, rootStructureConstant β γ α • positiveRootUpperOperator n γ) p + (∑ γ : PositiveRoot r, rootStructureConstant α γ β • positiveRootOperator n γ) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionCoboundaryDifferentialIncidence_diag {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) (α : PositiveRoot r) : rootPolynomialActionCoboundaryDifferentialIncidence lam f S α α = if α ∈ ↑↑S then if 0 < rootWedgeWeight lam S (positiveRootFirst α) then (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ((polarization r n (positiveRootSecond α) (positiveRootFirst α)) ↑↑(f S)) else 0 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionDifferentialCoboundaryIncidence_diag {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) (α : PositiveRoot r) : rootPolynomialActionDifferentialCoboundaryIncidence lam f S α α = if α ∈ ↑↑S then 0 else if 0 < rootWedgeWeight lam S (positiveRootSecond α) then (polarization r n (positiveRootSecond α) (positiveRootFirst α)) ((polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑(f S)) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionHodgeDiagonalIncidence_eq_positive_root_sums {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) : rootPolynomialActionHodgeDiagonalIncidence lam f S = (∑ α : PositiveRoot r, if α ∈ ↑↑S then if 0 < rootWedgeWeight lam S (positiveRootFirst α) then (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ((polarization r n (positiveRootSecond α) (positiveRootFirst α)) ↑↑(f S)) else 0 else 0) + ∑ α : PositiveRoot r, if α ∈ ↑↑S then 0 else if 0 < rootWedgeWeight lam S (positiveRootSecond α) then (polarization r n (positiveRootSecond α) (positiveRootFirst α)) ((polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑(f S)) else 0

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionHodge_apply_coe_eq_hodgeDiagonal_add_offDiagonal {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) : ↑↑((weightedExteriorActionCoboundary n lam k ∘ₗ weightedExteriorActionDifferential n lam k + weightedExteriorActionDifferential n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam (k + 1)) f S) = ↑↑((rootJointHarmonicHodgeDiagonal n lam (k + 1)) f S) + rootPolynomialActionHodgeOffDiagonalIncidence lam f S

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleSwap_first_eq_and_source_first_zero_of_inadmissible_erase {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (α β : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hbad : ¬∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i) : positiveRootFirst α = positiveRootFirst β ∧ rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm) (positiveRootFirst β) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleSwap_upper_lower_eq_zero_of_inadmissible_erase {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (α β : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hbad : ¬∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam ((↑↑S).erase α) i) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm))) : (positiveRootUpperOperator n α) ((positiveRootOperator n β) ↑↑p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleSwap_second_eq_and_source_second_zero_of_inadmissible_insert {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (α β : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hbad : ¬∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ↑↑S) i) : positiveRootSecond α = positiveRootSecond β ∧ rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm) (positiveRootSecond α) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleSwap_lower_upper_eq_zero_of_inadmissible_insert {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (α β : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) (hbad : ¬∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ↑↑S) i) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam (rootAdmissibleSwap lam S α β hα hβ hadm))) : (positiveRootOperator n β) ((positiveRootUpperOperator n α) ↑↑p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionCoboundaryDifferentialIncidence_swap {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) (α β : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) : rootPolynomialActionCoboundaryDifferentialIncidence lam f S α β = (realExteriorRootSign (↑↑S) α * realExteriorRootSign (insert β ((↑↑S).erase α)) β) • (positiveRootUpperOperator n α) ((positiveRootOperator n β) ↑↑(f (rootAdmissibleSwap lam S α β hα hβ hadm)))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionDifferentialCoboundaryIncidence_swap {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) (α β : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) : rootPolynomialActionDifferentialCoboundaryIncidence lam f S β α = (realExteriorRootSign (insert β ↑↑S) β * realExteriorRootSign (insert β ↑↑S) α) • (positiveRootOperator n β) ((positiveRootUpperOperator n α) ↑↑(f (rootAdmissibleSwap lam S α β hα hβ hadm)))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialActionIncidence_pair_eq_structureRoots {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam (k + 1)) (S : AdmissibleRootWedge lam (k + 1)) (α β : PositiveRoot r) (hα : α ∈ ↑↑S) (hβ : β ∉ ↑↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert β ((↑↑S).erase α)) i) : rootPolynomialActionCoboundaryDifferentialIncidence lam f S α β + rootPolynomialActionDifferentialCoboundaryIncidence lam f S β α = (∑ γ : PositiveRoot r, if _hγ : rootStructureConstant β γ α = 0 then 0 else (rootSwapExteriorHodgeSign S α β * rootStructureConstant β γ α) • (polarization r n (positiveRootFirst γ) (positiveRootSecond γ)) ↑↑(f (rootAdmissibleSwap lam S α β hα hβ hadm))) + ∑ γ : PositiveRoot r, if _hγ : rootStructureConstant α γ β = 0 then 0 else (rootSwapExteriorHodgeSign S α β * rootStructureConstant α γ β) • (polarization r n (positiveRootSecond γ) (positiveRootFirst γ)) ↑↑(f (rootAdmissibleSwap lam S α β hα hβ hadm))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionUpperRootStructureCross_polynomial_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) : ↑↑((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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionLowerRootStructureCross_polynomial_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) : ↑↑((rootJointHarmonicActionLowerRootStructureCross 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 (positiveRootSecond γ) (positiveRootFirst γ)) ↑↑(f (rootAdmissibleSwap lam S α β hα hβ hadm)) else 0 else 0

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

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketEdgeAdjoint {r k : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (T : AdmissibleRootWedge lam k) (h : rootBracketBoundaryCoefficient ↑S ↑T ≠ 0) : JointHarmonicWeightSpace n (rootWedgeWeight lam T) →ₗ[ℝ] JointHarmonicWeightSpace n (rootWedgeWeight lam S)

The reverse weight-space identification for a wedge edge with nonzero root-bracket boundary coefficient.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketEdgeAdjoint_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (T : AdmissibleRootWedge lam k) (h : rootBracketBoundaryCoefficient ↑S ↑T ≠ 0) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam T)) : ↑↑((weightedRootBracketEdgeAdjoint n lam S T h) p) = ↑↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketEdge_fischer_adjoint {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam (k + 1)) (T : AdmissibleRootWedge lam k) (h : rootBracketBoundaryCoefficient ↑S ↑T ≠ 0) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam S)) (q : JointHarmonicWeightSpace n (rootWedgeWeight lam T)) : inner ℝ ((weightedRootBracketEdge n lam S T h) p) q = inner ℝ p ((weightedRootBracketEdgeAdjoint n lam S T h) q)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketCoboundary {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam k →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)

The weighted root bracket coboundary used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketCoboundary_apply {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam (k + 1)) : (weightedRootBracketCoboundary n lam k) f S = ∑ T : AdmissibleRootWedge lam k, if h : rootBracketBoundaryCoefficient ↑S ↑T = 0 then 0 else rootBracketBoundaryCoefficient ↑S ↑T • (weightedRootBracketEdgeAdjoint n lam S T h) (f T)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketBoundary_fischer_adjoint {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam (k + 1)) (q : RootJointHarmonicChain n lam k) : inner ℝ ((weightedRootBracketBoundary n lam k) p) q = inner ℝ p ((weightedRootBracketCoboundary n lam k) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedRootBracketCoboundary_apply_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam (k + 1)) : ↑↑((weightedRootBracketCoboundary n lam k) f S) = ∑ T : AdmissibleRootWedge lam k, rootBracketBoundaryCoefficient ↑S ↑T • ↑↑(f T)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootContraction_creation_creation_contraction_anticommute {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] (a b c d : ι) : actualExteriorRootContraction M a * (actualExteriorRootCreation M b * (actualExteriorRootCreation M c * actualExteriorRootContraction M d)) + actualExteriorRootCreation M b * (actualExteriorRootCreation M c * actualExteriorRootContraction M d) * actualExteriorRootContraction M a = (if a = b then actualExteriorRootCreation M c * actualExteriorRootContraction M d else 0) - if a = c then actualExteriorRootCreation M b * actualExteriorRootContraction M d else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootContraction_creation_contraction_contraction_anticommute {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] (a b c d : ι) : actualExteriorRootContraction M a * (actualExteriorRootCreation M b * (actualExteriorRootContraction M c * actualExteriorRootContraction M d)) + actualExteriorRootCreation M b * (actualExteriorRootContraction M c * actualExteriorRootContraction M d) * actualExteriorRootContraction M a = if a = b then actualExteriorRootContraction M c * actualExteriorRootContraction M d else 0

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootBracketCoboundary {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] [Fintype ι] (structureConstant : ι → ι → ι → ℝ) : Module.End ℝ (Finset ι → M)

The actual exterior root bracket coboundary used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootContraction_bracketCoboundary_anticommute {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommGroup M] [Module ℝ M] [Fintype ι] (structureConstant : ι → ι → ι → ℝ) (a : ι) : actualExteriorRootContraction M a * actualExteriorRootBracketCoboundary structureConstant + actualExteriorRootBracketCoboundary structureConstant * actualExteriorRootContraction M a = ∑ c : ι, ∑ d : ι, structureConstant a c d • (actualExteriorRootCreation M c * actualExteriorRootContraction M d) - ∑ b : ι, ∑ d : ι, structureConstant b a d • (actualExteriorRootCreation M b * actualExteriorRootContraction M d)

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.FullRootExteriorPolynomialChain (r n : ℕ) : Type

The full root exterior polynomial chain used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorPolynomialAction (r n : ℕ) (α : PositiveRoot r) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The full root exterior polynomial action used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorPolynomialAction_apply {r n : ℕ} (α : PositiveRoot r) (f : FullRootExteriorPolynomialChain r n) (S : Finset (PositiveRoot r)) : (fullRootExteriorPolynomialAction r n α) f S = (positiveRootOperator n α) (f S)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorPolynomialAction_contraction_commute {r n : ℕ} (α β : PositiveRoot r) : fullRootExteriorPolynomialAction r n α * actualExteriorRootContraction (PolynomialSpace r n) β = actualExteriorRootContraction (PolynomialSpace r n) β * fullRootExteriorPolynomialAction r n α

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorPolynomialAction_creation_commute {r n : ℕ} (α β : PositiveRoot r) : fullRootExteriorPolynomialAction r n α * actualExteriorRootCreation (PolynomialSpace r n) β = actualExteriorRootCreation (PolynomialSpace r n) β * fullRootExteriorPolynomialAction r n α

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorPolynomialAction_commutator {r n : ℕ} (α β : PositiveRoot r) : fullRootExteriorPolynomialAction r n α * fullRootExteriorPolynomialAction r n β - fullRootExteriorPolynomialAction r n β * fullRootExteriorPolynomialAction r n α = ∑ γ : PositiveRoot r, rootStructureConstant α β γ • fullRootExteriorPolynomialAction r n γ

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootContraction_mul_self_zero {r n : ℕ} (α : PositiveRoot r) : actualExteriorRootContraction (PolynomialSpace r n) α * actualExteriorRootContraction (PolynomialSpace r n) α = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorActionAtom (r n : ℕ) (α : PositiveRoot r) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The full root exterior action atom used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorAction (r n : ℕ) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The full root exterior action used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracketAtom (r n : ℕ) (α β γ : PositiveRoot r) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The full root exterior bracket atom used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorBracket (r n : ℕ) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The full root exterior bracket used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialChainZeroExtension (r n k : ℕ) : RootPolynomialChain r n k →ₗ[ℝ] Finset (PositiveRoot r) → PolynomialSpace r n

The root polynomial chain zero extension used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialChainZeroExtension_apply {r n k : ℕ} (f : RootPolynomialChain r n k) (S : Finset (PositiveRoot r)) : (rootPolynomialChainZeroExtension r n k) f S = if h : S.card = k then f ⟨S, h⟩ else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialChainZeroExtension_wedge {r n k : ℕ} (f : RootPolynomialChain r n k) (S : RootWedge r k) : (rootPolynomialChainZeroExtension r n k) f ↑S = f S

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialChainZeroExtension_of_card_ne {r n k : ℕ} (f : RootPolynomialChain r n k) (S : Finset (PositiveRoot r)) (h : S.card ≠ k) : (rootPolynomialChainZeroExtension r n k) f S = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionBoundary_eq_exteriorContraction_zeroExtension {r n k : ℕ} (f : RootPolynomialChain r n (k + 1)) (T : RootWedge r k) : (rootActionBoundary r n k) f T = ∑ α : PositiveRoot r, (positiveRootOperator n α) ((actualExteriorRootContraction (PolynomialSpace r n) α) ((rootPolynomialChainZeroExtension r n (k + 1)) f) ↑T)

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeErase {r k : ℕ} (S : RootWedge r (k + 1)) (α : PositiveRoot r) (hα : α ∈ ↑S) : RootWedge r k

Erase a specified member of a root wedge, reducing its cardinality by one.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeErase S α hα = ⟨(↑S).erase α, ⋯⟩

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeErase_val {r k : ℕ} (S : RootWedge r (k + 1)) (α : PositiveRoot r) (hα : α ∈ ↑S) : ↑(rootWedgeErase S α hα) = (↑S).erase α

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionCoboundary (r n k : ℕ) : RootPolynomialChain r n k →ₗ[ℝ] RootPolynomialChain r n (k + 1)

The root action coboundary used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionCoboundary_apply {r n k : ℕ} (f : RootPolynomialChain r n k) (S : RootWedge r (k + 1)) : (rootActionCoboundary r n k) f S = ∑ α : PositiveRoot r, if hα : α ∈ ↑S then realExteriorRootSign (↑S) α • (positiveRootUpperOperator n α) (f (rootWedgeErase S α hα)) else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracketCoboundary (r n k : ℕ) : RootPolynomialChain r n k →ₗ[ℝ] RootPolynomialChain r n (k + 1)

The root bracket coboundary used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracketCoboundary_apply {r n k : ℕ} (f : RootPolynomialChain r n k) (S : RootWedge r (k + 1)) : (rootBracketCoboundary r n k) f S = ∑ T : RootWedge r k, rootBracketBoundaryCoefficient S T • f T

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicPolynomialInclusion_bracketCoboundary_intertwines {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : rootJointHarmonicPolynomialInclusion n lam (k + 1) ∘ₗ weightedRootBracketCoboundary n lam k = rootBracketCoboundary r n k ∘ₗ rootJointHarmonicPolynomialInclusion n lam k

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.upperRootOperator_eq_zero_of_inadmissible_insert {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (T : AdmissibleRootWedge lam k) (α : PositiveRoot r) (hα : α ∉ ↑↑T) (hbad : ¬∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (insert α ↑↑T) i) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam T)) : (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootUpperOperator_eq_zero_of_inadmissible_target {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (S : RootWedge r (k + 1)) (hS : ¬∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (↑S) i) (α : PositiveRoot r) (hα : α ∈ ↑S) (hadm : ∀ (i : Fin (r + 1)), 0 ≤ signedRootWeight lam (↑(rootWedgeErase S α hα)) i) (p : JointHarmonicWeightSpace n (rootWedgeWeight lam ⟨rootWedgeErase S α hα, hadm⟩)) : (positiveRootUpperOperator n α) ↑↑p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionCoboundary_eq_exteriorCreation_zeroExtension {r n k : ℕ} (f : RootPolynomialChain r n k) (S : RootWedge r (k + 1)) : (rootActionCoboundary r n k) f S = ∑ α : PositiveRoot r, (positiveRootUpperOperator n α) ((actualExteriorRootCreation (PolynomialSpace r n) α) ((rootPolynomialChainZeroExtension r n k) f) ↑S)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperPolynomialAction (r n : ℕ) (α : PositiveRoot r) : Module.End ℝ (Finset (PositiveRoot r) → PolynomialSpace r n)

The full root exterior upper polynomial action used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorUpperPolynomialAction_apply {r n : ℕ} (α : PositiveRoot r) (f : Finset (PositiveRoot r) → PolynomialSpace r n) (S : Finset (PositiveRoot r)) : (fullRootExteriorUpperPolynomialAction r n α) f S = (positiveRootUpperOperator n α) (f S)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorActionCoboundary (r n : ℕ) : Module.End ℝ (Finset (PositiveRoot r) → PolynomialSpace r n)

The full root exterior action coboundary used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionCoboundary_zeroExtension {r n k : ℕ} (f : RootPolynomialChain r n k) : (rootPolynomialChainZeroExtension r n (k + 1)) ((rootActionCoboundary r n k) f) = (fullRootExteriorActionCoboundary r n) ((rootPolynomialChainZeroExtension r n k) f)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicPolynomialInclusion_actionCoboundary_intertwines {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : rootJointHarmonicPolynomialInclusion n lam (k + 1) ∘ₗ weightedExteriorActionCoboundary n lam k = rootActionCoboundary r n k ∘ₗ rootJointHarmonicPolynomialInclusion n lam k

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionHodge_eq_diagonal_add_offDiagonal {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : 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)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialChainZeroExtension_eq_sum_single {r n k : ℕ} (f : RootPolynomialChain r n k) : (rootPolynomialChainZeroExtension r n k) f = ∑ S : RootWedge r k, Pi.single (↑S) (f S)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootExteriorBracketAtom_support_iff {ι : Type u_1} [LinearOrder ι] (S T : Finset ι) (α β γ : ι) : γ ∈ T ∧ β ∉ T.erase γ ∧ α ∉ insert β (T.erase γ) ∧ insert α (insert β (T.erase γ)) = S ↔ α ∈ S ∧ β ∈ S.erase α ∧ γ ∉ (S.erase α).erase β ∧ T = insert γ ((S.erase α).erase β)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorAction_zeroExtension_apply {r n k : ℕ} (f : RootPolynomialChain r n (k + 1)) (T : RootWedge r k) : (fullRootExteriorAction r n) ((rootPolynomialChainZeroExtension r n (k + 1)) f) ↑T = (rootActionBoundary r n k) f T

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_coboundaryIncidence_swap {M : Type u_1} [AddCommGroup M] [Module ℝ M] {r : ℕ} (a : PositiveRoot r) : ∑ b : PositiveRoot r, ∑ d : PositiveRoot r, rootStructureConstant b a d • (actualExteriorRootCreation M b * actualExteriorRootContraction M d) = -∑ c : PositiveRoot r, ∑ d : PositiveRoot r, rootStructureConstant a c d • (actualExteriorRootCreation M c * actualExteriorRootContraction M d)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualOrderedRootBracketCoboundary {M : Type u_1} [AddCommGroup M] [Module ℝ M] {r : ℕ} : Module.End ℝ (Finset (PositiveRoot r) → M)

The actual ordered root bracket coboundary used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.actualExteriorRootContraction_orderedBracketCoboundary_anticommute {M : Type u_1} [AddCommGroup M] [Module ℝ M] {r : ℕ} (a : PositiveRoot r) : actualExteriorRootContraction M a * actualOrderedRootBracketCoboundary + actualOrderedRootBracketCoboundary * actualExteriorRootContraction M a = ∑ c : PositiveRoot r, ∑ d : PositiveRoot r, rootStructureConstant a c d • (actualExteriorRootCreation M c * actualExteriorRootContraction M d)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicBracketActionMixed {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) : RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ] RootJointHarmonicChain n lam (k + 1)

The root joint harmonic bracket action mixed used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootPolynomialBracketActionMixed (r n k : ℕ) : RootPolynomialChain r n (k + 1) →ₗ[ℝ] RootPolynomialChain r n (k + 1)

The root polynomial bracket action mixed used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicPolynomialInclusion_bracketActionMixed_intertwines {r n k : ℕ} (lam : Fin (r + 1) → ℕ) : rootJointHarmonicPolynomialInclusion n lam (k + 1) ∘ₗ rootJointHarmonicBracketActionMixed n lam k = rootPolynomialBracketActionMixed r n k ∘ₗ rootJointHarmonicPolynomialInclusion n lam (k + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant_output_eq_right_zero {r : ℕ} (γ α : PositiveRoot r) : rootStructureConstant γ α α = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorPolynomialAction_orderedBracketCoboundary_commute {r n : ℕ} (γ : PositiveRoot r) : fullRootExteriorPolynomialAction r n γ * actualOrderedRootBracketCoboundary = actualOrderedRootBracketCoboundary * fullRootExteriorPolynomialAction r n γ

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorLowerRootStructureIncidence (r n : ℕ) : Module.End ℝ (FullRootExteriorPolynomialChain r n)

The full root exterior lower root structure incidence used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.fullRootExteriorAction_orderedBracketCoboundary_anticommute {r n : ℕ} : fullRootExteriorAction r n * actualOrderedRootBracketCoboundary + actualOrderedRootBracketCoboundary * fullRootExteriorAction r n = fullRootExteriorLowerRootStructureIncidence r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicActionLowerRootStructureCross_apply_coe {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (f : RootJointHarmonicChain n lam k) (S : AdmissibleRootWedge lam k) : ↑↑((rootJointHarmonicActionLowerRootStructureCross 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 (positiveRootSecond γ) (positiveRootFirst γ)) ↑↑(f (rootAdmissibleSwap lam S α β hα hβ hadm)) else 0 else 0