Gaussian measures

Stream: new members

[jsodd]

In this topic, I've asked how do we formalise measures on R^n. Here's a more specific question which I'm trying to solve.

I am trying to formalise Gaussian measures, and decided to start from the case of R^n. A Borel measure gamma on R^n is said to be Gaussian if for every linear functional R^n -> R the induced measure gamma o l^{-1} is a Gaussian measure on R. Here's my attempt at formalising this definition:

def isGaussianReal (γ : ProbabilityMeasure ℝ) : Prop := sorry

def isGaussianFinDim (γ : ProbabilityMeasure (n → ℝ)) [BorelSpace (n → ℝ)]:=
  ∀ (l : (n → ℝ) →L[ℝ] ℝ) (h : AEMeasurable l γ), isGaussianReal (ProbabilityMeasure.map γ h)

However, assuming h : AEMeasurable l γ seems unnecessary, which brings me to the following two quesions:

1. Where did I specify that n → ℝ is endowed with the Borel sigma-algebra? Is it somehow inferred? If yes, how should I find the definition?
2. Is there a way to avoid this assumption? It's not really needed.

[jsodd]

P.S. If I remove [BorelSpace n → ℝ], nothing changes, this was just my attempt to put this assumption somewhere

[Etienne Marion]

Yes, n \to \R is automatically endowed with borel sigma algebra (see docs#Real.borelSpace and docs#Pi.borelSpace)

[Etienne Marion]

And you can use docs#Continuous.aemeasurable

[Etienne Marion]

If you want to know how an instance is synthesized, you can do

import Mathlib
variable (n : Type) [Finite n]

#synth BorelSpace (n → ℝ)