Canonical spectral decomposition

Gelfand--Tsetlin completeness, Pieri channels, and projected-axis sufficiency.

theorem MetricCodes.Spherical.HigherYoungAllRankInvariantPositiveRootKernel.exists_jointRootKernel_mem_of_vector_wordKills {K : Type u_1} {V : Type u_2} {I : Type u_3} [Semiring K] [AddCommMonoid V] [Module K V] (E : I → V →ₗ[K] V) (W : Submodule K V) (hinvariant : ∀ (i : I), ∀ v ∈ W, (E i) v ∈ W) (N : ℕ) (v : V) (hv : v ∈ W) (hvzero : v ≠ 0) (hwords : ∀ (word : List I), word.length = N → (HigherYoungTwoRowLieIrreducibility.rootOperatorWord E word) v = 0) : ∃ w ∈ W, w ≠ 0 ∧ ∀ (i : I), (E i) w = 0

theorem MetricCodes.Spherical.HigherYoungAllRankInvariantPositiveRootKernel.exists_jointRootKernel_mem_of_wordKills {K : Type u_1} {V : Type u_2} {I : Type u_3} [Semiring K] [AddCommMonoid V] [Module K V] (E : I → V →ₗ[K] V) (W : Submodule K V) (hW : W ≠ ⊥) (hinvariant : ∀ (i : I), ∀ v ∈ W, (E i) v ∈ W) (N : ℕ) (hwords : ∀ v ∈ W, ∀ (word : List I), word.length = N → (HigherYoungTwoRowLieIrreducibility.rootOperatorWord E word) v = 0) : ∃ v ∈ W, v ≠ 0 ∧ ∀ (i : I), (E i) v = 0

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanHomogeneous.polynomialComplexSpan_le_homogeneousSubmodule {r n d : ℕ} (W : Submodule ℝ (HigherHarmonicYoung.PolynomialSpace r n)) (hW : ∀ p ∈ W, MvPolynomial.IsHomogeneous p d) : HigherYoungTwoRowLieIrreducibility.polynomialComplexSpan W ≤ MvPolynomial.homogeneousSubmodule (Fin ((r + 1) * n)) ℂ d

theorem MetricCodes.Spherical.HigherYoungFullComplexSpanHomogeneous.fullYoungComplexPolynomialSpan_isHomogeneous {r n : ℕ} (lam : Fin (r + 1) → ℕ) {z : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hz : z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) : z.IsHomogeneous (∑ i : Fin (r + 1), lam i)

theorem MetricCodes.Spherical.HigherYoungRotationInvariantComplexRootStability.orthogonalPositiveRootDerivation_youngComplexPolynomialSpan_mem {r n : ℕ} (h : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) W) (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n) (f : MvPolynomial (Fin ((r + 1) * n)) ℂ) (hf : f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W) : (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation h α) f ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W

noncomputable def MetricCodes.Spherical.HigherYoungRotationInvariantComplexRootStability.orthogonalPositiveRootLinearFamily {r n : ℕ} (h : 2 * (r + 1) ≤ n) : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n → MvPolynomial (Fin ((r + 1) * n)) ℂ →ₗ[ℂ] MvPolynomial (Fin ((r + 1) * n)) ℂ

The orthogonal positive-root derivations, viewed as a family of complex linear maps.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.allRankRotationIrreducible_of_complexJointRootLine {r n : ℕ} (lam : Fin (r + 1) → ℕ) {J : Type u_1} (E : J → MvPolynomial (Fin ((r + 1) * n)) ℂ →ₗ[ℂ] MvPolynomial (Fin ((r + 1) * n)) ℂ) (L : Submodule ℂ (MvPolynomial (Fin ((r + 1) * n)) ℂ)) (hline : Module.finrank ℂ ↥L = 1) (N : ℕ) (hnil : ∀ z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam, ∀ (word : List J), word.length = N → (HigherYoungTwoRowLieIrreducibility.rootOperatorWord E word) z = 0) (hroot : ∀ (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)), HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) W → ∀ (j : J), ∀ z ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W, (E j) z ∈ HigherYoungTwoRowLieIrreducibility.youngComplexPolynomialSpan lam W) (hhighest : ∀ z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam, (∀ (j : J), (E j) z = 0) → z ∈ L) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) W) : W = ⊥ ∨ W = ⊤

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.rootOperatorWord_append_singleton_apply {K : Type u_1} {V : Type u_2} {I : Type u_3} [Semiring K] [AddCommMonoid V] [Module K V] (R : I → V →ₗ[K] V) (word : List I) (i : I) (v : V) : (HigherYoungTwoRowLieIrreducibility.rootOperatorWord R (word ++ [i])) v = (R i) ((HigherYoungTwoRowLieIrreducibility.rootOperatorWord R word) v)

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.operatorWordSpan_rotationInvariant {V : Type u_1} {I : Type u_2} [AddCommGroup V] [Module ℝ V] (R : I → V →ₗ[ℝ] V) (v : V) : HigherYoungMixedGapLieGram.IsRotationInvariant R (HigherYoungCyclicHighestSchur.operatorWordSpan R v)

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.dominantHighestRotationWordSpan_rotationInvariant {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) (HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan hn lam hdom)

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.dominantHighestRotationWordSpan_ne_bot {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan hn lam hdom ≠ ⊥

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.allRankRotationIrreducible_of_orthogonalPositiveRootRigidity {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (N : ℕ) (hnil : ∀ z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam, ∀ (word : List (HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n)), word.length = N → (HigherYoungTwoRowLieIrreducibility.rootOperatorWord (HigherYoungRotationInvariantComplexRootStability.orthogonalPositiveRootLinearFamily hn) word) z = 0) (hhighest : ∀ z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam, (∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) z = 0) → z ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) W) : W = ⊥ ∨ W = ⊤

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.dominantHighestRotationWordSpan_eq_top_of_orthogonalPositiveRootRigidity {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (N : ℕ) (hnil : ∀ z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam, ∀ (word : List (HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n)), word.length = N → (HigherYoungTwoRowLieIrreducibility.rootOperatorWord (HigherYoungRotationInvariantComplexRootStability.orthogonalPositiveRootLinearFamily hn) word) z = 0) (hhighest : ∀ z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam, (∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) z = 0) → z ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam) : HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan hn lam hdom = ⊤

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.orthogonalPositiveRootWord_eq_zero_of_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {z : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hz : z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (word : List (HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n)) (hlength : (∑ i : Fin (r + 1), lam i) * (2 * (r + 1)) < word.length) : (HigherYoungTwoRowLieIrreducibility.rootOperatorWord (HigherYoungRotationInvariantComplexRootStability.orthogonalPositiveRootLinearFamily hn) word) z = 0

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.orthogonalPositiveRootWord_eq_zero_of_fullYoung_uniform {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) {z : MvPolynomial (Fin ((r + 1) * n)) ℂ} (hz : z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam) (word : List (HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n)) (hlength : word.length = (∑ i : Fin (r + 1), lam i) * (2 * (r + 1)) + 1) : (HigherYoungTwoRowLieIrreducibility.rootOperatorWord (HigherYoungRotationInvariantComplexRootStability.orthogonalPositiveRootLinearFamily hn) word) z = 0

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.allRankRotationIrreducible_of_orthogonalPositiveRootHighestRigidity {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hhighest : ∀ z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam, (∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) z = 0) → z ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam) (W : Submodule ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hW : HigherYoungMixedGapLieGram.IsRotationInvariant (HigherYoungMixedGapLieGram.youngRotationFamily lam) W) : W = ⊥ ∨ W = ⊤

theorem MetricCodes.Spherical.HigherYoungAllRankStabilizerHighestCyclicity.dominantHighestRotationWordSpan_eq_top_of_orthogonalPositiveRootHighestRigidity {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hhighest : ∀ z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan lam, (∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) z = 0) → z ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn lam) : HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan hn lam hdom = ⊤

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalEdgeRaisingGram.finiteInterlacing_two_mul_row_count_le {r n : ℕ} {low : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : HigherChannel.FiniteInterlacing n low mu) : 2 * (r + 1) ≤ n

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalEdgeRaisingGram.canonicalEdge_loweredInternalYoungWeight_raiseWeight {r : ℕ} (low : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight (HigherChannel.raiseWeight low row) row = low

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalEdgeRaisingGram.canonicalEdge_raiseWeight_strictly_removable {r : ℕ} (low : Fin (r + 1) → ℕ) (hdom : Antitone low) (row j : Fin (r + 1)) (hj : ↑j = ↑row + 1) : HigherChannel.raiseWeight low row j < HigherChannel.raiseWeight low row row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalEdgeRaisingGram.canonicalEdgeRaisingGram_of_cyclic {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (row : Fin (r + 1)) (h : HigherChannel.FiniteInterlacing n low mu) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight low row) mu) (hcyclic : HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan ⋯ low ⋯ = ⊤) : ∃ (raisingGram : ℝ), 0 < raisingGram ∧ (∀ (p q : ↥(HarmonicYoungSpace low)), inner ℝ ((youngClebschRaise (HigherChannel.raiseWeight low row) low ⋯ row) p) ((youngClebschRaise (HigherChannel.raiseWeight low row) low ⋯ row) q) = raisingGram * inner ℝ p q) ∧ raisingGram = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * HigherChannel.weylEdgeRatio n low row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalEdgeRaisingGram.canonicalEdgeRaisingGram {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (row : Fin (r + 1)) (h : HigherChannel.FiniteInterlacing n low mu) (hraise : HigherChannel.FiniteInterlacing n (HigherChannel.raiseWeight low row) mu) : ∃ (raisingGram : ℝ), 0 < raisingGram ∧ (∀ (p q : ↥(HarmonicYoungSpace low)), inner ℝ ((youngClebschRaise (HigherChannel.raiseWeight low row) low ⋯ row) p) ((youngClebschRaise (HigherChannel.raiseWeight low row) low ⋯ row) q) = raisingGram * inner ℝ p q) ∧ raisingGram = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * HigherChannel.weylEdgeRatio n low row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.positiveGelfandTsetlinFischerGram_of_positiveRootHighestRigidity {r n : ℕ} (hn : 2 * (r + 1) < n) (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hhighest : ∀ z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan mu, (∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation ⋯ α) z = 0) → z ∈ IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule ⋯ mu) : PositiveGelfandTsetlinFischerGram lam mu h

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.positiveGelfandTsetlinFischerGram {r n : ℕ} (hn : 2 * (r + 1) + 2 ≤ n) (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) : PositiveGelfandTsetlinFischerGram lam mu h

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalBoxPositiveFischerGram {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) : PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a n i) (HigherHierarchy.Weyl.flooredWeight b n) ⋯

def MetricCodes.Spherical.HigherYoungAllRankActualProjectedAxisAssembly.CanonicalBoxReverseAxisRange {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) i) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) : Prop

The reverse axis-range condition: projected lowering of the higher box fibre lands in the lower box fibre.

Equations

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

noncomputable def MetricCodes.Spherical.HigherYoungAllRankActualProjectedAxisAssembly.canonicalBoxEdgeAxisDataOfForwardAndRaisingGram {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) i) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) (hforward : HigherYoungArbitraryRowLoweringProjectedAxisWitness.GenuineLoweringFibreAxisData a b (HigherYoungAllRankActualBoxInstantiation.boxAxis (n + 1) ⋯) (HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalBoxGelfandTsetlinFibre a b hstable hgram) low high row ⋯) (hraising : ∃ (raisingGram : ℝ), 0 < raisingGram ∧ (∀ (p q : HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a (n + 1)) low), inner ℝ ((HigherHarmonicYoung.youngClebschRaise (HigherYoungActualGraphAssembly.boxSignature a (n + 1) high) (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) ⋯ row) p) ((HigherHarmonicYoung.youngClebschRaise (HigherYoungActualGraphAssembly.boxSignature a (n + 1) high) (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) ⋯ row) q) = raisingGram * inner ℝ p q) ∧ raisingGram = HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherYoungActualGraphAssembly.boxSignature a (n + 1) high) row * HigherChannel.weylEdgeRatio (n + 1) (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) (hreverse : CanonicalBoxReverseAxisRange a b hstable hgram low high row hrow) : HigherHarmonicYoung.AllRankCanonicalBoxProjectedAxisWitness.CanonicalBoxEdgeAxisData a b (HigherYoungAllRankActualBoxInstantiation.boxAxis (n + 1) ⋯) (HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalBoxGelfandTsetlinFibre a b hstable hgram) low high row hrow

Canonical box-edge axis data assembled from forward lowering data, a positive raising Gram scalar, and the reverse range condition.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankActualProjectedAxisAssembly.canonicalEdgeRaisingGram_of_signature_eq {r n : ℕ} (low high : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (row : Fin (r + 1)) (hrow : high = HigherChannel.raiseWeight low row) (hlow : HigherChannel.FiniteInterlacing n low mu) (hhigh : HigherChannel.FiniteInterlacing n high mu) : ∃ (raisingGram : ℝ), 0 < raisingGram ∧ (∀ (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace low)), inner ℝ ((HigherHarmonicYoung.youngClebschRaise high low ⋯ row) p) ((HigherHarmonicYoung.youngClebschRaise high low ⋯ row) q) = raisingGram * inner ℝ p q) ∧ raisingGram = HigherHarmonicYoung.ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar high row * HigherChannel.weylEdgeRatio n low row

noncomputable def MetricCodes.Spherical.HigherYoungAllRankActualProjectedAxisAssembly.canonicalBoxEdgeAxisDataOfPolynomialData {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) i) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) (D : HigherHarmonicYoung.AllRankCanonicalBoxActualForward.CanonicalBoxForwardPolynomialData a b hstable hgram low high row hrow) (hreverse : CanonicalBoxReverseAxisRange a b hstable hgram low high row hrow) : HigherHarmonicYoung.AllRankCanonicalBoxProjectedAxisWitness.CanonicalBoxEdgeAxisData a b (HigherYoungAllRankActualBoxInstantiation.boxAxis (n + 1) ⋯) (HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalBoxGelfandTsetlinFibre a b hstable hgram) low high row hrow

The canonical box edge axis data of polynomial data used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankActualBranchingDimension.finrank_harmonicYoung_eq_sum_fullBranch_of_weylBranching {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n) (hdom : Antitone lam) (hbranch : BranchingDimension.WeylBranchingRecurrence n lam) : Module.finrank ℝ ↥(HarmonicYoungSpace lam) = ∑ mu : BranchingDimension.FullBranchWeight lam, Module.finrank ℝ ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature mu))

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

theorem MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.youngComplexPair_mem_fullYoungComplexPolynomialSpan {r n : ℕ} (nu : Fin (r + 1) → ℕ) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace nu)) : HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair nu p q ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan nu

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

noncomputable def MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.youngIntertwinerHighestPolynomial {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu nu : Fin (r + 1) → ℕ) (hdom : Antitone mu) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace nu)) : MvPolynomial (Fin ((r + 1) * n)) ℂ

The complex polynomial obtained by applying an intertwiner to the real and imaginary parts of a dominant highest vector.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.rotationIntertwiner_ambientCartan_dominantHighest_of_signatures {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu nu : Fin (r + 1) → ℕ) (hdom : Antitone mu) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace nu)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation nu a b ∘ₗ A) (i : Fin (r + 1)) : (HigherHarmonicYoung.DeterminantVectors.ambientCartan hn i) (youngIntertwinerHighestPolynomial hn mu nu hdom A) = ↑(2 * mu i) • youngIntertwinerHighestPolynomial hn mu nu hdom A

theorem MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.rotationIntertwiner_ambientPositiveRoot_zero_of_signatures {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu nu : Fin (r + 1) → ℕ) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace nu)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation nu a b ∘ₗ A) (i j : Fin (r + 1)) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) (hroot : (HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot hn i j) (HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair mu p q) = 0) : (HigherHarmonicYoung.DeterminantVectors.ambientPositiveRoot hn i j) (HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair nu (A p) (A q)) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.rotationIntertwiner_ambientSumPositiveRoot_zero_of_signatures {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu nu : Fin (r + 1) → ℕ) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace nu)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation nu a b ∘ₗ A) (i j : Fin (r + 1)) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) (hroot : (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot hn i j) (HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair mu p q) = 0) : (HigherHarmonicYoung.DeterminantVectors.ambientSumPositiveRoot hn i j) (HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair nu (A p) (A q)) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.rotationIntertwiner_ambientShortPositiveRoot_zero_of_signatures {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu nu : Fin (r + 1) → ℕ) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace nu)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation nu a b ∘ₗ A) (i : Fin (r + 1)) (t : Fin n) (p q : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) (hroot : (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot hn i t) (HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair mu p q) = 0) : (HigherHarmonicYoung.DeterminantVectors.ambientShortPositiveRoot hn i t) (HigherYoungArbitraryRankDominantHighestLinePreservation.youngComplexPair nu (A p) (A q)) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.rotationIntertwiner_positiveRoot_dominantHighest_of_signatures {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu nu : Fin (r + 1) → ℕ) (hdom : Antitone mu) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace nu)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation nu a b ∘ₗ A) (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n) : (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) (youngIntertwinerHighestPolynomial hn mu nu hdom A) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.youngRotationIntertwiner_eq_zero_of_signature_ne_of_highest_and_cyclic {r n : ℕ} (hn : 2 * (r + 1) ≤ n) (mu nu : Fin (r + 1) → ℕ) (hmu : Antitone mu) (hne : mu ≠ nu) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace nu)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation nu a b ∘ₗ A) (hhighest : ∀ z ∈ HigherYoungTwoRowLieIrreducibility.fullYoungComplexPolynomialSpan nu, (∀ (α : HigherYoungArbitraryRankOrthogonalRootHighestKernel.OrthogonalPositiveRoot r n), (HigherYoungArbitraryRankOrthogonalRootHighestKernel.orthogonalPositiveRootDerivation hn α) z = 0) → z ∈ HigherHarmonicYoung.IsotropicAmbientHighestLine.ambientIsotropicHighestSubmodule hn nu) (hcyclic : HigherYoungCyclicHighestSchur.dominantHighestRotationWordSpan hn mu hmu = ⊤) : A = 0

