Harmonic Young branching

Trace ideals, Clebsch decompositions, and arbitrary-rank branching constructions.

theorem MetricCodes.Spherical.HigherYoungSameAxisTraceIdeal.homogeneousTraceFree_eq_iInf_ker {r n m : ℕ} : HigherHarmonicYoung.homogeneousTraceFreeSubmodule r n (m + 2) = ⨅ (ij : Fin (r + 1) × Fin (r + 1)), (HigherHarmonicYoung.homogeneousRowTrace ij.1 ij.2 m).ker

theorem MetricCodes.Spherical.HigherYoungSameAxisTraceIdeal.simultaneousHarmonicProjection_residual_mem_youngGramRadialIdeal {r n m : ℕ} (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (m + 2))) : ↑p - ↑↑((HigherHarmonicYoung.simultaneousHarmonicProjection r n (m + 2)) p) ∈ HigherHarmonicYoung.youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherYoungSameAxisTraceIdeal.simultaneousHarmonicProjection_eq_zero_iff_mem_youngGramRadialIdeal {r n m : ℕ} (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) (m + 2))) : (HigherHarmonicYoung.simultaneousHarmonicProjection r n (m + 2)) p = 0 ↔ ↑p ∈ HigherHarmonicYoung.youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranch.simultaneousHarmonicProjection_eq_zero_iff_gramIdeal {r n d : ℕ} (hd : 2 ≤ d) (p : ↥(SpherePacking.Fischer.Homogeneous ((r + 1) * n) d)) : (simultaneousHarmonicProjection r n d) p = 0 ↔ ↑p ∈ youngGramRadialIdeal r n

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranch.harmonicBranchOfHighestWeightSeed {E : Type u_1} [AddCommGroup E] [Module ℝ E] {r n : ℕ} (lam : Fin (r + 1) → ℕ) (seed : E →ₗ[ℝ] ↥(homogeneousYoungHighestWeightSubmodule lam)) : E →ₗ[ℝ] ↥(HarmonicYoungSpace lam)

The harmonic branch of highest weight seed used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankHarmonicBranch.harmonicBranchOfHighestWeightSeed lam seed = MetricCodes.Spherical.HigherHarmonicYoung.youngHarmonicLift lam ∘ₗ seed

theorem MetricCodes.Spherical.HigherYoungProjectedRaiseInjectivity.traceOperator_X_mul_coordinate {r n : ℕ} (a b row : Fin (r + 1)) (k : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.traceOperator r n a b) (MvPolynomial.X (HigherHarmonicYoung.variableIndex row k) * p) = (MvPolynomial.X (HigherHarmonicYoung.variableIndex row k) * (HigherHarmonicYoung.traceOperator r n a b) p + if a = row then (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex b k)) p else 0) + if b = row then (MvPolynomial.pderiv (HigherHarmonicYoung.variableIndex a k)) p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_chain_commutator {r n : ℕ} (i j k : Fin (r + 1)) (hik : i ≠ k) (p : PolynomialSpace r n) : (polarization r n i j) ((polarization r n j k) p) = (polarization r n i k) p + (polarization r n j k) ((polarization r n i j) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.polarization_eq_zero_of_simpleRoots {r n : ℕ} (p : PolynomialSpace r n) (hsimple : ∀ (a : Fin r), (polarization r n a.castSucc a.succ) p = 0) (i j : Fin (r + 1)) (hij : i < j) : (polarization r n i j) p = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankLowerRowBranching.polarization_polarization_commutator {r n : ℕ} (a b c d : Fin (r + 1)) (p : PolynomialSpace r n) : (polarization r n a b) ((polarization r n c d) p) = ((polarization r n c d) ((polarization r n a b) p) + if b = c then (polarization r n a d) p else 0) - if d = a then (polarization r n c b) p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.rowAxisPolynomial_smul {r n : ℕ} (i : Fin (r + 1)) (c : ℝ) (v : SpherePacking.Euclidean n) : rowAxisPolynomial i (c • v) = c • rowAxisPolynomial i v

theorem MetricCodes.Spherical.HigherHarmonicYoung.MultiplicityFreeClebsch.youngClebschLower_adjoint_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)) (v : SpherePacking.Euclidean n) (q : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (youngClebschLower mu lam hdeg row)) (v ⊗ₜ[ℝ] q) = (projectedCoordinateRaise lam mu hdeg row v) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.FullRankClebschProbabilities.normalizedYoungClebschLower_adjoint_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)) (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) (v : SpherePacking.Euclidean n) (q : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (normalizedYoungClebschLower mu lam hdeg row c hc hgram).toLinearMap) (v ⊗ₜ[ℝ] q) = (√c)⁻¹ • (projectedCoordinateRaise lam mu hdeg row v) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.FullRankClebschProbabilities.normalizedYoungClebschRaise_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)) (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) (v : SpherePacking.Euclidean n) (q : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (normalizedYoungClebschRaise mu lam hdeg row c hc hgram).toLinearMap) (v ⊗ₜ[ℝ] q) = (√c)⁻¹ • (projectedCoordinateLower lam mu hdeg row v) q

def MetricCodes.Spherical.HigherChannel.raiseWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (ℓ : Fin (r + 1)) : Fin (r + 1) → ℕ

The raise weight used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherChannel.raiseWeight lam ℓ = Function.update lam ℓ (lam ℓ + 1)

@[simp]

theorem MetricCodes.Spherical.HigherChannel.ambientShift_raiseWeight_self {r n : ℕ} (lam : Fin (r + 1) → ℕ) (ℓ : Fin (r + 1)) : ambientShift n (raiseWeight lam ℓ) ℓ = ambientShift n lam ℓ + 1

@[simp]

theorem MetricCodes.Spherical.HigherChannel.ambientShift_raiseWeight_other {r n : ℕ} (lam : Fin (r + 1) → ℕ) (ℓ j : Fin (r + 1)) (hj : j ≠ ℓ) : ambientShift n (raiseWeight lam ℓ) j = ambientShift n lam j

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

