Harmonic analysis for spherical codes

Harmonic polynomial, Gegenbauer, Perron, and adjacent-channel constructions.

@[reducible, inline]

abbrev MetricCodes.Sphere (n : ℕ) : Type

The sphere used in the metric-code argument.

Equations

• MetricCodes.Sphere n = { x : MetricCodes.Ambient n // ‖x‖ = 1 }

noncomputable def MetricCodes.sphericalInner {n : ℕ} (x y : Sphere n) : ℝ

The spherical inner used in the metric-code argument.

Equations

• MetricCodes.sphericalInner x y = inner ℝ ↑x ↑y

theorem MetricCodes.spherical_dist_sq {n : ℕ} (x y : Sphere n) : ‖↑x - ↑y‖ ^ 2 = 2 * (1 - sphericalInner x y)

def MetricCodes.IsSphericalCode {n : ℕ} (s : ℝ) (C : Finset (Sphere n)) : Prop

The predicate asserting spherical code.

Equations

• MetricCodes.IsSphericalCode s C = ∀ ⦃x : MetricCodes.Sphere n⦄, x ∈ C → ∀ ⦃y : MetricCodes.Sphere n⦄, y ∈ C → x ≠ y → MetricCodes.sphericalInner x y ≤ s

structure MetricCodes.SphericalCode (n : ℕ) (s : ℝ) : Type

Data encoding the spherical code construction.

• points : Finset (Sphere n)

  The points component.

• inner_le : IsSphericalCode s self.points

noncomputable def MetricCodes.sphericalCodeNumber (n : ℕ) (s : ℝ) : ℕ∞

The spherical code number used in the metric-code argument.

Equations

• MetricCodes.sphericalCodeNumber n s = ⨆ (C : MetricCodes.SphericalCode n s), ↑C.points.card

theorem MetricCodes.sphericalCodeNumber_le {n : ℕ} {s : ℝ} {B : ℕ∞} (hB : ∀ (C : SphericalCode n s), ↑C.points.card ≤ B) : sphericalCodeNumber n s ≤ B

theorem MetricCodes.sphericalCodeNumber_lt_top {n : ℕ} {s : ℝ} (hs : s < 1) : sphericalCodeNumber n s < ⊤

theorem MetricCodes.exists_maximal_sphericalCode {n : ℕ} {s : ℝ} (hs : s < 1) : ∃ (C : SphericalCode n s), ↑C.points.card = sphericalCodeNumber n s

theorem MetricCodes.sphericalEntropy_pos {u : ℝ} (hu : 0 < u) : 0 < sphericalEntropy u

theorem MetricCodes.Gamma_pos {a b : ℝ} (hb : 0 ≤ b) (hab : b < a) : 0 < Gamma a b

def MetricCodes.harmonicDimension (n : ℕ) : ℕ → ℕ

The harmonic dimension used in the metric-code argument.

Equations

• MetricCodes.harmonicDimension n 0 = 1
• MetricCodes.harmonicDimension n i.succ = (n + i - 1).choose (i + 1) + (n + i - 2).choose i

@[simp]

theorem MetricCodes.harmonicDimension_zero (n : ℕ) : harmonicDimension n 0 = 1

structure SpherePacking.SphericalCode (n : ℕ) (s : ℝ) : Type

Data encoding the spherical code construction.

• points : Finset (Euclidean n)

  The points component.

• unit_norm (x : Euclidean n) : x ∈ self.points → ‖x‖ = 1
• inner_le (x : Euclidean n) : x ∈ self.points → ∀ y ∈ self.points, x ≠ y → inner ℝ x y ≤ s

theorem SpherePacking.weighted_gram_sum_eq_norm_sq {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (C : Finset α) (w : α → ℝ) (v : α → E) : ∑ x ∈ C, ∑ y ∈ C, w x * w y * inner ℝ (v x) (v y) = ‖∑ x ∈ C, w x • v x‖ ^ 2

theorem SpherePacking.weighted_gram_sum_nonnegative {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (C : Finset α) (w : α → ℝ) (v : α → E) : 0 ≤ ∑ x ∈ C, ∑ y ∈ C, w x * w y * inner ℝ (v x) (v y)

theorem SpherePacking.positiveDefiniteKernel_of_features {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : α → E) : SpherePacking.PositiveDefiniteKernel✝ fun (x y : α) => inner ℝ (v x) (v y)

theorem SpherePacking.positiveDefiniteKernel_finset_sum {α : Type u_1} {ι : Type u_2} (I : Finset ι) (K : ι → α → α → ℝ) (hK : ∀ i ∈ I, SpherePacking.PositiveDefiniteKernel✝ (K i)) : SpherePacking.PositiveDefiniteKernel✝ fun (x y : α) => ∑ i ∈ I, K i x y

theorem SpherePacking.finite_linear_programming_bound {α : Type u_1} (C : Finset α) (f : α → α → ℝ) {c B : ℝ} (hc : 0 < c) (hB : 0 ≤ B) (hdiag : ∀ x ∈ C, f x x ≤ B) (hoff : ∀ x ∈ C, ∀ y ∈ C, x ≠ y → f x y ≤ 0) (hpositive : ↑C.card ^ 2 * c ≤ ∑ x ∈ C, ∑ y ∈ C, f x y) : ↑C.card ≤ B / c

noncomputable def SpherePacking.polynomialLaplacian (n : ℕ) : MvPolynomial (Fin n) ℝ →ₗ[ℝ] MvPolynomial (Fin n) ℝ

The polynomial laplacian used in the spherical-code argument.

Equations

• SpherePacking.polynomialLaplacian n = ∑ i : Fin n, ↑(MvPolynomial.pderiv i) ∘ₗ ↑(MvPolynomial.pderiv i)

@[simp]

theorem SpherePacking.polynomialLaplacian_apply (n : ℕ) (p : MvPolynomial (Fin n) ℝ) : (polynomialLaplacian n) p = ∑ i : Fin n, (MvPolynomial.pderiv i) ((MvPolynomial.pderiv i) p)

noncomputable def SpherePacking.harmonicHomogeneousSubmodule (n k : ℕ) : Submodule ℝ (MvPolynomial (Fin n) ℝ)

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

Equations

• SpherePacking.harmonicHomogeneousSubmodule n k = MvPolynomial.homogeneousSubmodule (Fin n) ℝ k ⊓ (SpherePacking.polynomialLaplacian n).ker

@[simp]

theorem SpherePacking.mem_harmonicHomogeneousSubmodule {n k : ℕ} (p : MvPolynomial (Fin n) ℝ) : p ∈ harmonicHomogeneousSubmodule n k ↔ p.IsHomogeneous k ∧ ∑ i : Fin n, (MvPolynomial.pderiv i) ((MvPolynomial.pderiv i) p) = 0

theorem SpherePacking.harmonicPolynomial_euler {n k : ℕ} (p : ↥(harmonicHomogeneousSubmodule n k)) : ∑ i : Fin n, MvPolynomial.X i * (MvPolynomial.pderiv i) ↑p = k • ↑p

theorem SpherePacking.finiteHilbertSchmidtKernel_positive {α : Type u_1} {ι : Type u_2} {F : Type u_3} {E : Type u_4} [Fintype ι] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : OrthonormalBasis ι ℝ F) (A : α → F →ₗ[ℝ] E) : SpherePacking.PositiveDefiniteKernel✝ (SpherePacking.finiteHilbertSchmidtKernel✝ b A)

theorem SpherePacking.finiteHilbertSchmidtKernel_eq_trace {α : Type u_1} {ι : Type u_2} {F : Type u_3} {E : Type u_4} [Fintype ι] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] (b : OrthonormalBasis ι ℝ F) (A : α → F →ₗ[ℝ] E) (x y : α) : SpherePacking.finiteHilbertSchmidtKernel✝ b A x y = (LinearMap.trace ℝ F) (LinearMap.adjoint (A x) ∘ₗ A y)

theorem SpherePacking.orthogonal_three_channel_inner {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p m r : α → E) (a b : ℝ) (hpm : ∀ (x y : α), inner ℝ (p x) (m y) = 0) (hpr : ∀ (x y : α), inner ℝ (p x) (r y) = 0) (hmr : ∀ (x y : α), inner ℝ (m x) (r y) = 0) (x y : α) : inner ℝ (a • p x + b • m x + r x) (a • p y + b • m y + r y) = a ^ 2 * inner ℝ (p x) (p y) + b ^ 2 * inner ℝ (m x) (m y) + inner ℝ (r x) (r y)

theorem SpherePacking.finiteHilbertSchmidtKernel_three_channel {α : Type u_1} {ι : Type u_2} {F : Type u_3} {E : Type u_4} [Fintype ι] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (basis : OrthonormalBasis ι ℝ F) (P M R : α → F →ₗ[ℝ] E) (a b : ℝ) (hPM : ∀ (x y : α) (i : ι), inner ℝ ((P x) (basis i)) ((M y) (basis i)) = 0) (hPR : ∀ (x y : α) (i : ι), inner ℝ ((P x) (basis i)) ((R y) (basis i)) = 0) (hMR : ∀ (x y : α) (i : ι), inner ℝ ((M x) (basis i)) ((R y) (basis i)) = 0) (x y : α) : SpherePacking.finiteHilbertSchmidtKernel✝ basis (fun (z : α) => a • P z + b • M z + R z) x y = a ^ 2 * SpherePacking.finiteHilbertSchmidtKernel✝ basis P x y + b ^ 2 * SpherePacking.finiteHilbertSchmidtKernel✝ basis M x y + SpherePacking.finiteHilbertSchmidtKernel✝ basis R x y

def SpherePacking.Gegenbauer.normalized (n : ℕ) : ℕ → Polynomial ℝ

The normalized used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.
• SpherePacking.Gegenbauer.normalized n 0 = 1
• SpherePacking.Gegenbauer.normalized n 1 = Polynomial.X

@[simp]

theorem SpherePacking.Gegenbauer.normalized_zero (n : ℕ) : normalized n 0 = 1

@[simp]

theorem SpherePacking.Gegenbauer.normalized_one (n : ℕ) : normalized n 1 = Polynomial.X

theorem SpherePacking.Gegenbauer.normalized_add_two (n i : ℕ) : normalized n (i + 2) = Polynomial.C (SpherePacking.Gegenbauer.forwardCoefficient✝ n (i + 1)) * Polynomial.X * normalized n (i + 1) - Polynomial.C (SpherePacking.Gegenbauer.backwardCoefficient✝ n (i + 1)) * normalized n i

theorem SpherePacking.Gegenbauer.recurrenceDenominator_pos {n i : ℕ} (hn : 2 ≤ n) (hi : 0 < i) : 0 < SpherePacking.Gegenbauer.recurrenceDenominator✝ n i

theorem SpherePacking.Gegenbauer.forwardCoefficient_pos {n i : ℕ} (hn : 2 ≤ n) (hi : 0 < i) : 0 < SpherePacking.Gegenbauer.forwardCoefficient✝ n i

theorem SpherePacking.Gegenbauer.backwardCoefficient_pos {n i : ℕ} (hn : 2 ≤ n) (hi : 0 < i) : 0 < SpherePacking.Gegenbauer.backwardCoefficient✝ n i

theorem SpherePacking.Gegenbauer.normalized_eval_one {n : ℕ} (hn : 2 ≤ n) (i : ℕ) : Polynomial.eval 1 (normalized n i) = 1

theorem SpherePacking.Gegenbauer.normalized_natDegree {n : ℕ} (hn : 2 ≤ n) (i : ℕ) : (normalized n i).natDegree = i

def SpherePacking.Gegenbauer.harmonicDimension (n : ℕ) : ℕ → ℕ

The harmonic dimension used in the spherical-code argument.

Equations

• SpherePacking.Gegenbauer.harmonicDimension n 0 = 1
• SpherePacking.Gegenbauer.harmonicDimension n i.succ = (n + i - 1).choose (i + 1) + (n + i - 2).choose i

@[simp]

theorem SpherePacking.Gegenbauer.harmonicDimension_zero (n : ℕ) : harmonicDimension n 0 = 1

theorem SpherePacking.Gegenbauer.harmonicDimension_succ (n i : ℕ) : harmonicDimension n (i + 1) = (n + i - 1).choose (i + 1) + (n + i - 2).choose i

theorem SpherePacking.Gegenbauer.harmonicDimension_pos {n : ℕ} (hn : 2 ≤ n) (i : ℕ) : 0 < harmonicDimension n i

theorem SpherePacking.Gegenbauer.harmonicDimension_branch_step {n : ℕ} (hn : 2 ≤ n) (i : ℕ) : harmonicDimension (n + 1) (i + 1) = harmonicDimension (n + 1) i + harmonicDimension n (i + 1)

theorem SpherePacking.Gegenbauer.harmonicDimension_branch_sum {n : ℕ} (hn : 2 ≤ n) (k : ℕ) : ∑ r ∈ Finset.range (k + 1), harmonicDimension n r = harmonicDimension (n + 1) k

def SpherePacking.Gegenbauer.fibreDimension (n k : ℕ) : ℕ

The fibre dimension used in the spherical-code argument.

Equations

• SpherePacking.Gegenbauer.fibreDimension n k = SpherePacking.Gegenbauer.harmonicDimension (n - 1) k

def SpherePacking.Gegenbauer.channelDimension (n r : ℕ) : ℕ

The channel dimension used in the spherical-code argument.

Equations

• SpherePacking.Gegenbauer.channelDimension n r = SpherePacking.Gegenbauer.harmonicDimension (n - 2) r

theorem SpherePacking.Gegenbauer.fibreDimension_pos {n : ℕ} (hn : 3 ≤ n) (k : ℕ) : 0 < fibreDimension n k

noncomputable def SpherePacking.Gegenbauer.alphaSq (n k i : ℕ) : ℝ

The alpha sq used in the spherical-code argument.

Equations

• SpherePacking.Gegenbauer.alphaSq n k i = (↑i - ↑k + 1) * (↑i + ↑k + ↑n - 2) / ((↑i + 1) * (2 * ↑i + ↑n - 2))

noncomputable def SpherePacking.Gegenbauer.betaSq (n k i : ℕ) : ℝ

The beta sq used in the spherical-code argument.

Equations

• SpherePacking.Gegenbauer.betaSq n k i = (↑i - ↑k) * (↑i + ↑k + ↑n - 3) / ((↑i + ↑n - 3) * (2 * ↑i + ↑n - 2))

noncomputable def SpherePacking.Gegenbauer.jacobiCoefficient (n k i : ℕ) : ℝ

The jacobi coefficient used in the spherical-code argument.

Equations

• SpherePacking.Gegenbauer.jacobiCoefficient n k i = (↑i - ↑k + 1) * (↑i + ↑k + ↑n - 2) / √((↑i + 1) * (↑i + ↑n - 2) * (2 * ↑i + ↑n - 2) * (2 * ↑i + ↑n))

theorem SpherePacking.Gegenbauer.alphaSq_pos {n k i : ℕ} (hn : 3 ≤ n) (hki : k ≤ i) : 0 < alphaSq n k i

theorem SpherePacking.Gegenbauer.jacobiCoefficient_pos {n k i : ℕ} (hn : 3 ≤ n) (hki : k ≤ i) : 0 < jacobiCoefficient n k i

theorem SpherePacking.Gegenbauer.jacobiMatrix_symmetric (n k L : ℕ) : (SpherePacking.Gegenbauer.jacobiMatrix✝ n k L).transpose = SpherePacking.Gegenbauer.jacobiMatrix✝ n k L

theorem SpherePacking.Gegenbauer.jacobiMatrix_upper_pos {n k L : ℕ} (hn : 3 ≤ n) (p q : Fin (L - k + 1)) (hpq : ↑p + 1 = ↑q) : 0 < SpherePacking.Gegenbauer.jacobiMatrix✝ n k L p q

theorem SpherePacking.mvPolynomial_pderiv_commute {n : ℕ} (i j : Fin n) (p : MvPolynomial (Fin n) ℝ) : (MvPolynomial.pderiv i) ((MvPolynomial.pderiv j) p) = (MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) p)

noncomputable def SpherePacking.directionalDerivative (n : ℕ) (x : Euclidean n) : MvPolynomial (Fin n) ℝ →ₗ[ℝ] MvPolynomial (Fin n) ℝ

The directional derivative used in the spherical-code argument.

Equations

• SpherePacking.directionalDerivative n x = ∑ i : Fin n, x.ofLp i • ↑(MvPolynomial.pderiv i)

@[simp]

