Documentation

LeanPool.GaussianMomentsCounterexamples.GeneratingFunctions

Coefficientwise exponential generating functions of genuine Gaussian moments. No analytic exponential integrability or infinite-sum/integral interchange is asserted.

source
noncomputable def GaussianMomentsCounterexamples.momentEGF {n : ℕ} (P : MvPolynomial (Fin n) ℂ) :
PowerSeries ℂ

The formal exponential generating function of the Gaussian moments of a polynomial.

Equations
Instances For
    source
    noncomputable def GaussianMomentsCounterexamples.mixedMomentEGF {n : ℕ} (Q P : MvPolynomial (Fin n) ℂ) :
    PowerSeries ℂ

    The formal generating function for mixed Gaussian moments.

    Equations
    Instances For
      source
      theorem GaussianMomentsCounterexamples.momentEGF_eq_one {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (h : ∀ (m : ℕ), 1 ≤ m → expectation (P ^ m) = 0) :
      momentEGF P = 1
      source
      theorem GaussianMomentsCounterexamples.mixedMomentEGF_eq_branch {n : ℕ} (Q P : MvPolynomial (Fin n) ℂ) (h0 : expectation Q = 0) (h : ∀ (m : ℕ), 1 ≤ m → expectation (Q * P ^ m) = ↑m.factorial) :
      mixedMomentEGF Q P = branchZeta
      source
      @[simp]
      theorem GaussianMomentsCounterexamples.expectation_Q3 :
      expectation Q3 = 0
      source
      @[simp]
      theorem GaussianMomentsCounterexamples.expectation_Q4 :
      expectation Q4 = 0
      source
      theorem GaussianMomentsCounterexamples.P3_momentEGF :
      momentEGF P3 = 1

      The displayed formal identity E(exp(t P₃)) = 1.

      source
      theorem GaussianMomentsCounterexamples.P4_momentEGF :
      momentEGF P4 = 1

      The displayed formal identity E(exp(t P₄)) = 1.

      source
      theorem GaussianMomentsCounterexamples.Q3_P3_mixedMomentEGF :
      mixedMomentEGF Q3 P3 = PowerSeries.X * (1 - PowerSeries.X)⁻¹

      The displayed formal identity E(Q₃ exp(t P₃)) = t/(1-t).

      source
      theorem GaussianMomentsCounterexamples.Q4_P4_mixedMomentEGF :
      mixedMomentEGF Q4 P4 = PowerSeries.X * (1 - PowerSeries.X)⁻¹

      The displayed formal identity E(Q₄ exp(t P₄)) = t/(1-t).

      source
      theorem GaussianMomentsCounterexamples.naturalP4_discovery_correspondence :
      naturalP4 = MvPolynomial.X 0 * (MvPolynomial.aeval ![MvPolynomial.X 1, MvPolynomial.X 3]) (discoveryHPolynomial 0) + MvPolynomial.X 2 * (MvPolynomial.aeval ![MvPolynomial.X 1, MvPolynomial.X 3]) (discoveryHPolynomial 1)

      The explicit discovery vector field produces exactly the four-variable polynomial.