Gaussian kernel coefficients and parity

Abstract

A rational Gaussian kernel has symmetric integer weights and even paired coefficients.

Definition 1.1 (The recursive integer array).

$$\forall m:\mathbb{N},(\forall k:\mathbb{N},((\mathrm{weight}\left(0,k\right)=1)\wedge ((\mathrm{weight}\left(m+1,0\right)=1)\wedge (\mathrm{weight}\left(m+1,k+1\right)=\mathrm{weight}\left(m,k+1\right)+\mathrm{weight}\left(m+1,k\right)+\mathrm{weight}\left(m,k\right)))))$$

Formalization. D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.weight (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2019). OEIS A323689: Gaussian generating function and square parity. URL: https://oeis.org/A323689.

Commentary.

The boundary entries are 1. Every interior entry is the sum of its west, south and southwest predecessors. All values lie in the integers.

Theorem 1.2 (Every recursive weight is odd).

$$\forall m:\mathbb{N},(\forall k:\mathbb{N},(\mathrm{Odd}\left(\mathrm{weight}\left(m,k\right)\right)))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.weight_odd (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2019). OEIS A323689: Gaussian generating function and square parity. URL: https://oeis.org/A323689.

Commentary.

Nested induction gives oddness: the three predecessor entries are odd and their sum is odd.

Definition 1.3 (The rational Gaussian kernel).

$$\forall m:\mathbb{N},(\mathrm{kernel}\left(m\right)=(X+C\left(\mathrm{Complex}.I\right){)}^m\cdot ((1+C\left(\mathrm{Complex}.I\right)\cdot X{)}^{m+1}{)}^{-1})$$

Formalization. D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.kernel (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2019). OEIS A323689: Gaussian generating function and square parity. URL: https://oeis.org/A323689.

Commentary.

The kernel is (X + C Complex.I)^m times the formal inverse of (1 + C Complex.I*X)^(m+1). The denominator has constant coefficient 1.

Theorem 1.4 (Expansion of the rational kernel).

$$\forall m:\mathbb{N},(\forall p:\mathbb{N},(\forall hp:p\ne 0,(\mathrm{expand}\left(p,hp,\mathrm{kernel}\left(m\right)\right)=((X{)}^p+C\left(\mathrm{Complex}.I\right){)}^m\cdot ((1+C\left(\mathrm{Complex}.I\right)\cdot (X{)}^p{)}^{m+1}{)}^{-1})))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.kernel_expansion (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2019). OEIS A323689: Gaussian generating function and square parity. URL: https://oeis.org/A323689.

Commentary.

Replacing X by X^p commutes with the rational expression when p is nonzero.

Theorem 1.5 (Finite coefficient extraction).

$$\forall p:\mathbb{N},(\forall N:\mathbb{N},(\forall hp:p\ne 0,(\forall f:\mathrm{PowerSeries}\left(\mathbb{C}\right),(\forall s:\mathrm{Finset}\left(\mathbb{N}\right),((\forall k:\mathbb{N},((p\cdot k=N)⟹(k\in s)))⟹(\mathrm{coeff}\left(N,\mathrm{expand}\left(p,hp,f\right)\right)=\sum _{k\in s}(\mathrm{if}(p\cdot k=N)\mathrm{then}\mathrm{coeff}\left(k,f\right)\mathrm{else}0)))))))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.expansion_coefficient (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2019). OEIS A323689: Gaussian generating function and square parity. URL: https://oeis.org/A323689.

Commentary.

A finite set containing every solution of p*k = N collects exactly the N-th coefficient of expand p hp f.

Theorem 1.6 (Finite shifted coefficient extraction).

$$\forall d:\mathbb{N},(\forall p:\mathbb{N},(\forall N:\mathbb{N},(\forall hp:p\ne 0,((d\le N)⟹(\forall f:\mathrm{PowerSeries}\left(\mathbb{C}\right),(\forall s:\mathrm{Finset}\left(\mathbb{N}\right),((\forall k:\mathbb{N},((d+p\cdot k=N)⟹(k\in s)))⟹(\mathrm{coeff}\left(N,(X{)}^d\cdot \mathrm{expand}\left(p,hp,f\right)\right)=\sum _{k\in s}(\mathrm{if}(d+p\cdot k=N)\mathrm{then}\mathrm{coeff}\left(k,f\right)\mathrm{else}0)))))))))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.shifted_expansion_coefficient (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2019). OEIS A323689: Gaussian generating function and square parity. URL: https://oeis.org/A323689.

Commentary.

For d at most N, the coefficient of X^d times expand p hp f is the sum over d+p*k = N.

Theorem 1.7 (Symmetric support and diagonal parity).

$$\forall s:\mathrm{Finset}\left(\mathbb{N}\right),(\forall P:\mathbb{N}\to \mathbb{N}\to Prop,([\mathrm{DecidableRel}\left(P\right)],(\forall m:\mathbb{N},(\forall k:\mathbb{N},(P\left(m,k\right)⟺P\left(k,m\right))))⟹(\exists z:\mathbb{Z},((\sum _{m\in s}(\sum _{k\in s}(\mathrm{if}(P\left(m,k\right))\mathrm{then}\mathrm{coeff}\left(k,\mathrm{kernel}\left(m\right)\right)\mathrm{else}0))=(z:\mathbb{C}))\wedge (\mathrm{Even}\left(z-\sum _{m\in s}(\mathrm{if}(P\left(m,m\right))\mathrm{then}\mathrm{weight}\left(m,m\right)\mathrm{else}0)\right))))))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.supported_matrix_integral (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2019). OEIS A323689: Gaussian generating function and square parity. URL: https://oeis.org/A323689.

Commentary.

On any finite set of natural indices, a symmetric decidable support selects an integer coefficient sum. Its difference from the supported integer diagonal sum is even. The coefficient identity is obtained by induction from the rational kernel; symmetry pairs all off-diagonal terms.

References

• Truth anchor: D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.expansion_coefficient
• Truth anchor: D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.kernel
• Truth anchor: D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.kernel_expansion
• Truth anchor: D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.shifted_expansion_coefficient
• Truth anchor: D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.supported_matrix_integral
• Truth anchor: D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.weight
• Truth anchor: D5/S1/Recurrence/Algebraic/HannaGaussianKernelParity.weight_odd