theorem SpherePacking.directionalDerivative_apply (n : ℕ) (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (directionalDerivative n x) p = ∑ i : Fin n, x.ofLp i • (MvPolynomial.pderiv i) p

@[simp]

theorem SpherePacking.directionalDerivation_apply (n : ℕ) (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (SpherePacking.directionalDerivation✝ n x) p = (directionalDerivative n x) p

theorem SpherePacking.directionalDerivative_mul {n : ℕ} (x : Euclidean n) (p q : MvPolynomial (Fin n) ℝ) : (directionalDerivative n x) (p * q) = (directionalDerivative n x) p * q + p * (directionalDerivative n x) q

noncomputable def SpherePacking.axisPolynomial (n : ℕ) (x : Euclidean n) : MvPolynomial (Fin n) ℝ

The axis polynomial used in the spherical-code argument.

Equations

• SpherePacking.axisPolynomial n x = ∑ i : Fin n, MvPolynomial.C (x.ofLp i) * MvPolynomial.X i

@[simp]

theorem SpherePacking.pderiv_axisPolynomial {n : ℕ} (x : Euclidean n) (i : Fin n) : (MvPolynomial.pderiv i) (axisPolynomial n x) = MvPolynomial.C (x.ofLp i)

theorem SpherePacking.directionalDerivative_axisPolynomial {n : ℕ} (x y : Euclidean n) : (directionalDerivative n x) (axisPolynomial n y) = MvPolynomial.C (inner ℝ x y)

theorem SpherePacking.pderiv_directionalDerivative {n : ℕ} (x : Euclidean n) (i : Fin n) (p : MvPolynomial (Fin n) ℝ) : (MvPolynomial.pderiv i) ((directionalDerivative n x) p) = (directionalDerivative n x) ((MvPolynomial.pderiv i) p)

theorem SpherePacking.polynomialLaplacian_directionalDerivative {n : ℕ} (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (polynomialLaplacian n) ((directionalDerivative n x) p) = (directionalDerivative n x) ((polynomialLaplacian n) p)

theorem SpherePacking.directionalDerivative_isHomogeneous {n k : ℕ} (x : Euclidean n) {p : MvPolynomial (Fin n) ℝ} (hp : p.IsHomogeneous k) : ((directionalDerivative n x) p).IsHomogeneous (k - 1)

theorem SpherePacking.axisPolynomial_isHomogeneous {n : ℕ} (x : Euclidean n) : (axisPolynomial n x).IsHomogeneous 1

theorem SpherePacking.polynomialLaplacian_axisPolynomial {n : ℕ} (x : Euclidean n) : (polynomialLaplacian n) (axisPolynomial n x) = 0

theorem SpherePacking.directionalDerivative_axisPolynomial_self {n : ℕ} (x : Euclidean n) (hx : ‖x‖ = 1) : (directionalDerivative n x) (axisPolynomial n x) = 1

theorem SpherePacking.directionalDerivative_mem_harmonic {n k : ℕ} (x : Euclidean n) {p : MvPolynomial (Fin n) ℝ} (hp : p ∈ harmonicHomogeneousSubmodule n (k + 1)) : (directionalDerivative n x) p ∈ harmonicHomogeneousSubmodule n k

noncomputable def SpherePacking.harmonicDirectionalDerivative (n k : ℕ) (x : Euclidean n) : ↥(harmonicHomogeneousSubmodule n (k + 1)) →ₗ[ℝ] ↥(harmonicHomogeneousSubmodule n k)

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

Equations

• SpherePacking.harmonicDirectionalDerivative n k x = (SpherePacking.directionalDerivative n x).restrict ⋯

noncomputable def SpherePacking.tangentHarmonicSubmodule (n k : ℕ) (x : Euclidean n) : Submodule ℝ (MvPolynomial (Fin n) ℝ)

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

Equations

• SpherePacking.tangentHarmonicSubmodule n k x = SpherePacking.harmonicHomogeneousSubmodule n k ⊓ (SpherePacking.directionalDerivative n x).ker

@[simp]

theorem SpherePacking.mem_tangentHarmonicSubmodule {n k : ℕ} (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : p ∈ tangentHarmonicSubmodule n k x ↔ p.IsHomogeneous k ∧ (polynomialLaplacian n) p = 0 ∧ (directionalDerivative n x) p = 0

@[reducible, inline]

abbrev SpherePacking.Fischer.MultiIndex (n : ℕ) : Type

The multi index used in the spherical-code argument.

Equations

• SpherePacking.Fischer.MultiIndex n = (Fin n →₀ ℕ)

def SpherePacking.Fischer.degreeIndices (n m : ℕ) : Finset (MultiIndex n)

The degree indices used in the spherical-code argument.

Equations

• SpherePacking.Fischer.degreeIndices n m = Finset.univ.finsuppAntidiag m

@[reducible, inline]

abbrev SpherePacking.Fischer.DegreeIndex (n m : ℕ) : Type

The degree index used in the spherical-code argument.

Equations

• SpherePacking.Fischer.DegreeIndex n m = ↥(SpherePacking.Fischer.degreeIndices n m)

@[reducible, inline]

abbrev SpherePacking.Fischer.Homogeneous (n m : ℕ) : Submodule ℝ (MvPolynomial (Fin n) ℝ)

The homogeneous used in the spherical-code argument.

Equations

• SpherePacking.Fischer.Homogeneous n m = MvPolynomial.homogeneousSubmodule (Fin n) ℝ m

@[reducible, inline]

abbrev SpherePacking.Fischer.CoefficientSpace (n m : ℕ) : Type

The coefficient space used in the spherical-code argument.

Equations

• SpherePacking.Fischer.CoefficientSpace n m = EuclideanSpace ℝ (SpherePacking.Fischer.DegreeIndex n m)

@[simp]

theorem SpherePacking.Fischer.mem_degreeIndices {n m : ℕ} (a : MultiIndex n) : a ∈ degreeIndices n m ↔ Finsupp.degree a = m

def SpherePacking.Fischer.multiFactorial {n : ℕ} (a : MultiIndex n) : ℝ

The multi factorial used in the spherical-code argument.

Equations

• SpherePacking.Fischer.multiFactorial a = ∏ i : Fin n, ↑(a i).factorial

theorem SpherePacking.Fischer.multiFactorial_pos {n : ℕ} (a : MultiIndex n) : 0 < multiFactorial a

theorem SpherePacking.Fischer.multiFactorial_add_single {n : ℕ} (a : MultiIndex n) (i : Fin n) : multiFactorial (a + Finsupp.single i 1) = ↑(a i + 1) * multiFactorial a

theorem SpherePacking.Fischer.coeff_pderiv (n : ℕ) (i : Fin n) (a : MultiIndex n) (p : MvPolynomial (Fin n) ℝ) : MvPolynomial.coeff a ((MvPolynomial.pderiv i) p) = ↑(a i + 1) * MvPolynomial.coeff (a + Finsupp.single i 1) p

def SpherePacking.Fischer.polynomialInner (n : ℕ) (p q : MvPolynomial (Fin n) ℝ) : ℝ

The polynomial inner used in the spherical-code argument.

Equations

• SpherePacking.Fischer.polynomialInner n p q = p.coeff.sum fun (a : Fin n →₀ ℕ) (c : ℝ) => SpherePacking.Fischer.multiFactorial a * c * MvPolynomial.coeff a q

@[simp]

theorem SpherePacking.Fischer.polynomialInner_monomial (n : ℕ) (a : MultiIndex n) (c : ℝ) (q : MvPolynomial (Fin n) ℝ) : polynomialInner n ((MvPolynomial.monomial a) c) q = multiFactorial a * c * MvPolynomial.coeff a q

theorem SpherePacking.Fischer.polynomialInner_add_left (n : ℕ) (p q r : MvPolynomial (Fin n) ℝ) : polynomialInner n (p + q) r = polynomialInner n p r + polynomialInner n q r

theorem SpherePacking.Fischer.polynomialInner_add_right (n : ℕ) (p q r : MvPolynomial (Fin n) ℝ) : polynomialInner n p (q + r) = polynomialInner n p q + polynomialInner n p r

theorem SpherePacking.Fischer.polynomialInner_comm (n : ℕ) (p q : MvPolynomial (Fin n) ℝ) : polynomialInner n p q = polynomialInner n q p

theorem SpherePacking.Fischer.polynomialInner_self_nonneg (n : ℕ) (p : MvPolynomial (Fin n) ℝ) : 0 ≤ polynomialInner n p p

theorem SpherePacking.Fischer.polynomialInner_self_pos (n : ℕ) {p : MvPolynomial (Fin n) ℝ} (hp : p ≠ 0) : 0 < polynomialInner n p p

@[simp]

theorem SpherePacking.Fischer.polynomialInner_self_eq_zero (n : ℕ) (p : MvPolynomial (Fin n) ℝ) : polynomialInner n p p = 0 ↔ p = 0

theorem SpherePacking.Fischer.polynomialInner_smul_left (n : ℕ) (c : ℝ) (p q : MvPolynomial (Fin n) ℝ) : polynomialInner n (c • p) q = c * polynomialInner n p q

theorem SpherePacking.Fischer.polynomialInner_smul_right (n : ℕ) (c : ℝ) (p q : MvPolynomial (Fin n) ℝ) : polynomialInner n p (c • q) = c * polynomialInner n p q

theorem SpherePacking.Fischer.polynomialInner_sum_left {ι : Type u_1} (n : ℕ) (s : Finset ι) (f : ι → MvPolynomial (Fin n) ℝ) (q : MvPolynomial (Fin n) ℝ) : polynomialInner n (∑ i ∈ s, f i) q = ∑ i ∈ s, polynomialInner n (f i) q

theorem SpherePacking.Fischer.polynomialInner_sum_right {ι : Type u_1} (n : ℕ) (p : MvPolynomial (Fin n) ℝ) (s : Finset ι) (f : ι → MvPolynomial (Fin n) ℝ) : polynomialInner n p (∑ i ∈ s, f i) = ∑ i ∈ s, polynomialInner n p (f i)

theorem SpherePacking.Fischer.polynomialInner_X_mul (n : ℕ) (i : Fin n) (p q : MvPolynomial (Fin n) ℝ) : polynomialInner n (MvPolynomial.X i * p) q = polynomialInner n p ((MvPolynomial.pderiv i) q)

theorem SpherePacking.Fischer.polynomialInner_radial_laplacian (n : ℕ) (p q : MvPolynomial (Fin n) ℝ) : polynomialInner n ((∑ i : Fin n, MvPolynomial.X i ^ 2) * p) q = polynomialInner n p (∑ i : Fin n, (MvPolynomial.pderiv i) ((MvPolynomial.pderiv i) q))

theorem SpherePacking.Fischer.polynomialInner_axis_directional (n : ℕ) (x : Euclidean n) (p q : MvPolynomial (Fin n) ℝ) : polynomialInner n (axisPolynomial n x * p) q = polynomialInner n p ((directionalDerivative n x) q)

noncomputable def SpherePacking.Fischer.coefficientEmbedding (n m : ℕ) : ↥(Homogeneous n m) →ₗ[ℝ] CoefficientSpace n m

The coefficient embedding used in the spherical-code argument.

Equations

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

@[simp]

theorem SpherePacking.Fischer.coefficientEmbedding_apply (n m : ℕ) (p : ↥(Homogeneous n m)) (a : DegreeIndex n m) : ((coefficientEmbedding n m) p).ofLp a = √(multiFactorial ↑a) * MvPolynomial.coeff ↑a ↑p

theorem SpherePacking.Fischer.coefficientEmbedding_injective (n m : ℕ) : Function.Injective ⇑(coefficientEmbedding n m)

theorem SpherePacking.Fischer.harmonicCoefficientEmbedding_injective (n m : ℕ) : Function.Injective ⇑(SpherePacking.Fischer.harmonicCoefficientEmbedding✝ n m)

noncomputable def SpherePacking.Fischer.homogeneousInner (n m : ℕ) (p q : ↥(Homogeneous n m)) : ℝ

The homogeneous inner used in the spherical-code argument.

Equations

• SpherePacking.Fischer.homogeneousInner n m p q = inner ℝ ((SpherePacking.Fischer.coefficientEmbedding n m) p) ((SpherePacking.Fischer.coefficientEmbedding n m) q)

theorem SpherePacking.Fischer.homogeneousInner_eq_sum (n m : ℕ) (p q : ↥(Homogeneous n m)) : homogeneousInner n m p q = ∑ a : DegreeIndex n m, multiFactorial ↑a * MvPolynomial.coeff ↑a ↑p * MvPolynomial.coeff ↑a ↑q

theorem SpherePacking.Fischer.homogeneousInner_eq_polynomialInner (n m : ℕ) (p q : ↥(Homogeneous n m)) : homogeneousInner n m p q = polynomialInner n ↑p ↑q

@[implicit_reducible]

noncomputable def SpherePacking.Fischer.homogeneousInnerCore (n m : ℕ) : InnerProductSpace.Core ℝ ↥(Homogeneous n m)

The homogeneous inner core used in the spherical-code argument.

Equations

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

@[simp]

theorem SpherePacking.Fischer.harmonicCoefficientEmbedding_apply (n m : ℕ) (p : ↥(harmonicHomogeneousSubmodule n m)) (a : DegreeIndex n m) : ((SpherePacking.Fischer.harmonicCoefficientEmbedding✝ n m) p).ofLp a = √(multiFactorial ↑a) * MvPolynomial.coeff ↑a ↑p

noncomputable def SpherePacking.Fischer.harmonicInner (n m : ℕ) (p q : ↥(harmonicHomogeneousSubmodule n m)) : ℝ

The harmonic inner used in the spherical-code argument.

Equations

• SpherePacking.Fischer.harmonicInner n m p q = inner ℝ ((SpherePacking.Fischer.harmonicCoefficientEmbedding✝ n m) p) ((SpherePacking.Fischer.harmonicCoefficientEmbedding✝ n m) q)

theorem SpherePacking.Fischer.harmonicInner_eq_sum (n m : ℕ) (p q : ↥(harmonicHomogeneousSubmodule n m)) : harmonicInner n m p q = ∑ a : DegreeIndex n m, multiFactorial ↑a * MvPolynomial.coeff ↑a ↑p * MvPolynomial.coeff ↑a ↑q

theorem SpherePacking.Fischer.harmonicInner_eq_polynomialInner (n m : ℕ) (p q : ↥(harmonicHomogeneousSubmodule n m)) : harmonicInner n m p q = polynomialInner n ↑p ↑q

@[implicit_reducible]

def SpherePacking.Fischer.embeddingInnerCore {F : Type u_1} {E : Type u_2} [AddCommGroup F] [Module ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : F →ₗ[ℝ] E) (hf : Function.Injective ⇑f) : InnerProductSpace.Core ℝ F

The embedding inner core used in the spherical-code argument.

Equations

• SpherePacking.Fischer.embeddingInnerCore f hf = { inner := fun (p q : F) => inner ℝ (f p) (f q), conj_inner_symm := ⋯, re_inner_nonneg := ⋯, add_left := ⋯, smul_left := ⋯, definite := ⋯ }

theorem SpherePacking.Fischer.tangentHarmonicSubmodule_le_harmonic (n m : ℕ) (x : Euclidean n) : tangentHarmonicSubmodule n m x ≤ harmonicHomogeneousSubmodule n m

theorem SpherePacking.Fischer.tangentCoefficientEmbedding_injective (n m : ℕ) (x : Euclidean n) : Function.Injective ⇑(SpherePacking.Fischer.tangentCoefficientEmbedding✝ n m x)

theorem SpherePacking.Fischer.tangent_finiteDimensional (n m : ℕ) (x : Euclidean n) : FiniteDimensional ℝ ↥(tangentHarmonicSubmodule n m x)

theorem SpherePacking.Fischer.tangentInner_eq_polynomialInner (n m : ℕ) (x : Euclidean n) (p q : ↥(tangentHarmonicSubmodule n m x)) : SpherePacking.Fischer.tangentInner✝ n m x p q = polynomialInner n ↑p ↑q

@[instance_reducible]

noncomputable instance SpherePacking.Fischer.instHarmonicFischerInner (n m : ℕ) : Inner ℝ ↥(harmonicHomogeneousSubmodule n m)

Equations

• SpherePacking.Fischer.instHarmonicFischerInner n m = { inner := SpherePacking.Fischer.harmonicInner n m }

@[instance_reducible]

noncomputable instance SpherePacking.Fischer.instHarmonicFischerNormedAddCommGroup (n m : ℕ) : NormedAddCommGroup ↥(harmonicHomogeneousSubmodule n m)

Equations

• SpherePacking.Fischer.instHarmonicFischerNormedAddCommGroup n m = InnerProductSpace.Core.toNormedAddCommGroup

@[instance_reducible]

noncomputable instance SpherePacking.Fischer.instHarmonicFischerInnerProductSpace (n m : ℕ) : InnerProductSpace ℝ ↥(harmonicHomogeneousSubmodule n m)

Equations

• SpherePacking.Fischer.instHarmonicFischerInnerProductSpace n m = InnerProductSpace.ofCore (SpherePacking.Fischer.harmonicInnerCore✝ n m).toCore

@[instance_reducible]

noncomputable instance SpherePacking.Fischer.instTangentFischerInner (n m : ℕ) (x : Euclidean n) : Inner ℝ ↥(tangentHarmonicSubmodule n m x)

Equations

• SpherePacking.Fischer.instTangentFischerInner n m x = { inner := SpherePacking.Fischer.tangentInner✝ n m x }

@[instance_reducible]

noncomputable instance SpherePacking.Fischer.instTangentFischerNormedAddCommGroup (n m : ℕ) (x : Euclidean n) : NormedAddCommGroup ↥(tangentHarmonicSubmodule n m x)

Equations

• SpherePacking.Fischer.instTangentFischerNormedAddCommGroup n m x = InnerProductSpace.Core.toNormedAddCommGroup

@[instance_reducible]

noncomputable instance SpherePacking.Fischer.instTangentFischerInnerProductSpace (n m : ℕ) (x : Euclidean n) : InnerProductSpace ℝ ↥(tangentHarmonicSubmodule n m x)

Equations

• SpherePacking.Fischer.instTangentFischerInnerProductSpace n m x = InnerProductSpace.ofCore (SpherePacking.Fischer.tangentInnerCore✝ n m x).toCore

@[simp]

theorem SpherePacking.Fischer.harmonic_inner_eq (n m : ℕ) (p q : ↥(harmonicHomogeneousSubmodule n m)) : inner ℝ p q = harmonicInner n m p q

@[simp]

theorem SpherePacking.Fischer.tangent_inner_eq (n m : ℕ) (x : Euclidean n) (p q : ↥(tangentHarmonicSubmodule n m x)) : inner ℝ p q = SpherePacking.Fischer.tangentInner✝ n m x p q

noncomputable def SpherePacking.radialPolynomial (n : ℕ) : MvPolynomial (Fin n) ℝ

The radial polynomial used in the spherical-code argument.

Equations

• SpherePacking.radialPolynomial n = ∑ i : Fin n, MvPolynomial.X i ^ 2

@[simp]

theorem SpherePacking.pderiv_radialPolynomial {n : ℕ} (i : Fin n) : (MvPolynomial.pderiv i) (radialPolynomial n) = 2 * MvPolynomial.X i

theorem SpherePacking.radialPolynomial_isHomogeneous (n : ℕ) : (radialPolynomial n).IsHomogeneous 2

theorem SpherePacking.radialPolynomial_ne_zero {n : ℕ} (hn : 0 < n) : radialPolynomial n ≠ 0

theorem SpherePacking.polynomialLaplacian_isHomogeneous {n m : ℕ} (p : MvPolynomial (Fin n) ℝ) (hp : p.IsHomogeneous m) : ((polynomialLaplacian n) p).IsHomogeneous (m - 2)

@[simp]

theorem SpherePacking.homogeneousExponentFinset_card (n m : ℕ) : (SpherePacking.homogeneousExponentFinset✝ n m).card = (n + m - 1).choose m

@[simp]

theorem SpherePacking.mem_homogeneousExponentFinset {n m : ℕ} (d : Fin n →₀ ℕ) : d ∈ SpherePacking.homogeneousExponentFinset✝ n m ↔ Finsupp.degree d = m

theorem SpherePacking.homogeneousSubmodule_eq_supported_exponents (n m : ℕ) : MvPolynomial.homogeneousSubmodule (Fin n) ℝ m = AddMonoidAlgebra.supported ℝ ℝ ↑(SpherePacking.homogeneousExponentFinset✝ n m)

instance SpherePacking.homogeneousSubmodule_finiteDimensional (n m : ℕ) : FiniteDimensional ℝ ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ m)

theorem SpherePacking.finrank_homogeneousSubmodule (n m : ℕ) : Module.finrank ℝ ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ m) = (n + m - 1).choose m

@[simp]

theorem SpherePacking.homogeneousRadialMultiplication_apply (n m : ℕ) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ m)) : ↑((SpherePacking.homogeneousRadialMultiplication✝ n m) p) = radialPolynomial n * ↑p

theorem SpherePacking.homogeneousRadialMultiplication_injective {n : ℕ} (hn : 0 < n) (m : ℕ) : Function.Injective ⇑(SpherePacking.homogeneousRadialMultiplication✝ n m)

theorem SpherePacking.surjective_of_injective_inner_adjoint {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (cE : InnerProductSpace.Core ℝ E) (cF : InnerProductSpace.Core ℝ F) (A : E →ₗ[ℝ] F) (B : F →ₗ[ℝ] E) (hpair : ∀ (x : F) (y : E), inner ℝ (B x) y = inner ℝ x (A y)) (hinj : Function.Injective ⇑A) : Function.Surjective ⇑B

@[simp]

theorem SpherePacking.homogeneousLaplacian_apply (n m : ℕ) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ (m + 2))) : ↑((SpherePacking.homogeneousLaplacian✝ n m) p) = (polynomialLaplacian n) ↑p

