Documentation

def SpherePacking.PositiveDefiniteKernel {α : Type u_1} (K : α → α → ℝ) :

Prop

Nonnegativity of every finite weighted quadratic form of the kernel.

Equations

SpherePacking.PositiveDefiniteKernel K = ∀ (C : Finset α) (w : α → ℝ), 0 ≤ ∑ x ∈ C, ∑ y ∈ C, w x * w y * K x y

Instances For

def SpherePacking.unitSphere (n : ℕ) :

Set (Euclidean n)

The unit sphere in the Euclidean space of dimension n.

Equations

SpherePacking.unitSphere n = {x : SpherePacking.Euclidean n | ‖x‖ = 1}

Instances For

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) :

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, PositiveDefiniteKernel (K i)) :

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)

Instances For

@[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 : ℕ) :

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

Equations

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

Instances For

@[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

noncomputable def SpherePacking.finiteHilbertSchmidtKernel {α : 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) (x y : α) :

The Hilbert–Schmidt Gram kernel of a family of linear maps, computed in the basis b.

Equations

SpherePacking.finiteHilbertSchmidtKernel b A x y = ∑ i : ι, inner ℝ ((A x) (b i)) ((A y) (b i))

Instances For

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) :

PositiveDefiniteKernel (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 : α) :

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 : α) :

finiteHilbertSchmidtKernel basis (fun (z : α) => a • P z + b • M z + R z) x y = a ^ 2 * finiteHilbertSchmidtKernel basis P x y + b ^ 2 * finiteHilbertSchmidtKernel basis M x y + finiteHilbertSchmidtKernel basis R x y

noncomputable def SpherePacking.mixedHilbertSchmidtKernel {α : Type u_1} {ι : Type u_2} {F : Type u_3} {E : Type u_4} {G : Type u_5} [Fintype ι] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] [FiniteDimensional ℝ F] [FiniteDimensional ℝ G] (basis : OrthonormalBasis ι ℝ G) (A : α → F →ₗ[ℝ ] E) (B : α → F →ₗ[ℝ ] G) :

α → α → ℝ

The Hilbert–Schmidt kernel of the compositions A x ∘ (B x).adjoint.

Equations

SpherePacking.mixedHilbertSchmidtKernel basis A B = SpherePacking.finiteHilbertSchmidtKernel basis fun (x : α) => A x ∘ₗ LinearMap.adjoint (B x)

Instances For

def SpherePacking.Gegenbauer.recurrenceDenominator (n i : ℕ) :

The common denominator i + n - 2 in the normalized Gegenbauer recurrence.

Equations

SpherePacking.Gegenbauer.recurrenceDenominator n i = ↑i + ↑n - 2

Instances For

noncomputable def SpherePacking.Gegenbauer.forwardCoefficient (n i : ℕ) :

The coefficient of X * normalized n i in the Gegenbauer recurrence.

Equations

SpherePacking.Gegenbauer.forwardCoefficient n i = (2 * ↑i + ↑n - 2) / SpherePacking.Gegenbauer.recurrenceDenominator n i

Instances For

noncomputable def SpherePacking.Gegenbauer.backwardCoefficient (n i : ℕ) :

The coefficient of the preceding polynomial in the Gegenbauer recurrence.

Equations

SpherePacking.Gegenbauer.backwardCoefficient n i = ↑i / SpherePacking.Gegenbauer.recurrenceDenominator n i

Instances For

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

Instances For

@[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 (forwardCoefficient n (i + 1)) * Polynomial.X * normalized n (i + 1) - Polynomial.C (backwardCoefficient n (i + 1)) * normalized n i

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

0 < recurrenceDenominator n i

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

0 < forwardCoefficient n i

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

0 < 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

Instances For

@[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

Instances For

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

Instances For

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))

Instances For

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))

Instances For

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))

Instances For

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

noncomputable def SpherePacking.Gegenbauer.jacobiMatrix (n k L : ℕ) :

Matrix (Fin (L - k + 1)) (Fin (L - k + 1)) ℝ

The symmetric tridiagonal matrix with Gegenbauer Jacobi coefficients between adjacent degrees.

Equations

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

Instances For

theorem SpherePacking.Gegenbauer.jacobiMatrix_symmetric (n k L : ℕ) :

(jacobiMatrix n k L).transpose = 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 < 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)

Instances For

@[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

noncomputable def SpherePacking.directionalDerivation (n : ℕ) (x : Euclidean n) :

Derivation ℝ (MvPolynomial (Fin n) ℝ) (MvPolynomial (Fin n) ℝ)

Directional differentiation of multivariate polynomials, bundled as a derivation.

Equations

SpherePacking.directionalDerivation n x = ∑ i : Fin n, x.ofLp i • MvPolynomial.pderiv i

Instances For

@[simp]

theorem SpherePacking.directionalDerivation_apply (n : ℕ) (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) :

(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

Instances For

@[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 ⋯

Instances For

noncomputable def SpherePacking.tangentHarmonicSubmodule (n k : ℕ) (x : Euclidean 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

Instances For

@[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 : ℕ) :

The multi index used in the spherical-code argument.

Equations

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

Instances For

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

Instances For

@[reducible, inline]

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

The degree index used in the spherical-code argument.

Equations

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

Instances For

@[reducible, inline]

abbrev SpherePacking.Fischer.Homogeneous (n m : ℕ) :

The homogeneous used in the spherical-code argument.

Equations

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

Instances For

@[reducible, inline]

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

The coefficient space used in the spherical-code argument.

Equations

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

Instances For

@[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

Instances For

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.pderiv i) p).coeff a = ↑(a i + 1) * p.coeff (a + Finsupp.single i 1)

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 * q.coeff a

Instances For

@[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 * q.coeff a

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.

Instances For

@[simp]

theorem SpherePacking.Fischer.coefficientEmbedding_apply (n m : ℕ) (p : ↥(Homogeneous n m)) (a : DegreeIndex n m) :

((coefficientEmbedding n m) p).ofLp a = √(multiFactorial ↑a) * (↑p).coeff ↑a

theorem SpherePacking.Fischer.coefficientEmbedding_injective (n m : ℕ) :

Function.Injective ⇑(coefficientEmbedding n m)

noncomputable def SpherePacking.Fischer.harmonicCoefficientEmbedding (n m : ℕ) :

↥(harmonicHomogeneousSubmodule n m) →ₗ[ℝ ] CoefficientSpace n m

The coefficient embedding restricted to homogeneous harmonic polynomials.

Equations

SpherePacking.Fischer.harmonicCoefficientEmbedding n m = SpherePacking.Fischer.coefficientEmbedding n m ∘ₗ Submodule.inclusion ⋯

Instances For

theorem SpherePacking.Fischer.harmonicCoefficientEmbedding_injective (n m : ℕ) :

Function.Injective ⇑(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)

Instances For

theorem SpherePacking.Fischer.homogeneousInner_eq_sum (n m : ℕ) (p q : ↥(Homogeneous n m)) :

homogeneousInner n m p q = ∑ a : DegreeIndex n m, multiFactorial ↑a * (↑p).coeff ↑a * (↑q).coeff ↑a

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.

Instances For

@[simp]

theorem SpherePacking.Fischer.harmonicCoefficientEmbedding_apply (n m : ℕ) (p : ↥(harmonicHomogeneousSubmodule n m)) (a : DegreeIndex n m) :

((harmonicCoefficientEmbedding n m) p).ofLp a = √(multiFactorial ↑a) * (↑p).coeff ↑a

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)

Instances For

theorem SpherePacking.Fischer.harmonicInner_eq_sum (n m : ℕ) (p q : ↥(harmonicHomogeneousSubmodule n m)) :

harmonicInner n m p q = ∑ a : DegreeIndex n m, multiFactorial ↑a * (↑p).coeff ↑a * (↑q).coeff ↑a

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 := ⋯ }

Instances For

@[implicit_reducible]

noncomputable def SpherePacking.Fischer.harmonicInnerCore (n m : ℕ) :

InnerProductSpace.Core ℝ ↥(harmonicHomogeneousSubmodule n m)

The Fischer inner product core on harmonic polynomials, pulled back from coefficient space.

Equations

SpherePacking.Fischer.harmonicInnerCore n m = SpherePacking.Fischer.embeddingInnerCore (SpherePacking.Fischer.harmonicCoefficientEmbedding n m) ⋯

Instances For

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

tangentHarmonicSubmodule n m x ≤ harmonicHomogeneousSubmodule n m

noncomputable def SpherePacking.Fischer.tangentCoefficientEmbedding (n m : ℕ) (x : Euclidean n) :

↥(tangentHarmonicSubmodule n m x) →ₗ[ℝ ] CoefficientSpace n m

The coefficient embedding restricted further to the tangent harmonic subspace at x.

Equations

SpherePacking.Fischer.tangentCoefficientEmbedding n m x = SpherePacking.Fischer.harmonicCoefficientEmbedding n m ∘ₗ Submodule.inclusion ⋯

Instances For

theorem SpherePacking.Fischer.tangentCoefficientEmbedding_injective (n m : ℕ) (x : Euclidean n) :

Function.Injective ⇑(tangentCoefficientEmbedding n m x)

theorem SpherePacking.Fischer.tangent_finiteDimensional (n m : ℕ) (x : Euclidean n) :

FiniteDimensional ℝ ↥(tangentHarmonicSubmodule n m x)

noncomputable def SpherePacking.Fischer.tangentInner (n m : ℕ) (x : Euclidean n) (p q : ↥(tangentHarmonicSubmodule n m x)) :

The inner product on tangent harmonics induced by their coefficient embedding.

Equations

SpherePacking.Fischer.tangentInner n m x p q = inner ℝ ((SpherePacking.Fischer.tangentCoefficientEmbedding n m x) p) ((SpherePacking.Fischer.tangentCoefficientEmbedding n m x) q)

Instances For

theorem SpherePacking.Fischer.tangentInner_eq_polynomialInner (n m : ℕ) (x : Euclidean n) (p q : ↥(tangentHarmonicSubmodule n m x)) :

tangentInner n m x p q = polynomialInner n ↑p ↑q

@[implicit_reducible]

noncomputable def SpherePacking.Fischer.tangentInnerCore (n m : ℕ) (x : Euclidean n) :

InnerProductSpace.Core ℝ ↥(tangentHarmonicSubmodule n m x)

The inner product core induced by the injective tangent coefficient embedding.

Equations

SpherePacking.Fischer.tangentInnerCore n m x = SpherePacking.Fischer.embeddingInnerCore (SpherePacking.Fischer.tangentCoefficientEmbedding n m x) ⋯

Instances For

@[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 = 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

Instances For

@[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)

def SpherePacking.homogeneousExponentFinset (n m : ℕ) :

Finset (Fin n →₀ ℕ)

The finite set of exponent vectors of total degree m in n variables.

Equations

SpherePacking.homogeneousExponentFinset n m = Finset.univ.finsuppAntidiag m

Instances For

@[simp]

theorem SpherePacking.homogeneousExponentFinset_card (n m : ℕ) :

(homogeneousExponentFinset n m).card = (n + m - 1).choose m

@[simp]

theorem SpherePacking.mem_homogeneousExponentFinset {n m : ℕ} (d : Fin n →₀ ℕ) :

d ∈ homogeneousExponentFinset n m ↔ Finsupp.degree d = m

theorem SpherePacking.homogeneousSubmodule_eq_supported_exponents (n m : ℕ) :

MvPolynomial.homogeneousSubmodule (Fin n) ℝ m = AddMonoidAlgebra.supported ℝ ℝ ↑(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

noncomputable def SpherePacking.homogeneousRadialMultiplication (n m : ℕ) :

↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ m) →ₗ[ℝ ] ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ (m + 2))

Multiplication by the radial polynomial, from homogeneous degree m to degree m + 2.

Equations

SpherePacking.homogeneousRadialMultiplication n m = (LinearMap.mulLeft ℝ (SpherePacking.radialPolynomial n)).restrict ⋯

Instances For

@[simp]

theorem SpherePacking.homogeneousRadialMultiplication_apply (n m : ℕ) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ m)) :