theorem MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.youngRotationIntertwiner_eq_zero_of_signature_ne {r n : ℕ} (hstable : 2 * (r + 1) + 2 ≤ n) (mu nu : Fin (r + 1) → ℕ) (hmu : Antitone mu) (hne : mu ≠ nu) (A : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace nu)) (hcomm : ∀ (a b : Fin n), A ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation nu a b ∘ₗ A) : A = 0

theorem MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.canonicalGelfandTsetlinFibre_crossGram_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hmuGram : HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu hmu) (hnuGram : HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (a b : Fin n) : (LinearMap.adjoint (HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam nu hnu hnuGram).toLinearMap ∘ₗ (HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu hmu hmuGram).toLinearMap) ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation nu a b ∘ₗ LinearMap.adjoint (HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam nu hnu hnuGram).toLinearMap ∘ₗ (HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu hmu hmuGram).toLinearMap

theorem MetricCodes.Spherical.HigherYoungAllRankDistinctSignatureStabilizerIntertwiner.canonicalGelfandTsetlinFibre_inner_eq_zero_of_signature_ne {r n : ℕ} (hstable : 2 * (r + 1) + 2 ≤ n) (lam : Fin (r + 2) → ℕ) (mu nu : Fin (r + 1) → ℕ) (hmu : HigherRepresentationGraph.Interlaces lam mu) (hnu : HigherRepresentationGraph.Interlaces lam nu) (hmuGram : HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu hmu) (hnuGram : HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam nu hnu) (hne : mu ≠ nu) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) (q : ↥(HigherHarmonicYoung.HarmonicYoungSpace nu)) : inner ℝ ((HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu hmu hmuGram) p) ((HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam nu hnu hnuGram) q) = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalBranchCompleteness.orthogonalBranchSum {ι : Type u_1} [Fintype ι] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] (f : (i : ι) → E i →ₗᵢ[ℝ] V) : ((i : ι) → E i) →ₗ[ℝ] V

The linear map summing the images of a finite family of isometric branch embeddings.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalBranchCompleteness.orthogonalBranchSum f = (LinearMap.lsum ℝ E ℝ) fun (i : ι) => (f i).toLinearMap

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalBranchCompleteness.orthogonalBranchSum_apply {ι : Type u_1} [Fintype ι] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] (f : (i : ι) → E i →ₗᵢ[ℝ] V) (x : (i : ι) → E i) : (orthogonalBranchSum f) x = ∑ i : ι, (f i) (x i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalBranchCompleteness.orthogonalBranchSum_range {ι : Type u_1} [Fintype ι] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] (f : (i : ι) → E i →ₗᵢ[ℝ] V) : (orthogonalBranchSum f).range = ⨆ (i : ι), (f i).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalBranchCompleteness.orthogonalBranchSum_injective {ι : Type u_1} [Fintype ι] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] (f : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((f i) p) ((f j) q) = 0) : Function.Injective ⇑(orthogonalBranchSum f)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalBranchCompleteness.orthogonalBranch_iSup_range_eq_top {ι : Type u_1} [Fintype ι] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (f : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((f i) p) ((f j) q) = 0) (hdim : Module.finrank ℝ V = ∑ i : ι, Module.finrank ℝ (E i)) : ⨆ (i : ι), (f i).range = ⊤

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalBranchCompleteness.orthogonalBranch_family {ι : Type u_1} {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] (f : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((f i) p) ((f j) q) = 0) : OrthogonalFamily ℝ (fun (i : ι) => ↥(f i).range) fun (i : ι) => (f i).range.subtypeₗᵢ

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalBranchCompleteness.orthogonalBranch_sum_projection {ι : Type u_1} [Fintype ι] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (f : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((f i) p) ((f j) q) = 0) (hdim : Module.finrank ℝ V = ∑ i : ι, Module.finrank ℝ (E i)) (x : V) : ∑ i : ι, (f i).range.starProjection x = x

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalBranchCompleteness.orthogonalBranch_mem_range_iff {ι : Type u_1} [Fintype ι] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (f : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((f i) p) ((f j) q) = 0) (hdim : Module.finrank ℝ V = ∑ i : ι, Module.finrank ℝ (E i)) (i : ι) (x : V) : x ∈ (f i).range ↔ ∀ (j : ι), j ≠ i → ∀ (y : E j), inner ℝ x ((f j) y) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalBranchCompleteness.orthogonalBranch_mem_range_of_orthogonal {ι : Type u_1} [Fintype ι] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (f : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((f i) p) ((f j) q) = 0) (hdim : Module.finrank ℝ V = ∑ i : ι, Module.finrank ℝ (E i)) (i : ι) (x : V) (hx : ∀ (j : ι), j ≠ i → ∀ (y : E j), inner ℝ x ((f j) y) = 0) : x ∈ (f i).range

def MetricCodes.Spherical.HigherYoungAllRankWeylBranchingRowDifference.adjacentRowDifference {R : Type u_1} [CommRing R] {r : ℕ} (M : Matrix (Fin (r + 1)) (Fin (r + 1)) R) : Matrix (Fin (r + 1)) (Fin (r + 1)) R

The matrix of adjacent row differences, with the final row retained.

Equations

• MetricCodes.Spherical.HigherYoungAllRankWeylBranchingRowDifference.adjacentRowDifference M i j = Fin.lastCases (M (Fin.last r) j) (fun (k : Fin r) => M k.castSucc j - M k.succ j) i

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankWeylBranchingRowDifference.adjacentRowDifference_castSucc {R : Type u_1} [CommRing R] {r : ℕ} (M : Matrix (Fin (r + 1)) (Fin (r + 1)) R) (i : Fin r) (j : Fin (r + 1)) : adjacentRowDifference M i.castSucc j = M i.castSucc j - M i.succ j

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankWeylBranchingRowDifference.adjacentRowDifference_last {R : Type u_1} [CommRing R] {r : ℕ} (M : Matrix (Fin (r + 1)) (Fin (r + 1)) R) (j : Fin (r + 1)) : adjacentRowDifference M (Fin.last r) j = M (Fin.last r) j

theorem MetricCodes.Spherical.HigherYoungAllRankWeylBranchingRowDifference.det_adjacentRowDifference {R : Type u_1} [CommRing R] {r : ℕ} (M : Matrix (Fin (r + 1)) (Fin (r + 1)) R) : (adjacentRowDifference M).det = M.det

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

The lower endpoint of a branching coordinate: the next weight entry, or zero in the final position.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.branchLower lam i = Fin.lastCases 0 (fun (j : Fin r) => lam j.succ) i

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.branchLower_castSucc {r : ℕ} (lam : Fin (r + 1) → ℕ) (i : Fin r) : branchLower lam i.castSucc = lam i.succ

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.BranchingDimension.branchLower_last {r : ℕ} (lam : Fin (r + 1) → ℕ) : branchLower lam (Fin.last r) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankWeylBranchingDeterminantSum.det_rowSum_eq_sum_det {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [CommRing R] {κ : ι → Type u_3} [(i : ι) → Fintype (κ i)] (row : (i : ι) → κ i → ι → R) : (Matrix.det fun (i j : ι) => ∑ a : κ i, row i a j) = ∑ a : (i : ι) → κ i, Matrix.det fun (i j : ι) => row i (a i) j

theorem MetricCodes.Spherical.HigherYoungAllRankWeylBranchingDeterminantSum.sum_det_eq_det_rowSum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [CommRing R] {κ : ι → Type u_3} [(i : ι) → Fintype (κ i)] (row : (i : ι) → κ i → ι → R) : (∑ a : (i : ι) → κ i, Matrix.det fun (i j : ι) => row i (a i) j) = Matrix.det fun (i j : ι) => ∑ a : κ i, row i a j

def MetricCodes.Spherical.HigherYoungAllRankWeylBranchingDeterminantSum.branchJacobiTrudiRow {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) (x : { a : Fin (lam i + 1) // HigherHarmonicYoung.BranchingDimension.branchLower lam i ≤ ↑a }) (j : Fin (r + 1)) : ℤ

A Jacobi–Trudi row evaluated at an allowed branching coordinate using the coefficients in ambient dimension n.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankWeylBranchingDeterminantSum.sum_orthogonalJacobiTrudiDimension_eq_det_branchRowSum {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ∑ mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam, HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n (HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu) = Matrix.det fun (i j : Fin (r + 1)) => ∑ x : { a : Fin (lam i + 1) // HigherHarmonicYoung.BranchingDimension.branchLower lam i ≤ ↑a }, branchJacobiTrudiRow n lam i x j

theorem MetricCodes.Spherical.HigherYoungAllRankWeylBranchingDeterminantSum.orthogonalJacobiTrudiDimension_eq_branchSum_of_rowSum {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hrow : ∀ (i j : Fin (r + 1)), ∑ x : { a : Fin (lam i + 1) // HigherHarmonicYoung.BranchingDimension.branchLower lam i ≤ ↑a }, branchJacobiTrudiRow (n - 1) lam i x j = HigherYoungAllRankWeylBranchingRowDifference.adjacentRowDifference (HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam) i j) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n lam = ∑ mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam, HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension (n - 1) (HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu)

theorem MetricCodes.Spherical.HigherYoungOrthogonalBranchCompleteCoefficient.orthogonalCompleteSymmetricCoefficient_dimension_sub {n : ℕ} (hn : 2 ≤ n) (k : ℤ) : HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n k - HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (k - 1) = HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient (n - 1) k

theorem MetricCodes.Spherical.HigherYoungOrthogonalBranchCompleteCoefficient.orthogonalCompleteSymmetricCoefficient_dimension_sum_range {n : ℕ} (hn : 2 ≤ n) (a : ℤ) (q : ℕ) : ∑ j ∈ Finset.range q, HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient (n - 1) (a + ↑j) = HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (a + ↑q - 1) - HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (a - 1)

theorem MetricCodes.Spherical.HigherYoungOrthogonalBranchCompleteCoefficient.orthogonalCompleteSymmetricCoefficient_dimension_sum_range_add {n : ℕ} (hn : 2 ≤ n) (shift : ℤ) (q : ℕ) : ∑ j ∈ Finset.range q, HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient (n - 1) (↑j + shift) = HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑q + shift - 1) - HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (shift - 1)

theorem MetricCodes.Spherical.HigherYoungOrthogonalBranchCompleteCoefficient.orthogonalCompleteSymmetricCoefficient_dimension_sum_Icc {n : ℕ} (hn : 2 ≤ n) {L U : ℕ} (hLU : L ≤ U) (shift : ℤ) : ∑ k ∈ Finset.Icc L U, HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient (n - 1) (↑k + shift) = HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑U + shift) - HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑L - 1 + shift)

theorem MetricCodes.Spherical.HigherYoungOrthogonalBranchCompleteCoefficient.orthogonalCompleteSymmetricCoefficient_dimension_sum_subtype {n : ℕ} (hn : 2 ≤ n) {L U : ℕ} (hLU : L ≤ U) (shift : ℤ) : ∑ k : { k : Fin (U + 1) // L ≤ ↑k }, HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient (n - 1) (↑↑↑k + shift) = HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑U + shift) - HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑L - 1 + shift)

@[reducible, inline]

abbrev MetricCodes.Spherical.HigherHarmonicYoung.AllRankWeylBranchingRecurrence.OrthogonalBranchCoordinate {r : ℕ} (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : Type

An integer branching coordinate between branchLower lam i and lam i, inclusive.

Equations

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

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankWeylBranchingRecurrence.orthogonalBranchRow {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) (a : OrthogonalBranchCoordinate lam i) (j : Fin (r + 1)) : ℤ

A Jacobi–Trudi row at an allowed branching coordinate, using the coefficients in ambient dimension n - 1.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankWeylBranchingRecurrence.branchLower_le_of_antitone {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (i : Fin (r + 1)) : BranchingDimension.branchLower lam i ≤ lam i

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankWeylBranchingRecurrence.orthogonalBranchRows_eq_adjacentRowDifference_of_interval {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hinterval : ∀ (L U : ℕ), L ≤ U → ∀ (shift : ℤ), ∑ a : { k : Fin (U + 1) // L ≤ ↑k }, HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient (n - 1) (↑↑↑a + shift) = HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑U + shift) - HigherWeylBinomialDeterminant.orthogonalCompleteSymmetricCoefficient n (↑L - 1 + shift)) : (fun (i j : Fin (r + 1)) => ∑ a : OrthogonalBranchCoordinate lam i, orthogonalBranchRow n lam i a j) = HigherYoungAllRankWeylBranchingRowDifference.adjacentRowDifference (HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankWeylBranchingRecurrence.orthogonalJacobiTrudiDimension_branching_allRank {r n : ℕ} (hn : 2 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n lam = ∑ mu : BranchingDimension.FullBranchWeight lam, HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension (n - 1) (BranchingDimension.fullBranchSignature mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankWeylBranchingRecurrence.weylBranchingRecurrence_of_jacobiTrudi_branching {r n : ℕ} (hn : 2 * r + 5 ≤ n) (lam : Fin (r + 1) → ℕ) (hbranch : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n lam = ∑ mu : BranchingDimension.FullBranchWeight lam, HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension (n - 1) (BranchingDimension.fullBranchSignature mu)) : BranchingDimension.WeylBranchingRecurrence n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankWeylBranchingRecurrence.weylBranchingRecurrence_allRank {r n : ℕ} (hn : 2 * r + 5 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : BranchingDimension.WeylBranchingRecurrence n lam

theorem MetricCodes.Spherical.HigherYoungAllRankZeroRowRotationEquivariance.ambientCoordinateDerivation_zeroRowPolynomial {r n : ℕ} (a b : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation a b) ((ThreeRowYoungBranching.zeroRowPolynomial n) p) = (ThreeRowYoungBranching.zeroRowPolynomial n) ((HigherHarmonicYoung.MixedSignature.ambientCoordinateDerivation a b) p)

theorem MetricCodes.Spherical.HigherYoungAllRankZeroRowRotationEquivariance.ambientRotation_zeroRowPolynomial {r n : ℕ} (a b : Fin n) (p : HigherHarmonicYoung.PolynomialSpace r n) : (HigherHarmonicYoung.MixedSignature.ambientRotation a b) ((ThreeRowYoungBranching.zeroRowPolynomial n) p) = (ThreeRowYoungBranching.zeroRowPolynomial n) ((HigherHarmonicYoung.MixedSignature.ambientRotation a b) p)

theorem MetricCodes.Spherical.HigherYoungAllRankZeroRowRotationEquivariance.appendZeroRowIsometryEquiv_rotation_intertwine {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) : ↑(ThreeRowYoungBranching.appendZeroRowIsometryEquiv lam).toLinearEquiv ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation (ThreeRowYoungBranching.appendZeroWeight lam) a b ∘ₗ ↑(ThreeRowYoungBranching.appendZeroRowIsometryEquiv lam).toLinearEquiv

theorem MetricCodes.Spherical.HigherYoungAllRankZeroRowRotationEquivariance.appendZeroRowIsometryEquiv_symm_rotation_intertwine {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) : ↑(ThreeRowYoungBranching.appendZeroRowIsometryEquiv lam).symm.toLinearEquiv ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation (ThreeRowYoungBranching.appendZeroWeight lam) a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a b ∘ₗ ↑(ThreeRowYoungBranching.appendZeroRowIsometryEquiv lam).symm.toLinearEquiv

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.fullBranchSignature_interlaces_appendZeroWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam) : HigherRepresentationGraph.Interlaces (ThreeRowYoungBranching.appendZeroWeight lam) (HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu)

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.fullBranchSignature_injective {r : ℕ} (lam : Fin (r + 1) → ℕ) : Function.Injective HigherHarmonicYoung.BranchingDimension.fullBranchSignature

noncomputable def MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n) (mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam) : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu)) →ₗᵢ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)

The canonical full branch fibre used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre_rotation_intertwine {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n + 1) (mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam) (a b : Fin n) : (canonicalFullBranchFibre lam hn mu).toLinearMap ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation (HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu) a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation lam a.castSucc b.castSucc ∘ₗ (canonicalFullBranchFibre lam hn mu).toLinearMap

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre_orthogonal {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n) (mu nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam) (hne : mu ≠ nu) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu))) (q : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu))) : inner ℝ ((canonicalFullBranchFibre lam hn mu) p) ((canonicalFullBranchFibre lam hn nu) q) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranch_finrank_sum {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n) (hdom : Antitone lam) (hbranch : HigherHarmonicYoung.BranchingDimension.WeylBranchingRecurrence n lam) : Module.finrank ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) = ∑ mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam, Module.finrank ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu))

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranch_finrank_sum_allRank {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n) (hdom : Antitone lam) : Module.finrank ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace lam) = ∑ mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam, Module.finrank ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu))

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranch_iSup_range_eq_top_allRank {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n) (hdom : Antitone lam) (horth : ∀ (mu nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam), mu ≠ nu → ∀ (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu))) (q : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu))), inner ℝ ((canonicalFullBranchFibre lam hn mu) p) ((canonicalFullBranchFibre lam hn nu) q) = 0) : ⨆ (mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam), (canonicalFullBranchFibre lam hn mu).range = ⊤

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranch_iSup_range_eq_top_unconditional {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n) (hdom : Antitone lam) : ⨆ (mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam), (canonicalFullBranchFibre lam hn mu).range = ⊤

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranch_sum_projection {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n) (hdom : Antitone lam) (x : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) : ∑ mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam, (canonicalFullBranchFibre lam hn mu).range.starProjection x = x

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranch_mem_range_of_orthogonal_allRank {r n : ℕ} (lam : Fin (r + 1) → ℕ) (hn : 2 * r + 5 ≤ n) (hdom : Antitone lam) (horth : ∀ (mu nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam), mu ≠ nu → ∀ (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature mu))) (q : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu))), inner ℝ ((canonicalFullBranchFibre lam hn mu) p) ((canonicalFullBranchFibre lam hn nu) q) = 0) (mu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam) (x : ↥(HigherHarmonicYoung.HarmonicYoungSpace lam)) (hx : ∀ (nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam), nu ≠ mu → ∀ (q : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu))), inner ℝ x ((canonicalFullBranchFibre lam hn nu) q) = 0) : x ∈ (canonicalFullBranchFibre lam hn mu).range