theorem SpherePacking.fischer_homogeneousInner_comm (n m : ℕ) (p q : ↥(Fischer.Homogeneous n m)) : Fischer.homogeneousInner n m p q = Fischer.homogeneousInner n m q p

theorem SpherePacking.fischer_homogeneousInner_radial_laplacian (n m : ℕ) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ m)) (q : ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ (m + 2))) : Fischer.homogeneousInner n (m + 2) ((SpherePacking.homogeneousRadialMultiplication✝ n m) p) q = Fischer.homogeneousInner n m p ((SpherePacking.homogeneousLaplacian✝ n m) q)

theorem SpherePacking.homogeneousLaplacian_surjective_of_fischer_adjoint {n : ℕ} (hn : 0 < n) (m : ℕ) (hpair : ∀ (q : ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ (m + 2))) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ m)), Fischer.homogeneousInner n m ((SpherePacking.homogeneousLaplacian✝ n m) q) p = Fischer.homogeneousInner n (m + 2) q ((SpherePacking.homogeneousRadialMultiplication✝ n m) p)) : Function.Surjective ⇑(SpherePacking.homogeneousLaplacian✝ n m)

theorem SpherePacking.homogeneousLaplacian_surjective {n : ℕ} (hn : 0 < n) (m : ℕ) : Function.Surjective ⇑(SpherePacking.homogeneousLaplacian✝ n m)

theorem SpherePacking.homogeneousLaplacian_ker (n m : ℕ) : (SpherePacking.homogeneousLaplacian✝ n m).ker = Submodule.comap (MvPolynomial.homogeneousSubmodule (Fin n) ℝ (m + 2)).subtype (polynomialLaplacian n).ker

theorem SpherePacking.homogeneousLaplacian_ker_map (n m : ℕ) : Submodule.map (MvPolynomial.homogeneousSubmodule (Fin n) ℝ (m + 2)).subtype (SpherePacking.homogeneousLaplacian✝ n m).ker = harmonicHomogeneousSubmodule n (m + 2)

instance SpherePacking.harmonicHomogeneousSubmodule_finiteDimensional (n m : ℕ) : FiniteDimensional ℝ ↥(harmonicHomogeneousSubmodule n m)

theorem SpherePacking.polynomialLaplacian_eq_zero_of_isHomogeneous_le_one {n m : ℕ} (p : MvPolynomial (Fin n) ℝ) (hp : p.IsHomogeneous m) (hm : m ≤ 1) : (polynomialLaplacian n) p = 0

theorem SpherePacking.harmonicHomogeneousSubmodule_eq_homogeneous_of_le_one {n m : ℕ} (hm : m ≤ 1) : harmonicHomogeneousSubmodule n m = MvPolynomial.homogeneousSubmodule (Fin n) ℝ m

theorem SpherePacking.harmonicDimension_succ_succ_add_choose {n : ℕ} (hn : 0 < n) (m : ℕ) : Gegenbauer.harmonicDimension n (m + 2) + (n + m - 1).choose m = (n + m + 1).choose (m + 2)

theorem SpherePacking.finrank_harmonicHomogeneousSubmodule_of_le_one {n m : ℕ} (hn : 0 < n) (hm : m ≤ 1) : Module.finrank ℝ ↥(harmonicHomogeneousSubmodule n m) = Gegenbauer.harmonicDimension n m

theorem SpherePacking.finrank_harmonicHomogeneousSubmodule_succ_succ_of_surjective {n : ℕ} (hn : 0 < n) (m : ℕ) (h : Function.Surjective ⇑(SpherePacking.homogeneousLaplacian✝ n m)) : Module.finrank ℝ ↥(harmonicHomogeneousSubmodule n (m + 2)) = Gegenbauer.harmonicDimension n (m + 2)

theorem SpherePacking.finrank_harmonicHomogeneousSubmodule {n : ℕ} (hn : 0 < n) (m : ℕ) : Module.finrank ℝ ↥(harmonicHomogeneousSubmodule n m) = Gegenbauer.harmonicDimension n m

theorem SpherePacking.polynomialLaplacian_radialPolynomial (n : ℕ) : (polynomialLaplacian n) (radialPolynomial n) = MvPolynomial.C (2 * ↑n)

theorem SpherePacking.polynomialLaplacian_mul {n : ℕ} (p q : MvPolynomial (Fin n) ℝ) : (polynomialLaplacian n) (p * q) = (polynomialLaplacian n) p * q + 2 * ∑ i : Fin n, (MvPolynomial.pderiv i) p * (MvPolynomial.pderiv i) q + p * (polynomialLaplacian n) q

theorem SpherePacking.polynomialLaplacian_radial_mul {n m : ℕ} (p : MvPolynomial (Fin n) ℝ) (hp : p.IsHomogeneous m) : (polynomialLaplacian n) (radialPolynomial n * p) = MvPolynomial.C (2 * (2 * ↑m + ↑n)) * p + radialPolynomial n * (polynomialLaplacian n) p