↑((homogeneousRadialMultiplication n m) p) = radialPolynomial n * ↑p

theorem SpherePacking.homogeneousRadialMultiplication_injective {n : ℕ} (hn : 0 < n) (m : ℕ) :

Function.Injective ⇑(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

noncomputable def SpherePacking.homogeneousLaplacian (n m : ℕ) :

↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ (m + 2)) →ₗ[ℝ ] ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ m)

The polynomial Laplacian restricted from homogeneous degree m + 2 to degree m.

Equations

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

Instances For

@[simp]

theorem SpherePacking.homogeneousLaplacian_apply (n m : ℕ) (p : ↥(MvPolynomial.homogeneousSubmodule (Fin n) ℝ (m + 2))) :

↑((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) ((homogeneousRadialMultiplication n m) p) q = Fischer.homogeneousInner n m p ((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 ((homogeneousLaplacian n m) q) p = Fischer.homogeneousInner n (m + 2) q ((homogeneousRadialMultiplication n m) p)) :

Function.Surjective ⇑(homogeneousLaplacian n m)

theorem SpherePacking.homogeneousLaplacian_surjective {n : ℕ} (hn : 0 < n) (m : ℕ) :

Function.Surjective ⇑(homogeneousLaplacian n m)

theorem SpherePacking.homogeneousLaplacian_ker (n m : ℕ) :

(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 (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 ⇑(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

Instances For

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)

Instances For

@[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

def SpherePacking.harmonicAxisProjectionDenominator (n k : ℕ) :

The denominator 2 * k + n used to remove the radial part of an axis projection.

Equations

SpherePacking.harmonicAxisProjectionDenominator n k = 2 * ↑k + ↑n

Instances For

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

0 < 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.

Instances For

@[simp]

theorem SpherePacking.harmonicAxisProjectionOperator_apply (n k : ℕ) (x : Euclidean n) (p : MvPolynomial (Fin n) ℝ) :

(harmonicAxisProjectionOperator n k x) p = axisPolynomial n x * p - (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 ⋯

Instances For

@[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 * (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 * (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) :

finiteHilbertSchmidtKernel b (fun (x : Unit) => ∑ x ∈ C, A x) () () = ∑ x ∈ C, ∑ y ∈ C, 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 ι) * 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, 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, 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

Instances For

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)))

Instances For

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))

Instances For

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

Instances For

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)

noncomputable def SpherePacking.harmonicEntropyBase (u : ℝ) (N : ℕ → ℕ) (n : ℕ) :

The binomial coefficient bounding harmonic dimensions in the entropy estimate.

Equations

SpherePacking.harmonicEntropyBase u N n = (⌊u * ↑n⌋₊ + (N n - 2)).choose ⌊u * ↑n⌋₊

Instances For

theorem SpherePacking.harmonicEntropyBase_pos (u : ℝ) (N : ℕ → ℕ) (n : ℕ) :

0 < 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 ↑(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 * 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⌋₊)

Instances For

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

Instances For

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⌋₊)

Instances For

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 : ℕ) :

The index used in the spherical-code argument.

Equations

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

Instances For

@[reducible, inline]

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

The space used in the spherical-code argument.

Equations

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

Instances For

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

Instances For

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)

Instances For

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)

Instances For

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

Instances For

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

Instances For

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) :

The coordinate abs used in the spherical-code argument.

Equations

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

Instances For

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))

Instances For

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

Instances For

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 : ℕ) :

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

Instances For

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

@[reducible, inline]

abbrev SpherePacking.CertificateFibre (n k : ℕ) :

The Euclidean model of the certificate fibre of dimension Gegenbauer.fibreDimension n k.

Equations

SpherePacking.CertificateFibre n k = SpherePacking.Euclidean (SpherePacking.Gegenbauer.fibreDimension n k)

Instances For

@[reducible, inline]

abbrev SpherePacking.CertificateAmbient (n k L : ℕ) :

The Euclidean ambient space for the certificate truncated to degrees k through L.

Equations

SpherePacking.CertificateAmbient n k L = SpherePacking.Euclidean (SpherePacking.truncatedHarmonicDimension n k L)

Instances For

noncomputable def SpherePacking.certificateFibreBasis (n k : ℕ) :

OrthonormalBasis (Fin (Gegenbauer.fibreDimension n k)) ℝ (CertificateFibre n k)

The standard orthonormal coordinate basis of the certificate fibre.

Equations

SpherePacking.certificateFibreBasis n k = EuclideanSpace.basisFun (Fin (SpherePacking.Gegenbauer.fibreDimension n k)) ℝ

Instances For

noncomputable def SpherePacking.certificateAmbientBasis (n k L : ℕ) :

OrthonormalBasis (Fin (truncatedHarmonicDimension n k L)) ℝ (CertificateAmbient n k L)

The standard orthonormal coordinate basis of the truncated certificate ambient space.

Equations

SpherePacking.certificateAmbientBasis n k L = EuclideanSpace.basisFun (Fin (SpherePacking.truncatedHarmonicDimension n k L)) ℝ

Instances For

noncomputable def SpherePacking.isometricPackingKernel {n k L : ℕ} (f : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (x y : Euclidean n) :

The Hilbert–Schmidt overlap kernel associated with a family of isometric certificate embeddings.

Equations

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

Instances For

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 : α) :

mixedHilbertSchmidtKernel bE (fun (z : α) => (f z).toLinearMap) (fun (z : α) => (f z).toLinearMap) x y = 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 ≤ 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 : α) :

mixedHilbertSchmidtKernel bE (fun (z : α) => (f z).toLinearMap) (fun (z : α) => (f z).toLinearMap) x x = ↑(Module.finrank ℝ F)

@[reducible, inline]

abbrev SpherePacking.CertificateDegreeAmbient (n k L : ℕ) (i : Jacobi.Index k L) :

The Euclidean model for the harmonic degree k + i.val summand of the certificate.

Equations

SpherePacking.CertificateDegreeAmbient n k L i = SpherePacking.Euclidean (SpherePacking.Gegenbauer.harmonicDimension n (k + ↑i))

Instances For

noncomputable def SpherePacking.finiteGramRecurrenceWeight (n k L : ℕ) (v : Jacobi.Space k L) (i : Jacobi.Index k L) :

A Jacobi coordinate weighted by the square root of its harmonic degree dimension.

Equations

SpherePacking.finiteGramRecurrenceWeight n k L v i = √↑(SpherePacking.Gegenbauer.harmonicDimension n (k + ↑i)) * v.ofLp i

Instances For

noncomputable def SpherePacking.finiteGramRecurrenceNormalization (n k L : ℕ) (v : Jacobi.Space k L) :

The sum of the dimension-weighted Jacobi coordinates used to normalize fibre amplitudes.

Equations

SpherePacking.finiteGramRecurrenceNormalization n k L v = ∑ i : SpherePacking.Jacobi.Index k L, SpherePacking.finiteGramRecurrenceWeight n k L v i

Instances For

noncomputable def SpherePacking.finiteGramFibreAmplitude (n k L : ℕ) (v : Jacobi.Space k L) (i : Jacobi.Index k L) :

The square root of a normalized recurrence weight, giving the amplitude of one degree fibre.

Equations

SpherePacking.finiteGramFibreAmplitude n k L v i = √(SpherePacking.finiteGramRecurrenceWeight n k L v i / SpherePacking.finiteGramRecurrenceNormalization n k L v)

Instances For

noncomputable def SpherePacking.finiteGramFibreAmplitudeVector (n k L : ℕ) (v : Jacobi.Space k L) :

The vector of normalized fibre amplitudes in the Euclidean Jacobi space.

Equations

SpherePacking.finiteGramFibreAmplitudeVector n k L v = WithLp.toLp 2 (SpherePacking.finiteGramFibreAmplitude n k L v)

Instances For

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 ≤ 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 < 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) :

finiteGramFibreAmplitude n k L v i ^ 2 = finiteGramRecurrenceWeight n k L v i / 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, 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) :

‖finiteGramFibreAmplitudeVector n k L v‖ = 1

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

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 = finiteGramFibreAmplitude n k L self.weights i
fibreAmplitudes_unit : ‖self.fibreAmplitudes‖ = 1
degreeFibre (i : Jacobi.Index k L) : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i
The degree fibre component.
degreeInjection (i : Jacobi.Index k L) : CertificateDegreeAmbient n k L i →ₗᵢ[ℝ ] CertificateAmbient n k L
The degree injection component.
degree_orthogonal (i j : Jacobi.Index k L) : i ≠ j → ∀ (u : CertificateDegreeAmbient n k L i) (v : CertificateDegreeAmbient n k L j), inner ℝ ((self.degreeInjection i) u) ((self.degreeInjection j) v) = 0
fibre : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L
The fibre component.
fibre_eq_weighted_degree (x : Euclidean n) (v : 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 → CertificateFibre n k →ₗ[ℝ ] Euclidean self.coordinateDimension
The lift component.
bulk : Euclidean n → CertificateFibre n k →ₗ[ℝ ] Euclidean self.coordinateDimension
The bulk component.
boundary : Euclidean n → CertificateFibre n k →ₗ[ℝ ] Euclidean self.coordinateDimension
The boundary component.
remainder : Euclidean n → 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 ∈ unitSphere n → self.lift x = self.spectralCoefficient • self.bulk x + 1 • self.boundary x + self.remainder x
lift_kernel (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, finiteHilbertSchmidtKernel (certificateFibreBasis n k) self.lift x y = inner ℝ x y * isometricPackingKernel self.fibre x y
bulk_kernel (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, finiteHilbertSchmidtKernel (certificateFibreBasis n k) self.bulk x y = isometricPackingKernel self.fibre x y
bulk_boundary_orthogonal (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.bulk x) ((certificateFibreBasis n k) i)) ((self.boundary y) ((certificateFibreBasis n k) i)) = 0
bulk_remainder_orthogonal (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.bulk x) ((certificateFibreBasis n k) i)) ((self.remainder y) ((certificateFibreBasis n k) i)) = 0
boundary_remainder_orthogonal (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.boundary x) ((certificateFibreBasis n k) i)) ((self.remainder y) ((certificateFibreBasis n k) i)) = 0

Instances For

noncomputable def SpherePacking.auxiliaryFiniteGramKernel {n k L : ℕ} (certificate : FiniteGramCertificate n k L) (s : ℝ) (x y : Euclidean n) :

The certificate overlap kernel multiplied by the inner-product shift ⟪x, y⟫ - s.

Equations

SpherePacking.auxiliaryFiniteGramKernel certificate s x y = (inner ℝ x y - s) * SpherePacking.isometricPackingKernel certificate.fibre x y

Instances For

