Isserlis' theorem: analytic reduction

Mathlib already identifies mixed moments with iterated Fréchet derivatives of a characteristic function. For a centered Gaussian measure its characteristic function is the exponential of the negative covariance quadratic form. This file packages those two facts in the exact form needed for the finite-dimensional Isserlis induction.

The remaining algebraic step is to differentiate that quadratic exponential and identify the result with wickPairingSum; keeping it separate makes the probabilistic transport and the finite pairing induction independently auditable.

theorem Anderson4D.gaussian_memLp_id {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ] (n : ℕ) : MeasureTheory.MemLp id (↑n) μ

A Gaussian measure has moments of every finite order, in the precise form expected by the characteristic-function differentiation theorem.

theorem Anderson4D.iteratedFDeriv_charFun_gaussian_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ] (n : ℕ) (x : Fin n → E) : (iteratedFDeriv ℝ n (MeasureTheory.charFun μ) 0) x = Complex.I ^ n * ↑(∫ (y : E), ∏ i : Fin n, inner ℝ y (x i) ∂μ)

Mixed inner-product moments are the iterated Fréchet derivatives of the Gaussian characteristic function at the origin.

theorem Anderson4D.charFun_centeredGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ] (hμ : ∫ (y : E), y ∂μ = 0) (t : E) : MeasureTheory.charFun μ t = Complex.exp (-↑(((ProbabilityTheory.covarianceBilin μ) t) t) / 2)

Characteristic function of a centered Gaussian measure, written only in terms of its covariance bilinear form.

theorem Anderson4D.iteratedFDeriv_covarianceExp_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ] (hμ : ∫ (y : E), y ∂μ = 0) (n : ℕ) (x : Fin n → E) : (iteratedFDeriv ℝ n (fun (t : E) => Complex.exp (-↑(((ProbabilityTheory.covarianceBilin μ) t) t) / 2)) 0) x = Complex.I ^ n * ↑(∫ (y : E), ∏ i : Fin n, inner ℝ y (x i) ∂μ)

Exact analytic reduction of Isserlis: the mixed moment is obtained by differentiating the exponential covariance quadratic form. No moment or measurability hypothesis remains beyond Gaussianity.