theorem SpherePacking.solidHarmonicAxis_polynomialLaplacian_axis_mul {n : ℕ} (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (polynomialLaplacian n) (axisPolynomial n x * p) = 2 * (directionalDerivative n x) p + axisPolynomial n x * (polynomialLaplacian n) p

theorem SpherePacking.directionalDerivative_radialPolynomial {n : ℕ} (x : Euclidean n) : (directionalDerivative n x) (radialPolynomial n) = 2 * axisPolynomial n x

theorem SpherePacking.directionalDerivative_radial_mul {n : ℕ} (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (directionalDerivative n x) (radialPolynomial n * p) = 2 * axisPolynomial n x * p + radialPolynomial n * (directionalDerivative n x) p

theorem SpherePacking.polynomialLaplacian_C_mul {n : ℕ} (c : ℝ) (p : MvPolynomial (Fin n) ℝ) : (polynomialLaplacian n) (MvPolynomial.C c * p) = MvPolynomial.C c * (polynomialLaplacian n) p

theorem SpherePacking.directionalDerivative_C_mul {n : ℕ} (x : Euclidean n) (c : ℝ) (p : MvPolynomial (Fin n) ℝ) : (directionalDerivative n x) (MvPolynomial.C c * p) = MvPolynomial.C c * (directionalDerivative n x) p

def SpherePacking.harmonicAxisParameter (n k : ℕ) : ℝ

The harmonic axis parameter used in the spherical-code argument.

Equations

• SpherePacking.harmonicAxisParameter n k = ↑n + 2 * ↑k

def SpherePacking.solidHarmonicAxisLift (n k : ℕ) (x : Euclidean n) : ℕ → MvPolynomial (Fin n) ℝ →ₗ[ℝ] MvPolynomial (Fin n) ℝ

The solid harmonic axis lift used in the spherical-code argument.

Equations

• One or more equations did not get rendered due to their size.
• SpherePacking.solidHarmonicAxisLift n k x 0 = LinearMap.id
• SpherePacking.solidHarmonicAxisLift n k x 1 = LinearMap.mulLeft ℝ (MvPolynomial.C (SpherePacking.harmonicAxisParameter n k - 2) * SpherePacking.axisPolynomial n x)

@[simp]

theorem SpherePacking.solidHarmonicAxisLift_zero_apply (n k : ℕ) (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (solidHarmonicAxisLift n k x 0) p = p

@[simp]

theorem SpherePacking.solidHarmonicAxisLift_one_apply (n k : ℕ) (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (solidHarmonicAxisLift n k x 1) p = MvPolynomial.C (harmonicAxisParameter n k - 2) * axisPolynomial n x * p

@[simp]

theorem SpherePacking.solidHarmonicAxisLift_succ_succ_apply (n k r : ℕ) (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (solidHarmonicAxisLift n k x (r + 2)) p = MvPolynomial.C (2 * ↑(r + 1) + harmonicAxisParameter n k - 2) * axisPolynomial n x * (solidHarmonicAxisLift n k x (r + 1)) p - MvPolynomial.C (↑(r + 1) * (↑(r + 1) + harmonicAxisParameter n k - 3)) * radialPolynomial n * (solidHarmonicAxisLift n k x r) p

theorem SpherePacking.solidHarmonicAxisLift_isHomogeneous {n k : ℕ} (x : Euclidean n) {p : MvPolynomial (Fin n) ℝ} (hp : p.IsHomogeneous k) (r : ℕ) : ((solidHarmonicAxisLift n k x r) p).IsHomogeneous (k + r)

theorem SpherePacking.fischer_harmonicInner_eq_polynomialInner (n k : ℕ) (p q : ↥(harmonicHomogeneousSubmodule n k)) : Fischer.harmonicInner n k p q = Fischer.polynomialInner n ↑p ↑q

theorem SpherePacking.fischer_harmonicInner_self_nonneg (n k : ℕ) (p : ↥(harmonicHomogeneousSubmodule n k)) : 0 ≤ Fischer.harmonicInner n k p p

theorem SpherePacking.fischer_harmonicInner_self_eq_zero_iff (n k : ℕ) (p : ↥(harmonicHomogeneousSubmodule n k)) : Fischer.harmonicInner n k p p = 0 ↔ p = 0

theorem SpherePacking.fischer_harmonicInner_comm (n k : ℕ) (p q : ↥(harmonicHomogeneousSubmodule n k)) : Fischer.harmonicInner n k p q = Fischer.harmonicInner n k q p

theorem SpherePacking.directionalDerivative_eq_zero_of_isHomogeneous_zero {n : ℕ} (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) (hp : p.IsHomogeneous 0) : (directionalDerivative n x) p = 0

theorem SpherePacking.fischer_polynomialInner_zero_right (n : ℕ) (p : MvPolynomial (Fin n) ℝ) : Fischer.polynomialInner n p 0 = 0

theorem SpherePacking.fischer_polynomialInner_sub_left (n : ℕ) (p q r : MvPolynomial (Fin n) ℝ) : Fischer.polynomialInner n (p - q) r = Fischer.polynomialInner n p r - Fischer.polynomialInner n q r

theorem SpherePacking.fischer_polynomialInner_radial_harmonic {n k : ℕ} (p : MvPolynomial (Fin n) ℝ) (q : ↥(harmonicHomogeneousSubmodule n k)) : Fischer.polynomialInner n (radialPolynomial n * p) ↑q = 0

theorem SpherePacking.polynomialLaplacian_axis_mul_for_tangent {n : ℕ} (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (polynomialLaplacian n) (axisPolynomial n x * p) = 2 * (directionalDerivative n x) p + axisPolynomial n x * (polynomialLaplacian n) p

theorem SpherePacking.harmonicAxisProjectionDenominator_pos {n : ℕ} (hn : 0 < n) (k : ℕ) : 0 < SpherePacking.harmonicAxisProjectionDenominator✝ n k

noncomputable def SpherePacking.harmonicAxisProjectionOperator (n k : ℕ) (x : Euclidean n) : MvPolynomial (Fin n) ℝ →ₗ[ℝ] MvPolynomial (Fin n) ℝ

The harmonic axis projection operator used in the spherical-code argument.

Equations

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

@[simp]

theorem SpherePacking.harmonicAxisProjectionOperator_apply (n k : ℕ) (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (harmonicAxisProjectionOperator n k x) p = axisPolynomial n x * p - (SpherePacking.harmonicAxisProjectionDenominator✝ n k)⁻¹ • (radialPolynomial n * (directionalDerivative n x) p)

theorem SpherePacking.harmonicAxisProjectionOperator_mem_harmonic {n : ℕ} (hn : 0 < n) (k : ℕ) (x : Euclidean n) {p : MvPolynomial (Fin n) ℝ} (hp : p ∈ harmonicHomogeneousSubmodule n (k + 1)) : (harmonicAxisProjectionOperator n k x) p ∈ harmonicHomogeneousSubmodule n (k + 2)

noncomputable def SpherePacking.harmonicAxisLift {n : ℕ} (hn : 0 < n) (k : ℕ) (x : Euclidean n) : ↥(harmonicHomogeneousSubmodule n (k + 1)) →ₗ[ℝ] ↥(harmonicHomogeneousSubmodule n (k + 2))

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

Equations

• SpherePacking.harmonicAxisLift hn k x = (SpherePacking.harmonicAxisProjectionOperator n k x).restrict ⋯

@[simp]

theorem SpherePacking.harmonicAxisLift_apply {n : ℕ} (hn : 0 < n) (k : ℕ) (x : Euclidean n) (p : ↥(harmonicHomogeneousSubmodule n (k + 1))) : ↑((harmonicAxisLift hn k x) p) = (harmonicAxisProjectionOperator n k x) ↑p

theorem SpherePacking.harmonicAxisLift_fischer_adjoint {n : ℕ} (hn : 0 < n) (k : ℕ) (x : Euclidean n) (p : ↥(harmonicHomogeneousSubmodule n (k + 1))) (q : ↥(harmonicHomogeneousSubmodule n (k + 2))) : Fischer.harmonicInner n (k + 2) ((harmonicAxisLift hn k x) p) q = Fischer.harmonicInner n (k + 1) p ((harmonicDirectionalDerivative n (k + 1) x) q)

theorem SpherePacking.harmonicAxisProjectionOperator_pair_axis {n : ℕ} (k : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) (p : ↥(harmonicHomogeneousSubmodule n (k + 1))) : Fischer.polynomialInner n ((harmonicAxisProjectionOperator n k x) ↑p) (axisPolynomial n x * ↑p) = Fischer.harmonicInner n (k + 1) p p + (1 - 2 * (SpherePacking.harmonicAxisProjectionDenominator✝ n k)⁻¹) * Fischer.harmonicInner n k ((harmonicDirectionalDerivative n k x) p) ((harmonicDirectionalDerivative n k x) p)

theorem SpherePacking.harmonicAxisProjection_correction_nonneg {n : ℕ} (hn : 2 ≤ n) (k : ℕ) : 0 ≤ 1 - 2 * (SpherePacking.harmonicAxisProjectionDenominator✝ n k)⁻¹

theorem SpherePacking.harmonicAxisLift_injective {n : ℕ} (hn : 2 ≤ n) (k : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) : Function.Injective ⇑(harmonicAxisLift ⋯ k x)

theorem SpherePacking.harmonicDirectionalDerivative_surjective_succ {n : ℕ} (hn : 2 ≤ n) (k : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) : Function.Surjective ⇑(harmonicDirectionalDerivative n (k + 1) x)

theorem SpherePacking.harmonicDirectionalDerivative_surjective {n : ℕ} (hn : 2 ≤ n) (k : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) : Function.Surjective ⇑(harmonicDirectionalDerivative n k x)

theorem SpherePacking.harmonicDirectionalDerivative_ker (n k : ℕ) (x : Euclidean n) : (harmonicDirectionalDerivative n k x).ker = Submodule.comap (harmonicHomogeneousSubmodule n (k + 1)).subtype (directionalDerivative n x).ker

theorem SpherePacking.harmonicDirectionalDerivative_ker_map (n k : ℕ) (x : Euclidean n) : Submodule.map (harmonicHomogeneousSubmodule n (k + 1)).subtype (harmonicDirectionalDerivative n k x).ker = tangentHarmonicSubmodule n (k + 1) x

theorem SpherePacking.tangentHarmonicSubmodule_zero_eq_harmonic (n : ℕ) (x : Euclidean n) : tangentHarmonicSubmodule n 0 x = harmonicHomogeneousSubmodule n 0

theorem SpherePacking.finrank_tangentHarmonicSubmodule {n : ℕ} (hn : 3 ≤ n) (k : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) : Module.finrank ℝ ↥(tangentHarmonicSubmodule n k x) = Gegenbauer.fibreDimension n k

theorem SpherePacking.finiteHilbertSchmidtKernel_finset_sum {α : Type u_1} {ι : Type u_2} {F : Type u_3} {E : Type u_4} [Fintype ι] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : OrthonormalBasis ι ℝ F) (C : Finset α) (A : α → F →ₗ[ℝ] E) : SpherePacking.finiteHilbertSchmidtKernel✝ b (fun (x : Unit) => ∑ x ∈ C, A x) () () = ∑ x ∈ C, ∑ y ∈ C, SpherePacking.finiteHilbertSchmidtKernel✝ b A x y

theorem SpherePacking.trace_sq_le_finiteHilbertSchmidtKernel {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : OrthonormalBasis ι ℝ E) (T : E →ₗ[ℝ] E) : (LinearMap.trace ℝ E) T ^ 2 ≤ ↑(Fintype.card ι) * SpherePacking.finiteHilbertSchmidtKernel✝ b (fun (x : Unit) => T) () ()

theorem SpherePacking.finiteHilbertSchmidt_trace_cauchy {α : Type u_1} {ι : Type u_2} {E : Type u_3} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : OrthonormalBasis ι ℝ E) (C : Finset α) (A : α → E →ₗ[ℝ] E) : (∑ x ∈ C, (LinearMap.trace ℝ E) (A x)) ^ 2 ≤ ↑(Fintype.card ι) * ∑ x ∈ C, ∑ y ∈ C, SpherePacking.finiteHilbertSchmidtKernel✝ b A x y

theorem SpherePacking.isometric_projection_trace {F : Type u_1} {E : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] (f : F →ₗᵢ[ℝ] E) : (LinearMap.trace ℝ E) (f.toLinearMap ∘ₗ LinearMap.adjoint f.toLinearMap) = ↑(Module.finrank ℝ F)

theorem SpherePacking.isometric_mixed_gram_trace_cauchy {α : Type u_1} {ι : Type u_2} {F : Type u_3} {E : Type u_4} [Fintype ι] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] (b : OrthonormalBasis ι ℝ E) (C : Finset α) (f : α → F →ₗᵢ[ℝ] E) : (↑C.card * ↑(Module.finrank ℝ F)) ^ 2 ≤ ↑(Fintype.card ι) * ∑ x ∈ C, ∑ y ∈ C, SpherePacking.mixedHilbertSchmidtKernel✝ b (fun (z : α) => (f z).toLinearMap) (fun (z : α) => (f z).toLinearMap) x y

noncomputable def SpherePacking.NumericalCertificate.binaryEntropy (u : ℝ) : ℝ

The binary entropy used in the spherical-code argument.

Equations

• SpherePacking.NumericalCertificate.binaryEntropy u = ((1 + u) * Real.log (1 + u) - u * Real.log u) / Real.log 2

noncomputable def SpherePacking.NumericalCertificate.gamma (a b : ℝ) : ℝ

The gamma used in the spherical-code argument.

Equations

• SpherePacking.NumericalCertificate.gamma a b = (a * (1 + a) - b * (1 + b)) / ((1 + 2 * a) * √(a * (1 + a)))

noncomputable def MetricCodes.Spherical.boundaryQuadratic (s a : ℝ) : ℝ

The boundary quadratic used in the spherical-code argument.

Equations

• MetricCodes.Spherical.boundaryQuadratic s a = a * (1 + a) - s / 2 * (1 + 2 * a) * √(a * (1 + a))

noncomputable def MetricCodes.Spherical.boundaryDegree (s a : ℝ) : ℝ

The boundary degree used in the spherical-code argument.

Equations

• MetricCodes.Spherical.boundaryDegree s a = (√(1 + 4 * MetricCodes.Spherical.boundaryQuadratic s a) - 1) / 2

theorem MetricCodes.Spherical.spectral_iff_quadratic {s a b : ℝ} (ha : 0 < a) : s < 2 * Gamma a b ↔ b * (1 + b) < boundaryQuadratic s a

theorem MetricCodes.Spherical.boundaryDegree_pos {s a : ℝ} (hQ : 0 < boundaryQuadratic s a) : 0 < boundaryDegree s a

theorem MetricCodes.Spherical.boundaryDegree_mul_one_add {s a : ℝ} (hQ : 0 ≤ boundaryQuadratic s a) : boundaryDegree s a * (1 + boundaryDegree s a) = boundaryQuadratic s a

theorem MetricCodes.Spherical.quadratic_iff_boundaryDegree {s a b : ℝ} (hb : 0 ≤ b) (hQ : 0 < boundaryQuadratic s a) : b * (1 + b) < boundaryQuadratic s a ↔ b < boundaryDegree s a

@[simp]

theorem MetricCodes.Spherical.HigherHierarchy.lagrangeWeight_zero (a : Fin 1 → ℝ) (b : Fin 0 → ℝ) (ℓ : Fin 1) : lagrangeWeight a b ℓ = 1

theorem MetricCodes.Spherical.HigherHierarchy.Gamma_zero (a : Fin 1 → ℝ) (b : Fin 0 → ℝ) : Gamma a b = spectralAtom (a 0)

theorem MetricCodes.Spherical.HigherHierarchy.Phi_zero (a : Fin 1 → ℝ) (b : Fin 0 → ℝ) : Phi a b = sphericalEntropy (a 0)

theorem MetricCodes.Spherical.HigherHierarchy.oneRowInterlacing_iff {a b : ℝ} : Interlacing ![a, 0] ![b] ↔ 0 < b ∧ b < a

theorem MetricCodes.Spherical.HigherHierarchy.Gamma_oneRow {a b : ℝ} (ha : 0 < a) : Gamma ![a, 0] ![b] = MetricCodes.Gamma a b

theorem MetricCodes.Spherical.HigherHierarchy.Phi_oneRow (a b : ℝ) : Phi ![a, 0] ![b] = sphericalEntropy a - sphericalEntropy b

theorem MetricCodes.Spherical.HigherHierarchy.spectralAtom_lt_half {u : ℝ} (hu : 0 ≤ u) : spectralAtom u < 1 / 2

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.Gamma_nonneg {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : 0 ≤ Gamma a b

theorem MetricCodes.Spherical.HigherHierarchy.Interlacing.Gamma_lt_half {r : ℕ} {a : Fin (r + 1) → ℝ} {b : Fin r → ℝ} (h : Interlacing a b) : Gamma a b < 1 / 2

theorem SpherePacking.tendsto_nat_sequence_sub_cast_div (N : ℕ → ℕ) (c : ℕ) (u : ℝ) (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (hNu : Filter.Tendsto (fun (n : ℕ) => ↑(N n) / ↑n) Filter.atTop (nhds u)) : Filter.Tendsto (fun (n : ℕ) => ↑(N n - c) / ↑n) Filter.atTop (nhds u)

theorem SpherePacking.harmonicEntropyBase_pos (u : ℝ) (N : ℕ → ℕ) (n : ℕ) : 0 < SpherePacking.harmonicEntropyBase✝ u N n

theorem SpherePacking.harmonicDimension_choose_bounds {n k : ℕ} (hn : 2 ≤ n) (hk : 1 ≤ k) : (n + k - 2).choose k ≤ Gegenbauer.harmonicDimension n k ∧ Gegenbauer.harmonicDimension n k ≤ 2 * (n + k - 2).choose k

theorem SpherePacking.tendsto_log_harmonicEntropyBase_div (u : ℝ) (hu : 0 < u) (N : ℕ → ℕ) (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (hNratio : Filter.Tendsto (fun (n : ℕ) => ↑(N n) / ↑n) Filter.atTop (nhds 1)) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑(SpherePacking.harmonicEntropyBase✝ u N n) / ↑n) Filter.atTop (nhds ((1 + u) * Real.log (1 + u) - u * Real.log u))

theorem SpherePacking.tendsto_log_two_mul_harmonicEntropyBase_div (u : ℝ) (hu : 0 < u) (N : ℕ → ℕ) (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (hNratio : Filter.Tendsto (fun (n : ℕ) => ↑(N n) / ↑n) Filter.atTop (nhds 1)) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑(2 * SpherePacking.harmonicEntropyBase✝ u N n) / ↑n) Filter.atTop (nhds ((1 + u) * Real.log (1 + u) - u * Real.log u))

theorem SpherePacking.tendsto_log_harmonicDimension_div (u : ℝ) (hu : 0 < u) (N : ℕ → ℕ) (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (hNratio : Filter.Tendsto (fun (n : ℕ) => ↑(N n) / ↑n) Filter.atTop (nhds 1)) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑(Gegenbauer.harmonicDimension (N n) ⌊u * ↑n⌋₊) / ↑n) Filter.atTop (nhds ((1 + u) * Real.log (1 + u) - u * Real.log u))

theorem SpherePacking.tendsto_log_harmonicDimension_div_log_two (u : ℝ) (hu : 0 < u) (N : ℕ → ℕ) (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (hNratio : Filter.Tendsto (fun (n : ℕ) => ↑(N n) / ↑n) Filter.atTop (nhds 1)) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑(Gegenbauer.harmonicDimension (N n) ⌊u * ↑n⌋₊) / ↑n / Real.log 2) Filter.atTop (nhds (NumericalCertificate.binaryEntropy u))

theorem SpherePacking.tendsto_natCast_div_self : Filter.Tendsto (fun (n : ℕ) => ↑n / ↑n) Filter.atTop (nhds 1)

theorem SpherePacking.tendsto_nat_succ_cast_div : Filter.Tendsto (fun (n : ℕ) => ↑(n + 1) / ↑n) Filter.atTop (nhds 1)

theorem SpherePacking.tendsto_nat_pred_cast_div : Filter.Tendsto (fun (n : ℕ) => ↑(n - 1) / ↑n) Filter.atTop (nhds 1)

noncomputable def SpherePacking.harmonicDimensionQuotient (a b : ℝ) (n : ℕ) : ℝ

The harmonic dimension quotient used in the spherical-code argument.

Equations

• SpherePacking.harmonicDimensionQuotient a b n = ↑(SpherePacking.Gegenbauer.harmonicDimension (n + 1) ⌊a * ↑n⌋₊) / ↑(SpherePacking.Gegenbauer.harmonicDimension (n - 1) ⌊b * ↑n⌋₊)

theorem SpherePacking.harmonicDimensionQuotient_pos (a b : ℝ) {n : ℕ} (hn : 3 ≤ n) : 0 < harmonicDimensionQuotient a b n

theorem SpherePacking.tendsto_log_harmonicDimensionQuotient (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : Filter.Tendsto (fun (n : ℕ) => Real.log (harmonicDimensionQuotient a b n) / ↑n / Real.log 2) Filter.atTop (nhds (NumericalCertificate.binaryEntropy a - NumericalCertificate.binaryEntropy b))

theorem SpherePacking.tendsto_log_const_mul_harmonicDimensionQuotient (a b C : ℝ) (ha : 0 < a) (hb : 0 < b) (hC : 0 < C) : Filter.Tendsto (fun (n : ℕ) => Real.log (C * harmonicDimensionQuotient a b n) / ↑n / Real.log 2) Filter.atTop (nhds (NumericalCertificate.binaryEntropy a - NumericalCertificate.binaryEntropy b))

def SpherePacking.truncatedHarmonicDimension (n k L : ℕ) : ℕ

The truncated harmonic dimension used in the spherical-code argument.

Equations

• SpherePacking.truncatedHarmonicDimension n k L = ∑ i ∈ Finset.Icc k L, SpherePacking.Gegenbauer.harmonicDimension n i

theorem SpherePacking.truncatedHarmonicDimension_le_successor {n : ℕ} (hn : 2 ≤ n) (k L : ℕ) : truncatedHarmonicDimension n k L ≤ Gegenbauer.harmonicDimension (n + 1) L

noncomputable def SpherePacking.truncatedDimensionQuotient (a b : ℝ) (n : ℕ) : ℝ

The truncated dimension quotient used in the spherical-code argument.

Equations

• SpherePacking.truncatedDimensionQuotient a b n = ↑(SpherePacking.truncatedHarmonicDimension n ⌊b * ↑n⌋₊ ⌊a * ↑n⌋₊) / ↑(SpherePacking.Gegenbauer.fibreDimension n ⌊b * ↑n⌋₊)

theorem SpherePacking.truncatedDimensionQuotient_le_harmonicDimensionQuotient (a b : ℝ) {n : ℕ} (hn : 3 ≤ n) : truncatedDimensionQuotient a b n ≤ harmonicDimensionQuotient a b n

theorem SpherePacking.harmonicDimension_le_truncated (n k L : ℕ) (hkl : k ≤ L) : Gegenbauer.harmonicDimension n k ≤ truncatedHarmonicDimension n k L

@[reducible, inline]

abbrev SpherePacking.Jacobi.Index (k L : ℕ) : Type

The index used in the spherical-code argument.

Equations

• SpherePacking.Jacobi.Index k L = Fin (L - k + 1)

@[reducible, inline]

abbrev SpherePacking.Jacobi.Space (k L : ℕ) : Type

The space used in the spherical-code argument.

Equations

• SpherePacking.Jacobi.Space k L = EuclideanSpace ℝ (SpherePacking.Jacobi.Index k L)

noncomputable def SpherePacking.Jacobi.matrix (n k L : ℕ) : Matrix (Index k L) (Index k L) ℝ

The matrix used in the spherical-code argument.

Equations

• SpherePacking.Jacobi.matrix n k L = SpherePacking.Gegenbauer.jacobiMatrix✝ n k L

theorem SpherePacking.Jacobi.matrix_hermitian (n k L : ℕ) : (matrix n k L).IsHermitian

noncomputable def SpherePacking.Jacobi.operator (n k L : ℕ) : Space k L →ₗ[ℝ] Space k L

The operator used in the spherical-code argument.

Equations

• SpherePacking.Jacobi.operator n k L = Matrix.toEuclideanLin (SpherePacking.Jacobi.matrix n k L)

theorem SpherePacking.Jacobi.operator_isSymmetric (n k L : ℕ) : (operator n k L).IsSymmetric

noncomputable def SpherePacking.Jacobi.continuousOperator (n k L : ℕ) : Space k L →L[ℝ] Space k L

The continuous operator used in the spherical-code argument.

Equations

• SpherePacking.Jacobi.continuousOperator n k L = LinearMap.toContinuousLinearMap (SpherePacking.Jacobi.operator n k L)

noncomputable def SpherePacking.Jacobi.rayleigh (n k L : ℕ) (x : Space k L) : ℝ

The rayleigh used in the spherical-code argument.

Equations

• SpherePacking.Jacobi.rayleigh n k L x = (SpherePacking.Jacobi.continuousOperator n k L).rayleighQuotient x

theorem SpherePacking.Jacobi.rayleigh_bddAbove (n k L : ℕ) : BddAbove (Set.range fun (x : { x : Space k L // x ≠ 0 }) => rayleigh n k L ↑x)

noncomputable def SpherePacking.Jacobi.topEigenvalue (n k L : ℕ) : ℝ

The top eigenvalue used in the spherical-code argument.

Equations

• SpherePacking.Jacobi.topEigenvalue n k L = ⨆ (x : { x : SpherePacking.Jacobi.Space k L // x ≠ 0 }), SpherePacking.Jacobi.rayleigh n k L ↑x

theorem SpherePacking.Jacobi.rayleigh_le_top (n k L : ℕ) (x : Space k L) (hx : x ≠ 0) : rayleigh n k L x ≤ topEigenvalue n k L

theorem SpherePacking.Jacobi.topEigenvalue_hasEigenvalue (n k L : ℕ) : Module.End.HasEigenvalue (operator n k L) (topEigenvalue n k L)

theorem SpherePacking.Jacobi.exists_topEigenvector (n k L : ℕ) : ∃ (x : Space k L), x ≠ 0 ∧ (operator n k L) x = topEigenvalue n k L • x

theorem SpherePacking.Jacobi.rayleigh_eq_inner (n k L : ℕ) (x : Space k L) : rayleigh n k L x = inner ℝ ((operator n k L) x) x / ‖x‖ ^ 2

@[reducible, inline]

abbrev SpherePacking.Perron.coordinateAbs (k L : ℕ) (x : Jacobi.Space k L) : Jacobi.Space k L

The coordinate abs used in the spherical-code argument.

Equations

• SpherePacking.Perron.coordinateAbs k L x = MetricCodes.Spherical.HigherHierarchyFinitePerron.coordinateAbs x

theorem SpherePacking.Perron.coordinateAbs_nonneg (k L : ℕ) (x : Jacobi.Space k L) (p : Jacobi.Index k L) : 0 ≤ (coordinateAbs k L x).ofLp p

theorem SpherePacking.Perron.coordinateAbs_norm (k L : ℕ) (x : Jacobi.Space k L) : ‖coordinateAbs k L x‖ = ‖x‖

theorem SpherePacking.Perron.coordinateAbs_ne_zero (k L : ℕ) {x : Jacobi.Space k L} (hx : x ≠ 0) : coordinateAbs k L x ≠ 0

theorem SpherePacking.Perron.matrix_entry_nonneg {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (p q : Jacobi.Index k L) : 0 ≤ Jacobi.matrix n k L p q

theorem SpherePacking.Perron.inner_le_inner_coordinateAbs {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (x : Jacobi.Space k L) : inner ℝ ((Jacobi.operator n k L) x) x ≤ inner ℝ ((Jacobi.operator n k L) (coordinateAbs k L x)) (coordinateAbs k L x)

theorem SpherePacking.Perron.rayleigh_le_coordinateAbs {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (x : Jacobi.Space k L) : Jacobi.rayleigh n k L x ≤ Jacobi.rayleigh n k L (coordinateAbs k L x)

theorem SpherePacking.Perron.rayleigh_eq_of_eigenvector (n k L : ℕ) (x : Jacobi.Space k L) (hx : x ≠ 0) (eigenvalue : ℝ) (heig : (Jacobi.operator n k L) x = eigenvalue • x) : Jacobi.rayleigh n k L x = eigenvalue

theorem SpherePacking.Perron.coordinateAbs_top_rayleigh {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (x : Jacobi.Space k L) (hx : x ≠ 0) (heig : (Jacobi.operator n k L) x = Jacobi.topEigenvalue n k L • x) : Jacobi.rayleigh n k L (coordinateAbs k L x) = Jacobi.topEigenvalue n k L

theorem SpherePacking.Perron.exists_nonnegative_topEigenvector {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) : ∃ (x : Jacobi.Space k L), x ≠ 0 ∧ (Jacobi.operator n k L) x = Jacobi.topEigenvalue n k L • x ∧ ∀ (p : Jacobi.Index k L), 0 ≤ x.ofLp p

theorem SpherePacking.Perron.exists_nonnegative_unit_topEigenvector {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) : ∃ (x : Jacobi.Space k L), ‖x‖ = 1 ∧ (Jacobi.operator n k L) x = Jacobi.topEigenvalue n k L • x ∧ ∀ (p : Jacobi.Index k L), 0 ≤ x.ofLp p

theorem SpherePacking.Perron.unit_coordinate_sq_sum {k L : ℕ} {x : Jacobi.Space k L} (hx : ‖x‖ = 1) : ∑ p : Jacobi.Index k L, x.ofLp p ^ 2 = 1

theorem SpherePacking.SpectralAsymptotics.tendsto_floored_ratio {a : ℝ} (ha : 0 ≤ a) : Filter.Tendsto (fun (n : ℕ) => ↑⌊a * ↑n⌋₊ / ↑n) Filter.atTop (nhds a)

noncomputable def SpherePacking.SpectralAsymptotics.normalizedCoefficient (x y z : ℝ) : ℝ

The normalized coefficient used in the spherical-code argument.

Equations

• SpherePacking.SpectralAsymptotics.normalizedCoefficient x y z = (x - y + z) * (x + y + 1 - 2 * z) / √((x + z) * (x + 1 - 2 * z) * (2 * x + 1 - 2 * z) * (2 * x + 1))

theorem SpherePacking.SpectralAsymptotics.jacobiCoefficient_eq_normalized (n k i : ℕ) (hn : 0 < n) : Gegenbauer.jacobiCoefficient n k i = normalizedCoefficient (↑i / ↑n) (↑k / ↑n) (1 / ↑n)

theorem SpherePacking.SpectralAsymptotics.tridiagonal_quadratic_sum (d : ℕ) (c v : ℕ → ℝ) : ∑ p ∈ Finset.range (d + 1), ∑ q ∈ Finset.range (d + 1), (if p + 1 = q then c p else if q + 1 = p then c q else 0) * v q * v p = 2 * ∑ p ∈ Finset.range d, c p * v p * v (p + 1)

def SpherePacking.SpectralAsymptotics.terminalIndicator (d m p : ℕ) : ℝ

The terminal indicator used in the spherical-code argument.

Equations

• SpherePacking.SpectralAsymptotics.terminalIndicator d m p = if d - m ≤ p then 1 else 0

theorem SpherePacking.SpectralAsymptotics.terminal_indicator_sum (d m : ℕ) (hm : m ≤ d) : ∑ p ∈ Finset.range (d + 1), terminalIndicator d m p = ↑m + 1

theorem SpherePacking.SpectralAsymptotics.terminal_indicator_edge_sum (d m : ℕ) (hm : m ≤ d) (c : ℕ → ℝ) : ∑ p ∈ Finset.range d, c p * terminalIndicator d m p * terminalIndicator d m (p + 1) = ∑ r ∈ Finset.range m, c (d - m + r)

def SpherePacking.SpectralAsymptotics.terminalVector (k L m : ℕ) : Jacobi.Space k L

The terminal vector used in the spherical-code argument.

Equations

• SpherePacking.SpectralAsymptotics.terminalVector k L m = WithLp.toLp 2 fun (p : Fin (L - k + 1)) => SpherePacking.SpectralAsymptotics.terminalIndicator (L - k) m ↑p

theorem SpherePacking.SpectralAsymptotics.terminalVector_last (k L m : ℕ) : (terminalVector k L m).ofLp (Fin.last (L - k)) = 1

theorem SpherePacking.SpectralAsymptotics.terminalVector_ne_zero (k L m : ℕ) : terminalVector k L m ≠ 0

theorem SpherePacking.SpectralAsymptotics.terminalVector_norm_sq (k L m : ℕ) (hm : m ≤ L - k) : ‖terminalVector k L m‖ ^ 2 = ↑m + 1

theorem SpherePacking.SpectralAsymptotics.terminalVector_inner (n k L m : ℕ) (hkl : k ≤ L) (hm : m ≤ L - k) : inner ℝ ((Jacobi.operator n k L) (terminalVector k L m)) (terminalVector k L m) = 2 * ∑ r ∈ Finset.range m, Gegenbauer.jacobiCoefficient n k (L - m + r)

theorem SpherePacking.SpectralAsymptotics.terminalVector_rayleigh (n k L m : ℕ) (hkl : k ≤ L) (hm : m ≤ L - k) : Jacobi.rayleigh n k L (terminalVector k L m) = (2 * ∑ r ∈ Finset.range m, Gegenbauer.jacobiCoefficient n k (L - m + r)) / (↑m + 1)

theorem SpherePacking.SpectralAsymptotics.terminal_edge_sum_le_top (n k L m : ℕ) (hkl : k ≤ L) (hm : m ≤ L - k) : (2 * ∑ r ∈ Finset.range m, Gegenbauer.jacobiCoefficient n k (L - m + r)) / (↑m + 1) ≤ Jacobi.topEigenvalue n k L

theorem SpherePacking.isometric_mixed_kernel_eq_overlap {α : Type u_1} {ι : Type u_2} {ρ : Type u_3} {F : Type u_4} {E : Type u_5} [Fintype ι] [Fintype ρ] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] (bE : OrthonormalBasis ι ℝ E) (bF : OrthonormalBasis ρ ℝ F) (f : α → F →ₗᵢ[ℝ] E) (x y : α) : SpherePacking.mixedHilbertSchmidtKernel✝ bE (fun (z : α) => (f z).toLinearMap) (fun (z : α) => (f z).toLinearMap) x y = SpherePacking.finiteHilbertSchmidtKernel✝ bF (fun (x_1 : Unit) => LinearMap.adjoint (f x).toLinearMap ∘ₗ (f y).toLinearMap) () ()

theorem SpherePacking.isometric_mixed_kernel_nonneg {α : Type u_1} {ι : Type u_2} {ρ : Type u_3} {F : Type u_4} {E : Type u_5} [Fintype ι] [Fintype ρ] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] (bE : OrthonormalBasis ι ℝ E) (bF : OrthonormalBasis ρ ℝ F) (f : α → F →ₗᵢ[ℝ] E) (x y : α) : 0 ≤ SpherePacking.mixedHilbertSchmidtKernel✝ bE (fun (z : α) => (f z).toLinearMap) (fun (z : α) => (f z).toLinearMap) x y

theorem SpherePacking.isometric_mixed_kernel_diag {α : Type u_1} {ι : Type u_2} {ρ : Type u_3} {F : Type u_4} {E : Type u_5} [Fintype ι] [Fintype ρ] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] (bE : OrthonormalBasis ι ℝ E) (bF : OrthonormalBasis ρ ℝ F) (f : α → F →ₗᵢ[ℝ] E) (x : α) : SpherePacking.mixedHilbertSchmidtKernel✝ bE (fun (z : α) => (f z).toLinearMap) (fun (z : α) => (f z).toLinearMap) x x = ↑(Module.finrank ℝ F)

theorem SpherePacking.finiteGramRecurrenceWeight_nonneg (n k L : ℕ) (v : Jacobi.Space k L) (hv : ∀ (i : Jacobi.Index k L), 0 ≤ v.ofLp i) (i : Jacobi.Index k L) : 0 ≤ SpherePacking.finiteGramRecurrenceWeight✝ n k L v i

theorem SpherePacking.finiteGramRecurrenceNormalization_pos {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (v : Jacobi.Space k L) (hunit : ‖v‖ = 1) (hv : ∀ (i : Jacobi.Index k L), 0 ≤ v.ofLp i) : 0 < SpherePacking.finiteGramRecurrenceNormalization✝ n k L v

theorem SpherePacking.finiteGramFibreAmplitude_sq {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (v : Jacobi.Space k L) (hunit : ‖v‖ = 1) (hv : ∀ (i : Jacobi.Index k L), 0 ≤ v.ofLp i) (i : Jacobi.Index k L) : SpherePacking.finiteGramFibreAmplitude✝ n k L v i ^ 2 = SpherePacking.finiteGramRecurrenceWeight✝ n k L v i / SpherePacking.finiteGramRecurrenceNormalization✝ n k L v

theorem SpherePacking.finiteGramFibreAmplitude_sq_sum {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (v : Jacobi.Space k L) (hunit : ‖v‖ = 1) (hv : ∀ (i : Jacobi.Index k L), 0 ≤ v.ofLp i) : ∑ i : Jacobi.Index k L, SpherePacking.finiteGramFibreAmplitude✝ n k L v i ^ 2 = 1

theorem SpherePacking.finiteGramFibreAmplitudeVector_unit {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (v : Jacobi.Space k L) (hunit : ‖v‖ = 1) (hv : ∀ (i : Jacobi.Index k L), 0 ≤ v.ofLp i) : ‖SpherePacking.finiteGramFibreAmplitudeVector✝ n k L v‖ = 1

structure SpherePacking.FiniteGramCertificate (n k L : ℕ) : Type

Data encoding the finite gram certificate construction.

• weights : Jacobi.Space k L

  The weights component.

• weights_unit : ‖self.weights‖ = 1
• weights_eigenvector : (Jacobi.operator n k L) self.weights = Jacobi.topEigenvalue n k L • self.weights
• weights_nonneg (i : Jacobi.Index k L) : 0 ≤ self.weights.ofLp i
• fibreAmplitudes : Jacobi.Space k L

  The fibre amplitudes component.

• fibreAmplitudes_eq (i : Jacobi.Index k L) : self.fibreAmplitudes.ofLp i = SpherePacking.finiteGramFibreAmplitude✝ n k L self.weights i
• fibreAmplitudes_unit : ‖self.fibreAmplitudes‖ = 1
• degreeFibre (i : Jacobi.Index k L) : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i

  The degree fibre component.

• degreeInjection (i : Jacobi.Index k L) : SpherePacking.CertificateDegreeAmbient✝ n k L i →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L

  The degree injection component.

• degree_orthogonal (i j : Jacobi.Index k L) : i ≠ j → ∀ (u : SpherePacking.CertificateDegreeAmbient✝ n k L i) (v : SpherePacking.CertificateDegreeAmbient✝ n k L j), inner ℝ ((self.degreeInjection i) u) ((self.degreeInjection j) v) = 0
• fibre : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L

  The fibre component.

• fibre_eq_weighted_degree (x : Euclidean n) (v : SpherePacking.CertificateFibre✝ n k) : (self.fibre x) v = ∑ i : Jacobi.Index k L, self.fibreAmplitudes.ofLp i • (self.degreeInjection i) ((self.degreeFibre i x) v)
• coordinateDimension : ℕ

  The coordinate dimension component.

• lift : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗ[ℝ] Euclidean self.coordinateDimension

  The lift component.

• bulk : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗ[ℝ] Euclidean self.coordinateDimension

  The bulk component.

• boundary : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗ[ℝ] Euclidean self.coordinateDimension

  The boundary component.

• remainder : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗ[ℝ] Euclidean self.coordinateDimension

  The remainder component.

• spectralCoefficient : ℝ

  The spectral coefficient component.

• spectralCoefficient_sq : self.spectralCoefficient ^ 2 = Jacobi.topEigenvalue n k L
• decomposition (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → self.lift x = self.spectralCoefficient • self.bulk x + 1 • self.boundary x + self.remainder x
• lift_kernel (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, SpherePacking.finiteHilbertSchmidtKernel✝ (SpherePacking.certificateFibreBasis✝ n k) self.lift x y = inner ℝ x y * SpherePacking.isometricPackingKernel✝ self.fibre x y
• bulk_kernel (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, SpherePacking.finiteHilbertSchmidtKernel✝ (SpherePacking.certificateFibreBasis✝ n k) self.bulk x y = SpherePacking.isometricPackingKernel✝ self.fibre x y
• bulk_boundary_orthogonal (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.bulk x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((self.boundary y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = 0
• bulk_remainder_orthogonal (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.bulk x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((self.remainder y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = 0
• boundary_remainder_orthogonal (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.boundary x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((self.remainder y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = 0

theorem SpherePacking.finiteGramCertificate_shift_identity {n k L : ℕ} (certificate : FiniteGramCertificate n k L) {x y : Euclidean n} (hx : x ∈ SpherePacking.unitSphere✝ n) (hy : y ∈ SpherePacking.unitSphere✝ n) : (inner ℝ x y - Jacobi.topEigenvalue n k L) * SpherePacking.isometricPackingKernel✝ certificate.fibre x y = SpherePacking.finiteHilbertSchmidtKernel✝ (SpherePacking.certificateFibreBasis✝ n k) certificate.boundary x y + SpherePacking.finiteHilbertSchmidtKernel✝ (SpherePacking.certificateFibreBasis✝ n k) certificate.remainder x y

theorem SpherePacking.isometricPackingKernel_nonneg {n k L : ℕ} (f : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (x y : Euclidean n) : 0 ≤ SpherePacking.isometricPackingKernel✝ f x y

theorem SpherePacking.isometricPackingKernel_diag {n k L : ℕ} (f : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (x : Euclidean n) : SpherePacking.isometricPackingKernel✝ f x x = ↑(Gegenbauer.fibreDimension n k)

theorem SpherePacking.isometricPackingKernel_trace_cauchy {n k L : ℕ} (f : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (C : Finset (Euclidean n)) : (↑C.card * ↑(Gegenbauer.fibreDimension n k)) ^ 2 ≤ ↑(truncatedHarmonicDimension n k L) * ∑ x ∈ C, ∑ y ∈ C, SpherePacking.isometricPackingKernel✝ f x y

theorem SpherePacking.finiteGramCertificate_shift_sum_nonnegative {n k L : ℕ} {s : ℝ} (certificate : FiniteGramCertificate n k L) (C : SphericalCode n s) : 0 ≤ ∑ x ∈ C.points, ∑ y ∈ C.points, (inner ℝ x y - Jacobi.topEigenvalue n k L) * SpherePacking.isometricPackingKernel✝ certificate.fibre x y

theorem SpherePacking.finiteGramCertificate_auxiliary_sum_lower {n k L : ℕ} {s : ℝ} (certificate : FiniteGramCertificate n k L) (C : SphericalCode n s) : (Jacobi.topEigenvalue n k L - s) * ∑ x ∈ C.points, ∑ y ∈ C.points, SpherePacking.isometricPackingKernel✝ certificate.fibre x y ≤ ∑ x ∈ C.points, ∑ y ∈ C.points, SpherePacking.auxiliaryFiniteGramKernel✝ certificate s x y

theorem SpherePacking.finiteGramCertificate_sphericalCode_bound {n k L : ℕ} (hn : 3 ≤ n) (hkl : k ≤ L) (certificate : FiniteGramCertificate n k L) {s : ℝ} (hs : s ≤ 1) (hgap : s < Jacobi.topEigenvalue n k L) (C : SphericalCode n s) : ↑C.points.card ≤ (1 - s) / (Jacobi.topEigenvalue n k L - s) * (↑(truncatedHarmonicDimension n k L) / ↑(Gegenbauer.fibreDimension n k))

theorem SpherePacking.HarmonicCertificateAssembly.degreeBlock_dimension_sum (n k L : ℕ) (hkl : k ≤ L) : ∑ i : Jacobi.Index k L, Gegenbauer.harmonicDimension n (k + ↑i) = truncatedHarmonicDimension n k L

theorem SpherePacking.HarmonicCertificateAssembly.degreeBlockIndex_card (n k L : ℕ) (hkl : k ≤ L) : Fintype.card (SpherePacking.HarmonicCertificateAssembly.DegreeBlockIndex✝ n k L) = truncatedHarmonicDimension n k L

theorem SpherePacking.HarmonicCertificateAssembly.degreeBlockSingle_orthogonal (n k L : ℕ) (i j : Jacobi.Index k L) (hij : i ≠ j) (u : SpherePacking.CertificateDegreeAmbient✝ n k L i) (v : SpherePacking.CertificateDegreeAmbient✝ n k L j) : inner ℝ ((SpherePacking.HarmonicCertificateAssembly.degreeBlockSingle✝ n k L i) u) ((SpherePacking.HarmonicCertificateAssembly.degreeBlockSingle✝ n k L j) v) = 0

theorem SpherePacking.HarmonicCertificateAssembly.degreeBlockInclusion_orthogonal (n k L : ℕ) (hkl : k ≤ L) (i j : Jacobi.Index k L) (hij : i ≠ j) (u : SpherePacking.CertificateDegreeAmbient✝ n k L i) (v : SpherePacking.CertificateDegreeAmbient✝ n k L j) : inner ℝ ((SpherePacking.HarmonicCertificateAssembly.degreeBlockInclusion✝ n k L hkl i) u) ((SpherePacking.HarmonicCertificateAssembly.degreeBlockInclusion✝ n k L hkl j) v) = 0

@[simp]

theorem SpherePacking.HarmonicCertificateAssembly.weightedDegreeLinearMap_apply (n k L : ℕ) (hkl : k ≤ L) (weights : Jacobi.Space k L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (x : Euclidean n) (v : SpherePacking.CertificateFibre✝ n k) : (SpherePacking.HarmonicCertificateAssembly.weightedDegreeLinearMap✝ n k L hkl weights degreeFibre x) v = ∑ i : Jacobi.Index k L, weights.ofLp i • (SpherePacking.HarmonicCertificateAssembly.degreeBlockInclusion✝ n k L hkl i) ((degreeFibre i x) v)

theorem SpherePacking.HarmonicCertificateAssembly.weightedDegreeLinearMap_inner (n k L : ℕ) (hkl : k ≤ L) (weights : Jacobi.Space k L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (x : Euclidean n) (v w : SpherePacking.CertificateFibre✝ n k) : inner ℝ ((SpherePacking.HarmonicCertificateAssembly.weightedDegreeLinearMap✝ n k L hkl weights degreeFibre x) v) ((SpherePacking.HarmonicCertificateAssembly.weightedDegreeLinearMap✝ n k L hkl weights degreeFibre x) w) = (∑ i : Jacobi.Index k L, weights.ofLp i ^ 2) * inner ℝ v w

theorem SpherePacking.HarmonicCertificateAssembly.weightedDegreeLinearMap_inner_of_unit (n k L : ℕ) (hkl : k ≤ L) (weights : Jacobi.Space k L) (hweights : ‖weights‖ = 1) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (x : Euclidean n) (v w : SpherePacking.CertificateFibre✝ n k) : inner ℝ ((SpherePacking.HarmonicCertificateAssembly.weightedDegreeLinearMap✝ n k L hkl weights degreeFibre x) v) ((SpherePacking.HarmonicCertificateAssembly.weightedDegreeLinearMap✝ n k L hkl weights degreeFibre x) w) = inner ℝ v w

@[simp]

theorem SpherePacking.HarmonicCertificateAssembly.weightedDegreeIsometry_apply (n k L : ℕ) (hkl : k ≤ L) (weights : Jacobi.Space k L) (hweights : ‖weights‖ = 1) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (x : Euclidean n) (v : SpherePacking.CertificateFibre✝ n k) : (SpherePacking.HarmonicCertificateAssembly.weightedDegreeIsometry✝ n k L hkl weights hweights degreeFibre x) v = ∑ i : Jacobi.Index k L, weights.ofLp i • (SpherePacking.HarmonicCertificateAssembly.degreeBlockInclusion✝ n k L hkl i) ((degreeFibre i x) v)

theorem SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights_unit (n k L : ℕ) (hn : 3 ≤ n) : ‖SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights✝ n k L hn‖ = 1

theorem SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights_eigenvector (n k L : ℕ) (hn : 3 ≤ n) : (Jacobi.operator n k L) (SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights✝ n k L hn) = Jacobi.topEigenvalue n k L • SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights✝ n k L hn

theorem SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights_nonneg (n k L : ℕ) (hn : 3 ≤ n) (i : Jacobi.Index k L) : 0 ≤ (SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights✝ n k L hn).ofLp i

theorem SpherePacking.HarmonicCertificateAssembly.harmonicRecurrenceNormalization_pos (n k L : ℕ) (hn : 3 ≤ n) : 0 < SpherePacking.HarmonicCertificateAssembly.harmonicRecurrenceNormalization✝ n k L hn

theorem SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes_unit (n k L : ℕ) (hn : 3 ≤ n) : ‖SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn‖ = 1

@[simp]

theorem SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes_apply (n k L : ℕ) (hn : 3 ≤ n) (i : Jacobi.Index k L) : (SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn).ofLp i = SpherePacking.finiteGramFibreAmplitude✝ n k L (SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights✝ n k L hn) i

theorem SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes_sq (n k L : ℕ) (hn : 3 ≤ n) (i : Jacobi.Index k L) : (SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn).ofLp i ^ 2 = SpherePacking.HarmonicCertificateAssembly.harmonicRecurrenceWeight✝ n k L hn i / SpherePacking.HarmonicCertificateAssembly.harmonicRecurrenceNormalization✝ n k L hn

@[simp]

theorem SpherePacking.HarmonicCertificateAssembly.harmonicWeightedFibre_apply (n k L : ℕ) (hn : 3 ≤ n) (hkl : k ≤ L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (x : Euclidean n) (v : SpherePacking.CertificateFibre✝ n k) : (SpherePacking.HarmonicCertificateAssembly.harmonicWeightedFibre✝ n k L hn hkl degreeFibre x) v = ∑ i : Jacobi.Index k L, (SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn).ofLp i • (SpherePacking.HarmonicCertificateAssembly.degreeBlockInclusion✝ n k L hkl i) ((degreeFibre i x) v)

structure SpherePacking.HarmonicCertificateAssembly.HarmonicCoordinateData (n k L : ℕ) (fibre : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) : Type

Data encoding the harmonic coordinate construction.

• coordinateDimension : ℕ

  The coordinate dimension component.

• lift : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗ[ℝ] Euclidean self.coordinateDimension

  The lift component.

• bulk : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗ[ℝ] Euclidean self.coordinateDimension

  The bulk component.

• boundary : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗ[ℝ] Euclidean self.coordinateDimension

  The boundary component.

• remainder : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗ[ℝ] Euclidean self.coordinateDimension

  The remainder component.

• spectralCoefficient : ℝ

  The spectral coefficient component.

• spectralCoefficient_sq : self.spectralCoefficient ^ 2 = Jacobi.topEigenvalue n k L
• decomposition (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → self.lift x = self.spectralCoefficient • self.bulk x + 1 • self.boundary x + self.remainder x
• lift_kernel (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, SpherePacking.finiteHilbertSchmidtKernel✝ (SpherePacking.certificateFibreBasis✝ n k) self.lift x y = inner ℝ x y * SpherePacking.isometricPackingKernel✝ fibre x y
• bulk_kernel (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, SpherePacking.finiteHilbertSchmidtKernel✝ (SpherePacking.certificateFibreBasis✝ n k) self.bulk x y = SpherePacking.isometricPackingKernel✝ fibre x y
• bulk_boundary_orthogonal (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.bulk x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((self.boundary y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = 0
• bulk_remainder_orthogonal (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.bulk x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((self.remainder y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = 0
• boundary_remainder_orthogonal (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.boundary x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((self.remainder y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = 0

theorem SpherePacking.solidHarmonicAxisLift_succ_apply (n k r : ℕ) (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) : (solidHarmonicAxisLift n k x (r + 1)) p = MvPolynomial.C (2 * ↑r + harmonicAxisParameter n k - 2) * axisPolynomial n x * (solidHarmonicAxisLift n k x r) p - MvPolynomial.C (↑r * (↑r + harmonicAxisParameter n k - 3)) * radialPolynomial n * (solidHarmonicAxisLift n k x (r - 1)) p

theorem SpherePacking.solidHarmonicAxisLift_harmonic_and_directional {n k : ℕ} (x : Euclidean n) (hx : ‖x‖ = 1) {p : MvPolynomial (Fin n) ℝ} (hp : p ∈ tangentHarmonicSubmodule n k x) (r : ℕ) : (polynomialLaplacian n) ((solidHarmonicAxisLift n k x r) p) = 0 ∧ (directionalDerivative n x) ((solidHarmonicAxisLift n k x r) p) = MvPolynomial.C (↑r * (↑r + harmonicAxisParameter n k - 3)) * (solidHarmonicAxisLift n k x (r - 1)) p

theorem SpherePacking.solidHarmonicAxisLift_mem_harmonic {n k : ℕ} (x : Euclidean n) (hx : ‖x‖ = 1) {p : MvPolynomial (Fin n) ℝ} (hp : p ∈ tangentHarmonicSubmodule n k x) (r : ℕ) : (solidHarmonicAxisLift n k x r) p ∈ harmonicHomogeneousSubmodule n (k + r)

def SpherePacking.solidHarmonicAxisFischerScale (n k r : ℕ) : ℝ

The solid harmonic axis fischer scale used in the spherical-code argument.

Equations

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

@[simp]

theorem SpherePacking.solidHarmonicAxisFischerScale_zero (n k : ℕ) : solidHarmonicAxisFischerScale n k 0 = 1

theorem SpherePacking.solidHarmonicAxisFischerScale_succ (n k r : ℕ) : solidHarmonicAxisFischerScale n k (r + 1) = solidHarmonicAxisFischerScale n k r * (2 * ↑r + harmonicAxisParameter n k - 2) * (↑r + 1) * (↑r + harmonicAxisParameter n k - 2)

theorem SpherePacking.solidHarmonicAxisFischerScale_pos {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : 0 < solidHarmonicAxisFischerScale n k r

theorem SpherePacking.fischer_polynomialInner_constant_mul_left (n : ℕ) (c : ℝ) (p q : MvPolynomial (Fin n) ℝ) : Fischer.polynomialInner n (MvPolynomial.C c * p) q = c * Fischer.polynomialInner n p q

theorem SpherePacking.fischer_polynomialInner_constant_mul_right (n : ℕ) (c : ℝ) (p q : MvPolynomial (Fin n) ℝ) : Fischer.polynomialInner n p (MvPolynomial.C c * q) = c * Fischer.polynomialInner n p q

theorem SpherePacking.solidHarmonicAxisLift_fischer_inner_succ {n k : ℕ} (x : Euclidean n) (hx : ‖x‖ = 1) (p q : ↥(tangentHarmonicSubmodule n k x)) (r : ℕ) : Fischer.polynomialInner n ((solidHarmonicAxisLift n k x (r + 1)) ↑p) ((solidHarmonicAxisLift n k x (r + 1)) ↑q) = (2 * ↑r + harmonicAxisParameter n k - 2) * (↑r + 1) * (↑r + harmonicAxisParameter n k - 2) * Fischer.polynomialInner n ((solidHarmonicAxisLift n k x r) ↑p) ((solidHarmonicAxisLift n k x r) ↑q)

theorem SpherePacking.solidHarmonicAxisLift_fischer_inner {n k : ℕ} (x : Euclidean n) (hx : ‖x‖ = 1) (p q : ↥(tangentHarmonicSubmodule n k x)) (r : ℕ) : Fischer.polynomialInner n ((solidHarmonicAxisLift n k x r) ↑p) ((solidHarmonicAxisLift n k x r) ↑q) = solidHarmonicAxisFischerScale n k r * Fischer.polynomialInner n ↑p ↑q

noncomputable def SpherePacking.solidHarmonicAxisPolynomialIsometry {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) : ↥(tangentHarmonicSubmodule n k x) →ₗᵢ[ℝ] ↥(harmonicHomogeneousSubmodule n (k + r))

The solid harmonic axis polynomial isometry used in the spherical-code argument.

Equations

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

@[simp]

theorem SpherePacking.harmonicReferenceUnitAxis_norm {n : ℕ} (hn : 0 < n) : ‖SpherePacking.harmonicReferenceUnitAxis✝ hn‖ = 1

noncomputable def SpherePacking.harmonicDegreeFibre {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (i : Jacobi.Index k L) (x : Euclidean n) : SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i

The harmonic degree fibre used in the spherical-code argument.

Equations

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

@[simp]

theorem SpherePacking.harmonicDegreeFibre_of_unit {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (i : Jacobi.Index k L) (x : Euclidean n) (hx : ‖x‖ = 1) : harmonicDegreeFibre hn k L i x = SpherePacking.unitHarmonicDegreeFibre✝ hn k L i x hx

theorem SpherePacking.JacobiSymmetrization.harmonicDimension_scaled_choose {n : ℕ} (hn : 3 ≤ n) (i : ℕ) : (n - 2) * Gegenbauer.harmonicDimension n i = (2 * i + n - 2) * (n + i - 3).choose i

theorem SpherePacking.JacobiSymmetrization.harmonicDimension_cross_mul {n : ℕ} (hn : 3 ≤ n) (i : ℕ) : Gegenbauer.harmonicDimension n i * (2 * i + n) * (i + n - 2) = Gegenbauer.harmonicDimension n (i + 1) * (2 * i + n - 2) * (i + 1)

theorem SpherePacking.SourceJacobiWeights.positiveRadicalSymmetrization {d e a b p q r : ℝ} (hd : 0 < d) (he : 0 < e) (ha : 0 < a) (hb : 0 < b) (hp : 0 < p) (hq : 0 < q) (hr : 0 ≤ r) (hcross : d * q * b = e * p * a) : r / (a * p) * √d = r / √(a * b * p * q) * √e

theorem SpherePacking.SourceJacobiWeights.alphaSq_sqrt_harmonicDimension {n k i : ℕ} (hn : 3 ≤ n) (hki : k ≤ i) : Gegenbauer.alphaSq n k i * √↑(Gegenbauer.harmonicDimension n i) = Gegenbauer.jacobiCoefficient n k i * √↑(Gegenbauer.harmonicDimension n (i + 1))

theorem SpherePacking.SourceJacobiWeights.betaSq_sqrt_harmonicDimension {n k i : ℕ} (hn : 3 ≤ n) (hki : k ≤ i) : Gegenbauer.betaSq n k (i + 1) * √↑(Gegenbauer.harmonicDimension n (i + 1)) = Gegenbauer.jacobiCoefficient n k i * √↑(Gegenbauer.harmonicDimension n i)

theorem SpherePacking.SourceJacobiWeights.jacobiMatrix_mul_sqrt_harmonicDimension {n k L : ℕ} (hn : 3 ≤ n) (m i : Jacobi.Index k L) : SpherePacking.Gegenbauer.jacobiMatrix✝ n k L m i * √↑(Gegenbauer.harmonicDimension n (k + ↑m)) = SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L m i * √↑(Gegenbauer.harmonicDimension n (k + ↑i))

theorem SpherePacking.SourceJacobiWeights.finiteGramRecurrenceWeight_eigenrecurrence {n k L : ℕ} (hn : 3 ≤ n) (v : Jacobi.Space k L) (eigenvalue : ℝ) (heigen : (Jacobi.operator n k L) v = eigenvalue • v) (m : Jacobi.Index k L) : ∑ i : Jacobi.Index k L, SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L m i * SpherePacking.finiteGramRecurrenceWeight✝ n k L v i = eigenvalue * SpherePacking.finiteGramRecurrenceWeight✝ n k L v m

theorem SpherePacking.SourceJacobiWeights.jacobiMatrix_adjacent_pos {n k L : ℕ} (hn : 3 ≤ n) (p q : Jacobi.Index k L) (hadjacent : ↑p + 1 = ↑q ∨ ↑q + 1 = ↑p) : 0 < SpherePacking.Gegenbauer.jacobiMatrix✝ n k L p q

theorem SpherePacking.SourceJacobiWeights.sourceChannelCoefficient_pos_of_adjacent {n k L : ℕ} (hn : 3 ≤ n) (m i : Jacobi.Index k L) (hadjacent : ↑m + 1 = ↑i ∨ ↑i + 1 = ↑m) : 0 < SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L m i

theorem SpherePacking.SourceJacobiWeights.nonnegative_eigenvector_zero_propagates {n k L : ℕ} (hn : 3 ≤ n) (v : Jacobi.Space k L) (eigenvalue : ℝ) (heigen : (Jacobi.operator n k L) v = eigenvalue • v) (hnonnegative : ∀ (i : Jacobi.Index k L), 0 ≤ v.ofLp i) (p q : Jacobi.Index k L) (hp : v.ofLp p = 0) (hadjacent : ↑p + 1 = ↑q ∨ ↑q + 1 = ↑p) : v.ofLp q = 0

theorem SpherePacking.SourceJacobiWeights.nonnegative_eigenvector_coordinate_pos {n k L : ℕ} (hn : 3 ≤ n) (v : Jacobi.Space k L) (eigenvalue : ℝ) (heigen : (Jacobi.operator n k L) v = eigenvalue • v) (hnonnegative : ∀ (i : Jacobi.Index k L), 0 ≤ v.ofLp i) (hnonzero : v ≠ 0) (i : Jacobi.Index k L) : 0 < v.ofLp i

theorem SpherePacking.SourceJacobiWeights.finiteGramRecurrenceWeight_pos_of_eigenvector {n k L : ℕ} (hn : 3 ≤ n) (v : Jacobi.Space k L) (eigenvalue : ℝ) (heigen : (Jacobi.operator n k L) v = eigenvalue • v) (hnonnegative : ∀ (i : Jacobi.Index k L), 0 ≤ v.ofLp i) (hnonzero : v ≠ 0) (i : Jacobi.Index k L) : 0 < SpherePacking.finiteGramRecurrenceWeight✝ n k L v i

theorem SpherePacking.SourceJacobiWeights.nonnegative_eigenvalue_pos_of_lt {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) (v : Jacobi.Space k L) (eigenvalue : ℝ) (heigen : (Jacobi.operator n k L) v = eigenvalue • v) (hnonnegative : ∀ (i : Jacobi.Index k L), 0 ≤ v.ofLp i) (hnonzero : v ≠ 0) : 0 < eigenvalue

theorem SpherePacking.HarmonicPerronPositivity.harmonicPerronWeights_ne_zero (n k L : ℕ) (hn : 3 ≤ n) : SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights✝ n k L hn ≠ 0

theorem SpherePacking.HarmonicPerronPositivity.harmonicRecurrenceWeight_pos (n k L : ℕ) (hn : 3 ≤ n) (i : Jacobi.Index k L) : 0 < SpherePacking.HarmonicCertificateAssembly.harmonicRecurrenceWeight✝ n k L hn i

theorem SpherePacking.HarmonicPerronPositivity.harmonicFibreAmplitudes_pos (n k L : ℕ) (hn : 3 ≤ n) (i : Jacobi.Index k L) : 0 < (SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn).ofLp i

theorem SpherePacking.HarmonicPerronPositivity.topEigenvalue_pos_of_lt {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) : 0 < Jacobi.topEigenvalue n k L

theorem SpherePacking.HarmonicCoordinateChannels.sourceChannelCoefficient_nonneg {n k L : ℕ} (hn : 3 ≤ n) (m i : Jacobi.Index k L) : 0 ≤ SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L m i

theorem SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient_sq {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) (target source : Jacobi.Index k L) : SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient✝ n k L hn target source ^ 2 = SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L source target * SpherePacking.HarmonicCertificateAssembly.harmonicRecurrenceWeight✝ n k L hn target / (Jacobi.topEigenvalue n k L * SpherePacking.HarmonicCertificateAssembly.harmonicRecurrenceWeight✝ n k L hn source)

theorem SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient_sq_sum {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) (source : Jacobi.Index k L) : ∑ target : Jacobi.Index k L, SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient✝ n k L hn target source ^ 2 = 1

theorem SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient_amplitude_identity {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) (target source : Jacobi.Index k L) : SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient✝ n k L hn target source * (SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn).ofLp target * √(SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L source target) = SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient✝ n k L hn target source ^ 2 * √(Jacobi.topEigenvalue n k L) * (SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn).ofLp source

theorem SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient_amplitude_sum {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) (source : Jacobi.Index k L) : ∑ target : Jacobi.Index k L, SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient✝ n k L hn target source * (SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn).ofLp target * √(SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L source target) = √(Jacobi.topEigenvalue n k L) * (SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn).ofLp source

structure SpherePacking.HarmonicCoordinateChannels.SourceAdjacentChannelData (n k L : ℕ) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) : Type

Data encoding the source adjacent channel construction.

• channel (target source : Jacobi.Index k L) : SpherePacking.CertificateDegreeAmbient✝ n k L source →ₗ[ℝ] SpherePacking.HarmonicCoordinateChannels.HarmonicDegreeRowChannelSpace✝ n k L target

  The channel component.

• channel_inner (target source : Jacobi.Index k L) : SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L source target ≠ 0 → ∀ (u v : SpherePacking.CertificateDegreeAmbient✝ n k L source), inner ℝ ((self.channel target source) u) ((self.channel target source) v) = inner ℝ u v
• channel_zero (target source : Jacobi.Index k L) : SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L source target = 0 → self.channel target source = 0
• channel_orthogonal (target source₁ source₂ : Jacobi.Index k L) : source₁ ≠ source₂ → ∀ (u : SpherePacking.CertificateDegreeAmbient✝ n k L source₁) (v : SpherePacking.CertificateDegreeAmbient✝ n k L source₂), inner ℝ ((self.channel target source₁) u) ((self.channel target source₂) v) = 0
• axis_projection (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ (target source : Jacobi.Index k L) (u : SpherePacking.CertificateFibre✝ n k), (LinearMap.adjoint (self.channel target source)) ((SpherePacking.HarmonicCoordinateChannels.harmonicDegreeAxisTensor✝ n k L target x) ((degreeFibre target x) u)) = √(SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L source target) • (degreeFibre source x) u

theorem SpherePacking.HarmonicCoordinateChannels.sourceAdjacentTargetLinearMap_inner {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (adjacent : SourceAdjacentChannelData n k L degreeFibre) (u v : SpherePacking.HarmonicCertificateAssembly.DegreeBlockPi✝ n k L) : inner ℝ ((SpherePacking.HarmonicCoordinateChannels.sourceAdjacentTargetLinearMap✝ hn degreeFibre adjacent) u) ((SpherePacking.HarmonicCoordinateChannels.sourceAdjacentTargetLinearMap✝ hn degreeFibre adjacent) v) = inner ℝ u v

theorem SpherePacking.HarmonicCoordinateChannels.sourceTargetRowTransportLinearMap_inner (n k L : ℕ) (hkl : k ≤ L) (u v : SpherePacking.HarmonicCoordinateChannels.SourceTargetRowSpace✝ n k L) : inner ℝ ((SpherePacking.HarmonicCoordinateChannels.sourceTargetRowTransportLinearMap✝ n k L hkl) u) ((SpherePacking.HarmonicCoordinateChannels.sourceTargetRowTransportLinearMap✝ n k L hkl) v) = inner ℝ u v

def SpherePacking.HarmonicCoordinateChannels.harmonicAxisTensor (n k L : ℕ) (x : Euclidean n) : SpherePacking.CertificateAmbient✝ n k L →ₗ[ℝ] SpherePacking.HarmonicCoordinateChannels.HarmonicRowChannelSpace✝ n k L

The harmonic axis tensor used in the spherical-code argument.

Equations

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

@[simp]

theorem SpherePacking.HarmonicCoordinateChannels.harmonicDegreeBlockEquiv_symm_degreeBlockInclusion (n k L : ℕ) (hkl : k ≤ L) (i : Jacobi.Index k L) (u : SpherePacking.CertificateDegreeAmbient✝ n k L i) : (SpherePacking.HarmonicCoordinateChannels.harmonicDegreeBlockEquiv✝ n k L hkl).symm ((SpherePacking.HarmonicCertificateAssembly.degreeBlockInclusion✝ n k L hkl i) u) = PiLp.single 2 i u

theorem SpherePacking.HarmonicCoordinateChannels.harmonicDegreeBlockEquiv_symm_weightedFibre (n k L : ℕ) (hn : 3 ≤ n) (hkl : k ≤ L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (x : Euclidean n) (u : SpherePacking.CertificateFibre✝ n k) (i : Jacobi.Index k L) : ((SpherePacking.HarmonicCoordinateChannels.harmonicDegreeBlockEquiv✝ n k L hkl).symm ((SpherePacking.HarmonicCertificateAssembly.harmonicWeightedFibre✝ n k L hn hkl degreeFibre x) u)).ofLp i = (SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn).ofLp i • (degreeFibre i x) u

theorem SpherePacking.HarmonicCoordinateChannels.sourceTargetRowTransport_inner_axisTensor (n k L : ℕ) (hkl : k ≤ L) (v : SpherePacking.HarmonicCoordinateChannels.SourceTargetRowSpace✝ n k L) (x : Euclidean n) (z : SpherePacking.CertificateAmbient✝ n k L) : inner ℝ ((SpherePacking.HarmonicCoordinateChannels.sourceTargetRowTransport✝ n k L hkl) v) ((harmonicAxisTensor n k L x) z) = ∑ target : Jacobi.Index k L, inner ℝ (v.ofLp target) ((SpherePacking.HarmonicCoordinateChannels.harmonicDegreeAxisTensor✝ n k L target x) (((SpherePacking.HarmonicCoordinateChannels.harmonicDegreeBlockEquiv✝ n k L hkl).symm z).ofLp target))

theorem SpherePacking.HarmonicCoordinateChannels.sourceAdjacentChannel_inner_degreeAxisTensor {n k L : ℕ} (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (adjacent : SourceAdjacentChannelData n k L degreeFibre) (x : Euclidean n) (hx : x ∈ SpherePacking.unitSphere✝ n) (target source : Jacobi.Index k L) (z : SpherePacking.CertificateDegreeAmbient✝ n k L source) (u : SpherePacking.CertificateFibre✝ n k) (a : ℝ) : inner ℝ ((adjacent.channel target source) z) ((SpherePacking.HarmonicCoordinateChannels.harmonicDegreeAxisTensor✝ n k L target x) (a • (degreeFibre target x) u)) = a * √(SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L source target) * inner ℝ z ((degreeFibre source x) u)

theorem SpherePacking.HarmonicCoordinateChannels.harmonicWeightedFibre_ambient_inner (n k L : ℕ) (hn : 3 ≤ n) (hkl : k ≤ L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (x : Euclidean n) (u : SpherePacking.CertificateFibre✝ n k) (z : SpherePacking.CertificateAmbient✝ n k L) : inner ℝ z ((SpherePacking.HarmonicCertificateAssembly.harmonicWeightedFibre✝ n k L hn hkl degreeFibre x) u) = ∑ source : Jacobi.Index k L, (SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes✝ n k L hn).ofLp source * inner ℝ (((SpherePacking.HarmonicCoordinateChannels.harmonicDegreeBlockEquiv✝ n k L hkl).symm z).ofLp source) ((degreeFibre source x) u)

theorem SpherePacking.HarmonicCoordinateChannels.sourceAdjacentHarmonicRow_inner_axis_fibre {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (adjacent : SourceAdjacentChannelData n k L degreeFibre) (x : Euclidean n) (hx : x ∈ SpherePacking.unitSphere✝ n) (u : SpherePacking.CertificateFibre✝ n k) (z : SpherePacking.CertificateAmbient✝ n k L) : inner ℝ ((SpherePacking.HarmonicCoordinateChannels.sourceAdjacentHarmonicRow✝ hn hkl degreeFibre adjacent) z) ((harmonicAxisTensor n k L x) ((SpherePacking.HarmonicCertificateAssembly.harmonicWeightedFibre✝ n k L hn ⋯ degreeFibre x) u)) = √(Jacobi.topEigenvalue n k L) * inner ℝ z ((SpherePacking.HarmonicCertificateAssembly.harmonicWeightedFibre✝ n k L hn ⋯ degreeFibre x) u)

@[simp]

theorem SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbeddingLinearMap_zero (n k L : ℕ) (row : SpherePacking.CertificateAmbient✝ n k L →ₗᵢ[ℝ] SpherePacking.HarmonicCoordinateChannels.HarmonicRowChannelSpace✝ n k L) (M : SpherePacking.HarmonicCoordinateChannels.ProjectionMatrixSpace✝ n k L) : ((SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbeddingLinearMap✝ n k L row) M).ofLp 0 = 0

theorem SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbeddingLinearMap_inner (n k L : ℕ) (row : SpherePacking.CertificateAmbient✝ n k L →ₗᵢ[ℝ] SpherePacking.HarmonicCoordinateChannels.HarmonicRowChannelSpace✝ n k L) (M N : SpherePacking.HarmonicCoordinateChannels.ProjectionMatrixSpace✝ n k L) : inner ℝ ((SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbeddingLinearMap✝ n k L row) M) ((SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbeddingLinearMap✝ n k L row) N) = inner ℝ M N

theorem SpherePacking.HarmonicCoordinateChannels.projectionMatrixFeature_inner {n k L : ℕ} (f : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (x y : Euclidean n) : inner ℝ (SpherePacking.HarmonicCoordinateChannels.projectionMatrixFeature✝ f x) (SpherePacking.HarmonicCoordinateChannels.projectionMatrixFeature✝ f y) = SpherePacking.isometricPackingKernel✝ f x y

@[simp]

theorem SpherePacking.HarmonicCoordinateChannels.rawLiftChannel_zero {n k L : ℕ} (f : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (x : Euclidean n) : (SpherePacking.HarmonicCoordinateChannels.rawLiftChannel✝ f x).ofLp 0 = 0

@[simp]

theorem SpherePacking.HarmonicCoordinateChannels.rawLiftChannel_succ {n k L : ℕ} (f : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (x : Euclidean n) (a : Fin n) : (SpherePacking.HarmonicCoordinateChannels.rawLiftChannel✝ f x).ofLp a.succ = x.ofLp a • SpherePacking.HarmonicCoordinateChannels.projectionMatrixFeature✝ f x

theorem SpherePacking.HarmonicCoordinateChannels.rawLiftChannel_inner {n k L : ℕ} (f : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (x y : Euclidean n) : inner ℝ (SpherePacking.HarmonicCoordinateChannels.rawLiftChannel✝ f x) (SpherePacking.HarmonicCoordinateChannels.rawLiftChannel✝ f y) = inner ℝ x y * SpherePacking.isometricPackingKernel✝ f x y

@[simp]

theorem SpherePacking.HarmonicCoordinateChannels.firstFibreVector_inner_basis (n k : ℕ) (hn : 3 ≤ n) (i : Fin (Gegenbauer.fibreDimension n k)) : inner ℝ (SpherePacking.HarmonicCoordinateChannels.firstFibreVector✝ n k hn) ((SpherePacking.certificateFibreBasis✝ n k) i) = if i = SpherePacking.HarmonicCoordinateChannels.firstFibreIndex✝ n k hn then 1 else 0

@[simp]

theorem SpherePacking.HarmonicCoordinateChannels.rankOneChannelMap_apply (n k L : ℕ) (hn : 3 ≤ n) (v : SpherePacking.HarmonicCoordinateChannels.ProjectionChannelSpace✝ n k L) (u : SpherePacking.CertificateFibre✝ n k) : (SpherePacking.HarmonicCoordinateChannels.rankOneChannelMap✝ n k L hn v) u = inner ℝ (SpherePacking.HarmonicCoordinateChannels.firstFibreVector✝ n k hn) u • v

theorem SpherePacking.HarmonicCoordinateChannels.rankOneChannelMap_kernel {α : Type u_1} (n k L : ℕ) (hn : 3 ≤ n) (v : α → SpherePacking.HarmonicCoordinateChannels.ProjectionChannelSpace✝ n k L) (x y : α) : SpherePacking.finiteHilbertSchmidtKernel✝ (SpherePacking.certificateFibreBasis✝ n k) (fun (z : α) => SpherePacking.HarmonicCoordinateChannels.rankOneChannelMap✝ n k L hn (v z)) x y = inner ℝ (v x) (v y)

theorem SpherePacking.HarmonicCoordinateChannels.embeddedBulkChannel_inner {n k L : ℕ} (embedding : SpherePacking.HarmonicCoordinateChannels.ProjectionMatrixSpace✝ n k L →ₗᵢ[ℝ] SpherePacking.HarmonicCoordinateChannels.ProjectionChannelSpace✝ n k L) (f : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (x y : Euclidean n) : inner ℝ (SpherePacking.HarmonicCoordinateChannels.embeddedBulkChannel✝ embedding f x) (SpherePacking.HarmonicCoordinateChannels.embeddedBulkChannel✝ embedding f y) = SpherePacking.isometricPackingKernel✝ f x y

structure SpherePacking.HarmonicCoordinateChannels.SourceSpectralRowData (n k L : ℕ) (fibre : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) : Type

Data encoding the source spectral row construction.

• row : SpherePacking.CertificateAmbient✝ n k L →ₗᵢ[ℝ] SpherePacking.HarmonicCoordinateChannels.HarmonicRowChannelSpace✝ n k L

  The row component.

• spectralCoefficient : ℝ

  The spectral coefficient component.

• spectralCoefficient_sq : self.spectralCoefficient ^ 2 = Jacobi.topEigenvalue n k L
• adjoint_axis_fibre (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ (u : SpherePacking.CertificateFibre✝ n k), (LinearMap.adjoint self.row.toLinearMap) ((harmonicAxisTensor n k L x) ((fibre x) u)) = self.spectralCoefficient • (fibre x) u

noncomputable def SpherePacking.HarmonicCoordinateChannels.sourceSpectralRowDataOfAdjacent {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (adjacent : SourceAdjacentChannelData n k L degreeFibre) : SourceSpectralRowData n k L (SpherePacking.HarmonicCertificateAssembly.harmonicWeightedFibre✝ n k L hn ⋯ degreeFibre)

The source spectral row data of adjacent used in the spherical-code argument.

Equations

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

theorem SpherePacking.HarmonicCoordinateChannels.sourceSpectralBulk_lift_inner {n k L : ℕ} (fibre : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (source : SourceSpectralRowData n k L fibre) (x y : Euclidean n) (hy : y ∈ SpherePacking.unitSphere✝ n) : inner ℝ (SpherePacking.HarmonicCoordinateChannels.embeddedBulkChannel✝ (SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbedding✝ n k L source.row) fibre x) (SpherePacking.HarmonicCoordinateChannels.rawLiftChannel✝ fibre y) = source.spectralCoefficient * SpherePacking.isometricPackingKernel✝ fibre x y

theorem SpherePacking.HarmonicCoordinateChannels.euclideanChannelFeatureMap_inner (n k L : ℕ) (hn : 3 ≤ n) (v w : SpherePacking.HarmonicCoordinateChannels.ProjectionChannelSpace✝ n k L) (u z : SpherePacking.CertificateFibre✝ n k) : inner ℝ ((SpherePacking.HarmonicCoordinateChannels.euclideanChannelFeatureMap✝ n k L hn v) u) ((SpherePacking.HarmonicCoordinateChannels.euclideanChannelFeatureMap✝ n k L hn w) z) = inner ℝ (SpherePacking.HarmonicCoordinateChannels.firstFibreVector✝ n k hn) u * (inner ℝ (SpherePacking.HarmonicCoordinateChannels.firstFibreVector✝ n k hn) z * inner ℝ v w)

theorem SpherePacking.HarmonicCoordinateChannels.euclideanChannelFeatureMap_kernel {α : Type u_1} (n k L : ℕ) (hn : 3 ≤ n) (v : α → SpherePacking.HarmonicCoordinateChannels.ProjectionChannelSpace✝ n k L) (x y : α) : SpherePacking.finiteHilbertSchmidtKernel✝ (SpherePacking.certificateFibreBasis✝ n k) (fun (z : α) => SpherePacking.HarmonicCoordinateChannels.euclideanChannelFeatureMap✝ n k L hn (v z)) x y = inner ℝ (v x) (v y)

theorem SpherePacking.HarmonicCoordinateChannels.bulkCoordinateMap_kernel {n k L : ℕ} (hn : 3 ≤ n) (embedding : SpherePacking.HarmonicCoordinateChannels.ProjectionMatrixSpace✝ n k L →ₗᵢ[ℝ] SpherePacking.HarmonicCoordinateChannels.ProjectionChannelSpace✝ n k L) (f : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (x y : Euclidean n) : SpherePacking.finiteHilbertSchmidtKernel✝ (SpherePacking.certificateFibreBasis✝ n k) (SpherePacking.HarmonicCoordinateChannels.bulkCoordinateMap✝ hn embedding f) x y = SpherePacking.isometricPackingKernel✝ f x y

theorem SpherePacking.HarmonicCoordinateChannels.liftCoordinateMap_kernel {n k L : ℕ} (hn : 3 ≤ n) (f : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (x y : Euclidean n) : SpherePacking.finiteHilbertSchmidtKernel✝ (SpherePacking.certificateFibreBasis✝ n k) (SpherePacking.HarmonicCoordinateChannels.liftCoordinateMap✝ hn f) x y = inner ℝ x y * SpherePacking.isometricPackingKernel✝ f x y

theorem SpherePacking.HarmonicCoordinateChannels.sourceSpectralBulk_lift_basis_inner {n k L : ℕ} (hn : 3 ≤ n) (fibre : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (source : SourceSpectralRowData n k L fibre) (x y : Euclidean n) (hy : y ∈ SpherePacking.unitSphere✝ n) (i : Fin (Gegenbauer.fibreDimension n k)) : inner ℝ ((SpherePacking.HarmonicCoordinateChannels.bulkCoordinateMap✝ hn (SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbedding✝ n k L source.row) fibre x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((SpherePacking.HarmonicCoordinateChannels.liftCoordinateMap✝ hn fibre y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = source.spectralCoefficient * inner ℝ ((SpherePacking.HarmonicCoordinateChannels.bulkCoordinateMap✝ hn (SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbedding✝ n k L source.row) fibre x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((SpherePacking.HarmonicCoordinateChannels.bulkCoordinateMap✝ hn (SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbedding✝ n k L source.row) fibre y) ((SpherePacking.certificateFibreBasis✝ n k) i))

structure SpherePacking.HarmonicCoordinateChannels.SpectralChannelRemainder (n k L : ℕ) (hn : 3 ≤ n) (fibre : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (embedding : SpherePacking.HarmonicCoordinateChannels.ProjectionMatrixSpace✝ n k L →ₗᵢ[ℝ] SpherePacking.HarmonicCoordinateChannels.ProjectionChannelSpace✝ n k L) : Type

Data encoding the spectral channel remainder construction.

• spectralCoefficient : ℝ

  The spectral coefficient component.

• spectralCoefficient_sq : self.spectralCoefficient ^ 2 = Jacobi.topEigenvalue n k L
• boundary : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗ[ℝ] Euclidean (SpherePacking.HarmonicCoordinateChannels.projectionChannelDimension✝ n k L)

  The boundary component.

• remainder : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗ[ℝ] Euclidean (SpherePacking.HarmonicCoordinateChannels.projectionChannelDimension✝ n k L)

  The remainder component.

• decomposition (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → SpherePacking.HarmonicCoordinateChannels.liftCoordinateMap✝ hn fibre x = self.spectralCoefficient • SpherePacking.HarmonicCoordinateChannels.bulkCoordinateMap✝ hn embedding fibre x + 1 • self.boundary x + self.remainder x
• bulk_boundary_orthogonal (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((SpherePacking.HarmonicCoordinateChannels.bulkCoordinateMap✝ hn embedding fibre x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((self.boundary y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = 0
• bulk_remainder_orthogonal (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((SpherePacking.HarmonicCoordinateChannels.bulkCoordinateMap✝ hn embedding fibre x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((self.remainder y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = 0
• boundary_remainder_orthogonal (x : Euclidean n) : x ∈ SpherePacking.unitSphere✝ n → ∀ y ∈ SpherePacking.unitSphere✝ n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.boundary x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((self.remainder y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = 0

theorem SpherePacking.HarmonicCoordinateChannels.sourceSpectralBulk_residual_orthogonal {n k L : ℕ} (hn : 3 ≤ n) (fibre : Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateAmbient✝ n k L) (source : SourceSpectralRowData n k L fibre) (x y : Euclidean n) (hy : y ∈ SpherePacking.unitSphere✝ n) (i : Fin (Gegenbauer.fibreDimension n k)) : inner ℝ ((SpherePacking.HarmonicCoordinateChannels.bulkCoordinateMap✝ hn (SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbedding✝ n k L source.row) fibre x) ((SpherePacking.certificateFibreBasis✝ n k) i)) ((SpherePacking.HarmonicCoordinateChannels.sourceSpectralResidual✝ hn fibre source y) ((SpherePacking.certificateFibreBasis✝ n k) i)) = 0

theorem SpherePacking.HarmonicCoordinateChannels.sphericalCode_bound_of_sourceSpectralRow {n k L : ℕ} (hn : 3 ≤ n) (hkl : k ≤ L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → SpherePacking.CertificateFibre✝ n k →ₗᵢ[ℝ] SpherePacking.CertificateDegreeAmbient✝ n k L i) (source : SourceSpectralRowData n k L (SpherePacking.HarmonicCertificateAssembly.harmonicWeightedFibre✝ n k L hn hkl degreeFibre)) {s : ℝ} (hs : s ≤ 1) (hgap : s < Jacobi.topEigenvalue n k L) (C : SphericalCode n s) : ↑C.points.card ≤ (1 - s) / (Jacobi.topEigenvalue n k L - s) * (↑(truncatedHarmonicDimension n k L) / ↑(Gegenbauer.fibreDimension n k))

@[simp]

theorem SpherePacking.HarmonicCoordinateOperators.axisPolynomial_coordinateAxis (n : ℕ) (j : Fin n) : axisPolynomial n (SpherePacking.HarmonicCoordinateOperators.coordinateAxis✝ n j) = MvPolynomial.X j

theorem SpherePacking.HarmonicCoordinateOperators.directionalDerivative_coordinateAxis (n : ℕ) (j : Fin n) (p : MvPolynomial (Fin n) ℝ) : (directionalDerivative n (SpherePacking.HarmonicCoordinateOperators.coordinateAxis✝ n j)) p = (MvPolynomial.pderiv j) p

@[simp]

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateDerivative_apply (n m : ℕ) (j : Fin n) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n (m + 1))) : ↑((SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateDerivative✝ n m j) p) = (MvPolynomial.pderiv j) ↑p

theorem SpherePacking.HarmonicCoordinateOperators.harmonicGradient_inner (n m : ℕ) (p q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n (m + 1))) : inner ℝ ((SpherePacking.HarmonicCoordinateOperators.harmonicGradient✝ n m) p) ((SpherePacking.HarmonicCoordinateOperators.harmonicGradient✝ n m) q) = ↑(m + 1) * inner ℝ p q

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising_eq_axisLift {n : ℕ} (hn : 0 < n) (k : ℕ) (j : Fin n) : SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising✝ n (k + 1) j = harmonicAxisLift hn k (SpherePacking.HarmonicCoordinateOperators.coordinateAxis✝ n j)

theorem SpherePacking.HarmonicCoordinateOperators.harmonicGradient_coGradient_orthogonal (n m : ℕ) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n (m + 2))) (q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) : inner ℝ ((SpherePacking.HarmonicCoordinateOperators.harmonicGradient✝ n (m + 1)) p) ((SpherePacking.HarmonicCoordinateOperators.harmonicCoGradient✝ n m) q) = 0

theorem SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator_pos {n : ℕ} (hn : 0 < n) (m : ℕ) : 0 < SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator✝ n m

theorem SpherePacking.HarmonicCoordinateOperators.upperChannelWeight_pos {n : ℕ} (hn : 0 < n) (m : ℕ) : 0 < SpherePacking.HarmonicCoordinateOperators.upperChannelWeight✝ n m

@[simp]

theorem SpherePacking.HarmonicCoordinateOperators.upperChannel_adjoint (n m : ℕ) : LinearMap.adjoint (SpherePacking.HarmonicCoordinateOperators.upperChannel✝ n m) = SpherePacking.HarmonicCoordinateOperators.upperChannelAdjoint✝ n m

theorem SpherePacking.HarmonicCoordinateOperators.upperChannelAdjoint_inner {n : ℕ} (hn : 0 < n) (m : ℕ) (p q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n (m + 1))) : inner ℝ ((SpherePacking.HarmonicCoordinateOperators.upperChannelAdjoint✝ n m) p) ((SpherePacking.HarmonicCoordinateOperators.upperChannelAdjoint✝ n m) q) = SpherePacking.HarmonicCoordinateOperators.upperChannelWeight✝ n m * inner ℝ p q

theorem SpherePacking.HarmonicCoordinateOperators.adjoint_comp_self_of_inner {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (A : E →ₗ[ℝ] F) (c : ℝ) (h : ∀ (p q : E), inner ℝ (A p) (A q) = c * inner ℝ p q) : LinearMap.adjoint A ∘ₗ A = c • LinearMap.id

noncomputable def SpherePacking.HarmonicCoordinateOperators.normalizedChannelIsometry {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (A : E →ₗ[ℝ] F) (c : ℝ) (hc : 0 < c) (h : ∀ (p q : E), inner ℝ (A p) (A q) = c * inner ℝ p q) : E →ₗᵢ[ℝ] F

The normalized channel isometry used in the spherical-code argument.

Equations

• SpherePacking.HarmonicCoordinateOperators.normalizedChannelIsometry A c hc h = ((√c)⁻¹ • A).isometryOfInner ⋯

theorem SpherePacking.HarmonicCoordinateOperators.lowerChannelWeight_pos {n : ℕ} (hn : 3 ≤ n) (m : ℕ) : 0 < SpherePacking.HarmonicCoordinateOperators.lowerChannelWeight✝ n m

@[simp]

theorem SpherePacking.HarmonicCoordinateOperators.lowerChannel_adjoint (n m : ℕ) : LinearMap.adjoint (SpherePacking.HarmonicCoordinateOperators.lowerChannel✝ n m) = SpherePacking.HarmonicCoordinateOperators.lowerChannelAdjoint✝ n m

theorem SpherePacking.HarmonicCoordinateOperators.upperChannelAdjoint_lowerChannelAdjoint_orthogonal (n m : ℕ) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n (m + 2))) (q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) : inner ℝ ((SpherePacking.HarmonicCoordinateOperators.upperChannelAdjoint✝ n (m + 1)) p) ((SpherePacking.HarmonicCoordinateOperators.lowerChannelAdjoint✝ n m) q) = 0

theorem SpherePacking.HarmonicCoordinateOperators.coordinatePolynomialMultiplication_derivative_sum (n : ℕ) (p : MvPolynomial (Fin n) ℝ) : ∑ j : Fin n, (MvPolynomial.pderiv j) (MvPolynomial.X j * p) = ↑n • p + ∑ j : Fin n, MvPolynomial.X j * (MvPolynomial.pderiv j) p

theorem SpherePacking.HarmonicCoordinateOperators.radialGradient_derivative_sum (n : ℕ) (p : MvPolynomial (Fin n) ℝ) : ∑ j : Fin n, (MvPolynomial.pderiv j) (radialPolynomial n * (MvPolynomial.pderiv j) p) = 2 * ∑ j : Fin n, MvPolynomial.X j * (MvPolynomial.pderiv j) p + radialPolynomial n * (polynomialLaplacian n) p

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateMultiplication_derivative_sum (n m : ℕ) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) : ∑ j : Fin n, (MvPolynomial.pderiv j) (MvPolynomial.X j * ↑p) = ↑(n + m) • ↑p

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising_zero_eq (n : ℕ) (j : Fin n) : SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising✝ n 0 j = SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaisingZero✝ n j

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising_apply_polynomial {n : ℕ} (hn : 0 < n) (m : ℕ) (j : Fin n) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) : ↑((SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising✝ n m j) p) = MvPolynomial.X j * ↑p - (SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator✝ n (m - 1))⁻¹ • (radialPolynomial n * (MvPolynomial.pderiv j) ↑p)

theorem SpherePacking.HarmonicCoordinateOperators.lowerFischerGradientWeight_eq {n : ℕ} (hn : 3 ≤ n) (m : ℕ) : SpherePacking.HarmonicCoordinateOperators.lowerFischerGradientWeight✝ n m = SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator✝ n m * SpherePacking.HarmonicCoordinateOperators.lowerChannelWeight✝ n m

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising_derivative_sum {n : ℕ} (hn : 3 ≤ n) (m : ℕ) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) : ∑ j : Fin n, (MvPolynomial.pderiv j) ↑((SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising✝ n m j) p) = SpherePacking.HarmonicCoordinateOperators.lowerFischerGradientWeight✝ n m • ↑p

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoGradient_inner {n : ℕ} (hn : 3 ≤ n) (m : ℕ) (p q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) : inner ℝ ((SpherePacking.HarmonicCoordinateOperators.harmonicCoGradient✝ n m) p) ((SpherePacking.HarmonicCoordinateOperators.harmonicCoGradient✝ n m) q) = SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator✝ n m * SpherePacking.HarmonicCoordinateOperators.lowerChannelWeight✝ n m * inner ℝ p q

theorem SpherePacking.HarmonicCoordinateOperators.lowerChannelAdjoint_inner {n : ℕ} (hn : 3 ≤ n) (m : ℕ) (p q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) : inner ℝ ((SpherePacking.HarmonicCoordinateOperators.lowerChannelAdjoint✝ n m) p) ((SpherePacking.HarmonicCoordinateOperators.lowerChannelAdjoint✝ n m) q) = SpherePacking.HarmonicCoordinateOperators.lowerChannelWeight✝ n m * inner ℝ p q

theorem SpherePacking.HarmonicCoordinateOperators.upperChannelIsometry_lowerChannelIsometry_orthogonal {n : ℕ} (hn : 3 ≤ n) (m : ℕ) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n (m + 2))) (q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) : inner ℝ ((SpherePacking.HarmonicCoordinateOperators.upperChannelIsometry✝ ⋯ (m + 1)) p) ((SpherePacking.HarmonicCoordinateOperators.lowerChannelIsometry✝ hn m) q) = 0

noncomputable def SpherePacking.HarmonicSourceProjection.harmonicAxisTensor (n m : ℕ) (x : Euclidean n) : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m) →ₗ[ℝ] SpherePacking.HarmonicCoordinateOperators.CoordinateHarmonicSpace✝ n m

The harmonic axis tensor used in the spherical-code argument.

Equations

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

theorem SpherePacking.HarmonicSourceProjection.upperChannel_harmonicAxisTensor_inner (n m : ℕ) (x : Euclidean n) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) (q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n (m + 1))) : inner ℝ ((SpherePacking.HarmonicCoordinateOperators.upperChannel✝ n m) ((harmonicAxisTensor n m x) p)) q = (√(SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator✝ n m))⁻¹ * Fischer.polynomialInner n (axisPolynomial n x * ↑p) ↑q

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicAxisLift_axis_pairing {n k : ℕ} (x : Euclidean n) (p : ↥(tangentHarmonicSubmodule n k x)) (r : ℕ) (q : ↥(harmonicHomogeneousSubmodule n (k + r + 1))) : (2 * ↑r + harmonicAxisParameter n k - 2) * Fischer.polynomialInner n (axisPolynomial n x * (solidHarmonicAxisLift n k x r) ↑p) ↑q = Fischer.polynomialInner n ((solidHarmonicAxisLift n k x (r + 1)) ↑p) ↑q

theorem SpherePacking.HarmonicSourceProjection.upperChannel_solidHarmonicSource {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) (p : ↥(tangentHarmonicSubmodule n k x)) : (SpherePacking.HarmonicCoordinateOperators.upperChannel✝ n (k + r)) ((SpherePacking.HarmonicSourceProjection.solidHarmonicSource✝ hn k r x hx) p) = SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperCoefficient✝ n k r • (solidHarmonicAxisPolynomialIsometry hn k (r + 1) x hx) p

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperCoefficient_pos {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : 0 < SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperCoefficient✝ n k r

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperCoefficient_sq {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperCoefficient✝ n k r ^ 2 = (↑r + 1) * (↑r + harmonicAxisParameter n k - 2) / ((2 * ↑r + harmonicAxisParameter n k - 2) * SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator✝ n (k + r))

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperIsometryCoefficient_sq {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperIsometryCoefficient✝ n k r ^ 2 = Gegenbauer.alphaSq n k (k + r)

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperIsometryCoefficient_pos {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : 0 < SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperIsometryCoefficient✝ n k r

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperIsometryCoefficient_eq_sqrt {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperIsometryCoefficient✝ n k r = √(Gegenbauer.alphaSq n k (k + r))

theorem SpherePacking.HarmonicSourceProjection.harmonic_inner_smul_right (n m : ℕ) (p q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) (c : ℝ) : inner ℝ p (c • q) = c * inner ℝ p q

theorem SpherePacking.HarmonicSourceProjection.harmonic_inner_smul_left (n m : ℕ) (p q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) (c : ℝ) : inner ℝ (c • p) q = c * inner ℝ p q

theorem SpherePacking.HarmonicSourceProjection.upperChannelIsometry_adjoint_solidHarmonicSource {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) (p : ↥(tangentHarmonicSubmodule n k x)) : (LinearMap.adjoint (SpherePacking.HarmonicCoordinateOperators.upperChannelIsometry✝ ⋯ (k + r)).toLinearMap) ((SpherePacking.HarmonicSourceProjection.solidHarmonicSource✝ hn k r x hx) p) = √(Gegenbauer.alphaSq n k (k + r)) • (solidHarmonicAxisPolynomialIsometry hn k (r + 1) x hx) p

theorem SpherePacking.HarmonicSourceProjection.lowerChannel_harmonicAxisTensor_inner (n m : ℕ) (x : Euclidean n) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n (m + 1))) (q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n m)) : inner ℝ ((SpherePacking.HarmonicCoordinateOperators.lowerChannel✝ n m) ((harmonicAxisTensor n (m + 1) x) p)) q = (√(SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator✝ n m))⁻¹ * Fischer.polynomialInner n ((directionalDerivative n x) ↑p) ↑q

theorem SpherePacking.HarmonicSourceProjection.lowerChannel_solidHarmonicSource {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) (p : ↥(tangentHarmonicSubmodule n k x)) : (SpherePacking.HarmonicCoordinateOperators.lowerChannel✝ n (k + r)) ((SpherePacking.HarmonicSourceProjection.solidHarmonicSource✝ hn k (r + 1) x hx) p) = SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerCoefficient✝ n k r • (solidHarmonicAxisPolynomialIsometry hn k r x hx) p

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerCoefficient_pos {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : 0 < SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerCoefficient✝ n k r

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerCoefficient_sq {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerCoefficient✝ n k r ^ 2 = (↑r + 1) * (↑r + harmonicAxisParameter n k - 2) / ((2 * ↑r + harmonicAxisParameter n k - 2) * SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator✝ n (k + r))

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerIsometryCoefficient_sq {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerIsometryCoefficient✝ n k r ^ 2 = Gegenbauer.betaSq n k (k + (r + 1))

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerIsometryCoefficient_pos {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : 0 < SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerIsometryCoefficient✝ n k r

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerIsometryCoefficient_eq_sqrt {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) : SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerIsometryCoefficient✝ n k r = √(Gegenbauer.betaSq n k (k + (r + 1)))

theorem SpherePacking.HarmonicSourceProjection.lowerChannelIsometry_adjoint_solidHarmonicSource {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) (p : ↥(tangentHarmonicSubmodule n k x)) : (LinearMap.adjoint (SpherePacking.HarmonicCoordinateOperators.lowerChannelIsometry✝ hn (k + r)).toLinearMap) ((SpherePacking.HarmonicSourceProjection.solidHarmonicSource✝ hn k (r + 1) x hx) p) = √(Gegenbauer.betaSq n k (k + (r + 1))) • (solidHarmonicAxisPolynomialIsometry hn k r x hx) p

theorem SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCastLinearMap_inner (n r s : ℕ) (h : r = s) (p q : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n r)) : inner ℝ ((SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCastLinearMap✝ n r s h) p) ((SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCastLinearMap✝ n r s h) q) = inner ℝ p q

@[simp]

theorem SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCast_adjoint_apply (n r s : ℕ) (h : r = s) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n s)) : (LinearMap.adjoint (SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCast✝ n r s h).toLinearMap) p = (SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCast✝ n s r ⋯) p

theorem SpherePacking.HarmonicAdjacentChannelTransport.transportedIsometry_adjoint {E : Type u_1} {F : Type u_2} {G : Type u_3} {B : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [NormedAddCommGroup B] [InnerProductSpace ℝ B] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [FiniteDimensional ℝ G] [FiniteDimensional ℝ B] (T : F →ₗᵢ[ℝ] G) (A : E →ₗᵢ[ℝ] F) (e : E ≃ₗᵢ[ℝ] B) (z : F) : (LinearMap.adjoint (T.comp (A.comp e.symm.toLinearIsometry)).toLinearMap) (T z) = e ((LinearMap.adjoint A.toLinearMap) z)

theorem SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCastLinearMap_inner (n r s : ℕ) (h : r = s) (z w : SpherePacking.HarmonicCoordinateOperators.CoordinateHarmonicSpace✝ n r) : inner ℝ ((SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCastLinearMap✝ n r s h) z) ((SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCastLinearMap✝ n r s h) w) = inner ℝ z w

@[simp]

theorem SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCast_adjoint_apply (n r s : ℕ) (h : r = s) (z : SpherePacking.HarmonicCoordinateOperators.CoordinateHarmonicSpace✝ n s) : (LinearMap.adjoint (SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCast✝ n r s h).toLinearMap) z = (SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCast✝ n s r ⋯) z

theorem SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCast_axis (n r s : ℕ) (h : r = s) (x : Euclidean n) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n r)) : (SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCast✝ n r s h) ((HarmonicSourceProjection.harmonicAxisTensor n r x) p) = (HarmonicSourceProjection.harmonicAxisTensor n s x) ((SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCast✝ n r s h) p)

theorem SpherePacking.HarmonicAdjacentChannelTransport.coordinateDegreeTransportLinearMap_inner {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (i : Jacobi.Index k L) (z w : SpherePacking.HarmonicCoordinateOperators.CoordinateHarmonicSpace✝ n (k + ↑i)) : inner ℝ ((SpherePacking.HarmonicAdjacentChannelTransport.coordinateDegreeTransportLinearMap✝ hn k L i) z) ((SpherePacking.HarmonicAdjacentChannelTransport.coordinateDegreeTransportLinearMap✝ hn k L i) w) = inner ℝ z w

theorem SpherePacking.HarmonicAdjacentChannelTransport.coordinateDegreeTransport_axis {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (i : Jacobi.Index k L) (x : Euclidean n) (p : ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace✝ n (k + ↑i))) : (SpherePacking.HarmonicAdjacentChannelTransport.coordinateDegreeTransport✝ hn k L i) ((HarmonicSourceProjection.harmonicAxisTensor n (k + ↑i) x) p) = (SpherePacking.HarmonicCoordinateChannels.harmonicDegreeAxisTensor✝ n k L i x) ((SpherePacking.HarmonicCertificateAssembly.harmonicDegreeEuclideanEquiv✝ n k L ⋯ i) p)

theorem SpherePacking.HarmonicAdjacentChannelTransport.upperAdjacentChannel_lowerAdjacentChannel_orthogonal {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (target high low : Jacobi.Index k L) (hhigh : ↑target + 1 = ↑high) (hlow : ↑low + 1 = ↑target) (p : SpherePacking.CertificateDegreeAmbient✝ n k L high) (q : SpherePacking.CertificateDegreeAmbient✝ n k L low) : inner ℝ ((SpherePacking.HarmonicAdjacentChannelTransport.upperAdjacentChannel✝ hn k L target high hhigh) p) ((SpherePacking.HarmonicAdjacentChannelTransport.lowerAdjacentChannel✝ hn k L target low hlow) q) = 0

theorem SpherePacking.HarmonicAdjacentChannelTransport.lowerAdjacentChannel_upperAdjacentChannel_orthogonal {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (target low high : Jacobi.Index k L) (hlow : ↑low + 1 = ↑target) (hhigh : ↑target + 1 = ↑high) (p : SpherePacking.CertificateDegreeAmbient✝ n k L low) (q : SpherePacking.CertificateDegreeAmbient✝ n k L high) : inner ℝ ((SpherePacking.HarmonicAdjacentChannelTransport.lowerAdjacentChannel✝ hn k L target low hlow) p) ((SpherePacking.HarmonicAdjacentChannelTransport.upperAdjacentChannel✝ hn k L target high hhigh) q) = 0

theorem SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel_inner {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (target source : Jacobi.Index k L) (hsource : SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L source target ≠ 0) (u v : SpherePacking.CertificateDegreeAmbient✝ n k L source) : inner ℝ ((SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel✝ hn k L target source) u) ((SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel✝ hn k L target source) v) = inner ℝ u v

theorem SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel_zero {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (target source : Jacobi.Index k L) (hzero : SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L source target = 0) : SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel✝ hn k L target source = 0

theorem SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel_orthogonal {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (target source₁ source₂ : Jacobi.Index k L) (hne : source₁ ≠ source₂) (u : SpherePacking.CertificateDegreeAmbient✝ n k L source₁) (v : SpherePacking.CertificateDegreeAmbient✝ n k L source₂) : inner ℝ ((SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel✝ hn k L target source₁) u) ((SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel✝ hn k L target source₂) v) = 0

theorem SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeFibre_apply_eq {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (i : Jacobi.Index k L) (x : Euclidean n) (hx : ‖x‖ = 1) (u : SpherePacking.CertificateFibre✝ n k) : (harmonicDegreeFibre hn k L i x) u = (SpherePacking.HarmonicCertificateAssembly.harmonicDegreeEuclideanEquiv✝ n k L ⋯ i) ((solidHarmonicAxisPolynomialIsometry hn k (↑i) x hx) (SpherePacking.HarmonicAdjacentChannelTransport.sourceTangentPolynomial✝ hn k x hx u))

theorem SpherePacking.HarmonicAdjacentChannelTransport.upperAdjacentChannel_axis_projection {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (target source : Jacobi.Index k L) (h : ↑target + 1 = ↑source) (x : Euclidean n) (hx : ‖x‖ = 1) (u : SpherePacking.CertificateFibre✝ n k) : (LinearMap.adjoint (SpherePacking.HarmonicAdjacentChannelTransport.upperAdjacentChannel✝ hn k L target source h).toLinearMap) ((SpherePacking.HarmonicCoordinateChannels.harmonicDegreeAxisTensor✝ n k L target x) ((harmonicDegreeFibre hn k L target x) u)) = √(Gegenbauer.alphaSq n k (k + ↑target)) • (harmonicDegreeFibre hn k L source x) u

theorem SpherePacking.HarmonicAdjacentChannelTransport.lowerAdjacentChannel_axis_projection {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (target source : Jacobi.Index k L) (h : ↑source + 1 = ↑target) (x : Euclidean n) (hx : ‖x‖ = 1) (u : SpherePacking.CertificateFibre✝ n k) : (LinearMap.adjoint (SpherePacking.HarmonicAdjacentChannelTransport.lowerAdjacentChannel✝ hn k L target source h).toLinearMap) ((SpherePacking.HarmonicCoordinateChannels.harmonicDegreeAxisTensor✝ n k L target x) ((harmonicDegreeFibre hn k L target x) u)) = √(Gegenbauer.betaSq n k (k + ↑target)) • (harmonicDegreeFibre hn k L source x) u

theorem SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel_axis_projection {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (x : Euclidean n) (hx : x ∈ SpherePacking.unitSphere✝ n) (target source : Jacobi.Index k L) (u : SpherePacking.CertificateFibre✝ n k) : (LinearMap.adjoint (SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel✝ hn k L target source)) ((SpherePacking.HarmonicCoordinateChannels.harmonicDegreeAxisTensor✝ n k L target x) ((harmonicDegreeFibre hn k L target x) u)) = √(SpherePacking.SourceJacobiWeights.sourceChannelCoefficient✝ n k L source target) • (harmonicDegreeFibre hn k L source x) u

noncomputable def SpherePacking.HarmonicAdjacentChannelTransport.actualSourceAdjacentChannelData {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) : HarmonicCoordinateChannels.SourceAdjacentChannelData n k L (harmonicDegreeFibre hn k L)

The actual source adjacent channel data used in the spherical-code argument.

Equations

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