The weyl edge ratio used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherChannel.plusProbability_eq_weylEdgeRatio_mul_minus {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (ℓ : Fin (r + 1)) (h : FiniteInterlacing n lam mu) (hraise : FiniteInterlacing n (raiseWeight lam ℓ) mu) : plusProbability n lam mu ℓ = weylEdgeRatio n lam ℓ * minusProbability n (raiseWeight lam ℓ) mu ℓ

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

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

The ratio of pair factors when the selected shifted ambient coordinate is increased by one.

Equations

• MetricCodes.Spherical.HigherChannel.pairEdgeRatio L ℓ j = ((L ℓ + 1) ^ 2 - L j ^ 2) / (L ℓ ^ 2 - L j ^ 2)

theorem MetricCodes.Spherical.HigherChannel.pairFactor_eq_shifted {r n : ℕ} (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) : HigherHierarchy.Weyl.pairFactor n lam i j = (ambientShift n lam i - ambientShift n lam j) / (↑↑j - ↑↑i) * ((ambientShift n lam i + ambientShift n lam j) / (↑n - ↑↑i - ↑↑j - 2))

theorem MetricCodes.Spherical.HigherChannel.pairFactor_raiseWeight {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (ℓ i j : Fin (r + 1)) (hij : i < j) (h : FiniteInterlacing n lam mu) : HigherHierarchy.Weyl.pairFactor n (raiseWeight lam ℓ) i j = HigherHierarchy.Weyl.pairFactor n lam i j * if i = ℓ then pairEdgeRatio (ambientShift n lam) ℓ j else if j = ℓ then pairEdgeRatio (ambientShift n lam) ℓ i else 1

theorem MetricCodes.Spherical.HigherChannel.incidentPairProduct {r : ℕ} (ℓ : Fin (r + 1)) (w : Fin (r + 1) → ℝ) : (∏ i : Fin (r + 1), ∏ j : Fin (r + 1), if i < j then if i = ℓ then w j else if j = ℓ then w i else 1 else 1) = ∏ j ∈ Finset.univ.erase ℓ, w j

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

The row factor in the Weyl-dimension ratio for increasing row ℓ by one.

Equations

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

theorem MetricCodes.Spherical.HigherChannel.tailLength_cast_eq_shifted {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (ℓ : Fin (r + 1)) : ↑(lam ℓ) + ↑(HigherHierarchy.Weyl.tailLength n r ℓ) + 1 = ambientShift n lam ℓ + wallShift n r

theorem MetricCodes.Spherical.HigherChannel.rowTail_cast_eq_shifted {r n : ℕ} (lam : Fin (r + 1) → ℕ) (ℓ : Fin (r + 1)) : ↑(lam ℓ) + ↑(HigherHierarchy.Weyl.rowTail ℓ) + 1 = ambientShift n lam ℓ + 1 - wallShift n r

theorem MetricCodes.Spherical.HigherChannel.rowFactor_raiseWeight_self {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (ℓ : Fin (r + 1)) : HigherHierarchy.Weyl.rowFactor n (raiseWeight lam ℓ) ℓ = HigherHierarchy.Weyl.rowFactor n lam ℓ * rowEdgeRatio n lam ℓ

theorem MetricCodes.Spherical.HigherChannel.rowFactor_raiseWeight_other {r n : ℕ} (lam : Fin (r + 1) → ℕ) (ℓ i : Fin (r + 1)) (hi : i ≠ ℓ) : HigherHierarchy.Weyl.rowFactor n (raiseWeight lam ℓ) i = HigherHierarchy.Weyl.rowFactor n lam i

theorem MetricCodes.Spherical.HigherChannel.rowFactorProduct_raiseWeight {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : FiniteInterlacing n lam mu) (ℓ : Fin (r + 1)) : ∏ i : Fin (r + 1), HigherHierarchy.Weyl.rowFactor n (raiseWeight lam ℓ) i = (∏ i : Fin (r + 1), HigherHierarchy.Weyl.rowFactor n lam i) * rowEdgeRatio n lam ℓ

theorem MetricCodes.Spherical.HigherChannel.pairEdgeRatio_prod_erase_eq {r : ℕ} (L : Fin (r + 1) → ℝ) (ℓ : Fin (r + 1)) : ∏ j ∈ Finset.univ.erase ℓ, pairEdgeRatio L ℓ j = ∏ q : Fin r, pairEdgeRatio L ℓ (ℓ.succAbove q)

theorem MetricCodes.Spherical.HigherChannel.pairFactorProduct_raiseWeight {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (ℓ : Fin (r + 1)) (h : FiniteInterlacing n lam mu) : (∏ i : Fin (r + 1), ∏ j : Fin (r + 1), if i < j then HigherHierarchy.Weyl.pairFactor n (raiseWeight lam ℓ) i j else 1) = (∏ i : Fin (r + 1), ∏ j : Fin (r + 1), if i < j then HigherHierarchy.Weyl.pairFactor n lam i j else 1) * ∏ q : Fin r, pairEdgeRatio (ambientShift n lam) ℓ (ℓ.succAbove q)

theorem MetricCodes.Spherical.HigherChannel.weylDimension_raiseWeight {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (ℓ : Fin (r + 1)) (h : FiniteInterlacing n lam mu) : HigherHierarchy.Weyl.dimension n (raiseWeight lam ℓ) = HigherHierarchy.Weyl.dimension n lam * weylEdgeRatio n lam ℓ

theorem MetricCodes.Spherical.HigherChannel.actual_weyl_detailed_balance {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (ℓ : Fin (r + 1)) (h : FiniteInterlacing n lam mu) (hraise : FiniteInterlacing n (raiseWeight lam ℓ) mu) : HigherHierarchy.Weyl.dimension n lam * plusProbability n lam mu ℓ = HigherHierarchy.Weyl.dimension n (raiseWeight lam ℓ) * minusProbability n (raiseWeight lam ℓ) mu ℓ

noncomputable def MetricCodes.Spherical.HigherChannel.flooredCoordinates {I : Type u_1} (a : I → ℝ) (n : ℕ) : I → ℕ

The floored coordinates used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherChannel.flooredCoordinates a n i = ⌊a i * ↑n⌋₊

theorem MetricCodes.Spherical.HigherChannel.tendsto_flooredCoordinates_ratio {I : Type u_1} (a : I → ℝ) (i : I) (ha : 0 ≤ a i) : Filter.Tendsto (fun (n : ℕ) => ↑(flooredCoordinates a n i) / ↑n) Filter.atTop (nhds (a i))

theorem MetricCodes.Spherical.HigherChannel.tendsto_wallShift_div (r : ℕ) : Filter.Tendsto (fun (n : ℕ) => wallShift n r / ↑n) Filter.atTop (nhds (1 / 2))

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHierarchyBoxSpectral.BoxVertex (r m : ℕ) : Type

The box vertex used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchyBoxSpectral.BoxVertex r m = (Fin (r + 1) → Fin (m + 1))

def MetricCodes.Spherical.HigherHierarchyBoxSpectral.nextVertex {r m : ℕ} (v : BoxVertex r m) (i : Fin (r + 1)) (h : ↑(v i) < m) : BoxVertex r m

The next vertex used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchyBoxSpectral.nextVertex v i h = Function.update v i ⟨↑(v i) + 1, ⋯⟩

def MetricCodes.Spherical.HigherHierarchyBoxSpectral.forwardMatrix {r m : ℕ} (edge : BoxVertex r m → Fin (r + 1) → ℝ) : Matrix (BoxVertex r m) (BoxVertex r m) ℝ

The weighted forward adjacency matrix of the rectangular box of signatures.

Equations

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

def MetricCodes.Spherical.HigherHierarchyBoxSpectral.adjacencyMatrix {r m : ℕ} (edge : BoxVertex r m → Fin (r + 1) → ℝ) : Matrix (BoxVertex r m) (BoxVertex r m) ℝ

The symmetric box adjacency matrix obtained by adding the forward matrix to its transpose.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchyBoxSpectral.adjacencyMatrix_transpose {r m : ℕ} (edge : BoxVertex r m → Fin (r + 1) → ℝ) : (adjacencyMatrix edge).transpose = adjacencyMatrix edge

theorem MetricCodes.Spherical.HigherHierarchyBoxSpectral.boxVertex_card (r m : ℕ) : Fintype.card (BoxVertex r m) = (m + 1) ^ (r + 1)

theorem MetricCodes.Spherical.HigherHierarchyBoxSpectral.upperFace_card {r m : ℕ} (i : Fin (r + 1)) : {v : BoxVertex r m | v i = Fin.last m}.card = (m + 1) ^ r

theorem MetricCodes.Spherical.HigherHierarchyBoxSpectral.forwardFace_card {r m : ℕ} (i : Fin (r + 1)) : {v : BoxVertex r m | ↑(v i) < m}.card = m * (m + 1) ^ r

theorem MetricCodes.Spherical.HigherHierarchyBoxSpectral.forwardMatrix_sum {r m : ℕ} (edge : BoxVertex r m → Fin (r + 1) → ℝ) : ∑ v : BoxVertex r m, ∑ w : BoxVertex r m, forwardMatrix edge v w = ∑ v : BoxVertex r m, ∑ i : Fin (r + 1), if ↑(v i) < m then edge v i else 0

theorem MetricCodes.Spherical.HigherHierarchyBoxSpectral.adjacencyMatrix_sum {r m : ℕ} (edge : BoxVertex r m → Fin (r + 1) → ℝ) : ∑ v : BoxVertex r m, ∑ w : BoxVertex r m, adjacencyMatrix edge v w = 2 * ∑ v : BoxVertex r m, ∑ i : Fin (r + 1), if ↑(v i) < m then edge v i else 0

noncomputable def MetricCodes.Spherical.HigherHierarchyBoxSpectral.constantRayleigh {r m : ℕ} (edge : BoxVertex r m → Fin (r + 1) → ℝ) : ℝ

The Rayleigh quotient of the constant vector for the weighted box adjacency matrix.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchyBoxSpectral.constantRayleigh_eq {r m : ℕ} (edge : BoxVertex r m → Fin (r + 1) → ℝ) : constantRayleigh edge = (2 * ∑ v : BoxVertex r m, ∑ i : Fin (r + 1), if ↑(v i) < m then edge v i else 0) / ↑(Fintype.card (BoxVertex r m))

theorem MetricCodes.Spherical.HigherHierarchyBoxSpectral.forwardFace_sum {r m : ℕ} (i : Fin (r + 1)) (c : ℝ) : (∑ v : BoxVertex r m, if ↑(v i) < m then c else 0) = ↑m * ↑(m + 1) ^ r * c

theorem MetricCodes.Spherical.HigherHierarchyBoxSpectral.constantRayleigh_const {r m : ℕ} (weight : Fin (r + 1) → ℝ) : (constantRayleigh fun (x : BoxVertex r m) => weight) = 2 * ↑m / (↑m + 1) * ∑ i : Fin (r + 1), weight i

theorem MetricCodes.Spherical.HigherHierarchyBoxSpectral.constantRayleigh_tendsto {r m : ℕ} (edge : ℕ → BoxVertex r m → Fin (r + 1) → ℝ) (weight : Fin (r + 1) → ℝ) (hlimit : ∀ (v : BoxVertex r m) (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => edge n v i) Filter.atTop (nhds (weight i))) : Filter.Tendsto (fun (n : ℕ) => constantRayleigh (edge n)) Filter.atTop (nhds (2 * ↑m / (↑m + 1) * ∑ i : Fin (r + 1), weight i))

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHierarchy.RectangularVertices.Vertex (r m : ℕ) : Type

The vertex used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.RectangularVertices.Vertex r m = (Fin (r + 1) → Fin (m + 1))

noncomputable def MetricCodes.Spherical.HigherHierarchy.RectangularVertices.signature {r : ℕ} (a : Fin (r + 1) → ℝ) (n : ℕ) {m : ℕ} (v : Vertex r m) : Fin (r + 1) → ℕ

The signature used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.RectangularVertices.signature a n v i = MetricCodes.Spherical.HigherChannel.flooredCoordinates a n i + ↑(v i)

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_offset_div {r m : ℕ} (v : ℕ → Vertex r m) (i : Fin (r + 1)) : Filter.Tendsto (fun (n : ℕ) => ↑↑(v n i) / ↑n) Filter.atTop (nhds 0)

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_signature_ratio {r m : ℕ} (a : Fin (r + 1) → ℝ) (v : ℕ → Vertex r m) (i : Fin (r + 1)) (ha : 0 ≤ a i) : Filter.Tendsto (fun (n : ℕ) => ↑(signature a n (v n) i) / ↑n) Filter.atTop (nhds (a i))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.eventually_signature_lt_of_lt {r m : ℕ} (a : Fin (r + 1) → ℝ) (v : ℕ → Vertex r m) (i j : Fin (r + 1)) (hi : 0 ≤ a i) (hj : 0 ≤ a j) (hij : a i < a j) : ∀ᶠ (n : ℕ) in Filter.atTop, signature a n (v n) i < signature a n (v n) j

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.eventually_signature_strictAnti {r m : ℕ} (a : Fin (r + 1) → ℝ) (ha : ∀ (i : Fin (r + 1)), 0 ≤ a i) (hanti : StrictAnti a) (v : ℕ → Vertex r m) : ∀ᶠ (n : ℕ) in Filter.atTop, StrictAnti (signature a n (v n))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.eventually_strictInterlaces_all {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (v : Vertex r m), HigherRepresentationGraph.StrictInterlaces (signature a n v) (HigherChannel.flooredCoordinates b n)

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.eventually_finiteInterlacing_all {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (v : Vertex r m), HigherChannel.FiniteInterlacing n (signature a n v) (HigherChannel.flooredCoordinates b n)

noncomputable def MetricCodes.Spherical.HigherHierarchy.RectangularVertices.correctedSignature {r m : ℕ} (a : Fin (r + 1) → ℝ) (v : ℕ → Vertex r m) (n : ℕ) : Fin (r + 1) → ℕ

The signature when it is dominant, with the floored ambient weight as a dominant fallback.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.correctedSignature_antitone {r m : ℕ} (a : Fin (r + 1) → ℝ) (hanti : Antitone a) (v : ℕ → Vertex r m) (n : ℕ) : Antitone (correctedSignature a v n)

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.eventually_correctedSignature_eq {r m : ℕ} (a : Fin (r + 1) → ℝ) (ha : ∀ (i : Fin (r + 1)), 0 ≤ a i) (hanti : StrictAnti a) (v : ℕ → Vertex r m) : ∀ᶠ (n : ℕ) in Filter.atTop, correctedSignature a v n = signature a n (v n)

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_correctedSignature_ratio {r m : ℕ} (a : Fin (r + 1) → ℝ) (ha : ∀ (i : Fin (r + 1)), 0 ≤ a i) (hanti : StrictAnti a) (v : ℕ → Vertex r m) (i : Fin (r + 1)) : Filter.Tendsto (fun (n : ℕ) => ↑(correctedSignature a v n i) / ↑n) Filter.atTop (nhds (a i))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_correctedSignature_atTop {r m : ℕ} (a : Fin (r + 1) → ℝ) (ha : ∀ (i : Fin (r + 1)), 0 < a i) (hanti : StrictAnti a) (v : ℕ → Vertex r m) (i : Fin (r + 1)) : Filter.Tendsto (fun (n : ℕ) => correctedSignature a v n i) Filter.atTop Filter.atTop

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_log_vertexDimension_div_log_two {r m : ℕ} (a : Fin (r + 1) → ℝ) (ha : ∀ (i : Fin (r + 1)), 0 < a i) (hanti : StrictAnti a) (v : ℕ → Vertex r m) : Filter.Tendsto (fun (n : ℕ) => Real.log (Weyl.dimension n (signature a n (v n))) / ↑n / Real.log 2) Filter.atTop (nhds (∑ i : Fin (r + 1), sphericalEntropy (a i)))

noncomputable def MetricCodes.Spherical.HigherHierarchy.RectangularVertices.vertexDimension {r m : ℕ} (a : Fin (r + 1) → ℝ) (n : ℕ) (v : Vertex r m) : ℝ

The vertex dimension used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHierarchy.RectangularVertices.dimensionSum {r m : ℕ} (a : Fin (r + 1) → ℝ) (n : ℕ) : ℝ

The dimension sum used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.eventually_vertexDimension_pos_all {r m : ℕ} (a : Fin (r + 1) → ℝ) (ha : ∀ (i : Fin (r + 1)), 0 < a i) (hanti : StrictAnti a) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (v : Vertex r m), 0 < vertexDimension a n v

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_log_finset_sum {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → ℕ → ℝ) (H : ℝ) (hf : ∀ (i : ι) (n : ℕ), 0 < f i n) (hlim : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => Real.log (f i n) / ↑n) Filter.atTop (nhds H)) : Filter.Tendsto (fun (n : ℕ) => Real.log (∑ i : ι, f i n) / ↑n) Filter.atTop (nhds H)

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_log_finset_sum_of_eventually_pos {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → ℕ → ℝ) (H : ℝ) (hf : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : ι), 0 < f i n) (hlim : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => Real.log (f i n) / ↑n) Filter.atTop (nhds H)) : Filter.Tendsto (fun (n : ℕ) => Real.log (∑ i : ι, f i n) / ↑n) Filter.atTop (nhds H)

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_log_finset_sum_div_log_two_of_eventually_pos {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → ℕ → ℝ) (H : ℝ) (hf : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : ι), 0 < f i n) (hlim : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => Real.log (f i n) / ↑n / Real.log 2) Filter.atTop (nhds H)) : Filter.Tendsto (fun (n : ℕ) => Real.log (∑ i : ι, f i n) / ↑n / Real.log 2) Filter.atTop (nhds H)

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_log_dimensionSum_div_log_two {r m : ℕ} (a : Fin (r + 1) → ℝ) (ha : ∀ (i : Fin (r + 1)), 0 < a i) (hanti : StrictAnti a) : Filter.Tendsto (fun (n : ℕ) => Real.log (dimensionSum a n) / ↑n / Real.log 2) Filter.atTop (nhds (∑ i : Fin (r + 1), sphericalEntropy (a i)))

def MetricCodes.Spherical.HigherHierarchy.RectangularVertices.nextVertex {r m : ℕ} (v : Vertex r m) (i : Fin (r + 1)) (h : ↑(v i) < m) : Vertex r m

The next vertex used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchy.RectangularVertices.nextVertex v i h = Function.update v i ⟨↑(v i) + 1, ⋯⟩

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.signature_nextVertex {r m : ℕ} (a : Fin (r + 1) → ℝ) (n : ℕ) (v : Vertex r m) (i : Fin (r + 1)) (h : ↑(v i) < m) : signature a n (nextVertex v i h) = HigherChannel.raiseWeight (signature a n v) i

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_ambientShift_of_ratio {r : ℕ} (lam : ℕ → Fin (r + 1) → ℕ) (a : Fin (r + 1) → ℝ) (i : Fin (r + 1)) (hlim : Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds (a i))) : Filter.Tendsto (fun (n : ℕ) => HigherChannel.ambientShift n (lam n) i / ↑n) Filter.atTop (nhds (a i + 1 / 2))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_stabilizerShift_of_ratio {r : ℕ} (mu : ℕ → Fin r → ℕ) (b : Fin r → ℝ) (i : Fin r) (hlim : Filter.Tendsto (fun (n : ℕ) => ↑(mu n i) / ↑n) Filter.atTop (nhds (b i))) : Filter.Tendsto (fun (n : ℕ) => HigherChannel.stabilizerShift n (mu n) i / ↑n) Filter.atTop (nhds (b i + 1 / 2))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_channelFactor_of_ratios {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) (lam : ℕ → Fin (r + 1) → ℕ) (mu : ℕ → Fin r → ℕ) (hlam : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds (a i))) (hmu : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => ↑(mu n i) / ↑n) Filter.atTop (nhds (b i))) (i : Fin (r + 1)) (j : Fin r) (c d : ℝ) : Filter.Tendsto (fun (n : ℕ) => ((HigherChannel.ambientShift n (lam n) i + c) ^ 2 - HigherChannel.stabilizerShift n (mu n) j ^ 2) / ((HigherChannel.ambientShift n (lam n) i + d) ^ 2 - HigherChannel.ambientShift n (lam n) (i.succAbove j) ^ 2)) Filter.atTop (nhds ((a i * (1 + a i) - b j * (1 + b j)) / (a i * (1 + a i) - a (i.succAbove j) * (1 + a (i.succAbove j)))))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_plusLeadingFactor_of_ratio {r : ℕ} (lam : ℕ → Fin (r + 1) → ℕ) (a : Fin (r + 1) → ℝ) (i : Fin (r + 1)) (ha : 0 ≤ a i) (hlim : Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds (a i))) : Filter.Tendsto (fun (n : ℕ) => (HigherChannel.ambientShift n (lam n) i + HigherChannel.wallShift n r) / (2 * HigherChannel.ambientShift n (lam n) i)) Filter.atTop (nhds ((a i + 1) / (2 * a i + 1)))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_raisedMinusLeadingFactor_of_ratio {r : ℕ} (lam : ℕ → Fin (r + 1) → ℕ) (a : Fin (r + 1) → ℝ) (i : Fin (r + 1)) (ha : 0 ≤ a i) (hlim : Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds (a i))) : Filter.Tendsto (fun (n : ℕ) => (HigherChannel.ambientShift n (lam n) i + 1 - HigherChannel.wallShift n r) / (2 * (HigherChannel.ambientShift n (lam n) i + 1))) Filter.atTop (nhds (a i / (2 * a i + 1)))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_plusProbability_of_ratios {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) (lam : ℕ → Fin (r + 1) → ℕ) (mu : ℕ → Fin r → ℕ) (hlam : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds (a i))) (hmu : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => ↑(mu n i) / ↑n) Filter.atTop (nhds (b i))) (i : Fin (r + 1)) : Filter.Tendsto (fun (n : ℕ) => HigherChannel.plusProbability n (lam n) (mu n) i) Filter.atTop (nhds ((a i + 1) / (2 * a i + 1) * lagrangeWeight a b i))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_minusProbability_raiseWeight_of_ratios {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) (lam : ℕ → Fin (r + 1) → ℕ) (mu : ℕ → Fin r → ℕ) (hlam : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds (a i))) (hmu : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => ↑(mu n i) / ↑n) Filter.atTop (nhds (b i))) (i : Fin (r + 1)) : Filter.Tendsto (fun (n : ℕ) => HigherChannel.minusProbability n (HigherChannel.raiseWeight (lam n) i) (mu n) i) Filter.atTop (nhds (a i / (2 * a i + 1) * lagrangeWeight a b i))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_actualEdgeWeight_of_ratios {r : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) (lam : ℕ → Fin (r + 1) → ℕ) (mu : ℕ → Fin r → ℕ) (hlam : ∀ (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => ↑(lam n i) / ↑n) Filter.atTop (nhds (a i))) (hmu : ∀ (i : Fin r), Filter.Tendsto (fun (n : ℕ) => ↑(mu n i) / ↑n) Filter.atTop (nhds (b i))) (i : Fin (r + 1)) : Filter.Tendsto (fun (n : ℕ) => √(HigherChannel.plusProbability n (lam n) (mu n) i * HigherChannel.minusProbability n (HigherChannel.raiseWeight (lam n) i) (mu n) i)) Filter.atTop (nhds (lagrangeWeight a b i * spectralAtom (a i)))

noncomputable def MetricCodes.Spherical.HigherHierarchy.RectangularVertices.edgeWeight {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v : Vertex r m) (i : Fin (r + 1)) : ℝ

The edge weight used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.tendsto_edgeWeight {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) (v : Vertex r m) (i : Fin (r + 1)) : Filter.Tendsto (fun (n : ℕ) => edgeWeight a b n v i) Filter.atTop (nhds (lagrangeWeight a b i * spectralAtom (a i)))

