Documentation

def MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight {r n : ℕ} (v : Fin ((r + 1) * n)) :

The isotropic coordinate coheight used in the positive-root weighted filtration.

Equations

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

Instances For

@[simp]

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

isotropicCoordinateCoheight (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) = ↑p

@[simp]

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

isotropicCoordinateCoheight (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p)) = 2 * (r + 1) - ↑p

@[simp]

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

isotropicCoordinateCoheight (HigherHarmonicYoung.variableIndex a t) = r + 1

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicCoordinateCoheight_le {r n : ℕ} (v : Fin ((r + 1) * n)) :

isotropicCoordinateCoheight v ≤ 2 * (r + 1)

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation {σ : Type u_1} (e : MvPolynomial σ ℂ ≃ₐ[ℂ ] MvPolynomial σ ℂ) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) :

Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)

The conjugated polynomial derivation used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation e D = MvPolynomial.mkDerivation ℂ fun (i : σ) => e.symm (D (e (MvPolynomial.X i)))

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation_X {σ : Type u_1} (e : MvPolynomial σ ℂ ≃ₐ[ℂ ] MvPolynomial σ ℂ) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (i : σ) :

(conjugatedPolynomialDerivation e D) (MvPolynomial.X i) = e.symm (D (e (MvPolynomial.X i)))

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation_intertwine {σ : Type u_1} (e : MvPolynomial σ ℂ ≃ₐ[ℂ ] MvPolynomial σ ℂ) (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (p : MvPolynomial σ ℂ) :

e ((conjugatedPolynomialDerivation e D) p) = D (e p)

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootDerivation {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) :

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

The isotropic orthogonal positive root derivation used in the spherical-code argument.

Equations

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

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootDerivation_intertwine {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) ((isotropicOrthogonalPositiveRootDerivation h α) p) = (orthogonalPositiveRootDerivation h α) ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) p)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.weighted_coefficient_smul_X_lt {σ : Type u_1} (weight : σ → ℕ) (u v : σ) (c : ℂ) (huv : weight u < weight v) (d : σ →₀ ℕ) (hd : (c • MvPolynomial.X u).coeff d ≠ 0) :

(Finsupp.weight weight) d + 1 ≤ weight v

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootWord_intertwine {r n : ℕ} (h : 2 * (r + 1) ≤ n) (word : List (OrthogonalPositiveRoot r n)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) :

(HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) ((HigherYoungTwoRowLieIrreducibility.rootOperatorWord (fun (α : OrthogonalPositiveRoot r n) => ↑(isotropicOrthogonalPositiveRootDerivation h α)) word) p) = (HigherYoungTwoRowLieIrreducibility.rootOperatorWord (fun (α : OrthogonalPositiveRoot r n) => ↑(orthogonalPositiveRootDerivation h α)) word) ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) p)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedDifferenceRoot_X_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a j : Fin (r + 1)) :

(isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.difference p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j))) = if q = j then 2 • MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedDifferenceRoot_X_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a j : Fin (r + 1)) :

(isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.difference p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j))) = if p = j then -2 • MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h q)) else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedSumRoot_X_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a j : Fin (r + 1)) :

(isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.sum p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j))) = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedSumRoot_X_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a j : Fin (r + 1)) :

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedDifferenceRoot_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.difference p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedSumRoot_X_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) :

(isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.sum p q hpq)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t)) = 0

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

(isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.short p t ht)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j))) = 0

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

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

(isotropicOrthogonalPositiveRootDerivation h (OrthogonalPositiveRoot.short p t ht)) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a u)) = if t = u then MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) else 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRoot_strict_even {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) (a j : Fin (r + 1)) (d : Fin ((r + 1) * n) →₀ ℕ) (hd : ((isotropicOrthogonalPositiveRootDerivation h α) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j)))).coeff d ≠ 0) :

(Finsupp.weight isotropicCoordinateCoheight) d + 1 ≤ isotropicCoordinateCoheight (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j))

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRoot_strict_odd {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) (a j : Fin (r + 1)) (d : Fin ((r + 1) * n) →₀ ℕ) (hd : ((isotropicOrthogonalPositiveRootDerivation h α) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j)))).coeff d ≠ 0) :

(Finsupp.weight isotropicCoordinateCoheight) d + 1 ≤ isotropicCoordinateCoheight (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j))

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRoot_strict_unused {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) (a : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) (d : Fin ((r + 1) * n) →₀ ℕ) (hd : ((isotropicOrthogonalPositiveRootDerivation h α) (MvPolynomial.X (HigherHarmonicYoung.variableIndex a t))).coeff d ≠ 0) :

(Finsupp.weight isotropicCoordinateCoheight) d + 1 ≤ isotropicCoordinateCoheight (HigherHarmonicYoung.variableIndex a t)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRoot_strict {r n : ℕ} (h : 2 * (r + 1) ≤ n) (α : OrthogonalPositiveRoot r n) (v : Fin ((r + 1) * n)) (d : Fin ((r + 1) * n) →₀ ℕ) (hd : ((isotropicOrthogonalPositiveRootDerivation h α) (MvPolynomial.X v)).coeff d ≠ 0) :

(Finsupp.weight isotropicCoordinateCoheight) d + 1 ≤ isotropicCoordinateCoheight v

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.isotropicOrthogonalPositiveRootWord_eq_zero_of_isHomogeneous {r n m : ℕ} (h : 2 * (r + 1) ≤ n) {p : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hp : p.IsHomogeneous m) (word : List (OrthogonalPositiveRoot r n)) (hlen : m * (2 * (r + 1)) < word.length) :

(HigherYoungTwoRowLieIrreducibility.rootOperatorWord (fun (α : OrthogonalPositiveRoot r n) => ↑(isotropicOrthogonalPositiveRootDerivation h α)) word) p = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootWord_eq_zero_of_isHomogeneous {r n m : ℕ} (h : 2 * (r + 1) ≤ n) {p : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hp : p.IsHomogeneous m) (word : List (OrthogonalPositiveRoot r n)) (hlen : m * (2 * (r + 1)) < word.length) :

(HigherYoungTwoRowLieIrreducibility.rootOperatorWord (fun (α : OrthogonalPositiveRoot r n) => ↑(orthogonalPositiveRootDerivation h α)) word) p = 0

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

Algebra.adjoin ℂ (Set.range fun (ap : Fin (r + 1) × Fin (r + 1)) => HigherHarmonicYoung.DeterminantVectors.isotropicVariable h ap.1 ap.2) = (HigherHarmonicYoung.nullSubstitution h).range

theorem MetricCodes.Spherical.HigherYoungIsotropicAdjoinRange.exists_nullSubstitution_of_mem_adjoin_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ Algebra.adjoin ℂ (Set.range fun (ap : Fin (r + 1) × Fin (r + 1)) => HigherHarmonicYoung.DeterminantVectors.isotropicVariable h ap.1 ap.2)) :

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

theorem MetricCodes.Spherical.HigherYoungEvenCoordinateHolomorphicAdjoin.isotropicCoordinateEquiv_mem_adjoin_of_even_vars {r n : ℕ} (h : 2 * (r + 1) ≤ n) (g : MvPolynomial (Fin ((r + 1) * n)) ℂ) (heven : ∀ v ∈ g.vars, ∃ (a : Fin (r + 1)) (p : Fin (r + 1)), v = HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) :

(HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) g ∈ Algebra.adjoin ℂ (Set.range fun (ap : Fin (r + 1) × Fin (r + 1)) => HigherHarmonicYoung.DeterminantVectors.isotropicVariable h ap.1 ap.2)

def MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect {r n : ℕ} (v : Fin ((r + 1) * n)) :

The isotropic defect weight: zero on even paired coordinates, two on odd ones, and one elsewhere.

Equations

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

Instances For

@[simp]

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

isotropicCoordinateDefect (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)) = 0

@[simp]

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

isotropicCoordinateDefect (HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.oddCoordinate h p)) = 2

@[simp]

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

isotropicCoordinateDefect (HigherHarmonicYoung.variableIndex a t) = 1

noncomputable def MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation {ι : Type u_1} (w : ι → ℕ) :

Derivation ℂ (MvPolynomial ι ℂ) (MvPolynomial ι ℂ)

The diagonal polynomial derivation sending each variable to its natural weight times itself.

Equations

MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation w = MvPolynomial.mkDerivation ℂ fun (i : ι) => ↑(w i) • MvPolynomial.X i

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation_X {ι : Type u_1} (w : ι → ℕ) (i : ι) :