theorem MetricCodes.Spherical.HigherYoungAllRankGTProjectedLowerRange.euclideanAmbientRotation_castSucc_last {n : ℕ} (a b : Fin n) : (HigherHarmonicYoung.ClebschRotation.euclideanAmbientRotation a.castSucc b.castSucc) ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankGTProjectedLowerRange.projectedCoordinateLower_fixedAxis_rotation_intertwine {r n : ℕ} (low high : Fin (r + 2) → ℕ) (hdeg : ∑ i : Fin (r + 2), high i = ∑ i : Fin (r + 2), low i + 1) (row : Fin (r + 2)) (a b : Fin n) : HigherHarmonicYoung.projectedCoordinateLower low high hdeg row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)) ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation high a.castSucc b.castSucc = HigherHarmonicYoung.MixedSignature.youngAmbientRotation low a.castSucc b.castSucc ∘ₗ HigherHarmonicYoung.projectedCoordinateLower low high hdeg row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))

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

theorem MetricCodes.Spherical.HigherYoungAllRankSelectedBranchSignature.fullBranch_ne_selected_iff_signature_ne_appendZeroWeight {r : ℕ} {lam : Fin (r + 2) → ℕ} (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam) : nu ≠ HigherHarmonicYoung.BranchingDimension.fullBranchOfInterlaces mu h ↔ HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu ≠ ThreeRowYoungBranching.appendZeroWeight mu

noncomputable def MetricCodes.Spherical.HigherYoungAllRankCanonicalBranchProjectedLowerCrossGram.canonicalBranchProjectedLowerCrossGram {r n : ℕ} (low high : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hhigh : HigherRepresentationGraph.Interlaces high mu) (hdeg : ∑ i : Fin (r + 2), high i = ∑ i : Fin (r + 2), low i + 1) (row : Fin (r + 2)) (hn : 2 * (r + 1) + 5 ≤ n + 1) (nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight low) : ↥(HigherHarmonicYoung.HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight mu)) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu))

The cross-Gram map from a canonical Gelfand–Tsetlin fibre to a full branch after projected lowering along the last coordinate axis.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalBranchProjectedLowerCrossGram.canonicalBranchProjectedLowerCrossGram_rotation_intertwine {r n : ℕ} (low high : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hhigh : HigherRepresentationGraph.Interlaces high mu) (hdeg : ∑ i : Fin (r + 2), high i = ∑ i : Fin (r + 2), low i + 1) (row : Fin (r + 2)) (hn : 2 * (r + 1) + 5 ≤ n + 1) (nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight low) (a b : Fin n) : canonicalBranchProjectedLowerCrossGram low high mu hhigh hdeg row hn nu ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation (ThreeRowYoungBranching.appendZeroWeight mu) a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation (HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu) a b ∘ₗ canonicalBranchProjectedLowerCrossGram low high mu hhigh hdeg row hn nu

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalBranchProjectedLowerCrossGram.canonicalBranchProjectedLowerCrossGram_eq_zero_of_ne_selected {r n : ℕ} (low high : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces high mu) (hdeg : ∑ i : Fin (r + 2), high i = ∑ i : Fin (r + 2), low i + 1) (row : Fin (r + 2)) (hn : 2 * (r + 1) + 5 ≤ n + 1) (nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight low) (hne : nu ≠ HigherHarmonicYoung.BranchingDimension.fullBranchOfInterlaces mu hlow) : canonicalBranchProjectedLowerCrossGram low high mu hhigh hdeg row hn nu = 0

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalBranchProjectedLowerCrossGram.canonicalBranchProjectedLower_orthogonal_of_ne_selected {r n : ℕ} (low high : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces high mu) (hdeg : ∑ i : Fin (r + 2), high i = ∑ i : Fin (r + 2), low i + 1) (row : Fin (r + 2)) (hn : 2 * (r + 1) + 5 ≤ n + 1) (nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight low) (hne : nu ≠ HigherHarmonicYoung.BranchingDimension.fullBranchOfInterlaces mu hlow) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) (q : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu))) : inner ℝ ((HigherHarmonicYoung.projectedCoordinateLower low high hdeg row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre high mu hhigh ⋯) p)) ((HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre low hn nu) q) = 0

noncomputable def MetricCodes.Spherical.HigherYoungAllRankCanonicalGTFullCrossOrthogonality.canonicalGelfandTsetlinFullBranchCrossGram {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hgram : HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam) : ↥(HigherHarmonicYoung.HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight mu)) →ₗ[ℝ] ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu))

The cross-Gram map between a canonical Gelfand–Tsetlin fibre and a full branch, after removing the appended zero row.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGTFullCrossOrthogonality.canonicalGelfandTsetlinFullBranchCrossGram_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hgram : HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam) (a b : Fin n) : canonicalGelfandTsetlinFullBranchCrossGram lam mu h hn hgram nu ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation (ThreeRowYoungBranching.appendZeroWeight mu) a b = HigherHarmonicYoung.MixedSignature.youngAmbientRotation (HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu) a b ∘ₗ canonicalGelfandTsetlinFullBranchCrossGram lam mu h hn hgram nu

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGTFullCrossOrthogonality.canonicalGelfandTsetlinFullBranchCrossGram_eq_zero_of_ne_selected {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hgram : HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam) (hne : nu ≠ HigherHarmonicYoung.BranchingDimension.fullBranchOfInterlaces mu h) : canonicalGelfandTsetlinFullBranchCrossGram lam mu h hn hgram nu = 0

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalGTFullCrossOrthogonality.canonicalGelfandTsetlinFibre_fullBranch_orthogonal_of_ne_selected {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hgram : HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (nu : HigherHarmonicYoung.BranchingDimension.FullBranchWeight lam) (hne : nu ≠ HigherHarmonicYoung.BranchingDimension.fullBranchOfInterlaces mu h) (p : ↥(HigherHarmonicYoung.HarmonicYoungSpace mu)) (q : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherHarmonicYoung.BranchingDimension.fullBranchSignature nu))) : inner ℝ ((HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu h hgram) p) ((HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre lam hn nu) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalSelectedBranchRange.orthogonalBranch_range_eq_of_cross_orthogonal {ι : Type u_1} [Fintype ι] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((f i) p) ((f j) q) = 0) (hdim : Module.finrank ℝ V = ∑ i : ι, Module.finrank ℝ (E i)) (g : F →ₗᵢ[ℝ] V) (i : ι) (hcross : ∀ (j : ι), j ≠ i → ∀ (p : F) (q : E j), inner ℝ (g p) ((f j) q) = 0) (heqdim : Module.finrank ℝ F = Module.finrank ℝ (E i)) : g.range = (f i).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalSelectedBranchRange.orthogonalBranch_range_eq_of_cross_orthogonal_of_equiv {ι : Type u_1} [Fintype ι] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((f i) p) ((f j) q) = 0) (hdim : Module.finrank ℝ V = ∑ i : ι, Module.finrank ℝ (E i)) (g : F →ₗᵢ[ℝ] V) (i : ι) (hcross : ∀ (j : ι), j ≠ i → ∀ (p : F) (q : E j), inner ℝ (g p) ((f j) q) = 0) (e : F ≃ₗᵢ[ℝ] E i) : g.range = (f i).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalSelectedBranchRange.canonicalGelfandTsetlinFibre_range_eq_selectedFullBranch {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 1) + 5 ≤ n + 1) (hdom : Antitone lam) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) : (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu h hgram).range = (HigherYoungAllRankCanonicalGelfandTsetlinCompleteness.canonicalFullBranchFibre lam hn (BranchingDimension.fullBranchOfInterlaces mu h)).range

theorem MetricCodes.Spherical.HigherYoungAllRankCanonicalBoxReverseRange.canonicalBoxReverseAxisRange_of_strongStable {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) i) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯) (hnstrong : 2 * (r + 1) + 5 ≤ n + 1) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) : HigherYoungAllRankActualProjectedAxisAssembly.CanonicalBoxReverseAxisRange a b hstable hgram low high row hrow

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankActualFischerGramRecurrence.canonicalGelfandTsetlinFischerGram_adjacent_of_projectedLower {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hdom : Antitone low) (hlowGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (hhighGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherChannel.raiseWeight low row) mu hhigh) (hexchange : ∀ (p : ↥(HarmonicYoungSpace mu)), (AllRankArbitraryRowBranchingOperator.arbitraryRowAxialRaise low row (Fin.last n)) ((ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed low mu) p) - (ArbitraryRankReverseInterlacingPolynomialSeed.reverseInterlacingPolynomialSeed (HigherChannel.raiseWeight low row) mu) p ∈ youngGramRadialIdeal (r + 1) (n + 1)) (hcartan : ∀ (p : ↥(HarmonicYoungSpace mu)), (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise low hdom row (Fin.last n)) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p)) = (ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row * ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * HigherChannel.plusProbability (n + 1) low mu row) • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p) (p : ↥(HarmonicYoungSpace mu)) (hp : p ≠ 0) : AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram (HigherChannel.raiseWeight low row) mu hhigh hhighGram = ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row ^ 2 * ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFischerGram low mu hlow hlowGram * HigherChannel.plusProbability (n + 1) low mu row

noncomputable def MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.signedAmbientCharacteristic {r : ℕ} (L : Fin (r + 1) → ℝ) : Polynomial ℝ

The signed ambient characteristic used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.signedAmbientCharacteristic L = Lagrange.nodal Finset.univ (MetricCodes.Spherical.HigherChannel.signedNode L)

theorem MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.signedAmbientCharacteristic_derivative_eval_pos {r : ℕ} (L : Fin (r + 1) → ℝ) (row : Fin (r + 1)) : Polynomial.eval (L row) (Polynomial.derivative (signedAmbientCharacteristic L)) = HigherChannel.activeDenominator L row

theorem MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.signedAmbientCharacteristic_derivative_eval_neg {r : ℕ} (L : Fin (r + 1) → ℝ) (row : Fin (r + 1)) : Polynomial.eval (-L row) (Polynomial.derivative (signedAmbientCharacteristic L)) = -HigherChannel.activeDenominator L row

noncomputable def MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Polynomial ℝ

The gt channel characteristic polynomial used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristic_derivative_eval_pos {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : Polynomial.eval (HigherChannel.ambientShift n lam row) (Polynomial.derivative (gtChannelCharacteristicPolynomial n lam)) = HigherChannel.activeDenominator (HigherChannel.ambientShift n lam) row

theorem MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristic_derivative_eval_neg {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : Polynomial.eval (-HigherChannel.ambientShift n lam row) (Polynomial.derivative (gtChannelCharacteristicPolynomial n lam)) = -HigherChannel.activeDenominator (HigherChannel.ambientShift n lam) row

theorem MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.plusProbability_eq_gtCharacteristic_residue {r n : ℕ} (lam : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (row : Fin (r + 1)) : HigherChannel.plusProbability n lam mu row = Polynomial.eval (HigherChannel.ambientShift n lam row) (HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift n r) (HigherChannel.stabilizerShift n mu)) / Polynomial.eval (HigherChannel.ambientShift n lam row) (Polynomial.derivative (gtChannelCharacteristicPolynomial n lam))

theorem MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.FiniteInterlacing.gtChannelCharacteristic_derivative_eval_ne_zero {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : HigherChannel.FiniteInterlacing n lam mu) (row : Fin (r + 1)) (sign : Bool) : Polynomial.eval (HigherChannel.signedNode (HigherChannel.ambientShift n lam) (row, sign)) (Polynomial.derivative (gtChannelCharacteristicPolynomial n lam)) ≠ 0

theorem MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.characteristicResidue_unique_of_resolvent {ι : Type u_1} [Fintype ι] (nodes : ι → ℝ) (hinjective : Function.Injective nodes) (numerator : Polynomial ℝ) (weight : ι → ℝ) (hresolvent : ∀ (z : ℝ), (∀ (i : ι), z ≠ nodes i) → Polynomial.eval z numerator / Polynomial.eval z (Lagrange.nodal Finset.univ nodes) = ∑ i : ι, weight i / (z - nodes i)) (i : ι) : weight i = Polynomial.eval (nodes i) numerator / Polynomial.eval (nodes i) (Polynomial.derivative (Lagrange.nodal Finset.univ nodes))

theorem MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.characteristicResidue_scaled_unique_of_resolvent {ι : Type u_1} [Fintype ι] (nodes : ι → ℝ) (hinjective : Function.Injective nodes) (numerator : Polynomial ℝ) (weight : ι → ℝ) (scale : ℝ) (hresolvent : ∀ (z : ℝ), (∀ (i : ι), z ≠ nodes i) → scale * Polynomial.eval z numerator / Polynomial.eval z (Lagrange.nodal Finset.univ nodes) = ∑ i : ι, weight i / (z - nodes i)) (i : ι) : weight i = scale * Polynomial.eval (nodes i) numerator / Polynomial.eval (nodes i) (Polynomial.derivative (Lagrange.nodal Finset.univ nodes))

theorem MetricCodes.Spherical.HigherYoungAllRankGTCharacteristicResidue.FiniteInterlacing.gtChannel_positiveWeight_eq_mul_plusProbability_of_resolvent {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : HigherChannel.FiniteInterlacing n lam mu) (weight : Fin (r + 1) × Bool → ℝ) (scale : ℝ) (hresolvent : ∀ (z : ℝ), (∀ (i : Fin (r + 1) × Bool), z ≠ HigherChannel.signedNode (HigherChannel.ambientShift n lam) i) → scale * Polynomial.eval z (HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift n r) (HigherChannel.stabilizerShift n mu)) / Polynomial.eval z (gtChannelCharacteristicPolynomial n lam) = ∑ i : Fin (r + 1) × Bool, weight i / (z - HigherChannel.signedNode (HigherChannel.ambientShift n lam) i)) (row : Fin (r + 1)) : weight (row, true) = scale * HigherChannel.plusProbability n lam mu row

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankCartanCharacteristicInterpolation.cartanCharacteristicInterpolationProjector {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [AddCommGroup V] [Module ℝ V] (nodes : ι → ℝ) (T : Module.End ℝ V) (i : ι) : Module.End ℝ V

The Lagrange interpolation polynomial for node i, evaluated at the endomorphism T.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCartanCharacteristicInterpolation.cartanCharacteristicInterpolationProjector_apply_of_eigenvector {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [AddCommGroup V] [Module ℝ V] (nodes : ι → ℝ) (T : Module.End ℝ V) (hnode : Function.Injective nodes) (i j : ι) (x : V) (hx : T x = nodes j • x) : (cartanCharacteristicInterpolationProjector nodes T i) x = if i = j then x else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCartanCharacteristicInterpolation.cartanCharacteristicInterpolationBasis_mul_eq_nodal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (nodes : ι → ℝ) (i : ι) : (Polynomial.X - Polynomial.C (nodes i)) * Lagrange.basis Finset.univ nodes i = Polynomial.C (Lagrange.nodalWeight Finset.univ nodes i) * Lagrange.nodal Finset.univ nodes

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCartanCharacteristicInterpolation.signedAmbientCharacteristicNodes_injective {r n : ℕ} {lam : Fin (r + 1) → ℕ} {mu : Fin r → ℕ} (h : HigherChannel.FiniteInterlacing n lam mu) : Function.Injective (HigherChannel.signedNode (HigherChannel.ambientShift n lam))

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtTensorCasimir {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Module.End ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam))

The tensor Casimir operator, one half of the sum of the negative squares of the tensor ambient rotations.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtTensorCasimir_intertwiner {r n : ℕ} (source target : Fin (r + 1) → ℕ) (A : ↥(HarmonicYoungSpace source) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation source a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ A) : gtTensorCasimir target ∘ₗ A = A ∘ₗ MixedSignature.youngAmbientCasimir source

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtTensorCasimir_channel {r n : ℕ} (source target : Fin (r + 1) → ℕ) (A : ↥(HarmonicYoungSpace source) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation source a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ A) (p : ↥(HarmonicYoungSpace source)) : (gtTensorCasimir target) (A p) = MixedSignature.allRankCasimirEigenvalue n source • A p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtRelativeCasimir {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Module.End ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam))

The gt relative casimir used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtRelativeCasimir_channel {r n : ℕ} (source target : Fin (r + 1) → ℕ) (A : ↥(HarmonicYoungSpace source) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation source a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ A) (p : ↥(HarmonicYoungSpace source)) : (gtRelativeCasimir target) (A p) = ((MixedSignature.allRankCasimirEigenvalue n source - MixedSignature.allRankCasimirEigenvalue n target - 1) / 2) • A p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtRelativeCasimir_raise_eigenvalue {r n : ℕ} (target : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : (MixedSignature.allRankCasimirEigenvalue n (HigherChannel.raiseWeight target row) - MixedSignature.allRankCasimirEigenvalue n target - 1) / 2 = HigherChannel.ambientShift n target row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtRelativeCasimir_lower_eigenvalue {r n : ℕ} (target source : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hsource : target = HigherChannel.raiseWeight source row) : (MixedSignature.allRankCasimirEigenvalue n source - MixedSignature.allRankCasimirEigenvalue n target - 1) / 2 = -HigherChannel.ambientShift n target row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtRelativeCasimir_raise_channel {r n : ℕ} (target : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (A : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight target row)) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation (HigherChannel.raiseWeight target row) a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ A) (p : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight target row))) : (gtRelativeCasimir target) (A p) = HigherChannel.signedNode (HigherChannel.ambientShift n target) (row, true) • A p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtRelativeCasimir_lower_channel {r n : ℕ} (target source : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hsource : target = HigherChannel.raiseWeight source row) (A : ↥(HarmonicYoungSpace source) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation source a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ A) (p : ↥(HarmonicYoungSpace source)) : (gtRelativeCasimir target) (A p) = HigherChannel.signedNode (HigherChannel.ambientShift n target) (row, false) • A p

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirProjector.gtCharacteristicProjector {r n : ℕ} (target : Fin (r + 1) → ℕ) (z : Fin (r + 1) × Bool) : Module.End ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target))

