Documentation

Mathlib.Probability.Distributions.Gaussian

Gaussian distributions over ℝ #

We define a Gaussian measure over the reals.

Main definitions #

Main results #

noncomputable def ProbabilityTheory.gaussianPDFReal (μ : ) (v : NNReal) (x : ) :

Probability density function of the gaussian distribution with mean μ and variance v.

Equations
Instances For
    theorem ProbabilityTheory.gaussianPDFReal_def (μ : ) (v : NNReal) :
    ProbabilityTheory.gaussianPDFReal μ v = fun (x : ) => ((2 * Real.pi * v))⁻¹ * Real.exp (-(x - μ) ^ 2 / (2 * v))

    The gaussian pdf is positive when the variance is not zero.

    The gaussian pdf is nonnegative.

    The gaussian distribution pdf integrates to 1 when the variance is not zero.

    The gaussian distribution pdf integrates to 1 when the variance is not zero.

    theorem ProbabilityTheory.gaussianPDFReal_inv_mul {μ : } {v : NNReal} {c : } (hc : c 0) (x : ) :
    theorem ProbabilityTheory.gaussianPDFReal_mul {μ : } {v : NNReal} {c : } (hc : c 0) (x : ) :
    noncomputable def ProbabilityTheory.gaussianPDF (μ : ) (v : NNReal) (x : ) :

    The pdf of a Gaussian distribution on ℝ with mean μ and variance v.

    Equations
    Instances For
      @[simp]
      theorem ProbabilityTheory.lintegral_gaussianPDF_eq_one (μ : ) {v : NNReal} (h : v 0) :
      ∫⁻ (x : ), ProbabilityTheory.gaussianPDF μ v x = 1

      A Gaussian distribution on with mean μ and variance v.

      Equations
      Instances For
        theorem ProbabilityTheory.gaussianReal_of_var_ne_zero (μ : ) {v : NNReal} (hv : v 0) :
        ProbabilityTheory.gaussianReal μ v = MeasureTheory.volume.withDensity (ProbabilityTheory.gaussianPDF μ v)
        theorem ProbabilityTheory.gaussianReal_apply (μ : ) {v : NNReal} (hv : v 0) (s : Set ) :
        theorem ProbabilityTheory.gaussianReal_absolutelyContinuous (μ : ) {v : NNReal} (hv : v 0) :
        (ProbabilityTheory.gaussianReal μ v).AbsolutelyContinuous MeasureTheory.volume
        theorem ProbabilityTheory.gaussianReal_absolutelyContinuous' (μ : ) {v : NNReal} (hv : v 0) :
        MeasureTheory.volume.AbsolutelyContinuous (ProbabilityTheory.gaussianReal μ v)
        theorem ProbabilityTheory.rnDeriv_gaussianReal (μ : ) (v : NNReal) :
        (ProbabilityTheory.gaussianReal μ v).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] ProbabilityTheory.gaussianPDF μ v
        theorem MeasurableEmbedding.gaussianReal_comap_apply {μ : } {v : NNReal} (hv : v 0) {f : } (hf : MeasurableEmbedding f) {f' : } (h_deriv : ∀ (x : ), HasDerivAt f (f' x) x) {s : Set } (hs : MeasurableSet s) :
        theorem MeasurableEquiv.gaussianReal_map_symm_apply {μ : } {v : NNReal} (hv : v 0) (f : ≃ᵐ ) {f' : } (h_deriv : ∀ (x : ), HasDerivAt (f) (f' x) x) {s : Set } (hs : MeasurableSet s) :

        The map of a Gaussian distribution by addition of a constant is a Gaussian.

        The map of a Gaussian distribution by addition of a constant is a Gaussian.

        The map of a Gaussian distribution by multiplication by a constant is a Gaussian.

        The map of a Gaussian distribution by multiplication by a constant is a Gaussian.

        theorem ProbabilityTheory.gaussianReal_add_const {μ : } {v : NNReal} {Ω : Type} [MeasureTheory.MeasureSpace Ω] {X : Ω} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v) (y : ) :
        MeasureTheory.Measure.map (fun (ω : Ω) => X ω + y) MeasureTheory.volume = ProbabilityTheory.gaussianReal (μ + y) v

        If X is a real random variable with Gaussian law with mean μ and variance v, then X + y has Gaussian law with mean μ + y and variance v.

        theorem ProbabilityTheory.gaussianReal_const_add {μ : } {v : NNReal} {Ω : Type} [MeasureTheory.MeasureSpace Ω] {X : Ω} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v) (y : ) :
        MeasureTheory.Measure.map (fun (ω : Ω) => y + X ω) MeasureTheory.volume = ProbabilityTheory.gaussianReal (μ + y) v

        If X is a real random variable with Gaussian law with mean μ and variance v, then y + X has Gaussian law with mean μ + y and variance v.

        theorem ProbabilityTheory.gaussianReal_const_mul {μ : } {v : NNReal} {Ω : Type} [MeasureTheory.MeasureSpace Ω] {X : Ω} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v) (c : ) :
        MeasureTheory.Measure.map (fun (ω : Ω) => c * X ω) MeasureTheory.volume = ProbabilityTheory.gaussianReal (c * μ) (c ^ 2, * v)

        If X is a real random variable with Gaussian law with mean μ and variance v, then c * X has Gaussian law with mean c * μ and variance c^2 * v.

        theorem ProbabilityTheory.gaussianReal_mul_const {μ : } {v : NNReal} {Ω : Type} [MeasureTheory.MeasureSpace Ω] {X : Ω} (hX : MeasureTheory.Measure.map X MeasureTheory.volume = ProbabilityTheory.gaussianReal μ v) (c : ) :
        MeasureTheory.Measure.map (fun (ω : Ω) => X ω * c) MeasureTheory.volume = ProbabilityTheory.gaussianReal (c * μ) (c ^ 2, * v)

        If X is a real random variable with Gaussian law with mean μ and variance v, then X * c has Gaussian law with mean c * μ and variance c^2 * v.