(naturalDiagonalDerivation w) (MvPolynomial.X i) = ↑(w i) • MvPolynomial.X i

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.coeff_X_mul_pderiv {ι : Type u_1} (p : MvPolynomial ι ℂ) (i : ι) (d : ι →₀ ℕ) :

(MvPolynomial.X i * (MvPolynomial.pderiv i) p).coeff d = ↑(d i) * p.coeff d

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation_eq_sum {ι : Type u_1} [Fintype ι] (w : ι → ℕ) :

naturalDiagonalDerivation w = ∑ i : ι, ↑(w i) • MvPolynomial.X i • MvPolynomial.pderiv i

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation_apply {ι : Type u_1} [Fintype ι] (w : ι → ℕ) (p : MvPolynomial ι ℂ) :

(naturalDiagonalDerivation w) p = ∑ i : ι, ↑(w i) • (MvPolynomial.X i * (MvPolynomial.pderiv i) p)

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation_coeff {ι : Type u_1} [Fintype ι] (w : ι → ℕ) (p : MvPolynomial ι ℂ) (d : ι →₀ ℕ) :

((naturalDiagonalDerivation w) p).coeff d = ↑(∑ i : ι, w i * d i) * p.coeff d

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

(HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation (HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h)) (MvPolynomial.X v) = 2 • MvPolynomial.X v - ↑(2 * isotropicCoordinateDefect v) • MvPolynomial.X v

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

HigherYoungArbitraryRankOrthogonalRootHighestKernel.conjugatedPolynomialDerivation (HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h) (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) = (2 • naturalDiagonalDerivation fun (x : Fin ((r + 1) * n)) => 1) - naturalDiagonalDerivation fun (i : Fin ((r + 1) * n)) => 2 * isotropicCoordinateDefect i

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.naturalDiagonalDerivation_one_of_homogeneous {ι : Type u_1} [Finite ι] {d : ℕ} (p : MvPolynomial ι ℂ) (hp : p.IsHomogeneous d) :

(naturalDiagonalDerivation fun (x : ι) => 1) p = ↑d • p

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.exists_evenCoordinate_of_defect_eq_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) (v : Fin ((r + 1) * n)) (hv : isotropicCoordinateDefect v = 0) :

∃ (a : Fin (r + 1)) (p : Fin (r + 1)), v = HigherHarmonicYoung.variableIndex a (HigherHarmonicYoung.DeterminantVectors.evenCoordinate h p)

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefectDerivation_eq_zero_of_maximalCartan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : ℕ) (hfhom : f.IsHomogeneous d) (hcartan : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) f = ↑(2 * d) • f) :

(naturalDiagonalDerivation fun (i : Fin ((r + 1) * n)) => 2 * isotropicCoordinateDefect i) ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h).symm f) = 0

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.isotropicCoordinateDefect_eq_zero_of_mem_vars_of_maximalCartan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : ℕ) (hfhom : f.IsHomogeneous d) (hcartan : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) f = ↑(2 * d) • f) (v : Fin ((r + 1) * n)) (hv : v ∈ ((HigherYoungAmbientRootNilpotence.isotropicCoordinateEquiv h).symm f).vars) :

isotropicCoordinateDefect v = 0

theorem MetricCodes.Spherical.HigherYoungMaximalCartanNullSubstitutionRange.maximalTotalAmbientCartan_mem_nullSubstitution_range {r n : ℕ} (h : 2 * (r + 1) ≤ n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : ℕ) (hfhom : f.IsHomogeneous d) (hcartan : (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan h) f = ↑(2 * d) • f) :

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

noncomputable def MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

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

The young complex pair used in the spherical-code argument.

Equations

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

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.polynomialRealPart_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

HigherHarmonicYoung.polynomialRealPart (youngComplexPair lam p q) = ↑p

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.polynomialImaginaryPart_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

HigherHarmonicYoung.polynomialImaginaryPart (youngComplexPair lam p q) = ↑q

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.complexPolynomial_eq_of_real_imaginary {r n : ℕ} (p q : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hreal : HigherHarmonicYoung.polynomialRealPart p = HigherHarmonicYoung.polynomialRealPart q) (himag : HigherHarmonicYoung.polynomialImaginaryPart p = HigherHarmonicYoung.polynomialImaginaryPart q) :