The gt characteristic projector used in the spherical-code argument.

Equations

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

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) : ↥(HarmonicYoungSpace mu) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace lam)

The canonical gelfand tsetlin axis tensor used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor_apply {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (p : ↥(HarmonicYoungSpace mu)) : (canonicalGelfandTsetlinAxisTensor lam mu h hgram) p = (EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n) ⊗ₜ[ℝ] (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu h hgram) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor_inner {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ ((canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) ((canonicalGelfandTsetlinAxisTensor lam mu h hgram) q) = inner ℝ p q

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolvent.signedCharacteristicProjector {r : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℝ V] (L : Fin (r + 1) → ℝ) (T : Module.End ℝ V) (i : Fin (r + 1) × Bool) : Module.End ℝ V

The signed characteristic projector used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolvent.sum_signedCharacteristicProjector {r : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℝ V] (L : Fin (r + 1) → ℝ) (hL : Function.Injective (HigherChannel.signedNode L)) (T : Module.End ℝ V) : ∑ i : Fin (r + 1) × Bool, signedCharacteristicProjector L T i = LinearMap.id

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolvent.signedNode_sub_mul_basis {r : ℕ} (L : Fin (r + 1) → ℝ) (i : Fin (r + 1) × Bool) : (Polynomial.X - Polynomial.C (HigherChannel.signedNode L i)) * Lagrange.basis Finset.univ (HigherChannel.signedNode L) i = Polynomial.C (Lagrange.nodalWeight Finset.univ (HigherChannel.signedNode L) i) * HigherYoungAllRankGTCharacteristicResidue.signedAmbientCharacteristic L

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolvent.signedCharacteristicProjector_eigen_of_aeval_apply {r : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℝ V] (L : Fin (r + 1) → ℝ) (T : Module.End ℝ V) (i : Fin (r + 1) × Bool) (v : V) (hchar : ((Polynomial.aeval T) (HigherYoungAllRankGTCharacteristicResidue.signedAmbientCharacteristic L)) v = 0) : T ((signedCharacteristicProjector L T i) v) = HigherChannel.signedNode L i • (signedCharacteristicProjector L T i) v

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirPureAxis.gtEuclideanCasimir (n : ℕ) : Module.End ℝ (SpherePacking.Euclidean n)

The Euclidean Casimir operator, one half of the sum of the negative squares of the ambient rotations.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirPureAxis.gtEuclideanCasimir_eq_smul_id (n : ℕ) : gtEuclideanCasimir n = (↑n - 1) • LinearMap.id

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirPureAxis.gtTensorCasimir_tmul {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (AllRankGTRelativeCasimirProjector.gtTensorCasimir lam) (v ⊗ₜ[ℝ] p) = 2⁻¹ • ∑ a : Fin n, ∑ b : Fin n, -((ClebschRotation.euclideanAmbientRotation a b) ((ClebschRotation.euclideanAmbientRotation a b) v) ⊗ₜ[ℝ] p + (ClebschRotation.euclideanAmbientRotation a b) v ⊗ₜ[ℝ] (MixedSignature.youngAmbientRotation lam a b) p + ((ClebschRotation.euclideanAmbientRotation a b) v ⊗ₜ[ℝ] (MixedSignature.youngAmbientRotation lam a b) p + v ⊗ₜ[ℝ] (MixedSignature.youngAmbientRotation lam a b) ((MixedSignature.youngAmbientRotation lam a b) p)))

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Module.End ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam))

The gt mixed rotation operator used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirPureAxis.gtMixedRotationOperator_tmul {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (gtMixedRotationOperator lam) (v ⊗ₜ[ℝ] p) = ∑ a : Fin n, ∑ b : Fin n, (ClebschRotation.euclideanAmbientRotation a b) v ⊗ₜ[ℝ] (MixedSignature.youngAmbientRotation lam a b) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirPureAxis.gtEuclideanCasimir_tmul {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (gtEuclideanCasimir n) v ⊗ₜ[ℝ] p = 2⁻¹ • ∑ a : Fin n, ∑ b : Fin n, -(ClebschRotation.euclideanAmbientRotation a b) ((ClebschRotation.euclideanAmbientRotation a b) v) ⊗ₜ[ℝ] p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirPureAxis.gtYoungCasimir_tmul {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : v ⊗ₜ[ℝ] (MixedSignature.youngAmbientCasimir lam) p = 2⁻¹ • ∑ a : Fin n, ∑ b : Fin n, -v ⊗ₜ[ℝ] (MixedSignature.youngAmbientRotation lam a b) ((MixedSignature.youngAmbientRotation lam a b) p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirPureAxis.gtTensorCasimir_tmul_eq_vector_add_young_sub_mixed {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (AllRankGTRelativeCasimirProjector.gtTensorCasimir lam) (v ⊗ₜ[ℝ] p) = (gtEuclideanCasimir n) v ⊗ₜ[ℝ] p + v ⊗ₜ[ℝ] (MixedSignature.youngAmbientCasimir lam) p - (gtMixedRotationOperator lam) (v ⊗ₜ[ℝ] p)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirPureAxis.gtRelativeCasimir_tmul_eq_scalar_sub_mixed {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) (v ⊗ₜ[ℝ] p) = ((↑n - 2) / 2) • v ⊗ₜ[ℝ] p - 2⁻¹ • (gtMixedRotationOperator lam) (v ⊗ₜ[ℝ] p)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector {r n : ℕ} (target : Fin (r + 1) → ℕ) (channel : Fin (r + 1) × Bool) : Module.End ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target))

The all rank cartan characteristic projector used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector_apply_eigenvector {r n : ℕ} (target : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (h : HigherChannel.FiniteInterlacing n target mu) (selected actual : Fin (r + 1) × Bool) (x : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hx : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir target) x = HigherChannel.signedNode (HigherChannel.ambientShift n target) actual • x) : (allRankCartanCharacteristicProjector target selected) x = if selected = actual then x else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector_raise_channel {r n : ℕ} (target : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (h : HigherChannel.FiniteInterlacing n target mu) (selected : Fin (r + 1) × Bool) (row : Fin (r + 1)) (A : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight target row)) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation (HigherChannel.raiseWeight target row) a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ A) (p : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight target row))) : (allRankCartanCharacteristicProjector target selected) (A p) = if selected = (row, true) then A p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector_lower_channel {r n : ℕ} (target : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (h : HigherChannel.FiniteInterlacing n target mu) (selected : Fin (r + 1) × Bool) (row : Fin (r + 1)) (source : Fin (r + 1) → ℕ) (hsource : target = HigherChannel.raiseWeight source row) (A : ↥(HarmonicYoungSpace source) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation source a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ A) (p : ↥(HarmonicYoungSpace source)) : (allRankCartanCharacteristicProjector target selected) (A p) = if selected = (row, false) then A p else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector_youngClebschLower {r n : ℕ} (target : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (h : HigherChannel.FiniteInterlacing n target mu) (selected : Fin (r + 1) × Bool) (row : Fin (r + 1)) (p : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight target row))) : (allRankCartanCharacteristicProjector target selected) ((youngClebschLower target (HigherChannel.raiseWeight target row) ⋯ row) p) = if selected = (row, true) then (youngClebschLower target (HigherChannel.raiseWeight target row) ⋯ row) p else 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (p q : ↥(HarmonicYoungSpace mu)) (channel : Fin (r + 2) × Bool) : ℝ

The gt axis compressed signed projector 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.AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial ℝ

The gt axis compressed characteristic minor used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor_eval_signedNode {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) (channel : Fin (r + 2) × Bool) : Polynomial.eval (HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) channel) (gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = Polynomial.eval (HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) channel) (Polynomial.derivative (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) * gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q channel

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor_degree_lt {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) : (gtAxisCompressedCharacteristicMinor lam mu h hgram p q).degree < ↑Finset.univ.card

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedCharacteristicMinor.sum_gtAxisCompressedSignedProjectorCoefficient {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) : ∑ channel : Fin (r + 2) × Bool, gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q channel = inner ℝ p q

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor_eq_sum_nodal_erase {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) : gtAxisCompressedCharacteristicMinor lam mu h hgram p q = ∑ channel : Fin (r + 2) × Bool, Polynomial.C (gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q channel) * Lagrange.nodal (Finset.univ.erase channel) (HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam))

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor_div_characteristic {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) (z : ℝ) (hz : ∀ (channel : Fin (r + 2) × Bool), z ≠ HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) channel) : Polynomial.eval z (gtAxisCompressedCharacteristicMinor lam mu h hgram p q) / Polynomial.eval z (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam) = ∑ channel : Fin (r + 2) × Bool, gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q channel / (z - HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) channel)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient_pos_eq_plusProbability_of_minor {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (p q : ↥(HarmonicYoungSpace mu)) (hminor : gtAxisCompressedCharacteristicMinor lam mu h hgram p q = Polynomial.C (inner ℝ p q) * HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu)) (row : Fin (r + 2)) : gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (row, true) = inner ℝ p q * HigherChannel.plusProbability (n + 1) lam mu row

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.gtYoungAxisTensor {r n : ℕ} (lam : Fin (r + 1) → ℕ) (axis : SpherePacking.Euclidean n) : ↥(HarmonicYoungSpace lam) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)

The linear map sending a harmonic Young vector p to the pure tensor axis ⊗ₜ p.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.gtYoungAxisTensor_apply {r n : ℕ} (lam : Fin (r + 1) → ℕ) (axis : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (gtYoungAxisTensor lam axis) p = axis ⊗ₜ[ℝ] p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.youngClebschLower_adjoint_comp_gtYoungAxisTensor {r n : ℕ} (low high : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), high i = ∑ i : Fin (r + 1), low i + 1) (row : Fin (r + 1)) (axis : SpherePacking.Euclidean n) : LinearMap.adjoint (youngClebschLower low high hdeg row) ∘ₗ gtYoungAxisTensor low axis = projectedCoordinateRaise high low hdeg row axis

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.gtYoungAxisTensor_adjoint_comp_youngClebschLower {r n : ℕ} (low high : Fin (r + 1) → ℕ) (hdeg : ∑ i : Fin (r + 1), high i = ∑ i : Fin (r + 1), low i + 1) (row : Fin (r + 1)) (axis : SpherePacking.Euclidean n) : LinearMap.adjoint (gtYoungAxisTensor low axis) ∘ₗ youngClebschLower low high hdeg row = projectedCoordinateLower low high hdeg row axis

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.arbitraryRowSameAxisHarmonicRaise_eq_lowerScalar_smul_projectedCoordinateRaise {r n : ℕ} (low : Fin (r + 1) → ℕ) (hdom : Antitone low) (row : Fin (r + 1)) (k : Fin n) (p : ↥(HarmonicYoungSpace low)) : (AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise low hdom row k) p = ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row • (projectedCoordinateRaise (HigherChannel.raiseWeight low row) low ⋯ row ((EuclideanSpace.basisFun (Fin n) ℝ) k)) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.projectedCoordinateLower_sameAxisHarmonicRaise_eq_axisClebschGram {r n : ℕ} (low : Fin (r + 1) → ℕ) (hdom : Antitone low) (row : Fin (r + 1)) (k : Fin n) (p : ↥(HarmonicYoungSpace low)) : (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin n) ℝ) k)) ((AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise low hdom row k) p) = ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row • (LinearMap.adjoint (gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin n) ℝ) k))) ((youngClebschLower low (HigherChannel.raiseWeight low row) ⋯ row ∘ₗ LinearMap.adjoint (youngClebschLower low (HigherChannel.raiseWeight low row) ⋯ row)) ((gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin n) ℝ) k)) p))

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector {r n : ℕ} (low : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : Module.End ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace low))

The gt selected row clebsch range projector used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.internalRowLowerGramScalar_raiseWeight_pos {r : ℕ} (low : Fin (r + 1) → ℕ) (hdom : Antitone low) (row : Fin (r + 1)) : 0 < ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.youngClebschLower_raiseWeight_adjoint_comp_self {r n : ℕ} (low : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hhigh : Antitone (HigherChannel.raiseWeight low row)) : LinearMap.adjoint (youngClebschLower low (HigherChannel.raiseWeight low row) ⋯ row) ∘ₗ youngClebschLower low (HigherChannel.raiseWeight low row) ⋯ row = ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row • LinearMap.id

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector_youngClebschLower {r n : ℕ} (low : Fin (r + 1) → ℕ) (hdom : Antitone low) (row : Fin (r + 1)) (hhigh : Antitone (HigherChannel.raiseWeight low row)) (p : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight low row))) : (gtSelectedRowClebschRangeProjector low row) ((youngClebschLower low (HigherChannel.raiseWeight low row) ⋯ row) p) = (youngClebschLower low (HigherChannel.raiseWeight low row) ⋯ row) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.projectedCoordinateLower_sameAxisHarmonicRaise_eq_selectedClebschProjector_compression {r n : ℕ} (low : Fin (r + 1) → ℕ) (hdom : Antitone low) (row : Fin (r + 1)) (k : Fin n) (p : ↥(HarmonicYoungSpace low)) : (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin n) ℝ) k)) ((AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise low hdom row k) p) = (ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row * ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row) • (LinearMap.adjoint (gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin n) ℝ) k))) ((gtSelectedRowClebschRangeProjector low row) ((gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin n) ℝ) k)) p))

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.projectedCoordinateLower_sameAxisHarmonicRaise_eq_plusProbability_iff {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (hdom : Antitone low) (row : Fin (r + 1)) (k : Fin n) (p : ↥(HarmonicYoungSpace low)) : (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin n) ℝ) k)) ((AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise low hdom row k) p) = (ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row * ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * HigherChannel.plusProbability n low mu row) • p ↔ (LinearMap.adjoint (gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin n) ℝ) k))) ((gtSelectedRowClebschRangeProjector low row) ((gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin n) ℝ) k)) p)) = HigherChannel.plusProbability n low mu row • p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.reverseInterlacing_projectedCoordinateLower_sameAxis_eq_plusProbability_iff {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hlow : HigherRepresentationGraph.Interlaces low mu) (hdom : Antitone low) (row : Fin (r + 2)) (p : ↥(HarmonicYoungSpace mu)) : (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise low hdom row (Fin.last n)) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p)) = (ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row * ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * HigherChannel.plusProbability (n + 1) low mu row) • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p ↔ (LinearMap.adjoint (gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)))) ((gtSelectedRowClebschRangeProjector low row) ((gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p))) = HigherChannel.plusProbability (n + 1) low mu row • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.canonicalGelfandTsetlinFibre_selectedClebschCompression_iff_reverse {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hlow : HigherRepresentationGraph.Interlaces low mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (row : Fin (r + 2)) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)))) ((gtSelectedRowClebschRangeProjector low row) ((gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hgram) p))) = HigherChannel.plusProbability (n + 1) low mu row • (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hgram) p ↔ (LinearMap.adjoint (gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)))) ((gtSelectedRowClebschRangeProjector low row) ((gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p))) = HigherChannel.plusProbability (n + 1) low mu row • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector_axisCompression_mem_reverseBranch_range {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hforward : ∀ (p : ↥(HarmonicYoungSpace mu)), (projectedCoordinateRaise (HigherChannel.raiseWeight low row) low ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p) ∈ (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch (HigherChannel.raiseWeight low row) mu hhigh).range) (hreverse : ∀ (p : ↥(HarmonicYoungSpace mu)), (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch (HigherChannel.raiseWeight low row) mu hhigh) p) ∈ (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow).range) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)))) ((gtSelectedRowClebschRangeProjector low row) ((gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p))) ∈ (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector_axisCompression_mem_canonicalFibre_range {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (hforward : ∀ (p : ↥(HarmonicYoungSpace mu)), (projectedCoordinateRaise (HigherChannel.raiseWeight low row) low ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p) ∈ (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch (HigherChannel.raiseWeight low row) mu hhigh).range) (hreverse : ∀ (p : ↥(HarmonicYoungSpace mu)), (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch (HigherChannel.raiseWeight low row) mu hhigh) p) ∈ (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow).range) (p : ↥(HarmonicYoungSpace mu)) : (LinearMap.adjoint (gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)))) ((gtSelectedRowClebschRangeProjector low row) ((gtYoungAxisTensor low ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hgram) p))) ∈ (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hgram).range

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedProjectorCompression.gtSelectedProjectorCompression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (row : Fin (r + 2)) : Module.End ℝ ↥(HarmonicYoungSpace mu)

