Derivatives of exponential covariance quadratics

This file closes the analytic-combinatorial step in Isserlis' theorem. We differentiate a symmetric continuous quadratic form by directional derivatives, prove the exact Leibniz rule for a linear factor, and identify the resulting recursion with wickPairingList.

def Anderson4D.directionalFDerivList {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℂ) : List E → E → ℂ

Iterated directional derivatives, with the head of the list applied outermost. This orientation agrees with iteratedFDeriv_succ_apply_left.

Equations

• Anderson4D.directionalFDerivList f [] x✝ = f x✝
• Anderson4D.directionalFDerivList f (x_2 :: xs) x✝ = (fderiv ℝ (Anderson4D.directionalFDerivList f xs) x✝) x_2

@[simp]

theorem Anderson4D.directionalFDerivList_nil {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℂ) : directionalFDerivList f [] = f

@[simp]

theorem Anderson4D.directionalFDerivList_cons {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℂ) (x : E) (xs : List E) : directionalFDerivList f (x :: xs) = fun (t : E) => (fderiv ℝ (directionalFDerivList f xs) t) x

theorem Anderson4D.directionalFDerivList_append {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℂ) (xs ys : List E) : directionalFDerivList f (xs ++ ys) = directionalFDerivList (directionalFDerivList f ys) xs

Splitting a list of directions splits the corresponding derivative iteration, with the right-hand block differentiated first.

theorem Anderson4D.directionalFDerivList_eq_iteratedFDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℂ) (hf : ContDiff ℝ ⊤ f) (xs : List E) (t : E) : directionalFDerivList f xs t = (iteratedFDeriv ℝ xs.length f t) xs.get

The list presentation is exactly the standard iterated Fréchet derivative, evaluated on the list entries in their given order.

theorem Anderson4D.directionalFDerivList_ofFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℂ) (hf : ContDiff ℝ ⊤ f) {n : ℕ} (v : Fin n → E) (t : E) : directionalFDerivList f (List.ofFn v) t = (iteratedFDeriv ℝ n f t) v

Vector-indexed specialization of directionalFDerivList_eq_iteratedFDeriv.

theorem Anderson4D.directionalFDerivList_cons_rotate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℂ) (hf : ContDiff ℝ ⊤ f) (x : E) (xs : List E) (t : E) : directionalFDerivList f (x :: xs) t = directionalFDerivList f (xs ++ [x]) t

Symmetry of smooth iterated derivatives, specialized to moving the head direction to the end of a list.

theorem Anderson4D.directionalFDerivList_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℂ) (hf : ContDiff ℝ ⊤ f) (xs : List E) : ContDiff ℝ ⊤ (directionalFDerivList f xs)

Smoothness is preserved by taking any fixed finite list of directional derivatives.

theorem Anderson4D.directionalFDerivList_linear_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : E →L[ℝ] ℂ) (f : E → ℂ) (hf : ContDiff ℝ ⊤ f) (xs : List E) (t : E) : directionalFDerivList (fun (y : E) => L y * f y) xs t = L t * directionalFDerivList f xs t + ∑ j : Fin xs.length, L (xs.get j) * directionalFDerivList f (xs.eraseIdx ↑j) t

Exact higher Leibniz rule when one factor is continuous linear. Since the linear factor has no derivatives above order one, the sum records the unique direction that differentiates it.

noncomputable def Anderson4D.covarianceQuadratic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) (t : E) : ℝ

The real quadratic exponent associated with a continuous bilinear form.

Equations

• Anderson4D.covarianceQuadratic B t = -(B t) t / 2

noncomputable def Anderson4D.covarianceQuadraticExp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) (t : E) : ℂ

The complex exponential of covarianceQuadratic.

Equations

• Anderson4D.covarianceQuadraticExp B t = Complex.exp ↑(Anderson4D.covarianceQuadratic B t)

theorem Anderson4D.covarianceQuadratic_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) : ContDiff ℝ ⊤ (covarianceQuadratic B)

theorem Anderson4D.covarianceQuadraticExp_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) : ContDiff ℝ ⊤ (covarianceQuadraticExp B)

theorem Anderson4D.fderiv_covarianceQuadratic_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) (hB : ∀ (u v : E), (B u) v = (B v) u) (t x : E) : (fderiv ℝ (covarianceQuadratic B) t) x = -(B t) x

For a symmetric bilinear form, the derivative of t ↦ -B(t,t)/2 in direction x is -B(t,x).

noncomputable def Anderson4D.negCovarianceDirection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) (x : E) : E →L[ℝ] ℂ

The complex continuous linear form t ↦ -B(t,x).

Equations

• Anderson4D.negCovarianceDirection B x = -Complex.ofRealCLM ∘SL B.flip x