p = q

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair_eq_zero_iff {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

youngComplexPair lam p q = 0 ↔ p = 0 ∧ q = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.complexAmbientRotation_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

(HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a b) (youngComplexPair lam p q) = youngComplexPair lam ((HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b) p) ((HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b) q)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.complex_smul_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (c : ℂ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

c • youngComplexPair lam p q = youngComplexPair lam (c.re • p - c.im • q) (c.im • p + c.re • q)

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair_add {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q p' q' : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

youngComplexPair lam (p + p') (q + q') = youngComplexPair lam p q + youngComplexPair lam p' q'

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.complexRotationCombination_youngComplexPair {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin k → Fin n) (c : Fin k → ℂ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

∑ i : Fin k, c i • (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation (a i) (b i)) (youngComplexPair lam p q) = youngComplexPair lam (∑ i : Fin k, ((c i).re • (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (a i) (b i)) p - (c i).im • (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (a i) (b i)) q)) (∑ i : Fin k, ((c i).im • (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (a i) (b i)) p + (c i).re • (HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam (a i) (b i)) q))

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rowDerivation_self_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (i : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.rowDerivation i i) (youngComplexPair lam p q) = ↑(lam i) • youngComplexPair lam p q

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rowDerivation_upper_youngComplexPair {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (i j : Fin (r + 1)) (hij : i < j) :

(HigherHarmonicYoung.DeterminantVectors.rowDerivation i j) (youngComplexPair lam p q) = 0

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

youngComplexPair lam (HigherYoungCyclicHighestSchur.dominantHighestRealVector hn lam hdom) (HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn lam hdom) = (HigherHarmonicYoung.DeterminantVectors.dominantHighestWeightWitness hn lam hdom).polynomial

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

youngComplexPair lam (A (HigherYoungCyclicHighestSchur.dominantHighestRealVector hn lam hdom)) (A (HigherYoungCyclicHighestSchur.dominantHighestImaginaryVector hn lam hdom)) = HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair_isHomogeneous {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) :

(youngComplexPair lam p q).IsHomogeneous (∑ i : Fin (r + 1), lam i)

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

(HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A).IsHomogeneous (∑ i : Fin (r + 1), lam i)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_complexCombination_eigen {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) (a b : Fin k → Fin n) (c : Fin k → ℂ) (z : ℂ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (heigen : ∑ i : Fin k, c i • (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation (a i) (b i)) (youngComplexPair lam p q) = z • youngComplexPair lam p q) :

∑ i : Fin k, c i • (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation (a i) (b i)) (youngComplexPair lam (A p) (A q)) = z • youngComplexPair lam (A p) (A q)

@[simp]

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.complexAmbientRotation_self {r n : ℕ} (a : Fin n) :

HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a a = 0

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.ambientCartan_eq_twice_I_complexRotation {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (i : Fin (r + 1)) :

HigherHarmonicYoung.DeterminantVectors.ambientCartan hn i = (2 * Complex.I) • HigherYoungTwoRowLieIrreducibility.complexAmbientRotation (HigherHarmonicYoung.DeterminantVectors.oddCoordinate hn i) (HigherHarmonicYoung.DeterminantVectors.evenCoordinate hn i)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_complexRotation_eigen {r n : ℕ} (lam : Fin (r + 1) → ℕ) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) (a b : Fin n) (c z : ℂ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (heigen : c • (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a b) (youngComplexPair lam p q) = z • youngComplexPair lam p q) :

c • (HigherYoungTwoRowLieIrreducibility.complexAmbientRotation a b) (youngComplexPair lam (A p) (A q)) = z • youngComplexPair lam (A p) (A q)

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_ambientCartan_dominantHighest {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) (i : Fin (r + 1)) :

(HigherHarmonicYoung.DeterminantVectors.ambientCartan hn i) (HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A) = ↑(2 * lam i) • HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_totalAmbientCartan_dominantHighest {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) :

(HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan hn) (HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A) = ↑(2 * ∑ i : Fin (r + 1), lam i) • HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_dominantHighest_mem_ambientIsotropic_of_maximalCartan_range {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) (hrange : ∀ (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (d : ℕ), f.IsHomogeneous d → (HigherYoungAmbientCartanIsotropicEigenvalues.totalAmbientCartan hn) f = ↑(2 * d) • f → ∃ (q : HigherHarmonicYoung.BideterminantHighestLine.SourceMatrix (r + 1)), (HigherHarmonicYoung.nullSubstitution hn) q = f) :

HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

theorem MetricCodes.Spherical.HigherYoungArbitraryRankDominantHighestLinePreservation.rotationIntertwiner_dominantHighest_mem_ambientIsotropic {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) →ₗ[ℝ ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ A) :

HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn lam hdom A ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaiseTensorGram.arbitraryRowRaisingGramScalar_eq_tensorGramScalar {r n : ℕ} (high : Fin (r + 1) → ℕ) (row : Fin (r + 1)) :

ArbitraryRowRaisingSchurTraceGram.arbitraryRowRaisingGramScalar high row = ArbitraryRowRaiseLowerTensorTrace.arbitraryRowRaiseTensorGramScalar high row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaiseTensorGram.youngClebschRaise_arbitrary_inner_of_highestLine_and_cyclic {r n : ℕ} (high : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (ha : 0 < high row) (hn : 2 * (r + 1) ≤ n) (hdomhigh : Antitone high) (hdomlow : Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row)) (hhighest : HigherYoungArbitraryRankGelfandTsetlinHighestEigenpair.youngEndomorphismHighestPolynomial hn (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) hdomlow (LinearMap.adjoint (youngClebschRaise high (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) ⋯ row) ∘ₗ youngClebschRaise high (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) ⋯ row) ∈ IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row)) (hcyclic : HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan hn (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) hdomlow = ⊤) (p q : ↥(HarmonicYoungSpace (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row))) :

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

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

0 < ArbitraryRowRaiseLowerTensorTrace.arbitraryRowRaiseTensorGramScalar high row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowRaiseTensorGram.youngClebschRaise_arbitrary_inner_of_cyclic {r n : ℕ} (high : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (ha : 0 < high row) (hn : 2 * (r + 1) ≤ n) (hdomhigh : Antitone high) (hdomlow : Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row)) (hcyclic : HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan hn (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row) hdomlow = ⊤) (p q : ↥(HarmonicYoungSpace (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight high row))) :

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.PositiveRoot (r : ℕ) :

The positive root used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.PositiveRoot r = { z : Fin (r + 1) × Fin (r + 1) // z.1 < z.2 }

Instances For

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOperator {r : ℕ} (n : ℕ) (α : PositiveRoot r) :

PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n

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

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOperator n α = MetricCodes.Spherical.HigherHarmonicYoung.polarization r n (↑α).2 (↑α).1

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootOperator_apply {r n : ℕ} (α : PositiveRoot r) (p : PolynomialSpace r n) :

(positiveRootOperator n α) p = (polarization r n (↑α).2 (↑α).1) p

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign {α : Type u_1} [LinearOrder α] (s : Finset α) (a : α) :

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

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign s a = (-1) ^ {x ∈ s | x < a}.card

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRoot_predecessorCard_erase_lt {α : Type u_1} [LinearOrder α] (s : Finset α) {a b : α} (ha : a ∈ s) (hab : a < b) :

{x ∈ s | x < b}.card = {x ∈ s.erase a | x < b}.card + 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRoot_predecessors_erase_not_lt {α : Type u_1} [LinearOrder α] (s : Finset α) {a b : α} (hab : ¬a < b) :

{x ∈ s.erase a | x < b} = {x ∈ s | x < b}

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign_erase_of_lt {α : Type u_1} [LinearOrder α] (s : Finset α) {a b : α} (ha : a ∈ s) (hab : a < b) :

exteriorRootSign s b = -exteriorRootSign (s.erase a) b

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign_erase_of_not_lt {α : Type u_1} [LinearOrder α] (s : Finset α) {a b : α} (hab : ¬a < b) :

exteriorRootSign (s.erase a) b = exteriorRootSign s b

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign_erase_anticommute {α : Type u_1} [LinearOrder α] (s : Finset α) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (hab : a ≠ b) :

exteriorRootSign s a * exteriorRootSign (s.erase a) b = -(exteriorRootSign s b * exteriorRootSign (s.erase b) a)

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootWedge (r k : ℕ) :

The root wedge used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootWedge r k = { S : Finset (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.PositiveRoot r) // S.card = k }

Instances For

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFirst {r : ℕ} (α : PositiveRoot r) :

Fin (r + 1)

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

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFirst α = (↑α).1

Instances For

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootSecond {r : ℕ} (α : PositiveRoot r) :

Fin (r + 1)

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

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootSecond α = (↑α).2

Instances For

@[simp]

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

positiveRootFirst α < positiveRootSecond α

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

positiveRootFirst α ≠ positiveRootSecond α

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

The root charge used in the spherical-code argument.

Equations

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

Instances For

@[simp]

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

rootCharge α (positiveRootFirst α) = 1

@[simp]

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

rootCharge α (positiveRootSecond α) = -1

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootCharge_eq_zero_of_ne {r : ℕ} (α : PositiveRoot r) (i : Fin (r + 1)) (hfirst : i ≠ positiveRootFirst α) (hsecond : i ≠ positiveRootSecond α) :

rootCharge α i = 0

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge {r : ℕ} (S : Finset (PositiveRoot r)) (i : Fin (r + 1)) :

The root family charge used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge S i = ∑ α ∈ S, MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootCharge α i

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge_empty {r : ℕ} (i : Fin (r + 1)) :

rootFamilyCharge ∅ i = 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge_singleton {r : ℕ} (α : PositiveRoot r) (i : Fin (r + 1)) :

rootFamilyCharge {α} i = rootCharge α i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge_insert {r : ℕ} (S : Finset (PositiveRoot r)) (α : PositiveRoot r) (hα : α ∉ S) (i : Fin (r + 1)) :

rootFamilyCharge (insert α S) i = rootCharge α i + rootFamilyCharge S i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge_erase {r : ℕ} (S : Finset (PositiveRoot r)) (α : PositiveRoot r) (hα : α ∈ S) (i : Fin (r + 1)) :

rootFamilyCharge (S.erase α) i = rootFamilyCharge S i - rootCharge α i

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : Finset (PositiveRoot r)) (i : Fin (r + 1)) :

The signed root weight used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight lam S i = ↑(lam i) + MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootFamilyCharge S i

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight_insert {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : Finset (PositiveRoot r)) (α : PositiveRoot r) (hα : α ∉ S) (i : Fin (r + 1)) :

signedRootWeight lam (insert α S) i = signedRootWeight lam S i + rootCharge α i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight_erase {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : Finset (PositiveRoot r)) (α : PositiveRoot r) (hα : α ∈ S) (i : Fin (r + 1)) :

signedRootWeight lam (S.erase α) i = signedRootWeight lam S i - rootCharge α i

@[reducible, inline]

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

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

Equations

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

Instances For

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeWeight {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (i : Fin (r + 1)) :

The root wedge weight used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeWeight lam S i = (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.signedRootWeight lam (↑↑S) i).toNat

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeWeight_cast {r k : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam k) (i : Fin (r + 1)) :

↑(rootWedgeWeight lam S i) = signedRootWeight lam (↑↑S) i

@[reducible, inline]

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

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

Equations

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

Instances For

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootPolynomialChain (r n k : ℕ) :

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

Equations

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

Instances For

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootVector (r : ℕ) :

The root vector used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.RootVector r = (MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.PositiveRoot r →₀ ℝ)

Instances For

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootStructureConstant {r : ℕ} (α β γ : PositiveRoot r) :

ℝ

The root structure constant used in the spherical-code argument.

Equations

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

Instances For

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootBracket {r : ℕ} (α β : PositiveRoot r) :

RootVector r

The root bracket used in the spherical-code argument.

Equations

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

Instances For

@[simp]

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

(rootBracket α β) γ = rootStructureConstant α β γ

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction {r : ℕ} (n : ℕ) :

RootVector r →ₗ[ℝ ] PolynomialSpace r n →ₗ[ℝ ] PolynomialSpace r n

The linear extension of positive-root operators from finitely supported root vectors.

Equations

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

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction_single {r n : ℕ} (α : PositiveRoot r) (c : ℝ) :

((rootAction n) fun₀ | α => c) = c • positiveRootOperator n α

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

positiveRootOperator n α ∘ₗ positiveRootOperator n β - positiveRootOperator n β ∘ₗ positiveRootOperator n α = ∑ γ : PositiveRoot r, rootStructureConstant α β γ • positiveRootOperator n γ

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

(rootAction n) (rootBracket α β) = positiveRootOperator n α ∘ₗ positiveRootOperator n β - positiveRootOperator n β ∘ₗ positiveRootOperator n α

@[instance_reducible]

instance MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootLinearOrder (r : ℕ) :

LinearOrder (PositiveRoot r)

Equations

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

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeInsert {r k : ℕ} (T : RootWedge r k) (α : PositiveRoot r) (hα : α ∉ ↑T) :

RootWedge r (k + 1)

The root wedge insert used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeInsert T α hα = ⟨insert α ↑T, ⋯⟩

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeInsert_val {r k : ℕ} (T : RootWedge r k) (α : PositiveRoot r) (hα : α ∉ ↑T) :

↑(rootWedgeInsert T α hα) = insert α ↑T

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.realExteriorRootSign {α : Type u_1} [LinearOrder α] (S : Finset α) (a : α) :

ℝ

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

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.realExteriorRootSign S a = ↑(MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.exteriorRootSign S a)

Instances For

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionBoundary (r n k : ℕ) :

RootPolynomialChain r n (k + 1) →ₗ[ℝ ] RootPolynomialChain r n k

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

Equations

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

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootActionBoundary_apply (r n k : ℕ) (f : RootPolynomialChain r n (k + 1)) (T : RootWedge r k) :

(rootActionBoundary r n k) f T = ∑ α : PositiveRoot r, if hα : α ∈ ↑T then 0 else realExteriorRootSign (insert α ↑T) α • (positiveRootOperator n α) (f (rootWedgeInsert T α hα))

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.realExteriorRootSign_erase_anticommute {α : Type u_1} [LinearOrder α] (S : Finset α) {a b : α} (ha : a ∈ S) (hb : b ∈ S) (hab : a ≠ b) :

realExteriorRootSign S a * realExteriorRootSign (S.erase a) b = -(realExteriorRootSign S b * realExteriorRootSign (S.erase b) a)

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.lowerRootWeight {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (i : Fin (r + 1)) :

The lower root weight used in the spherical-code argument.

Equations

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

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.lowerRootWeight_first {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) :

lowerRootWeight μ α (positiveRootFirst α) = μ (positiveRootFirst α) - 1

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.lowerRootWeight_second {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) :

lowerRootWeight μ α (positiveRootSecond α) = μ (positiveRootSecond α) + 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.lowerRootWeight_other {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (i : Fin (r + 1)) (hfirst : i ≠ positiveRootFirst α) (hsecond : i ≠ positiveRootSecond α) :

lowerRootWeight μ α i = μ i

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootTransferBase {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) :

Fin (r + 1) → ℕ

The row weight obtained by subtracting one at the first endpoint of a positive root.

Equations

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

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootTransferSource_eq {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) :

μ = Function.update (rootTransferBase μ α) (positiveRootFirst α) (rootTransferBase μ α (positiveRootFirst α) + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootTransferTarget_eq {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) :

lowerRootWeight μ α = Function.update (rootTransferBase μ α) (positiveRootSecond α) (rootTransferBase μ α (positiveRootSecond α) + 1)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedPositiveRootOperator {r : ℕ} (n : ℕ) (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) :

JointHarmonicWeightSpace n μ →ₗ[ℝ ] JointHarmonicWeightSpace n (lowerRootWeight μ α)

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

Equations

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

Instances For

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedPositiveRootOperatorStar {r : ℕ} (n : ℕ) (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) :

JointHarmonicWeightSpace n (lowerRootWeight μ α) →ₗ[ℝ ] JointHarmonicWeightSpace n μ

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

Equations

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

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedPositiveRootOperator_coe {r n : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) (p : JointHarmonicWeightSpace n μ) :

↑↑((weightedPositiveRootOperator n μ α hμ) p) = (positiveRootOperator n α) ↑↑p

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedPositiveRootOperatorStar_coe {r n : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) (q : JointHarmonicWeightSpace n (lowerRootWeight μ α)) :

↑↑((weightedPositiveRootOperatorStar n μ α hμ) q) = (polarization r n (positiveRootFirst α) (positiveRootSecond α)) ↑↑q

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.lowerRootWeight_cast {r : ℕ} (μ : Fin (r + 1) → ℕ) (α : PositiveRoot r) (hμ : 0 < μ (positiveRootFirst α)) (i : Fin (r + 1)) :

↑(lowerRootWeight μ α i) = ↑(μ i) - rootCharge α i

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert {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) :

AdmissibleRootWedge lam (k + 1)

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

Equations

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

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_val {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) :

↑↑(rootAdmissibleInsert lam T α hα hadm) = insert α ↑↑T

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_weight_charge {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) (i : Fin (r + 1)) :

↑(rootWedgeWeight lam (rootAdmissibleInsert lam T α hα hadm) i) = ↑(rootWedgeWeight lam T i) + rootCharge α i

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_first_pos {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) :

0 < rootWedgeWeight lam (rootAdmissibleInsert lam T α hα hadm) (positiveRootFirst α)

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAdmissibleInsert_lowerRootWeight {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) :

lowerRootWeight (rootWedgeWeight lam (rootAdmissibleInsert lam T α hα hadm)) α = rootWedgeWeight lam T

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.jointHarmonicWeightCast {r : ℕ} (n : ℕ) (μ ν : Fin (r + 1) → ℕ) (h : μ = ν) :

JointHarmonicWeightSpace n μ ≃ₗ[ℝ ] JointHarmonicWeightSpace n ν

The joint harmonic weight cast used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.jointHarmonicWeightCast n μ ν h = h ▸ LinearEquiv.refl ℝ (MetricCodes.Spherical.HigherHarmonicYoung.JointHarmonicWeightSpace n μ)

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.jointHarmonicWeightCast_coe {r n : ℕ} (μ ν : Fin (r + 1) → ℕ) (h : μ = ν) (p : JointHarmonicWeightSpace n μ) :

↑↑((jointHarmonicWeightCast n μ ν h) p) = ↑↑p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorRootEdge {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 (rootAdmissibleInsert lam T α hα hadm)) →ₗ[ℝ ] JointHarmonicWeightSpace n (rootWedgeWeight lam T)

The weighted exterior root edge used in the spherical-code argument.

Equations

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

Instances For

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.weightedExteriorActionDifferential {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) :

RootJointHarmonicChain n lam (k + 1) →ₗ[ℝ ] RootJointHarmonicChain n lam k

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

Equations

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

Instances For

@[simp]

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

(weightedExteriorActionDifferential n lam k) f 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) α • (weightedExteriorRootEdge n lam T α hα hadm) (f (rootAdmissibleInsert lam T α hα hadm)) else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal (r n k : ℕ) :

Ideal (PolynomialSpace r n)

The ideal generated by the first k Gram quadratic relations.

Equations

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

Instances For

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) :

Submodule ℝ ↥(youngMultihomogeneousSubmodule n lam)

The multihomogeneous weight submodule lying in the ideal of the first k Gram relations.

Equations

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

Instances For

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.YoungGramPrefixWeightQuotient {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) :

The multihomogeneous weight space modulo the first k Gram relations.

Equations

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

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_youngGramPrefixWeightSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (k : ℕ) (p : ↥(youngMultihomogeneousSubmodule n lam)) :

p ∈ youngGramPrefixWeightSubmodule n lam k ↔ ↑p ∈ youngGramPrefixIdeal r n k

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_zero (r n : ℕ) :

youngGramPrefixIdeal r n 0 = ⊥

@[simp]

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

youngGramPrefixWeightSubmodule n lam 0 = ⊥

def MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight (r n : ℕ) :

Fin ((r + 1) * n) → Fin (r + 1) → ℕ

The row multidegree of a polynomial variable, given by one in its row and zero elsewhere.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight r n x = Pi.single (finProdFinEquiv.symm x).1 1

Instances For

def MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree {r : ℕ} (i j : Fin (r + 1)) :

Fin (r + 1) → ℕ

The row multidegree of the Gram pairing between rows i and j.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairDegree i j = Pi.single i 1 + Pi.single j 1

Instances For

@[simp]

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

youngVariableRowWeight r n (variableIndex i k) = Pi.single i 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngVariableRowWeight_weight {r n : ℕ} (d : Fin ((r + 1) * n) →₀ ℕ) :

(Finsupp.weight (youngVariableRowWeight r n)) d = fun (i : Fin (r + 1)) => Finsupp.degree (rowExponent d i)

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

youngMultihomogeneousSubmodule n lam = MvPolynomial.weightedHomogeneousSubmodule ℝ (youngVariableRowWeight r n) lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngWeightedComponent_mem_youngMultihomogeneousSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : PolynomialSpace r n) :

(MvPolynomial.weightedHomogeneousComponent (youngVariableRowWeight r n) lam) p ∈ youngMultihomogeneousSubmodule n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowPairingPolynomial_isWeightedHomogeneous {r n : ℕ} (i j : Fin (r + 1)) :

MvPolynomial.IsWeightedHomogeneous (youngVariableRowWeight r n) (rowPairingPolynomial i j) (youngGramPairDegree i j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowPairingPolynomial_isHomogeneousElem {r n : ℕ} (i j : Fin (r + 1)) :

SetLike.IsHomogeneousElem (MvPolynomial.weightedHomogeneousSubmodule ℝ (youngVariableRowWeight r n)) (rowPairingPolynomial i j)

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

Ideal.IsHomogeneous (MvPolynomial.weightedHomogeneousSubmodule ℝ (youngVariableRowWeight r n)) (youngGramPrefixIdeal r n k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_weightedHomogeneousComponent_mem {r n k : ℕ} {p : PolynomialSpace r n} (hp : p ∈ youngGramPrefixIdeal r n k) (lam : Fin (r + 1) → ℕ) :

(MvPolynomial.weightedHomogeneousComponent (youngVariableRowWeight r n) lam) p ∈ youngGramPrefixIdeal r n k

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

Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam k) + Module.finrank ℝ ↥(youngGramPrefixWeightSubmodule n lam k) = ∏ i : Fin (r + 1), (n + lam i - 1).choose (lam i)

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

(MvPolynomial.weightedHomogeneousComponent (youngVariableRowWeight r n) (youngGramPairDegree i j + mu)) (rowPairingPolynomial i j * p) = rowPairingPolynomial i j * (MvPolynomial.weightedHomogeneousComponent (youngVariableRowWeight r n) mu) p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairWeightMultiplication {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (mu : Fin (r + 1) → ℕ) :

↥(youngMultihomogeneousSubmodule n mu) →ₗ[ℝ ] ↥(youngMultihomogeneousSubmodule n (youngGramPairDegree i j + mu))

Multiplication by a Gram pairing, with the corresponding increase in row multidegree.

Equations

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

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_succ {r n k : ℕ} (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) :

youngGramPrefixIdeal r n (k + 1) = youngGramPrefixIdeal r n k ⊔ Ideal.span {(ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)[k]}

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_le_succ {r n k : ℕ} (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) :

youngGramPrefixIdeal r n k ≤ youngGramPrefixIdeal r n (k + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule_le_succ {r n k : ℕ} (lam : Fin (r + 1) → ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) :

youngGramPrefixWeightSubmodule n lam k ≤ youngGramPrefixWeightSubmodule n lam (k + 1)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixQuotientNext {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) :

YoungGramPrefixWeightQuotient n lam k →ₗ[ℝ ] YoungGramPrefixWeightQuotient n lam (k + 1)

The natural quotient map obtained by imposing the next Gram relation.

Equations

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

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixQuotientNext_surjective {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) :

Function.Surjective ⇑(youngGramPrefixQuotientNext n lam k hk)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairPrefixQuotientMultiplication {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (mu : Fin (r + 1) → ℕ) (k : ℕ) :

YoungGramPrefixWeightQuotient n mu k →ₗ[ℝ ] YoungGramPrefixWeightQuotient n (youngGramPairDegree i j + mu) k

Multiplication by a Gram pairing induced on the quotient by the first k Gram relations.

Equations

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

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairPrefixQuotientMultiplication_injective {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (mu : Fin (r + 1) → ℕ) (k : ℕ) (hreg : ∀ (p : PolynomialSpace r n), rowPairingPolynomial i j * p ∈ youngGramPrefixIdeal r n k → p ∈ youngGramPrefixIdeal r n k) :

Function.Injective ⇑(youngGramPairPrefixQuotientMultiplication n i j mu k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPairPrefixQuotient_exact {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (mu : Fin (r + 1) → ℕ) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) (hgen : (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)[k] = rowPairingPolynomial i j) :

(youngGramPairPrefixQuotientMultiplication n i j mu k).range = (youngGramPrefixQuotientNext n (youngGramPairDegree i j + mu) k hk).ker

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngGramPrefixWeightQuotient_succ_of_fits {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (mu : Fin (r + 1) → ℕ) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) (hgen : (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)[k] = rowPairingPolynomial i j) (hreg : ∀ (p : PolynomialSpace r n), rowPairingPolynomial i j * p ∈ youngGramPrefixIdeal r n k → p ∈ youngGramPrefixIdeal r n k) :

Module.finrank ℝ (YoungGramPrefixWeightQuotient n (youngGramPairDegree i j + mu) (k + 1)) + Module.finrank ℝ (YoungGramPrefixWeightQuotient n mu k) = Module.finrank ℝ (YoungGramPrefixWeightQuotient n (youngGramPairDegree i j + mu) k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngWeightedComponent_gram_mul_eq_zero_of_overweight {r n : ℕ} (i j : Fin (r + 1)) (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (hover : lam a < youngGramPairDegree i j a) (p : PolynomialSpace r n) :

(MvPolynomial.weightedHomogeneousComponent (youngVariableRowWeight r n) lam) (rowPairingPolynomial i j * p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightSubmodule_succ_eq_of_overweight {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) (hgen : (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)[k] = rowPairingPolynomial i j) (hover : lam a < youngGramPairDegree i j a) :

youngGramPrefixWeightSubmodule n lam (k + 1) = youngGramPrefixWeightSubmodule n lam k

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngGramPrefixWeightQuotient_succ_of_overweight {r : ℕ} (n : ℕ) (i j : Fin (r + 1)) (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1)) (k : ℕ) (hk : k < (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length) (hgen : (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)[k] = rowPairingPolynomial i j) (hover : lam a < youngGramPairDegree i j a) :

Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam (k + 1)) = Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam k)

def MetricCodes.Spherical.HigherHarmonicYoung.gramPairRowDegree {r : ℕ} (z : ArbitraryRankMixedTraceRegularity.UpperGramPair r) (i : Fin (r + 1)) :

The gram pair row degree used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.gramPairRowDegree z i = (if (↑z).1 = i then 1 else 0) + if (↑z).2 = i then 1 else 0

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPairRowDegree_eq_youngGramPairDegree {r : ℕ} (z : ArbitraryRankMixedTraceRegularity.UpperGramPair r) :

gramPairRowDegree z = youngGramPairDegree (↑z).1 (↑z).2

def MetricCodes.Spherical.HigherHarmonicYoung.gramFamilyRowDegree {r : ℕ} (s : Finset (ArbitraryRankMixedTraceRegularity.UpperGramPair r)) (i : Fin (r + 1)) :

The gram family row degree used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.gramFamilyRowDegree s i = ∑ z ∈ s, MetricCodes.Spherical.HigherHarmonicYoung.gramPairRowDegree z i

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramFamilyRowDegree_insert {r : ℕ} (s : Finset (ArbitraryRankMixedTraceRegularity.UpperGramPair r)) (z : ArbitraryRankMixedTraceRegularity.UpperGramPair r) (hz : z ∉ s) (i : Fin (r + 1)) :

gramFamilyRowDegree (insert z s) i = gramPairRowDegree z i + gramFamilyRowDegree s i

def MetricCodes.Spherical.HigherHarmonicYoung.shiftedYoungAmbientCoefficient {r : ℕ} (n : ℕ) (lam delta : Fin (r + 1) → ℕ) :

The shifted young ambient coefficient used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.shiftedYoungAmbientCoefficient n lam delta = ∏ i : Fin (r + 1), if delta i ≤ lam i then (n + (lam i - delta i) - 1).choose (lam i - delta i) else 0

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.shiftedYoungAmbientCoefficient_eq_zero_of_not_le {r n : ℕ} (lam delta : Fin (r + 1) → ℕ) (i : Fin (r + 1)) (hi : lam i < delta i) :

shiftedYoungAmbientCoefficient n lam delta = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.shiftedYoungAmbientCoefficient_add {r n : ℕ} (lam delta epsilon : Fin (r + 1) → ℕ) (hdelta : ∀ (i : Fin (r + 1)), delta i ≤ lam i) :

(shiftedYoungAmbientCoefficient n lam fun (i : Fin (r + 1)) => delta i + epsilon i) = shiftedYoungAmbientCoefficient n (fun (i : Fin (r + 1)) => lam i - delta i) epsilon

def MetricCodes.Spherical.HigherHarmonicYoung.gramKoszulCoefficient {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (s : Finset (ArbitraryRankMixedTraceRegularity.UpperGramPair r)) :

The gram koszul coefficient used in the spherical-code argument.

Equations

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

Instances For

@[simp]

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

gramKoszulCoefficient n lam ∅ = ↑(∏ i : Fin (r + 1), (n + lam i - 1).choose (lam i))

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramKoszulCoefficient_insert {r n : ℕ} (lam : Fin (r + 1) → ℕ) (s : Finset (ArbitraryRankMixedTraceRegularity.UpperGramPair r)) (z : ArbitraryRankMixedTraceRegularity.UpperGramPair r) (hz : z ∉ s) :

gramKoszulCoefficient n lam (insert z s) = gramKoszulCoefficient n lam s - if ∀ (i : Fin (r + 1)), gramPairRowDegree z i ≤ lam i then gramKoszulCoefficient n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree z i) s else 0

def MetricCodes.Spherical.HigherHarmonicYoung.fullGramKoszulCoefficient {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) :

The full gram koszul coefficient used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.fullGramKoszulCoefficient n lam = MetricCodes.Spherical.HigherHarmonicYoung.gramKoszulCoefficient n lam Finset.univ

Instances For

Finset (ArbitraryRankMixedTraceRegularity.UpperGramPair r)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset (r k : ℕ) :

The first k upper Gram pairs in the fixed finite enumeration.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset r k = (List.take k Finset.univ.toList).toFinset

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset_zero (r : ℕ) :

gramPrefixPairFinset r 0 = ∅

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset_length (r n : ℕ) :

gramPrefixPairFinset r (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length = Finset.univ

ArbitraryRankMixedTraceRegularity.UpperGramPair r

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt {r : ℕ} (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) :

The upper Gram pair at position k in the fixed finite enumeration.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt k = Finset.univ.toList.get ⟨↑k, ⋯⟩

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPrefixPairFinset_succ {r : ℕ} (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) :

gramPrefixPairFinset r (↑k + 1) = insert (gramPairAt k) (gramPrefixPairFinset r ↑k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt_not_mem_gramPrefixPairFinset {r : ℕ} (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) :

gramPairAt k ∉ gramPrefixPairFinset r ↑k

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramKoszulCoefficient_prefix_succ {r n : ℕ} (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) :

gramKoszulCoefficient n lam (gramPrefixPairFinset r (↑k + 1)) = gramKoszulCoefficient n lam (gramPrefixPairFinset r ↑k) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (gramPairAt k) i ≤ lam i then gramKoszulCoefficient n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (gramPairAt k) i) (gramPrefixPairFinset r ↑k) else 0

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

Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam 0) = ∏ i : Fin (r + 1), (n + lam i - 1).choose (lam i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngGramPrefixWeightQuotient_eq_gramKoszulCoefficient_of_recurrence {r n : ℕ} (hstep : ∀ (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))), ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam (↑k + 1))) = ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam ↑k)) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (gramPairAt k) i ≤ lam i then ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (gramPairAt k) i) ↑k)) else 0) (k : ℕ) (hk : k ≤ Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r)) (lam : Fin (r + 1) → ℕ) :

↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam k)) = gramKoszulCoefficient n lam (gramPrefixPairFinset r k)

def MetricCodes.Spherical.HigherHarmonicYoung.weylShift {r : ℕ} (lam : Fin (r + 1) → ℕ) (σ : Equiv.Perm (Fin (r + 1))) (i : Fin (r + 1)) :

The weyl shift used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.weylShift lam σ i = ↑(lam i) - ↑↑i + ↑↑(σ i)

Instances For

def MetricCodes.Spherical.HigherHarmonicYoung.signedFullGramKoszulCoefficient {r : ℕ} (n : ℕ) (mu : Fin (r + 1) → ℤ) :

The signed full gram koszul coefficient used in the spherical-code argument.

Equations

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

Instances For

def MetricCodes.Spherical.HigherHarmonicYoung.alternatingGramKoszulCoefficient {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) :

The alternating gram koszul coefficient used in the spherical-code argument.

Equations

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

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixIdeal_length (r n : ℕ) :

youngGramPrefixIdeal r n (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length = youngGramRadialIdeal r n

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

youngGramPrefixWeightSubmodule n lam (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length = youngGramRadialWeightSubmodule n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramQuadraticList_length_eq_upperGramPair_card (r n : ℕ) :

(ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).length = Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r)

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramQuadraticList_getElem_gramPairAt {r n : ℕ} (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) :

(ArbitraryRankMixedTraceRegularity.gramQuadraticList r n).get ⟨↑k, ⋯⟩ = ArbitraryRankMixedTraceRegularity.gramPairPolynomial n (gramPairAt k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramPairAt_mul_mem_prefix_of_weaklyRegular {r n : ℕ} (hregular : RingTheory.Sequence.IsWeaklyRegular (PolynomialSpace r n) (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) (p : PolynomialSpace r n) (hp : ArbitraryRankMixedTraceRegularity.gramPairPolynomial n (gramPairAt k) * p ∈ youngGramPrefixIdeal r n ↑k) :

p ∈ youngGramPrefixIdeal r n ↑k

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightQuotient_signed_recurrence_of_fits_and_overweight {r n : ℕ} (hfits : ∀ (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) (mu : Fin (r + 1) → ℕ), Module.finrank ℝ (YoungGramPrefixWeightQuotient n (youngGramPairDegree (↑(gramPairAt k)).1 (↑(gramPairAt k)).2 + mu) (↑k + 1)) + Module.finrank ℝ (YoungGramPrefixWeightQuotient n mu ↑k) = Module.finrank ℝ (YoungGramPrefixWeightQuotient n (youngGramPairDegree (↑(gramPairAt k)).1 (↑(gramPairAt k)).2 + mu) ↑k)) (hoverweight : ∀ (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)), lam i < youngGramPairDegree (↑(gramPairAt k)).1 (↑(gramPairAt k)).2 i → Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam (↑k + 1)) = Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam ↑k)) (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) :

↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam (↑k + 1))) = ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam ↑k)) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (gramPairAt k) i ≤ lam i then ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (gramPairAt k) i) ↑k)) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngGramPrefixWeightQuotient_signed_recurrence_of_weaklyRegular {r n : ℕ} (hregular : RingTheory.Sequence.IsWeaklyRegular (PolynomialSpace r n) (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)) (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))) :

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngGramRadialWeightQuotient_eq_fullGramKoszulCoefficient_of_recurrence {r n : ℕ} (hstep : ∀ (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))), ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam (↑k + 1))) = ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam ↑k)) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (gramPairAt k) i ≤ lam i then ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (gramPairAt k) i) ↑k)) else 0) (lam : Fin (r + 1) → ℕ) :