The signed characteristic projector for (row, true), compressed along the canonical Gelfand–Tsetlin axis tensor map.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedProjectorCompression.gtSelectedProjectorCompression_inner {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (row : Fin (r + 2)) (p q : ↥(HarmonicYoungSpace mu)) : inner ℝ p ((gtSelectedProjectorCompression lam mu h hgram row) q) = AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (row, true)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedProjectorCompression.gtSelectedProjectorCompression_inner_eq_plusProbability_of_minor {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (row : Fin (r + 2)) (p q : ↥(HarmonicYoungSpace mu)) (hminor : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q = Polynomial.C (inner ℝ p q) * HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu)) : inner ℝ p ((gtSelectedProjectorCompression lam mu h hgram row) q) = inner ℝ p q * HigherChannel.plusProbability (n + 1) lam mu row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedProjectorCompression.gtSelectedProjectorCompression_eq_plusProbability_of_minor {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (row : Fin (r + 2)) (hminor : ∀ (p q : ↥(HarmonicYoungSpace mu)), AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q = Polynomial.C (inner ℝ p q) * HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu)) : gtSelectedProjectorCompression lam mu h hgram row = HigherChannel.plusProbability (n + 1) lam mu row • LinearMap.id

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedProjectorCompression.gtSelectedPhysicalAxisCompression {r n : ℕ} (lam : Fin (r + 2) → ℕ) (row : Fin (r + 2)) : Module.End ℝ ↥(HarmonicYoungSpace lam)

The selected Clebsch range projector compressed along tensoring with the last coordinate axis.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedProjectorCompression.gtSelectedProjectorCompression_eq_fibre_adjoint_physical_of_selected {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (row : Fin (r + 2)) (hselected : ∀ (p : ↥(HarmonicYoungSpace mu)), (AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector lam (row, true)) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) = (AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector lam row) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p)) : gtSelectedProjectorCompression lam mu h hgram row = LinearMap.adjoint (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu h hgram).toLinearMap ∘ₗ gtSelectedPhysicalAxisCompression lam row ∘ₗ (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu h hgram).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedProjectorCompression.gtSelectedPhysicalAxisCompression_fibre_eq_plusProbability_of_minor_and_range {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (row : Fin (r + 2)) (hminor : ∀ (p q : ↥(HarmonicYoungSpace mu)), AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q = Polynomial.C (inner ℝ p q) * HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu)) (hselected : ∀ (p : ↥(HarmonicYoungSpace mu)), (AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector lam (row, true)) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) = (AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector lam row) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p)) (hrange : ∀ (p : ↥(HarmonicYoungSpace mu)), (gtSelectedPhysicalAxisCompression lam row) ((AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu h hgram) p) ∈ (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu h hgram).range) (p : ↥(HarmonicYoungSpace mu)) : (gtSelectedPhysicalAxisCompression lam row) ((AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu h hgram) p) = HigherChannel.plusProbability (n + 1) lam mu row • (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre lam mu h hgram) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedProjectorCompression.reverseInterlacing_projectedCoordinateLower_sameAxis_eq_plusProbability_of_minor {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hlow : HigherRepresentationGraph.Interlaces low mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (hfinite : HigherChannel.FiniteInterlacing (n + 1) low mu) (hdom : Antitone low) (row : Fin (r + 2)) (hminor : ∀ (p q : ↥(HarmonicYoungSpace mu)), AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor low mu hlow hgram p q = Polynomial.C (inner ℝ p q) * HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu)) (hselected : ∀ (p : ↥(HarmonicYoungSpace mu)), (AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector low (row, true)) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor low mu hlow hgram) p) = (AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector low row) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor low mu hlow hgram) p)) (hrange : ∀ (p : ↥(HarmonicYoungSpace mu)), (gtSelectedPhysicalAxisCompression low row) ((AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hgram) p) ∈ (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hgram).range) (p : ↥(HarmonicYoungSpace mu)) : (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise low hdom row (Fin.last n)) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p)) = (ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row * ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * HigherChannel.plusProbability (n + 1) low mu row) • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedPhysicalAxisRange.projectedCoordinateLower_canonicalGelfandTsetlinFibre_mem_range_of_strongStable {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hnstrong : 2 * (r + 1) + 5 ≤ n + 1) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hlowGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (hhighGram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherChannel.raiseWeight low row) mu hhigh) (p : ↥(HarmonicYoungSpace mu)) : (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre (HigherChannel.raiseWeight low row) mu hhigh hhighGram) p) ∈ (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hlowGram).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedPhysicalAxisRange.projectedCoordinateLower_reverseInterlacingHarmonicBranch_mem_range_of_strongStable {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hnstrong : 2 * (r + 1) + 5 ≤ n + 1) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (p : ↥(HarmonicYoungSpace mu)) : (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch (HigherChannel.raiseWeight low row) mu hhigh) p) ∈ (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedPhysicalAxisRange.projectedCoordinateRaise_reverseInterlacingHarmonicBranch_mem_range {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (p : ↥(HarmonicYoungSpace mu)) : (projectedCoordinateRaise (HigherChannel.raiseWeight low row) low ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p) ∈ (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch (HigherChannel.raiseWeight low row) mu hhigh).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedPhysicalAxisRange.gtSelectedPhysicalAxisCompression_canonicalFibre_mem_range_of_strongStable {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hnstrong : 2 * (r + 1) + 5 ≤ n + 1) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (p : ↥(HarmonicYoungSpace mu)) : (AllRankGTSelectedProjectorCompression.gtSelectedPhysicalAxisCompression low row) ((AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hgram) p) ∈ (AllRankGelfandTsetlinCanonicalFibre.canonicalGelfandTsetlinFibre low mu hlow hgram).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedPhysicalAxisRange.reverseInterlacing_projectedCoordinateLower_sameAxis_eq_plusProbability_of_minor_of_strongStable {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 2)) (hnstrong : 2 * (r + 1) + 5 ≤ n + 1) (hlow : HigherRepresentationGraph.Interlaces low mu) (hhigh : HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight low row) mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu hlow) (hfinite : HigherChannel.FiniteInterlacing (n + 1) low mu) (hdom : Antitone low) (hminor : ∀ (p q : ↥(HarmonicYoungSpace mu)), AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor low mu hlow hgram p q = Polynomial.C (inner ℝ p q) * HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu)) (hselected : ∀ (p : ↥(HarmonicYoungSpace mu)), (AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector low (row, true)) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor low mu hlow hgram) p) = (AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector low row) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor low mu hlow hgram) p)) (p : ↥(HarmonicYoungSpace mu)) : (projectedCoordinateLower low (HigherChannel.raiseWeight low row) ⋯ row ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n))) ((AllRankRawProjectedRaiseMickelsson.arbitraryRowSameAxisHarmonicRaise low hdom row (Fin.last n)) ((ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p)) = (ArbitraryRowAxialAdjointGram.arbitraryRowAxialLowerScalar low row * ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight low row) row * HigherChannel.plusProbability (n + 1) low mu row) • (ArbitraryRankGelfandTsetlinHarmonicIsometry.reverseInterlacingHarmonicBranch low mu hlow) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankCanonicalBoxFischerRecurrenceOfCharacteristicMinor.canonicalBoxAdjacentFischerRecurrence_of_minor_of_strongStable {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ) (hstable : ∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing (n + 1) (HigherHierarchy.RectangularVertices.signature a (n + 1) v) (HigherChannel.flooredCoordinates b (n + 1))) (hgram : ∀ (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m), AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram (HigherYoungActualGraphAssembly.boxSignature a (n + 1) i) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯) (low high : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (row : Fin (r + 2)) (hrow : HigherYoungActualGraphAssembly.boxSignature a (n + 1) high = HigherChannel.raiseWeight (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) (hnstrong : 2 * (r + 1) + 5 ≤ n + 1) (hminor : ∀ (p q : ↥(HarmonicYoungSpace (HigherHierarchy.Weyl.flooredWeight b (n + 1)))), AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯ ⋯ p q = Polynomial.C (inner ℝ p q) * HigherChannel.channelNumeratorPolynomial (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) (HigherHierarchy.Weyl.flooredWeight b (n + 1)))) (hselected : ∀ (p : ↥(HarmonicYoungSpace (HigherHierarchy.Weyl.flooredWeight b (n + 1)))), (AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) (row, true)) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯ ⋯) p) = (AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) row) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor (HigherYoungActualGraphAssembly.boxSignature a (n + 1) low) (HigherHierarchy.Weyl.flooredWeight b (n + 1)) ⋯ ⋯) p)) : AllRankCanonicalBoxActualForward.CanonicalBoxAdjacentFischerRecurrence a b hstable hgram low high row

def MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient (n : ℕ) (z j : ℤ) : ℤ

The difference of orthogonal complete symmetric coefficients at indices z + j and z - j - 2 used in the tensor Pieri formula.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_row_shift (n : ℕ) (z j : ℤ) : orthogonalTensorPieriCoefficient n (z + 1) j + orthogonalTensorPieriCoefficient n (z - 1) j = orthogonalTensorPieriCoefficient n z (j + 1) + orthogonalTensorPieriCoefficient n z (j - 1)

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_neg_one (n : ℕ) (z : ℤ) : orthogonalTensorPieriCoefficient n z (-1) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_padded_zero_lt (n r j : ℕ) (hj : j < r) : orthogonalTensorPieriCoefficient n (-↑r) ↑j = 0

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_padded_zero_self (n r : ℕ) : orthogonalTensorPieriCoefficient n (-↑r) ↑r = 1

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_padded_zero_succ (n r : ℕ) : orthogonalTensorPieriCoefficient n (-↑r) ↑(r + 1) = ↑n

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_padded_zero_fin (n r : ℕ) (j : Fin (r + 1)) : orthogonalTensorPieriCoefficient n (-↑r) ↑↑j = if ↑j = r then 1 else 0

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_padded_zero_pred_fin (n r : ℕ) (j : Fin (r + 1)) : orthogonalTensorPieriCoefficient n (-↑r - 1) ↑↑j = 0

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_eq_matrix {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam i j = orthogonalTensorPieriCoefficient n (↑(lam i) - ↑↑i) ↑↑j

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_raise_row {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n (Function.update lam i (lam i + 1)) i j = orthogonalTensorPieriCoefficient n (↑(lam i) - ↑↑i + 1) ↑↑j

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_lower_row {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) (hi : 0 < lam i) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n (Function.update lam i (lam i - 1)) i j = orthogonalTensorPieriCoefficient n (↑(lam i) - ↑↑i - 1) ↑↑j

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient_update_row_ne {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i ell j : Fin (r + 1)) (m : ℕ) (hi : i ≠ ell) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n (Function.update lam ell m) i j = HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam i j

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriInvalidRows.orthogonalJacobiTrudiMatrix_raiseWeight_eq_updateRow {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n (HigherChannel.raiseWeight lam i) = (HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).updateRow i fun (j : Fin (r + 1)) => HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient n (↑(lam i) - ↑↑i + 1) ↑↑j

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriInvalidRows.orthogonalJacobiTrudiMatrix_lowered_eq_updateRow {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) (hi : 0 < lam i) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam i) = (HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).updateRow i fun (j : Fin (r + 1)) => HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient n (↑(lam i) - ↑↑i - 1) ↑↑j

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriInvalidRows.orthogonalJacobiTrudiDimension_raiseWeight_eq_zero_of_not_antitone {r : ℕ} (n : ℕ) {lam : Fin (r + 1) → ℕ} (hlam : Antitone lam) (i : Fin (r + 1)) (hbad : ¬Antitone (HigherChannel.raiseWeight lam i)) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n (HigherChannel.raiseWeight lam i) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriInvalidRows.orthogonalJacobiTrudiDimension_lowered_eq_zero_of_not_antitone {r : ℕ} (n : ℕ) {lam : Fin (r + 1) → ℕ} (hlam : Antitone lam) (i : Fin (r + 1)) (hbad : ¬Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam i)) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam i) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriInvalidRows.orthogonalJacobiTrudiMatrix_signed_lower_update_det_eq_zero {r : ℕ} (n : ℕ) {lam : Fin (r + 1) → ℕ} (hlam : Antitone lam) (i : Fin (r + 1)) (hi : lam i = 0) : ((HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).updateRow i fun (j : Fin (r + 1)) => HigherYoungAllRankOrthogonalTensorPieriCoefficient.orthogonalTensorPieriCoefficient n (↑(lam i) - ↑↑i - 1) ↑↑j).det = 0

def MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriRowFiltering.orthogonalTensorPieriRaiseRow {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : Fin (r + 1) → ℤ

The tensor Pieri coefficient row obtained by raising the shifted weight coordinate lam i - i by one.

Equations

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

def MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriRowFiltering.orthogonalTensorPieriLowerRow {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : Fin (r + 1) → ℤ

The tensor Pieri coefficient row obtained by lowering the shifted weight coordinate lam i - i by one.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriRowFiltering.sum_eq_subtype_of_eq_zero {ι : Type u_1} {A : Type u_2} [Fintype ι] [AddCommMonoid A] (P : ι → Prop) [DecidablePred P] (f : ι → A) (hzero : ∀ (i : ι), ¬P i → f i = 0) : ∑ i : ι, f i = ∑ i : { i : ι // P i }, f ↑i

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriRowFiltering.sum_det_updateRow_raise_eq_dominant_subtype {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (hlam : Antitone lam) : ∑ i : Fin (r + 1), ((HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).updateRow i (orthogonalTensorPieriRaiseRow n lam i)).det = ∑ i : { i : Fin (r + 1) // Antitone (HigherChannel.raiseWeight lam i) }, HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n (HigherChannel.raiseWeight lam ↑i)

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriRowFiltering.sum_det_updateRow_lower_eq_positive_dominant_subtype {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (hlam : Antitone lam) : ∑ i : Fin (r + 1), ((HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).updateRow i (orthogonalTensorPieriLowerRow n lam i)).det = ∑ i : { i : Fin (r + 1) // 0 < lam i ∧ Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam i) }, HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam ↑i)

def MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriRaiseRow {r : ℕ} (lam : Fin (r + 1) → ℕ) : Type

The padded pieri raise row used in the spherical-code argument.

Equations

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

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriRaiseRowFintype {r : ℕ} (lam : Fin (r + 1) → ℕ) : Fintype (PaddedPieriRaiseRow lam)

Equations

• MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriRaiseRowFintype lam = id inferInstance

def MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriLowerRow {r : ℕ} (lam : Fin (r + 1) → ℕ) : Type

The padded pieri lower row used in the spherical-code argument.

Equations

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

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriLowerRowFintype {r : ℕ} (lam : Fin (r + 1) → ℕ) : Fintype (PaddedPieriLowerRow lam)

Equations

• MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriLowerRowFintype lam = id inferInstance

def MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel {r : ℕ} (lam : Fin (r + 1) → ℕ) : Type

The padded pieri channel used in the spherical-code argument.

Equations

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

@[instance_reducible]

noncomputable instance MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriChannelFintype {r : ℕ} (lam : Fin (r + 1) → ℕ) : Fintype (PaddedPieriChannel lam)

Equations

• MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriChannelFintype lam = id inferInstance

def MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource {r : ℕ} (lam : Fin (r + 1) → ℕ) : PaddedPieriChannel lam → Fin (r + 1) → ℕ

The padded pieri source used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource_inr {r : ℕ} (lam : Fin (r + 1) → ℕ) (i : PaddedPieriLowerRow lam) : paddedPieriSource lam (Sum.inr i) = HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam ↑i

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.raiseWeight_row_injective {r : ℕ} (lam : Fin (r + 1) → ℕ) : Function.Injective (HigherChannel.raiseWeight lam)

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.loweredInternalYoungWeight_row_injective_of_positive {r : ℕ} (lam : Fin (r + 1) → ℕ) {i j : Fin (r + 1)} (hi : 0 < lam i) (hij : HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam i = HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam j) : i = j

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.raiseWeight_ne_loweredInternalYoungWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (i j : Fin (r + 1)) : HigherChannel.raiseWeight lam i ≠ HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam j

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource_injective {r : ℕ} (lam : Fin (r + 1) → ℕ) : Function.Injective (paddedPieriSource lam)

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.raiseWeight_loweredInternalYoungWeight {r : ℕ} (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) (hi : 0 < lam i) : HigherChannel.raiseWeight (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam i) i = lam

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource_isOneBoxNeighbor {r : ℕ} (lam : Fin (r + 1) → ℕ) (i : PaddedPieriChannel lam) : HigherHarmonicYoung.MixedSignature.IsAllRankOneBoxNeighbor lam (paddedPieriSource lam i)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankPaddedLowerClebschIntertwining.normalizedPaddedPieriLower {r n : ℕ} (target : Fin (r + 1) → ℕ) (hdominant : Antitone target) (row : Fin (r + 1)) (hsource : Antitone (HigherChannel.raiseWeight target row)) : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight target row)) →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)

The normalized padded pieri lower used in the spherical-code argument.

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankPaddedLowerClebschIntertwining.normalizedPaddedPieriLower_toLinearMap {r n : ℕ} (target : Fin (r + 1) → ℕ) (hdominant : Antitone target) (row : Fin (r + 1)) (hsource : Antitone (HigherChannel.raiseWeight target row)) : (normalizedPaddedPieriLower target hdominant row hsource).toLinearMap = (√(ArbitraryRankInternalRowLowerGram.internalRowLowerGramScalar (HigherChannel.raiseWeight target row) row))⁻¹ • youngClebschLower target (HigherChannel.raiseWeight target row) ⋯ row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankPaddedLowerClebschIntertwining.normalizedPaddedPieriLower_rotation_intertwine {r n : ℕ} (target : Fin (r + 1) → ℕ) (hdominant : Antitone target) (row : Fin (r + 1)) (hsource : Antitone (HigherChannel.raiseWeight target row)) (i j : Fin n) : (normalizedPaddedPieriLower target hdominant row hsource).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation (HigherChannel.raiseWeight target row) i j = ClebschRotation.tensorAmbientRotation target i j ∘ₗ (normalizedPaddedPieriLower target hdominant row hsource).toLinearMap

theorem MetricCodes.Spherical.HigherYoungAllRankGTAppendedRowLegality.appendZeroWeight_antitone {r : ℕ} (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedRowExclusion.appendedRowFullBranchSignature_terminal_pos {r : ℕ} (lam : Fin (r + 1) → ℕ) (nu : BranchingDimension.FullBranchWeight (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 1)))) : 0 < BranchingDimension.fullBranchSignature nu (Fin.last r).castSucc

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedRowExclusion.appendedRowFullBranchSignature_ne_appendZero {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (nu : BranchingDimension.FullBranchWeight (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) : BranchingDimension.fullBranchSignature nu ≠ ThreeRowYoungBranching.appendZeroWeight (ThreeRowYoungBranching.appendZeroWeight mu)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankTensorClebschCompleteness.actualTensorClebsch_iSup_range_eq_top_of_finrank {ι : Type u_1} [Fintype ι] {r n : ℕ} (hn : 2 * r + 2 ≤ n) (target : Fin (r + 1) → ℕ) (hdom : Antitone target) (source : ι → Fin (r + 1) → ℕ) (hsource : ∀ (i : ι), MixedSignature.IsAllRankOneBoxNeighbor target (source i)) (hinj : Function.Injective source) (A : (i : ι) → ↥(HarmonicYoungSpace (source i)) →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hA : ∀ (i : ι) (a b : Fin n), (A i).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation (source i) a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ (A i).toLinearMap) (hdim : n * Module.finrank ℝ ↥(HarmonicYoungSpace target) = ∑ i : ι, Module.finrank ℝ ↥(HarmonicYoungSpace (source i))) : ⨆ (i : ι), (A i).range = ⊤

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankTensorClebschCompleteness.orthogonalCompleteBranch_mem_selected_iSup {ι : Type u_1} {V : Type u_2} [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (A : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((A i) p) ((A j) q) = 0) (hdim : Module.finrank ℝ V = ∑ i : ι, Module.finrank ℝ (E i)) (P : ι → Prop) (x : V) (hexcluded : ∀ (i : ι), ¬P i → ∀ (y : E i), inner ℝ x ((A i) y) = 0) : x ∈ ⨆ (i : { i : ι // P i }), (A ↑i).range

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan {r n : ℕ} (lam : Fin (r + 1) → ℕ) : Submodule ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam))

The gt signed eigenvector span used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolventSpectral.gtChannelCharacteristic_eval_signedNode {r n : ℕ} (lam : Fin (r + 1) → ℕ) (z : Fin (r + 1) × Bool) : Polynomial.eval (HigherChannel.signedNode (HigherChannel.ambientShift n lam) z) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial n lam) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolventSpectral.gtChannelCharacteristic_aeval_apply_eigen {r n : ℕ} (lam : Fin (r + 1) → ℕ) (z : Fin (r + 1) × Bool) (v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (hv : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) v = HigherChannel.signedNode (HigherChannel.ambientShift n lam) z • v) : ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial n lam)) v = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolventSpectral.gtSignedEigenspace_le_characteristic_ker {r n : ℕ} (lam : Fin (r + 1) → ℕ) (z : Fin (r + 1) × Bool) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam).eigenspace (HigherChannel.signedNode (HigherChannel.ambientShift n lam) z) ≤ LinearMap.ker ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial n lam))

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan_le_characteristic_ker {r n : ℕ} (lam : Fin (r + 1) → ℕ) : gtSignedEigenvectorSpan lam ≤ LinearMap.ker ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial n lam))

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan_mem_of_orthogonalComplete_retained_channels {ι : Type u_1} [Fintype ι] {r n : ℕ} (lam : Fin (r + 1) → ℕ) (E : ι → Type u_2) [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (A : (i : ι) → E i →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((A i) p) ((A j) q) = 0) (hdim : Module.finrank ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) = ∑ i : ι, Module.finrank ℝ (E i)) (P : ι → Prop) (heigen : ∀ (i : ι), P i → ∃ (z : Fin (r + 1) × Bool), ∀ (q : E i), (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((A i) q) = HigherChannel.signedNode (HigherChannel.ambientShift n lam) z • (A i) q) (v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (hexcluded : ∀ (i : ι), ¬P i → ∀ (q : E i), inner ℝ v ((A i) q) = 0) : v ∈ gtSignedEigenvectorSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan_gtRelativeCasimir_mem {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (hv : v ∈ gtSignedEigenvectorSpan lam) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) v ∈ gtSignedEigenvectorSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan_gtRelativeCasimir_iterate_mem {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (hv : v ∈ gtSignedEigenvectorSpan lam) (k : ℕ) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ^ k) v ∈ gtSignedEigenvectorSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolventSpectral.gtChannelCharacteristic_aeval_apply_iterate_eq_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (hv : v ∈ gtSignedEigenvectorSpan lam) (k : ℕ) : ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial n lam)) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ^ k) v) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCompressedResolventSpectral.gtChannelCharacteristic_aeval_apply_canonicalAxis_iterate_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (p : ↥(HarmonicYoungSpace mu)) (hp : (AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p ∈ gtSignedEigenvectorSpan lam) (k : ℕ) : ((Polynomial.aeval (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)) (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) ((AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ^ k) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p)) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriBoundaryColumn.det_updateCol_of_row_delta {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι R) (i : ι) (v : ι → R) (hrow : ∀ (j : ι), M i j = if j = i then 1 else 0) : (M.updateCol i v).det = v i * M.det

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriBoundaryColumn.det_updateCol_last_of_lastRow_delta {R : Type u_1} [CommRing R] {r : ℕ} (M : Matrix (Fin (r + 1)) (Fin (r + 1)) R) (v : Fin (r + 1) → R) (hrow : ∀ (j : Fin (r + 1)), M (Fin.last r) j = if j = Fin.last r then 1 else 0) : (M.updateCol (Fin.last r) v).det = v (Fin.last r) * M.det

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.orthogonalTensorPieriSignedShiftMatrix {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : Matrix (Fin (r + 1)) (Fin (r + 1)) ℤ

The matrix whose rows sum the raised and lowered tensor Pieri coefficient rows.

Equations

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

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.orthogonalTensorPieriNextColumn {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (j : Fin (r + 1)) : Fin (r + 1) → ℤ

The tensor Pieri coefficient column with the column index shifted up by one.

Equations

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

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.orthogonalTensorPieriPrevColumn {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (j : Fin (r + 1)) : Fin (r + 1) → ℤ

The tensor Pieri coefficient column with the column index shifted down by one.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.orthogonalTensorPieriSignedShiftMatrix_column {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (j : Fin (r + 1)) : (fun (i : Fin (r + 1)) => orthogonalTensorPieriSignedShiftMatrix n lam i j) = orthogonalTensorPieriNextColumn n lam j + orthogonalTensorPieriPrevColumn n lam j

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.det_updateCol_orthogonalTensorPieriNextColumn_eq_zero {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (j : Fin (r + 1)) (hj : j ≠ Fin.last r) : ((HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).updateCol j (orthogonalTensorPieriNextColumn n lam j)).det = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.det_updateCol_orthogonalTensorPieriPrevColumn_eq_zero {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (j : Fin (r + 1)) : ((HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).updateCol j (orthogonalTensorPieriPrevColumn n lam j)).det = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.sum_det_updateCol_orthogonalTensorPieriSignedShiftMatrix {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) : ∑ j : Fin (r + 1), ((HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).updateCol j fun (i : Fin (r + 1)) => orthogonalTensorPieriSignedShiftMatrix n lam i j).det = ((HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).updateCol (Fin.last r) (orthogonalTensorPieriNextColumn n lam (Fin.last r))).det

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.sum_det_updateRow_eq_sum_det_updateCol {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing R] (M B : Matrix ι ι R) : ∑ i : ι, (M.updateRow i (B i)).det = ∑ j : ι, (M.updateCol j fun (i : ι) => B i j).det

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.orthogonalJacobiTrudiMatrix_lastRow_delta {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (hzero : lam (Fin.last r) = 0) (j : Fin (r + 1)) : HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam (Fin.last r) j = if j = Fin.last r then 1 else 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.orthogonalTensorPieriNextColumn_last {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (hzero : lam (Fin.last r) = 0) : orthogonalTensorPieriNextColumn n lam (Fin.last r) (Fin.last r) = ↑n

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.sum_det_updateRow_orthogonalTensorPieriSignedShiftMatrix {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (hzero : lam (Fin.last r) = 0) : ∑ i : Fin (r + 1), ((HigherWeylBinomialDeterminant.orthogonalJacobiTrudiMatrix n lam).updateRow i (orthogonalTensorPieriSignedShiftMatrix n lam i)).det = ↑n * HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.orthogonalJacobiTrudiDimension_tensorPieri {r : ℕ} (n : ℕ) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hzero : lam (Fin.last r) = 0) : ∑ i : { i : Fin (r + 1) // Antitone (HigherChannel.raiseWeight lam i) }, HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n (HigherChannel.raiseWeight lam ↑i) + ∑ i : { i : Fin (r + 1) // 0 < lam i ∧ Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam i) }, HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam ↑i) = ↑n * HigherWeylBinomialDeterminant.orthogonalJacobiTrudiDimension n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.weyl_tensorPieri_dimension {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hzero : lam (Fin.last r) = 0) : ∑ i : { i : Fin (r + 1) // Antitone (HigherChannel.raiseWeight lam i) }, HigherHierarchy.Weyl.dimension n (HigherChannel.raiseWeight lam ↑i) + ∑ i : { i : Fin (r + 1) // 0 < lam i ∧ Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam i) }, HigherHierarchy.Weyl.dimension n (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam ↑i) = ↑n * HigherHierarchy.Weyl.dimension n lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankOrthogonalTensorPieriDimension.finrank_harmonicYoung_tensorPieri {r n : ℕ} (hn : 2 * r + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone lam) (hzero : lam (Fin.last r) = 0) : ∑ i : { i : Fin (r + 1) // Antitone (HigherChannel.raiseWeight lam i) }, Module.finrank ℝ ↥(HarmonicYoungSpace (HigherChannel.raiseWeight lam ↑i)) + ∑ i : { i : Fin (r + 1) // 0 < lam i ∧ Antitone (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam i) }, Module.finrank ℝ ↥(HarmonicYoungSpace (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam ↑i)) = n * Module.finrank ℝ ↥(HarmonicYoungSpace lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTensorPieriNormalizedChannels.existsNormalizedPaddedPieriRaising_metriccodes2_9210a270 {r n : ℕ} (hn : 2 * r + 4 ≤ n) (target : Fin (r + 1) → ℕ) (hdom : Antitone target) (row : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriLowerRow target) : ∃ (A : ↥(HarmonicYoungSpace (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight target ↑row)) →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)), ∀ (a b : Fin n), A.toLinearMap ∘ₗ MixedSignature.youngAmbientRotation (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight target ↑row) a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ A.toLinearMap

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTensorPieriNormalizedChannels.normalizedPaddedPieriRaising {r n : ℕ} (hn : 2 * r + 4 ≤ n) (target : Fin (r + 1) → ℕ) (hdom : Antitone target) (row : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriLowerRow target) : ↥(HarmonicYoungSpace (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight target ↑row)) →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)

A chosen normalized isometric Pieri raising map from the lowered internal Young weight into the tensor representation.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTensorPieriNormalizedChannels.normalizedPaddedPieriRaising hn target hdom row = Classical.choose ⋯

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTensorPieriNormalizedChannels.normalizedPaddedPieriRaising_rotation_intertwine {r n : ℕ} (hn : 2 * r + 4 ≤ n) (target : Fin (r + 1) → ℕ) (hdom : Antitone target) (row : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriLowerRow target) (a b : Fin n) : (normalizedPaddedPieriRaising hn target hdom row).toLinearMap ∘ₗ MixedSignature.youngAmbientRotation (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight target ↑row) a b = ClebschRotation.tensorAmbientRotation target a b ∘ₗ (normalizedPaddedPieriRaising hn target hdom row).toLinearMap

noncomputable def MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieriChannel {r n : ℕ} (hn : 2 * r + 4 ≤ n) (target : Fin (r + 1) → ℕ) (hdom : Antitone target) (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel target) : ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource target i)) →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HigherHarmonicYoung.HarmonicYoungSpace target)

The padded orthogonal tensor pieri channel used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieriChannel_rotation_intertwine {r n : ℕ} (hn : 2 * r + 4 ≤ n) (target : Fin (r + 1) → ℕ) (hdom : Antitone target) (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel target) (a b : Fin n) : (paddedOrthogonalTensorPieriChannel hn target hdom i).toLinearMap ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource target i) a b = HigherHarmonicYoung.ClebschRotation.tensorAmbientRotation target a b ∘ₗ (paddedOrthogonalTensorPieriChannel hn target hdom i).toLinearMap

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieri_finrank {r n : ℕ} (hn : 2 * r + 4 ≤ n) (target : Fin (r + 1) → ℕ) (hdom : Antitone target) (hzero : target (Fin.last r) = 0) : n * Module.finrank ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace target) = ∑ i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel target, Module.finrank ℝ ↥(HigherHarmonicYoung.HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource target i))

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieri_iSup_range_eq_top {r n : ℕ} (hn : 2 * r + 4 ≤ n) (target : Fin (r + 1) → ℕ) (hdom : Antitone target) (hzero : target (Fin.last r) = 0) : ⨆ (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel target), (paddedOrthogonalTensorPieriChannel hn target hdom i).range = ⊤

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankZeroRowTensorCasimirConjugacy.allRankCasimirEigenvalue_appendZeroWeight {r n : ℕ} (lam : Fin (r + 1) → ℕ) : MixedSignature.allRankCasimirEigenvalue n (ThreeRowYoungBranching.appendZeroWeight lam) = MixedSignature.allRankCasimirEigenvalue n lam

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

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

Equations

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

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankZeroRowTensorCasimirConjugacy.zeroRowTensorIsometryEquiv_tmul {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace lam)) : (zeroRowTensorIsometryEquiv lam) (v ⊗ₜ[ℝ] p) = v ⊗ₜ[ℝ] (ThreeRowYoungBranching.appendZeroRowIsometryEquiv lam) p

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankZeroRowTensorCasimirConjugacy.zeroRowTensorIsometryEquiv_symm_tmul {r n : ℕ} (lam : Fin (r + 1) → ℕ) (v : SpherePacking.Euclidean n) (p : ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight lam))) : (zeroRowTensorIsometryEquiv lam).symm (v ⊗ₜ[ℝ] p) = v ⊗ₜ[ℝ] (ThreeRowYoungBranching.appendZeroRowIsometryEquiv lam).symm p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankZeroRowTensorCasimirConjugacy.zeroRowTensorIsometryEquiv_rotation_intertwine {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) : ↑(zeroRowTensorIsometryEquiv lam).toLinearEquiv ∘ₗ ClebschRotation.tensorAmbientRotation lam a b = ClebschRotation.tensorAmbientRotation (ThreeRowYoungBranching.appendZeroWeight lam) a b ∘ₗ ↑(zeroRowTensorIsometryEquiv lam).toLinearEquiv

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankZeroRowTensorCasimirConjugacy.zeroRowTensorIsometryEquiv_symm_rotation_intertwine {r n : ℕ} (lam : Fin (r + 1) → ℕ) (a b : Fin n) : ↑(zeroRowTensorIsometryEquiv lam).symm.toLinearEquiv ∘ₗ ClebschRotation.tensorAmbientRotation (ThreeRowYoungBranching.appendZeroWeight lam) a b = ClebschRotation.tensorAmbientRotation lam a b ∘ₗ ↑(zeroRowTensorIsometryEquiv lam).symm.toLinearEquiv

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankZeroRowTensorCasimirConjugacy.zeroRowTensorIsometryEquiv_symm_tensorCasimir_intertwine {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ↑(zeroRowTensorIsometryEquiv lam).symm.toLinearEquiv ∘ₗ AllRankGTRelativeCasimirProjector.gtTensorCasimir (ThreeRowYoungBranching.appendZeroWeight lam) = AllRankGTRelativeCasimirProjector.gtTensorCasimir lam ∘ₗ ↑(zeroRowTensorIsometryEquiv lam).symm.toLinearEquiv

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankZeroRowTensorCasimirConjugacy.zeroRowTensorIsometryEquiv_symm_relativeCasimir_intertwine {r n : ℕ} (lam : Fin (r + 1) → ℕ) : ↑(zeroRowTensorIsometryEquiv lam).symm.toLinearEquiv ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir (ThreeRowYoungBranching.appendZeroWeight lam) = AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ ↑(zeroRowTensorIsometryEquiv lam).symm.toLinearEquiv

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.ambientShift_appendZeroWeight_castSucc {r n : ℕ} (lam : Fin (r + 1) → ℕ) (i : Fin (r + 1)) : HigherChannel.ambientShift n (ThreeRowYoungBranching.appendZeroWeight lam) i.castSucc = HigherChannel.ambientShift n lam i

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriChannel {r : ℕ} (lam : Fin (r + 1) → ℕ) : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam) → Prop