theorem MetricCodes.Spherical.HigherHierarchy.RectangularVertices.eventually_edgeWeight_pos_all {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : Interlacing a b) (ha : ∀ (i : Fin (r + 1)), 0 < a i) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (v : Vertex r m) (i : Fin (r + 1)), 0 < edgeWeight a b n v i

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.Vertex (r m : ℕ) : Type

The vertex used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.Vertex r m = MetricCodes.Spherical.HigherHierarchyBoxSpectral.BoxVertex r m

noncomputable def MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.signature {r m : ℕ} (a : Fin (r + 1) → ℝ) (n : ℕ) (v : Vertex r m) : Fin (r + 1) → ℕ

The signature used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.signature a n v i = MetricCodes.Spherical.HigherChannel.flooredCoordinates a n i + ↑(v i)

theorem MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.signature_nextVertex {r m : ℕ} (a : Fin (r + 1) → ℝ) (n : ℕ) (v : Vertex r m) (i : Fin (r + 1)) (h : ↑(v i) < m) : signature a n (HigherHierarchyBoxSpectral.nextVertex v i h) = HigherChannel.raiseWeight (signature a n v) i

noncomputable def MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.edgeWeight {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v : Vertex r m) (i : Fin (r + 1)) : ℝ

The edge weight used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.edgeWeight_nonneg {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v : Vertex r m) (i : Fin (r + 1)) : 0 ≤ edgeWeight a b n v i

noncomputable def MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.matrix {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) : Matrix (Vertex r m) (Vertex r m) ℝ

The matrix used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.matrix_symmetric {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) : (matrix a b n).transpose = matrix a b n

theorem MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.matrix_nonneg {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v w : Vertex r m) : 0 ≤ matrix a b n v w

def MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.grid (r m : ℕ) : SimpleGraph (Vertex r m)

The grid used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.grid_adj_nextVertex {r m : ℕ} (v : Vertex r m) (i : Fin (r + 1)) (h : ↑(v i) < m) : (grid r m).Adj v (HigherHierarchyBoxSpectral.nextVertex v i h)

theorem MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.reachable_zero {r m : ℕ} (v : Vertex r m) : (grid r m).Reachable (fun (x : Fin (r + 1)) => 0) v

theorem MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.grid_connected (r m : ℕ) : (grid r m).Connected