↑(Module.finrank ℝ (YoungGramRadialWeightQuotient n lam)) = fullGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_jointHarmonicWeight_eq_fullGramKoszulCoefficient_of_recurrence {r n : ℕ} (hstep : ∀ (lam : Fin (r + 1) → ℕ) (k : Fin (Fintype.card (ArbitraryRankMixedTraceRegularity.UpperGramPair r))), ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam (↑k + 1))) = ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n lam ↑k)) - if ∀ (i : Fin (r + 1)), gramPairRowDegree (gramPairAt k) i ≤ lam i then ↑(Module.finrank ℝ (YoungGramPrefixWeightQuotient n (fun (i : Fin (r + 1)) => lam i - gramPairRowDegree (gramPairAt k) i) ↑k)) else 0) (lam : Fin (r + 1) → ℕ) :

↑(Module.finrank ℝ (JointHarmonicWeightSpace n lam)) = fullGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_jointHarmonicWeight_eq_fullGramKoszulCoefficient {r n : ℕ} (hregular : RingTheory.Sequence.IsWeaklyRegular (PolynomialSpace r n) (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)) (lam : Fin (r + 1) → ℕ) :

↑(Module.finrank ℝ (JointHarmonicWeightSpace n lam)) = fullGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_jointHarmonicWeight_eq_fullGramKoszulCoefficient_of_stable {r n : ℕ} (hn : 2 * r < n) (lam : Fin (r + 1) → ℕ) :