The retained padded pieri channel used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriChannel lam (Sum.inl row) = (↑row ≠ Fin.last (r + 1))
• MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriChannel lam (Sum.inr val) = True

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.paddedPieriLowerRow_ne_last {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriLowerRow (ThreeRowYoungBranching.appendZeroWeight lam)) : ↑row ≠ Fin.last (r + 1)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.raiseWeight_appendZeroWeight_castSucc {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) row.castSucc = ThreeRowYoungBranching.appendZeroWeight (HigherChannel.raiseWeight lam row)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.loweredInternalYoungWeight_appendZeroWeight_castSucc {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight (ThreeRowYoungBranching.appendZeroWeight lam) row.castSucc = ThreeRowYoungBranching.appendZeroWeight (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam row)

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriSignedNode {r : ℕ} (lam : Fin (r + 1) → ℕ) : { i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam) // retainedPaddedPieriChannel lam i } → Fin (r + 1) × Bool

The retained padded pieri signed node used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriSignedNode lam ⟨Sum.inl row, hrow⟩ = ((↑row).castPred hrow, true)
• MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriSignedNode lam ⟨Sum.inr row, property⟩ = ((↑row).castPred ⋯, false)

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriPhysicalSource {r : ℕ} (lam : Fin (r + 1) → ℕ) : { i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam) // retainedPaddedPieriChannel lam i } → Fin (r + 1) → ℕ

The retained padded pieri physical source used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.paddedPieriSource_retained_eq_appendZero {r : ℕ} (lam : Fin (r + 1) → ℕ) (i : { j : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam) // retainedPaddedPieriChannel lam j }) : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) ↑i = ThreeRowYoungBranching.appendZeroWeight (retainedPaddedPieriPhysicalSource lam i)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriSignedNode_injective {r : ℕ} (lam : Fin (r + 1) → ℕ) : Function.Injective (retainedPaddedPieriSignedNode lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.signedNode_appendZeroWeight_retained_raise {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriRaiseRow (ThreeRowYoungBranching.appendZeroWeight lam)) (hrow : ↑row ≠ Fin.last (r + 1)) : HigherChannel.signedNode (HigherChannel.ambientShift n (ThreeRowYoungBranching.appendZeroWeight lam)) (↑row, true) = HigherChannel.signedNode (HigherChannel.ambientShift n lam) (retainedPaddedPieriSignedNode lam ⟨Sum.inl row, hrow⟩)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.signedNode_appendZeroWeight_retained_lower {r n : ℕ} (lam : Fin (r + 1) → ℕ) (row : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriLowerRow (ThreeRowYoungBranching.appendZeroWeight lam)) : HigherChannel.signedNode (HigherChannel.ambientShift n (ThreeRowYoungBranching.appendZeroWeight lam)) (↑row, false) = HigherChannel.signedNode (HigherChannel.ambientShift n lam) (retainedPaddedPieriSignedNode lam ⟨Sum.inr row, trivial⟩)

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.zeroRowTransportPaddedPieriChannel {r n : ℕ} (lam : Fin (r + 1) → ℕ) {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : E →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight lam))) : E →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)

The zero row transport padded pieri channel used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.zeroRowTransportPaddedPieriChannel_eigen_of_intertwine {r n : ℕ} (lam : Fin (r + 1) → ℕ) {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : E →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight lam))) (hconj : AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam ∘ₗ ↑(AllRankZeroRowTensorCasimirConjugacy.zeroRowTensorIsometryEquiv lam).symm.toLinearEquiv = ↑(AllRankZeroRowTensorCasimirConjugacy.zeroRowTensorIsometryEquiv lam).symm.toLinearEquiv ∘ₗ AllRankGTRelativeCasimirProjector.gtRelativeCasimir (ThreeRowYoungBranching.appendZeroWeight lam)) (c : ℝ) (p : E) (heigen : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir (ThreeRowYoungBranching.appendZeroWeight lam)) (A p) = c • A p) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((zeroRowTransportPaddedPieriChannel lam A) p) = c • (zeroRowTransportPaddedPieriChannel lam A) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirZeroRowTransport.transportedPaddedPieriChannel_eigen_of_retained {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (i : { j : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam) // retainedPaddedPieriChannel lam j }) (p : ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) ↑i))) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) ((zeroRowTransportPaddedPieriChannel lam (HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieriChannel hn (ThreeRowYoungBranching.appendZeroWeight lam) hdom ↑i)) p) = HigherChannel.signedNode (HigherChannel.ambientShift n lam) (retainedPaddedPieriSignedNode lam i) • (zeroRowTransportPaddedPieriChannel lam (HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieriChannel hn (ThreeRowYoungBranching.appendZeroWeight lam) hdom ↑i)) p

noncomputable def MetricCodes.Spherical.HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode {r : ℕ} (rho : ℝ) (M : Fin r → ℝ) : Unit ⊕ Fin r × Bool → ℝ

The gt stabilizer arrowhead node used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode rho M (Sum.inl val) = -rho
• MetricCodes.Spherical.HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode rho M (Sum.inr (m, true)) = M m - 1 / 2
• MetricCodes.Spherical.HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode rho M (Sum.inr (m, false)) = -M m - 1 / 2

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode_pos {r : ℕ} (rho : ℝ) (M : Fin r → ℝ) (m : Fin r) : gtStabilizerArrowheadNode rho M (Sum.inr (m, true)) = M m - 1 / 2

@[simp]

theorem MetricCodes.Spherical.HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode_neg {r : ℕ} (rho : ℝ) (M : Fin r → ℝ) (m : Fin r) : gtStabilizerArrowheadNode rho M (Sum.inr (m, false)) = -M m - 1 / 2

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

The gt stabilizer arrowhead minor used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadMinor_eq_channelNumerator {r : ℕ} (rho : ℝ) (M : Fin r → ℝ) : gtStabilizerArrowheadMinor rho M = HigherChannel.channelNumeratorPolynomial rho M

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.not_interlaces_raiseWeight_iff_upperWall {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (row : Fin (r + 1)) : ¬HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row) ↔ lam row.castSucc = mu row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.not_interlaces_loweredInternalYoungWeight_iff_lowerWall {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (row : Fin (r + 1)) (hpositive : 0 < mu row) : ¬HigherRepresentationGraph.Interlaces lam (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight mu row) ↔ lam row.succ = mu row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.negativeStabilizerNode_eq_negativeAmbient_of_upperWall {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hwall : lam row.castSucc = mu row) : HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false)) = HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) (row.castSucc, false)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.positiveStabilizerNode_eq_positiveAmbient_of_lowerWall {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hwall : lam row.succ = mu row) : HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true)) = HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) (row.succ, true)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.not_interlaces_raiseAmbient_of_lowerWall {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hwall : lam row.succ = mu row) : ¬HigherRepresentationGraph.Interlaces (HigherChannel.raiseWeight lam row.succ) mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.not_interlaces_lowerAmbient_of_upperWall {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hwall : lam row.castSucc = mu row) (hpositive : 0 < lam row.castSucc) : ¬HigherRepresentationGraph.Interlaces (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight lam row.castSucc) mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.gtAxisCompressedCharacteristicMinor_eval_negativeStabilizerNode {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (row : Fin (r + 1)) (hbad : ¬HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false))) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = Polynomial.eval (HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) (row.castSucc, false)) (Polynomial.derivative (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) * AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (row.castSucc, false)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.lowerWall_of_invalid_lower_stabilizer {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (row : Fin (r + 1)) (hbad : mu row = 0 ∨ ¬HigherRepresentationGraph.Interlaces lam (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight mu row)) : lam row.succ = mu row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.gtAxisCompressedCharacteristicMinor_eval_positiveStabilizerNode {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (row : Fin (r + 1)) (hbad : mu row = 0 ∨ ¬HigherRepresentationGraph.Interlaces lam (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight mu row)) (p q : ↥(HarmonicYoungSpace mu)) : Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true))) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = Polynomial.eval (HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) lam) (row.succ, true)) (Polynomial.derivative (HigherYoungAllRankGTCharacteristicResidue.gtChannelCharacteristicPolynomial (n + 1) lam)) * AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (row.succ, true)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.gtAxisCompressedCharacteristicMinor_eval_negativeStabilizerNode_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (row : Fin (r + 1)) (hbad : ¬HigherRepresentationGraph.Interlaces lam (HigherChannel.raiseWeight mu row)) (p q : ↥(HarmonicYoungSpace mu)) (hzero : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (row.castSucc, false) = 0) : Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, false))) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidRowCharacteristicMinorVanishing.gtAxisCompressedCharacteristicMinor_eval_positiveStabilizerNode_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) lam mu) (row : Fin (r + 1)) (hbad : mu row = 0 ∨ ¬HigherRepresentationGraph.Interlaces lam (HigherYoungPenultimateRowProjectedLower.loweredInternalYoungWeight mu row)) (p q : ↥(HarmonicYoungSpace mu)) (hzero : AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedSignedProjectorCoefficient lam mu h hgram p q (row.succ, true) = 0) : Polynomial.eval (HigherYoungAllRankGTArrowheadSchurComplement.gtStabilizerArrowheadNode (HigherChannel.wallShift (n + 1) (r + 1)) (HigherChannel.stabilizerShift (n + 1) mu) (Sum.inr (row, true))) (AllRankGTAxisCompressedCharacteristicMinor.gtAxisCompressedCharacteristicMinor lam mu h hgram p q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankTensorClebschSpectralProjection.orthogonalChannelSelector_apply_eq_comp_adjoint_of_mem_span {ι : Type u_1} {V : Type u_2} [DecidableEq ι] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (A : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((A i) p) ((A j) q) = 0) (P : Module.End ℝ V) (selected : ι) (hselector : ∀ (j : ι) (p : E j), P ((A j) p) = if selected = j then (A j) p else 0) (x : V) (hx : x ∈ ⨆ (j : ι), (A j).range) : P x = ((A selected).toLinearMap ∘ₗ LinearMap.adjoint (A selected).toLinearMap) x

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankTensorClebschSpectralProjection.cartanCharacteristicProjector_eq_channel_comp_adjoint_of_complete {ι : Type u_1} {V : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (nodes : ι → ℝ) (hnode : Function.Injective nodes) (T : Module.End ℝ V) (A : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((A i) p) ((A j) q) = 0) (hcomplete : ⨆ (i : ι), (A i).range = ⊤) (heigen : ∀ (i : ι) (p : E i), T ((A i) p) = nodes i • (A i) p) (selected : ι) : AllRankCartanCharacteristicInterpolation.cartanCharacteristicInterpolationProjector nodes T selected = (A selected).toLinearMap ∘ₗ LinearMap.adjoint (A selected).toLinearMap

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAbsentSignedProjectorOnRetainedSpan.cartanCharacteristicProjector_apply_eq_zero_of_absent_eigenchannel_span {κ : Type u_1} {ι : Type u_2} {V : Type u_3} [Fintype κ] [DecidableEq κ] [AddCommGroup V] [Module ℝ V] {E : ι → Type u_4} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module ℝ (E i)] (nodes : κ → ℝ) (hnode : Function.Injective nodes) (T : Module.End ℝ V) (selected : κ) (channelIndex : ι → κ) (A : (i : ι) → E i →ₗ[ℝ] V) (heigen : ∀ (i : ι) (p : E i), T ((A i) p) = nodes (channelIndex i) • (A i) p) (habsent : ∀ (i : ι), selected ≠ channelIndex i) (x : V) (hx : x ∈ ⨆ (i : ι), (A i).range) : (AllRankCartanCharacteristicInterpolation.cartanCharacteristicInterpolationProjector nodes T selected) x = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAbsentSignedProjectorOnRetainedSpan.cartanCharacteristicProjector_apply_eq_zero_of_matching_adjoint_zero {κ : Type u_1} {ι : Type u_2} {V : Type u_3} [Fintype κ] [DecidableEq κ] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_4} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (nodes : κ → ℝ) (hnode : Function.Injective nodes) (T : Module.End ℝ V) (selected : κ) (channelIndex : ι → κ) (hindex : Function.Injective channelIndex) (A : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((A i) p) ((A j) q) = 0) (heigen : ∀ (i : ι) (p : E i), T ((A i) p) = nodes (channelIndex i) • (A i) p) (x : V) (hx : x ∈ ⨆ (i : ι), (A i).range) (hzero : ∀ (i : ι), channelIndex i = selected → (LinearMap.adjoint (A i).toLinearMap) x = 0) : (AllRankCartanCharacteristicInterpolation.cartanCharacteristicInterpolationProjector nodes T selected) x = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAbsentSignedProjectorOnRetainedSpan.gtCharacteristicProjector_apply_eq_zero_of_matching_adjoint_zero {r n : ℕ} (target : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (hfinite : HigherChannel.FiniteInterlacing n target mu) {ι : Type u_1} {E : ι → Type u_2} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (channelIndex : ι → Fin (r + 1) × Bool) (hindex : Function.Injective channelIndex) (A : (i : ι) → E i →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((A i) p) ((A j) q) = 0) (heigen : ∀ (i : ι) (p : E i), (AllRankGTRelativeCasimirProjector.gtRelativeCasimir target) ((A i) p) = HigherChannel.signedNode (HigherChannel.ambientShift n target) (channelIndex i) • (A i) p) (selected : Fin (r + 1) × Bool) (x : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace target)) (hx : x ∈ ⨆ (i : ι), (A i).range) (hzero : ∀ (i : ι), channelIndex i = selected → (LinearMap.adjoint (A i).toLinearMap) x = 0) : (AllRankGTRelativeCasimirProjector.gtCharacteristicProjector target selected) x = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidFullBranchExclusion.interlaces_of_fullBranchSignature_eq_appendZeroWeight {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (nu : BranchingDimension.FullBranchWeight lam) (hsignature : BranchingDimension.fullBranchSignature nu = ThreeRowYoungBranching.appendZeroWeight mu) : HigherRepresentationGraph.Interlaces lam mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidFullBranchExclusion.fullBranchSignature_ne_appendZeroWeight_of_not_interlaces {r : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hbad : ¬HigherRepresentationGraph.Interlaces lam mu) (nu : BranchingDimension.FullBranchWeight lam) : BranchingDimension.fullBranchSignature nu ≠ ThreeRowYoungBranching.appendZeroWeight mu

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTIllegalStabilizerIntertwiner.illegalYoungStabilizerIntertwiner_eq_zero {r n : ℕ} (S : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hn : 2 * (r + 2) + 2 ≤ n) (hdomS : Antitone S) (hdomMu : Antitone mu) (hbad : ¬HigherRepresentationGraph.Interlaces S mu) (A : ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight mu)) →ₗ[ℝ] ↥(HarmonicYoungSpace S)) (hA : ∀ (a b : Fin n), A ∘ₗ MixedSignature.youngAmbientRotation (ThreeRowYoungBranching.appendZeroWeight mu) a b = MixedSignature.youngAmbientRotation S a.castSucc b.castSucc ∘ₗ A) : A = 0

theorem MetricCodes.Spherical.HigherYoungAllRankGTAxisTensorRotationIntertwining.euclideanAmbientRotation_castSucc_last {n : ℕ} (a b : Fin n) : (HigherHarmonicYoung.ClebschRotation.euclideanAmbientRotation a.castSucc b.castSucc) ((EuclideanSpace.basisFun (Fin (n + 1)) ℝ) (Fin.last n)) = 0

theorem MetricCodes.Spherical.HigherYoungAllRankGTAxisTensorRotationIntertwining.canonicalGelfandTsetlinAxisTensor_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : HigherHarmonicYoung.AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (a b : Fin n) : HigherHarmonicYoung.AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram ∘ₗ HigherHarmonicYoung.MixedSignature.youngAmbientRotation mu a b = HigherHarmonicYoung.ClebschRotation.tensorAmbientRotation lam a.castSucc b.castSucc ∘ₗ HigherHarmonicYoung.AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTNoninterlacingTensorChannelAxisOrthogonality.paddedPieriSource_antitone {r : ℕ} (lam : Fin (r + 1) → ℕ) (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel lam) : Antitone (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource lam i)

def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidNonterminalProjectorVanishing.paddedPieriSignedChannel {r : ℕ} (lam : Fin (r + 1) → ℕ) : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel lam → Fin (r + 1) × Bool

The padded pieri signed channel used in the spherical-code argument.

Equations

• MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidNonterminalProjectorVanishing.paddedPieriSignedChannel lam (Sum.inl row) = (↑row, true)
• MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidNonterminalProjectorVanishing.paddedPieriSignedChannel lam (Sum.inr row) = (↑row, false)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidNonterminalProjectorVanishing.paddedPieriSignedChannel_inl {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriRaiseRow lam) : paddedPieriSignedChannel lam (Sum.inl row) = (↑row, true)

