The canonical Gaussian probability space and its polynomial integrability. All expectations in this development are genuine Bochner integrals.

noncomputable def GaussianMomentsCounterexamples.gaussianMeasure (n : ℕ) : MeasureTheory.Measure (Fin n → ℝ)

The law of n independent standard real Gaussian coordinates.

Equations

• GaussianMomentsCounterexamples.gaussianMeasure n = MeasureTheory.Measure.pi fun (x : Fin n) => ProbabilityTheory.gaussianReal 0 1

instance GaussianMomentsCounterexamples.instIsProbabilityMeasureForallFinRealGaussianMeasure (n : ℕ) : MeasureTheory.IsProbabilityMeasure (gaussianMeasure n)

def GaussianMomentsCounterexamples.realEval {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (x : Fin n → ℝ) : ℂ

Evaluate a complex polynomial on real coordinates.

Equations

• GaussianMomentsCounterexamples.realEval P x = (MvPolynomial.eval fun (i : Fin n) => ↑(x i)) P

noncomputable def GaussianMomentsCounterexamples.expectation {n : ℕ} (P : MvPolynomial (Fin n) ℂ) : ℂ

Genuine Gaussian expectation of a complex polynomial.

Equations

• GaussianMomentsCounterexamples.expectation P = ∫ (x : Fin n → ℝ), GaussianMomentsCounterexamples.realEval P x ∂GaussianMomentsCounterexamples.gaussianMeasure n

theorem GaussianMomentsCounterexamples.integrable_real_pow (k : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ k) (ProbabilityTheory.gaussianReal 0 1)

theorem GaussianMomentsCounterexamples.integrable_complex_pow (k : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => ↑x ^ k) (ProbabilityTheory.gaussianReal 0 1)

theorem GaussianMomentsCounterexamples.realEval_monomial {n : ℕ} (d : Fin n →₀ ℕ) (c : ℂ) (x : Fin n → ℝ) : realEval ((MvPolynomial.monomial d) c) x = c * ∏ i : Fin n, ↑(x i) ^ d i

theorem GaussianMomentsCounterexamples.integrable_realEval {n : ℕ} (P : MvPolynomial (Fin n) ℂ) : MeasureTheory.Integrable (realEval P) (gaussianMeasure n)

Every complex polynomial, including every mixed power, is integrable.

def GaussianMomentsCounterexamples.GMC (n : ℕ) : Prop

The conjecture with its actual eventual-vanishing quantifiers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GaussianMomentsCounterexamples.expectation_add {n : ℕ} (P Q : MvPolynomial (Fin n) ℂ) : expectation (P + Q) = expectation P + expectation Q

@[simp]

theorem GaussianMomentsCounterexamples.expectation_C_mul {n : ℕ} (c : ℂ) (P : MvPolynomial (Fin n) ℂ) : expectation (MvPolynomial.C c * P) = c * expectation P

theorem GaussianMomentsCounterexamples.expectation_monomial {n : ℕ} (d : Fin n →₀ ℕ) (c : ℂ) : expectation ((MvPolynomial.monomial d) c) = c * ∏ i : Fin n, ∫ (x : ℝ), ↑x ^ d i ∂ProbabilityTheory.gaussianReal 0 1

Independent-coordinate factorization, with integrability established above.

@[simp]

theorem GaussianMomentsCounterexamples.expectation_zero {n : ℕ} : expectation 0 = 0

@[simp]

theorem GaussianMomentsCounterexamples.expectation_C {n : ℕ} (c : ℂ) : expectation (MvPolynomial.C c) = c

@[simp]

theorem GaussianMomentsCounterexamples.expectation_one {n : ℕ} : expectation 1 = 1

@[simp]

theorem GaussianMomentsCounterexamples.expectation_sub {n : ℕ} (P Q : MvPolynomial (Fin n) ℂ) : expectation (P - Q) = expectation P - expectation Q

@[simp]

theorem GaussianMomentsCounterexamples.expectation_smul {n : ℕ} (c : ℂ) (P : MvPolynomial (Fin n) ℂ) : expectation (c • P) = c * expectation P

theorem GaussianMomentsCounterexamples.expectation_X_pow {n : ℕ} (i : Fin n) (k : ℕ) : expectation (MvPolynomial.X i ^ k) = ∫ (x : ℝ), ↑x ^ k ∂ProbabilityTheory.gaussianReal 0 1

A single coordinate has the standard real Gaussian moments.

noncomputable def GaussianMomentsCounterexamples.expectationLinear (n : ℕ) : MvPolynomial (Fin n) ℂ →ₗ[ℂ] ℂ

The integral is a complex-linear functional on the entire polynomial ring.

Equations

• GaussianMomentsCounterexamples.expectationLinear n = { toFun := GaussianMomentsCounterexamples.expectation, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem GaussianMomentsCounterexamples.expectation_sum {n : ℕ} {ι : Type u_1} (s : Finset ι) (P : ι → MvPolynomial (Fin n) ℂ) : expectation (∑ i ∈ s, P i) = ∑ i ∈ s, expectation (P i)