↑(Module.finrank ℝ (JointHarmonicWeightSpace n lam)) = fullGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.bgg_range_eq_ker_of_hodgeLaplacian_injective {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ G] (d : F →ₗ[ℝ ] E) (e : G →ₗ[ℝ ] F) (hchain : d ∘ₗ e = 0) (hinj : Function.Injective ⇑(LinearMap.adjoint d ∘ₗ d + e ∘ₗ LinearMap.adjoint e)) :

e.range = d.ker

theorem MetricCodes.Spherical.HigherHarmonicYoung.bgg_range_eq_ker_of_fischerCore_hodgeLaplacian_injective {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [AddCommGroup G] [Module ℝ G] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ G] (cE : InnerProductSpace.Core ℝ E) (cF : InnerProductSpace.Core ℝ F) (cG : InnerProductSpace.Core ℝ G) (d : F →ₗ[ℝ ] E) (dStar : E →ₗ[ℝ ] F) (e : G →ₗ[ℝ ] F) (eStar : F →ₗ[ℝ ] G) (hdStar : ∀ (x : E) (y : F), inner ℝ (dStar x) y = inner ℝ x (d y)) (heStar : ∀ (x : F) (y : G), inner ℝ (eStar x) y = inner ℝ x (e y)) (hchain : d ∘ₗ e = 0) (hinj : Function.Injective ⇑(dStar ∘ₗ d + e ∘ₗ eStar)) :