theorem SpherePacking.finiteGramCertificate_shift_identity {n k L : ℕ} (certificate : FiniteGramCertificate n k L) {x y : Euclidean n} (hx : x ∈ unitSphere n) (hy : y ∈ unitSphere n) :

(inner ℝ x y - Jacobi.topEigenvalue n k L) * isometricPackingKernel certificate.fibre x y = finiteHilbertSchmidtKernel (certificateFibreBasis n k) certificate.boundary x y + finiteHilbertSchmidtKernel (certificateFibreBasis n k) certificate.remainder x y

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

0 ≤ isometricPackingKernel f x y

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

isometricPackingKernel f x x = ↑(Gegenbauer.fibreDimension n k)

theorem SpherePacking.isometricPackingKernel_trace_cauchy {n k L : ℕ} (f : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (C : Finset (Euclidean n)) :

(↑C.card * ↑(Gegenbauer.fibreDimension n k)) ^ 2 ≤ ↑(truncatedHarmonicDimension n k L) * ∑ x ∈ C, ∑ y ∈ C, 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) * 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, isometricPackingKernel certificate.fibre x y ≤ ∑ x ∈ C.points, ∑ y ∈ C.points, 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))

@[reducible, inline]

abbrev SpherePacking.HarmonicCertificateAssembly.DegreeBlockIndex (n k L : ℕ) :

Coordinates indexed jointly by a truncated degree and a harmonic basis vector in that degree.

Equations

SpherePacking.HarmonicCertificateAssembly.DegreeBlockIndex n k L = ((i : SpherePacking.Jacobi.Index k L) × Fin (SpherePacking.Gegenbauer.harmonicDimension n (k + ↑i)))

Instances For

@[reducible, inline]

abbrev SpherePacking.HarmonicCertificateAssembly.DegreeBlockPi (n k L : ℕ) :

The orthogonal product of the Euclidean harmonic degree summands.

Equations

SpherePacking.HarmonicCertificateAssembly.DegreeBlockPi n k L = PiLp 2 fun (i : SpherePacking.Jacobi.Index k L) => SpherePacking.CertificateDegreeAmbient n k L i

Instances For

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 (DegreeBlockIndex n k L) = truncatedHarmonicDimension n k L

noncomputable def SpherePacking.HarmonicCertificateAssembly.degreeBlockIndexEquiv (n k L : ℕ) (hkl : k ≤ L) :

DegreeBlockIndex n k L ≃ Fin (truncatedHarmonicDimension n k L)

An enumeration of all degree-block coordinates by the truncated harmonic dimension.

Equations

SpherePacking.HarmonicCertificateAssembly.degreeBlockIndexEquiv n k L hkl = Fintype.equivOfCardEq ⋯

Instances For

noncomputable def SpherePacking.HarmonicCertificateAssembly.degreeBlockReindex (n k L : ℕ) (hkl : k ≤ L) :

EuclideanSpace ℝ (DegreeBlockIndex n k L) ≃ₗᵢ[ℝ ] CertificateAmbient n k L

The coordinate reindexing isometry from the degree-block basis to the certificate ambient space.

Equations

SpherePacking.HarmonicCertificateAssembly.degreeBlockReindex n k L hkl = LinearIsometryEquiv.piLpCongrLeft 2 ℝ ℝ (SpherePacking.HarmonicCertificateAssembly.degreeBlockIndexEquiv n k L hkl)

Instances For

def SpherePacking.HarmonicCertificateAssembly.degreeBlockSingle (n k L : ℕ) (i : Jacobi.Index k L) :

CertificateDegreeAmbient n k L i →ₗᵢ[ℝ ] DegreeBlockPi n k L

The isometric inclusion of one degree summand into the orthogonal product of all degree blocks.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCertificateAssembly.degreeBlockFlatten (n k L : ℕ) :

DegreeBlockPi n k L ≃ₗᵢ[ℝ ] EuclideanSpace ℝ (DegreeBlockIndex n k L)

The isometry flattening the product of degree spaces into joint degree-and-coordinate indices.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCertificateAssembly.degreeBlockTransport (n k L : ℕ) (hkl : k ≤ L) :

DegreeBlockPi n k L →ₗᵢ[ℝ ] CertificateAmbient n k L

The isometry identifying the orthogonal product of degree blocks with the certificate ambient space.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCertificateAssembly.degreeBlockInclusion (n k L : ℕ) (hkl : k ≤ L) (i : Jacobi.Index k L) :

CertificateDegreeAmbient n k L i →ₗᵢ[ℝ ] CertificateAmbient n k L

The inclusion of a single harmonic degree summand into the certificate ambient space.

Equations

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

Instances For

theorem SpherePacking.HarmonicCertificateAssembly.degreeBlockSingle_orthogonal (n k L : ℕ) (i j : Jacobi.Index k L) (hij : i ≠ j) (u : CertificateDegreeAmbient n k L i) (v : CertificateDegreeAmbient n k L j) :

