Representation-theoretic foundations

Associated Gegenbauer systems, harmonic Young spaces, and higher projection graphs.

noncomputable def MetricCodes.Spherical.AssociatedGegenbauer.normalizedSequence (n : ℕ) (hn : 2 ≤ n) : Polynomial.Sequence ℝ

The normalized Gegenbauer polynomials bundled as a polynomial sequence with degree equal to the index.

Equations

• MetricCodes.Spherical.AssociatedGegenbauer.normalizedSequence n hn = { elems' := SpherePacking.Gegenbauer.normalized n, degree_eq' := ⋯ }

theorem MetricCodes.Spherical.AssociatedGegenbauer.normalizedSequence_leadingCoeff_isUnit (n : ℕ) (hn : 2 ≤ n) (i : ℕ) : IsUnit (↑(normalizedSequence n hn) i).leadingCoeff

noncomputable def MetricCodes.Spherical.AssociatedGegenbauer.normalizedBasis (n : ℕ) (hn : 2 ≤ n) : Module.Basis ℕ ℝ (Polynomial ℝ)

The basis of real polynomials given by the normalized Gegenbauer sequence.

Equations

• MetricCodes.Spherical.AssociatedGegenbauer.normalizedBasis n hn = (MetricCodes.Spherical.AssociatedGegenbauer.normalizedSequence n hn).basis ⋯

noncomputable def MetricCodes.Spherical.AssociatedGegenbauer.coefficient (n : ℕ) (hn : 2 ≤ n) (r : ℕ) (p : Polynomial ℝ) : ℝ

The coefficient used in the spherical-code argument.

Equations

• MetricCodes.Spherical.AssociatedGegenbauer.coefficient n hn r p = ((MetricCodes.Spherical.AssociatedGegenbauer.normalizedBasis n hn).repr p) r

noncomputable def MetricCodes.Spherical.AssociatedGegenbauer.derivativeValue (n i j : ℕ) (t : ℝ) : ℝ

Evaluate the jth derivative of the degree-i normalized Gegenbauer polynomial at t.

Equations

• MetricCodes.Spherical.AssociatedGegenbauer.derivativeValue n i j t = Polynomial.eval t ((⇑Polynomial.derivative)^[j] (SpherePacking.Gegenbauer.normalized n i))

noncomputable def MetricCodes.Spherical.AssociatedGegenbauer.generatorTerm (n i k : ℕ) (t : ℝ) (l : ℕ) : Polynomial ℝ

The lth shifted-power term in the associated Gegenbauer generator, with its derivative and combinatorial coefficient.

Equations

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

noncomputable def MetricCodes.Spherical.AssociatedGegenbauer.generator (n i k : ℕ) (t : ℝ) : Polynomial ℝ

The sum of the generator terms normalized by k! times the kth derivative at one.

Equations

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

noncomputable def MetricCodes.Spherical.AssociatedGegenbauer.theta (n : ℕ) (hn : 4 ≤ n) (i k r : ℕ) (t : ℝ) : ℝ

The theta used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.AssociatedOverlap.polynomialInner_sub_right (n : ℕ) (p q r : MvPolynomial (Fin n) ℝ) : SpherePacking.Fischer.polynomialInner n p (q - r) = SpherePacking.Fischer.polynomialInner n p q - SpherePacking.Fischer.polynomialInner n p r

theorem MetricCodes.Spherical.AssociatedOverlap.eval_axisPolynomial {n : ℕ} (x y : SpherePacking.Euclidean n) : (MvPolynomial.eval fun (i : Fin n) => x.ofLp i) (SpherePacking.axisPolynomial n y) = inner ℝ x y

noncomputable def MetricCodes.Spherical.AssociatedAxisTransport.commonAxisReflection {n : ℕ} (x y : SpherePacking.Euclidean n) : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n

The common axis reflection used in the spherical-code argument.

Equations

• MetricCodes.Spherical.AssociatedAxisTransport.commonAxisReflection x y = (ℝ ∙ (x - y))ᗮ.reflection