@[simp]

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidNonterminalProjectorVanishing.paddedPieriSignedChannel_inr {r : ℕ} (lam : Fin (r + 1) → ℕ) (row : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriLowerRow lam) : paddedPieriSignedChannel lam (Sum.inr row) = (↑row, false)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidNonterminalProjectorVanishing.paddedPieriSignedChannel_injective {r : ℕ} (lam : Fin (r + 1) → ℕ) : Function.Injective (paddedPieriSignedChannel lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTInvalidNonterminalProjectorVanishing.paddedOrthogonalTensorPieriChannel_relativeCasimir {r n : ℕ} (hn : 2 * r + 4 ≤ n) (target : Fin (r + 1) → ℕ) (hdom : Antitone target) (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel target) (p : ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource target i))) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir target) ((HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieriChannel hn target hdom i) p) = HigherChannel.signedNode (HigherChannel.ambientShift n target) (paddedPieriSignedChannel target i) • (HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieriChannel hn target hdom i) p

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirCompressedResolvent.gtTensorCasimir_adjoint {r n : ℕ} (lam : Fin (r + 1) → ℕ) : LinearMap.adjoint (AllRankGTRelativeCasimirProjector.gtTensorCasimir lam) = AllRankGTRelativeCasimirProjector.gtTensorCasimir lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirCompressedResolvent.gtRelativeCasimir_adjoint {r n : ℕ} (lam : Fin (r + 1) → ℕ) : LinearMap.adjoint (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) = AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirCompressedResolvent.gtRelativeCasimir_isSymmetric {r n : ℕ} (lam : Fin (r + 1) → ℕ) : LinearMap.IsSymmetric (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam)

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTRelativeCasimirCompressedResolvent.gtRelativeCasimir_eigen_inner_eq_zero {r n : ℕ} (lam : Fin (r + 1) → ℕ) (u v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (s t : ℝ) (hu : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) u = s • u) (hv : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir lam) v = t • v) (hne : s ≠ t) : inner ℝ u v = 0

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam)) : ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) i)) →ₗᵢ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)

The physical padded pieri channel used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel_inner_eq_zero {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (i j : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam)) (hij : i ≠ j) (p : ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) i))) (q : ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) j))) : inner ℝ ((physicalPaddedPieriChannel hn lam hdom i) p) ((physicalPaddedPieriChannel hn lam hdom j) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel_finrank {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) : Module.finrank ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) = ∑ i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam), Module.finrank ℝ ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) i))

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalEigenchannelEigenspace.orthogonalEigenchannel_eigenspace_eq_range {ι : Type u_1} {V : Type u_2} [Finite ι] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (nodes : ι → ℝ) (hnode : Function.Injective nodes) (T : Module.End ℝ V) (A : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((A i) p) ((A j) q) = 0) (hcomplete : ⨆ (i : ι), (A i).range = ⊤) (heigen : ∀ (i : ι) (p : E i), T ((A i) p) = nodes i • (A i) p) (selected : ι) : T.eigenspace (nodes selected) = (A selected).range

theorem MetricCodes.Spherical.HigherYoungAllRankOrthogonalEigenchannelEigenspace.orthogonalEigenchannel_eigenspace_eq_range_of_finrank {ι : Type u_1} {V : Type u_2} [Fintype ι] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), FiniteDimensional ℝ (E i)] (nodes : ι → ℝ) (hnode : Function.Injective nodes) (T : Module.End ℝ V) (A : (i : ι) → E i →ₗᵢ[ℝ] V) (horth : ∀ (i j : ι), i ≠ j → ∀ (p : E i) (q : E j), inner ℝ ((A i) p) ((A j) q) = 0) (hdim : Module.finrank ℝ V = ∑ i : ι, Module.finrank ℝ (E i)) (heigen : ∀ (i : ι) (p : E i), T ((A i) p) = nodes i • (A i) p) (selected : ι) : T.eigenspace (nodes selected) = (A selected).range

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedPhysicalChannelRange.physicalPaddedPieriChannel_relativeCasimir {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n) (low : Fin (r + 1) → ℕ) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight low)) (channel : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight low)) (q : ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight low) channel))) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir low) ((AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel hn low hdom channel) q) = HigherChannel.signedNode (HigherChannel.ambientShift n (ThreeRowYoungBranching.appendZeroWeight low)) (AllRankGTInvalidNonterminalProjectorVanishing.paddedPieriSignedChannel (ThreeRowYoungBranching.appendZeroWeight low) channel) • (AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel hn low hdom channel) q

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedPhysicalChannelRange.selectedSignedEigenspace_le_youngClebschLower_range {r n : ℕ} (hn : 2 * (r + 2) + 4 ≤ n + 1) (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (hfinite : HigherChannel.FiniteInterlacing (n + 1) low mu) (hdom : Antitone low) (row : Fin (r + 2)) (hhigh : Antitone (HigherChannel.raiseWeight low row)) : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir low).eigenspace (HigherChannel.signedNode (HigherChannel.ambientShift (n + 1) low) (row, true)) ≤ (youngClebschLower low (HigherChannel.raiseWeight low row) ⋯ row).range

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedRestrictedProjectorEquality.gtSelectedPhysicalSignedSpan {r n : ℕ} (low : Fin (r + 1) → ℕ) (row : Fin (r + 1)) : Submodule ℝ (TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace low))

The span of the selected physical Clebsch range and all signed Casimir eigenspaces other than the selected channel.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedRestrictedProjectorEquality.youngClebschLower_adjoint_signedEigen_eq_zero {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (hfinite : HigherChannel.FiniteInterlacing n low mu) (row : Fin (r + 1)) (channel : Fin (r + 1) × Bool) (hne : channel ≠ (row, true)) (v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace low)) (hv : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir low) v = HigherChannel.signedNode (HigherChannel.ambientShift n low) channel • v) : (LinearMap.adjoint (youngClebschLower low (HigherChannel.raiseWeight low row) ⋯ row)) v = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedRestrictedProjectorEquality.gtSelectedRowClebschRangeProjector_signedEigen_eq_zero {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (hfinite : HigherChannel.FiniteInterlacing n low mu) (row : Fin (r + 1)) (channel : Fin (r + 1) × Bool) (hne : channel ≠ (row, true)) (v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace low)) (hv : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir low) v = HigherChannel.signedNode (HigherChannel.ambientShift n low) channel • v) : (AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector low row) v = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedRestrictedProjectorEquality.allRankCartanCharacteristicProjector_eq_selectedClebsch_of_mem_physicalSignedSpan {r n : ℕ} (low : Fin (r + 1) → ℕ) (mu : Fin r → ℕ) (hfinite : HigherChannel.FiniteInterlacing n low mu) (hdom : Antitone low) (row : Fin (r + 1)) (hhigh : Antitone (HigherChannel.raiseWeight low row)) (v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace low)) (hv : v ∈ gtSelectedPhysicalSignedSpan low row) : (AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector low (row, true)) v = (AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector low row) v

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTSelectedRestrictedProjectorEquality.gtSignedEigenvectorSpan_le_selectedPhysicalSignedSpan {r n : ℕ} (low : Fin (r + 1) → ℕ) (row : Fin (r + 1)) (hselected : (AllRankGTRelativeCasimirProjector.gtRelativeCasimir low).eigenspace (HigherChannel.signedNode (HigherChannel.ambientShift n low) (row, true)) ≤ (youngClebschLower low (HigherChannel.raiseWeight low row) ⋯ row).range) : AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan low ≤ gtSelectedPhysicalSignedSpan low row

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedClebschOrthogonality.appendedFullBranchPieriLower {r n : ℕ} (lam : Fin (r + 2) → ℕ) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (nu : BranchingDimension.FullBranchWeight (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) : ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature nu)) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight lam))

The appended full branch pieri lower used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedClebschOrthogonality.appendedFullBranchPieriLower_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (nu : BranchingDimension.FullBranchWeight (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (a b : Fin n) : appendedFullBranchPieriLower lam hdominant hsource hn nu ∘ₗ MixedSignature.youngAmbientRotation (BranchingDimension.fullBranchSignature nu) a b = ClebschRotation.tensorAmbientRotation (ThreeRowYoungBranching.appendZeroWeight lam) a.castSucc b.castSucc ∘ₗ appendedFullBranchPieriLower lam hdominant hsource hn nu

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedPieriPhysicalAxisOrthogonality.originalPaddedSelectedAxisTensor {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) : ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight (ThreeRowYoungBranching.appendZeroWeight mu))) →ₗ[ℝ] TensorProduct ℝ (SpherePacking.Euclidean (n + 1)) ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight lam))

The original padded selected axis tensor used in the spherical-code argument.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedPieriPhysicalAxisOrthogonality.originalPaddedSelectedAxisTensor_rotation_intertwine {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (a b : Fin n) : originalPaddedSelectedAxisTensor lam mu h hgram ∘ₗ MixedSignature.youngAmbientRotation (ThreeRowYoungBranching.appendZeroWeight (ThreeRowYoungBranching.appendZeroWeight mu)) a b = ClebschRotation.tensorAmbientRotation (ThreeRowYoungBranching.appendZeroWeight lam) a.castSucc b.castSucc ∘ₗ originalPaddedSelectedAxisTensor lam mu h hgram

noncomputable def MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedPieriPhysicalAxisOrthogonality.originalAppendedFullBranchAxisCrossGram {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (nu : BranchingDimension.FullBranchWeight (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) : ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight (ThreeRowYoungBranching.appendZeroWeight mu))) →ₗ[ℝ] ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature nu))

The cross-Gram map between the original padded selected-axis tensor and an appended full- branch Pieri lowering map.

Equations

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

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedPieriPhysicalAxisOrthogonality.originalAppendedFullBranchAxisCrossGram_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (nu : BranchingDimension.FullBranchWeight (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) : originalAppendedFullBranchAxisCrossGram lam mu h hgram hdominant hsource hn nu = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedPieriPhysicalAxisOrthogonality.originalAppendedFullBranchAxis_inner_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (nu : BranchingDimension.FullBranchWeight (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (p : ↥(HarmonicYoungSpace (ThreeRowYoungBranching.appendZeroWeight (ThreeRowYoungBranching.appendZeroWeight mu)))) (q : ↥(HarmonicYoungSpace (BranchingDimension.fullBranchSignature nu))) : inner ℝ ((originalPaddedSelectedAxisTensor lam mu h hgram) p) ((AllRankGTAppendedClebschOrthogonality.appendedFullBranchPieriLower lam hdominant hsource hn nu) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedPieriPhysicalAxisOrthogonality.appendedPaddedPieriLower_adjoint_originalPaddedSelectedAxisTensor_eq_zero {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) : LinearMap.adjoint (AllRankPaddedLowerClebschIntertwining.normalizedPaddedPieriLower (ThreeRowYoungBranching.appendZeroWeight lam) hdominant (Fin.last (r + 2)) hsource).toLinearMap ∘ₗ originalPaddedSelectedAxisTensor lam mu h hgram = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedPieriPhysicalAxisOrthogonality.appendedPaddedPieriLower_originalCanonicalAxis_orthogonal {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) (q : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2))))) : inner ℝ ((AllRankZeroRowTensorCasimirConjugacy.zeroRowTensorIsometryEquiv lam) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p)) ((AllRankPaddedLowerClebschIntertwining.normalizedPaddedPieriLower (ThreeRowYoungBranching.appendZeroWeight lam) hdominant (Fin.last (r + 2)) hsource) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTAppendedPieriPhysicalAxisOrthogonality.paddedOrthogonalTensorPieriChannel_appended_originalCanonicalAxis_orthogonal {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (hdominant : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (hsource : Antitone (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2)))) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) (q : ↥(HarmonicYoungSpace (HigherChannel.raiseWeight (ThreeRowYoungBranching.appendZeroWeight lam) (Fin.last (r + 2))))) : inner ℝ ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p) ((AllRankGTRelativeCasimirZeroRowTransport.zeroRowTransportPaddedPieriChannel lam (HigherYoungAllRankOrthogonalTensorPieriActualChannels.paddedOrthogonalTensorPieriChannel ⋯ (ThreeRowYoungBranching.appendZeroWeight lam) hdominant (Sum.inl ⟨Fin.last (r + 2), hsource⟩))) q) = 0

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTPhysicalPaddedPieriSignedSpan.gtSignedEigenvectorSpan_mem_of_physicalPaddedPieriChannel_excluded {r n : ℕ} (hn : 2 * (r + 1) + 4 ≤ n) (lam : Fin (r + 1) → ℕ) (hdom : Antitone (ThreeRowYoungBranching.appendZeroWeight lam)) (v : TensorProduct ℝ (SpherePacking.Euclidean n) ↥(HarmonicYoungSpace lam)) (hexcluded : ∀ (i : HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.PaddedPieriChannel (ThreeRowYoungBranching.appendZeroWeight lam)), ¬AllRankGTRelativeCasimirZeroRowTransport.retainedPaddedPieriChannel lam i → ∀ (q : ↥(HarmonicYoungSpace (HigherYoungAllRankOrthogonalTensorPieriSourceSignatureInjectivity.paddedPieriSource (ThreeRowYoungBranching.appendZeroWeight lam) i))), inner ℝ v ((AllRankGTTransportedPieriOrthogonality.physicalPaddedPieriChannel hn lam hdom i) q) = 0) : v ∈ AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTTransverseOrthogonalCompleteness.canonicalGelfandTsetlinAxisTensor_mem_gtSignedEigenvectorSpan {r n : ℕ} (lam : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces lam mu) (hn : 2 * (r + 2) + 5 ≤ n + 1) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram lam mu h) (p : ↥(HarmonicYoungSpace mu)) : (AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor lam mu h hgram) p ∈ AllRankGTCompressedResolventSpectral.gtSignedEigenvectorSpan lam

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCanonicalPhysicalSignedSpan.canonicalGelfandTsetlinAxisTensor_mem_gtSelectedPhysicalSignedSpan {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces low mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) low mu) (hdom : Antitone low) (row : Fin (r + 2)) (hhigh : Antitone (HigherChannel.raiseWeight low row)) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) : (AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor low mu h hgram) p ∈ AllRankGTSelectedRestrictedProjectorEquality.gtSelectedPhysicalSignedSpan low row

theorem MetricCodes.Spherical.HigherHarmonicYoung.AllRankGTCanonicalPhysicalSignedSpan.allRankCartanCharacteristicProjector_canonicalAxis_eq_physicalClebsch {r n : ℕ} (low : Fin (r + 2) → ℕ) (mu : Fin (r + 1) → ℕ) (h : HigherRepresentationGraph.Interlaces low mu) (hgram : AllRankGelfandTsetlinCanonicalFibre.PositiveGelfandTsetlinFischerGram low mu h) (hfinite : HigherChannel.FiniteInterlacing (n + 1) low mu) (hdom : Antitone low) (row : Fin (r + 2)) (hhigh : Antitone (HigherChannel.raiseWeight low row)) (hn : 2 * (r + 2) + 5 ≤ n + 1) (p : ↥(HarmonicYoungSpace mu)) : (AllRankCartanCharacteristicProjector.allRankCartanCharacteristicProjector low (row, true)) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor low mu h hgram) p) = (AllRankGTCartanHodgeSelector.gtSelectedRowClebschRangeProjector low row) ((AllRankGTCompressedResolvent.canonicalGelfandTsetlinAxisTensor low mu h hgram) p)

theorem MetricCodes.Spherical.HigherYoungAllRankStrongStableActualBoxSufficiency.fixedLevelHierarchyCodeBound_of_extraStrongStableBoxRepresentationData (hrepresentation : ∀ {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ), HigherHierarchy.Interlacing a b → 0 < a (Fin.last (r + 1)) → 2 * (r + 2) + 5 ≤ n → (∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) → Nonempty (HigherHierarchyActualBoxSufficiency.BoxRepresentationData a b)) : HigherHierarchy.FixedLevelHierarchyCodeBound

theorem MetricCodes.Spherical.HigherYoungAllRankStrongStableActualBoxSufficiency.fixedLevelHierarchyCodeBound_of_extraStrongStableProjectedAxis (hrealization : ∀ {r m n : ℕ} (a : Fin (r + 2) → ℝ) (b : Fin (r + 1) → ℝ), HigherHierarchy.Interlacing a b → 0 < a (Fin.last (r + 1)) → 2 * (r + 2) + 5 ≤ n → (∀ (v : HigherHierarchy.RectangularVertices.Vertex (r + 1) m), HigherChannel.FiniteInterlacing n (HigherHierarchy.RectangularVertices.signature a n v) (HigherChannel.flooredCoordinates b n)) → ∃ (o : HigherProjectionInstantiation.SpherePoint n) (fibre : (i : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) → ↥(HigherHierarchyActualBoxSufficiency.BoxStabilizer n b) →ₗᵢ[ℝ] HigherYoungMovingFibres.YoungVertex (HigherYoungActualGraphAssembly.boxSignature a n) i), ∀ (target source : HigherYoungActualGraphAssembly.BoxIndex (r + 1) m) (h : 0 < HigherHierarchyActualBoxSufficiency.boxProbability a b n target source), Nonempty (HigherYoungAllRankActualBoxInstantiation.BoxProjectedAxisWitness a b o fibre target source h)) : HigherHierarchy.FixedLevelHierarchyCodeBound