theorem MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.matrix_pos_of_grid_adj {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (hpositive : ∀ (v : Vertex r m) (i : Fin (r + 1)), ↑(v i) < m → 0 < edgeWeight a b n v i) {v w : Vertex r m} (hadj : (grid r m).Adj v w) : 0 < matrix a b n v w

theorem MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.matrix_irreducible {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (hm : 0 < m) (hpositive : ∀ (v : Vertex r m) (i : Fin (r + 1)), ↑(v i) < m → 0 < edgeWeight a b n v i) : HigherHierarchyFinitePerron.ConnectedNonnegativeMatrix (matrix a b n)

theorem MetricCodes.Spherical.HigherHierarchyTrueGridAdjacency.eventually_matrix_irreducible {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (h : HigherHierarchy.Interlacing a b) (ha : ∀ (i : Fin (r + 1)), 0 < a i) (hm : 0 < m) : ∀ᶠ (n : ℕ) in Filter.atTop, HigherHierarchyFinitePerron.ConnectedNonnegativeMatrix (matrix a b n)

noncomputable def MetricCodes.Spherical.HigherHierarchyBoxChannels.plusEdge {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v : HigherHierarchyTrueGridAdjacency.Vertex r m) (i : Fin (r + 1)) : ℝ

The plus edge used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHierarchyBoxChannels.minusEdge {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v : HigherHierarchyTrueGridAdjacency.Vertex r m) (i : Fin (r + 1)) : ℝ

The minus edge used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHierarchyBoxChannels.probability {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v w : HigherHierarchyTrueGridAdjacency.Vertex r m) : ℝ

The probability used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHierarchyBoxChannels.vertexWeylDimension {r m : ℕ} (a : Fin (r + 1) → ℝ) (n : ℕ) (v : HigherHierarchyTrueGridAdjacency.Vertex r m) : ℝ

The Weyl dimension evaluated at the signature attached to a rectangular-box vertex.

Equations

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

theorem MetricCodes.Spherical.HigherHierarchyBoxChannels.nextVertex_direction_injective {r m : ℕ} (v : HigherHierarchyTrueGridAdjacency.Vertex r m) (i j : Fin (r + 1)) (hi : ↑(v i) < m) (hj : ↑(v j) < m) (heq : HigherHierarchyBoxSpectral.nextVertex v i hi = HigherHierarchyBoxSpectral.nextVertex v j hj) : i = j

theorem MetricCodes.Spherical.HigherHierarchyBoxChannels.nextVertex_not_forward_back {r m : ℕ} (v : HigherHierarchyTrueGridAdjacency.Vertex r m) (i j : Fin (r + 1)) (hi : ↑(v i) < m) (hj : ↑(HigherHierarchyBoxSpectral.nextVertex v i hi j) < m) : v ≠ HigherHierarchyBoxSpectral.nextVertex (HigherHierarchyBoxSpectral.nextVertex v i hi) j hj

theorem MetricCodes.Spherical.HigherHierarchyBoxChannels.forwardMatrix_nextVertex {r m : ℕ} (edge : HigherHierarchyTrueGridAdjacency.Vertex r m → Fin (r + 1) → ℝ) (v : HigherHierarchyTrueGridAdjacency.Vertex r m) (i : Fin (r + 1)) (hi : ↑(v i) < m) : HigherHierarchyBoxSpectral.forwardMatrix edge v (HigherHierarchyBoxSpectral.nextVertex v i hi) = edge v i

theorem MetricCodes.Spherical.HigherHierarchyBoxChannels.forwardMatrix_nextVertex_reverse {r m : ℕ} (edge : HigherHierarchyTrueGridAdjacency.Vertex r m → Fin (r + 1) → ℝ) (v : HigherHierarchyTrueGridAdjacency.Vertex r m) (i : Fin (r + 1)) (hi : ↑(v i) < m) : HigherHierarchyBoxSpectral.forwardMatrix edge (HigherHierarchyBoxSpectral.nextVertex v i hi) v = 0

theorem MetricCodes.Spherical.HigherHierarchyBoxChannels.probability_nextVertex {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v : HigherHierarchyTrueGridAdjacency.Vertex r m) (i : Fin (r + 1)) (hi : ↑(v i) < m) : probability a b n v (HigherHierarchyBoxSpectral.nextVertex v i hi) = plusEdge a b n v i

theorem MetricCodes.Spherical.HigherHierarchyBoxChannels.probability_nextVertex_reverse {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v : HigherHierarchyTrueGridAdjacency.Vertex r m) (i : Fin (r + 1)) (hi : ↑(v i) < m) : probability a b n (HigherHierarchyBoxSpectral.nextVertex v i hi) v = minusEdge a b n v i

theorem MetricCodes.Spherical.HigherHierarchyBoxChannels.probability_eq_zero_of_not_adjacent {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v w : HigherHierarchyTrueGridAdjacency.Vertex r m) (h : ¬(HigherHierarchyTrueGridAdjacency.grid r m).Adj v w) : probability a b n v w = 0

theorem MetricCodes.Spherical.HigherHierarchyBoxChannels.probability_nonneg {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (hinterlacing : ∀ (v : HigherHierarchyTrueGridAdjacency.Vertex r m), HigherChannel.FiniteInterlacing n (HigherHierarchyTrueGridAdjacency.signature a n v) (HigherChannel.flooredCoordinates b n)) (v w : HigherHierarchyTrueGridAdjacency.Vertex r m) : 0 ≤ probability a b n v w

theorem MetricCodes.Spherical.HigherHierarchyBoxChannels.weyl_detailed_balance {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (hinterlacing : ∀ (v : HigherHierarchyTrueGridAdjacency.Vertex r m), HigherChannel.FiniteInterlacing n (HigherHierarchyTrueGridAdjacency.signature a n v) (HigherChannel.flooredCoordinates b n)) (v w : HigherHierarchyTrueGridAdjacency.Vertex r m) : vertexWeylDimension a n v * probability a b n v w = vertexWeylDimension a n w * probability a b n w v

theorem MetricCodes.Spherical.HigherHierarchyBoxChannels.symmetric_probability_eq_trueGrid {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (v w : HigherHierarchyTrueGridAdjacency.Vertex r m) : √(probability a b n v w * probability a b n w v) = HigherHierarchyTrueGridAdjacency.matrix a b n v w

def MetricCodes.Spherical.HigherHierarchyBoxPerron.constantVector (r m : ℕ) : HigherHierarchyFinitePerron.Space (HigherHierarchyBoxSpectral.BoxVertex r m)

The vector with every box-vertex coordinate equal to one.

Equations

• MetricCodes.Spherical.HigherHierarchyBoxPerron.constantVector r m = WithLp.toLp 2 fun (x : MetricCodes.Spherical.HigherHierarchyBoxSpectral.BoxVertex r m) => 1

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.constantVector_ne_zero (r m : ℕ) : constantVector r m ≠ 0

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.constantVector_norm_sq (r m : ℕ) : ‖constantVector r m‖ ^ 2 = ↑(Fintype.card (HigherHierarchyBoxSpectral.BoxVertex r m))

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.constantVector_rayleigh {r m : ℕ} (edge : HigherHierarchyBoxSpectral.BoxVertex r m → Fin (r + 1) → ℝ) : HigherHierarchyFinitePerron.rayleigh (HigherHierarchyBoxSpectral.adjacencyMatrix edge) (constantVector r m) = HigherHierarchyBoxSpectral.constantRayleigh edge

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.constantRayleigh_le_top {r m : ℕ} (edge : HigherHierarchyBoxSpectral.BoxVertex r m → Fin (r + 1) → ℝ) : HigherHierarchyBoxSpectral.constantRayleigh edge ≤ HigherHierarchyFinitePerron.topEigenvalue (HigherHierarchyBoxSpectral.adjacencyMatrix edge)

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.boxWidth_ratio_tendsto : Filter.Tendsto (fun (m : ℕ) => ↑m / (↑m + 1)) Filter.atTop (nhds 1)

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.exists_boxWidth_spectral_gap {s gamma : ℝ} (hspectral : s < 2 * gamma) : ∃ (m : ℕ), 0 < m ∧ s < 2 * ↑m / (↑m + 1) * gamma

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.eventually_topEigenvalue_gt_of_edge_limits {r m : ℕ} (edge : ℕ → HigherHierarchyBoxSpectral.BoxVertex r m → Fin (r + 1) → ℝ) (weight : Fin (r + 1) → ℝ) (hlimit : ∀ (v : HigherHierarchyBoxSpectral.BoxVertex r m) (i : Fin (r + 1)), Filter.Tendsto (fun (n : ℕ) => edge n v i) Filter.atTop (nhds (weight i))) {s : ℝ} (hspectral : s < 2 * ↑m / (↑m + 1) * ∑ i : Fin (r + 1), weight i) : ∀ᶠ (n : ℕ) in Filter.atTop, s < HigherHierarchyFinitePerron.topEigenvalue (HigherHierarchyBoxSpectral.adjacencyMatrix (edge n))

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.exists_boxWidth_eventually_actual_topEigenvalue_gt {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : HigherHierarchy.Interlacing a b) {s : ℝ} (hspectral : s < 2 * HigherHierarchy.Gamma a b) : ∃ (m : ℕ), 0 < m ∧ ∀ᶠ (n : ℕ) in Filter.atTop, s < HigherHierarchyFinitePerron.topEigenvalue (HigherHierarchyBoxSpectral.adjacencyMatrix (HigherHierarchy.RectangularVertices.edgeWeight a b n))

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.trueGrid_matrix_eq_rectangular {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) : HigherHierarchyTrueGridAdjacency.matrix a b n = HigherHierarchyBoxSpectral.adjacencyMatrix (HigherHierarchy.RectangularVertices.edgeWeight a b n)

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.exists_boxWidth_eventually_positive_eigenpair_gt {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : HigherHierarchy.Interlacing a b) (ha : ∀ (i : Fin (r + 1)), 0 < a i) {s : ℝ} (hspectral : s < 2 * HigherHierarchy.Gamma a b) : ∃ (m : ℕ), 0 < m ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (eigenvalue : ℝ) (x : HigherHierarchyBoxSpectral.BoxVertex r m → ℝ), s < eigenvalue ∧ (∀ (v : HigherHierarchyBoxSpectral.BoxVertex r m), 0 < x v) ∧ ∑ v : HigherHierarchyBoxSpectral.BoxVertex r m, x v ^ 2 = 1 ∧ ∀ (v : HigherHierarchyBoxSpectral.BoxVertex r m), ∑ w : HigherHierarchyBoxSpectral.BoxVertex r m, HigherHierarchyTrueGridAdjacency.matrix a b n v w * x w = eigenvalue * x v

theorem MetricCodes.Spherical.HigherHierarchyBoxPerron.exists_boxWidth_positive_gap_eventually_positive_eigenpair {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : HigherHierarchy.Interlacing a b) (ha : ∀ (i : Fin (r + 1)), 0 < a i) {s : ℝ} (hspectral : s < 2 * HigherHierarchy.Gamma a b) : ∃ (m : ℕ) (gap : ℝ), 0 < m ∧ 0 < gap ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (eigenvalue : ℝ) (x : HigherHierarchyBoxSpectral.BoxVertex r m → ℝ), s + gap < eigenvalue ∧ (∀ (v : HigherHierarchyBoxSpectral.BoxVertex r m), 0 < x v) ∧ ∑ v : HigherHierarchyBoxSpectral.BoxVertex r m, x v ^ 2 = 1 ∧ ∀ (v : HigherHierarchyBoxSpectral.BoxVertex r m), ∑ w : HigherHierarchyBoxSpectral.BoxVertex r m, HigherHierarchyTrueGridAdjacency.matrix a b n v w * x w = eigenvalue * x v

theorem MetricCodes.Spherical.HigherHierarchy.interlacing_strictAnti_stabilizer {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : StrictAnti b

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_flooredCoordinates_succ_ratio {I : Type u_1} (a : I → ℝ) (i : I) (ha : 0 ≤ a i) : Filter.Tendsto (fun (n : ℕ) => ↑(HigherChannel.flooredCoordinates a (n + 1) i) / ↑n) Filter.atTop (nhds (a i))

theorem MetricCodes.Spherical.HigherHierarchy.tendsto_log_stabilizerDimension_floor_current_div_log_two {r : ℕ} (b : Fin (r + 1) → ℝ) (hb : ∀ (i : Fin (r + 1)), 0 < b i) (hanti : StrictAnti b) : Filter.Tendsto (fun (n : ℕ) => Real.log (Weyl.dimension (n - 1) (Weyl.flooredWeight b n)) / ↑n / Real.log 2) Filter.atTop (nhds (∑ i : Fin (r + 1), sphericalEntropy (b i)))

structure MetricCodes.Spherical.HigherHierarchy.IndexedHierarchyGraph (n : ℕ) : Type

Data encoding the indexed hierarchy graph construction.

• vertexCount : ℕ

  The vertex count component.

• ambientDimension : ℕ

  The ambient dimension component.

• fibreDimension : ℕ

  The fibre dimension component.

• channelDimension : ℕ

  The channel dimension component.

• graph : HigherProjectionGraph.Data (Fin self.vertexCount) (HigherProjectionInstantiation.SpherePoint n) self.ambientDimension self.fibreDimension self.channelDimension

  The graph component.

theorem MetricCodes.Spherical.HigherHierarchy.eventually_sphericalCode_card_lt_of_eventualGraphCertificates {s R gap : ℝ} (hs' : s < 1) (hgap : 0 < gap) (stable : ℕ → Prop) (hstable : ∀ᶠ (n : ℕ) in Filter.atTop, stable n) (G : (n : ℕ) → stable n → IndexedHierarchyGraph n) (hvertex : ∀ (n : ℕ) (h : stable n), 0 < (G n h).vertexCount) (hfibre : ∀ (n : ℕ) (h : stable n), 0 < (G n h).fibreDimension) (hcorrelation : ∀ (n : ℕ) (h : stable n) (x y : HigherProjectionInstantiation.SpherePoint n), (G n h).graph.correlation x y = inner ℝ ↑x ↑y) (heigenvalue : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (h : stable n), s + gap < (G n h).graph.eigenvalue) (hdimension : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (h : stable n), (1 - s) / gap * ((∑ k : Fin (G n h).vertexCount, ↑((G n h).graph.dimension k)) / ↑(G n h).fibreDimension) < 2 ^ (R * ↑n)) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : SpherePacking.SphericalCode n s), ↑C.points.card < 2 ^ (R * ↑n)

theorem MetricCodes.Spherical.HigherHierarchy.eventually_const_mul_lt_rpow_of_logRate {q : ℕ → ℝ} {L R K : ℝ} (hq : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < q n) (hlim : Filter.Tendsto (fun (n : ℕ) => Real.log (q n) / ↑n / Real.log 2) Filter.atTop (nhds L)) (hR : L < R) (hK : 0 < K) : ∀ᶠ (n : ℕ) in Filter.atTop, K * q n < 2 ^ (R * ↑n)

theorem MetricCodes.Spherical.HigherHierarchy.eventually_const_mul_rectangularWeylQuotient_lt {r m : ℕ} {R K : ℝ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (h : Interlacing a b) (hlast : 0 < a (Fin.last (r + 1))) (hR : Phi a b < R) (hK : 0 < K) : ∀ᶠ (n : ℕ) in Filter.atTop, K * (RectangularVertices.dimensionSum a n / Weyl.dimension (n - 1) (Weyl.flooredWeight b n)) < 2 ^ (R * ↑n)

theorem MetricCodes.Spherical.HigherHierarchy.fixedLevelHierarchyCodeBound_levelZero {s R : ℝ} (hs : 0 < s) (hs' : s < 1) (a : Fin 1 → ℝ) (b : Fin 0 → ℝ) (hinterlacing : Interlacing a b) (hspectral : s < 2 * Gamma a b) (hR : Phi a b < R) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : SpherePacking.SphericalCode n s), ↑C.points.card < 2 ^ (R * ↑n)

theorem MetricCodes.Spherical.HigherHierarchy.fixedLevelHierarchyCodeBound_of_positiveTerminal (hpositive : ∀ {r : ℕ} {s R : ℝ}, 0 < s → s < 1 → ∀ (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ), Interlacing a b → 0 < a (Fin.last r) → s < 2 * Gamma a b → Phi a b < R → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : SpherePacking.SphericalCode n s), ↑C.points.card < 2 ^ (R * ↑n)) : FixedLevelHierarchyCodeBound

theorem MetricCodes.Spherical.HigherHierarchy.fixedLevelHierarchyCodeBound_of_actualRectangularGraphs (hboxes : ∀ {r : ℕ} {s R : ℝ}, 0 < s → s < 1 → ∀ (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ), Interlacing a b → 0 < a (Fin.last (r + 1)) → s < 2 * Gamma a b → Phi a b < R → ∃ (m : ℕ) (gap : ℝ) (_ : 0 < gap) (stable : ℕ → Prop) (x : DecidablePred stable) (_ : ∀ᶠ (n : ℕ) in Filter.atTop, stable n) (G : (n : ℕ) → stable n → IndexedHierarchyGraph n), (∀ (n : ℕ) (h : stable n), 0 < (G n h).vertexCount) ∧ (∀ (n : ℕ) (h : stable n), 0 < (G n h).fibreDimension) ∧ (∀ (n : ℕ) (h : stable n) (x y : HigherProjectionInstantiation.SpherePoint n), (G n h).graph.correlation x y = inner ℝ ↑x ↑y) ∧ (∀ᶠ (n : ℕ) in Filter.atTop, ∀ (h : stable n), s + gap < (G n h).graph.eigenvalue) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (h : stable n), (∑ i : Fin (G n h).vertexCount, ↑((G n h).graph.dimension i)) / ↑(G n h).fibreDimension = RectangularVertices.dimensionSum a n / Weyl.dimension (n - 1) (Weyl.flooredWeight b n)) : FixedLevelHierarchyCodeBound

@[reducible, inline]

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

The young ambient used in the spherical-code argument.

Equations

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

@[reducible, inline]

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

The young coordinate ambient used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherYoungActualGraphAssembly.coordinateInclusion {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (i : I) : TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam i) →ₗᵢ[ℝ] YoungCoordinateAmbient n lam

The tensor-product inclusion of one Young vertex into the full coordinate ambient space.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.coordinateInclusion_tmul {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (i : I) (x : SpherePacking.Euclidean n) (v : HigherYoungMovingFibres.YoungVertex lam i) : (coordinateInclusion lam i) (x ⊗ₜ[ℝ] v) = x ⊗ₜ[ℝ] (HigherYoungGraphAssembly.vertexInclusion (HigherYoungMovingFibres.YoungVertex lam) i) v

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.coordinateInclusion_orthogonal {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) {i j : I} (hij : i ≠ j) : LinearMap.adjoint (coordinateInclusion lam i).toLinearMap ∘ₗ (coordinateInclusion lam j).toLinearMap = 0

@[simp]

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.coordinateInclusion_adjoint_axis_self {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (i : I) (x : SpherePacking.Euclidean n) (v : HigherYoungMovingFibres.YoungVertex lam i) : (LinearMap.adjoint (coordinateInclusion lam i).toLinearMap) (x ⊗ₜ[ℝ] (HigherYoungGraphAssembly.vertexInclusion (HigherYoungMovingFibres.YoungVertex lam) i) v) = x ⊗ₜ[ℝ] v

@[simp]

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.coordinateInclusion_adjoint_axis_ne {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (i j : I) (hij : i ≠ j) (x : SpherePacking.Euclidean n) (v : HigherYoungMovingFibres.YoungVertex lam j) : (LinearMap.adjoint (coordinateInclusion lam i).toLinearMap) (x ⊗ₜ[ℝ] (HigherYoungGraphAssembly.vertexInclusion (HigherYoungMovingFibres.YoungVertex lam) j) v) = 0

noncomputable def MetricCodes.Spherical.HigherYoungActualGraphAssembly.liftChannel {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (target source : I) (T : HigherYoungMovingFibres.YoungVertex lam source →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam target)) : YoungAmbient n lam →ₗ[ℝ] YoungCoordinateAmbient n lam

The ambient channel obtained by projecting to a source vertex and including the target tensor space.

Equations

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

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.liftChannel_adjoint_comp_self {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (target source : I) (T : HigherYoungMovingFibres.YoungVertex lam source →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam target)) : LinearMap.adjoint (liftChannel lam target source T) ∘ₗ liftChannel lam target source T = HigherYoungGraphAssembly.vertexProjection (HigherYoungMovingFibres.YoungVertex lam) source

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.liftChannel_orthogonal_of_target_ne {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (target source target' source' : I) (T : HigherYoungMovingFibres.YoungVertex lam source →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam target)) (T' : HigherYoungMovingFibres.YoungVertex lam source' →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam target')) (hne : target ≠ target') : LinearMap.adjoint (liftChannel lam target source T) ∘ₗ liftChannel lam target' source' T' = 0

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.liftChannel_orthogonal_of_clebsch {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (target source source' : I) (T : HigherYoungMovingFibres.YoungVertex lam source →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam target)) (T' : HigherYoungMovingFibres.YoungVertex lam source' →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam target)) (horthogonal : LinearMap.adjoint T.toLinearMap ∘ₗ T'.toLinearMap = 0) : LinearMap.adjoint (liftChannel lam target source T) ∘ₗ liftChannel lam target source' T' = 0

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.liftChannel_adjoint_axis_self {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (target source : I) (T : HigherYoungMovingFibres.YoungVertex lam source →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam target)) (x : HigherProjectionInstantiation.SpherePoint n) (v : HigherYoungMovingFibres.YoungVertex lam target) : (LinearMap.adjoint (liftChannel lam target source T)) ((HigherYoungMovingFibres.axisTensor x) ((HigherYoungGraphAssembly.vertexInclusion (HigherYoungMovingFibres.YoungVertex lam) target) v)) = (HigherYoungGraphAssembly.vertexInclusion (HigherYoungMovingFibres.YoungVertex lam) source) ((LinearMap.adjoint T.toLinearMap) (↑x ⊗ₜ[ℝ] v))

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.liftChannel_adjoint_axis_ne {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (target source j : I) (T : HigherYoungMovingFibres.YoungVertex lam source →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam target)) (h : target ≠ j) (x : HigherProjectionInstantiation.SpherePoint n) (v : HigherYoungMovingFibres.YoungVertex lam j) : (LinearMap.adjoint (liftChannel lam target source T)) ((HigherYoungMovingFibres.axisTensor x) ((HigherYoungGraphAssembly.vertexInclusion (HigherYoungMovingFibres.YoungVertex lam) j) v)) = 0

noncomputable def MetricCodes.Spherical.HigherYoungActualGraphAssembly.actualYoungChannel {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} (lam : I → Fin (r + 1) → ℕ) (probability : I → I → ℝ) (edge : (target source : I) → 0 < probability target source → HigherYoungMovingFibres.YoungVertex lam source →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam target)) (target source : I) : YoungAmbient n lam →ₗ[ℝ] YoungCoordinateAmbient n lam

The lifted Young edge channel when its transition probability is positive, and zero otherwise.

Equations

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

noncomputable def MetricCodes.Spherical.HigherYoungActualGraphAssembly.actualYoungHilbertGraph {I : Type u_1} [Fintype I] [DecidableEq I] {r n : ℕ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (lam : I → Fin (r + 1) → ℕ) (o : HigherProjectionInstantiation.SpherePoint n) (base : (i : I) → E →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex lam i) (hfibre : 0 < Module.finrank ℝ E) (probability : I → I → ℝ) (hprobability : ∀ (target source : I), 0 ≤ probability target source) (hbalance : ∀ (target source : I), ↑(Module.finrank ℝ (HigherYoungMovingFibres.YoungVertex lam target)) * probability target source = ↑(Module.finrank ℝ (HigherYoungMovingFibres.YoungVertex lam source)) * probability source target) (edge : (target source : I) → 0 < probability target source → HigherYoungMovingFibres.YoungVertex lam source →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex lam target)) (horthogonal : ∀ (target source source' : I) (h : 0 < probability target source) (h' : 0 < probability target source'), source ≠ source' → LinearMap.adjoint (edge target source h).toLinearMap ∘ₗ (edge target source' h').toLinearMap = 0) (hclebsch : ∀ (target source : I) (h : 0 < probability target source) (x : HigherProjectionInstantiation.SpherePoint n) (v : E), (LinearMap.adjoint (edge target source h).toLinearMap) (↑x ⊗ₜ[ℝ] (HigherYoungMovingFibres.movingYoungFibre (lam target) o (base target) x) v) = √(probability target source) • (HigherYoungMovingFibres.movingYoungFibre (lam source) o (base source) x) v) (eigenvalue : ℝ) (heigenvalue : 0 < eigenvalue) (eigenvector : I → ℝ) (heigenvector : ∀ (i : I), 0 < eigenvector i) (heigenvector_unit : ∑ i : I, eigenvector i ^ 2 = 1) (heigenvector_equation : ∀ (i : I), ∑ j : I, √(probability i j * probability j i) * eigenvector j = eigenvalue * eigenvector i) : HigherProjectionInstantiation.RealizedHilbertGraph I (HigherProjectionInstantiation.SpherePoint n) E (YoungAmbient n lam) (YoungCoordinateAmbient n lam)

The realized Hilbert graph assembled from Young vertex fibres and their isometric edge channels.

Equations

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

noncomputable def MetricCodes.Spherical.HigherYoungActualGraphAssembly.actualYoungIndexedHierarchyGraph {k r n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (lam : Fin k → Fin (r + 1) → ℕ) (G : HigherProjectionInstantiation.RealizedHilbertGraph (Fin k) (HigherProjectionInstantiation.SpherePoint n) E (YoungAmbient n lam) (YoungCoordinateAmbient n lam)) : HigherHierarchy.IndexedHierarchyGraph n

The actual young indexed hierarchy graph used in the spherical-code argument.

Equations

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

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherYoungActualGraphAssembly.BoxIndex (r m : ℕ) : Type

The box index used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungActualGraphAssembly.BoxIndex r m = Fin (Fintype.card (MetricCodes.Spherical.HigherHierarchy.RectangularVertices.Vertex r m))

noncomputable def MetricCodes.Spherical.HigherYoungActualGraphAssembly.boxSignature {r m : ℕ} (a : Fin (r + 1) → ℝ) (n : ℕ) (i : BoxIndex r m) : Fin (r + 1) → ℕ

The box signature used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.sum_boxSignature_weyl {r m : ℕ} (a : Fin (r + 1) → ℝ) (n : ℕ) : ∑ i : BoxIndex r m, HigherHierarchy.Weyl.dimension n (boxSignature a n i) = HigherHierarchy.RectangularVertices.dimensionSum a n

theorem MetricCodes.Spherical.HigherYoungActualGraphAssembly.actualYoungBox_rankQuotient_eq_weyl {r m n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (G : HigherProjectionInstantiation.RealizedHilbertGraph (BoxIndex (r + 1) m) (HigherProjectionInstantiation.SpherePoint n) E (YoungAmbient n (boxSignature a n)) (YoungCoordinateAmbient n (boxSignature a n))) (hdimension : ∀ (i : BoxIndex (r + 1) m), G.dimension i = Module.finrank ℝ (HigherYoungMovingFibres.YoungVertex (boxSignature a n) i)) (hweyl : ∀ (i : BoxIndex (r + 1) m), HigherHierarchy.Weyl.dimension n (boxSignature a n i) = ↑(Module.finrank ℝ (HigherYoungMovingFibres.YoungVertex (boxSignature a n) i))) (hfibre : HigherHierarchy.Weyl.dimension (n - 1) (HigherHierarchy.Weyl.flooredWeight b n) = ↑(Module.finrank ℝ E)) : (∑ i : Fin (actualYoungIndexedHierarchyGraph (boxSignature a n) G).vertexCount, ↑((actualYoungIndexedHierarchyGraph (boxSignature a n) G).graph.dimension i)) / ↑(actualYoungIndexedHierarchyGraph (boxSignature a n) G).fibreDimension = HigherHierarchy.RectangularVertices.dimensionSum a n / HigherHierarchy.Weyl.dimension (n - 1) (HigherHierarchy.Weyl.flooredWeight b n)

@[reducible, inline]

noncomputable abbrev MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.BoxStabilizer {r : ℕ} (n : ℕ) (b : Fin (r + 1) → ℝ) : Submodule ℝ (HigherHarmonicYoung.PolynomialSpace r (n - 1))

The box stabilizer used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.boxProbability {r m : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (n : ℕ) (target source : HigherYoungActualGraphAssembly.BoxIndex r m) : ℝ

The box probability used in the spherical-code argument.

Equations

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

structure MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.BoxRepresentationData {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) : Type

Data encoding the box representation construction.

• axis : HigherProjectionInstantiation.SpherePoint n

  The axis component.

• stabilizer_pos : 0 < Module.finrank ℝ ↥(BoxStabilizer n b)
• stabilizer_weyl : HigherHierarchy.Weyl.dimension (n - 1) (HigherHierarchy.Weyl.flooredWeight b n) = ↑(Module.finrank ℝ ↥(BoxStabilizer n b))
• vertex_weyl (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) : HigherHierarchy.Weyl.dimension n (HigherYoungActualGraphAssembly.boxSignature a n i) = ↑(Module.finrank ℝ (HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i))
• fibre (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) : ↥(BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i

  The fibre component.

• edge (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) : 0 < boxProbability a b n target source → HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) source →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) (HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) target)

  The edge component.

• edge_orthogonal (target source source' : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (h : 0 < boxProbability a b n target source) (h' : 0 < boxProbability a b n target source') : source ≠ source' → LinearMap.adjoint (self.edge target source h).toLinearMap ∘ₗ (self.edge target source' h').toLinearMap = 0
• edge_axis (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (h : 0 < boxProbability a b n target source) (x : HigherProjectionInstantiation.SpherePoint n) (v : ↥(BoxStabilizer n b)) : (LinearMap.adjoint (self.edge target source h).toLinearMap) (↑x ⊗ₜ[ℝ] (HigherYoungMovingFibres.movingYoungFibre (HigherYoungActualGraphAssembly.boxSignature a n target) self.axis (self.fibre target) x) v) = √(boxProbability a b n target source) • (HigherYoungMovingFibres.movingYoungFibre (HigherYoungActualGraphAssembly.boxSignature a n source) self.axis (self.fibre source) x) v

theorem MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.boxProbability_nonneg {r m n : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex r m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (target source : HigherYoungActualGraphAssembly.BoxIndex r m) : 0 ≤ boxProbability a b n target source

theorem MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.BoxRepresentationData.detailed_balance {r m n : ℕ} {a : Fin (r + 2) → ℝ} {b : Fin (r + 1) → ℝ} (A : BoxRepresentationData a b) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) : ↑(Module.finrank ℝ (HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) target)) * boxProbability a b n target source = ↑(Module.finrank ℝ (HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) source)) * boxProbability a b n source target

noncomputable def MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.indexedEigenvector {r m : ℕ} (x : HigherHierarchy.RectangularVertices.Vertex r m → ℝ) (i : HigherYoungActualGraphAssembly.BoxIndex r m) : ℝ

The box eigenvector reindexed by the canonical finite enumeration of rectangular vertices.

Equations

• MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.indexedEigenvector x i = x ((Fintype.equivFin (MetricCodes.Spherical.HigherHierarchy.RectangularVertices.Vertex r m)).symm i)

theorem MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.indexedEigenvector_unit {r m : ℕ} (x : HigherHierarchy.RectangularVertices.Vertex r m → ℝ) (hx : ∑ v : HigherHierarchy.RectangularVertices.Vertex r m, x v ^ 2 = 1) : ∑ i : HigherYoungActualGraphAssembly.BoxIndex r m, indexedEigenvector x i ^ 2 = 1

theorem MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.indexedEigenvector_equation {r m n : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (eigenvalue : ℝ) (x : HigherHierarchy.RectangularVertices.Vertex r m → ℝ) (hx : ∀ (v : HigherHierarchy.RectangularVertices.Vertex r m), ∑ w : HigherHierarchy.RectangularVertices.Vertex r m, HigherHierarchyTrueGridAdjacency.matrix a b n v w * x w = eigenvalue * x v) (i : HigherYoungActualGraphAssembly.BoxIndex r m) : ∑ j : HigherYoungActualGraphAssembly.BoxIndex r m, √(boxProbability a b n i j * boxProbability a b n j i) * indexedEigenvector x j = eigenvalue * indexedEigenvector x i

structure MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.BoxPerronData {r m n : ℕ} (a : Fin (r + 1) → ℝ) (b : Fin r → ℝ) (s gap : ℝ) : Type

Data encoding the box perron construction.

• eigenvalue : ℝ

  The eigenvalue component.

• eigenvector : HigherHierarchy.RectangularVertices.Vertex r m → ℝ

  The eigenvector component.

• spectral_gap : s + gap < self.eigenvalue
• positive (v : HigherHierarchy.RectangularVertices.Vertex r m) : 0 < self.eigenvector v
• unit : ∑ v : HigherHierarchy.RectangularVertices.Vertex r m, self.eigenvector v ^ 2 = 1
• equation (v : HigherHierarchy.RectangularVertices.Vertex r m) : ∑ w : HigherHierarchy.RectangularVertices.Vertex r m, HigherHierarchyTrueGridAdjacency.matrix a b n v w * self.eigenvector w = self.eigenvalue * self.eigenvector v

noncomputable def MetricCodes.Spherical.HigherHierarchyActualBoxSufficiency.BoxRepresentationData.toHilbertGraph {r m n : ℕ} {a : Fin (r + 2) → ℝ} {b : Fin (r + 1) → ℝ} (A : BoxRepresentationData a b) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (eigenvalue : ℝ) (heigenvalue : 0 < eigenvalue) (x : HigherHierarchy.RectangularVertices.Vertex (r + 1) m → ℝ) (hx : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), 0 < x v) (hunit : ∑ v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m, x v ^ 2 = 1) (hequation : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), ∑ w : HigherHierarchy.RectangularVertices.Vertex (r + 1) m, HigherHierarchyTrueGridAdjacency.matrix a b n v w * x w = eigenvalue * x v) : HigherProjectionInstantiation.RealizedHilbertGraph (HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (HigherProjectionInstantiation.SpherePoint n) (↥(BoxStabilizer n b)) (HigherYoungActualGraphAssembly.YoungAmbient n (HigherYoungActualGraphAssembly.boxSignature a n)) (HigherYoungActualGraphAssembly.YoungCoordinateAmbient n (HigherYoungActualGraphAssembly.boxSignature a n))

The to hilbert graph used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankClebschBranchCoherence.projectedCoordinateRaise_movingFibre {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {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)) (o x : HigherProjectionInstantiation.SpherePoint n) (base : E →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (v : E) : (projectedCoordinateRaise mu lam hdeg row ↑x) ((HigherYoungMovingFibres.movingYoungFibre lam o base x) v) = (youngOrthogonalIsometry (AssociatedAxisTransport.commonAxisReflection ↑o ↑x) mu) ((projectedCoordinateRaise mu lam hdeg row ↑o) (base v))

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankClebschBranchCoherence.projectedCoordinateLower_movingFibre {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {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)) (o x : HigherProjectionInstantiation.SpherePoint n) (base : E →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (v : E) : (projectedCoordinateLower mu lam hdeg row ↑x) ((HigherYoungMovingFibres.movingYoungFibre lam o base x) v) = (youngOrthogonalIsometry (AssociatedAxisTransport.commonAxisReflection ↑o ↑x) mu) ((projectedCoordinateLower mu lam hdeg row ↑o) (base v))

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankClebschBranchCoherence.projectedCoordinateRaise_movingFibre_eq_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {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)) (o : HigherProjectionInstantiation.SpherePoint n) (source : E →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (target : E →ₗᵢ[ℝ] ↥(HarmonicYoungSpace mu)) (c : ℝ) (hbase : ∀ (v : E), (projectedCoordinateRaise mu lam hdeg row ↑o) (source v) = c • target v) (x : HigherProjectionInstantiation.SpherePoint n) (v : E) : (projectedCoordinateRaise mu lam hdeg row ↑x) ((HigherYoungMovingFibres.movingYoungFibre lam o source x) v) = c • (HigherYoungMovingFibres.movingYoungFibre mu o target x) v

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankClebschBranchCoherence.projectedCoordinateLower_movingFibre_eq_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {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)) (o : HigherProjectionInstantiation.SpherePoint n) (source : E →ₗᵢ[ℝ] ↥(HarmonicYoungSpace lam)) (target : E →ₗᵢ[ℝ] ↥(HarmonicYoungSpace mu)) (c : ℝ) (hbase : ∀ (v : E), (projectedCoordinateLower mu lam hdeg row ↑o) (source v) = c • target v) (x : HigherProjectionInstantiation.SpherePoint n) (v : E) : (projectedCoordinateLower mu lam hdeg row ↑x) ((HigherYoungMovingFibres.movingYoungFibre lam o source x) v) = c • (HigherYoungMovingFibres.movingYoungFibre mu o target x) v

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.precedingRows {r : ℕ} (row : Fin (r + 1)) : Finset (Fin (r + 1))

The preceding rows used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.precedingRows row = {i : Fin (r + 1) | i < row}

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.mem_precedingRows {r : ℕ} (i row : Fin (r + 1)) : i ∈ precedingRows row ↔ i < row

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.shiftedRowGap {r : ℕ} (lam : Fin (r + 1) → ℕ) (row i : Fin (r + 1)) : ℝ

The shifted row gap used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.shiftedRowGap lam row i = ↑(lam i - lam row) + ↑(↑row - ↑i - 1)

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.arbitraryRowLeadingScalar {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : ℝ

The arbitrary row leading scalar used in the spherical-code argument.

Equations

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

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.lowerPolarizationPath {r n : ℕ} : List (Fin (r + 1)) → PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The lower polarization path used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.
• MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.lowerPolarizationPath [] = LinearMap.id
• MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.lowerPolarizationPath [head] = LinearMap.id

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.polarizationPathStart {r : ℕ} (row : Fin (r + 1)) (S : Finset (Fin (r + 1))) : Fin (r + 1)

The polarization path start used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.polarizationPathStart row S = if h : S.Nonempty then S.min' h else row

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.polarizationPathCoefficient {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (S : Finset (Fin (r + 1))) : ℝ

The polarization path coefficient used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) : PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The arbitrary row axial 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.AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise_apply {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) : (arbitraryRowAxialRaise lam row k) p = ∑ S ∈ (precedingRows row).powerset, polarizationPathCoefficient lam row S • (MvPolynomial.X (variableIndex (polarizationPathStart row S) k) * (lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])) p)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.polarizationPathStart_empty {r : ℕ} (row : Fin (r + 1)) : polarizationPathStart row ∅ = row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.polarizationPathStart_lt_of_nonempty {r : ℕ} (row : Fin (r + 1)) (S : Finset (Fin (r + 1))) (hS : S.Nonempty) (hsub : S ⊆ precedingRows row) : polarizationPathStart row S < row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.shiftedRowGap_pos {r : ℕ} (lam : Fin (r + 1) → ℕ) (row i : Fin (r + 1)) (hi : i < row) (hstrict : ∀ (j : Fin (r + 1)), ↑j + 1 = ↑row → lam row < lam j) : 0 < shiftedRowGap lam row i

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.arbitraryRowLeadingScalar_pos {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hstrict : ∀ (j : Fin (r + 1)), ↑j + 1 = ↑row → lam row < lam j) : 0 < arbitraryRowLeadingScalar lam row

def MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) : ℕ

The interlacing gap used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap lam mu row = lam row - MetricCodes.Spherical.ThreeRowYoungBranching.appendZeroWeight mu row

theorem MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingGapSchedule.appendZeroWeight_le_of_interlaces {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) (row : Fin (r + 2)) : ThreeRowYoungBranching.appendZeroWeight mu row ≤ lam row

theorem MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingGapSchedule.appendZeroWeight_add_interlacingGap {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) (row : Fin (r + 2)) : ThreeRowYoungBranching.appendZeroWeight mu row + interlacingGap lam mu row = lam row

theorem MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingGapSchedule.interlaces_of_between_appendZero_and_target {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) (theta : Fin (r + 2) → ℕ) (hlower : ∀ (row : Fin (r + 2)), ThreeRowYoungBranching.appendZeroWeight mu row ≤ theta row) (hupper : ∀ (row : Fin (r + 2)), theta row ≤ lam row) : HigherRepresentationGraph.Interlaces theta mu

def MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingGapSchedule.interlacingRowSchedule {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) : List (Fin (r + 2))

The interlacing row schedule used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingGapSchedule.foldl_raiseWeight_apply {r : ℕ} (rows : List (Fin (r + 2))) (weight : Fin (r + 2) → ℕ) (row : Fin (r + 2)) : List.foldl (fun (w : Fin (r + 1 + 1) → ℕ) (i : Fin (r + 1 + 1)) => HigherChannel.raiseWeight w i) weight rows row = weight row + List.count row rows

theorem MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingGapSchedule.interlacingRowSchedule_count {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) : List.count row (interlacingRowSchedule lam mu) = interlacingGap lam mu row

theorem MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingLegalSchedule.foldl_interlaces_of_count_le_gap {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) (rows : List (Fin (r + 2))) (hrows : ∀ (row : Fin (r + 2)), List.count row rows ≤ HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap lam mu row) : HigherRepresentationGraph.Interlaces (List.foldl (fun (weight : HigherRepresentationGraph.AmbientWeight (r + 1)) (row : Fin (r + 1 + 1)) => HigherChannel.raiseWeight weight row) (ThreeRowYoungBranching.appendZeroWeight mu) rows) mu

theorem MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingLegalSchedule.foldl_strict_predecessor_of_count_lt_gap {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) (rows : List (Fin (r + 2))) (hrows : ∀ (row : Fin (r + 2)), List.count row rows ≤ HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap lam mu row) (row j : Fin (r + 2)) (hrow : List.count row rows < HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap lam mu row) (hj : ↑j + 1 = ↑row) : List.foldl (fun (weight : Fin (r + 1 + 1) → ℕ) (i : Fin (r + 1 + 1)) => HigherChannel.raiseWeight weight i) (ThreeRowYoungBranching.appendZeroWeight mu) rows row < List.foldl (fun (weight : Fin (r + 1 + 1) → ℕ) (i : Fin (r + 1 + 1)) => HigherChannel.raiseWeight weight i) (ThreeRowYoungBranching.appendZeroWeight mu) rows j

theorem MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingLegalSchedule.foldl_arbitraryRowLeadingScalar_pos_of_count_lt_gap {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) (rows : List (Fin (r + 2))) (hrows : ∀ (row : Fin (r + 2)), List.count row rows ≤ HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap lam mu row) (row : Fin (r + 2)) (hrow : List.count row rows < HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap lam mu row) : 0 < HigherHarmonicYoung.AllRankArbitraryRowBranchingOperator.arbitraryRowLeadingScalar (List.foldl (fun (weight : Fin (r + 1 + 1) → ℕ) (i : Fin (r + 1 + 1)) => HigherChannel.raiseWeight weight i) (ThreeRowYoungBranching.appendZeroWeight mu) rows) row

def MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) : List (Fin (r + 2))

The reverse interlacing row schedule used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule_count {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) : List.count row (reverseInterlacingRowSchedule lam mu) = HigherYoungArbitraryRankInterlacingGapSchedule.interlacingGap lam mu row

theorem MetricCodes.Spherical.HigherYoungArbitraryRankInterlacingLegalSchedule.foldl_reverseInterlacingRowSchedule_eq_target {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) : List.foldl (fun (weight : Fin (r + 1 + 1) → ℕ) (row : Fin (r + 1 + 1)) => HigherChannel.raiseWeight weight row) (ThreeRowYoungBranching.appendZeroWeight mu) (reverseInterlacingRowSchedule lam mu) = lam

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

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.UpperGramPair (r : ℕ) : Type

The upper gram pair used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.UpperGramPair r = { z : Fin (r + 1) × Fin (r + 1) // z.1 ≤ z.2 }

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPairPolynomial {r : ℕ} (n : ℕ) (z : UpperGramPair r) : PolynomialSpace r n

The gram pair polynomial used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPairPolynomial n z = MetricCodes.Spherical.HigherHarmonicYoung.rowPairingPolynomial (↑z).1 (↑z).2

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramQuadraticList (r n : ℕ) : List (PolynomialSpace r n)

The gram quadratic list used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPriorIdeal (r n k : ℕ) : Ideal (PolynomialSpace r n)

The gram prior ideal used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.mem_ideal_smul_top_iff {R : Type u_1} [CommRing R] (I : Ideal R) (p : R) : p ∈ I • ⊤ ↔ p ∈ I

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramQuadraticList_weaklyRegular_iff_saturation (r n : ℕ) : RingTheory.Sequence.IsWeaklyRegular (PolynomialSpace r n) (gramQuadraticList r n) ↔ ∀ (k : Fin (gramQuadraticList r n).length) (p : PolynomialSpace r n), (gramQuadraticList r n)[k] * p ∈ gramPriorIdeal r n ↑k → p ∈ gramPriorIdeal r n ↑k

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivot {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) : Fin n

The gram pivot used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivot hn z = ⟨↑(↑z).1 + ↑(↑z).2, ⋯⟩

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivot_val {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) : ↑(gramPivot hn z) = ↑(↑z).1 + ↑(↑z).2

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivotVariables {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) : Finset (Fin ((r + 1) * n))

The gram pivot variables used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivot_pair_eq_of_variable_eq {r n : ℕ} (hn : 2 * r < n) (z w : UpperGramPair r) (a b : Fin (r + 1)) (ha : a = (↑z).1 ∨ a = (↑z).2) (hb : b = (↑w).1 ∨ b = (↑w).2) (h : variableIndex a (gramPivot hn z) = variableIndex b (gramPivot hn w)) : z = w

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivotVariables_disjoint {r n : ℕ} (hn : 2 * r < n) (z w : UpperGramPair r) (hzw : z ≠ w) : Disjoint (gramPivotVariables hn z) (gramPivotVariables hn w)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivotExponent {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) : Fin ((r + 1) * n) →₀ ℕ

The gram pivot exponent used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramSummandExponent {r n : ℕ} (z : UpperGramPair r) (k : Fin n) : Fin ((r + 1) * n) →₀ ℕ

The monomial exponent of one coordinate summand in a Gram pairing.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramSummandExponent_support {r n : ℕ} (z : UpperGramPair r) (k : Fin n) : (gramSummandExponent z k).support = {variableIndex (↑z).1 k, variableIndex (↑z).2 k}

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivotExponent_support {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) : (gramPivotExponent hn z).support = gramPivotVariables hn z

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivotExponent_support_disjoint {r n : ℕ} (hn : 2 * r < n) (z w : UpperGramPair r) (hzw : z ≠ w) : Disjoint (gramPivotExponent hn z).support (gramPivotExponent hn w).support

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramSummandExponent_eq_pivot_iff {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) (k : Fin n) : gramSummandExponent z k = gramPivotExponent hn z ↔ k = gramPivot hn z

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.coeff_gramPairPolynomial_pivot {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) : (gramPairPolynomial n z).coeff (gramPivotExponent hn z) = 1

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableWeight (r n : ℕ) (i : Fin (r + 1)) (k : Fin n) : ℤ

The quadratic integer variable weight used to distinguish the leading Gram monomial.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableWeight r n i k = ↑(n + 2 * r) ^ 2 - (↑↑k - 2 * ↑↑i) ^ 2

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramSummandWeight {r n : ℕ} (z : UpperGramPair r) (k : Fin n) : ℤ

The sum of the two variable weights in a coordinate summand of a Gram pairing.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivot_weight_sub {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) (k : Fin n) : gramSummandWeight z (gramPivot hn z) - gramSummandWeight z k = 2 * (↑↑k - (↑↑(↑z).1 + ↑↑(↑z).2)) ^ 2

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivot_unique_max_weight {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) (k : Fin n) (hk : k ≠ gramPivot hn z) : gramSummandWeight z k < gramSummandWeight z (gramPivot hn z)

def MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex {σ : Type u_1} (_w : σ → ℕ) : Type u_1

A copy of exponent vectors carrying the weighted lexicographic ordering.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex _w = (σ →₀ ℕ)

def MetricCodes.Spherical.HigherHarmonicYoung.toYoungWeightedLex {σ : Type u_1} (w : σ → ℕ) : (σ →₀ ℕ) ≃ YoungWeightedLex w

The identity equivalence from exponent vectors to their weighted-lexicographic copy.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.toYoungWeightedLex w = Equiv.refl (σ →₀ ℕ)

def MetricCodes.Spherical.HigherHarmonicYoung.ofYoungWeightedLex {σ : Type u_1} (w : σ → ℕ) : YoungWeightedLex w ≃ (σ →₀ ℕ)

The identity equivalence from the weighted-lexicographic copy back to exponent vectors.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.ofYoungWeightedLex w = Equiv.refl (MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex w)

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.instAddCommMonoidYoungWeightedLex {σ : Type u_1} (w : σ → ℕ) : AddCommMonoid (YoungWeightedLex w)

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.instAddCommMonoidYoungWeightedLex w = (MetricCodes.Spherical.HigherHarmonicYoung.ofYoungWeightedLex w).addCommMonoid

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.toYoungWeightedLex_add {σ : Type u_1} (w : σ → ℕ) (a b : σ →₀ ℕ) : (toYoungWeightedLex w) (a + b) = (toYoungWeightedLex w) a + (toYoungWeightedLex w) b

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.ofYoungWeightedLex_add {σ : Type u_1} (w : σ → ℕ) (a b : YoungWeightedLex w) : (ofYoungWeightedLex w) (a + b) = (ofYoungWeightedLex w) a + (ofYoungWeightedLex w) b

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.key {σ : Type u_1} (w : σ → ℕ) (a : YoungWeightedLex w) : Lex (ℕ × Lex (σ →₀ ℕ))

The lexicographic key comparing total weight first and then the exponent vector.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.key_injective_metriccodes2_a7f44027 {σ : Type u_1} (w : σ → ℕ) : Function.Injective (key w)

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.instLinearOrderYoungWeightedLex {σ : Type u_1} (w : σ → ℕ) [LinearOrder σ] : LinearOrder (YoungWeightedLex w)

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.instLinearOrderYoungWeightedLex w = LinearOrder.lift' (MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.key w) ⋯

theorem MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.lt_iff {σ : Type u_1} (w : σ → ℕ) [LinearOrder σ] {a b : YoungWeightedLex w} : a < b ↔ (Finsupp.weight w) ((ofYoungWeightedLex w) a) < (Finsupp.weight w) ((ofYoungWeightedLex w) b) ∨ (Finsupp.weight w) ((ofYoungWeightedLex w) a) = (Finsupp.weight w) ((ofYoungWeightedLex w) b) ∧ toLex ((ofYoungWeightedLex w) a) < toLex ((ofYoungWeightedLex w) b)

theorem MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.le_iff {σ : Type u_1} (w : σ → ℕ) [LinearOrder σ] {a b : YoungWeightedLex w} : a ≤ b ↔ (Finsupp.weight w) ((ofYoungWeightedLex w) a) < (Finsupp.weight w) ((ofYoungWeightedLex w) b) ∨ (Finsupp.weight w) ((ofYoungWeightedLex w) a) = (Finsupp.weight w) ((ofYoungWeightedLex w) b) ∧ toLex ((ofYoungWeightedLex w) a) ≤ toLex ((ofYoungWeightedLex w) b)

instance MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.instIsOrderedCancelAddMonoidYoungWeightedLex {σ : Type u_1} (w : σ → ℕ) [LinearOrder σ] : IsOrderedCancelAddMonoid (YoungWeightedLex w)

instance MetricCodes.Spherical.HigherHarmonicYoung.YoungWeightedLex.instWellFoundedLTYoungWeightedLex {σ : Type u_1} (w : σ → ℕ) [LinearOrder σ] [WellFoundedGT σ] : WellFoundedLT (YoungWeightedLex w)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.weightedMonomialOrder {σ : Type u_1} [LinearOrder σ] [WellFoundedGT σ] (w : σ → ℕ) : MonomialOrder σ

The weighted monomial order used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.weightedMonomialOrder_lt_iff {σ : Type u_1} [LinearOrder σ] [WellFoundedGT σ] (w : σ → ℕ) (a b : σ →₀ ℕ) : (weightedMonomialOrder w).toSyn a < (weightedMonomialOrder w).toSyn b ↔ (Finsupp.weight w) a < (Finsupp.weight w) b ∨ (Finsupp.weight w) a = (Finsupp.weight w) b ∧ toLex a < toLex b

theorem MetricCodes.Spherical.HigherHarmonicYoung.weightedMonomialOrder_lt_of_weight_lt {σ : Type u_1} [LinearOrder σ] [WellFoundedGT σ] {w : σ → ℕ} {a b : σ →₀ ℕ} (h : (Finsupp.weight w) a < (Finsupp.weight w) b) : (weightedMonomialOrder w).toSyn a < (weightedMonomialOrder w).toSyn b

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableWeight_nonneg {r n : ℕ} (i : Fin (r + 1)) (k : Fin n) : 0 ≤ gramVariableWeight r n i k

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableNatWeight (r n : ℕ) (a : Fin ((r + 1) * n)) : ℕ

The gram variable nat weight used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramVariableNatWeight_variableIndex {r n : ℕ} (i : Fin (r + 1)) (k : Fin n) : gramVariableNatWeight r n (variableIndex i k) = (gramVariableWeight r n i k).toNat

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramSummandExponent_natWeight {r n : ℕ} (z : UpperGramPair r) (k : Fin n) : (Finsupp.weight (gramVariableNatWeight r n)) (gramSummandExponent z k) = (gramSummandWeight z k).toNat

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPivot_unique_max_natWeight {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) (k : Fin n) (hk : k ≠ gramPivot hn z) : (Finsupp.weight (gramVariableNatWeight r n)) (gramSummandExponent z k) < (Finsupp.weight (gramVariableNatWeight r n)) (gramPivotExponent hn z)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPairPolynomial_support_exponent {r n : ℕ} (z : UpperGramPair r) {d : Fin ((r + 1) * n) →₀ ℕ} (hd : d ∈ MvPolynomial.support (gramPairPolynomial n z)) : ∃ (k : Fin n), d = gramSummandExponent z k

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPairPolynomial_weighted_degree {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) : (weightedMonomialOrder (gramVariableNatWeight r n)).degree (gramPairPolynomial n z) = gramPivotExponent hn z

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPairPolynomial_weighted_leadingCoeff {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) : (weightedMonomialOrder (gramVariableNatWeight r n)).leadingCoeff (gramPairPolynomial n z) = 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPairPolynomial_weighted_monic {r n : ℕ} (hn : 2 * r < n) (z : UpperGramPair r) : (weightedMonomialOrder (gramVariableNatWeight r n)).Monic (gramPairPolynomial n z)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.gramPairPolynomial_weighted_degree_support_disjoint {r n : ℕ} (hn : 2 * r < n) (z w : UpperGramPair r) (hzw : z ≠ w) : Disjoint ((weightedMonomialOrder (gramVariableNatWeight r n)).degree (gramPairPolynomial n z)).support ((weightedMonomialOrder (gramVariableNatWeight r n)).degree (gramPairPolynomial n w)).support

theorem MetricCodes.Spherical.HigherHarmonicYoung.finsupp_sup_eq_add_of_disjoint_support {σ : Type u_1} (a b : σ →₀ ℕ) (h : Disjoint a.support b.support) : a ⊔ b = a + b

theorem MetricCodes.Spherical.HigherHarmonicYoung.coprime_sPolynomial_eq {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (f g : MvPolynomial σ K) (hf : m.Monic f) (hg : m.Monic g) (h : Disjoint (m.degree f).support (m.degree g).support) : m.sPolynomial f g = (m.leadingTerm g - g) * f + (f - m.leadingTerm f) * g

theorem MetricCodes.Spherical.HigherHarmonicYoung.coprime_sPolynomial_left_product_lt {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (f g : MvPolynomial σ K) (hf : m.Monic f) (hterm : (m.leadingTerm g - g) * f ≠ 0) : m.toSyn (m.degree ((m.leadingTerm g - g) * f)) < m.toSyn (m.degree f + m.degree g)

theorem MetricCodes.Spherical.HigherHarmonicYoung.coprime_sPolynomial_right_product_lt {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (f g : MvPolynomial σ K) (hg : m.Monic g) (hterm : (f - m.leadingTerm f) * g ≠ 0) : m.toSyn (m.degree ((f - m.leadingTerm f) * g)) < m.toSyn (m.degree f + m.degree g)

theorem MetricCodes.Spherical.HigherHarmonicYoung.coprime_sPolynomial_monomial_left_product_lt {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (f g : MvPolynomial σ K) (hf : m.Monic f) (c : σ →₀ ℕ) (a : K) (hterm : (MvPolynomial.monomial c) a * ((m.leadingTerm g - g) * f) ≠ 0) : m.toSyn (m.degree ((MvPolynomial.monomial c) a * ((m.leadingTerm g - g) * f))) < m.toSyn (c + m.degree f + m.degree g)

theorem MetricCodes.Spherical.HigherHarmonicYoung.coprime_sPolynomial_monomial_right_product_lt {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (f g : MvPolynomial σ K) (hg : m.Monic g) (c : σ →₀ ℕ) (a : K) (hterm : (MvPolynomial.monomial c) a * ((f - m.leadingTerm f) * g) ≠ 0) : m.toSyn (m.degree ((MvPolynomial.monomial c) a * ((f - m.leadingTerm f) * g))) < m.toSyn (c + m.degree f + m.degree g)

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.mem_ofList_iff_exists_linearCombination {σ : Type u_1} {K : Type u_2} [Field K] (fs : List (MvPolynomial σ K)) (p : MvPolynomial σ K) : p ∈ Ideal.ofList fs ↔ ∃ (g : { f : MvPolynomial σ K // f ∈ fs } →₀ MvPolynomial σ K), (Finsupp.linearCombination (MvPolynomial σ K) fun (f : { f : MvPolynomial σ K // f ∈ fs }) => ↑f) g = p

noncomputable def MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.representationDegree {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (g : ι →₀ MvPolynomial σ K) : m.syn

The maximum monomial-order degree of the summands in a finitely supported polynomial representation.

Equations

• MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.representationDegree m b g = g.support.sup fun (i : ι) => m.toSyn (m.degree (b i * g i))

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.degree_mul_le_representationDegree {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (g : ι →₀ MvPolynomial σ K) (i : ι) (hi : g i ≠ 0) : m.toSyn (m.degree (b i * g i)) ≤ representationDegree m b g

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.degree_mul_le_representationDegree_all {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (g : ι →₀ MvPolynomial σ K) (i : ι) : m.toSyn (m.degree (b i * g i)) ≤ representationDegree m b g

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.exists_minimalRepresentation {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (p : MvPolynomial σ K) (hrep : ∃ (g : ι →₀ MvPolynomial σ K), (Finsupp.linearCombination (MvPolynomial σ K) b) g = p) : ∃ (g : ι →₀ MvPolynomial σ K), (Finsupp.linearCombination (MvPolynomial σ K) b) g = p ∧ ∀ (h : ι →₀ MvPolynomial σ K), (Finsupp.linearCombination (MvPolynomial σ K) b) h = p → representationDegree m b g ≤ representationDegree m b h

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.degree_linearCombination_le_representationDegree {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (g : ι →₀ MvPolynomial σ K) : m.toSyn (m.degree ((Finsupp.linearCombination (MvPolynomial σ K) b) g)) ≤ representationDegree m b g

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.representationDegree_add_le {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (g h : ι →₀ MvPolynomial σ K) : representationDegree m b (g + h) ≤ max (representationDegree m b g) (representationDegree m b h)

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.representationDegree_lt_of_forall {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (g : ι →₀ MvPolynomial σ K) (d : m.syn) (hd : ⊥ < d) (hterm : ∀ (i : ι), g i ≠ 0 → m.toSyn (m.degree (b i * g i)) < d) : representationDegree m b g < d

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.representationDegree_sum_lt {σ : Type u_1} {K : Type u_2} {ι : Type u_3} {α : Type u_4} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (s : Finset α) (g : α → ι →₀ MvPolynomial σ K) (d : m.syn) (hd : ⊥ < d) (hterm : ∀ a ∈ s, representationDegree m b (g a) < d) : representationDegree m b (∑ a ∈ s, g a) < d

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.representationDegree_sum_sum_lt {σ : Type u_1} {K : Type u_2} {ι : Type u_3} {α : Type u_4} {β : Type u_5} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (s : Finset α) (t : Finset β) (g : α → β → ι →₀ MvPolynomial σ K) (d : m.syn) (hd : ⊥ < d) (hterm : ∀ a ∈ s, ∀ a' ∈ t, representationDegree m b (g a a') < d) : representationDegree m b (∑ a ∈ s, ∑ a' ∈ t, g a a') < d

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.representationDegree_add_sum_sum_lt {σ : Type u_1} {K : Type u_2} {ι : Type u_3} {α : Type u_4} {β : Type u_5} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (r : ι →₀ MvPolynomial σ K) (s : Finset α) (t : Finset β) (g : α → β → ι →₀ MvPolynomial σ K) (d : m.syn) (hd : ⊥ < d) (hr : representationDegree m b r < d) (hterm : ∀ a ∈ s, ∀ a' ∈ t, representationDegree m b (g a a') < d) : representationDegree m b (r + ∑ a ∈ s, ∑ a' ∈ t, g a a') < d

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.representationDegree_single_lt {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (i : ι) (x : MvPolynomial σ K) (d : m.syn) (hd : ⊥ < d) (hx : b i * x = 0 ∨ m.toSyn (m.degree (b i * x)) < d) : representationDegree m b (Finsupp.single i x) < d

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.representationDegree_pair_lt {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (i j : ι) (x y : MvPolynomial σ K) (d : m.syn) (hd : ⊥ < d) (hx : b i * x = 0 ∨ m.toSyn (m.degree (b i * x)) < d) (hy : b j * y = 0 ∨ m.toSyn (m.degree (b j * y)) < d) : representationDegree m b (Finsupp.single i x + Finsupp.single j y) < d

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.exists_topRepresentationIndex {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (g : ι →₀ MvPolynomial σ K) (hg : g ≠ 0) : ∃ (i : ι), g i ≠ 0 ∧ m.toSyn (m.degree (b i * g i)) = representationDegree m b g

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.exists_topRepresentationIndex_of_ne_zero {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (p : MvPolynomial σ K) (g : ι →₀ MvPolynomial σ K) (hrep : (Finsupp.linearCombination (MvPolynomial σ K) b) g = p) (hp : p ≠ 0) : ∃ (i : ι), g i ≠ 0 ∧ m.toSyn (m.degree (b i * g i)) = representationDegree m b g

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.exists_degree_le_of_representationImprovement {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (hb : ∀ (i : ι), b i ≠ 0) (p : MvPolynomial σ K) (hp : p ≠ 0) (hrep : ∃ (g : ι →₀ MvPolynomial σ K), (Finsupp.linearCombination (MvPolynomial σ K) b) g = p) (himprove : ∀ (g : ι →₀ MvPolynomial σ K), (Finsupp.linearCombination (MvPolynomial σ K) b) g = p → m.toSyn (m.degree p) < representationDegree m b g → ∃ (h : ι →₀ MvPolynomial σ K), (Finsupp.linearCombination (MvPolynomial σ K) b) h = p ∧ representationDegree m b h < representationDegree m b g) : ∃ (i : ι), m.degree (b i) ≤ m.degree p

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.top_leading_multiple_sPolynomial_decomposition {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (B : Finset ι) (b q : ι → MvPolynomial σ K) (d : m.syn) (hd : ∀ i ∈ B, m.toSyn (m.degree (m.leadingTerm (q i) * b i)) = d ∨ m.leadingTerm (q i) * b i = 0) (hsum : m.toSyn (m.degree (∑ i ∈ B, m.leadingTerm (q i) * b i)) < d) : ∃ (c : ι → ι → K), ∑ i ∈ B, m.leadingTerm (q i) * b i = ∑ i ∈ B, ∑ j ∈ B, c i j • ((MvPolynomial.monomial (m.degree (q i * b i) ⊔ m.degree (q j * b j) - m.degree (b i) ⊔ m.degree (b j))) (m.leadingCoeff (q i) * m.leadingCoeff (q j)) * m.sPolynomial (b i) (b j))

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.top_leadingTerm_sum_degree_lt {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] [DecidableEq σ] (m : MonomialOrder σ) (b g : ι → MvPolynomial σ K) (s : Finset ι) (D : σ →₀ ℕ) (hbound : ∀ i ∈ s, m.toSyn (m.degree (b i * g i)) ≤ m.toSyn D) (htotal : m.toSyn (m.degree (∑ i ∈ s, b i * g i)) < m.toSyn D) : m.toSyn (m.degree (∑ i ∈ s with m.degree (b i * g i) = D, m.leadingTerm (g i) * b i)) < m.toSyn D

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.linearCombination_top_reassembly {R : Type u_1} {ι : Type u_2} [CommRing R] (b : ι → R) (g : ι →₀ R) (B : Finset ι) (u : ι → R) (v w : ι → ι → R) (hreplace : ∑ i ∈ B, u i * b i = ∑ i ∈ B, ∑ j ∈ B, (v i j * b i + w i j * b j)) : (Finsupp.linearCombination R b) (g - ∑ i ∈ B, Finsupp.single i (u i) + ∑ i ∈ B, ∑ j ∈ B, (Finsupp.single i (v i j) + Finsupp.single j (w i j))) = (Finsupp.linearCombination R b) g

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.linearCombination_buchberger_reassembly {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (g : ι →₀ MvPolynomial σ K) (B : Finset ι) (c : ι → ι → K) (P : ι → ι → MvPolynomial σ K) (hreplace : ∑ i ∈ B, m.leadingTerm (g i) * b i = ∑ i ∈ B, ∑ j ∈ B, c i j • (P i j * ((m.leadingTerm (b j) - b j) * b i + (b i - m.leadingTerm (b i)) * b j))) : (Finsupp.linearCombination (MvPolynomial σ K) b) (g - ∑ i ∈ B, Finsupp.single i (m.leadingTerm (g i)) + ∑ i ∈ B, ∑ j ∈ B, (Finsupp.single i (c i j • (P i j * (m.leadingTerm (b j) - b j))) + Finsupp.single j (c i j • (P i j * (b i - m.leadingTerm (b i)))))) = (Finsupp.linearCombination (MvPolynomial σ K) b) g

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.representationDegree_strip_top_leading_terms_lt {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (g : ι →₀ MvPolynomial σ K) (B : Finset ι) (d : m.syn) (hd : ⊥ < d) (hb : ∀ (i : ι), b i ≠ 0) (hbound : ∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ d) (hB : ∀ (i : ι), i ∈ B ↔ g i ≠ 0 ∧ m.toSyn (m.degree (b i * g i)) = d) : representationDegree m b (g - ∑ i ∈ B, Finsupp.single i (m.leadingTerm (g i))) < d

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.buchberger_representation_improvement {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (hmonic : ∀ (i : ι), m.Monic (b i)) (hdisjoint : ∀ (i j : ι), i ≠ j → Disjoint (m.degree (b i)).support (m.degree (b j)).support) (g : ι →₀ MvPolynomial σ K) (p : MvPolynomial σ K) (hrep : (Finsupp.linearCombination (MvPolynomial σ K) b) g = p) (hbad : m.toSyn (m.degree p) < representationDegree m b g) (hresidual : representationDegree m b (g - ∑ i ∈ g.support with m.toSyn (m.degree (b i * g i)) = representationDegree m b g, Finsupp.single i (m.leadingTerm (g i))) < representationDegree m b g) : ∃ (g' : ι →₀ MvPolynomial σ K), (Finsupp.linearCombination (MvPolynomial σ K) b) g' = p ∧ representationDegree m b g' < representationDegree m b g

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.buchberger_representation_improvement_of_monic {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (m : MonomialOrder σ) (b : ι → MvPolynomial σ K) (hmonic : ∀ (i : ι), m.Monic (b i)) (hdisjoint : ∀ (i j : ι), i ≠ j → Disjoint (m.degree (b i)).support (m.degree (b j)).support) (g : ι →₀ MvPolynomial σ K) (p : MvPolynomial σ K) (hrep : (Finsupp.linearCombination (MvPolynomial σ K) b) g = p) (hbad : m.toSyn (m.degree p) < representationDegree m b g) : ∃ (g' : ι →₀ MvPolynomial σ K), (Finsupp.linearCombination (MvPolynomial σ K) b) g' = p ∧ representationDegree m b g' < representationDegree m b g

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingBuchberger.pairwise_coprime_monic_leadingDivisibility {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (fs : List (MvPolynomial σ K)) (hmonic : ∀ f ∈ fs, m.Monic f) (hdisjoint : List.Pairwise (fun (f g : MvPolynomial σ K) => Disjoint (m.degree f).support (m.degree g).support) fs) (p : MvPolynomial σ K) : p ∈ Ideal.ofList fs → p ≠ 0 → ∃ f ∈ fs, m.degree f ≤ m.degree p

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingRegularSequence.finsupp_le_add_of_disjoint_support {σ : Type u_1} {a b c : σ →₀ ℕ} (hdisjoint : Disjoint a.support b.support) (hle : a ≤ b + c) : a ≤ c

def MetricCodes.Spherical.HigherYoungCoprimeLeadingRegularSequence.IsLeadingGroebnerFamily {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (fs : List (MvPolynomial σ K)) : Prop

The leading-degree condition that every nonzero ideal element has degree above some generator.

Equations

• MetricCodes.Spherical.HigherYoungCoprimeLeadingRegularSequence.IsLeadingGroebnerFamily m fs = ∀ p ∈ Ideal.ofList fs, p ≠ 0 → ∃ f ∈ fs, m.degree f ≤ m.degree p

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingRegularSequence.linearCombination_mem_ofList {σ : Type u_1} {K : Type u_2} {ι : Type u_3} [Field K] (fs : List (MvPolynomial σ K)) (b : ι → MvPolynomial σ K) (hb : ∀ (i : ι), b i ∈ fs) (g : ι →₀ MvPolynomial σ K) : (Finsupp.linearCombination (MvPolynomial σ K) b) g ∈ Ideal.ofList fs

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingRegularSequence.mem_of_mul_mem_of_disjoint_leading {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (fs : List (MvPolynomial σ K)) (hmonic : ∀ g ∈ fs, m.Monic g) (hgroebner : IsLeadingGroebnerFamily m fs) (f : MvPolynomial σ K) (hf : m.Monic f) (hdisjoint : ∀ g ∈ fs, Disjoint (m.degree g).support (m.degree f).support) (p : MvPolynomial σ K) (hp : f * p ∈ Ideal.ofList fs) : p ∈ Ideal.ofList fs

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingRegularSequence.mem_ideal_smul_top_iff {R : Type u_1} [CommRing R] (I : Ideal R) (p : R) : p ∈ I • ⊤ ↔ p ∈ I

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingRegularSequence.mem_of_X_mul_mem_of_avoids_leading_support {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (fs : List (MvPolynomial σ K)) (hmonic : ∀ g ∈ fs, m.Monic g) (hgroebner : IsLeadingGroebnerFamily m fs) (i : σ) (havoid : ∀ g ∈ fs, i ∉ (m.degree g).support) (p : MvPolynomial σ K) (hp : MvPolynomial.X i * p ∈ Ideal.ofList fs) : p ∈ Ideal.ofList fs

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingRegularSequence.isWeaklyRegular_of_leadingGroebner_prefix {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (fs : List (MvPolynomial σ K)) (hmonic : ∀ f ∈ fs, m.Monic f) (hpairwise : List.Pairwise (fun (f g : MvPolynomial σ K) => Disjoint (m.degree f).support (m.degree g).support) fs) (hgroebner : ∀ (k : Fin fs.length), IsLeadingGroebnerFamily m (List.take (↑k) fs)) : RingTheory.Sequence.IsWeaklyRegular (MvPolynomial σ K) fs

theorem MetricCodes.Spherical.HigherYoungCoprimeLeadingRegularSequence.isWeaklyRegular_of_pairwise_disjoint_monic_leading {σ : Type u_1} {K : Type u_2} [Field K] (m : MonomialOrder σ) (fs : List (MvPolynomial σ K)) (hmonic : ∀ f ∈ fs, m.Monic f) (hpairwise : List.Pairwise (fun (f g : MvPolynomial σ K) => Disjoint (m.degree f).support (m.degree g).support) fs) : RingTheory.Sequence.IsWeaklyRegular (MvPolynomial σ K) fs

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramQuadraticList_ideal_eq_youngGramRadialIdeal (r n : ℕ) : Ideal.ofList (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n) = youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramQuadraticList_weighted_monic {r n : ℕ} (hn : 2 * r < n) (p : PolynomialSpace r n) (hp : p ∈ ArbitraryRankMixedTraceRegularity.gramQuadraticList r n) : (weightedMonomialOrder (ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r n)).Monic p

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramQuadraticList_weighted_degree_pairwise_disjoint {r n : ℕ} (hn : 2 * r < n) : List.Pairwise (fun (p q : MvPolynomial (Fin ((r + 1) * n)) ℝ) => Disjoint ((weightedMonomialOrder (ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r n)).degree p).support ((weightedMonomialOrder (ArbitraryRankMixedTraceRegularity.gramVariableNatWeight r n)).degree q).support) (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)

theorem MetricCodes.Spherical.HigherHarmonicYoung.gramQuadraticList_isWeaklyRegular {r n : ℕ} (hn : 2 * r < n) : RingTheory.Sequence.IsWeaklyRegular (PolynomialSpace r n) (ArbitraryRankMixedTraceRegularity.gramQuadraticList r n)

theorem MetricCodes.Spherical.HigherYoungMixedGapBranching.polarization_mem_youngGramRadialIdeal {r N : ℕ} (a b : Fin (r + 1)) {p : HigherHarmonicYoung.PolynomialSpace r N} (hp : p ∈ HigherHarmonicYoung.youngGramRadialIdeal r N) : (HigherHarmonicYoung.polarization r N a b) p ∈ HigherHarmonicYoung.youngGramRadialIdeal r N

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.lowerPolarizationPath_mem_youngGramRadialIdeal {r n : ℕ} (path : List (Fin (r + 1))) {p : PolynomialSpace r n} (hp : p ∈ youngGramRadialIdeal r n) : (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p ∈ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.arbitraryRowAxialRaise_mem_youngGramRadialIdeal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) {p : PolynomialSpace r n} (hp : p ∈ youngGramRadialIdeal r n) : (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p ∈ youngGramRadialIdeal r n

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.arbitraryRowAxialRaise_sub_mem_youngGramRadialIdeal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p q : PolynomialSpace r n) (h : p - q ∈ youngGramRadialIdeal r n) : (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p - (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) q ∈ youngGramRadialIdeal r n

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) : List (Fin (r + 1)) → Fin (r + 1) → ℕ

The arbitrary row path weight used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.
• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight lam [] = lam

def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise {r n : ℕ} (lam : Fin (r + 1) → ℕ) (k : Fin n) : List (Fin (r + 1)) → PolynomialSpace r n →ₗ[ℝ] PolynomialSpace r n

The iterated arbitrary row axial raise used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.
• MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise lam k [] = LinearMap.id

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise_append {r n : ℕ} (lam : Fin (r + 1) → ℕ) (k : Fin n) (rows rows' : List (Fin (r + 1))) : iteratedArbitraryRowAxialRaise lam k (rows ++ rows') = iteratedArbitraryRowAxialRaise (arbitraryRowPathWeight lam rows) k rows' ∘ₗ iteratedArbitraryRowAxialRaise lam k rows

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonWeightHomogeneity.lowerPolarizationPath_isHomogeneous {r n m : ℕ} (path : List (Fin (r + 1))) (p : PolynomialSpace r n) (hp : MvPolynomial.IsHomogeneous p m) : MvPolynomial.IsHomogeneous ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p) m

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonWeightHomogeneity.arbitraryRowAxialRaise_isHomogeneous {r n m : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) (hp : MvPolynomial.IsHomogeneous p m) : MvPolynomial.IsHomogeneous ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) (m + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonWeightHomogeneity.rowEuler_lowerPolarizationPath_append_singleton {r n : ℕ} (a target : Fin (r + 1)) (rows : List (Fin (r + 1))) (p : PolynomialSpace r n) (c : ℝ) (hp : (rowEuler r n a) p = c • p) : (rowEuler r n a) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (rows ++ [target])) p) = (c • (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (rows ++ [target])) p + if a = target then (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (rows ++ [target])) p else 0) - if a = rows.headD target then (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath (rows ++ [target])) p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonWeightHomogeneity.sort_headD_eq_polarizationPathStart {r : ℕ} (row : Fin (r + 1)) (S : Finset (Fin (r + 1))) : (S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2).headD row = AllRankArbitraryRowBranchingOperator.polarizationPathStart row S

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonWeightHomogeneity.rowEuler_axialCoordinate_lowerPolarizationPath {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row a : Fin (r + 1)) (k : Fin n) (S : Finset (Fin (r + 1))) (p : PolynomialSpace r n) (hp : (rowEuler r n a) p = ↑(lam a) • p) : (rowEuler r n a) (MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart row S) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])) p) = ↑(HigherChannel.raiseWeight lam row a) • (MvPolynomial.X (variableIndex (AllRankArbitraryRowBranchingOperator.polarizationPathStart row S) k) * (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonWeightHomogeneity.arbitraryRowAxialRaise_rowEuler {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) (hp : ∀ (a : Fin (r + 1)), (rowEuler r n a) p = ↑(lam a) • p) (a : Fin (r + 1)) : (rowEuler r n a) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) = ↑(HigherChannel.raiseWeight lam row a) • (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonWeightHomogeneity.sum_raiseWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : ∑ a : Fin (r + 1), HigherChannel.raiseWeight lam row a = ∑ a : Fin (r + 1), lam a + 1

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisSchedule.sum_arbitraryRowPathWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (rows : List (Fin (r + 1))) : ∑ i : Fin (r + 1), ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight lam rows i = ∑ i : Fin (r + 1), lam i + rows.length

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisSchedule.iteratedArbitraryRowAxialRaise_rowEuler {r n : ℕ} (lam : Fin (r + 1) → ℕ) (k : Fin n) (rows : List (Fin (r + 1))) (p : PolynomialSpace r n) (hp : ∀ (i : Fin (r + 1)), (rowEuler r n i) p = ↑(lam i) • p) (i : Fin (r + 1)) : (rowEuler r n i) ((ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise lam k rows) p) = ↑(ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight lam rows i) • (ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise lam k rows) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowSameAxisSchedule.iteratedArbitraryRowAxialRaise_isHomogeneous {r n d : ℕ} (lam : Fin (r + 1) → ℕ) (k : Fin n) (rows : List (Fin (r + 1))) (p : PolynomialSpace r n) (hp : MvPolynomial.IsHomogeneous p d) : MvPolynomial.IsHomogeneous ((ArbitraryRowMickelssonGramIdeal.iteratedArbitraryRowAxialRaise lam k rows) p) (d + rows.length)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankInterlacingPolynomialSeed.arbitraryRowPathWeight_eq_foldl {r : ℕ} (weight : Fin (r + 1) → ℕ) (rows : List (Fin (r + 1))) : ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight weight rows = List.foldl (fun (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) => HigherChannel.raiseWeight lam row) weight rows

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankReverseInterlacingPolynomialSeed.arbitraryRowPathWeight_reverseInterlacingRowSchedule {r : ℕ} {lam : Fin (r + 2) → ℕ} {mu : Fin (r + 1) → ℕ} (h : HigherRepresentationGraph.Interlaces lam mu) : ArbitraryRowMickelssonGramIdeal.arbitraryRowPathWeight (ThreeRowYoungBranching.appendZeroWeight mu) (HigherYoungArbitraryRankInterlacingLegalSchedule.reverseInterlacingRowSchedule lam mu) = lam

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] PolynomialSpace (r + 1) (n + 1)

The reverse interlacing polynomial seed used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed_rowEuler {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (p : ↥(HarmonicYoungSpace mu)) (i : Fin (r + 2)) : (rowEuler (r + 1) (n + 1) i) ((reverseInterlacingPolynomialSeed lam mu) p) = ↑(lam i) • (reverseInterlacingPolynomialSeed lam mu) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed_isHomogeneous {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (p : ↥(HarmonicYoungSpace mu)) : MvPolynomial.IsHomogeneous ((reverseInterlacingPolynomialSeed lam mu) p) (∑ i : Fin (r + 2), lam i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonHighest.polarization_lowerPolarizationPath_commute_tail {r n : ℕ} (row a b : Fin (r + 1)) (hrow : row ≤ a) (hab : a < b) (path : List (Fin (r + 1))) (hpath : ∀ i ∈ path, i ≤ row) (hordered : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) path) (p : PolynomialSpace r n) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) p) = (AllRankArbitraryRowBranchingOperator.lowerPolarizationPath path) ((polarization r n a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonHighest.sortedPolarizationPath_pairwise {r : ℕ} (row : Fin (r + 1)) (S : Finset (Fin (r + 1))) (hsub : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows row) : List.Pairwise (fun (x1 x2 : Fin (r + 1)) => x1 < x2) ((S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row])

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonHighest.sortedPolarizationPath_le_row {r : ℕ} (row : Fin (r + 1)) (S : Finset (Fin (r + 1))) (hsub : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows row) (i : Fin (r + 1)) (hi : i ∈ (S.sort fun (x1 x2 : Fin (r + 1)) => x1 ≤ x2) ++ [row]) : i ≤ row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonHighest.polarizationPathStart_le_row {r : ℕ} (row : Fin (r + 1)) (S : Finset (Fin (r + 1))) (hsub : S ⊆ AllRankArbitraryRowBranchingOperator.precedingRows row) : AllRankArbitraryRowBranchingOperator.polarizationPathStart row S ≤ row

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonHighest.arbitraryRowAxialRaise_polarization_tail {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row a b : Fin (r + 1)) (k : Fin n) (hrow : row ≤ a) (hab : a < b) (p : PolynomialSpace r n) (hhighest : ∀ (i j : Fin (r + 1)), i < j → (polarization r n i j) p = 0) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonHighest.arbitraryRowAxialRaise_polarization_of_initial_simpleRoots {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (k : Fin n) (p : PolynomialSpace r n) (hhighest : ∀ (i j : Fin (r + 1)), i < j → (polarization r n i j) p = 0) (hsimple : ∀ (a : Fin r), a.castSucc < row → (polarization r n a.castSucc a.succ) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) = 0) (a b : Fin (r + 1)) (hab : a < b) : (polarization r n a b) ((AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise lam row k) p) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_laterLower_of_highest {r n : ℕ} (a b j : Fin (r + 1)) (hab : a < b) (hbj : b < j) (q : PolynomialSpace r n) (hq : (polarization r n a b) q = 0) : (polarization r n a b) ((polarization r n j b) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_incomingLower_of_highest {r n : ℕ} (i a b : Fin (r + 1)) (hia : i < a) (q : PolynomialSpace r n) (hq : (polarization r n a b) q = 0) : (polarization r n a b) ((polarization r n b i) q) = (polarization r n a i) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_outgoingLower_of_highest {r n : ℕ} (a b j : Fin (r + 1)) (hbj : b < j) (q : PolynomialSpace r n) (hq : (polarization r n a b) q = 0) : (polarization r n a b) ((polarization r n j a) q) = -(polarization r n j b) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_path_neither {r n : ℕ} (i a b j : Fin (r + 1)) (hia : i < a) (hbj : b < j) (q : PolynomialSpace r n) (hq : (polarization r n a b) q = 0) : (polarization r n a b) ((polarization r n j i) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_oppositeLaterLower_of_highest {r n : ℕ} (a b j : Fin (r + 1)) (hab : a < b) (hbj : b < j) (q : PolynomialSpace r n) (A B : ℝ) (hq : (polarization r n a b) q = 0) (hqa : (rowEuler r n a) q = A • q) (hqb : (rowEuler r n b) q = B • q) : (polarization r n a b) ((polarization r n b a) ((polarization r n j b) q)) = (A - B + 1) • (polarization r n j b) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_path_first_only {r n : ℕ} (i a b j : Fin (r + 1)) (hia : i < a) (hab : a < b) (hbj : b < j) (q : PolynomialSpace r n) (hq : (polarization r n a b) q = 0) : (polarization r n a b) ((polarization r n a i) ((polarization r n j a) q)) = -(polarization r n a i) ((polarization r n j b) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_path_second_only {r n : ℕ} (i a b j : Fin (r + 1)) (hia : i < a) (hab : a < b) (hbj : b < j) (q : PolynomialSpace r n) (hq : (polarization r n a b) q = 0) : (polarization r n a b) ((polarization r n b i) ((polarization r n j b) q)) = (polarization r n a i) ((polarization r n j b) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_path_both {r n : ℕ} (i a b j : Fin (r + 1)) (hia : i < a) (hab : a < b) (hbj : b < j) (q : PolynomialSpace r n) (A B : ℝ) (hq : (polarization r n a b) q = 0) (hqa : (rowEuler r n a) q = A • q) (hqb : (rowEuler r n b) q = B • q) : (polarization r n a b) ((polarization r n a i) ((polarization r n b a) ((polarization r n j b) q))) = (A - B + 1) • (polarization r n a i) ((polarization r n j b) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_coordinate_first_only {r n : ℕ} (a b j : Fin (r + 1)) (k : Fin n) (hab : a < b) (hbj : b < j) (q : PolynomialSpace r n) (hq : (polarization r n a b) q = 0) : (polarization r n a b) (MvPolynomial.X (variableIndex a k) * (polarization r n j a) q) = -(MvPolynomial.X (variableIndex a k) * (polarization r n j b) q)

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_coordinate_second_only {r n : ℕ} (a b j : Fin (r + 1)) (k : Fin n) (hab : a < b) (hbj : b < j) (q : PolynomialSpace r n) (hq : (polarization r n a b) q = 0) : (polarization r n a b) (MvPolynomial.X (variableIndex b k) * (polarization r n j b) q) = MvPolynomial.X (variableIndex a k) * (polarization r n j b) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRowMickelssonSimpleRoot.simpleRoot_coordinate_both {r n : ℕ} (a b j : Fin (r + 1)) (k : Fin n) (hab : a < b) (hbj : b < j) (q : PolynomialSpace r n) (A B : ℝ) (hq : (polarization r n a b) q = 0) (hqa : (rowEuler r n a) q = A • q) (hqb : (rowEuler r n b) q = B • q) : (polarization r n a b) (MvPolynomial.X (variableIndex a k) * (polarization r n b a) ((polarization r n j b) q)) = (A - B + 1) • (MvPolynomial.X (variableIndex a k) * (polarization r n j b) q)