Standard Gaussian

Stream: Brownian motion

[Peter Pfaffelhuber]

I am making my way through the Gaussian measures, not very productive yet. Here is a question. We have:

noncomputable
def stdGaussian : Measure E :=
  (Measure.pi (fun _ : Fin (Module.finrank ℝ E) ↦ gaussianReal 0 1)).map
    (fun x ↦ ∑ i, x i • stdOrthonormalBasis ℝ E i)

As it stands, the stdGaussian depends on which stdOrthonormalBasis one chooses, right?
The same applies to variance_dual_stdGaussian, where the right hand side has a basis, which must be chosen first.
It should be true that

lemma stdGaussian_iff (d : ℕ) : stdGaussian (E := (EuclideanSpace ℝ (Fin d))) =
    (Measure.pi (fun _ : Fin d ↦ gaussianReal 0 1)) := by
  sorry

although this requires to prove first that the left hand side does not depend on the chosen basis...

For me, stdGaussian should either use a basis-free definition (e.g. using the norm in the vector space and the corresponding norm on its dual), or be restricted to the case of Euclidean space.

What do you think?

[Peter Pfaffelhuber]

Maybe something like

noncomputable
def IsStdGaussian' (μ : Measure E): Prop := ∀ (L : E →L[ℝ] ℝ), μ.map L =
  gaussianReal 0 (‖L‖^2).toNNReal

[Etienne Marion]

I think things are fine as they are. The key to prove equality I think is to compute the characteristic function, which does not depend on the basis. I did the computation in #68 (it's charFun_stdGaussian in MultivariateGaussian.lean.)

[Etienne Marion]

This works in #68 after charFun_stdGaussian.

lemma charFun_pi {ι : Type*} [Fintype ι] {E : ι → Type*} {mE : ∀ i, MeasurableSpace (E i)}
    [∀ i, NormedAddCommGroup (E i)] [∀ i, InnerProductSpace ℝ (E i)] (μ : (i : ι) → Measure (E i))
    [∀ i, IsProbabilityMeasure (μ i)] (t : PiLp 2 E) :
    charFun (E := PiLp 2 E) (Measure.pi μ) t = ∏ i, charFun (μ i) (t i) := by
  simp_rw [charFun, PiLp.inner_apply, Complex.ofReal_sum, Finset.sum_mul, Complex.exp_sum,
    PiLp, WithLp]
  rw [integral_fintype_prod_eq_prod (f := fun i x ↦ Complex.exp (⟪x, t i⟫ * Complex.I))]

lemma stdGaussian_iff (d : ℕ) : stdGaussian (EuclideanSpace ℝ (Fin d)) =
    (Measure.pi (fun _ : Fin d ↦ gaussianReal 0 1)) := by
  have : IsFiniteMeasure (Measure.pi fun _ : Fin d ↦ gaussianReal 0 1) := inferInstance
  have : ∀ (t : EuclideanSpace ℝ (Fin d)), ‖t‖ ^ 2 = ∑ i, (t i) ^ 2 := by -- missing lemma
    intro t
    rw [EuclideanSpace.norm_eq, Real.sq_sqrt]
    · congr with i
      simp
    positivity
  apply Measure.ext_of_charFun
  ext t
  simp_rw [charFun_stdGaussian, charFun_pi, charFun_gaussianReal, ← Complex.exp_sum,
    ← Complex.ofReal_pow, this t]
  simp [Finset.sum_div, neg_div]

[David Ledvinka]

I agree in principal that the definition should be basis free.

[Rémy Degenne]

I don't see the issue with the definition of stdGaussian E. It is building a measure on E, and it happens to use a basis in order to do so, but the measure we get does not depend on the basis (because its characteristic function does not).
The IsStdGaussian' of Peter is the property of being a standard Gaussian, and this is different from stdGaussian which actually builds a measure.

[Notification Bot]

A message was moved here from #Brownian motion > Tasks and claims by Rémy Degenne.

[Peter Pfaffelhuber]

Usually, when you define something, you should take care of existence and uniqueness. When you use a basis in the definition, you have the problem of uniqueness (i.e. you should show later that the definition from before does not depend on the choice of the basis). My definition of the property IsStdGaussian, on the other hand, has the problem of existence, since it is not clear per se if the property can be satisfied at all.

When I go though Hairers notes, he does not have the corresponding concept of stdGaussian as it is now in the project. Rather, he only uses this on $\mathbb R^d$ as far as I can see. This avoids both complications from above, since it is only a product measure of existing measures (therefore unique since the product measure is unique).

I am not saying that the code has errors, but it feels like the wrong definition. What do we actually gain from having stdGaussian on a general finite dimensional space (with the compliactions from above), rather than on $\mathbb R^d$?

[Sébastien Gouëzel]

Having something defined using some arbitrary basis, and then another theorem showing that it does not depend on the basis, is a pretty common construction in mathlib (used for instance to define the determinant of a linear map on a finite-dimensional vector space, or the Lebesgue measure on an inner product space). And it works very well in practice!

[Peter Pfaffelhuber]

Ok, I see.
Is there a guideline when or when not to avoid noncomputable defs? As it stands, as far as I can see, there is no way to avoid this noncomputable definition for stdGaussian, but a definition of a standard Gaussian on $\mathbb R^d$ would be computable. (As I understand, a determinant of a linear map on a finite-dimensional vector space is noncomputable as well.)

[Rémy Degenne]

For the project I think $\mathbb{R}^d$ would be enough. I defined it on a finite dimensional space because from experience there always comes a time when you actually want to use your object on a type that is not exactly of the form $\mathbb{R}^d$, so it would be more future-proof.
For other definitions it's often for product spaces or subtypes. Here I don't know what may come up in the future, but say for example that one wants to define a standard Gaussian on a subspace.

Anyway, with the lemma proved by Etienne above, on $\mathbb{R}^d$ using that definition or the product does not change much.

[Rémy Degenne]

I expect pretty much everything in the project to be noncomputable, and to me that does not matter. We are using real numbers, so we won't be able to compute anything.

[Peter Pfaffelhuber]

Good point. However,

def realNumber (x : ℝ) := x

does not need to be labelled noncomputable (for some reason I don't understand).
Using what Etienne showed, we should also show that an orthogonal map of a stdGaussian is a stdGaussian.