e.range = d.ker

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.signedJointHarmonicWeightDimension {r : ℕ} (n : ℕ) (mu : Fin (r + 1) → ℤ) :

The signed joint harmonic weight dimension used in the spherical-code argument.

Equations

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

Instances For

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

The alternating joint harmonic weight dimension used in the spherical-code argument.

Equations

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

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.alternatingJointHarmonicWeightDimension_eq_alternatingGramKoszul {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hgram : ∀ (mu : Fin (r + 1) → ℕ), ↑(Module.finrank ℝ (JointHarmonicWeightSpace n mu)) = fullGramKoszulCoefficient n mu) :

alternatingJointHarmonicWeightDimension n lam = alternatingGramKoszulCoefficient n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.alternatingJointHarmonicWeightDimension_eq_alternatingGramKoszul_of_stable {r n : ℕ} (hn : 2 * r < n) (lam : Fin (r + 1) → ℕ) :

alternatingJointHarmonicWeightDimension n lam = alternatingGramKoszulCoefficient n lam

@[implicit_reducible]

def MetricCodes.Spherical.HigherHarmonicYoung.finitePiFischerCore {ι : Type u_1} [Fintype ι] (V : ι → Type u_2) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℝ (V i)] (c : (i : ι) → InnerProductSpace.Core ℝ (V i)) :