@[simp]

theorem Anderson4D.negCovarianceDirection_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) (x t : E) : (negCovarianceDirection B x) t = -↑((B t) x)

theorem Anderson4D.fderiv_covarianceQuadraticExp_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) (hB : ∀ (u v : E), (B u) v = (B v) u) (t x : E) : (fderiv ℝ (covarianceQuadraticExp B) t) x = (negCovarianceDirection B x) t * covarianceQuadraticExp B t

First derivative of the covariance quadratic exponential.

theorem Anderson4D.directionalFDerivList_covarianceQuadraticExp_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) (hB : ∀ (u v : E), (B u) v = (B v) u) (xs : List E) : directionalFDerivList (covarianceQuadraticExp B) xs 0 = ↑(wickPairingList (fun (u v : E) => -(B u) v) xs)

Directional derivatives of the quadratic exponential satisfy exactly the recursive Wick pairing formula, with covariance -B.

theorem Anderson4D.wickPairingList_map {α : Type u_2} {β : Type u_3} (C : β → β → ℝ) (f : α → β) (xs : List α) : wickPairingList C (List.map f xs) = wickPairingList (fun (i j : α) => C (f i) (f j)) xs

Recursive Wick sums commute with relabeling a list.

theorem Anderson4D.iteratedFDeriv_covarianceQuadraticExp_zero_eq_wick {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) (hB : ∀ (u v : E), (B u) v = (B v) u) (n : ℕ) (x : Fin n → E) : (iteratedFDeriv ℝ n (covarianceQuadraticExp B) 0) x = ↑(wickPairingSum fun (i j : Fin n) => -(B (x i)) (x j))

The exact iterated Fréchet derivative at zero, in the project's wickPairingSum presentation.

theorem Anderson4D.wickPairingList_scale_even {α : Type u_2} (a : ℝ) (C : α → α → ℝ) (q : ℕ) (xs : List α) : xs.length = 2 * q → wickPairingList (fun (i j : α) => a * C i j) xs = a ^ q * wickPairingList C xs

Scaling every covariance entry by a scales a full pairing on 2q labels by a^q.

theorem Anderson4D.wickPairingSum_neg_even (q : ℕ) (C : Fin (2 * q) → Fin (2 * q) → ℝ) : (wickPairingSum fun (i j : Fin (2 * q)) => -C i j) = (-1) ^ q * wickPairingSum C

Negating covariance contributes one minus sign per pair.

theorem Anderson4D.iteratedFDeriv_covarianceExp_even_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) (hB : ∀ (u v : E), (B u) v = (B v) u) (q : ℕ) (x : Fin (2 * q) → E) : (iteratedFDeriv ℝ (2 * q) (fun (t : E) => Complex.exp (-↑((B t) t) / 2)) 0) x = (-1) ^ q * ↑(wickPairingSum fun (i j : Fin (2 * q)) => (B (x i)) (x j))

Even-order derivative of the exact quadratic exponential appearing in the characteristic-function formula.

theorem Anderson4D.iteratedFDeriv_covarianceExp_odd_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] ℝ) (hB : ∀ (u v : E), (B u) v = (B v) u) (q : ℕ) (x : Fin (2 * q + 1) → E) : (iteratedFDeriv ℝ (2 * q + 1) (fun (t : E) => Complex.exp (-↑((B t) t) / 2)) 0) x = 0

Odd-order derivatives vanish.

theorem Anderson4D.centeredGaussian_mixedMoment_eq_wickPairingSum {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] [SecondCountableTopology H] (μ : MeasureTheory.Measure H) [ProbabilityTheory.IsGaussian μ] (hμ : ∫ (y : H), y ∂μ = 0) (q : ℕ) (x : Fin (2 * q) → H) : ∫ (y : H), ∏ i : Fin (2 * q), inner ℝ y (x i) ∂μ = wickPairingSum fun (i j : Fin (2 * q)) => ((ProbabilityTheory.covarianceBilin μ) (x i)) (x j)

Isserlis' theorem, even case. Mixed moments of a centered Gaussian measure are the sum of covariance products over all labeled full pairings.

theorem Anderson4D.centeredGaussian_mixedMoment_odd_eq_zero {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] [SecondCountableTopology H] (μ : MeasureTheory.Measure H) [ProbabilityTheory.IsGaussian μ] (hμ : ∫ (y : H), y ∂μ = 0) (q : ℕ) (x : Fin (2 * q + 1) → H) : ∫ (y : H), ∏ i : Fin (2 * q + 1), inner ℝ y (x i) ∂μ = 0

Isserlis' theorem, odd case. Every centered Gaussian mixed moment of odd total degree vanishes.