Documentation

Verification.GaussianDifference

← Mathematical handbook

Stability of centered Gaussian differences #

The characteristic function proves that the difference of two independent copies, divided by sqrt(2), has the original law. No density assumption is needed, so singular covariance matrices are included.

source
noncomputable def Verification.gaussianDifference :
EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) →L[ℝ] EuclideanSpace ℝ (Fin 2)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Verification.gaussianDifference_apply (p : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2)) :
    gaussianDifference p = (√2)⁻¹ • (p.1 - p.2)
    source
    theorem Verification.map_gaussianDifference (r : ℝ) :
    have μ := ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r); MeasureTheory.Measure.map (⇑gaussianDifference) (μ.prod μ) = μ