InnerProductSpace.Core ℝ ((i : ι) → V i)

The inner product core on a finite product, obtained by summing the component Fischer cores.

Equations

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

Instances For

def MetricCodes.Spherical.HigherHarmonicYoung.finiteFischerRootLaplacian {ι : Type u_1} {V : Type u_2} [Fintype ι] [AddCommGroup V] [Module ℝ V] (W : ι → Type u_3) [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℝ (W i)] (A : (i : ι) → V →ₗ[ℝ ] W i) (Astar : (i : ι) → W i →ₗ[ℝ ] V) :

V →ₗ[ℝ ] V

The finite fischer root laplacian used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.finiteFischerRootLaplacian W A Astar = ∑ i : ι, Astar i ∘ₗ A i

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.finiteFischerRootLaplacian_energy {ι : Type u_1} {V : Type u_2} [Fintype ι] [AddCommGroup V] [Module ℝ V] (cV : InnerProductSpace.Core ℝ V) (W : ι → Type u_3) [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℝ (W i)] (cW : (i : ι) → InnerProductSpace.Core ℝ (W i)) (A : (i : ι) → V →ₗ[ℝ ] W i) (Astar : (i : ι) → W i →ₗ[ℝ ] V) (hadjoint : ∀ (i : ι) (x : W i) (y : V), inner ℝ ((Astar i) x) y = inner ℝ x ((A i) y)) (x : V) :

inner ℝ x ((finiteFischerRootLaplacian W A Astar) x) = ∑ i : ι, inner ℝ ((A i) x) ((A i) x)

theorem MetricCodes.Spherical.HigherHarmonicYoung.finiteFischerRootLaplacian_eq_zero_iff {ι : Type u_1} {V : Type u_2} [Fintype ι] [AddCommGroup V] [Module ℝ V] (cV : InnerProductSpace.Core ℝ V) (W : ι → Type u_3) [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℝ (W i)] (cW : (i : ι) → InnerProductSpace.Core ℝ (W i)) (A : (i : ι) → V →ₗ[ℝ ] W i) (Astar : (i : ι) → W i →ₗ[ℝ ] V) (hadjoint : ∀ (i : ι) (x : W i) (y : V), inner ℝ ((Astar i) x) y = inner ℝ x ((A i) y)) (x : V) :

(finiteFischerRootLaplacian W A Astar) x = 0 ↔ ∀ (i : ι), (A i) x = 0

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.ActivePositiveRoot {r : ℕ} (lam : Fin (r + 1) → ℕ) :

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

Equations

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

Instances For

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

Fin (r + 1) → ℕ

The active root base weight used in the spherical-code argument.

Equations

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

Instances For

@[simp]

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

Function.update (activeRootBaseWeight lam α) (positiveRootSecond ↑α) (activeRootBaseWeight lam α (positiveRootSecond ↑α) + 1) = lam

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

Fin (r + 1) → ℕ

The active root raised weight used in the spherical-code argument.

Equations

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

Instances For

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

JointHarmonicWeightSpace n lam →ₗ[ℝ ] JointHarmonicWeightSpace n (activeRootRaisedWeight lam α)

The active positive root raise used in the spherical-code argument.

Equations

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

Instances For

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

JointHarmonicWeightSpace n (activeRootRaisedWeight lam α) →ₗ[ℝ ] JointHarmonicWeightSpace n lam

The active positive root lower used in the spherical-code argument.

Equations

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

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activePositiveRootRaise_coe {r n : ℕ} (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) (p : JointHarmonicWeightSpace n lam) :

↑↑((activePositiveRootRaise n lam α) p) = (polarization r n (positiveRootFirst ↑α) (positiveRootSecond ↑α)) ↑↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.activePositiveRoot_fischer_adjoint {r n : ℕ} (lam : Fin (r + 1) → ℕ) (α : ActivePositiveRoot lam) (p : JointHarmonicWeightSpace n (activeRootRaisedWeight lam α)) (q : JointHarmonicWeightSpace n lam) :

inner ℝ ((activePositiveRootLower n lam α) p) q = inner ℝ p ((activePositiveRootRaise n lam α) q)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFischerLaplacian {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) :

JointHarmonicWeightSpace n lam →ₗ[ℝ ] JointHarmonicWeightSpace n lam

The finite Fischer Laplacian associated with the active positive-root raising maps.

Equations

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

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFischerLaplacian_eq_zero_iff {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : JointHarmonicWeightSpace n lam) :

(positiveRootFischerLaplacian n lam) p = 0 ↔ ∀ (α : ActivePositiveRoot lam), (activePositiveRootRaise n lam α) p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.positiveRootFischerLaplacian_eq_zero_iff_harmonicYoung {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : JointHarmonicWeightSpace n lam) :

(positiveRootFischerLaplacian n lam) p = 0 ↔ ↑↑p ∈ harmonicYoungSubmodule lam