inner ℝ ((degreeBlockSingle n k L i) u) ((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 : CertificateDegreeAmbient n k L i) (v : CertificateDegreeAmbient n k L j) :

inner ℝ ((degreeBlockInclusion n k L hkl i) u) ((degreeBlockInclusion n k L hkl j) v) = 0

noncomputable def SpherePacking.HarmonicCertificateAssembly.weightedDegreeLinearMap (n k L : ℕ) (hkl : k ≤ L) (weights : Jacobi.Space k L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (x : Euclidean n) :

CertificateFibre n k →ₗ[ℝ ] CertificateAmbient n k L

The weighted sum of degree-fibre embeddings into mutually orthogonal ambient degree blocks.

Equations

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

Instances For

@[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 → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (x : Euclidean n) (v : CertificateFibre n k) :

(weightedDegreeLinearMap n k L hkl weights degreeFibre x) v = ∑ i : Jacobi.Index k L, weights.ofLp i • (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 → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (x : Euclidean n) (v w : CertificateFibre n k) :

inner ℝ ((weightedDegreeLinearMap n k L hkl weights degreeFibre x) v) ((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 → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (x : Euclidean n) (v w : CertificateFibre n k) :

inner ℝ ((weightedDegreeLinearMap n k L hkl weights degreeFibre x) v) ((weightedDegreeLinearMap n k L hkl weights degreeFibre x) w) = inner ℝ v w

noncomputable def SpherePacking.HarmonicCertificateAssembly.weightedDegreeIsometry (n k L : ℕ) (hkl : k ≤ L) (weights : Jacobi.Space k L) (hweights : ‖weights‖ = 1) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (x : Euclidean n) :

CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L

The weighted degree embedding bundled as an isometry when the weight vector has unit norm.

Equations

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

Instances For

@[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 → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (x : Euclidean n) (v : CertificateFibre n k) :

(weightedDegreeIsometry n k L hkl weights hweights degreeFibre x) v = ∑ i : Jacobi.Index k L, weights.ofLp i • (degreeBlockInclusion n k L hkl i) ((degreeFibre i x) v)

noncomputable def SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights (n k L : ℕ) (hn : 3 ≤ n) :

A chosen nonnegative unit eigenvector for the largest Gegenbauer Jacobi eigenvalue.

Equations

SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights n k L hn = Classical.choose ⋯

Instances For

theorem SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights_unit (n k L : ℕ) (hn : 3 ≤ n) :

‖harmonicPerronWeights n k L hn‖ = 1

theorem SpherePacking.HarmonicCertificateAssembly.harmonicPerronWeights_eigenvector (n k L : ℕ) (hn : 3 ≤ n) :

(Jacobi.operator n k L) (harmonicPerronWeights n k L hn) = Jacobi.topEigenvalue n k L • harmonicPerronWeights n k L hn

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

0 ≤ (harmonicPerronWeights n k L hn).ofLp i

noncomputable def SpherePacking.HarmonicCertificateAssembly.harmonicRecurrenceWeight (n k L : ℕ) (hn : 3 ≤ n) (i : Jacobi.Index k L) :

The dimension-weighted recurrence coordinate of the chosen harmonic Perron eigenvector.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCertificateAssembly.harmonicRecurrenceNormalization (n k L : ℕ) (hn : 3 ≤ n) :

The normalization sum for the recurrence weights of the harmonic Perron eigenvector.

Equations

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

Instances For

theorem SpherePacking.HarmonicCertificateAssembly.harmonicRecurrenceNormalization_pos (n k L : ℕ) (hn : 3 ≤ n) :

0 < harmonicRecurrenceNormalization n k L hn

noncomputable def SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes (n k L : ℕ) (hn : 3 ≤ n) :

The unit fibre-amplitude vector obtained from the harmonic Perron eigenvector.

Equations

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

Instances For

theorem SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes_unit (n k L : ℕ) (hn : 3 ≤ n) :

‖harmonicFibreAmplitudes n k L hn‖ = 1

@[simp]

theorem SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes_apply (n k L : ℕ) (hn : 3 ≤ n) (i : Jacobi.Index k L) :

(harmonicFibreAmplitudes n k L hn).ofLp i = finiteGramFibreAmplitude n k L (harmonicPerronWeights n k L hn) i

theorem SpherePacking.HarmonicCertificateAssembly.harmonicFibreAmplitudes_sq (n k L : ℕ) (hn : 3 ≤ n) (i : Jacobi.Index k L) :

(harmonicFibreAmplitudes n k L hn).ofLp i ^ 2 = harmonicRecurrenceWeight n k L hn i / harmonicRecurrenceNormalization n k L hn

noncomputable def SpherePacking.HarmonicCertificateAssembly.harmonicWeightedFibre (n k L : ℕ) (hn : 3 ≤ n) (hkl : k ≤ L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) :

Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L

The certificate fibre isometry assembled with amplitudes from the harmonic Perron eigenvector.

Equations

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

Instances For

@[simp]

theorem SpherePacking.HarmonicCertificateAssembly.harmonicWeightedFibre_apply (n k L : ℕ) (hn : 3 ≤ n) (hkl : k ≤ L) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (x : Euclidean n) (v : CertificateFibre n k) :

(harmonicWeightedFibre n k L hn hkl degreeFibre x) v = ∑ i : Jacobi.Index k L, (harmonicFibreAmplitudes n k L hn).ofLp i • (degreeBlockInclusion n k L hkl i) ((degreeFibre i x) v)

noncomputable def SpherePacking.HarmonicCertificateAssembly.harmonicPolynomialEuclideanEquiv (n m : ℕ) (hn : 0 < n) :

↥(harmonicHomogeneousSubmodule n m) ≃ₗᵢ[ℝ ] Euclidean (Gegenbauer.harmonicDimension n m)

An orthonormal coordinate identification of homogeneous harmonic polynomials with Euclidean space.

Equations

SpherePacking.HarmonicCertificateAssembly.harmonicPolynomialEuclideanEquiv n m hn = ((stdOrthonormalBasis ℝ ↥(SpherePacking.harmonicHomogeneousSubmodule n m)).reindex (finCongr ⋯)).repr

Instances For

noncomputable def SpherePacking.HarmonicCertificateAssembly.harmonicDegreeEuclideanEquiv (n k L : ℕ) (hn : 0 < n) (i : Jacobi.Index k L) :

↥(harmonicHomogeneousSubmodule n (k + ↑i)) ≃ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i

The harmonic polynomial coordinate isometry for one degree of the truncated certificate.

Equations

SpherePacking.HarmonicCertificateAssembly.harmonicDegreeEuclideanEquiv n k L hn i = SpherePacking.HarmonicCertificateAssembly.harmonicPolynomialEuclideanEquiv n (k + ↑i) hn

Instances For

noncomputable def SpherePacking.HarmonicCertificateAssembly.tangentPolynomialEuclideanEquiv (n k : ℕ) (x : Euclidean n) (hdimension : Module.finrank ℝ ↥(tangentHarmonicSubmodule n k x) = Gegenbauer.fibreDimension n k) :

↥(tangentHarmonicSubmodule n k x) ≃ₗᵢ[ℝ ] CertificateFibre n k

An orthonormal identification of tangent harmonics with the certificate fibre, using its dimension.

Equations

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

Instances For

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

Data encoding the harmonic coordinate construction.

coordinateDimension : ℕ
The coordinate dimension component.
lift : Euclidean n → CertificateFibre n k →ₗ[ℝ ] Euclidean self.coordinateDimension
The lift component.
bulk : Euclidean n → CertificateFibre n k →ₗ[ℝ ] Euclidean self.coordinateDimension
The bulk component.
boundary : Euclidean n → CertificateFibre n k →ₗ[ℝ ] Euclidean self.coordinateDimension
The boundary component.
remainder : Euclidean n → 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 ∈ unitSphere n → self.lift x = self.spectralCoefficient • self.bulk x + 1 • self.boundary x + self.remainder x
lift_kernel (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, finiteHilbertSchmidtKernel (certificateFibreBasis n k) self.lift x y = inner ℝ x y * isometricPackingKernel fibre x y
bulk_kernel (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, finiteHilbertSchmidtKernel (certificateFibreBasis n k) self.bulk x y = isometricPackingKernel fibre x y
bulk_boundary_orthogonal (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.bulk x) ((certificateFibreBasis n k) i)) ((self.boundary y) ((certificateFibreBasis n k) i)) = 0
bulk_remainder_orthogonal (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.bulk x) ((certificateFibreBasis n k) i)) ((self.remainder y) ((certificateFibreBasis n k) i)) = 0
boundary_remainder_orthogonal (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.boundary x) ((certificateFibreBasis n k) i)) ((self.remainder y) ((certificateFibreBasis n k) i)) = 0

Instances For

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.

Instances For

@[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.solidHarmonicAxisPolynomialLift {n : ℕ} (k r : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) :

↥(tangentHarmonicSubmodule n k x) →ₗ[ℝ ] ↥(harmonicHomogeneousSubmodule n (k + r))

The solid harmonic axis lift restricted from tangent harmonics to the target harmonic degree.

Equations

SpherePacking.solidHarmonicAxisPolynomialLift k r x hx = (SpherePacking.solidHarmonicAxisLift n k x r).restrict ⋯

Instances For

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.

Instances For

noncomputable def SpherePacking.harmonicReferenceUnitAxis {n : ℕ} (hn : 0 < n) :

Euclidean n

The first standard coordinate vector, chosen as a reference unit axis.

Equations

SpherePacking.harmonicReferenceUnitAxis hn = EuclideanSpace.single ⟨0, hn⟩ 1

Instances For

@[simp]

theorem SpherePacking.harmonicReferenceUnitAxis_norm {n : ℕ} (hn : 0 < n) :

‖harmonicReferenceUnitAxis hn‖ = 1

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

CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i

The isometric degree-fibre embedding obtained by a solid harmonic lift along a unit axis.

Equations

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

Instances For

noncomputable def SpherePacking.harmonicDegreeFibre {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (i : Jacobi.Index k L) (x : Euclidean n) :

CertificateFibre n k →ₗᵢ[ℝ ] 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.

Instances For

@[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 = 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)

noncomputable def SpherePacking.SourceJacobiWeights.sourceChannelCoefficient (n k L : ℕ) (m i : Jacobi.Index k L) :

The squared Gegenbauer channel coefficient between adjacent source and target degrees.

Equations

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

Instances For

theorem SpherePacking.SourceJacobiWeights.jacobiMatrix_mul_sqrt_harmonicDimension {n k L : ℕ} (hn : 3 ≤ n) (m i : Jacobi.Index k L) :

Gegenbauer.jacobiMatrix n k L m i * √↑(Gegenbauer.harmonicDimension n (k + ↑m)) = 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, sourceChannelCoefficient n k L m i * finiteGramRecurrenceWeight n k L v i = eigenvalue * 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 < 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 < 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 < 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) :

HarmonicCertificateAssembly.harmonicPerronWeights n k L hn ≠ 0

theorem SpherePacking.HarmonicPerronPositivity.harmonicRecurrenceWeight_pos (n k L : ℕ) (hn : 3 ≤ n) (i : Jacobi.Index k L) :

0 < HarmonicCertificateAssembly.harmonicRecurrenceWeight n k L hn i

theorem SpherePacking.HarmonicPerronPositivity.harmonicFibreAmplitudes_pos (n k L : ℕ) (hn : 3 ≤ n) (i : Jacobi.Index k L) :

0 < (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

@[reducible, inline]

abbrev SpherePacking.HarmonicCoordinateChannels.MatrixCoordinateIndex (n k L : ℕ) :

The pair of ambient coordinate indices used to flatten a projection matrix.

Equations

SpherePacking.HarmonicCoordinateChannels.MatrixCoordinateIndex n k L = ((_ : Fin (SpherePacking.truncatedHarmonicDimension n k L)) × Fin (SpherePacking.truncatedHarmonicDimension n k L))

Instances For

@[reducible, inline]

abbrev SpherePacking.HarmonicCoordinateChannels.ProjectionMatrixSpace (n k L : ℕ) :

The Euclidean space of projection matrices, represented as a family of ambient column vectors.

Equations

SpherePacking.HarmonicCoordinateChannels.ProjectionMatrixSpace n k L = PiLp 2 fun (x : Fin (SpherePacking.truncatedHarmonicDimension n k L)) => SpherePacking.CertificateAmbient n k L

Instances For

@[reducible, inline]

abbrev SpherePacking.HarmonicCoordinateChannels.HarmonicRowChannelSpace (n k L : ℕ) :

The Euclidean space of n ambient row-channel vectors.

Equations

SpherePacking.HarmonicCoordinateChannels.HarmonicRowChannelSpace n k L = PiLp 2 fun (x : Fin n) => SpherePacking.CertificateAmbient n k L

Instances For

@[reducible, inline]

abbrev SpherePacking.HarmonicCoordinateChannels.HarmonicDegreeRowChannelSpace (n k L : ℕ) (i : Jacobi.Index k L) :

The row-channel space restricted to one harmonic degree summand.

Equations

SpherePacking.HarmonicCoordinateChannels.HarmonicDegreeRowChannelSpace n k L i = PiLp 2 fun (x : Fin n) => SpherePacking.CertificateDegreeAmbient n k L i

Instances For

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

0 ≤ SourceJacobiWeights.sourceChannelCoefficient n k L m i

noncomputable def SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient (n k L : ℕ) (hn : 3 ≤ n) (target source : Jacobi.Index k L) :

The adjacent-block amplitude normalized by Perron recurrence weights and the top Jacobi eigenvalue.

Equations

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

Instances For

theorem SpherePacking.HarmonicCoordinateChannels.sourceAdjacentBlockCoefficient_sq {n k L : ℕ} (hn : 3 ≤ n) (hkl : k < L) (target source : Jacobi.Index k L) :

sourceAdjacentBlockCoefficient n k L hn target source ^ 2 = SourceJacobiWeights.sourceChannelCoefficient n k L source target * HarmonicCertificateAssembly.harmonicRecurrenceWeight n k L hn target / (Jacobi.topEigenvalue n k L * 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, 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) :

sourceAdjacentBlockCoefficient n k L hn target source * (HarmonicCertificateAssembly.harmonicFibreAmplitudes n k L hn).ofLp target * √(SourceJacobiWeights.sourceChannelCoefficient n k L source target) = sourceAdjacentBlockCoefficient n k L hn target source ^ 2 * √(Jacobi.topEigenvalue n k L) * (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, sourceAdjacentBlockCoefficient n k L hn target source * (HarmonicCertificateAssembly.harmonicFibreAmplitudes n k L hn).ofLp target * √(SourceJacobiWeights.sourceChannelCoefficient n k L source target) = √(Jacobi.topEigenvalue n k L) * (HarmonicCertificateAssembly.harmonicFibreAmplitudes n k L hn).ofLp source

noncomputable def SpherePacking.HarmonicCoordinateChannels.harmonicDegreeBlockEquiv (n k L : ℕ) (hkl : k ≤ L) :

HarmonicCertificateAssembly.DegreeBlockPi n k L ≃ₗᵢ[ℝ ] CertificateAmbient n k L

The isometric equivalence between the orthogonal degree blocks and the certificate ambient space.

Equations

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

Instances For

def SpherePacking.HarmonicCoordinateChannels.harmonicDegreeAxisTensor (n k L : ℕ) (i : Jacobi.Index k L) (x : Euclidean n) :

CertificateDegreeAmbient n k L i →ₗ[ℝ ] HarmonicDegreeRowChannelSpace n k L i

The linear map sending a degree vector u to the row family a ↦ x a • u.

Equations

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

Instances For

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

Data encoding the source adjacent channel construction.

channel (target source : Jacobi.Index k L) : CertificateDegreeAmbient n k L source →ₗ[ℝ ] HarmonicDegreeRowChannelSpace n k L target
The channel component.
channel_inner (target source : Jacobi.Index k L) : SourceJacobiWeights.sourceChannelCoefficient n k L source target ≠ 0 → ∀ (u v : 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) : 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 : CertificateDegreeAmbient n k L source₁) (v : CertificateDegreeAmbient n k L source₂), inner ℝ ((self.channel target source₁) u) ((self.channel target source₂) v) = 0
axis_projection (x : Euclidean n) : x ∈ unitSphere n → ∀ (target source : Jacobi.Index k L) (u : CertificateFibre n k), (LinearMap.adjoint (self.channel target source)) ((harmonicDegreeAxisTensor n k L target x) ((degreeFibre target x) u)) = √(SourceJacobiWeights.sourceChannelCoefficient n k L source target) • (degreeFibre source x) u

Instances For

@[reducible, inline]

abbrev SpherePacking.HarmonicCoordinateChannels.SourceTargetRowSpace (n k L : ℕ) :

The orthogonal product of row-channel spaces over all target degrees.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCoordinateChannels.sourceAdjacentTargetLinearMap {n k L : ℕ} (hn : 3 ≤ n) (degreeFibre : (i : Jacobi.Index k L) → Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (adjacent : SourceAdjacentChannelData n k L degreeFibre) :

HarmonicCertificateAssembly.DegreeBlockPi n k L →ₗ[ℝ ] SourceTargetRowSpace n k L

The weighted adjacent-channel map from source degree blocks to target row-channel blocks.

Equations

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

Instances For

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

inner ℝ ((sourceAdjacentTargetLinearMap hn degreeFibre adjacent) u) ((sourceAdjacentTargetLinearMap hn degreeFibre adjacent) v) = inner ℝ u v

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

HarmonicCertificateAssembly.DegreeBlockPi n k L →ₗᵢ[ℝ ] SourceTargetRowSpace n k L

The adjacent source-to-target map bundled as an isometry using the channel inner-product identity.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCoordinateChannels.sourceTargetRowTransportLinearMap (n k L : ℕ) (hkl : k ≤ L) :

SourceTargetRowSpace n k L →ₗ[ℝ ] HarmonicRowChannelSpace n k L

The linear map that assembles target degree components separately in each ambient row.

Equations

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

Instances For

theorem SpherePacking.HarmonicCoordinateChannels.sourceTargetRowTransportLinearMap_inner (n k L : ℕ) (hkl : k ≤ L) (u v : SourceTargetRowSpace n k L) :

inner ℝ ((sourceTargetRowTransportLinearMap n k L hkl) u) ((sourceTargetRowTransportLinearMap n k L hkl) v) = inner ℝ u v

noncomputable def SpherePacking.HarmonicCoordinateChannels.sourceTargetRowTransport (n k L : ℕ) (hkl : k ≤ L) :

SourceTargetRowSpace n k L →ₗᵢ[ℝ ] HarmonicRowChannelSpace n k L

The isometry assembling the target degree row blocks into ambient row channels.

Equations

SpherePacking.HarmonicCoordinateChannels.sourceTargetRowTransport n k L hkl = (SpherePacking.HarmonicCoordinateChannels.sourceTargetRowTransportLinearMap n k L hkl).isometryOfInner ⋯

Instances For

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

CertificateAmbient n k L →ₗᵢ[ℝ ] HarmonicRowChannelSpace n k L

The adjacent-channel isometry expressed in certificate ambient coordinates.

Equations

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

Instances For

@[reducible, inline]

abbrev SpherePacking.HarmonicCoordinateChannels.ProjectionChannelSpace (n k L : ℕ) :

The orthogonal product of n + 1 projection-matrix channels.

Equations

SpherePacking.HarmonicCoordinateChannels.ProjectionChannelSpace n k L = PiLp 2 fun (x : Fin (n + 1)) => SpherePacking.HarmonicCoordinateChannels.ProjectionMatrixSpace n k L

Instances For

def SpherePacking.HarmonicCoordinateChannels.harmonicAxisTensor (n k L : ℕ) (x : Euclidean n) :

CertificateAmbient n k L →ₗ[ℝ ] 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.

Instances For

@[simp]

theorem SpherePacking.HarmonicCoordinateChannels.harmonicDegreeBlockEquiv_symm_degreeBlockInclusion (n k L : ℕ) (hkl : k ≤ L) (i : Jacobi.Index k L) (u : CertificateDegreeAmbient n k L i) :

(harmonicDegreeBlockEquiv n k L hkl).symm ((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 → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (x : Euclidean n) (u : CertificateFibre n k) (i : Jacobi.Index k L) :

((harmonicDegreeBlockEquiv n k L hkl).symm ((HarmonicCertificateAssembly.harmonicWeightedFibre n k L hn hkl degreeFibre x) u)).ofLp i = (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 : SourceTargetRowSpace n k L) (x : Euclidean n) (z : CertificateAmbient n k L) :

inner ℝ ((sourceTargetRowTransport n k L hkl) v) ((harmonicAxisTensor n k L x) z) = ∑ target : Jacobi.Index k L, inner ℝ (v.ofLp target) ((harmonicDegreeAxisTensor n k L target x) (((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 → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (adjacent : SourceAdjacentChannelData n k L degreeFibre) (x : Euclidean n) (hx : x ∈ unitSphere n) (target source : Jacobi.Index k L) (z : CertificateDegreeAmbient n k L source) (u : CertificateFibre n k) (a : ℝ) :

inner ℝ ((adjacent.channel target source) z) ((harmonicDegreeAxisTensor n k L target x) (a • (degreeFibre target x) u)) = a * √(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 → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (x : Euclidean n) (u : CertificateFibre n k) (z : CertificateAmbient n k L) :

inner ℝ z ((HarmonicCertificateAssembly.harmonicWeightedFibre n k L hn hkl degreeFibre x) u) = ∑ source : Jacobi.Index k L, (HarmonicCertificateAssembly.harmonicFibreAmplitudes n k L hn).ofLp source * inner ℝ (((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 → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (adjacent : SourceAdjacentChannelData n k L degreeFibre) (x : Euclidean n) (hx : x ∈ unitSphere n) (u : CertificateFibre n k) (z : CertificateAmbient n k L) :

inner ℝ ((sourceAdjacentHarmonicRow hn hkl degreeFibre adjacent) z) ((harmonicAxisTensor n k L x) ((HarmonicCertificateAssembly.harmonicWeightedFibre n k L hn ⋯ degreeFibre x) u)) = √(Jacobi.topEigenvalue n k L) * inner ℝ z ((HarmonicCertificateAssembly.harmonicWeightedFibre n k L hn ⋯ degreeFibre x) u)

def SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbeddingLinearMap (n k L : ℕ) (row : CertificateAmbient n k L →ₗᵢ[ℝ ] HarmonicRowChannelSpace n k L) :

ProjectionMatrixSpace n k L →ₗ[ℝ ] ProjectionChannelSpace n k L

The linear embedding applying a row isometry to each matrix column, with a zero leading channel.

Equations

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

Instances For

@[simp]

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

((spectralMatrixEmbeddingLinearMap n k L row) M).ofLp 0 = 0

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

inner ℝ ((spectralMatrixEmbeddingLinearMap n k L row) M) ((spectralMatrixEmbeddingLinearMap n k L row) N) = inner ℝ M N

def SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbedding (n k L : ℕ) (row : CertificateAmbient n k L →ₗᵢ[ℝ ] HarmonicRowChannelSpace n k L) :

ProjectionMatrixSpace n k L →ₗᵢ[ℝ ] ProjectionChannelSpace n k L

The projection-matrix embedding bundled as an isometry into the enlarged channel space.

Equations

SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbedding n k L row = { toLinearMap := SpherePacking.HarmonicCoordinateChannels.spectralMatrixEmbeddingLinearMap n k L row, norm_map' := ⋯ }

Instances For

@[reducible, inline]

abbrev SpherePacking.HarmonicCoordinateChannels.ProjectionChannelIndex (n k L : ℕ) :

Coordinates indexed by a channel and a pair of ambient matrix coordinates.

Equations

SpherePacking.HarmonicCoordinateChannels.ProjectionChannelIndex n k L = ((_ : Fin (n + 1)) × SpherePacking.HarmonicCoordinateChannels.MatrixCoordinateIndex n k L)

Instances For

def SpherePacking.HarmonicCoordinateChannels.projectionChannelDimension (n k L : ℕ) :

The total number of coordinates in the projection channel space.

Equations

SpherePacking.HarmonicCoordinateChannels.projectionChannelDimension n k L = Fintype.card (SpherePacking.HarmonicCoordinateChannels.ProjectionChannelIndex n k L)

Instances For

noncomputable def SpherePacking.HarmonicCoordinateChannels.fibreProjection {n k L : ℕ} (f : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (x : Euclidean n) :

CertificateAmbient n k L →ₗ[ℝ ] CertificateAmbient n k L

The orthogonal projection onto the image of the isometric fibre embedding at x.

Equations

SpherePacking.HarmonicCoordinateChannels.fibreProjection f x = (f x).toLinearMap ∘ₗ LinearMap.adjoint (f x).toLinearMap

Instances For

noncomputable def SpherePacking.HarmonicCoordinateChannels.projectionMatrixFeature {n k L : ℕ} (f : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (x : Euclidean n) :

ProjectionMatrixSpace n k L

The matrix columns of the fibre projection in the standard certificate ambient basis.

Equations

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

Instances For

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

inner ℝ (projectionMatrixFeature f x) (projectionMatrixFeature f y) = isometricPackingKernel f x y

noncomputable def SpherePacking.HarmonicCoordinateChannels.projectionMatrixFlatten (n k L : ℕ) :

ProjectionMatrixSpace n k L ≃ₗᵢ[ℝ ] EuclideanSpace ℝ (MatrixCoordinateIndex n k L)

The isometry flattening a projection matrix into joint row-and-column coordinates.

Equations

SpherePacking.HarmonicCoordinateChannels.projectionMatrixFlatten n k L = (LinearIsometryEquiv.piLpCurry ℝ 2 fun (x x_1 : Fin (SpherePacking.truncatedHarmonicDimension n k L)) => ℝ).symm

Instances For

noncomputable def SpherePacking.HarmonicCoordinateChannels.projectionChannelFlatten (n k L : ℕ) :

ProjectionChannelSpace n k L ≃ₗᵢ[ℝ ] EuclideanSpace ℝ (ProjectionChannelIndex n k L)

The isometry flattening all projection channels into a single coordinate space.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCoordinateChannels.projectionChannelEuclideanEquiv (n k L : ℕ) :

ProjectionChannelSpace n k L ≃ₗᵢ[ℝ ] Euclidean (projectionChannelDimension n k L)

The coordinate isometry from projection channels to Euclidean space of their total dimension.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCoordinateChannels.rawLiftChannel {n k L : ℕ} (f : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (x : Euclidean n) :

ProjectionChannelSpace n k L

The axis-weighted projection-matrix feature, preceded by a zero channel.

Equations

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

Instances For

@[simp]

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

(rawLiftChannel f x).ofLp 0 = 0

@[simp]

theorem SpherePacking.HarmonicCoordinateChannels.rawLiftChannel_succ {n k L : ℕ} (f : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (x : Euclidean n) (a : Fin n) :

(rawLiftChannel f x).ofLp a.succ = x.ofLp a • projectionMatrixFeature f x

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

inner ℝ (rawLiftChannel f x) (rawLiftChannel f y) = inner ℝ x y * isometricPackingKernel f x y

def SpherePacking.HarmonicCoordinateChannels.firstFibreIndex (n k : ℕ) (hn : 3 ≤ n) :

Fin (Gegenbauer.fibreDimension n k)

The zero coordinate index in the nonempty certificate fibre.

Equations

SpherePacking.HarmonicCoordinateChannels.firstFibreIndex n k hn = ⟨0, ⋯⟩

Instances For

noncomputable def SpherePacking.HarmonicCoordinateChannels.firstFibreVector (n k : ℕ) (hn : 3 ≤ n) :

CertificateFibre n k

The first standard orthonormal vector of the certificate fibre.

Equations

SpherePacking.HarmonicCoordinateChannels.firstFibreVector n k hn = (SpherePacking.certificateFibreBasis n k) (SpherePacking.HarmonicCoordinateChannels.firstFibreIndex n k hn)

Instances For

@[simp]

theorem SpherePacking.HarmonicCoordinateChannels.firstFibreVector_inner_basis (n k : ℕ) (hn : 3 ≤ n) (i : Fin (Gegenbauer.fibreDimension n k)) :

inner ℝ (firstFibreVector n k hn) ((certificateFibreBasis n k) i) = if i = firstFibreIndex n k hn then 1 else 0

noncomputable def SpherePacking.HarmonicCoordinateChannels.rankOneChannelMap (n k L : ℕ) (hn : 3 ≤ n) (v : ProjectionChannelSpace n k L) :

CertificateFibre n k →ₗ[ℝ ] ProjectionChannelSpace n k L

The rank-one map extracting the first fibre coordinate and multiplying a prescribed channel vector.

Equations

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

Instances For

@[simp]

theorem SpherePacking.HarmonicCoordinateChannels.rankOneChannelMap_apply (n k L : ℕ) (hn : 3 ≤ n) (v : ProjectionChannelSpace n k L) (u : CertificateFibre n k) :

(rankOneChannelMap n k L hn v) u = inner ℝ (firstFibreVector n k hn) u • v

theorem SpherePacking.HarmonicCoordinateChannels.rankOneChannelMap_kernel {α : Type u_1} (n k L : ℕ) (hn : 3 ≤ n) (v : α → ProjectionChannelSpace n k L) (x y : α) :

finiteHilbertSchmidtKernel (certificateFibreBasis n k) (fun (z : α) => rankOneChannelMap n k L hn (v z)) x y = inner ℝ (v x) (v y)

noncomputable def SpherePacking.HarmonicCoordinateChannels.embeddedBulkChannel {n k L : ℕ} (embedding : ProjectionMatrixSpace n k L →ₗᵢ[ℝ ] ProjectionChannelSpace n k L) (f : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (x : Euclidean n) :

ProjectionChannelSpace n k L

The fibre projection feature transported into the channel space by an isometric embedding.

Equations

SpherePacking.HarmonicCoordinateChannels.embeddedBulkChannel embedding f x = embedding (SpherePacking.HarmonicCoordinateChannels.projectionMatrixFeature f x)

Instances For

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

inner ℝ (embeddedBulkChannel embedding f x) (embeddedBulkChannel embedding f y) = isometricPackingKernel f x y

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

Data encoding the source spectral row construction.

row : CertificateAmbient n k L →ₗᵢ[ℝ ] 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 ∈ unitSphere n → ∀ (u : CertificateFibre n k), (LinearMap.adjoint self.row.toLinearMap) ((harmonicAxisTensor n k L x) ((fibre x) u)) = self.spectralCoefficient • (fibre x) u

Instances For

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

SourceSpectralRowData n k L (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.

Instances For

theorem SpherePacking.HarmonicCoordinateChannels.sourceSpectralBulk_lift_inner {n k L : ℕ} (fibre : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (source : SourceSpectralRowData n k L fibre) (x y : Euclidean n) (hy : y ∈ unitSphere n) :

inner ℝ (embeddedBulkChannel (spectralMatrixEmbedding n k L source.row) fibre x) (rawLiftChannel fibre y) = source.spectralCoefficient * isometricPackingKernel fibre x y

noncomputable def SpherePacking.HarmonicCoordinateChannels.euclideanChannelFeatureMap (n k L : ℕ) (hn : 3 ≤ n) (v : ProjectionChannelSpace n k L) :

CertificateFibre n k →ₗ[ℝ ] Euclidean (projectionChannelDimension n k L)

The rank-one channel feature map expressed in ordinary Euclidean coordinates.

Equations

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

Instances For

theorem SpherePacking.HarmonicCoordinateChannels.euclideanChannelFeatureMap_inner (n k L : ℕ) (hn : 3 ≤ n) (v w : ProjectionChannelSpace n k L) (u z : CertificateFibre n k) :

inner ℝ ((euclideanChannelFeatureMap n k L hn v) u) ((euclideanChannelFeatureMap n k L hn w) z) = inner ℝ (firstFibreVector n k hn) u * (inner ℝ (firstFibreVector n k hn) z * inner ℝ v w)

theorem SpherePacking.HarmonicCoordinateChannels.euclideanChannelFeatureMap_kernel {α : Type u_1} (n k L : ℕ) (hn : 3 ≤ n) (v : α → ProjectionChannelSpace n k L) (x y : α) :

finiteHilbertSchmidtKernel (certificateFibreBasis n k) (fun (z : α) => euclideanChannelFeatureMap n k L hn (v z)) x y = inner ℝ (v x) (v y)

noncomputable def SpherePacking.HarmonicCoordinateChannels.bulkCoordinateMap {n k L : ℕ} (hn : 3 ≤ n) (embedding : ProjectionMatrixSpace n k L →ₗᵢ[ℝ ] ProjectionChannelSpace n k L) (f : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (x : Euclidean n) :

CertificateFibre n k →ₗ[ℝ ] Euclidean (projectionChannelDimension n k L)

The Euclidean feature map for an isometrically embedded bulk projection channel.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCoordinateChannels.liftCoordinateMap {n k L : ℕ} (hn : 3 ≤ n) (f : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (x : Euclidean n) :

CertificateFibre n k →ₗ[ℝ ] Euclidean (projectionChannelDimension n k L)

The Euclidean feature map for the axis-weighted lifted projection channel.

Equations

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

Instances For

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

finiteHilbertSchmidtKernel (certificateFibreBasis n k) (bulkCoordinateMap hn embedding f) x y = isometricPackingKernel f x y

theorem SpherePacking.HarmonicCoordinateChannels.liftCoordinateMap_kernel {n k L : ℕ} (hn : 3 ≤ n) (f : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (x y : Euclidean n) :

finiteHilbertSchmidtKernel (certificateFibreBasis n k) (liftCoordinateMap hn f) x y = inner ℝ x y * isometricPackingKernel f x y

theorem SpherePacking.HarmonicCoordinateChannels.sourceSpectralBulk_lift_basis_inner {n k L : ℕ} (hn : 3 ≤ n) (fibre : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (source : SourceSpectralRowData n k L fibre) (x y : Euclidean n) (hy : y ∈ unitSphere n) (i : Fin (Gegenbauer.fibreDimension n k)) :

inner ℝ ((bulkCoordinateMap hn (spectralMatrixEmbedding n k L source.row) fibre x) ((certificateFibreBasis n k) i)) ((liftCoordinateMap hn fibre y) ((certificateFibreBasis n k) i)) = source.spectralCoefficient * inner ℝ ((bulkCoordinateMap hn (spectralMatrixEmbedding n k L source.row) fibre x) ((certificateFibreBasis n k) i)) ((bulkCoordinateMap hn (spectralMatrixEmbedding n k L source.row) fibre y) ((certificateFibreBasis n k) i))

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

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 → CertificateFibre n k →ₗ[ℝ ] Euclidean (projectionChannelDimension n k L)
The boundary component.
remainder : Euclidean n → CertificateFibre n k →ₗ[ℝ ] Euclidean (projectionChannelDimension n k L)
The remainder component.
decomposition (x : Euclidean n) : x ∈ unitSphere n → liftCoordinateMap hn fibre x = self.spectralCoefficient • bulkCoordinateMap hn embedding fibre x + 1 • self.boundary x + self.remainder x
bulk_boundary_orthogonal (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((bulkCoordinateMap hn embedding fibre x) ((certificateFibreBasis n k) i)) ((self.boundary y) ((certificateFibreBasis n k) i)) = 0
bulk_remainder_orthogonal (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((bulkCoordinateMap hn embedding fibre x) ((certificateFibreBasis n k) i)) ((self.remainder y) ((certificateFibreBasis n k) i)) = 0
boundary_remainder_orthogonal (x : Euclidean n) : x ∈ unitSphere n → ∀ y ∈ unitSphere n, ∀ (i : Fin (Gegenbauer.fibreDimension n k)), inner ℝ ((self.boundary x) ((certificateFibreBasis n k) i)) ((self.remainder y) ((certificateFibreBasis n k) i)) = 0

Instances For

noncomputable def SpherePacking.HarmonicCoordinateChannels.sourceSpectralResidual {n k L : ℕ} (hn : 3 ≤ n) (fibre : Euclidean n → CertificateFibre n k →ₗᵢ[ℝ ] CertificateAmbient n k L) (source : SourceSpectralRowData n k L fibre) (x : Euclidean n) :

CertificateFibre n k →ₗ[ℝ ] Euclidean (projectionChannelDimension n k L)

The lifted coordinate map minus the prescribed spectral multiple of the bulk coordinate map.

Equations

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

Instances For

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

inner ℝ ((bulkCoordinateMap hn (spectralMatrixEmbedding n k L source.row) fibre x) ((certificateFibreBasis n k) i)) ((sourceSpectralResidual hn fibre source y) ((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 → CertificateFibre n k →ₗᵢ[ℝ ] CertificateDegreeAmbient n k L i) (source : SourceSpectralRowData n k L (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))

@[reducible, inline]

noncomputable abbrev SpherePacking.HarmonicCoordinateOperators.HarmonicSpace (n m : ℕ) :

The Fischer inner product space of homogeneous harmonic polynomials of degree m.

Equations

SpherePacking.HarmonicCoordinateOperators.HarmonicSpace n m = SpherePacking.harmonicHomogeneousSubmodule n m

Instances For

@[reducible, inline]

abbrev SpherePacking.HarmonicCoordinateOperators.CoordinateHarmonicSpace (n m : ℕ) :

The orthogonal product of one harmonic polynomial space for each coordinate direction.

Equations

SpherePacking.HarmonicCoordinateOperators.CoordinateHarmonicSpace n m = PiLp 2 fun (x : Fin n) => ↥(SpherePacking.HarmonicCoordinateOperators.HarmonicSpace n m)

Instances For

noncomputable def SpherePacking.HarmonicCoordinateOperators.coordinateAxis (n : ℕ) (j : Fin n) :

Euclidean n

The standard unit vector in coordinate direction j.

Equations

SpherePacking.HarmonicCoordinateOperators.coordinateAxis n j = EuclideanSpace.single j 1

Instances For

@[simp]

theorem SpherePacking.HarmonicCoordinateOperators.axisPolynomial_coordinateAxis (n : ℕ) (j : Fin n) :

axisPolynomial n (coordinateAxis n j) = MvPolynomial.X j

theorem SpherePacking.HarmonicCoordinateOperators.directionalDerivative_coordinateAxis (n : ℕ) (j : Fin n) (p : MvPolynomial (Fin n) ℝ) :

(directionalDerivative n (coordinateAxis n j)) p = (MvPolynomial.pderiv j) p

noncomputable def SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateDerivative (n m : ℕ) (j : Fin n) :

↥(HarmonicSpace n (m + 1)) →ₗ[ℝ ] ↥(HarmonicSpace n m)

Coordinate differentiation restricted from harmonic degree m + 1 to degree m.

Equations

SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateDerivative n m j = SpherePacking.harmonicDirectionalDerivative n m (SpherePacking.HarmonicCoordinateOperators.coordinateAxis n j)

Instances For

@[simp]

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateDerivative_apply (n m : ℕ) (j : Fin n) (p : ↥(HarmonicSpace n (m + 1))) :

↑((harmonicCoordinateDerivative n m j) p) = (MvPolynomial.pderiv j) ↑p

noncomputable def SpherePacking.HarmonicCoordinateOperators.harmonicGradient (n m : ℕ) :

↥(HarmonicSpace n (m + 1)) →ₗ[ℝ ] CoordinateHarmonicSpace n m

The vector of coordinate derivatives of a homogeneous harmonic polynomial.

Equations

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

Instances For

theorem SpherePacking.HarmonicCoordinateOperators.harmonicGradient_inner (n m : ℕ) (p q : ↥(HarmonicSpace n (m + 1))) :

inner ℝ ((harmonicGradient n m) p) ((harmonicGradient n m) q) = ↑(m + 1) * inner ℝ p q

noncomputable def SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising (n m : ℕ) (j : Fin n) :

↥(HarmonicSpace n m) →ₗ[ℝ ] ↥(HarmonicSpace n (m + 1))

The Fischer adjoint of coordinate differentiation, raising the harmonic degree by one.

Equations

SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising n m j = LinearMap.adjoint (SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateDerivative n m j)

Instances For

noncomputable def SpherePacking.HarmonicCoordinateOperators.harmonicCoGradient (n m : ℕ) :

↥(HarmonicSpace n m) →ₗ[ℝ ] CoordinateHarmonicSpace n (m + 1)

The vector of Fischer adjoint coordinate-raising operators.

Equations

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

Instances For

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising_eq_axisLift {n : ℕ} (hn : 0 < n) (k : ℕ) (j : Fin n) :

harmonicCoordinateRaising n (k + 1) j = harmonicAxisLift hn k (coordinateAxis n j)

theorem SpherePacking.HarmonicCoordinateOperators.harmonicGradient_coGradient_orthogonal (n m : ℕ) (p : ↥(HarmonicSpace n (m + 2))) (q : ↥(HarmonicSpace n m)) :

inner ℝ ((harmonicGradient n (m + 1)) p) ((harmonicCoGradient n m) q) = 0

def SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator (n m : ℕ) :

The factor 2 * m + n used to normalize the upper and lower harmonic channels.

Equations

SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator n m = 2 * ↑m + ↑n

Instances For

noncomputable def SpherePacking.HarmonicCoordinateOperators.upperChannelWeight (n m : ℕ) :

The squared norm factor (m + 1) / (2 * m + n) of the upper channel adjoint.

Equations

SpherePacking.HarmonicCoordinateOperators.upperChannelWeight n m = ↑(m + 1) / SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator n m

Instances For

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

0 < upperChannelDenominator n m

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

0 < upperChannelWeight n m

noncomputable def SpherePacking.HarmonicCoordinateOperators.upperChannelAdjoint (n m : ℕ) :

↥(HarmonicSpace n (m + 1)) →ₗ[ℝ ] CoordinateHarmonicSpace n m

The harmonic gradient scaled by the inverse square root of the channel denominator.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCoordinateOperators.upperChannel (n m : ℕ) :

CoordinateHarmonicSpace n m →ₗ[ℝ ] ↥(HarmonicSpace n (m + 1))

The Fischer adjoint of the scaled harmonic gradient.

Equations

SpherePacking.HarmonicCoordinateOperators.upperChannel n m = LinearMap.adjoint (SpherePacking.HarmonicCoordinateOperators.upperChannelAdjoint n m)

Instances For

@[simp]

theorem SpherePacking.HarmonicCoordinateOperators.upperChannel_adjoint (n m : ℕ) :

LinearMap.adjoint (upperChannel n m) = upperChannelAdjoint n m

theorem SpherePacking.HarmonicCoordinateOperators.upperChannelAdjoint_inner {n : ℕ} (hn : 0 < n) (m : ℕ) (p q : ↥(HarmonicSpace n (m + 1))) :

inner ℝ ((upperChannelAdjoint n m) p) ((upperChannelAdjoint n m) q) = 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 ⋯

Instances For

noncomputable def SpherePacking.HarmonicCoordinateOperators.upperChannelIsometry {n : ℕ} (hn : 0 < n) (m : ℕ) :

↥(HarmonicSpace n (m + 1)) →ₗᵢ[ℝ ] CoordinateHarmonicSpace n m

The upper channel adjoint normalized to an isometry from harmonics to coordinate harmonics.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCoordinateOperators.lowerChannelWeight (n m : ℕ) :

The squared norm factor (m + n - 2) / (2 * m + n - 2) of the lower channel adjoint.

Equations

SpherePacking.HarmonicCoordinateOperators.lowerChannelWeight n m = (↑m + ↑n - 2) / (2 * ↑m + ↑n - 2)

Instances For

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

0 < lowerChannelWeight n m

noncomputable def SpherePacking.HarmonicCoordinateOperators.lowerChannelAdjoint (n m : ℕ) :

↥(HarmonicSpace n m) →ₗ[ℝ ] CoordinateHarmonicSpace n (m + 1)

The harmonic co-gradient scaled by the inverse square root of the channel denominator.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicCoordinateOperators.lowerChannel (n m : ℕ) :

CoordinateHarmonicSpace n (m + 1) →ₗ[ℝ ] ↥(HarmonicSpace n m)

The Fischer adjoint of the scaled harmonic co-gradient.

Equations

SpherePacking.HarmonicCoordinateOperators.lowerChannel n m = LinearMap.adjoint (SpherePacking.HarmonicCoordinateOperators.lowerChannelAdjoint n m)

Instances For

@[simp]

theorem SpherePacking.HarmonicCoordinateOperators.lowerChannel_adjoint (n m : ℕ) :

LinearMap.adjoint (lowerChannel n m) = lowerChannelAdjoint n m

theorem SpherePacking.HarmonicCoordinateOperators.upperChannelAdjoint_lowerChannelAdjoint_orthogonal (n m : ℕ) (p : ↥(HarmonicSpace n (m + 2))) (q : ↥(HarmonicSpace n m)) :

inner ℝ ((upperChannelAdjoint n (m + 1)) p) ((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 : ↥(HarmonicSpace n m)) :

∑ j : Fin n, (MvPolynomial.pderiv j) (MvPolynomial.X j * ↑p) = ↑(n + m) • ↑p

noncomputable def SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaisingZero (n : ℕ) (j : Fin n) :

↥(HarmonicSpace n 0) →ₗ[ℝ ] ↥(HarmonicSpace n 1)

Coordinate multiplication restricted from constant harmonics to degree-one harmonics.

Equations

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

Instances For

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising_zero_eq (n : ℕ) (j : Fin n) :

harmonicCoordinateRaising n 0 j = harmonicCoordinateRaisingZero n j

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising_apply_polynomial {n : ℕ} (hn : 0 < n) (m : ℕ) (j : Fin n) (p : ↥(HarmonicSpace n m)) :

↑((harmonicCoordinateRaising n m j) p) = MvPolynomial.X j * ↑p - (upperChannelDenominator n (m - 1))⁻¹ • (radialPolynomial n * (MvPolynomial.pderiv j) ↑p)

noncomputable def SpherePacking.HarmonicCoordinateOperators.lowerFischerGradientWeight (n m : ℕ) :

The Fischer squared norm factor for the harmonic co-gradient before channel normalization.

Equations

SpherePacking.HarmonicCoordinateOperators.lowerFischerGradientWeight n m = ↑(n + m) - (SpherePacking.HarmonicCoordinateOperators.upperChannelDenominator n (m - 1))⁻¹ * (2 * ↑m)

Instances For

theorem SpherePacking.HarmonicCoordinateOperators.lowerFischerGradientWeight_eq {n : ℕ} (hn : 3 ≤ n) (m : ℕ) :

lowerFischerGradientWeight n m = upperChannelDenominator n m * lowerChannelWeight n m

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoordinateRaising_derivative_sum {n : ℕ} (hn : 3 ≤ n) (m : ℕ) (p : ↥(HarmonicSpace n m)) :

∑ j : Fin n, (MvPolynomial.pderiv j) ↑((harmonicCoordinateRaising n m j) p) = lowerFischerGradientWeight n m • ↑p

theorem SpherePacking.HarmonicCoordinateOperators.harmonicCoGradient_inner {n : ℕ} (hn : 3 ≤ n) (m : ℕ) (p q : ↥(HarmonicSpace n m)) :

inner ℝ ((harmonicCoGradient n m) p) ((harmonicCoGradient n m) q) = upperChannelDenominator n m * lowerChannelWeight n m * inner ℝ p q

theorem SpherePacking.HarmonicCoordinateOperators.lowerChannelAdjoint_inner {n : ℕ} (hn : 3 ≤ n) (m : ℕ) (p q : ↥(HarmonicSpace n m)) :

inner ℝ ((lowerChannelAdjoint n m) p) ((lowerChannelAdjoint n m) q) = lowerChannelWeight n m * inner ℝ p q

noncomputable def SpherePacking.HarmonicCoordinateOperators.lowerChannelIsometry {n : ℕ} (hn : 3 ≤ n) (m : ℕ) :

↥(HarmonicSpace n m) →ₗᵢ[ℝ ] CoordinateHarmonicSpace n (m + 1)

The lower channel adjoint normalized to an isometry into the next coordinate-harmonic degree.

Equations

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

Instances For

theorem SpherePacking.HarmonicCoordinateOperators.upperChannelIsometry_lowerChannelIsometry_orthogonal {n : ℕ} (hn : 3 ≤ n) (m : ℕ) (p : ↥(HarmonicSpace n (m + 2))) (q : ↥(HarmonicSpace n m)) :

inner ℝ ((upperChannelIsometry ⋯ (m + 1)) p) ((lowerChannelIsometry hn m) q) = 0

noncomputable def SpherePacking.HarmonicSourceProjection.harmonicAxisTensor (n m : ℕ) (x : Euclidean n) :

↥(HarmonicCoordinateOperators.HarmonicSpace n m) →ₗ[ℝ ] 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.

Instances For

noncomputable def SpherePacking.HarmonicSourceProjection.solidHarmonicSource {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) :

↥(tangentHarmonicSubmodule n k x) →ₗ[ℝ ] HarmonicCoordinateOperators.CoordinateHarmonicSpace n (k + r)

The solid harmonic axis isometry followed by tensoring with the source axis.

Equations

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

Instances For

theorem SpherePacking.HarmonicSourceProjection.upperChannel_harmonicAxisTensor_inner (n m : ℕ) (x : Euclidean n) (p : ↥(HarmonicCoordinateOperators.HarmonicSpace n m)) (q : ↥(HarmonicCoordinateOperators.HarmonicSpace n (m + 1))) :

inner ℝ ((HarmonicCoordinateOperators.upperChannel n m) ((harmonicAxisTensor n m x) p)) q = (√(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

noncomputable def SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperCoefficient (n k r : ℕ) :

The coefficient of the upper-channel image of a solid harmonic source, in Fischer normalization.

Equations

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

Instances For

theorem SpherePacking.HarmonicSourceProjection.upperChannel_solidHarmonicSource {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) (p : ↥(tangentHarmonicSubmodule n k x)) :

(HarmonicCoordinateOperators.upperChannel n (k + r)) ((solidHarmonicSource hn k r x hx) p) = solidHarmonicSourceUpperCoefficient n k r • (solidHarmonicAxisPolynomialIsometry hn k (r + 1) x hx) p

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

0 < solidHarmonicSourceUpperCoefficient n k r

noncomputable def SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperIsometryCoefficient (n k r : ℕ) :

The upper solid-harmonic source coefficient adjusted to the normalized channel isometry.

Equations

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

Instances For

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperCoefficient_sq {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) :

solidHarmonicSourceUpperCoefficient n k r ^ 2 = (↑r + 1) * (↑r + harmonicAxisParameter n k - 2) / ((2 * ↑r + harmonicAxisParameter n k - 2) * HarmonicCoordinateOperators.upperChannelDenominator n (k + r))

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperIsometryCoefficient_sq {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) :

solidHarmonicSourceUpperIsometryCoefficient n k r ^ 2 = Gegenbauer.alphaSq n k (k + r)

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

0 < solidHarmonicSourceUpperIsometryCoefficient n k r

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceUpperIsometryCoefficient_eq_sqrt {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) :

solidHarmonicSourceUpperIsometryCoefficient n k r = √(Gegenbauer.alphaSq n k (k + r))

theorem SpherePacking.HarmonicSourceProjection.harmonic_inner_smul_right (n m : ℕ) (p q : ↥(HarmonicCoordinateOperators.HarmonicSpace n m)) (c : ℝ) :

inner ℝ p (c • q) = c * inner ℝ p q

theorem SpherePacking.HarmonicSourceProjection.harmonic_inner_smul_left (n m : ℕ) (p q : ↥(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 (HarmonicCoordinateOperators.upperChannelIsometry ⋯ (k + r)).toLinearMap) ((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 : ↥(HarmonicCoordinateOperators.HarmonicSpace n (m + 1))) (q : ↥(HarmonicCoordinateOperators.HarmonicSpace n m)) :

inner ℝ ((HarmonicCoordinateOperators.lowerChannel n m) ((harmonicAxisTensor n (m + 1) x) p)) q = (√(HarmonicCoordinateOperators.upperChannelDenominator n m))⁻¹ * Fischer.polynomialInner n ((directionalDerivative n x) ↑p) ↑q

noncomputable def SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerCoefficient (n k r : ℕ) :

The coefficient of the lower-channel image of a solid harmonic source, in Fischer normalization.

Equations

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

Instances For

theorem SpherePacking.HarmonicSourceProjection.lowerChannel_solidHarmonicSource {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) (p : ↥(tangentHarmonicSubmodule n k x)) :

(HarmonicCoordinateOperators.lowerChannel n (k + r)) ((solidHarmonicSource hn k (r + 1) x hx) p) = solidHarmonicSourceLowerCoefficient n k r • (solidHarmonicAxisPolynomialIsometry hn k r x hx) p

noncomputable def SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerIsometryCoefficient (n k r : ℕ) :

The lower solid-harmonic source coefficient adjusted to the normalized channel isometry.

Equations

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

Instances For

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

0 < solidHarmonicSourceLowerCoefficient n k r

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerCoefficient_sq {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) :

solidHarmonicSourceLowerCoefficient n k r ^ 2 = (↑r + 1) * (↑r + harmonicAxisParameter n k - 2) / ((2 * ↑r + harmonicAxisParameter n k - 2) * HarmonicCoordinateOperators.upperChannelDenominator n (k + r))

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerIsometryCoefficient_sq {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) :

solidHarmonicSourceLowerIsometryCoefficient n k r ^ 2 = Gegenbauer.betaSq n k (k + (r + 1))

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

0 < solidHarmonicSourceLowerIsometryCoefficient n k r

theorem SpherePacking.HarmonicSourceProjection.solidHarmonicSourceLowerIsometryCoefficient_eq_sqrt {n : ℕ} (hn : 3 ≤ n) (k r : ℕ) :

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 (HarmonicCoordinateOperators.lowerChannelIsometry hn (k + r)).toLinearMap) ((solidHarmonicSource hn k (r + 1) x hx) p) = √(Gegenbauer.betaSq n k (k + (r + 1))) • (solidHarmonicAxisPolynomialIsometry hn k r x hx) p

def SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCastLinearMap (n r s : ℕ) (h : r = s) :

↥(HarmonicCoordinateOperators.HarmonicSpace n r) →ₗ[ℝ ] ↥(HarmonicCoordinateOperators.HarmonicSpace n s)

The identity on underlying polynomials transported along an equality of harmonic degrees.

Equations

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

Instances For

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

inner ℝ ((harmonicDegreeCastLinearMap n r s h) p) ((harmonicDegreeCastLinearMap n r s h) q) = inner ℝ p q

noncomputable def SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCast (n r s : ℕ) (h : r = s) :

↥(HarmonicCoordinateOperators.HarmonicSpace n r) →ₗᵢ[ℝ ] ↥(HarmonicCoordinateOperators.HarmonicSpace n s)

The isometric degree cast on harmonic polynomials.

Equations

SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCast n r s h = (SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCastLinearMap n r s h).isometryOfInner ⋯

Instances For

@[simp]

theorem SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeCast_adjoint_apply (n r s : ℕ) (h : r = s) (p : ↥(HarmonicCoordinateOperators.HarmonicSpace n s)) :

(LinearMap.adjoint (harmonicDegreeCast n r s h).toLinearMap) p = (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)

HarmonicCoordinateOperators.CoordinateHarmonicSpace n r →ₗ[ℝ ] HarmonicCoordinateOperators.CoordinateHarmonicSpace n s

noncomputable def SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCastLinearMap (n r s : ℕ) (h : r = s) :

The linear map applying the harmonic degree cast in every coordinate direction.

Equations

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

Instances For

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

inner ℝ ((coordinateHarmonicDegreeCastLinearMap n r s h) z) ((coordinateHarmonicDegreeCastLinearMap n r s h) w) = inner ℝ z w

HarmonicCoordinateOperators.CoordinateHarmonicSpace n r →ₗᵢ[ℝ ] HarmonicCoordinateOperators.CoordinateHarmonicSpace n s

noncomputable def SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCast (n r s : ℕ) (h : r = s) :

The isometric degree cast on coordinate families of harmonic polynomials.

Equations

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

Instances For

@[simp]

theorem SpherePacking.HarmonicAdjacentChannelTransport.coordinateHarmonicDegreeCast_adjoint_apply (n r s : ℕ) (h : r = s) (z : HarmonicCoordinateOperators.CoordinateHarmonicSpace n s) :

(LinearMap.adjoint (coordinateHarmonicDegreeCast n r s h).toLinearMap) z = (coordinateHarmonicDegreeCast n s r ⋯) z

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

(coordinateHarmonicDegreeCast n r s h) ((HarmonicSourceProjection.harmonicAxisTensor n r x) p) = (HarmonicSourceProjection.harmonicAxisTensor n s x) ((harmonicDegreeCast n r s h) p)

noncomputable def SpherePacking.HarmonicAdjacentChannelTransport.coordinateDegreeTransportLinearMap {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (i : Jacobi.Index k L) :

HarmonicCoordinateOperators.CoordinateHarmonicSpace n (k + ↑i) →ₗ[ℝ ] HarmonicCoordinateChannels.HarmonicDegreeRowChannelSpace n k L i

The linear map expressing each coordinate harmonic polynomial in its degree-fibre Euclidean basis.

Equations

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

Instances For

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

inner ℝ ((coordinateDegreeTransportLinearMap hn k L i) z) ((coordinateDegreeTransportLinearMap hn k L i) w) = inner ℝ z w

noncomputable def SpherePacking.HarmonicAdjacentChannelTransport.coordinateDegreeTransport {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (i : Jacobi.Index k L) :

HarmonicCoordinateOperators.CoordinateHarmonicSpace n (k + ↑i) →ₗᵢ[ℝ ] HarmonicCoordinateChannels.HarmonicDegreeRowChannelSpace n k L i

The coordinatewise harmonic-to-Euclidean degree transport bundled as an isometry.

Equations

SpherePacking.HarmonicAdjacentChannelTransport.coordinateDegreeTransport hn k L i = (SpherePacking.HarmonicAdjacentChannelTransport.coordinateDegreeTransportLinearMap hn k L i).isometryOfInner ⋯

Instances For

theorem SpherePacking.HarmonicAdjacentChannelTransport.coordinateDegreeTransport_axis {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (i : Jacobi.Index k L) (x : Euclidean n) (p : ↥(HarmonicCoordinateOperators.HarmonicSpace n (k + ↑i))) :

(coordinateDegreeTransport hn k L i) ((HarmonicSourceProjection.harmonicAxisTensor n (k + ↑i) x) p) = (HarmonicCoordinateChannels.harmonicDegreeAxisTensor n k L i x) ((HarmonicCertificateAssembly.harmonicDegreeEuclideanEquiv n k L ⋯ i) p)

noncomputable def SpherePacking.HarmonicAdjacentChannelTransport.upperAdjacentChannel {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (target source : Jacobi.Index k L) (hadjacent : ↑target + 1 = ↑source) :

CertificateDegreeAmbient n k L source →ₗᵢ[ℝ ] HarmonicCoordinateChannels.HarmonicDegreeRowChannelSpace n k L target

The normalized upper channel transported between adjacent Euclidean degree fibres.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicAdjacentChannelTransport.lowerAdjacentChannel {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (target source : Jacobi.Index k L) (hadjacent : ↑source + 1 = ↑target) :

CertificateDegreeAmbient n k L source →ₗᵢ[ℝ ] HarmonicCoordinateChannels.HarmonicDegreeRowChannelSpace n k L target

The normalized lower channel transported between adjacent Euclidean degree fibres.

Equations

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

Instances For

noncomputable def SpherePacking.HarmonicAdjacentChannelTransport.adjacentChannel {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (target source : Jacobi.Index k L) :

CertificateDegreeAmbient n k L source →ₗ[ℝ ] HarmonicCoordinateChannels.HarmonicDegreeRowChannelSpace n k L target

The appropriate upper or lower adjacent-degree channel, and zero for nonadjacent degrees.

Equations

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

Instances For

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 : CertificateDegreeAmbient n k L high) (q : CertificateDegreeAmbient n k L low) :

inner ℝ ((upperAdjacentChannel hn k L target high hhigh) p) ((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 : CertificateDegreeAmbient n k L low) (q : CertificateDegreeAmbient n k L high) :

inner ℝ ((lowerAdjacentChannel hn k L target low hlow) p) ((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 : SourceJacobiWeights.sourceChannelCoefficient n k L source target ≠ 0) (u v : CertificateDegreeAmbient n k L source) :

inner ℝ ((adjacentChannel hn k L target source) u) ((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 : SourceJacobiWeights.sourceChannelCoefficient n k L source target = 0) :

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 : CertificateDegreeAmbient n k L source₁) (v : CertificateDegreeAmbient n k L source₂) :

inner ℝ ((adjacentChannel hn k L target source₁) u) ((adjacentChannel hn k L target source₂) v) = 0

noncomputable def SpherePacking.HarmonicAdjacentChannelTransport.sourceTangentPolynomial {n : ℕ} (hn : 3 ≤ n) (k : ℕ) (x : Euclidean n) (hx : ‖x‖ = 1) (u : CertificateFibre n k) :

↥(tangentHarmonicSubmodule n k x)

The tangent harmonic polynomial represented by a certificate fibre vector at a unit axis.

Equations

SpherePacking.HarmonicAdjacentChannelTransport.sourceTangentPolynomial hn k x hx u = (SpherePacking.HarmonicCertificateAssembly.tangentPolynomialEuclideanEquiv n k x ⋯).symm u

Instances For

theorem SpherePacking.HarmonicAdjacentChannelTransport.harmonicDegreeFibre_apply_eq {n : ℕ} (hn : 3 ≤ n) (k L : ℕ) (i : Jacobi.Index k L) (x : Euclidean n) (hx : ‖x‖ = 1) (u : CertificateFibre n k) :

(harmonicDegreeFibre hn k L i x) u = (HarmonicCertificateAssembly.harmonicDegreeEuclideanEquiv n k L ⋯ i) ((solidHarmonicAxisPolynomialIsometry hn k (↑i) x hx) (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 : CertificateFibre n k) :

(LinearMap.adjoint (upperAdjacentChannel hn k L target source h).toLinearMap) ((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 : CertificateFibre n k) :

(LinearMap.adjoint (lowerAdjacentChannel hn k L target source h).toLinearMap) ((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 ∈ unitSphere n) (target source : Jacobi.Index k L) (u : CertificateFibre n k) :

(LinearMap.adjoint (adjacentChannel hn k L target source)) ((HarmonicCoordinateChannels.harmonicDegreeAxisTensor n k L target x) ((harmonicDegreeFibre hn k L target x) u)) = √(SourceJacobiWeights.sourceChannelCoefficient n k L source target) • (harmonicDegreeFibre hn k L source x) u