Normalized complex Gaussian contractions, derived from real Gaussian Stein identities.

noncomputable def GaussianMomentsCounterexamples.derivZ {n : ℕ} (i j : Fin n) : Derivation ℂ (MvPolynomial (Fin n) ℂ) (MvPolynomial (Fin n) ℂ)

Differentiation with respect to Z in the invertible (W,Z) coordinates.

Equations

• GaussianMomentsCounterexamples.derivZ i j = GaussianMomentsCounterexamples.normalization • (MvPolynomial.pderiv i - Complex.I • MvPolynomial.pderiv j)

noncomputable def GaussianMomentsCounterexamples.derivW {n : ℕ} (i j : Fin n) : Derivation ℂ (MvPolynomial (Fin n) ℂ) (MvPolynomial (Fin n) ℂ)

Differentiation with respect to W in the invertible (W,Z) coordinates.

Equations

• GaussianMomentsCounterexamples.derivW i j = GaussianMomentsCounterexamples.normalization • (MvPolynomial.pderiv i + Complex.I • MvPolynomial.pderiv j)

theorem GaussianMomentsCounterexamples.expectation_normalizedW_mul {n : ℕ} (i j : Fin n) (P : MvPolynomial (Fin n) ℂ) : expectation (normalizedW i j * P) = expectation ((derivZ i j) P)

theorem GaussianMomentsCounterexamples.expectation_normalizedZ_mul {n : ℕ} (i j : Fin n) (P : MvPolynomial (Fin n) ℂ) : expectation (normalizedZ i j * P) = expectation ((derivW i j) P)

@[simp]

theorem GaussianMomentsCounterexamples.derivZ_normalizedW {n : ℕ} {i j : Fin n} (hij : i ≠ j) : (derivZ i j) (normalizedW i j) = 0

@[simp]

theorem GaussianMomentsCounterexamples.derivZ_normalizedZ {n : ℕ} {i j : Fin n} (hij : i ≠ j) : (derivZ i j) (normalizedZ i j) = 1

@[simp]

theorem GaussianMomentsCounterexamples.derivW_normalizedZ {n : ℕ} {i j : Fin n} (hij : i ≠ j) : (derivW i j) (normalizedZ i j) = 0

@[simp]

theorem GaussianMomentsCounterexamples.derivW_normalizedW {n : ℕ} {i j : Fin n} (hij : i ≠ j) : (derivW i j) (normalizedW i j) = 1

theorem GaussianMomentsCounterexamples.expectation_pair_mul {n : ℕ} {i j : Fin n} (hij : i ≠ j) (a b : ℕ) (R : MvPolynomial (Fin n) ℂ) (hRZ : (derivZ i j) R = 0) (hRW : (derivW i j) R = 0) : expectation (normalizedW i j ^ a * normalizedZ i j ^ b * R) = (if a = b then ↑a.factorial else 0) * expectation R

Balanced contractions, allowing any residual polynomial independent of this pair. The two derivative hypotheses express independence of the polynomial coordinates, not moment assumptions.

theorem GaussianMomentsCounterexamples.expectation_pair {n : ℕ} {i j : Fin n} (hij : i ≠ j) (a b : ℕ) : expectation (normalizedW i j ^ a * normalizedZ i j ^ b) = if a = b then ↑a.factorial else 0

The manuscript's normalized complex Gaussian contraction in any distinct pair.