theorem MetricCodes.Spherical.AssociatedAxisTransport.commonAxisReflection_apply_left {n : ℕ} (x y : SpherePacking.Euclidean n) (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : (commonAxisReflection x y) x = y

noncomputable def MetricCodes.Spherical.OrthogonalPolynomialTransport.polynomialMap {n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) : MvPolynomial (Fin n) ℝ →ₐ[ℝ] MvPolynomial (Fin n) ℝ

The polynomial map used in the spherical-code argument.

Equations

• MetricCodes.Spherical.OrthogonalPolynomialTransport.polynomialMap U = MvPolynomial.aeval fun (i : Fin n) => SpherePacking.axisPolynomial n (U (EuclideanSpace.single i 1))

@[simp]

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.polynomialMap_X {n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (i : Fin n) : (polynomialMap U) (MvPolynomial.X i) = SpherePacking.axisPolynomial n (U (EuclideanSpace.single i 1))

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.eval_polynomialMap {n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (p : MvPolynomial (Fin n) ℝ) (x : SpherePacking.Euclidean n) : (MvPolynomial.eval fun (i : Fin n) => x.ofLp i) ((polynomialMap U) p) = (MvPolynomial.eval fun (i : Fin n) => (U.symm x).ofLp i) p

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.polynomialMap_axisPolynomial {n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (x : SpherePacking.Euclidean n) : (polynomialMap U) (SpherePacking.axisPolynomial n x) = SpherePacking.axisPolynomial n (U x)

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.polynomialMap_comp {n : ℕ} (U V : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) : (polynomialMap U).comp (polynomialMap V) = polynomialMap (V.trans U)

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.polynomialMap_refl (n : ℕ) : polynomialMap (LinearIsometryEquiv.refl ℝ (SpherePacking.Euclidean n)) = AlgHom.id ℝ (MvPolynomial (Fin n) ℝ)

noncomputable def MetricCodes.Spherical.OrthogonalPolynomialTransport.polynomialEquiv {n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) : MvPolynomial (Fin n) ℝ ≃ₐ[ℝ] MvPolynomial (Fin n) ℝ

The polynomial equiv used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.polynomialMap_isHomogeneous {n k : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (p : MvPolynomial (Fin n) ℝ) (hp : p.IsHomogeneous k) : ((polynomialMap U) p).IsHomogeneous k

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.directionalDerivative_X {n : ℕ} (x : SpherePacking.Euclidean n) (i : Fin n) : (SpherePacking.directionalDerivative n x) (MvPolynomial.X i) = MvPolynomial.C (x.ofLp i)

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.directionalDerivative_polynomialMap {n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (x : SpherePacking.Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (SpherePacking.directionalDerivative n (U x)) ((polynomialMap U) p) = (polynomialMap U) ((SpherePacking.directionalDerivative n x) p)

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.rotatedCoordinate_orthogonality {n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (j k : Fin n) : ∑ i : Fin n, (U (EuclideanSpace.single i 1)).ofLp j * (U (EuclideanSpace.single i 1)).ofLp k = if j = k then 1 else 0

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.directionalDerivative_single {n : ℕ} (i : Fin n) (p : MvPolynomial (Fin n) ℝ) : (SpherePacking.directionalDerivative n (EuclideanSpace.single i 1)) p = (MvPolynomial.pderiv i) p

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.coeff_zero_polynomialMap {n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (p : MvPolynomial (Fin n) ℝ) : ((polynomialMap U) p).coeff 0 = p.coeff 0

theorem MetricCodes.Spherical.OrthogonalPolynomialTransport.polynomialInner_polynomialMap {n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (p q : MvPolynomial (Fin n) ℝ) : SpherePacking.Fischer.polynomialInner n ((polynomialMap U) p) ((polynomialMap U) q) = SpherePacking.Fischer.polynomialInner n p q

@[reducible, inline]

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

The polynomial space used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.PolynomialSpace r n = MvPolynomial (Fin ((r + 1) * n)) ℝ

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

The variable index used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.variableIndex i j = finProdFinEquiv (i, j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.variableIndex_injective {r n : ℕ} : Function.Injective fun (z : Fin (r + 1) × Fin n) => variableIndex z.1 z.2

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.rowEuler (r n : ℕ) (i : Fin (r + 1)) : PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The row euler used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuler_apply {r n : ℕ} (i : Fin (r + 1)) (p : PolynomialSpace r n) : (rowEuler r n i) p = ∑ j : Fin n, MvPolynomial.X (variableIndex i j) * (MvPolynomial.pderiv (variableIndex i j)) p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.traceOperator (r n : ℕ) (i j : Fin (r + 1)) : PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The trace operator used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.traceOperator_apply {r n : ℕ} (i j : Fin (r + 1)) (p : PolynomialSpace r n) : (traceOperator r n i j) p = ∑ k : Fin n, (MvPolynomial.pderiv (variableIndex i k)) ((MvPolynomial.pderiv (variableIndex j k)) p)

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.polarization (r n : ℕ) (i j : Fin (r + 1)) : PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The polarization used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_apply {r n : ℕ} (i j : Fin (r + 1)) (p : PolynomialSpace r n) : (polarization r n i j) p = ∑ k : Fin n, MvPolynomial.X (variableIndex i k) * (MvPolynomial.pderiv (variableIndex j k)) p

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_self {r n : ℕ} (i : Fin (r + 1)) : polarization r n i i = rowEuler r n i

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.rowWeightSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Submodule ℝ (PolynomialSpace r n)

The simultaneous row-Euler eigenspace with eigenvalues specified by lam.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.rowWeightSubmodule lam = ⨅ (i : Fin (r + 1)), (MetricCodes.Spherical.HigherHarmonicYoung.rowEuler r n i - ↑(lam i) • LinearMap.id).ker

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_rowWeightSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : PolynomialSpace r n) : p ∈ rowWeightSubmodule lam ↔ ∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.traceFreeSubmodule (r n : ℕ) : Submodule ℝ (PolynomialSpace r n)

The trace free submodule used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.traceFreeSubmodule r n = ⨅ (i : Fin (r + 1)), ⨅ (j : Fin (r + 1)), (MetricCodes.Spherical.HigherHarmonicYoung.traceOperator r n i j).ker

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_traceFreeSubmodule {r n : ℕ} (p : PolynomialSpace r n) : p ∈ traceFreeSubmodule r n ↔ ∀ (i j : Fin (r + 1)), (traceOperator r n i j) p = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.highestWeightSubmodule (r n : ℕ) : Submodule ℝ (PolynomialSpace r n)

The intersection of the kernels of the upper-row polarization operators.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_highestWeightSubmodule {r n : ℕ} (p : PolynomialSpace r n) : p ∈ highestWeightSubmodule r n ↔ ∀ (i j : Fin (r + 1)), i < j → (polarization r n i j) p = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.harmonicYoungSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Submodule ℝ (PolynomialSpace r n)

The harmonic young submodule used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_harmonicYoungSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : PolynomialSpace r n) : p ∈ harmonicYoungSubmodule lam ↔ MvPolynomial.IsHomogeneous p (∑ i : Fin (r + 1), lam i) ∧ (∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p) ∧ (∀ (i j : Fin (r + 1)), (traceOperator r n i j) p = 0) ∧ ∀ (i j : Fin (r + 1)), i < j → (polarization r n i j) p = 0

@[reducible, inline]

noncomputable abbrev MetricCodes.Spherical.HigherHarmonicYoung.HarmonicYoungSpace {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Submodule ℝ (PolynomialSpace r n)

The harmonic young space used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.HarmonicYoungSpace lam = MetricCodes.Spherical.HigherHarmonicYoung.harmonicYoungSubmodule lam

instance MetricCodes.Spherical.HigherHarmonicYoung.harmonicYoungSpace_finiteDimensional {r n : ℕ} (lam : Fin (r + 1) → ℕ) : FiniteDimensional ℝ ↥(HarmonicYoungSpace lam)

@[reducible, inline]

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

The Euclidean product of r + 1 rows, each with n coordinates.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.RowEuclideanSpace r n = PiLp 2 fun (x : Fin (r + 1)) => SpherePacking.Euclidean n

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.rowEuclideanEquiv (r n : ℕ) : SpherePacking.Euclidean ((r + 1) * n) ≃ₗᵢ[ℝ] RowEuclideanSpace r n

The isometry regrouping a flat Euclidean coordinate vector into its rows.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuclideanEquiv_apply {r n : ℕ} (x : SpherePacking.Euclidean ((r + 1) * n)) (i : Fin (r + 1)) (j : Fin n) : (((rowEuclideanEquiv r n) x).ofLp i).ofLp j = x.ofLp (variableIndex i j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuclideanEquiv_symm_apply {r n : ℕ} (x : RowEuclideanSpace r n) (i : Fin (r + 1)) (j : Fin n) : ((rowEuclideanEquiv r n).symm x).ofLp (variableIndex i j) = (x.ofLp i).ofLp j

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.blockIsometry {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) : SpherePacking.Euclidean ((r + 1) * n) ≃ₗᵢ[ℝ] SpherePacking.Euclidean ((r + 1) * n)

Apply the same Euclidean isometry independently to every row of a flat coordinate vector.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.blockIsometry_apply {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (x : SpherePacking.Euclidean ((r + 1) * n)) (i : Fin (r + 1)) (j : Fin n) : ((blockIsometry U) x).ofLp (variableIndex i j) = (U (WithLp.toLp 2 fun (k : Fin n) => x.ofLp (variableIndex i k))).ofLp j

theorem MetricCodes.Spherical.HigherHarmonicYoung.row_of_single_same {r n : ℕ} (i : Fin (r + 1)) (j : Fin n) : (WithLp.toLp 2 fun (k : Fin n) => (EuclideanSpace.single (variableIndex i j) 1).ofLp (variableIndex i k)) = EuclideanSpace.single j 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.row_of_single_ne {r n : ℕ} (i h : Fin (r + 1)) (j : Fin n) (hne : h ≠ i) : (WithLp.toLp 2 fun (k : Fin n) => (EuclideanSpace.single (variableIndex i j) 1).ofLp (variableIndex h k)) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.blockIsometry_single {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (i h : Fin (r + 1)) (j k : Fin n) : ((blockIsometry U) (EuclideanSpace.single (variableIndex i j) 1)).ofLp (variableIndex h k) = if h = i then (U (EuclideanSpace.single j 1)).ofLp k else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.polynomialAction {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) : PolynomialSpace r n ≃ₐ[ℝ] PolynomialSpace r n

The polynomial algebra action induced by applying the orthogonal transformation to every row.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.polynomialAction U = MetricCodes.Spherical.OrthogonalPolynomialTransport.polynomialEquiv (MetricCodes.Spherical.HigherHarmonicYoung.blockIsometry U)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.rowVector {r n : ℕ} (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) : SpherePacking.Euclidean ((r + 1) * n)

Embed a Euclidean vector into row i, with every other row zero.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.rowVector i v = (MetricCodes.Spherical.HigherHarmonicYoung.rowEuclideanEquiv r n).symm (PiLp.single 2 i v)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowVector_apply {r n : ℕ} (i h : Fin (r + 1)) (v : SpherePacking.Euclidean n) (k : Fin n) : (rowVector i v).ofLp (variableIndex h k) = if h = i then v.ofLp k else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.blockIsometry_rowVector {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) : (blockIsometry U) (rowVector i v) = rowVector i (U v)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.rowDirectionalDerivative (r n : ℕ) (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) : PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The row directional derivative used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.rowDirectionalDerivative r n i v = SpherePacking.directionalDerivative ((r + 1) * n) (MetricCodes.Spherical.HigherHarmonicYoung.rowVector i v)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowDirectionalDerivative_apply {r n : ℕ} (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) (p : PolynomialSpace r n) : (rowDirectionalDerivative r n i v) p = ∑ k : Fin n, v.ofLp k • (MvPolynomial.pderiv (variableIndex i k)) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowDirectionalDerivative_polynomialAction {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) (p : PolynomialSpace r n) : (rowDirectionalDerivative r n i (U v)) ((polynomialAction U) p) = (polynomialAction U) ((rowDirectionalDerivative r n i v) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowDirectionalDerivative_single {r n : ℕ} (i : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) : (rowDirectionalDerivative r n i (EuclideanSpace.single k 1)) p = (MvPolynomial.pderiv (variableIndex i k)) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.rotatedRowTrace {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (i j : Fin (r + 1)) (p : PolynomialSpace r n) : ∑ k : Fin n, (rowDirectionalDerivative r n i (U (EuclideanSpace.single k 1))) ((rowDirectionalDerivative r n j (U (EuclideanSpace.single k 1))) p) = (traceOperator r n i j) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.traceOperator_polynomialAction {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (i j : Fin (r + 1)) (p : PolynomialSpace r n) : (traceOperator r n i j) ((polynomialAction U) p) = (polynomialAction U) ((traceOperator r n i j) p)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngHomogeneousEmbedding {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (∑ i : Fin (r + 1), lam i))

The young homogeneous embedding used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.youngHomogeneousEmbedding lam = Submodule.inclusion ⋯

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngHomogeneousEmbedding_injective {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Function.Injective ⇑(youngHomogeneousEmbedding lam)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngCoefficientEmbedding {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) (∑ i : Fin (r + 1), lam i)

The Fischer coefficient embedding restricted to the harmonic Young space of weight lam.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngCoefficientEmbedding_injective {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Function.Injective ⇑(youngCoefficientEmbedding lam)

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

The Fischer inner product of harmonic Young polynomials through their homogeneous embedding.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngFischerInner_eq_polynomialInner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HarmonicYoungSpace lam)) : youngFischerInner lam p q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) ↑p ↑q

@[implicit_reducible]

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngFischerCore {r n : ℕ} (lam : Fin (r + 1) → ℕ) : InnerProductSpace.Core ℝ ↥(HarmonicYoungSpace lam)

The inner product core on the harmonic Young space induced by its injective coefficient embedding.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.youngFischerCore lam = SpherePacking.Fischer.embeddingInnerCore (MetricCodes.Spherical.HigherHarmonicYoung.youngCoefficientEmbedding lam) ⋯

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherHarmonicYoung.instYoungFischerInner {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Inner ℝ ↥(HarmonicYoungSpace lam)

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.instYoungFischerInner lam = { inner := MetricCodes.Spherical.HigherHarmonicYoung.youngFischerInner lam }

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherHarmonicYoung.instYoungFischerNormedAddCommGroup {r n : ℕ} (lam : Fin (r + 1) → ℕ) : NormedAddCommGroup ↥(HarmonicYoungSpace lam)

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.instYoungFischerNormedAddCommGroup lam = InnerProductSpace.Core.toNormedAddCommGroup

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherHarmonicYoung.instYoungFischerInnerProductSpace {r n : ℕ} (lam : Fin (r + 1) → ℕ) : InnerProductSpace ℝ ↥(HarmonicYoungSpace lam)

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.instYoungFischerInnerProductSpace lam = InnerProductSpace.ofCore (MetricCodes.Spherical.HigherHarmonicYoung.youngFischerCore lam).toCore

theorem MetricCodes.Spherical.HigherHarmonicYoung.young_inner_eq_polynomialInner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(HarmonicYoungSpace lam)) : inner ℝ p q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) ↑p ↑q

theorem MetricCodes.Spherical.HigherHarmonicYoung.young_polynomialAction_inner {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (lam : Fin (r + 1) → ℕ) (p q p' q' : ↥(HarmonicYoungSpace lam)) (hp : ↑p' = (polynomialAction U) ↑p) (hq : ↑q' = (polynomialAction U) ↑q) : inner ℝ p' q' = inner ℝ p q

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.rowAxisPolynomial {r n : ℕ} (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) : PolynomialSpace r n

The row axis polynomial used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.rowAxisPolynomial i v = SpherePacking.axisPolynomial ((r + 1) * n) (MetricCodes.Spherical.HigherHarmonicYoung.rowVector i v)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowAxisPolynomial_eq_sum {r n : ℕ} (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) : rowAxisPolynomial i v = ∑ k : Fin n, MvPolynomial.C (v.ofLp k) * MvPolynomial.X (variableIndex i k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rotatedRowPolarization {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (i j : Fin (r + 1)) (p : PolynomialSpace r n) : ∑ k : Fin n, rowAxisPolynomial i (U (EuclideanSpace.single k 1)) * (rowDirectionalDerivative r n j (U (EuclideanSpace.single k 1))) p = (polarization r n i j) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialAction_variableIndex {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (i : Fin (r + 1)) (k : Fin n) : (polynomialAction U) (MvPolynomial.X (variableIndex i k)) = rowAxisPolynomial i (U (EuclideanSpace.single k 1))

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_polynomialAction {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (i j : Fin (r + 1)) (p : PolynomialSpace r n) : (polarization r n i j) ((polynomialAction U) p) = (polynomialAction U) ((polarization r n i j) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuler_polynomialAction {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (i : Fin (r + 1)) (p : PolynomialSpace r n) : (rowEuler r n i) ((polynomialAction U) p) = (polynomialAction U) ((rowEuler r n i) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialAction_mem_harmonicYoungSubmodule {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (lam : Fin (r + 1) → ℕ) {p : PolynomialSpace r n} (hp : p ∈ harmonicYoungSubmodule lam) : (polynomialAction U) p ∈ harmonicYoungSubmodule lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.blockIsometry_symm_apply_apply {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (x : SpherePacking.Euclidean ((r + 1) * n)) : (blockIsometry U.symm) ((blockIsometry U) x) = x

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialAction_symm_apply_apply {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (p : PolynomialSpace r n) : (polynomialAction U.symm) ((polynomialAction U) p) = p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngOrthogonalLinearEquiv {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (lam : Fin (r + 1) → ℕ) : ↥(HarmonicYoungSpace lam) ≃ₗ[ℝ] ↥(HarmonicYoungSpace lam)

The linear equivalence on harmonic Young space induced by the rowwise orthogonal polynomial action.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngOrthogonalIsometry {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (lam : Fin (r + 1) → ℕ) : ↥(HarmonicYoungSpace lam) ≃ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)

The young orthogonal isometry used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.youngOrthogonalIsometry U lam = (MetricCodes.Spherical.HigherHarmonicYoung.youngOrthogonalLinearEquiv U lam).isometryOfInner ⋯

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngCoefficientRange {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Submodule ℝ (SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) (∑ i : Fin (r + 1), lam i))

The subspace of Fischer coefficients arising from harmonic Young polynomials of weight lam.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.youngCoefficientRange lam = (MetricCodes.Spherical.HigherHarmonicYoung.youngCoefficientEmbedding lam).range

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngProjection {r n : ℕ} (lam : Fin (r + 1) → ℕ) : SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) (∑ i : Fin (r + 1), lam i) →ₗ[ℝ] ↥(HarmonicYoungSpace lam)

Project coefficient space orthogonally onto the harmonic Young coefficient range and recover its polynomial.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngProjection_coefficientEmbedding {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(HarmonicYoungSpace lam)) : (youngProjection lam) ((youngCoefficientEmbedding lam) p) = p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngHomogeneousProjection {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (∑ i : Fin (r + 1), lam i)) →ₗ[ℝ] ↥(HarmonicYoungSpace lam)

The young homogeneous projection used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.rowAxisHomogeneous {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (∑ j : Fin (r + 1), mu j))

The row axis homogeneous used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateRaise {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HarmonicYoungSpace mu)

The projected coordinate raise used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.rowDirectionalHomogeneous {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (∑ j : Fin (r + 1), mu j))

The row directional homogeneous used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateLower {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(HarmonicYoungSpace mu)

The projected coordinate lower used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngCoefficientIsometry {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ↥(HarmonicYoungSpace lam) →ₗᵢ[ℝ] SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) (∑ i : Fin (r + 1), lam i)

The harmonic Young coefficient embedding bundled as a linear isometry.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.youngCoefficientIsometry lam = (MetricCodes.Spherical.HigherHarmonicYoung.youngCoefficientEmbedding lam).isometryOfInner ⋯

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngProjection_residual_orthogonal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) (∑ i : Fin (r + 1), lam i)) : v - (youngCoefficientEmbedding lam) ((youngProjection lam) v) ∈ (youngCoefficientRange lam)ᗮ

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngProjection_inner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) (∑ i : Fin (r + 1), lam i)) (p : ↥(HarmonicYoungSpace lam)) : inner ℝ ((youngProjection lam) v) p = inner ℝ v ((youngCoefficientIsometry lam) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngHomogeneousProjection_inner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (∑ i : Fin (r + 1), lam i))) (p : ↥(HarmonicYoungSpace lam)) : inner ℝ ((youngHomogeneousProjection lam) v) p = SpherePacking.Fischer.polynomialInner ((r + 1) * n) ↑v ↑p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngHomogeneousAction {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (k : ℕ) : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) k) →ₗ[ℝ] ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) k)

The rowwise orthogonal polynomial action restricted to homogeneous degree k.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngHomogeneousProjection_equivariant {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (lam : Fin (r + 1) → ℕ) (v : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (∑ i : Fin (r + 1), lam i))) : (youngHomogeneousProjection lam) ((youngHomogeneousAction U (∑ i : Fin (r + 1), lam i)) v) = (youngOrthogonalIsometry U lam) ((youngHomogeneousProjection lam) v)

theorem MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateRaise_inner {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) (q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((projectedCoordinateRaise mu lam hdeg i v) p) q = inner ℝ p ((projectedCoordinateLower lam mu hdeg i v) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateRaise_equivariant {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (projectedCoordinateRaise mu lam hdeg i (U v)) ((youngOrthogonalIsometry U lam) p) = (youngOrthogonalIsometry U mu) ((projectedCoordinateRaise mu lam hdeg i v) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateLower_equivariant {r n : ℕ} (U : SpherePacking.Euclidean n ≃ₗᵢ[ℝ] SpherePacking.Euclidean n) (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (i : Fin (r + 1)) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (projectedCoordinateLower mu lam hdeg i (U v)) ((youngOrthogonalIsometry U lam) p) = (youngOrthogonalIsometry U mu) ((projectedCoordinateLower mu lam hdeg i v) p)

def MetricCodes.Spherical.HigherHierarchy.Weyl.tailLength (n r : ℕ) (i : Fin (r + 1)) : ℕ

The tail length used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.Weyl.tailLength n r i = n - ↑i - r - 3

def MetricCodes.Spherical.HigherHierarchy.Weyl.rowTail {r : ℕ} (i : Fin (r + 1)) : ℕ

The row tail used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.Weyl.rowTail i = r - ↑i

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

The row factor used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHierarchy.Weyl.pairFactor {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) : ℝ

The pair factor used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.Weyl.pairFactor n lam i j = (↑(lam i) - ↑(lam j) + ↑↑j - ↑↑i) / (↑↑j - ↑↑i) * ((↑(lam i) + ↑(lam j) + ↑n - ↑↑i - ↑↑j - 2) / (↑n - ↑↑i - ↑↑j - 2))

noncomputable def MetricCodes.Spherical.HigherHierarchy.Weyl.dimension {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ℝ

The dimension used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.linearDenominator_pos {r n : ℕ} (hn : 2 * r + 4 ≤ n) (i : Fin (r + 1)) : 0 < ↑n - 2 * ↑(↑i + 1)

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.rowFactor_pos {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : 0 < rowFactor n lam i

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.differenceNumerator_pos {r : ℕ} {lam : Fin (r + 1) → ℕ} (hlam : Antitone lam) {i j : Fin (r + 1)} (hij : i < j) : 0 < ↑(lam i) - ↑(lam j) + ↑↑j - ↑↑i

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.sumDenominator_pos {r n : ℕ} (hn : 2 * r + 4 ≤ n) (i j : Fin (r + 1)) : 0 < ↑n - ↑↑i - ↑↑j - 2

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.pairFactor_pos {r n : ℕ} (hn : 2 * r + 4 ≤ n) {lam : Fin (r + 1) → ℕ} (hlam : Antitone lam) {i j : Fin (r + 1)} (hij : i < j) : 0 < pairFactor n lam i j

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.dimension_pos {r n : ℕ} (hn : 2 * r + 4 ≤ n) {lam : Fin (r + 1) → ℕ} (hlam : Antitone lam) : 0 < dimension n lam

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.rowFactor_eq_binomial {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : rowFactor n lam i = (2 * ↑(lam i) + ↑n - 2 * ↑(↑i + 1)) / (↑n - 2 * ↑(↑i + 1)) * (↑((lam i + tailLength n r i).choose (lam i)) / ↑((lam i + rowTail i).choose (lam i)))

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.rowFactor_update_succ_self {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (ell : Fin (r + 1)) : rowFactor n (Function.update lam ell (lam ell + 1)) ell = rowFactor n lam ell * ((2 * ↑(lam ell) + ↑n - 2 * ↑(↑ell + 1) + 2) / (2 * ↑(lam ell) + ↑n - 2 * ↑(↑ell + 1))) * ((↑(lam ell) + ↑(tailLength n r ell) + 1) / (↑(lam ell) + ↑(rowTail ell) + 1))

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.rowFactor_update_succ_ne {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (ell i : Fin (r + 1)) (h : i ≠ ell) : rowFactor n (Function.update lam ell (lam ell + 1)) i = rowFactor n lam i

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.tendsto_log_linear_div {x : ℕ → ℝ} {c : ℝ} (hc : 0 < c) (hx : Filter.Tendsto (fun (n : ℕ) => x n / ↑n) Filter.atTop (nhds c)) : Filter.Tendsto (fun (n : ℕ) => Real.log (x n) / ↑n) Filter.atTop (nhds 0)

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.tendsto_log_fixedTail_choose_div (k : ℕ → ℕ) (c : ℕ) {a : ℝ} (ha : 0 < a) (hk : Filter.Tendsto (fun (n : ℕ) => ↑(k n) / ↑n) Filter.atTop (nhds a)) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑((k n + c).choose (k n)) / ↑n) Filter.atTop (nhds 0)

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.tendsto_tailLength_ratio (r : ℕ) (i : Fin (r + 1)) : Filter.Tendsto (fun (n : ℕ) => ↑(tailLength n r i) / ↑n) Filter.atTop (nhds 1)

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.tendsto_log_rowBinomial_div {r : ℕ} (i : Fin (r + 1)) (k : ℕ → ℕ) {a : ℝ} (ha : 0 < a) (hkTop : Filter.Tendsto k Filter.atTop Filter.atTop) (hk : Filter.Tendsto (fun (n : ℕ) => ↑(k n) / ↑n) Filter.atTop (nhds a)) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑((k n + tailLength n r i).choose (k n)) / ↑n) Filter.atTop (nhds ((1 + a) * Real.log (1 + a) - a * Real.log a))

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.tendsto_linearRowFactor (k : ℕ → ℕ) (c : ℕ) {a : ℝ} (hk : Filter.Tendsto (fun (n : ℕ) => ↑(k n) / ↑n) Filter.atTop (nhds a)) : Filter.Tendsto (fun (n : ℕ) => (2 * ↑(k n) + ↑n - ↑c) / (↑n - ↑c)) Filter.atTop (nhds (2 * a + 1))

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.tendsto_log_rowFactor_div {r : ℕ} (i : Fin (r + 1)) (lam : ℕ → Fin (r + 1) → ℕ) {a : ℝ} (ha : 0 < a) (hlamTop : Filter.Tendsto (fun (n : ℕ) => lam n i) Filter.atTop Filter.atTop) (hlam : Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds a)) : Filter.Tendsto (fun (n : ℕ) => Real.log (rowFactor n (lam n) i) / ↑n) Filter.atTop (nhds ((1 + a) * Real.log (1 + a) - a * Real.log a))

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.tendsto_log_pairFactor_div {r : ℕ} (i j : Fin (r + 1)) (hij : i < j) (lam : ℕ → Fin (r + 1) → ℕ) {aᵢ aⱼ : ℝ} (haᵢ : 0 < aᵢ) (haⱼ : 0 < aⱼ) (hsep : aⱼ < aᵢ) (hi : Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds aᵢ)) (hj : Filter.Tendsto (fun (n : ℕ) => ↑(lam n j) / ↑n) Filter.atTop (nhds aⱼ)) : Filter.Tendsto (fun (n : ℕ) => Real.log (pairFactor n (lam n) i j) / ↑n) Filter.atTop (nhds 0)

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.tendsto_log_dimension_div {r : ℕ} (lam : ℕ → Fin (r + 1) → ℕ) (a : Fin (r + 1) → ℝ) (ha : ∀ (i : Fin (r + 1)), 0 < a i) (hanti : StrictAnti a) (hdominant : ∀ (n : ℕ), Antitone (lam n)) (hTop : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => lam n i) Filter.atTop Filter.atTop) (hlim : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds (a i))) : Filter.Tendsto (fun (n : ℕ) => Real.log (dimension n (lam n)) / ↑n) Filter.atTop (nhds (∑ i : Fin (r + 1), ((1 + a i) * Real.log (1 + a i) - a i * Real.log (a i))))

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.tendsto_log_dimension_div_log_two {r : ℕ} (lam : ℕ → Fin (r + 1) → ℕ) (a : Fin (r + 1) → ℝ) (ha : ∀ (i : Fin (r + 1)), 0 < a i) (hanti : StrictAnti a) (hdominant : ∀ (n : ℕ), Antitone (lam n)) (hTop : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => lam n i) Filter.atTop Filter.atTop) (hlim : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds (a i))) : Filter.Tendsto (fun (n : ℕ) => Real.log (dimension n (lam n)) / ↑n / Real.log 2) Filter.atTop (nhds (∑ i : Fin (r + 1), sphericalEntropy (a i)))

noncomputable def MetricCodes.Spherical.HigherHierarchy.Weyl.flooredWeight {r : ℕ} (a : Fin (r + 1) → ℝ) (n : ℕ) (i : Fin (r + 1)) : ℕ

The floored weight used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.Weyl.flooredWeight a n i = ⌊a i * ↑n⌋₊

theorem MetricCodes.Spherical.HigherHierarchy.Weyl.flooredWeight_antitone {r : ℕ} {a : Fin (r + 1) → ℝ} (ha : Antitone a) (n : ℕ) : Antitone (flooredWeight a n)

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherRepresentationGraph.AmbientWeight (r : ℕ) : Type

The ambient weight used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherRepresentationGraph.AmbientWeight r = (Fin (r + 1) → ℕ)

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherRepresentationGraph.StabilizerWeight (r : ℕ) : Type

A stabilizer weight with r natural-number coordinates.

Equations

• MetricCodes.Spherical.HigherRepresentationGraph.StabilizerWeight r = (Fin r → ℕ)

def MetricCodes.Spherical.HigherRepresentationGraph.Interlaces {r : ℕ} (lam : AmbientWeight r) (μ : StabilizerWeight r) : Prop

The interlaces used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherRepresentationGraph.Interlaces lam μ = ∀ (i : Fin r), μ i ≤ lam i.castSucc ∧ lam i.succ ≤ μ i

def MetricCodes.Spherical.HigherRepresentationGraph.StrictInterlaces {r : ℕ} (lam : AmbientWeight r) (μ : StabilizerWeight r) : Prop

The strict interlaces used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherRepresentationGraph.StrictInterlaces lam μ = ∀ (i : Fin r), μ i < lam i.castSucc ∧ lam i.succ < μ i

theorem MetricCodes.Spherical.HigherRepresentationGraph.StrictInterlaces.interlaces {r : ℕ} {lam : AmbientWeight r} {μ : StabilizerWeight r} (h : StrictInterlaces lam μ) : Interlaces lam μ

theorem MetricCodes.Spherical.HigherRepresentationGraph.Interlaces.antitone_ambient {r : ℕ} {lam : AmbientWeight r} {μ : StabilizerWeight r} (h : Interlaces lam μ) : Antitone lam

def MetricCodes.Spherical.HigherRepresentationGraph.raise {r : ℕ} (lam : AmbientWeight r) (i : Fin (r + 1)) : AmbientWeight r

The raise used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherRepresentationGraph.raise lam i j = if j = i then lam j + 1 else lam j

def MetricCodes.Spherical.HigherRepresentationGraph.Adjacent {r : ℕ} (lam ν : AmbientWeight r) : Prop

Adjacency of ambient weights when either is obtained from the other by raising one coordinate.

Equations

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

theorem MetricCodes.Spherical.HigherRepresentationGraph.Adjacent.symm {r : ℕ} {lam ν : AmbientWeight r} (h : Adjacent lam ν) : Adjacent ν lam

theorem MetricCodes.Spherical.TwoRowYoungBidegreeDecomposition.coeff_X_mul_pderiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (a : σ) (d : σ →₀ ℕ) : (MvPolynomial.X a * (MvPolynomial.pderiv a) p).coeff d = d a • p.coeff d

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.rowExponent {r n : ℕ} (d : Fin ((r + 1) * n) →₀ ℕ) (i : Fin (r + 1)) : Fin n →₀ ℕ

The row exponent used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.rowExponent d i = Finsupp.equivFunOnFinite.symm fun (j : Fin n) => d (MetricCodes.Spherical.HigherHarmonicYoung.variableIndex i j)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowExponent_apply {r n : ℕ} (d : Fin ((r + 1) * n) →₀ ℕ) (i : Fin (r + 1)) (j : Fin n) : (rowExponent d i) j = d (variableIndex i j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowExponent_degree {r n : ℕ} (d : Fin ((r + 1) * n) →₀ ℕ) (i : Fin (r + 1)) : Finsupp.degree (rowExponent d i) = ∑ j : Fin n, d (variableIndex i j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.degree_eq_sum_rowExponent {r n : ℕ} (d : Fin ((r + 1) * n) →₀ ℕ) : Finsupp.degree d = ∑ i : Fin (r + 1), Finsupp.degree (rowExponent d i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.coeff_rowEuler {r n : ℕ} (p : PolynomialSpace r n) (i : Fin (r + 1)) (d : Fin ((r + 1) * n) →₀ ℕ) : ((rowEuler r n i) p).coeff d = Finsupp.degree (rowExponent d i) • p.coeff d

theorem MetricCodes.Spherical.HigherHarmonicYoung.harmonicYoung_rowExponent_degree {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(HarmonicYoungSpace lam)) (d : Fin ((r + 1) * n) →₀ ℕ) (hd : (↑p).coeff d ≠ 0) (i : Fin (r + 1)) : Finsupp.degree (rowExponent d i) = lam i

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.flattenRowExponents {r n : ℕ} (a : Fin (r + 1) → Fin n →₀ ℕ) : Fin ((r + 1) * n) →₀ ℕ

The flatten row exponents used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.flattenRowExponents a = Finsupp.equivFunOnFinite.symm fun (k : Fin ((r + 1) * n)) => (a (finProdFinEquiv.symm k).1) (finProdFinEquiv.symm k).2

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.flattenRowExponents_apply {r n : ℕ} (a : Fin (r + 1) → Fin n →₀ ℕ) (i : Fin (r + 1)) (j : Fin n) : (flattenRowExponents a) (variableIndex i j) = (a i) j

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowExponent_flattenRowExponents {r n : ℕ} (a : Fin (r + 1) → Fin n →₀ ℕ) (i : Fin (r + 1)) : rowExponent (flattenRowExponents a) i = a i

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.flattenRowExponents_rowExponent {r n : ℕ} (d : Fin ((r + 1) * n) →₀ ℕ) : (flattenRowExponents fun (i : Fin (r + 1)) => rowExponent d i) = d

theorem MetricCodes.Spherical.HigherHarmonicYoung.flattenRowExponents_injective {r n : ℕ} : Function.Injective flattenRowExponents

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

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

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_rowDegreeFamilies {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a : Fin (r + 1) → Fin n →₀ ℕ) : a ∈ rowDegreeFamilies lam ↔ ∀ (i : Fin (r + 1)), Finsupp.degree (a i) = lam i

theorem MetricCodes.Spherical.HigherHarmonicYoung.card_rowDegreeFamilies {r n : ℕ} (lam : Fin (r + 1) → ℕ) : (rowDegreeFamilies lam).card = ∏ i : Fin (r + 1), (n + lam i - 1).choose (lam i)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousExponents {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Finset (Fin ((r + 1) * n) →₀ ℕ)

The young multihomogeneous exponents used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.card_youngMultihomogeneousExponents {r n : ℕ} (lam : Fin (r + 1) → ℕ) : (youngMultihomogeneousExponents n lam).card = ∏ i : Fin (r + 1), (n + lam i - 1).choose (lam i)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousSubmodule {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Submodule ℝ (PolynomialSpace r n)

The young multihomogeneous submodule used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousSubmodule n lam = MvPolynomial.restrictSupport ℝ ↑(MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousExponents n lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_youngMultihomogeneousSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Module.finrank ℝ ↥(youngMultihomogeneousSubmodule n lam) = ∏ i : Fin (r + 1), (n + lam i - 1).choose (lam i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.harmonicYoung_mem_youngMultihomogeneousSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(HarmonicYoungSpace lam)) : ↑p ∈ youngMultihomogeneousSubmodule n lam

instance MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousSubmodule_finiteDimensional {r n : ℕ} (lam : Fin (r + 1) → ℕ) : FiniteDimensional ℝ ↥(youngMultihomogeneousSubmodule n lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneous_rowExponent_degree {r n : ℕ} (lam : Fin (r + 1) → ℕ) {p : PolynomialSpace r n} (hp : p ∈ youngMultihomogeneousSubmodule n lam) {d : Fin ((r + 1) * n) →₀ ℕ} (hd : p.coeff d ≠ 0) (i : Fin (r + 1)) : Finsupp.degree (rowExponent d i) = lam i

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneous_rowEuler {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(youngMultihomogeneousSubmodule n lam)) (i : Fin (r + 1)) : (rowEuler r n i) ↑p = ↑(lam i) • ↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneous_isHomogeneous {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(youngMultihomogeneousSubmodule n lam)) : MvPolynomial.IsHomogeneous (↑p) (∑ i : Fin (r + 1), lam i)

structure MetricCodes.HigherProjectionGraph.Data (I : Type u_3) (X : Type u_4) [Fintype I] [DecidableEq I] (D d Q : ℕ) : Type (max u_3 u_4)

Data encoding the data construction.

• dimension : I → ℕ

  The dimension component.

• dimension_pos (i : I) : 0 < self.dimension i
• block : I → Matrix (Fin D) (Fin D) ℝ

  The block component.

• block_symmetric (i : I) : (self.block i).transpose = self.block i
• block_idempotent (i : I) : self.block i * self.block i = self.block i
• block_orthogonal (i j : I) : i ≠ j → self.block i * self.block j = 0
• block_complete : ∑ i : I, self.block i = 1
• block_trace (i : I) : (self.block i).trace = ↑(self.dimension i)
• fibre : I → X → Matrix (Fin D) (Fin d) ℝ

  The fibre component.

• fibre_isometry (i : I) (x : X) : (self.fibre i x).transpose * self.fibre i x = 1
• fibre_support (i : I) (x : X) : self.block i * self.fibre i x = self.fibre i x
• correlation : X → X → ℝ

  The correlation component.

• axis : X → Matrix (Fin Q) (Fin D) ℝ

  The axis component.

• axis_inner (x y : X) : (self.axis x).transpose * self.axis y = self.correlation x y • 1
• probability : I → I → ℝ

  The probability component.

• probability_nonneg (target source : I) : 0 ≤ self.probability target source
• balance (target source : I) : ↑(self.dimension target) * self.probability target source = ↑(self.dimension source) * self.probability source target
• channel : I → I → Matrix (Fin Q) (Fin D) ℝ

  The channel component.

• channel_isometry (target source : I) : (self.channel target source).transpose * self.channel target source = if 0 < self.probability target source then self.block source else 0
• channel_orthogonal (target source target' source' : I) : (target, source) ≠ (target', source') → (self.channel target source).transpose * self.channel target' source' = 0
• channel_axis (target source j : I) (x : X) : (self.channel target source).transpose * self.axis x * self.fibre j x = if target = j then √(self.probability target source) • self.fibre source x else 0
• eigenvalue : ℝ

  The eigenvalue component.

• eigenvalue_pos : 0 < self.eigenvalue
• eigenvector : I → ℝ

  The eigenvector component.

• eigenvector_pos (i : I) : 0 < self.eigenvector i
• eigenvector_unit : ∑ i : I, self.eigenvector i ^ 2 = 1
• eigenvector_equation (i : I) : ∑ j : I, √(self.probability i j * self.probability j i) * self.eigenvector j = self.eigenvalue * self.eigenvector i

noncomputable def MetricCodes.HigherProjectionGraph.Data.weight {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (i : I) : ℝ

The weight used in the metric-code argument.

Equations

• A.weight i = √↑(A.dimension i) * A.eigenvector i

theorem MetricCodes.HigherProjectionGraph.Data.weight_pos {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (i : I) : 0 < A.weight i

noncomputable def MetricCodes.HigherProjectionGraph.Data.normalization {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) : ℝ

The sum of the positive vertex weights used to normalize the graph amplitudes.

Equations

• A.normalization = ∑ i : I, A.weight i

theorem MetricCodes.HigherProjectionGraph.Data.normalization_pos {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] : 0 < A.normalization

theorem MetricCodes.HigherProjectionGraph.Data.sqrt_dimension_mul_symmetric_edge {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (target source : I) : √↑(A.dimension source) * √(A.probability source target * A.probability target source) = A.probability target source * √↑(A.dimension target)

theorem MetricCodes.HigherProjectionGraph.Data.weighted_eigenvector_equation {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (source : I) : ∑ target : I, A.probability target source * A.weight target = A.eigenvalue * A.weight source

noncomputable def MetricCodes.HigherProjectionGraph.Data.amplitude {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (i : I) : ℝ

The square root of the vertex weight divided by the total weight.

Equations

• A.amplitude i = √(A.weight i / A.normalization)

theorem MetricCodes.HigherProjectionGraph.Data.amplitude_pos {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (i : I) : 0 < A.amplitude i

theorem MetricCodes.HigherProjectionGraph.Data.amplitude_sq {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (i : I) : A.amplitude i ^ 2 = A.weight i / A.normalization

theorem MetricCodes.HigherProjectionGraph.Data.amplitude_sq_sum {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] : ∑ i : I, A.amplitude i ^ 2 = 1

theorem MetricCodes.HigherProjectionGraph.Data.amplitude_eigenvector_equation {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (source : I) : ∑ target : I, A.probability target source * A.amplitude target ^ 2 = A.eigenvalue * A.amplitude source ^ 2

theorem MetricCodes.HigherProjectionGraph.Data.fibre_orthogonal {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) {i j : I} (hij : i ≠ j) (x y : X) : (A.fibre i x).transpose * A.fibre j y = 0

noncomputable def MetricCodes.HigherProjectionGraph.Data.combinedFibre {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (x : X) : Matrix (Fin D) (Fin d) ℝ

The sum of the fibre matrices weighted by their normalized amplitudes.

Equations

• A.combinedFibre x = ∑ i : I, A.amplitude i • A.fibre i x

theorem MetricCodes.HigherProjectionGraph.Data.combinedFibre_isometry {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x : X) : (A.combinedFibre x).transpose * A.combinedFibre x = 1

noncomputable def MetricCodes.HigherProjectionGraph.Data.combinedProjection {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (x : X) : Matrix (Fin D) (Fin D) ℝ

The projection matrix obtained by multiplying the combined fibre matrix by its transpose.

Equations

• A.combinedProjection x = A.combinedFibre x * (A.combinedFibre x).transpose

theorem MetricCodes.HigherProjectionGraph.Data.combinedProjection_symmetric {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (x : X) : (A.combinedProjection x).transpose = A.combinedProjection x

theorem MetricCodes.HigherProjectionGraph.Data.combinedProjection_idempotent {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x : X) : A.combinedProjection x * A.combinedProjection x = A.combinedProjection x

theorem MetricCodes.HigherProjectionGraph.Data.combinedProjection_trace {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x : X) : (A.combinedProjection x).trace = ↑d

noncomputable def MetricCodes.HigherProjectionGraph.Data.projectionFamily {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] : ProjectionFamily X D d

The projection family assembled from the weighted orthogonal fibres.

Equations

• A.projectionFamily = { projection := A.combinedProjection, symmetric := ⋯, idempotent := ⋯, trace_eq := ⋯ }

noncomputable def MetricCodes.HigherProjectionGraph.Data.edgeCoefficient {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (target source : I) : ℝ

The edge-channel coefficient scaled by the target-to-source amplitude ratio and the square root of the eigenvalue.

Equations

• A.edgeCoefficient target source = √(A.probability target source) * A.amplitude target / (√A.eigenvalue * A.amplitude source)

theorem MetricCodes.HigherProjectionGraph.Data.edgeCoefficient_sq {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (target source : I) : A.edgeCoefficient target source ^ 2 = A.probability target source * A.amplitude target ^ 2 / (A.eigenvalue * A.amplitude source ^ 2)

theorem MetricCodes.HigherProjectionGraph.Data.edgeCoefficient_sq_sum {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (source : I) : ∑ target : I, A.edgeCoefficient target source ^ 2 = 1

noncomputable def MetricCodes.HigherProjectionGraph.Data.assembledChannel {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) : Matrix (Fin Q) (Fin D) ℝ

The sum of all edge channels weighted by their edge coefficients.

Equations

• A.assembledChannel = ∑ e : I × I, A.edgeCoefficient e.1 e.2 • A.channel e.1 e.2

theorem MetricCodes.HigherProjectionGraph.Data.edgeCoefficient_smul_channelGram {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (target source : I) : (A.edgeCoefficient target source ^ 2 • if 0 < A.probability target source then A.block source else 0) = A.edgeCoefficient target source ^ 2 • A.block source

theorem MetricCodes.HigherProjectionGraph.Data.assembledChannel_isometry {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] : A.assembledChannel.transpose * A.assembledChannel = 1

theorem MetricCodes.HigherProjectionGraph.Data.edgeCoefficient_axis_scalar {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (target source : I) : A.edgeCoefficient target source * A.amplitude target * √(A.probability target source) = A.probability target source * A.amplitude target ^ 2 / (√A.eigenvalue * A.amplitude source)

theorem MetricCodes.HigherProjectionGraph.Data.edgeCoefficient_axis_sum {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (source : I) : ∑ target : I, A.edgeCoefficient target source * A.amplitude target * √(A.probability target source) = √A.eigenvalue * A.amplitude source

theorem MetricCodes.HigherProjectionGraph.Data.assembledChannel_axis {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x : X) : A.assembledChannel.transpose * A.axis x * A.combinedFibre x = √A.eigenvalue • A.combinedFibre x

theorem MetricCodes.HigherProjectionGraph.Data.assembledChannel_axis_projection {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x : X) : A.assembledChannel.transpose * A.axis x * A.combinedProjection x = √A.eigenvalue • A.combinedProjection x

theorem MetricCodes.HigherProjectionGraph.Data.projection_axis_transpose_assembled {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x : X) : A.combinedProjection x * (A.axis x).transpose * A.assembledChannel = √A.eigenvalue • A.combinedProjection x

noncomputable def MetricCodes.HigherProjectionGraph.Data.lift {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (x : X) : Matrix (Fin Q) (Fin D) ℝ

The lift used in the metric-code argument.

Equations

• A.lift x = A.axis x * A.combinedProjection x

noncomputable def MetricCodes.HigherProjectionGraph.Data.bulk {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (x : X) : Matrix (Fin Q) (Fin D) ℝ

The bulk used in the metric-code argument.

Equations

• A.bulk x = A.assembledChannel * A.combinedProjection x

noncomputable def MetricCodes.HigherProjectionGraph.Data.remainder {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (x : X) : Matrix (Fin Q) (Fin D) ℝ

The remainder used in the metric-code argument.

Equations

• A.remainder x = A.lift x - √A.eigenvalue • A.bulk x

theorem MetricCodes.HigherProjectionGraph.Data.lift_transpose_mul_lift {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (x y : X) : (A.lift x).transpose * A.lift y = A.correlation x y • (A.combinedProjection x * A.combinedProjection y)

theorem MetricCodes.HigherProjectionGraph.Data.bulk_transpose_mul_bulk {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x y : X) : (A.bulk x).transpose * A.bulk y = A.combinedProjection x * A.combinedProjection y

theorem MetricCodes.HigherProjectionGraph.Data.lift_transpose_mul_bulk {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x y : X) : (A.lift x).transpose * A.bulk y = √A.eigenvalue • (A.combinedProjection x * A.combinedProjection y)

theorem MetricCodes.HigherProjectionGraph.Data.bulk_transpose_mul_lift {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x y : X) : (A.bulk x).transpose * A.lift y = √A.eigenvalue • (A.combinedProjection x * A.combinedProjection y)

theorem MetricCodes.HigherProjectionGraph.Data.remainder_transpose_mul {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x y : X) : (A.remainder x).transpose * A.remainder y = (A.correlation x y - A.eigenvalue) • (A.combinedProjection x * A.combinedProjection y)

def MetricCodes.HigherProjectionGraph.Data.matrixFeature {D Q : ℕ} (M : Matrix (Fin Q) (Fin D) ℝ) : EuclideanSpace ℝ (Fin Q × Fin D)

The Euclidean vector of matrix entries used for the graph's Hilbert–Schmidt features.

Equations

• MetricCodes.HigherProjectionGraph.Data.matrixFeature M = WithLp.toLp 2 fun (i : Fin Q × Fin D) => M i.1 i.2

theorem MetricCodes.HigherProjectionGraph.Data.matrixFeature_inner {D Q : ℕ} (M N : Matrix (Fin Q) (Fin D) ℝ) : inner ℝ (matrixFeature M) (matrixFeature N) = (M.transpose * N).trace

noncomputable def MetricCodes.HigherProjectionGraph.Data.remainderFeature {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) (x : X) : EuclideanSpace ℝ (Fin Q × Fin D)

The Euclidean matrix-entry feature of the graph remainder at x.

Equations

• A.remainderFeature x = MetricCodes.HigherProjectionGraph.Data.matrixFeature (A.remainder x)

theorem MetricCodes.HigherProjectionGraph.Data.remainderFeature_inner {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (x y : X) : inner ℝ (A.remainderFeature x) (A.remainderFeature y) = (A.correlation x y - A.eigenvalue) * A.projectionFamily.overlap x y

theorem MetricCodes.HigherProjectionGraph.Data.ambientDimension_eq_sum {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) : ↑D = ∑ i : I, ↑(A.dimension i)

theorem MetricCodes.HigherProjectionGraph.Data.code_bound {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] {D d Q : ℕ} (A : Data I X D d Q) [Nonempty I] (C : Finset X) {s : ℝ} (hd : 0 < d) (hs : s < 1) (hgap : s < A.eigenvalue) (hdiag : ∀ x ∈ C, A.correlation x x = 1) (hsep : ∀ x ∈ C, ∀ y ∈ C, x ≠ y → A.correlation x y ≤ s) : ↑C.card ≤ (1 - s) / (A.eigenvalue - s) * ((∑ i : I, ↑(A.dimension i)) / ↑d)

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherProjectionInstantiation.SpherePoint (n : ℕ) : Type

The sphere point used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherProjectionInstantiation.SpherePoint n = { x : SpherePacking.Euclidean n // ‖x‖ = 1 }

structure MetricCodes.Spherical.HigherProjectionInstantiation.RealizedHilbertGraph (I : Type u_1) (X : Type u_2) (E : Type u_3) (V : Type u_4) (F : Type u_5) [Fintype I] [DecidableEq I] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] : Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

Data encoding the realized hilbert graph construction.

• dimension : I → ℕ

  The dimension component.

• dimension_pos (i : I) : 0 < self.dimension i
• block : I → V →ₗ[ℝ] V

  The block component.

• block_adjoint (i : I) : LinearMap.adjoint (self.block i) = self.block i
• block_idempotent (i : I) : self.block i ∘ₗ self.block i = self.block i
• block_orthogonal (i j : I) : i ≠ j → self.block i ∘ₗ self.block j = 0
• block_complete : ∑ i : I, self.block i = LinearMap.id
• block_trace (i : I) : (LinearMap.trace ℝ V) (self.block i) = ↑(self.dimension i)
• fibre : I → X → E →ₗᵢ[ℝ] V

  The fibre component.

• fibre_support (i : I) (x : X) : self.block i ∘ₗ (self.fibre i x).toLinearMap = (self.fibre i x).toLinearMap
• correlation : X → X → ℝ

  The correlation component.

• axis : X → V →ₗ[ℝ] F

  The axis component.

• axis_inner (x y : X) : LinearMap.adjoint (self.axis x) ∘ₗ self.axis y = self.correlation x y • LinearMap.id
• probability : I → I → ℝ

  The probability component.

• probability_nonneg (target source : I) : 0 ≤ self.probability target source
• balance (target source : I) : ↑(self.dimension target) * self.probability target source = ↑(self.dimension source) * self.probability source target
• channel : I → I → V →ₗ[ℝ] F

  The channel component.

• channel_isometry (target source : I) : LinearMap.adjoint (self.channel target source) ∘ₗ self.channel target source = if 0 < self.probability target source then self.block source else 0
• channel_orthogonal (target source target' source' : I) : (target, source) ≠ (target', source') → LinearMap.adjoint (self.channel target source) ∘ₗ self.channel target' source' = 0
• channel_axis (target source j : I) (x : X) : LinearMap.adjoint (self.channel target source) ∘ₗ self.axis x ∘ₗ (self.fibre j x).toLinearMap = if target = j then √(self.probability target source) • (self.fibre source x).toLinearMap else 0
• eigenvalue : ℝ

  The eigenvalue component.

• eigenvalue_pos : 0 < self.eigenvalue
• eigenvector : I → ℝ

  The eigenvector component.

• eigenvector_pos (i : I) : 0 < self.eigenvector i
• eigenvector_unit : ∑ i : I, self.eigenvector i ^ 2 = 1
• eigenvector_equation (i : I) : ∑ j : I, √(self.probability i j * self.probability j i) * self.eigenvector j = self.eigenvalue * self.eigenvector i

@[reducible, inline]

noncomputable abbrev MetricCodes.Spherical.HigherProjectionInstantiation.RealizedHilbertGraph.euclideanBasis (T : Type u_6) [NormedAddCommGroup T] [InnerProductSpace ℝ T] [FiniteDimensional ℝ T] : OrthonormalBasis (Fin (Module.finrank ℝ T)) ℝ T

The standard orthonormal basis indexed by the finite dimension of the real inner product space.

Equations

• MetricCodes.Spherical.HigherProjectionInstantiation.RealizedHilbertGraph.euclideanBasis T = stdOrthonormalBasis ℝ T

noncomputable def MetricCodes.Spherical.HigherProjectionInstantiation.RealizedHilbertGraph.coordinateMatrix {U : Type u_6} {T : Type u_7} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [NormedAddCommGroup T] [InnerProductSpace ℝ T] [FiniteDimensional ℝ T] (f : U →ₗ[ℝ] T) : Matrix (Fin (Module.finrank ℝ T)) (Fin (Module.finrank ℝ U)) ℝ

The matrix of a linear map in the standard orthonormal bases of its source and target.

Equations

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

noncomputable def MetricCodes.Spherical.HigherProjectionInstantiation.RealizedHilbertGraph.toFiniteData {I : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} {F : Type u_5} [Fintype I] [DecidableEq I] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (G : RealizedHilbertGraph I X E V F) : HigherProjectionGraph.Data I X (Module.finrank ℝ V) (Module.finrank ℝ E) (Module.finrank ℝ F)

The to finite data used in the spherical-code argument.

Equations

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

def MetricCodes.Spherical.HigherProjectionInstantiation.codePoints {n : ℕ} {s : ℝ} (C : SpherePacking.SphericalCode n s) : Finset (SpherePoint n)

The points of a spherical code bundled with their unit-norm proofs.

Equations

• MetricCodes.Spherical.HigherProjectionInstantiation.codePoints C = Finset.map { toFun := fun (x : ↥C.points) => ⟨↑x, ⋯⟩, inj' := ⋯ } C.points.attach

@[simp]

theorem MetricCodes.Spherical.HigherProjectionInstantiation.codePoints_card {n : ℕ} {s : ℝ} (C : SpherePacking.SphericalCode n s) : (codePoints C).card = C.points.card

theorem MetricCodes.Spherical.HigherProjectionInstantiation.mem_codePoints_iff {n : ℕ} {s : ℝ} (C : SpherePacking.SphericalCode n s) (x : SpherePoint n) : x ∈ codePoints C ↔ ↑x ∈ C.points

theorem MetricCodes.Spherical.HigherProjectionInstantiation.sphericalCode_bound_of_realized_graph {I : Type u_1} [Fintype I] [DecidableEq I] [Nonempty I] {n D d Q : ℕ} (A : HigherProjectionGraph.Data I (SpherePoint n) D d Q) (hinner : ∀ (x y : SpherePoint n), A.correlation x y = inner ℝ ↑x ↑y) {s : ℝ} (hd : 0 < d) (hs : s < 1) (hgap : s < A.eigenvalue) (C : SpherePacking.SphericalCode n s) : ↑C.points.card ≤ (1 - s) / (A.eigenvalue - s) * ((∑ i : I, ↑(A.dimension i)) / ↑d)

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherYoungGraphAssembly.VertexAmbient {I : Type u_1} (V : I → Type u_2) : Type (max u_1 u_2)

The vertex ambient used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungGraphAssembly.VertexAmbient V = PiLp 2 V

noncomputable def MetricCodes.Spherical.HigherYoungGraphAssembly.vertexInclusion {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] (i : I) : V i →ₗᵢ[ℝ] VertexAmbient V

The vertex inclusion used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungGraphAssembly.vertexInclusion V i = { toFun := fun (v : V i) => PiLp.single 2 i v, map_add' := ⋯, map_smul' := ⋯ }.isometryOfInner ⋯

@[simp]

theorem MetricCodes.Spherical.HigherYoungGraphAssembly.vertexInclusion_apply_self {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] (i : I) (v : V i) : ((vertexInclusion V i) v).ofLp i = v

@[simp]

theorem MetricCodes.Spherical.HigherYoungGraphAssembly.vertexInclusion_apply_ne {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] {i j : I} (h : j ≠ i) (v : V i) : ((vertexInclusion V i) v).ofLp j = 0

@[simp]

theorem MetricCodes.Spherical.HigherYoungGraphAssembly.vertexInclusion_adjoint_apply {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] [∀ (i : I), FiniteDimensional ℝ (V i)] (i : I) (v : VertexAmbient V) : (LinearMap.adjoint (vertexInclusion V i).toLinearMap) v = v.ofLp i

noncomputable def MetricCodes.Spherical.HigherYoungGraphAssembly.vertexProjection {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] [∀ (i : I), FiniteDimensional ℝ (V i)] (i : I) : VertexAmbient V →ₗ[ℝ] VertexAmbient V

The vertex projection used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherYoungGraphAssembly.vertexProjection_apply_self {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] [∀ (i : I), FiniteDimensional ℝ (V i)] (i : I) (v : VertexAmbient V) : ((vertexProjection V i) v).ofLp i = v.ofLp i

@[simp]

theorem MetricCodes.Spherical.HigherYoungGraphAssembly.vertexProjection_apply_ne {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] [∀ (i : I), FiniteDimensional ℝ (V i)] {i j : I} (h : j ≠ i) (v : VertexAmbient V) : ((vertexProjection V i) v).ofLp j = 0

theorem MetricCodes.Spherical.HigherYoungGraphAssembly.vertexProjection_adjoint {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] [∀ (i : I), FiniteDimensional ℝ (V i)] (i : I) : LinearMap.adjoint (vertexProjection V i) = vertexProjection V i

theorem MetricCodes.Spherical.HigherYoungGraphAssembly.vertexProjection_idempotent {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] [∀ (i : I), FiniteDimensional ℝ (V i)] (i : I) : vertexProjection V i ∘ₗ vertexProjection V i = vertexProjection V i

theorem MetricCodes.Spherical.HigherYoungGraphAssembly.vertexProjection_orthogonal {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] [∀ (i : I), FiniteDimensional ℝ (V i)] {i j : I} (h : i ≠ j) : vertexProjection V i ∘ₗ vertexProjection V j = 0

theorem MetricCodes.Spherical.HigherYoungGraphAssembly.sum_vertexProjection {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] [∀ (i : I), FiniteDimensional ℝ (V i)] : ∑ i : I, vertexProjection V i = LinearMap.id

theorem MetricCodes.Spherical.HigherYoungGraphAssembly.trace_vertexProjection {I : Type u_1} [Fintype I] [DecidableEq I] (V : I → Type u_2) [(i : I) → NormedAddCommGroup (V i)] [(i : I) → InnerProductSpace ℝ (V i)] [∀ (i : I), FiniteDimensional ℝ (V i)] (i : I) : (LinearMap.trace ℝ (VertexAmbient V)) (vertexProjection V i) = ↑(Module.finrank ℝ (V i))

noncomputable def MetricCodes.Spherical.HigherYoungMovingFibres.movingYoungFibre {r n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (lam : Fin (r + 1) → ℕ) (o : HigherProjectionInstantiation.SpherePoint n) (base : E →ₗᵢ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (x : HigherProjectionInstantiation.SpherePoint n) : E →ₗᵢ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)

The moving young fibre used in the spherical-code argument.

Equations

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

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherYoungMovingFibres.YoungVertex {I : Type u_1} {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (i : I) : Type

The young vertex used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungMovingFibres.YoungVertex lam i = ↥(MetricCodes.Spherical.HigherHarmonicYoung.HarmonicYoungSpace (lam i))

noncomputable def MetricCodes.Spherical.HigherYoungMovingFibres.movingYoungBlockFibre {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (lam : I → Fin (r + 1) → ℕ) (o : HigherProjectionInstantiation.SpherePoint n) (base : (i : I) → E →ₗᵢ[ℝ] YoungVertex lam i) (i : I) (x : HigherProjectionInstantiation.SpherePoint n) : E →ₗᵢ[ℝ] HigherYoungGraphAssembly.VertexAmbient (YoungVertex lam)

The moving young block fibre used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherYoungMovingFibres.movingYoungBlockFibre_apply_self {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (lam : I → Fin (r + 1) → ℕ) (o : HigherProjectionInstantiation.SpherePoint n) (base : (i : I) → E →ₗᵢ[ℝ] YoungVertex lam i) (i : I) (x : HigherProjectionInstantiation.SpherePoint n) (v : E) : ((movingYoungBlockFibre lam o base i x) v).ofLp i = (movingYoungFibre (lam i) o (base i) x) v

@[simp]

theorem MetricCodes.Spherical.HigherYoungMovingFibres.movingYoungBlockFibre_apply_ne {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (lam : I → Fin (r + 1) → ℕ) (o : HigherProjectionInstantiation.SpherePoint n) (base : (i : I) → E →ₗᵢ[ℝ] YoungVertex lam i) (i j : I) (hji : j ≠ i) (x : HigherProjectionInstantiation.SpherePoint n) (v : E) : ((movingYoungBlockFibre lam o base i x) v).ofLp j = 0

theorem MetricCodes.Spherical.HigherYoungMovingFibres.movingYoungBlockFibre_support {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (lam : I → Fin (r + 1) → ℕ) (o : HigherProjectionInstantiation.SpherePoint n) (base : (i : I) → E →ₗᵢ[ℝ] YoungVertex lam i) (i : I) (x : HigherProjectionInstantiation.SpherePoint n) : HigherYoungGraphAssembly.vertexProjection (YoungVertex lam) i ∘ₗ (movingYoungBlockFibre lam o base i x).toLinearMap = (movingYoungBlockFibre lam o base i x).toLinearMap

def MetricCodes.Spherical.HigherYoungMovingFibres.axisTensor {n : ℕ} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : HigherProjectionInstantiation.SpherePoint n) : V →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) V

The axis tensor used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungMovingFibres.axisTensor x = (TensorProduct.mk ℝ (SpherePacking.Euclidean n) V) ↑x

@[simp]

theorem MetricCodes.Spherical.HigherYoungMovingFibres.axisTensor_apply {n : ℕ} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : HigherProjectionInstantiation.SpherePoint n) (v : V) : (axisTensor x) v = ↑x ⊗ₜ[ℝ] v

theorem MetricCodes.Spherical.HigherYoungMovingFibres.axisTensor_adjoint_comp {n : ℕ} {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (x y : HigherProjectionInstantiation.SpherePoint n) : LinearMap.adjoint (axisTensor x) ∘ₗ axisTensor y = inner ℝ ↑x ↑y • LinearMap.id

theorem MetricCodes.Spherical.HigherHarmonicYoung.GelfandTsetlin.rowEuler_mul {r n : ℕ} (i : Fin (r + 1)) (p q : PolynomialSpace r n) : (rowEuler r n i) (p * q) = (rowEuler r n i) p * q + p * (rowEuler r n i) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.GelfandTsetlin.polarization_mul {r n : ℕ} (i j : Fin (r + 1)) (p q : PolynomialSpace r n) : (polarization r n i j) (p * q) = (polarization r n i j) p * q + p * (polarization r n i j) q

theorem MetricCodes.Spherical.HigherYoungBranchingFibres.multiFactorial_eq_finsupp_prod {n : ℕ} (a : Fin n →₀ ℕ) : SpherePacking.Fischer.multiFactorial a = a.prod fun (x : Fin n) (k : ℕ) => ↑k.factorial

theorem MetricCodes.Spherical.HigherYoungBranchingFibres.multiFactorial_mapDomain {n m : ℕ} (f : Fin n → Fin m) (hf : Function.Injective f) (a : Fin n →₀ ℕ) : SpherePacking.Fischer.multiFactorial (Finsupp.mapDomain f a) = SpherePacking.Fischer.multiFactorial a

theorem MetricCodes.Spherical.HigherYoungBranchingFibres.polynomialInner_rename_injective {n m : ℕ} (f : Fin n → Fin m) (hf : Function.Injective f) (p q : MvPolynomial (Fin n) ℝ) : SpherePacking.Fischer.polynomialInner m ((MvPolynomial.rename f) p) ((MvPolynomial.rename f) q) = SpherePacking.Fischer.polynomialInner n p q

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.rowPairingPolynomial {r n : ℕ} (i j : Fin (r + 1)) : PolynomialSpace r n

The row pairing polynomial used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowPairingPolynomial_isHomogeneous {r n : ℕ} (i j : Fin (r + 1)) : MvPolynomial.IsHomogeneous (rowPairingPolynomial i j) 2

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.homogeneousRowPairingMultiplication {r n : ℕ} (i j : Fin (r + 1)) (m : ℕ) : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m) →ₗ[ℝ] ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (m + 2))

The homogeneous row pairing multiplication used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.homogeneousRowPairingMultiplication i j m = (LinearMap.mulLeft ℝ (MetricCodes.Spherical.HigherHarmonicYoung.rowPairingPolynomial i j)).restrict ⋯

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.homogeneousRowPairingMultiplication_apply {r n : ℕ} (i j : Fin (r + 1)) (m : ℕ) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) : ↑((homogeneousRowPairingMultiplication i j m) p) = rowPairingPolynomial i j * ↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.traceOperator_isHomogeneous {r n m : ℕ} (i j : Fin (r + 1)) (p : PolynomialSpace r n) (hp : MvPolynomial.IsHomogeneous p m) : MvPolynomial.IsHomogeneous ((traceOperator r n i j) p) (m - 2)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.homogeneousRowTrace {r n : ℕ} (i j : Fin (r + 1)) (m : ℕ) : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (m + 2)) →ₗ[ℝ] ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)

The homogeneous row trace used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.homogeneousRowTrace_apply {r n : ℕ} (i j : Fin (r + 1)) (m : ℕ) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (m + 2))) : ↑((homogeneousRowTrace i j m) p) = (traceOperator r n i j) ↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialInner_rowPairing_trace {r n : ℕ} (i j : Fin (r + 1)) (p q : PolynomialSpace r n) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) (rowPairingPolynomial i j * p) q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) p ((traceOperator r n i j) q)

structure MetricCodes.Spherical.HigherHarmonicYoung.YoungPolynomialFrame {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (ι : Type u_1) : Type u_1

Data encoding the young polynomial frame construction.

• polynomial : ι → PolynomialSpace r n

  The polynomial component.

• homogeneous (i : ι) : MvPolynomial.IsHomogeneous (self.polynomial i) (∑ j : Fin (r + 1), lam j)
• rowEuler (i : ι) (j : Fin (r + 1)) : (HigherHarmonicYoung.rowEuler r n j) (self.polynomial i) = ↑(lam j) • self.polynomial i
• traceFree (i : ι) (j k : Fin (r + 1)) : (traceOperator r n j k) (self.polynomial i) = 0
• highestWeight (i : ι) (j k : Fin (r + 1)) : j < k → (polarization r n j k) (self.polynomial i) = 0
• independent : LinearIndependent ℝ self.polynomial

def MetricCodes.Spherical.HigherHarmonicYoung.YoungPolynomialFrame.vector {r n : ℕ} {lam : Fin (r + 1) → ℕ} {ι : Type u_1} (F : YoungPolynomialFrame n lam ι) (i : ι) : ↥(HarmonicYoungSpace lam)

The harmonic Young vector obtained from a frame polynomial and its defining certificates.

Equations

• F.vector i = ⟨F.polynomial i, ⋯⟩

theorem MetricCodes.Spherical.HigherHarmonicYoung.YoungPolynomialFrame.vector_linearIndependent {r n : ℕ} {lam : Fin (r + 1) → ℕ} {ι : Type u_1} (F : YoungPolynomialFrame n lam ι) : LinearIndependent ℝ F.vector

theorem MetricCodes.Spherical.HigherHarmonicYoung.YoungPolynomialFrame.span_vector_eq_top {r n : ℕ} {lam : Fin (r + 1) → ℕ} {ι : Type u_1} (F : YoungPolynomialFrame n lam ι) (hspan : ∀ p ∈ harmonicYoungSubmodule lam, p ∈ Submodule.span ℝ (Set.range F.polynomial)) : Submodule.span ℝ (Set.range F.vector) = ⊤

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.YoungPolynomialFrame.basis {r n : ℕ} {lam : Fin (r + 1) → ℕ} {ι : Type u_1} (F : YoungPolynomialFrame n lam ι) (hspan : ∀ p ∈ harmonicYoungSubmodule lam, p ∈ Submodule.span ℝ (Set.range F.polynomial)) : Module.Basis ι ℝ ↥(HarmonicYoungSpace lam)

The basis used in the spherical-code argument.

Equations

• F.basis hspan = Module.Basis.mk ⋯ ⋯

theorem MetricCodes.Spherical.HigherHarmonicYoung.variableIndex_eq_iff_harmonicLift {r n : ℕ} (i j : Fin (r + 1)) (a b : Fin n) : variableIndex i a = variableIndex j b ↔ i = j ∧ a = b

theorem MetricCodes.Spherical.HigherHarmonicYoung.pderiv_polarization_harmonicLift {r n : ℕ} (a i j : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) : (MvPolynomial.pderiv (variableIndex a k)) ((polarization r n i j) p) = (if a = i then (MvPolynomial.pderiv (variableIndex j k)) p else 0) + (polarization r n i j) ((MvPolynomial.pderiv (variableIndex a k)) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.traceOperator_polarization_harmonicLift {r n : ℕ} (a b i j : Fin (r + 1)) (p : PolynomialSpace r n) : (traceOperator r n a b) ((polarization r n i j) p) = ((polarization r n i j) ((traceOperator r n a b) p) + if a = i then (traceOperator r n j b) p else 0) + if b = i then (traceOperator r n a j) p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.traceFree_of_firstTrace_and_highestWeight {r n : ℕ} (p : PolynomialSpace r n) (hfirst : (traceOperator r n 0 0) p = 0) (hyoung : ∀ (i j : Fin (r + 1)), i < j → (polarization r n i j) p = 0) (a b : Fin (r + 1)) : (traceOperator r n a b) p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_harmonicYoungSubmodule_iff_firstTrace_and_highestWeight {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : PolynomialSpace r n) : p ∈ harmonicYoungSubmodule lam ↔ MvPolynomial.IsHomogeneous p (∑ i : Fin (r + 1), lam i) ∧ (∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p) ∧ (traceOperator r n 0 0) p = 0 ∧ ∀ (i j : Fin (r + 1)), i < j → (polarization r n i j) p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_harmonicYoungSubmodule_iff_multihomogeneous_firstTrace_highestWeight {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : PolynomialSpace r n) : p ∈ harmonicYoungSubmodule lam ↔ p ∈ youngMultihomogeneousSubmodule n lam ∧ (traceOperator r n 0 0) p = 0 ∧ ∀ (i j : Fin (r + 1)), i < j → (polarization r n i j) p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_mem_traceFreeSubmodule {r n : ℕ} (i j : Fin (r + 1)) (p : PolynomialSpace r n) (hp : p ∈ traceFreeSubmodule r n) : (polarization r n i j) p ∈ traceFreeSubmodule r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialInner_polarization_harmonicLift {r n : ℕ} (i j : Fin (r + 1)) (p q : PolynomialSpace r n) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((polarization r n i j) p) q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) p ((polarization r n j i) q)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.homogeneousTraceFreeSubmodule (r n m : ℕ) : Submodule ℝ ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)

The homogeneous trace free submodule used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_homogeneousTraceFreeSubmodule {r n m : ℕ} (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) : p ∈ homogeneousTraceFreeSubmodule r n m ↔ ∀ (i j : Fin (r + 1)), (traceOperator r n i j) ↑p = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.homogeneousTraceFreeCoefficientEmbedding (r n m : ℕ) : ↥(homogeneousTraceFreeSubmodule r n m) →ₗ[ℝ] SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) m

The coefficient embedding restricted to homogeneous trace-free polynomials.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.homogeneousTraceFreeCoefficientEmbedding_injective (r n m : ℕ) : Function.Injective ⇑(homogeneousTraceFreeCoefficientEmbedding r n m)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.homogeneousTraceFreeCoefficientRange (r n m : ℕ) : Submodule ℝ (SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) m)

The range of the homogeneous trace-free coefficient embedding.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.homogeneousTraceFreeCoefficientRange r n m = (MetricCodes.Spherical.HigherHarmonicYoung.homogeneousTraceFreeCoefficientEmbedding r n m).range

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicCoefficientProjection (r n m : ℕ) : SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) m →ₗ[ℝ] ↥(homogeneousTraceFreeSubmodule r n m)

Orthogonally project coefficient space to the homogeneous trace-free range and recover the polynomial.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicProjection (r n m : ℕ) : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m) →ₗ[ℝ] ↥(homogeneousTraceFreeSubmodule r n m)

The simultaneous harmonic projection used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicProjection_traceFree {r n m : ℕ} (p : ↥(homogeneousTraceFreeSubmodule r n m)) : (simultaneousHarmonicProjection r n m) ↑p = p

theorem MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicProjection_traceOperator {r n m : ℕ} (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) (i j : Fin (r + 1)) : (traceOperator r n i j) ↑↑((simultaneousHarmonicProjection r n m) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicProjection_coefficient_eq_projection {r n m : ℕ} (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) : (homogeneousTraceFreeCoefficientEmbedding r n m) ((simultaneousHarmonicProjection r n m) p) = ((homogeneousTraceFreeCoefficientRange r n m).projection (homogeneousTraceFreeCoefficientRange r n m)ᗮ ⋯) ((SpherePacking.Fischer.coefficientEmbedding ((r + 1) * n) m) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicProjection_residual_orthogonal {r n m : ℕ} (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) : (SpherePacking.Fischer.coefficientEmbedding ((r + 1) * n) m) p - (homogeneousTraceFreeCoefficientEmbedding r n m) ((simultaneousHarmonicProjection r n m) p) ∈ (homogeneousTraceFreeCoefficientRange r n m)ᗮ

theorem MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicProjection_polynomialInner {r n m : ℕ} (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) (q : ↥(homogeneousTraceFreeSubmodule r n m)) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) ↑↑((simultaneousHarmonicProjection r n m) p) ↑↑q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) ↑p ↑↑q

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_isHomogeneous_harmonicLift {r n m : ℕ} (i j : Fin (r + 1)) (p : PolynomialSpace r n) (hp : MvPolynomial.IsHomogeneous p m) : MvPolynomial.IsHomogeneous ((polarization r n i j) p) m

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.homogeneousPolarization (r n m : ℕ) (i j : Fin (r + 1)) : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m) →ₗ[ℝ] ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)

The row polarization operator restricted to homogeneous degree m.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.homogeneousPolarization r n m i j = (MetricCodes.Spherical.HigherHarmonicYoung.polarization r n i j).restrict ⋯

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.homogeneousPolarization_apply_coe {r n m : ℕ} (i j : Fin (r + 1)) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) : ↑((homogeneousPolarization r n m i j) p) = (polarization r n i j) ↑p

theorem MetricCodes.Spherical.HigherHarmonicYoung.homogeneousPolarization_mem_traceFree {r n m : ℕ} (i j : Fin (r + 1)) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) (hp : p ∈ homogeneousTraceFreeSubmodule r n m) : (homogeneousPolarization r n m i j) p ∈ homogeneousTraceFreeSubmodule r n m

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.traceFreeHomogeneousPolarization (r n m : ℕ) (i j : Fin (r + 1)) : ↥(homogeneousTraceFreeSubmodule r n m) →ₗ[ℝ] ↥(homogeneousTraceFreeSubmodule r n m)

The row polarization operator restricted further to homogeneous trace-free polynomials.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.traceFreeHomogeneousPolarization r n m i j = (MetricCodes.Spherical.HigherHarmonicYoung.homogeneousPolarization r n m i j).restrict ⋯

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialInner_sub_left_harmonicLift {N : ℕ} (p q s : MvPolynomial (Fin N) ℝ) : SpherePacking.Fischer.polynomialInner N (p - q) s = SpherePacking.Fischer.polynomialInner N p s - SpherePacking.Fischer.polynomialInner N q s

theorem MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicProjection_polarization {r n m : ℕ} (i j : Fin (r + 1)) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) : (simultaneousHarmonicProjection r n m) ((homogeneousPolarization r n m i j) p) = (traceFreeHomogeneousPolarization r n m i j) ((simultaneousHarmonicProjection r n m) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicProjection_polarization_coe {r n m : ℕ} (i j : Fin (r + 1)) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) : ↑↑((simultaneousHarmonicProjection r n m) ((homogeneousPolarization r n m i j) p)) = (polarization r n i j) ↑↑((simultaneousHarmonicProjection r n m) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicProjection_rowWeight {r n m : ℕ} (i : Fin (r + 1)) (c : ℝ) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) (hp : (rowEuler r n i) ↑p = c • ↑p) : (rowEuler r n i) ↑↑((simultaneousHarmonicProjection r n m) p) = c • ↑↑((simultaneousHarmonicProjection r n m) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.simultaneousHarmonicProjection_polarization_eq_zero {r n m : ℕ} (i j : Fin (r + 1)) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) m)) (hp : (polarization r n i j) ↑p = 0) : (polarization r n i j) ↑↑((simultaneousHarmonicProjection r n m) p) = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.homogeneousYoungHighestWeightSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Submodule ℝ ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (∑ i : Fin (r + 1), lam i))

The homogeneous young highest weight submodule used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_homogeneousYoungHighestWeightSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (∑ i : Fin (r + 1), lam i))) : p ∈ homogeneousYoungHighestWeightSubmodule lam ↔ (∀ (i : Fin (r + 1)), (rowEuler r n i) ↑p = ↑(lam i) • ↑p) ∧ ∀ (i j : Fin (r + 1)), i < j → (polarization r n i j) ↑p = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.harmonicYoungHighestWeightEmbedding {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] ↥(homogeneousYoungHighestWeightSubmodule lam)

The harmonic young highest weight embedding used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngHarmonicLift {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ↥(homogeneousYoungHighestWeightSubmodule lam) →ₗ[ℝ] ↥(HarmonicYoungSpace lam)

The young harmonic lift used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_youngMultihomogeneousSubmodule_iff_rowEuler {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : PolynomialSpace r n) : p ∈ youngMultihomogeneousSubmodule n lam ↔ ∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_mul_euler {r n : ℕ} (i j : Fin (r + 1)) (p q : PolynomialSpace r n) : (polarization r n i j) (p * q) = (polarization r n i j) p * q + p * (polarization r n i j) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_X_euler {r n : ℕ} (i j a : Fin (r + 1)) (k : Fin n) : (polarization r n i j) (MvPolynomial.X (variableIndex a k)) = if j = a then MvPolynomial.X (variableIndex i k) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuler_polarization_commutator {r n : ℕ} (a i j : Fin (r + 1)) (p : PolynomialSpace r n) : (rowEuler r n a) ((polarization r n i j) p) = ((polarization r n i j) ((rowEuler r n a) p) + if a = i then (polarization r n i j) p else 0) - if a = j then (polarization r n i j) p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_mem_youngMultihomogeneous_transfer {r n : ℕ} (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (hij : i ≠ j) {p : PolynomialSpace r n} (hp : p ∈ youngMultihomogeneousSubmodule n (Function.update lam j (lam j + 1))) : (polarization r n i j) p ∈ youngMultihomogeneousSubmodule n (Function.update lam i (lam i + 1))

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneous_pderiv_eq_zero_of_rowDegree_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(youngMultihomogeneousSubmodule n lam)) (a : Fin (r + 1)) (ha : lam a = 0) (k : Fin n) : (MvPolynomial.pderiv (variableIndex a k)) ↑p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneous_polarization_eq_zero_of_rowDegree_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(youngMultihomogeneousSubmodule n lam)) (a b : Fin (r + 1)) (hb : lam b = 0) : (polarization r n a b) ↑p = 0

def MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.FullBranchWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) : Type

The full branch weight used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam = { mu : (i : Fin (r + 1)) → Fin (lam i + 1) // ∀ (i : Fin r), lam i.succ ≤ ↑(mu i.castSucc) }

@[instance_reducible]

instance MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchWeightFintype {r : ℕ} (lam : Fin (r + 1) → ℕ) : Fintype (FullBranchWeight lam)

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchWeightFintype lam = id inferInstance

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchWeightDecidableEq {r : ℕ} (lam : Fin (r + 1) → ℕ) : DecidableEq (FullBranchWeight lam)

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchWeightDecidableEq lam = Classical.decEq (MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam)

def MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchSignature {r : ℕ} {lam : Fin (r + 1) → ℕ} (mu : FullBranchWeight lam) : Fin (r + 1) → ℕ

The full branch signature used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu i = ↑(↑mu i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchSignature_le {r : ℕ} {lam : Fin (r + 1) → ℕ} (mu : FullBranchWeight lam) (i : Fin (r + 1)) : fullBranchSignature mu i ≤ lam i

theorem MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchSignature_succ_le {r : ℕ} {lam : Fin (r + 1) → ℕ} (mu : FullBranchWeight lam) (i : Fin r) : lam i.succ ≤ fullBranchSignature mu i.castSucc

theorem MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchSignature_antitone {r : ℕ} {lam : Fin (r + 1) → ℕ} (mu : FullBranchWeight lam) : Antitone (fullBranchSignature mu)

def MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchOfInterlaces {r : ℕ} {lam : Fin (r + 1) → ℕ} (mu : Fin r → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) : FullBranchWeight lam

The full branch of interlaces used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchOfInterlaces mu h = ⟨fun (i : Fin (r + 1)) => ⟨Fin.snoc mu 0 i, ⋯⟩, ⋯⟩

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchOfInterlaces_castSucc {r : ℕ} {lam : Fin (r + 1) → ℕ} (mu : Fin r → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (i : Fin r) : fullBranchSignature (fullBranchOfInterlaces mu h) i.castSucc = mu i

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchOfInterlaces_last {r : ℕ} {lam : Fin (r + 1) → ℕ} (mu : Fin r → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) : fullBranchSignature (fullBranchOfInterlaces mu h) (Fin.last r) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.fullBranchOfInterlaces_signature {r : ℕ} {lam : Fin (r + 1) → ℕ} (mu : Fin r → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) : fullBranchSignature (fullBranchOfInterlaces mu h) = Fin.snoc mu 0

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

The weyl branching recurrence used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.polynomialRealPart {σ : Type u_1} : MvPolynomial σ ℂ →ₗ[ℝ] MvPolynomial σ ℝ

The polynomial real part used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.polynomialRealPart = ↑(AddMonoidAlgebra.coeffLinearEquiv ℝ).symm ∘ₗ Finsupp.mapRange.linearMap Complex.reLm ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv ℝ)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.polynomialImaginaryPart {σ : Type u_1} : MvPolynomial σ ℂ →ₗ[ℝ] MvPolynomial σ ℝ

The polynomial imaginary part used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.coeff_polynomialRealPart {σ : Type u_1} (p : MvPolynomial σ ℂ) (d : σ →₀ ℕ) : (polynomialRealPart p).coeff d = (p.coeff d).re

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.coeff_polynomialImaginaryPart {σ : Type u_1} (p : MvPolynomial σ ℂ) (d : σ →₀ ℕ) : (polynomialImaginaryPart p).coeff d = (p.coeff d).im

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialRealPart_ne_zero_or_polynomialImaginaryPart_ne_zero {σ : Type u_1} {p : MvPolynomial σ ℂ} (hp : p ≠ 0) : polynomialRealPart p ≠ 0 ∨ polynomialImaginaryPart p ≠ 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialRealPart_pderiv {σ : Type u_1} (i : σ) (p : MvPolynomial σ ℂ) : polynomialRealPart ((MvPolynomial.pderiv i) p) = (MvPolynomial.pderiv i) (polynomialRealPart p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialImaginaryPart_pderiv {σ : Type u_1} (i : σ) (p : MvPolynomial σ ℂ) : polynomialImaginaryPart ((MvPolynomial.pderiv i) p) = (MvPolynomial.pderiv i) (polynomialImaginaryPart p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialRealPart_X_mul {σ : Type u_1} (i : σ) (p : MvPolynomial σ ℂ) : polynomialRealPart (MvPolynomial.X i * p) = MvPolynomial.X i * polynomialRealPart p

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialImaginaryPart_X_mul {σ : Type u_1} (i : σ) (p : MvPolynomial σ ℂ) : polynomialImaginaryPart (MvPolynomial.X i * p) = MvPolynomial.X i * polynomialImaginaryPart p

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialRealPart_isHomogeneous {σ : Type u_1} {p : MvPolynomial σ ℂ} {k : ℕ} (hp : p.IsHomogeneous k) : (polynomialRealPart p).IsHomogeneous k

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialImaginaryPart_isHomogeneous {σ : Type u_1} {p : MvPolynomial σ ℂ} {k : ℕ} (hp : p.IsHomogeneous k) : (polynomialImaginaryPart p).IsHomogeneous k

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.complexRowEuler {r n : ℕ} (i : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : MvPolynomial (Fin ((r + 1) * n)) ℂ

The complex row euler used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.complexTraceOperator {r n : ℕ} (i j : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : MvPolynomial (Fin ((r + 1) * n)) ℂ

The complex trace operator used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.complexPolarization {r n : ℕ} (i j : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : MvPolynomial (Fin ((r + 1) * n)) ℂ

The complex polarization used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialRealPart_complexRowEuler {r n : ℕ} (i : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : polynomialRealPart (complexRowEuler i p) = (rowEuler r n i) (polynomialRealPart p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialImaginaryPart_complexRowEuler {r n : ℕ} (i : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : polynomialImaginaryPart (complexRowEuler i p) = (rowEuler r n i) (polynomialImaginaryPart p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialRealPart_complexTraceOperator {r n : ℕ} (i j : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : polynomialRealPart (complexTraceOperator i j p) = (traceOperator r n i j) (polynomialRealPart p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialImaginaryPart_complexTraceOperator {r n : ℕ} (i j : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : polynomialImaginaryPart (complexTraceOperator i j p) = (traceOperator r n i j) (polynomialImaginaryPart p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialRealPart_complexPolarization {r n : ℕ} (i j : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : polynomialRealPart (complexPolarization i j p) = (polarization r n i j) (polynomialRealPart p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialImaginaryPart_complexPolarization {r n : ℕ} (i j : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : polynomialImaginaryPart (complexPolarization i j p) = (polarization r n i j) (polynomialImaginaryPart p)

structure MetricCodes.Spherical.HigherHarmonicYoung.ComplexHighestWeightWitness {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Type

Data encoding the complex highest weight witness construction.

• polynomial : MvPolynomial (Fin ((r + 1) * n)) ℂ

  The polynomial component.

• nonzero : self.polynomial ≠ 0
• homogeneous : self.polynomial.IsHomogeneous (∑ i : Fin (r + 1), lam i)
• rowEuler (i : Fin (r + 1)) : complexRowEuler i self.polynomial = ↑(lam i) • self.polynomial
• traceFree (i j : Fin (r + 1)) : complexTraceOperator i j self.polynomial = 0
• highestWeight (i j : Fin (r + 1)) : i < j → complexPolarization i j self.polynomial = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ComplexHighestWeightWitness.realPart_mem {r n : ℕ} {lam : Fin (r + 1) → ℕ} (w : ComplexHighestWeightWitness lam) : polynomialRealPart w.polynomial ∈ harmonicYoungSubmodule lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.ComplexHighestWeightWitness.imaginaryPart_mem {r n : ℕ} {lam : Fin (r + 1) → ℕ} (w : ComplexHighestWeightWitness lam) : polynomialImaginaryPart w.polynomial ∈ harmonicYoungSubmodule lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.exists_nonzero_harmonicYoung_of_complexWitness {r n : ℕ} {lam : Fin (r + 1) → ℕ} (w : ComplexHighestWeightWitness lam) : ∃ (p : ↥(HarmonicYoungSpace lam)), p ≠ 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_harmonicYoung_pos_of_complexWitness {r n : ℕ} {lam : Fin (r + 1) → ℕ} (w : ComplexHighestWeightWitness lam) : 0 < Module.finrank ℝ ↥(HarmonicYoungSpace lam)

def MetricCodes.Spherical.HigherHarmonicYoung.nullEvenCoordinate {m n : ℕ} (hn : 2 * m ≤ n) (i : Fin m) : Fin n

The even coordinate 2 * i in the ambient space reserved for a null-coordinate pair.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.nullEvenCoordinate hn i = ⟨2 * ↑i, ⋯⟩

def MetricCodes.Spherical.HigherHarmonicYoung.nullOddCoordinate {m n : ℕ} (hn : 2 * m ≤ n) (i : Fin m) : Fin n

The odd coordinate 2 * i + 1 in the ambient space reserved for a null-coordinate pair.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.nullOddCoordinate hn i = ⟨2 * ↑i + 1, ⋯⟩

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.nullEvenCoordinate_inj {m n : ℕ} (hn : 2 * m ≤ n) {i j : Fin m} : nullEvenCoordinate hn i = nullEvenCoordinate hn j ↔ i = j

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.nullOddCoordinate_inj {m n : ℕ} (hn : 2 * m ≤ n) {i j : Fin m} : nullOddCoordinate hn i = nullOddCoordinate hn j ↔ i = j

theorem MetricCodes.Spherical.HigherHarmonicYoung.nullEvenCoordinate_ne_nullOddCoordinate {m n : ℕ} (hn : 2 * m ≤ n) (i j : Fin m) : nullEvenCoordinate hn i ≠ nullOddCoordinate hn j

def MetricCodes.Spherical.HigherHarmonicYoung.nullCoordinateCoefficient {m n : ℕ} (hn : 2 * m ≤ n) (i : Fin m) (k : Fin n) : ℂ

The complex coefficients 1 and I on the even and odd coordinates of a null pair, and zero elsewhere.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.sum_nullCoordinateCoefficient_mul {m n : ℕ} (hn : 2 * m ≤ n) (i j : Fin m) : ∑ k : Fin n, nullCoordinateCoefficient hn i k * nullCoordinateCoefficient hn j k = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.variableIndex_eq_iff {r n : ℕ} (i j : Fin (r + 1)) (k l : Fin n) : variableIndex i k = variableIndex j l ↔ i = j ∧ k = l

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.nullRowLinearForm {r m n : ℕ} (hn : 2 * m ≤ n) (i : Fin (r + 1)) (j : Fin m) : MvPolynomial (Fin ((r + 1) * n)) ℂ

The null row linear form used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.pderiv_nullRowLinearForm {r m n : ℕ} (hn : 2 * m ≤ n) (h i : Fin (r + 1)) (j : Fin m) (k : Fin n) : (MvPolynomial.pderiv (variableIndex h k)) (nullRowLinearForm hn i j) = if h = i then MvPolynomial.C (nullCoordinateCoefficient hn j k) else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.nullSubstitution {r m n : ℕ} (hn : 2 * m ≤ n) : MvPolynomial (Fin (r + 1) × Fin m) ℂ →ₐ[ℂ] MvPolynomial (Fin ((r + 1) * n)) ℂ

The null substitution used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.nullSubstitution hn = MvPolynomial.aeval fun (z : Fin (r + 1) × Fin m) => MetricCodes.Spherical.HigherHarmonicYoung.nullRowLinearForm hn z.1 z.2

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.nullSubstitution_X {r m n : ℕ} (hn : 2 * m ≤ n) (i : Fin (r + 1)) (j : Fin m) : (nullSubstitution hn) (MvPolynomial.X (i, j)) = nullRowLinearForm hn i j

theorem MetricCodes.Spherical.HigherHarmonicYoung.pderiv_nullSubstitution {r m n : ℕ} (hn : 2 * m ≤ n) (i : Fin (r + 1)) (k : Fin n) (q : MvPolynomial (Fin (r + 1) × Fin m) ℂ) : (MvPolynomial.pderiv (variableIndex i k)) ((nullSubstitution hn) q) = ∑ j : Fin m, MvPolynomial.C (nullCoordinateCoefficient hn j k) * (nullSubstitution hn) ((MvPolynomial.pderiv (i, j)) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.complexTraceOperator_nullSubstitution {r m n : ℕ} (hn : 2 * m ≤ n) (i j : Fin (r + 1)) (q : MvPolynomial (Fin (r + 1) × Fin m) ℂ) : complexTraceOperator i j ((nullSubstitution hn) q) = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.sourcePolarization {r m : ℕ} (i j : Fin (r + 1)) (q : MvPolynomial (Fin (r + 1) × Fin m) ℂ) : MvPolynomial (Fin (r + 1) × Fin m) ℂ

The source polarization used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.sourcePolarization i j q = ∑ a : Fin m, MvPolynomial.X (i, a) * (MvPolynomial.pderiv (j, a)) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.complexPolarization_nullSubstitution {r m n : ℕ} (hn : 2 * m ≤ n) (i j : Fin (r + 1)) (q : MvPolynomial (Fin (r + 1) × Fin m) ℂ) : complexPolarization i j ((nullSubstitution hn) q) = (nullSubstitution hn) (sourcePolarization i j q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.nullRowLinearForm_eq_even_add_I_odd {r m n : ℕ} (hn : 2 * m ≤ n) (i : Fin (r + 1)) (j : Fin m) : nullRowLinearForm hn i j = MvPolynomial.X (variableIndex i (nullEvenCoordinate hn j)) + MvPolynomial.C Complex.I * MvPolynomial.X (variableIndex i (nullOddCoordinate hn j))

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.nullRetraction {r m n : ℕ} (hn : 2 * m ≤ n) : MvPolynomial (Fin ((r + 1) * n)) ℂ →ₐ[ℂ] MvPolynomial (Fin (r + 1) × Fin m) ℂ

The polynomial retraction retaining the selected even coordinates as variables and sending the other coordinates to zero.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.nullRetraction_X_variableIndex {r m n : ℕ} (hn : 2 * m ≤ n) (i : Fin (r + 1)) (k : Fin n) : (nullRetraction hn) (MvPolynomial.X (variableIndex i k)) = ∑ a : Fin m, if k = nullEvenCoordinate hn a then MvPolynomial.X (i, a) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.nullRetraction_X_even {r m n : ℕ} (hn : 2 * m ≤ n) (i : Fin (r + 1)) (a : Fin m) : (nullRetraction hn) (MvPolynomial.X (variableIndex i (nullEvenCoordinate hn a))) = MvPolynomial.X (i, a)

theorem MetricCodes.Spherical.HigherHarmonicYoung.nullRetraction_X_odd {r m n : ℕ} (hn : 2 * m ≤ n) (i : Fin (r + 1)) (a : Fin m) : (nullRetraction hn) (MvPolynomial.X (variableIndex i (nullOddCoordinate hn a))) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.nullRetraction_nullSubstitution {r m n : ℕ} (hn : 2 * m ≤ n) (q : MvPolynomial (Fin (r + 1) × Fin m) ℂ) : (nullRetraction hn) ((nullSubstitution hn) q) = q

theorem MetricCodes.Spherical.HigherHarmonicYoung.nullSubstitution_injective {r m n : ℕ} (hn : 2 * m ≤ n) : Function.Injective ⇑(nullSubstitution hn)

def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.evenCoordinate {r n : ℕ} (h : 2 * (r + 1) ≤ n) (j : Fin (r + 1)) : Fin n

The even coordinate used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.evenCoordinate h j = ⟨2 * ↑j, ⋯⟩

def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.oddCoordinate {r n : ℕ} (h : 2 * (r + 1) ≤ n) (j : Fin (r + 1)) : Fin n

The odd coordinate used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.oddCoordinate h j = ⟨2 * ↑j + 1, ⋯⟩

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.evenCoordinate_val {r n : ℕ} (h : 2 * (r + 1) ≤ n) (j : Fin (r + 1)) : ↑(evenCoordinate h j) = 2 * ↑j

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.oddCoordinate_val {r n : ℕ} (h : 2 * (r + 1) ≤ n) (j : Fin (r + 1)) : ↑(oddCoordinate h j) = 2 * ↑j + 1

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.evenCoordinate_inj {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) : evenCoordinate h i = evenCoordinate h j ↔ i = j

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.oddCoordinate_inj {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) : oddCoordinate h i = oddCoordinate h j ↔ i = j

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.evenCoordinate_ne_oddCoordinate {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) : evenCoordinate h i ≠ oddCoordinate h j

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.variableIndex_eq_iff {r n : ℕ} (i j : Fin (r + 1)) (a b : Fin n) : variableIndex i a = variableIndex j b ↔ i = j ∧ a = b

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) : MvPolynomial (Fin ((r + 1) * n)) ℂ

The isotropic variable used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.isotropicVariable_isHomogeneous {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) : (isotropicVariable h i j).IsHomogeneous 1

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.rowDerivation {r n : ℕ} (i j : Fin (r + 1)) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The row derivation used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.rowDerivation_apply {r n : ℕ} (i j : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (rowDerivation i j) p = ∑ a : Fin n, MvPolynomial.X (variableIndex i a) * (MvPolynomial.pderiv (variableIndex j a)) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.rowDerivation_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j a b : Fin (r + 1)) : (rowDerivation i j) (isotropicVariable h a b) = if j = a then isotropicVariable h i b else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.derivation_prod_eq_zero {σ : Type u_1} {α : Type u_2} (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (s : Finset α) (f : α → MvPolynomial σ ℂ) (h : ∀ a ∈ s, D (f a) = 0) : D (∏ a ∈ s, f a) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.derivation_prod_update {σ : Type u_1} {α : Type u_2} [DecidableEq α] (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (s : Finset α) (f : α → MvPolynomial σ ℂ) (a : α) (ha : a ∈ s) (h : ∀ b ∈ s, b ≠ a → D (f b) = 0) : D (∏ b ∈ s, f b) = ∏ b ∈ s, if b = a then D (f a) else f b

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.derivation_det_singleRow {σ : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (A : Matrix ι ι (MvPolynomial σ ℂ)) (a : ι) (h : ∀ (b c : ι), b ≠ a → D (A b c) = 0) : D A.det = (A.updateRow a fun (c : ι) => D (A a c)).det

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.derivation_det_eq_zero {σ : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (A : Matrix ι ι (MvPolynomial σ ℂ)) (h : ∀ (a b : ι), D (A a b) = 0) : D A.det = 0

def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.minorIndex {r : ℕ} (k : Fin (r + 1)) (i : Fin (↑k + 1)) : Fin (r + 1)

The minor index used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.minorIndex k i = ⟨↑i, ⋯⟩

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.leadingMinor {r n : ℕ} (h : 2 * (r + 1) ≤ n) (k : Fin (r + 1)) : MvPolynomial (Fin ((r + 1) * n)) ℂ

The determinant of the leading (k + 1)-square matrix of isotropic variables.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.leadingMinor_isHomogeneous {r n : ℕ} (h : 2 * (r + 1) ≤ n) (k : Fin (r + 1)) : (leadingMinor h k).IsHomogeneous (↑k + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.rowDerivation_leadingMinor_upper {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) (hij : i < j) (k : Fin (r + 1)) : (rowDerivation i j) (leadingMinor h k) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.rowDerivation_leadingMinor_self {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i k : Fin (r + 1)) : (rowDerivation i i) (leadingMinor h k) = if i ≤ k then leadingMinor h k else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.isotropicVariable_eq_nullRowLinearForm {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) : isotropicVariable h i j = nullRowLinearForm h i j

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.sourceLeadingMinor {r : ℕ} (k : Fin (r + 1)) : MvPolynomial (Fin (r + 1) × Fin (r + 1)) ℂ

The source leading minor used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.nullSubstitution_sourceLeadingMinor {r n : ℕ} (h : 2 * (r + 1) ≤ n) (k : Fin (r + 1)) : (nullSubstitution h) (sourceLeadingMinor k) = leadingMinor h k

def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.diagonalEvaluation {r n : ℕ} : Fin ((r + 1) * n) → ℂ

The diagonal evaluation used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.diagonalEvaluation a = if ↑(finProdFinEquiv.symm a).2 = 2 * ↑(finProdFinEquiv.symm a).1 then 1 else 0

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.diagonalEvaluation_variableIndex {r n : ℕ} (i : Fin (r + 1)) (j : Fin n) : diagonalEvaluation (variableIndex i j) = if ↑j = 2 * ↑i then 1 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.eval_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) : (MvPolynomial.eval diagonalEvaluation) (isotropicVariable h i j) = if i = j then 1 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.eval_leadingMinor {r n : ℕ} (h : 2 * (r + 1) ≤ n) (k : Fin (r + 1)) : (MvPolynomial.eval diagonalEvaluation) (leadingMinor h k) = 1

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.highestWeightPolynomial {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) : MvPolynomial (Fin ((r + 1) * n)) ℂ

The highest weight polynomial used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.highestWeightPolynomial h e = ∏ k : Fin (r + 1), MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.leadingMinor h k ^ e k

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.sourceHighestWeightPolynomial {r : ℕ} (e : Fin (r + 1) → ℕ) : MvPolynomial (Fin (r + 1) × Fin (r + 1)) ℂ

The source highest weight polynomial used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.nullSubstitution_sourceHighestWeightPolynomial {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) : (nullSubstitution h) (sourceHighestWeightPolynomial e) = highestWeightPolynomial h e

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.complexTraceOperator_highestWeightPolynomial {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) : complexTraceOperator i j (highestWeightPolynomial h e) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.rowDerivation_highestWeightPolynomial_upper {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (hij : i < j) : (rowDerivation i j) (highestWeightPolynomial h e) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.highestWeightPolynomial_isHomogeneous_minorDegrees {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) : (highestWeightPolynomial h e).IsHomogeneous (∑ k : Fin (r + 1), (↑k + 1) * e k)

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.derivation_prod_eigen {σ : Type u_1} {α : Type u_2} (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (s : Finset α) (f : α → MvPolynomial σ ℂ) (c : α → ℕ) (h : ∀ a ∈ s, D (f a) = ↑(c a) • f a) : D (∏ a ∈ s, f a) = (∑ a ∈ s, ↑(c a)) • ∏ a ∈ s, f a

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.eval_highestWeightPolynomial {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) : (MvPolynomial.eval diagonalEvaluation) (highestWeightPolynomial h e) = 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.highestWeightPolynomial_ne_zero {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) : highestWeightPolynomial h e ≠ 0

def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.determinantWeight {r : ℕ} (e : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : ℕ

The determinant weight used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.determinantWeight e i = ∑ k : Fin (r + 1), if i ≤ k then e k else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.sum_determinantWeight {r : ℕ} (e : Fin (r + 1) → ℕ) : ∑ i : Fin (r + 1), determinantWeight e i = ∑ k : Fin (r + 1), (↑k + 1) * e k

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.highestWeightPolynomial_isHomogeneous {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) : (highestWeightPolynomial h e).IsHomogeneous (∑ i : Fin (r + 1), determinantWeight e i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.rowDerivation_highestWeightPolynomial_self {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : (rowDerivation i i) (highestWeightPolynomial h e) = ↑(determinantWeight e i) • highestWeightPolynomial h e

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.complexPolarization_eq_rowDerivation {r n : ℕ} (i j : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : complexPolarization i j p = (rowDerivation i j) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.complexRowEuler_eq_rowDerivation {r n : ℕ} (i : Fin (r + 1)) (p : MvPolynomial (Fin ((r + 1) * n)) ℂ) : complexRowEuler i p = (rowDerivation i i) p

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

The signature exponent used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.signatureExponent lam i = Fin.lastCases (lam (Fin.last r)) (fun (i : Fin r) => lam i.castSucc - lam i.succ) i

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.signatureExponent_last {r : ℕ} (lam : Fin (r + 1) → ℕ) : signatureExponent lam (Fin.last r) = lam (Fin.last r)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.signatureExponent_castSucc {r : ℕ} (lam : Fin (r + 1) → ℕ) (i : Fin r) : signatureExponent lam i.castSucc = lam i.castSucc - lam i.succ

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.determinantWeight_last {r : ℕ} (e : Fin (r + 1) → ℕ) : determinantWeight e (Fin.last r) = e (Fin.last r)

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.determinantWeight_castSucc {r : ℕ} (e : Fin (r + 1) → ℕ) (i : Fin r) : determinantWeight e i.castSucc = e i.castSucc + determinantWeight e i.succ

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.determinantWeight_signatureExponent {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : determinantWeight (signatureExponent lam) = lam

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.dominantHighestWeightWitness {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : ComplexHighestWeightWitness lam

The dominant highest weight witness used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.exists_nonzero_harmonicYoung_of_antitone {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : ∃ (p : ↥(HarmonicYoungSpace lam)), p ≠ 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.finrank_harmonicYoung_pos_of_antitone {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : 0 < Module.finrank ℝ ↥(HarmonicYoungSpace lam)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.conjugateIsotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (i j : Fin (r + 1)) : MvPolynomial (Fin ((r + 1) * n)) ℂ

The conjugate isotropic variable used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.pderiv_even_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p i j : Fin (r + 1)) : (MvPolynomial.pderiv (variableIndex a (evenCoordinate h p))) (isotropicVariable h i j) = if a = i ∧ p = j then 1 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.pderiv_odd_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p i j : Fin (r + 1)) : (MvPolynomial.pderiv (variableIndex a (oddCoordinate h p))) (isotropicVariable h i j) = if a = i ∧ p = j then MvPolynomial.C Complex.I else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

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

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot_apply {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) : (ambientPositiveRoot h p q) f = ∑ a : Fin (r + 1), (isotropicVariable h a p * ((MvPolynomial.pderiv (variableIndex a (evenCoordinate h q))) f - MvPolynomial.C Complex.I * (MvPolynomial.pderiv (variableIndex a (oddCoordinate h q))) f) - conjugateIsotropicVariable h a q * ((MvPolynomial.pderiv (variableIndex a (evenCoordinate h p))) f + MvPolynomial.C Complex.I * (MvPolynomial.pderiv (variableIndex a (oddCoordinate h p))) f))

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q i j : Fin (r + 1)) : (ambientPositiveRoot h p q) (isotropicVariable h i j) = if q = j then 2 • isotropicVariable h i p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.derivation_det_singleColumn {σ : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (D : Derivation ℂ (MvPolynomial σ ℂ) (MvPolynomial σ ℂ)) (A : Matrix ι ι (MvPolynomial σ ℂ)) (a : ι) (h : ∀ (b c : ι), c ≠ a → D (A b c) = 0) : D A.det = (A.updateCol a fun (b : ι) => D (A b a)).det

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot_leadingMinor {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) (hpq : p < q) (k : Fin (r + 1)) : (ambientPositiveRoot h p q) (leadingMinor h k) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot_highestWeightPolynomial {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) (p q : Fin (r + 1)) (hpq : p < q) : (ambientPositiveRoot h p q) (highestWeightPolynomial h e) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot_dominantHighestWeightWitness {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (p q : Fin (r + 1)) (hpq : p < q) : (ambientPositiveRoot h p q) (dominantHighestWeightWitness h lam hdom).polynomial = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p : Fin (r + 1)) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The antiholomorphic derivative used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.antiholomorphicDerivative_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a p i j : Fin (r + 1)) : (antiholomorphicDerivative h a p) (isotropicVariable h i j) = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q : Fin (r + 1)) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The ambient sum positive root used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q i j : Fin (r + 1)) : (ambientSumPositiveRoot h p q) (isotropicVariable h i j) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot_leadingMinor {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p q k : Fin (r + 1)) : (ambientSumPositiveRoot h p q) (leadingMinor h k) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot_highestWeightPolynomial {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) (p q : Fin (r + 1)) : (ambientSumPositiveRoot h p q) (highestWeightPolynomial h e) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot_dominantHighestWeightWitness {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (p q : Fin (r + 1)) : (ambientSumPositiveRoot h p q) (dominantHighestWeightWitness h lam hdom).polynomial = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.pderiv_outside_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (a i j : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (MvPolynomial.pderiv (variableIndex a t)) (isotropicVariable h i j) = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) (t : Fin n) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The ambient short positive root used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p i j : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (ambientShortPositiveRoot h p t) (isotropicVariable h i j) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot_leadingMinor {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p k : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (ambientShortPositiveRoot h p t) (leadingMinor h k) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot_highestWeightPolynomial {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) (p : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (ambientShortPositiveRoot h p t) (highestWeightPolynomial h e) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot_dominantHighestWeightWitness {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (p : Fin (r + 1)) (t : Fin n) (ht : 2 * (r + 1) ≤ ↑t) : (ambientShortPositiveRoot h p t) (dominantHighestWeightWitness h lam hdom).polynomial = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientCartan {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p : Fin (r + 1)) : Derivation ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ) (MvPolynomial (Fin ((r + 1) * n)) ℂ)

The ambient cartan used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientCartan h p = MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot h p p

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientCartan_isotropicVariable {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p i j : Fin (r + 1)) : (ambientCartan h p) (isotropicVariable h i j) = if p = j then 2 • isotropicVariable h i p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientCartan_leadingMinor {r n : ℕ} (h : 2 * (r + 1) ≤ n) (p k : Fin (r + 1)) : (ambientCartan h p) (leadingMinor h k) = if p ≤ k then 2 • leadingMinor h k else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientCartan_highestWeightPolynomial {r n : ℕ} (h : 2 * (r + 1) ≤ n) (e : Fin (r + 1) → ℕ) (p : Fin (r + 1)) : (ambientCartan h p) (highestWeightPolynomial h e) = ↑(2 * determinantWeight e p) • highestWeightPolynomial h e

theorem MetricCodes.Spherical.HigherHarmonicYoung.DeterminantVectors.ambientCartan_dominantHighestWeightWitness {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (p : Fin (r + 1)) : (ambientCartan h p) (dominantHighestWeightWitness h lam hdom).polynomial = ↑(2 * lam p) • (dominantHighestWeightWitness h lam hdom).polynomial

def MetricCodes.Spherical.HigherChannel.FiniteInterlacing {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) : Prop

The finite interlacing used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherChannel.FiniteInterlacing n lam mu = (2 * r + 4 ≤ n ∧ ∀ (m : Fin r), mu m ≤ lam m.castSucc ∧ lam m.succ ≤ mu m)

noncomputable def MetricCodes.Spherical.HigherChannel.ambientShift {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (ℓ : Fin (r + 1)) : ℝ

The ambient shift used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherChannel.ambientShift n lam ℓ = ↑(lam ℓ) + ↑n / 2 - (↑↑ℓ + 1)

noncomputable def MetricCodes.Spherical.HigherChannel.stabilizerShift {r : ℕ} (n : ℕ) (mu : Fin r → ℕ) (m : Fin r) : ℝ

The stabilizer shift used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherChannel.stabilizerShift n mu m = ↑(mu m) + (↑n - 1) / 2 - (↑↑m + 1)

noncomputable def MetricCodes.Spherical.HigherChannel.wallShift (n r : ℕ) : ℝ

The wall shift used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherChannel.wallShift n r = ↑n / 2 - ↑r - 1

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.wallShift_pos {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) : 0 < wallShift n r

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.one_le_wallShift {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) : 1 ≤ wallShift n r

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.ambientShift_succ_add_one_le {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (m : Fin r) : ambientShift n lam m.succ + 1 ≤ ambientShift n lam m.castSucc

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.ambientShift_strictAnti {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) : StrictAnti (ambientShift n lam)

theorem MetricCodes.Spherical.HigherChannel.ambientShift_last {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ambientShift n lam (Fin.last r) = ↑(lam (Fin.last r)) + wallShift n r

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.ambientShift_pos {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (ℓ : Fin (r + 1)) : 0 < ambientShift n lam ℓ

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.wallShift_le_ambientShift {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (ℓ : Fin (r + 1)) : wallShift n r ≤ ambientShift n lam ℓ

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.ambientShift_castSucc_ge {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (m : Fin r) : stabilizerShift n mu m + 1 / 2 ≤ ambientShift n lam m.castSucc

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.stabilizerShift_ge_succ {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (m : Fin r) : ambientShift n lam m.succ + 1 / 2 ≤ stabilizerShift n mu m

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.stabilizerShift_pos {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (m : Fin r) : 0 < stabilizerShift n mu m

def MetricCodes.Spherical.HigherChannel.activeDenominator {r : ℕ} (L : Fin (r + 1) → ℝ) (ℓ : Fin (r + 1)) : ℝ

The active denominator used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherChannel.activeDenominator L ℓ = 2 * L ℓ * ∏ q : Fin r, (L ℓ ^ 2 - L (ℓ.succAbove q) ^ 2)

noncomputable def MetricCodes.Spherical.HigherChannel.plusProbability {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (ℓ : Fin (r + 1)) : ℝ

The plus probability used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherChannel.minusProbability {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (ℓ : Fin (r + 1)) : ℝ

The minus probability used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.activeDenominator_ne_zero {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (ℓ : Fin (r + 1)) : activeDenominator (ambientShift n lam) ℓ ≠ 0

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.plusFactor_nonneg {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (ℓ : Fin (r + 1)) (m : Fin r) : 0 ≤ ((ambientShift n lam ℓ + 1 / 2) ^ 2 - stabilizerShift n mu m ^ 2) / (ambientShift n lam ℓ ^ 2 - ambientShift n lam (ℓ.succAbove m) ^ 2)

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.minusFactor_nonneg {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (ℓ : Fin (r + 1)) (m : Fin r) : 0 ≤ ((ambientShift n lam ℓ - 1 / 2) ^ 2 - stabilizerShift n mu m ^ 2) / (ambientShift n lam ℓ ^ 2 - ambientShift n lam (ℓ.succAbove m) ^ 2)

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.plusProbability_nonneg {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (ℓ : Fin (r + 1)) : 0 ≤ plusProbability n lam mu ℓ

theorem MetricCodes.Spherical.HigherChannel.FiniteInterlacing.minusProbability_nonneg {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (ℓ : Fin (r + 1)) : 0 ≤ minusProbability n lam mu ℓ

def MetricCodes.Spherical.HigherChannel.signedNode {r : ℕ} (L : Fin (r + 1) → ℝ) (z : Fin (r + 1) × Bool) : ℝ

The signed node used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherChannel.signedNode L z = if z.2 = true then L z.1 else -L z.1

theorem MetricCodes.Spherical.HigherChannel.signedNode_injective {r : ℕ} {L : Fin (r + 1) → ℝ} (hpos : ∀ (ℓ : Fin (r + 1)), 0 < L ℓ) (hinj : Function.Injective L) : Function.Injective (signedNode L)

noncomputable def MetricCodes.Spherical.HigherChannel.channelNumeratorPolynomial {r : ℕ} (rho : ℝ) (M : Fin r → ℝ) : Polynomial ℝ

The channel numerator polynomial used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherChannel.channelNumeratorPolynomial_eval_pos {r : ℕ} (rho : ℝ) (M : Fin r → ℝ) (t : ℝ) : Polynomial.eval t (channelNumeratorPolynomial rho M) = (t + rho) * ∏ m : Fin r, ((t + 1 / 2) ^ 2 - M m ^ 2)

theorem MetricCodes.Spherical.HigherChannel.signedNode_denominator_pos {r : ℕ} (L : Fin (r + 1) → ℝ) (ℓ : Fin (r + 1)) : ∏ z ∈ Finset.univ.erase (ℓ, true), (L ℓ - signedNode L z) = 2 * L ℓ * ∏ j ∈ Finset.univ.erase ℓ, (L ℓ ^ 2 - L j ^ 2)

theorem MetricCodes.Spherical.HigherChannel.signedNode_denominator_neg {r : ℕ} (L : Fin (r + 1) → ℝ) (ℓ : Fin (r + 1)) : ∏ z ∈ Finset.univ.erase (ℓ, false), (-L ℓ - signedNode L z) = -(2 * L ℓ * ∏ j ∈ Finset.univ.erase ℓ, (L ℓ ^ 2 - L j ^ 2))

theorem MetricCodes.Spherical.HigherChannel.activeQuadraticDenominator_eq_prod_erase {r : ℕ} (L : Fin (r + 1) → ℝ) (ℓ : Fin (r + 1)) : ∏ m : Fin r, (L ℓ ^ 2 - L (ℓ.succAbove m) ^ 2) = ∏ j ∈ Finset.univ.erase ℓ, (L ℓ ^ 2 - L j ^ 2)

theorem MetricCodes.Spherical.HigherChannel.signedNode_denominator_pos_eq_active {r : ℕ} (L : Fin (r + 1) → ℝ) (ℓ : Fin (r + 1)) : ∏ z ∈ Finset.univ.erase (ℓ, true), (L ℓ - signedNode L z) = activeDenominator L ℓ

theorem MetricCodes.Spherical.HigherChannel.signedNode_denominator_neg_eq_active {r : ℕ} (L : Fin (r + 1) → ℝ) (ℓ : Fin (r + 1)) : ∏ z ∈ Finset.univ.erase (ℓ, false), (-L ℓ - signedNode L z) = -activeDenominator L ℓ

def MetricCodes.Spherical.ThreeRowYoungBranching.transverseVariableIndex {r n : ℕ} (a : Fin ((r + 1) * n)) : Fin ((r + 2) * (n + 1))

Embed a row-variable index into the larger array with one additional row and one additional coordinate.

Equations

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

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.transverseVariableIndex_variableIndex {r n : ℕ} (i : Fin (r + 1)) (j : Fin n) : transverseVariableIndex (HigherHarmonicYoung.variableIndex i j) = HigherHarmonicYoung.variableIndex i.castSucc j.castSucc

theorem MetricCodes.Spherical.ThreeRowYoungBranching.transverseVariableIndex_injective {r n : ℕ} : Function.Injective transverseVariableIndex

noncomputable def MetricCodes.Spherical.ThreeRowYoungBranching.transversePolynomial {r : ℕ} (n : ℕ) : HigherHarmonicYoung.PolynomialSpace r n →ₐ[ℝ] HigherHarmonicYoung.PolynomialSpace (r + 1) (n + 1)

The transverse polynomial used in the spherical-code argument.

Equations

• MetricCodes.Spherical.ThreeRowYoungBranching.transversePolynomial n = MvPolynomial.rename MetricCodes.Spherical.ThreeRowYoungBranching.transverseVariableIndex

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.transversePolynomial_X {r n : ℕ} (i : Fin (r + 1)) (j : Fin n) : (transversePolynomial n) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i j)) = MvPolynomial.X (HigherHarmonicYoung.variableIndex i.castSucc j.castSucc)

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.pderiv_transversePolynomial_castSucc {r n : ℕ} (i : Fin (r + 1)) (j : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r n) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i.castSucc j.castSucc)) ((transversePolynomial n) p) = (transversePolynomial n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i j)) p)

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.pderiv_transversePolynomial_lastCoordinate {r n : ℕ} (i : Fin (r + 2)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i (Fin.last n))) ((transversePolynomial n) p) = 0

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.pderiv_transversePolynomial_lastRow {r n : ℕ} (j : Fin (n + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex (Fin.last (r + 1)) j)) ((transversePolynomial n) p) = 0

def MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroWeight {r : ℕ} (mu : Fin (r + 1) → ℕ) : Fin (r + 2) → ℕ

The append zero weight used in the spherical-code argument.

Equations

• MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroWeight mu i = Fin.lastCases 0 mu i

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroWeight_castSucc {r : ℕ} (mu : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : appendZeroWeight mu i.castSucc = mu i

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroWeight_last {r : ℕ} (mu : Fin (r + 1) → ℕ) : appendZeroWeight mu (Fin.last (r + 1)) = 0

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.sum_appendZeroWeight {r : ℕ} (mu : Fin (r + 1) → ℕ) : ∑ i : Fin (r + 2), appendZeroWeight mu i = ∑ i : Fin (r + 1), mu i

theorem MetricCodes.Spherical.ThreeRowYoungBranching.rowEuler_transversePolynomial_castSucc {r n : ℕ} (i : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.rowEuler (r + 1) (n + 1) i.castSucc) ((transversePolynomial n) p) = (transversePolynomial n) ((HigherHarmonicYoung.rowEuler r n i) p)

theorem MetricCodes.Spherical.ThreeRowYoungBranching.traceOperator_transversePolynomial_castSucc {r n : ℕ} (i j : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.traceOperator (r + 1) (n + 1) i.castSucc j.castSucc) ((transversePolynomial n) p) = (transversePolynomial n) ((HigherHarmonicYoung.traceOperator r n i j) p)

theorem MetricCodes.Spherical.ThreeRowYoungBranching.traceOperator_transversePolynomial_last_right {r n : ℕ} (i : Fin (r + 2)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.traceOperator (r + 1) (n + 1) i (Fin.last (r + 1))) ((transversePolynomial n) p) = 0

theorem MetricCodes.Spherical.ThreeRowYoungBranching.traceOperator_transversePolynomial_last_left {r n : ℕ} (i : Fin (r + 2)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.traceOperator (r + 1) (n + 1) (Fin.last (r + 1)) i) ((transversePolynomial n) p) = 0

theorem MetricCodes.Spherical.ThreeRowYoungBranching.polarization_transversePolynomial_castSucc {r n : ℕ} (i j : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.polarization (r + 1) (n + 1) i.castSucc j.castSucc) ((transversePolynomial n) p) = (transversePolynomial n) ((HigherHarmonicYoung.polarization r n i j) p)

theorem MetricCodes.Spherical.ThreeRowYoungBranching.transversePolynomial_mem_harmonicYoung {r n : ℕ} (mu : Fin (r + 1) → ℕ) (p : HigherHarmonicYoung.PolynomialSpace r n) (hp : p ∈ HigherHarmonicYoung.harmonicYoungSubmodule mu) : (transversePolynomial n) p ∈ HigherHarmonicYoung.harmonicYoungSubmodule (appendZeroWeight mu)

noncomputable def MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroYoungEmbedding {r n : ℕ} (mu : Fin (r + 1) → ℕ) : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace (appendZeroWeight mu))

Embed harmonic Young space by appending a zero weight and adding a transverse coordinate.

Equations

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

noncomputable def MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroYoungIsometry {r n : ℕ} (mu : Fin (r + 1) → ℕ) : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗᵢ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace (appendZeroWeight mu))

The transverse embedding with an appended zero weight, bundled as a linear isometry.

Equations

• MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroYoungIsometry mu = (MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroYoungEmbedding mu).isometryOfInner ⋯

def MetricCodes.Spherical.ThreeRowYoungBranching.zeroRowVariableIndex {r n : ℕ} (a : Fin ((r + 1) * n)) : Fin ((r + 2) * n)

Embed a row-variable index into the larger array with one additional row and the same coordinate dimension.

Equations

• MetricCodes.Spherical.ThreeRowYoungBranching.zeroRowVariableIndex a = MetricCodes.Spherical.HigherHarmonicYoung.variableIndex (finProdFinEquiv.symm a).1.castSucc (finProdFinEquiv.symm a).2

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.zeroRowVariableIndex_variableIndex {r n : ℕ} (i : Fin (r + 1)) (j : Fin n) : zeroRowVariableIndex (HigherHarmonicYoung.variableIndex i j) = HigherHarmonicYoung.variableIndex i.castSucc j

theorem MetricCodes.Spherical.ThreeRowYoungBranching.zeroRowVariableIndex_injective {r n : ℕ} : Function.Injective zeroRowVariableIndex

noncomputable def MetricCodes.Spherical.ThreeRowYoungBranching.zeroRowPolynomial {r : ℕ} (n : ℕ) : HigherHarmonicYoung.PolynomialSpace r n →ₐ[ℝ] HigherHarmonicYoung.PolynomialSpace (r + 1) n

The zero row polynomial used in the spherical-code argument.

Equations

• MetricCodes.Spherical.ThreeRowYoungBranching.zeroRowPolynomial n = MvPolynomial.rename MetricCodes.Spherical.ThreeRowYoungBranching.zeroRowVariableIndex

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.zeroRowPolynomial_X {r n : ℕ} (i : Fin (r + 1)) (j : Fin n) : (zeroRowPolynomial n) (MvPolynomial.X (HigherHarmonicYoung.variableIndex i j)) = MvPolynomial.X (HigherHarmonicYoung.variableIndex i.castSucc j)

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.pderiv_zeroRowPolynomial_castSucc {r n : ℕ} (i : Fin (r + 1)) (j : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r n) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i.castSucc j)) ((zeroRowPolynomial n) p) = (zeroRowPolynomial n) ((MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex i j)) p)

@[simp]

theorem MetricCodes.Spherical.ThreeRowYoungBranching.pderiv_zeroRowPolynomial_lastRow {r n : ℕ} (j : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r n) : (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex (Fin.last (r + 1)) j)) ((zeroRowPolynomial n) p) = 0

theorem MetricCodes.Spherical.ThreeRowYoungBranching.rowEuler_zeroRowPolynomial_castSucc {r n : ℕ} (i : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.rowEuler (r + 1) n i.castSucc) ((zeroRowPolynomial n) p) = (zeroRowPolynomial n) ((HigherHarmonicYoung.rowEuler r n i) p)

theorem MetricCodes.Spherical.ThreeRowYoungBranching.traceOperator_zeroRowPolynomial_castSucc {r n : ℕ} (i j : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.traceOperator (r + 1) n i.castSucc j.castSucc) ((zeroRowPolynomial n) p) = (zeroRowPolynomial n) ((HigherHarmonicYoung.traceOperator r n i j) p)

theorem MetricCodes.Spherical.ThreeRowYoungBranching.traceOperator_zeroRowPolynomial_last_right {r n : ℕ} (i : Fin (r + 2)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.traceOperator (r + 1) n i (Fin.last (r + 1))) ((zeroRowPolynomial n) p) = 0

theorem MetricCodes.Spherical.ThreeRowYoungBranching.traceOperator_zeroRowPolynomial_last_left {r n : ℕ} (i : Fin (r + 2)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.traceOperator (r + 1) n (Fin.last (r + 1)) i) ((zeroRowPolynomial n) p) = 0

theorem MetricCodes.Spherical.ThreeRowYoungBranching.polarization_zeroRowPolynomial_castSucc {r n : ℕ} (i j : Fin (r + 1)) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.polarization (r + 1) n i.castSucc j.castSucc) ((zeroRowPolynomial n) p) = (zeroRowPolynomial n) ((HigherHarmonicYoung.polarization r n i j) p)

theorem MetricCodes.Spherical.ThreeRowYoungBranching.zeroRowPolynomial_mem_harmonicYoung {r n : ℕ} (mu : Fin (r + 1) → ℕ) (p : HigherHarmonicYoung.PolynomialSpace r n) (hp : p ∈ HigherHarmonicYoung.harmonicYoungSubmodule mu) : (zeroRowPolynomial n) p ∈ HigherHarmonicYoung.harmonicYoungSubmodule (appendZeroWeight mu)

theorem MetricCodes.Spherical.ThreeRowYoungBranching.zeroRowPolynomial_mem_harmonicYoung_iff {r n : ℕ} (mu : Fin (r + 1) → ℕ) (p : HigherHarmonicYoung.PolynomialSpace r n) : (zeroRowPolynomial n) p ∈ HigherHarmonicYoung.harmonicYoungSubmodule (appendZeroWeight mu) ↔ p ∈ HigherHarmonicYoung.harmonicYoungSubmodule mu

noncomputable def MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroRowEmbedding {r n : ℕ} (mu : Fin (r + 1) → ℕ) : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace (appendZeroWeight mu))

Embed harmonic Young space by appending a zero row weight while retaining the coordinate dimension.

Equations

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

theorem MetricCodes.Spherical.ThreeRowYoungBranching.vars_appendZeroYoung_subset_range {r n : ℕ} (mu : Fin (r + 1) → ℕ) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace (appendZeroWeight mu))) : ↑(MvPolynomial.vars ↑p) ⊆ Set.range zeroRowVariableIndex

theorem MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroRowEmbedding_surjective {r n : ℕ} (mu : Fin (r + 1) → ℕ) : Function.Surjective ⇑(appendZeroRowEmbedding mu)

noncomputable def MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroRowIsometry {r n : ℕ} (mu : Fin (r + 1) → ℕ) : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗᵢ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace (appendZeroWeight mu))

The embedding that appends a zero row weight, bundled as a linear isometry.

Equations

• MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroRowIsometry mu = (MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroRowEmbedding mu).isometryOfInner ⋯

noncomputable def MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroRowIsometryEquiv {r n : ℕ} (mu : Fin (r + 1) → ℕ) : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) ≃ₗᵢ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace (appendZeroWeight mu))

The append zero row isometry equiv used in the spherical-code argument.

Equations

• MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroRowIsometryEquiv mu = LinearIsometryEquiv.ofSurjective (MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroRowIsometry mu) ⋯

theorem MetricCodes.Spherical.ThreeRowYoungBranching.finrank_harmonicYoung_appendZero_eq {r n : ℕ} (mu : Fin (r + 1) → ℕ) : Module.finrank ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace (appendZeroWeight mu)) = Module.finrank ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankBranching.appendZeroWeight_eq_snoc {r : ℕ} (mu : Fin (r + 1) → ℕ) : ThreeRowYoungBranching.appendZeroWeight mu = Fin.snoc mu 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankBranching.fullBranchOfInterlaces_signature_eq_appendZeroWeight {r : ℕ} {lam : Fin (r + 2) → ℕ} (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) : BranchingDimension.fullBranchSignature (BranchingDimension.fullBranchOfInterlaces mu h) = ThreeRowYoungBranching.appendZeroWeight mu

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankBranching.terminalZeroSelectedBranchIsometry {r n : ℕ} (mu : Fin (r + 1) → ℕ) : ↥(HarmonicYoungSpace mu) →ₗᵢ[ℝ] ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight mu))

The terminal zero selected branch isometry used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankBranching.terminalZeroSelectedBranchIsometry mu = MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroYoungIsometry mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankBranching.interlaces_antitone_stabilizer {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) : Antitone mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankBranching.finrank_selectedStabilizer_pos {r n : ℕ} {lam : Fin (r + 2) → ℕ} (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) ≤ n - 1) : 0 < Module.finrank ℝ ↥(HarmonicYoungSpace mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateLower_axis_add {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (v w : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (projectedCoordinateLower mu lam hdeg row (v + w)) p = (projectedCoordinateLower mu lam hdeg row v) p + (projectedCoordinateLower mu lam hdeg row w) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateLower_axis_smul {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (c : ℝ) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (projectedCoordinateLower mu lam hdeg row (c • v)) p = c • (projectedCoordinateLower mu lam hdeg row v) p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateLowerAxis {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (p : ↥(HarmonicYoungSpace lam)) : SpherePacking.Euclidean n →ₗ[ℝ] ↥(HarmonicYoungSpace mu)

The projected coordinate lower axis used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateRaise_axis_add {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (v w : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (projectedCoordinateRaise mu lam hdeg row (v + w)) p = (projectedCoordinateRaise mu lam hdeg row v) p + (projectedCoordinateRaise mu lam hdeg row w) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateRaise_axis_smul {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (c : ℝ) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (projectedCoordinateRaise mu lam hdeg row (c • v)) p = c • (projectedCoordinateRaise mu lam hdeg row v) p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.projectedCoordinateRaiseAxis {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (p : ↥(HarmonicYoungSpace lam)) : SpherePacking.Euclidean n →ₗ[ℝ] ↥(HarmonicYoungSpace mu)

The projected coordinate raise axis used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngClebschRaise {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)

The young clebsch raise used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschRaise_apply {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (p : ↥(HarmonicYoungSpace lam)) : (youngClebschRaise mu lam hdeg row) p = ∑ j : Fin n, (EuclideanSpace.basisFun (Fin n) ℝ) j ⊗ₜ[ℝ] (projectedCoordinateRaise mu lam hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j)) p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngClebschLower {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)

The young clebsch lower used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschLower_apply {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (p : ↥(HarmonicYoungSpace lam)) : (youngClebschLower mu lam hdeg row) p = ∑ j : Fin n, (EuclideanSpace.basisFun (Fin n) ℝ) j ⊗ₜ[ℝ] (projectedCoordinateLower mu lam hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j)) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschLower_inner {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (p q : ↥(HarmonicYoungSpace lam)) : inner ℝ ((youngClebschLower mu lam hdeg row) p) ((youngClebschLower mu lam hdeg row) q) = ∑ j : Fin n, inner ℝ ((projectedCoordinateLower mu lam hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j)) p) ((projectedCoordinateLower mu lam hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j)) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschRaise_inner_basis_tmul {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (j : Fin n) (p : ↥(HarmonicYoungSpace lam)) (q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((youngClebschRaise mu lam hdeg row) p) ((EuclideanSpace.basisFun (Fin n) ℝ) j ⊗ₜ[ℝ] q) = inner ℝ p ((projectedCoordinateLower lam mu hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j)) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschRaise_adjoint_basis_tmul {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (j : Fin n) (q : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (youngClebschRaise mu lam hdeg row)) ((EuclideanSpace.basisFun (Fin n) ℝ) j ⊗ₜ[ℝ] q) = (projectedCoordinateLower lam mu hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j)) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschRaise_adjoint_tmul {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (v : SpherePacking.Euclidean n) (q : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (youngClebschRaise mu lam hdeg row)) (v ⊗ₜ[ℝ] q) = (projectedCoordinateLower lam mu hdeg row v) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschLower_adjoint_basis_tmul {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (j : Fin n) (q : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (youngClebschLower mu lam hdeg row)) ((EuclideanSpace.basisFun (Fin n) ℝ) j ⊗ₜ[ℝ] q) = (projectedCoordinateRaise lam mu hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j)) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschRaise_adjoint_comp_self {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) : LinearMap.adjoint (youngClebschRaise mu lam hdeg row) ∘ₗ youngClebschRaise mu lam hdeg row = ∑ j : Fin n, projectedCoordinateLower lam mu hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j) ∘ₗ projectedCoordinateRaise mu lam hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschLower_adjoint_comp_self {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) : LinearMap.adjoint (youngClebschLower mu lam hdeg row) ∘ₗ youngClebschLower mu lam hdeg row = ∑ j : Fin n, projectedCoordinateRaise lam mu hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j) ∘ₗ projectedCoordinateLower mu lam hdeg row ((EuclideanSpace.basisFun (Fin n) ℝ) j)

theorem MetricCodes.Spherical.HigherHarmonicYoung.FullRankClebsch.oppositePolarization_commutator {r n : ℕ} (i j : Fin (r + 1)) (p : PolynomialSpace r n) : (polarization r n i j) ((polarization r n j i) p) + (rowEuler r n j) p = (polarization r n j i) ((polarization r n i j) p) + (rowEuler r n i) p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.jointHarmonicWeightSubmodule {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Submodule ℝ ↥(youngMultihomogeneousSubmodule n lam)

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

Equations

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

@[reducible, inline]

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

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

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.JointHarmonicWeightSpace n lam = ↥(MetricCodes.Spherical.HigherHarmonicYoung.jointHarmonicWeightSubmodule n lam)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_jointHarmonicWeightSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(youngMultihomogeneousSubmodule n lam)) : p ∈ jointHarmonicWeightSubmodule n lam ↔ ↑p ∈ traceFreeSubmodule r n

instance MetricCodes.Spherical.HigherHarmonicYoung.jointHarmonicWeightSpace_finiteDimensional {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : FiniteDimensional ℝ (JointHarmonicWeightSpace n lam)

def MetricCodes.Spherical.HigherHarmonicYoung.jointHarmonicWeightHomogeneousEmbedding {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : JointHarmonicWeightSpace n lam →ₗ[ℝ] ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (∑ i : Fin (r + 1), lam i))

Regard a joint harmonic weight polynomial as homogeneous of degree equal to the sum of its row weights.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.jointHarmonicWeightHomogeneousEmbedding_injective {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Function.Injective ⇑(jointHarmonicWeightHomogeneousEmbedding n lam)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.jointHarmonicWeightCoefficientEmbedding {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : JointHarmonicWeightSpace n lam →ₗ[ℝ] SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) (∑ i : Fin (r + 1), lam i)

The Fischer coefficient embedding of the joint harmonic weight space.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.jointHarmonicWeightCoefficientEmbedding_injective {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Function.Injective ⇑(jointHarmonicWeightCoefficientEmbedding n lam)

@[implicit_reducible]

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.jointHarmonicWeightFischerCore {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : InnerProductSpace.Core ℝ (JointHarmonicWeightSpace n lam)

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

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.jointHarmonicWeightFischerCore_inner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : JointHarmonicWeightSpace n lam) : inner ℝ p q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) ↑↑p ↑↑q

theorem MetricCodes.Spherical.HigherHarmonicYoung.traceOperator_pderiv_comm {r n : ℕ} (a b row : Fin (r + 1)) (j : Fin n) (p : PolynomialSpace r n) : (traceOperator r n a b) ((MvPolynomial.pderiv (variableIndex row j)) p) = (MvPolynomial.pderiv (variableIndex row j)) ((traceOperator r n a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_pderiv_of_ne {r n : ℕ} (a b row : Fin (r + 1)) (j : Fin n) (hne : a ≠ row) (p : PolynomialSpace r n) : (polarization r n a b) ((MvPolynomial.pderiv (variableIndex row j)) p) = (MvPolynomial.pderiv (variableIndex row j)) ((polarization r n a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuler_pderiv_of_ne {r n : ℕ} (a row : Fin (r + 1)) (j : Fin n) (hne : a ≠ row) (p : PolynomialSpace r n) : (rowEuler r n a) ((MvPolynomial.pderiv (variableIndex row j)) p) = (MvPolynomial.pderiv (variableIndex row j)) ((rowEuler r n a) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuler_pderiv_self {r n : ℕ} (row : Fin (r + 1)) (j : Fin n) (p : PolynomialSpace r n) : (rowEuler r n row) ((MvPolynomial.pderiv (variableIndex row j)) p) = (MvPolynomial.pderiv (variableIndex row j)) ((rowEuler r n row) p) - (MvPolynomial.pderiv (variableIndex row j)) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowDerivative_fischer_inner_sum {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (p q : ↥(HarmonicYoungSpace lam)) : ∑ j : Fin n, SpherePacking.Fischer.polynomialInner ((r + 1) * n) ((MvPolynomial.pderiv (variableIndex row j)) ↑p) ((MvPolynomial.pderiv (variableIndex row j)) ↑q) = ↑(lam row) * inner ℝ p q

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngClebschRaiseLower_trace {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) : (LinearMap.trace ℝ ↥(HarmonicYoungSpace lam)) (LinearMap.adjoint (youngClebschRaise mu lam hdeg row) ∘ₗ youngClebschRaise mu lam hdeg row) = (LinearMap.trace ℝ ↥(HarmonicYoungSpace mu)) (LinearMap.adjoint (youngClebschLower lam mu hdeg row) ∘ₗ youngClebschLower lam mu hdeg row)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.normalizedYoungClebschRaise {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (c : ℝ) (hc : 0 < c) (hgram : ∀ (p q : ↥(HarmonicYoungSpace lam)), inner ℝ ((youngClebschRaise mu lam hdeg row) p) ((youngClebschRaise mu lam hdeg row) q) = c * inner ℝ p q) : ↥(HarmonicYoungSpace lam) →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)

The normalized young clebsch raise used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.normalizedYoungClebschLower {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (c : ℝ) (hc : 0 < c) (hgram : ∀ (p q : ↥(HarmonicYoungSpace lam)), inner ℝ ((youngClebschLower mu lam hdeg row) p) ((youngClebschLower mu lam hdeg row) q) = c * inner ℝ p q) : ↥(HarmonicYoungSpace lam) →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace mu)

The normalized young clebsch lower used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.normalizedYoungClebschRaise_toLinearMap {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), mu i = ∑ i : Fin (r + 1), lam i + 1) (row : Fin (r + 1)) (c : ℝ) (hc : 0 < c) (hgram : ∀ (p q : ↥(HarmonicYoungSpace lam)), inner ℝ ((youngClebschRaise mu lam hdeg row) p) ((youngClebschRaise mu lam hdeg row) q) = c * inner ℝ p q) : (normalizedYoungClebschRaise mu lam hdeg row c hc hgram).toLinearMap = (√c)⁻¹ • youngClebschRaise mu lam hdeg row

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.normalizedYoungClebschLower_toLinearMap {r n : ℕ} (mu lam : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), lam i = ∑ i : Fin (r + 1), mu i + 1) (row : Fin (r + 1)) (c : ℝ) (hc : 0 < c) (hgram : ∀ (p q : ↥(HarmonicYoungSpace lam)), inner ℝ ((youngClebschLower mu lam hdeg row) p) ((youngClebschLower mu lam hdeg row) q) = c * inner ℝ p q) : (normalizedYoungClebschLower mu lam hdeg row c hc hgram).toLinearMap = (√c)⁻¹ • youngClebschLower mu lam hdeg row

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngGramRadialIdeal (r n : ℕ) : Ideal (PolynomialSpace r n)

The young gram radial ideal used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowPairingPolynomial_mem_youngGramRadialIdeal {r n : ℕ} (i j : Fin (r + 1)) : rowPairingPolynomial i j ∈ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.polynomialInner_youngGramRadialIdeal_eq_zero_of_traceFree {r n : ℕ} (p q : PolynomialSpace r n) (hp : ∀ (i j : Fin (r + 1)), (traceOperator r n i j) p = 0) (hq : q ∈ youngGramRadialIdeal r n) : SpherePacking.Fischer.polynomialInner ((r + 1) * n) q p = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngGramRadialWeightSubmodule {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Submodule ℝ ↥(youngMultihomogeneousSubmodule n lam)

The young gram radial weight submodule used in the spherical-code argument.

Equations

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

@[reducible, inline]

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

The young gram radial weight quotient used in the spherical-code argument.

Equations

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

def MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousHomogeneousEmbedding {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ↥(youngMultihomogeneousSubmodule n lam) →ₗ[ℝ] ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (∑ i : Fin (r + 1), lam i))

Regard a polynomial of the prescribed row multidegrees as homogeneous of their total degree.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousHomogeneousEmbedding_injective {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Function.Injective ⇑(youngMultihomogeneousHomogeneousEmbedding n lam)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousCoefficientEmbedding {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ↥(youngMultihomogeneousSubmodule n lam) →ₗ[ℝ] SpherePacking.Fischer.CoefficientSpace ((r + 1) * n) (∑ i : Fin (r + 1), lam i)

The Fischer coefficient embedding restricted to the prescribed row multidegrees.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousCoefficientEmbedding_injective {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Function.Injective ⇑(youngMultihomogeneousCoefficientEmbedding n lam)

@[implicit_reducible]

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousFischerCore {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : InnerProductSpace.Core ℝ ↥(youngMultihomogeneousSubmodule n lam)

The inner product core on row-multihomogeneous polynomials induced by their coefficient embedding.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.youngMultihomogeneousFischerCore_inner {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p q : ↥(youngMultihomogeneousSubmodule n lam)) : inner ℝ p q = SpherePacking.Fischer.polynomialInner ((r + 1) * n) ↑p ↑q

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuler_variableIndex_X {r n : ℕ} (a i : Fin (r + 1)) (k : Fin n) : (rowEuler r n a) (MvPolynomial.X (variableIndex i k)) = if a = i then MvPolynomial.X (variableIndex i k) else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuler_rowPairingPolynomial {r n : ℕ} (a i j : Fin (r + 1)) : (rowEuler r n a) (rowPairingPolynomial i j) = (if a = i then rowPairingPolynomial i j else 0) + if a = j then rowPairingPolynomial i j else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuler_pderiv_variableIndex {r n : ℕ} (a i : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) : (rowEuler r n a) ((MvPolynomial.pderiv (variableIndex i k)) p) = (MvPolynomial.pderiv (variableIndex i k)) ((rowEuler r n a) p) - if a = i then (MvPolynomial.pderiv (variableIndex i k)) p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuler_traceOperator_commutator {r n : ℕ} (a i j : Fin (r + 1)) (p : PolynomialSpace r n) : (rowEuler r n a) ((traceOperator r n i j) p) = ((traceOperator r n i j) ((rowEuler r n a) p) - if a = i then (traceOperator r n i j) p else 0) - if a = j then (traceOperator r n i j) p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowEuler_rowPairing_mul_trace {r n : ℕ} (a i j : Fin (r + 1)) (p : PolynomialSpace r n) : (rowEuler r n a) (rowPairingPolynomial i j * (traceOperator r n i j) p) = rowPairingPolynomial i j * (traceOperator r n i j) ((rowEuler r n a) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowPairing_mul_trace_mem_youngMultihomogeneousSubmodule {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(youngMultihomogeneousSubmodule n lam)) (i j : Fin (r + 1)) : rowPairingPolynomial i j * (traceOperator r n i j) ↑p ∈ youngMultihomogeneousSubmodule n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.mem_jointHarmonicWeight_iff_gramOrthogonal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (p : ↥(youngMultihomogeneousSubmodule n lam)) : p ∈ jointHarmonicWeightSubmodule n lam ↔ ∀ q ∈ youngGramRadialWeightSubmodule n lam, inner ℝ q p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_jointHarmonicWeight_add_finrank_youngGramRadialWeight {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Module.finrank ℝ (JointHarmonicWeightSpace n lam) + Module.finrank ℝ ↥(youngGramRadialWeightSubmodule n lam) = ∏ i : Fin (r + 1), (n + lam i - 1).choose (lam i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.finrank_jointHarmonicWeight_eq_finrank_youngGramRadialWeightQuotient {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Module.finrank ℝ (JointHarmonicWeightSpace n lam) = Module.finrank ℝ (YoungGramRadialWeightQuotient n lam)