@[implicit_reducible]

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicChainFischerCore {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (k : ℕ) :

InnerProductSpace.Core ℝ (RootJointHarmonicChain n lam k)

The root joint harmonic chain fischer core component.

Equations

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

Instances For

@[simp]

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

inner ℝ p q = ∑ S : AdmissibleRootWedge lam k, inner ℝ (p S) (q S)

def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.emptyAdmissibleRootWedge {r : ℕ} (lam : Fin (r + 1) → ℕ) :

AdmissibleRootWedge lam 0

The empty admissible root wedge used in the spherical-code argument.

Equations

MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.emptyAdmissibleRootWedge lam = ⟨⟨∅, ⋯⟩, ⋯⟩

Instances For

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.admissibleRootWedge_zero_eq_empty {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam 0) :

S = emptyAdmissibleRootWedge lam

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.admissibleRootWedgeZeroUnique {r : ℕ} (lam : Fin (r + 1) → ℕ) :

Unique (AdmissibleRootWedge lam 0)

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootWedgeWeight_degree_zero {r : ℕ} (lam : Fin (r + 1) → ℕ) (S : AdmissibleRootWedge lam 0) :

rootWedgeWeight lam S = lam

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootJointHarmonicDegreeZeroEquiv {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) :

RootJointHarmonicChain n lam 0 ≃ₗ[ℝ ] JointHarmonicWeightSpace n lam

The root joint harmonic degree zero equiv used in the spherical-code argument.

Equations

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

Instances For

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroPositiveCochain {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) :

RootJointHarmonicChain n lam 0 →ₗ[ℝ ] (α : ActivePositiveRoot lam) → JointHarmonicWeightSpace n (activeRootRaisedWeight lam α)

The root degree zero positive cochain used in the spherical-code argument.

Equations

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

Instances For

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroPositiveCochain_apply {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : RootJointHarmonicChain n lam 0) (α : ActivePositiveRoot lam) :

(rootDegreeZeroPositiveCochain n lam) p α = (activePositiveRootRaise n lam α) ((rootJointHarmonicDegreeZeroEquiv n lam) p)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootDegreeZeroFischerLaplacian {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) :

RootJointHarmonicChain n lam 0 →ₗ[ℝ ] RootJointHarmonicChain n lam 0

The positive-root Fischer Laplacian transported to root-chain degree zero.

Equations

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

Instances For

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

(rootDegreeZeroPositiveCochain n lam) p = 0 ↔ ↑↑((rootJointHarmonicDegreeZeroEquiv n lam) p) ∈ harmonicYoungSubmodule lam

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

(rootDegreeZeroFischerLaplacian n lam) p = 0 ↔ ↑↑((rootJointHarmonicDegreeZeroEquiv n lam) p) ∈ harmonicYoungSubmodule lam

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

(rootDegreeZeroPositiveCochain n lam) p = 0 ↔ (rootDegreeZeroFischerLaplacian n lam) p = 0

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

Module.finrank ℝ ↥(rootDegreeZeroPositiveCochain n lam).ker = Module.finrank ℝ ↥(HarmonicYoungSpace lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.finiteChain_eulerCharacteristic_eq_degreeZero_sub_boundary_add_top (V : ℕ → Type u_1) [(k : ℕ) → AddCommGroup (V k)] [(k : ℕ) → Module ℝ (V k)] [∀ (k : ℕ), FiniteDimensional ℝ (V k)] (d : (k : ℕ) → V (k + 1) →ₗ[ℝ ] V k) (N : ℕ) (hexact : ∀ k < N, (d (k + 1)).range = (d k).ker) :

∑ k ∈ Finset.range (N + 1), (-1) ^ k * ↑(Module.finrank ℝ (V k)) = ↑(Module.finrank ℝ (V 0)) - ↑(Module.finrank ℝ ↥(d 0).range) + (-1) ^ N * ↑(Module.finrank ℝ ↥(d N).range)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_reversed_vandermonde {R : Type u_1} [CommRing R] {r : ℕ} (x : Fin (r + 1) → R) :

(Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j)) = ∏ i : Fin (r + 1), ∏ j > i, (x i - x j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_quadratic_projective_vandermonde {R : Type u_1} [CommRing R] {r : ℕ} (x : Fin (r + 1) → R) :

(Matrix.projVandermonde (fun (i : Fin (r + 1)) => 1 + x i ^ 2) x).det = (Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j)) * ∏ i : Fin (r + 1), ∏ j > i, (1 - x i * x j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.upper_gram_pair_product {R : Type u_1} [CommRing R] {r : ℕ} (x : Fin (r + 1) → R) :

(∏ i : Fin (r + 1), (1 - x i ^ 2)) * ∏ i : Fin (r + 1), ∏ j > i, (1 - x i * x j) = ∏ i : Fin (r + 1), ∏ j ≥ i, (1 - x i * x j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.orthogonal_denominator_entry {R : Type u_1} [CommRing R] (x : R) (r j : ℕ) (hj : j ≤ r) :

x ^ (r - j) - x ^ (r + j + 2) = (1 - x ^ 2) * x ^ (r - j) * ∑ k ∈ Finset.range (j + 1), x ^ (2 * k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.chebyshevS_isMonicOfDegree (R : Type u_1) [CommRing R] [Nontrivial R] (j : ℕ) :

(Polynomial.Chebyshev.S R ↑j).IsMonicOfDegree j

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.chebyshevS_monic (R : Type u_1) [CommRing R] [Nontrivial R] (j : ℕ) :

(Polynomial.Chebyshev.S R ↑j).Monic

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.chebyshevS_natDegree (R : Type u_1) [CommRing R] [Nontrivial R] (j : ℕ) :

(Polynomial.Chebyshev.S R ↑j).natDegree = j

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.homogenize_shift {R : Type u_1} [CommSemiring R] (p : Polynomial R) (n k : ℕ) (hp : p.natDegree ≤ n) :

p.homogenize (n + k) = p.homogenize n * MvPolynomial.X 1 ^ k

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.chebyshevS_homogenize_add_two (R : Type u_1) [CommRing R] [Nontrivial R] (n : ℕ) :

(Polynomial.Chebyshev.S R ↑(n + 2)).homogenize (n + 2) = MvPolynomial.X 0 * (Polynomial.Chebyshev.S R ↑(n + 1)).homogenize (n + 1) - MvPolynomial.X 1 ^ 2 * (Polynomial.Chebyshev.S R ↑n).homogenize n

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.even_geometric_sum_add_two {R : Type u_1} [CommRing R] (x : R) (n : ℕ) :

∑ k ∈ Finset.range (n + 3), x ^ (2 * k) = (1 + x ^ 2) * ∑ k ∈ Finset.range (n + 2), x ^ (2 * k) - x ^ 2 * ∑ k ∈ Finset.range (n + 1), x ^ (2 * k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.chebyshevS_homogenize_eval_one_add_sq (R : Type u_1) [CommRing R] [Nontrivial R] (j : ℕ) (x : R) :

(MvPolynomial.eval ![1 + x ^ 2, x]) ((Polynomial.Chebyshev.S R ↑j).homogenize j) = ∑ k ∈ Finset.range (j + 1), x ^ (2 * k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_homogenized_monic_evaluation {R : Type u_1} [CommRing R] {r : ℕ} (p : Fin (r + 1) → Polynomial R) (hdegree : ∀ (j : Fin (r + 1)), (p j).natDegree = ↑j) (hmonic : ∀ (j : Fin (r + 1)), (p j).Monic) (v w : Fin (r + 1) → R) :

(Matrix.det fun (i j : Fin (r + 1)) => ∑ k ∈ Finset.range (↑j + 1), (p j).coeff k * v i ^ k * w i ^ (r - k)) = (Matrix.projVandermonde v w).det

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.homogenize_eval_eq_sum_coeff {R : Type u_1} [CommSemiring R] (p : Polynomial R) (j : ℕ) (v w : R) :

(MvPolynomial.eval ![v, w]) (p.homogenize j) = ∑ k ∈ Finset.range (j + 1), p.coeff k * v ^ k * w ^ (j - k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_orthogonal_denominator_row_factor {R : Type u_1} [CommRing R] {r : ℕ} (x : Fin (r + 1) → R) :

(Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j) - x i ^ (r + ↑j + 2)) = (∏ i : Fin (r + 1), (1 - x i ^ 2)) * Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j) * ∑ k ∈ Finset.range (↑j + 1), x i ^ (2 * k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_chebyshev_geometric_sum {R : Type u_1} [CommRing R] [Nontrivial R] {r : ℕ} (x : Fin (r + 1) → R) :

(Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j) * ∑ k ∈ Finset.range (↑j + 1), x i ^ (2 * k)) = (Matrix.projVandermonde (fun (i : Fin (r + 1)) => 1 + x i ^ 2) x).det

theorem MetricCodes.Spherical.HigherHarmonicYoung.OrthogonalDenominator.det_orthogonal_denominator {R : Type u_1} [CommRing R] {r : ℕ} (x : Fin (r + 1) → R) :

(Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j) - x i ^ (r + ↑j + 2)) = (Matrix.det fun (i j : Fin (r + 1)) => x i ^ (r - ↑j)) * ∏ i : Fin (r + 1), ∏ j ≥ i, (1 - x i * x j)