Documentation

Mathlib.Probability.Moments

Moments and moment generating function #

Main definitions #

Main results #

def ProbabilityTheory.moment {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω) (p : ) (μ : MeasureTheory.Measure Ω) :

Moment of a real random variable, μ[X ^ p].

Equations
Instances For
    def ProbabilityTheory.centralMoment {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω) (p : ) (μ : MeasureTheory.Measure Ω) :

    Central moment of a real random variable, μ[(X - μ[X]) ^ p].

    Equations
    Instances For
      @[simp]
      theorem ProbabilityTheory.moment_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {p : } {μ : MeasureTheory.Measure Ω} (hp : p 0) :
      @[simp]
      theorem ProbabilityTheory.centralMoment_one' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (h_int : MeasureTheory.Integrable X μ) :
      ProbabilityTheory.centralMoment X 1 μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X xμ
      def ProbabilityTheory.mgf {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω) (μ : MeasureTheory.Measure Ω) (t : ) :

      Moment generating function of a real random variable X: fun t => μ[exp(t*X)].

      Equations
      Instances For
        def ProbabilityTheory.cgf {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω) (μ : MeasureTheory.Measure Ω) (t : ) :

        Cumulant generating function of a real random variable X: fun t => log μ[exp(t*X)].

        Equations
        Instances For
          @[simp]
          theorem ProbabilityTheory.mgf_zero_fun {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } :
          ProbabilityTheory.mgf 0 μ t = (μ Set.univ).toReal
          @[simp]
          theorem ProbabilityTheory.cgf_zero_fun {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } :
          ProbabilityTheory.cgf 0 μ t = Real.log (μ Set.univ).toReal
          @[simp]
          theorem ProbabilityTheory.mgf_zero_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {t : } :
          @[simp]
          theorem ProbabilityTheory.cgf_zero_measure {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {t : } :
          @[simp]
          theorem ProbabilityTheory.mgf_const' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } (c : ) :
          ProbabilityTheory.mgf (fun (x : Ω) => c) μ t = (μ Set.univ).toReal * Real.exp (t * c)
          theorem ProbabilityTheory.mgf_const {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } (c : ) [MeasureTheory.IsProbabilityMeasure μ] :
          ProbabilityTheory.mgf (fun (x : Ω) => c) μ t = Real.exp (t * c)
          @[simp]
          theorem ProbabilityTheory.cgf_const' {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } [MeasureTheory.IsFiniteMeasure μ] (hμ : μ 0) (c : ) :
          ProbabilityTheory.cgf (fun (x : Ω) => c) μ t = Real.log (μ Set.univ).toReal + t * c
          @[simp]
          theorem ProbabilityTheory.cgf_const {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } [MeasureTheory.IsProbabilityMeasure μ] (c : ) :
          ProbabilityTheory.cgf (fun (x : Ω) => c) μ t = t * c
          @[simp]
          theorem ProbabilityTheory.mgf_zero' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} :
          ProbabilityTheory.mgf X μ 0 = (μ Set.univ).toReal
          @[simp]
          theorem ProbabilityTheory.cgf_zero' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} :
          ProbabilityTheory.cgf X μ 0 = Real.log (μ Set.univ).toReal
          theorem ProbabilityTheory.mgf_undef {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } (hX : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
          theorem ProbabilityTheory.cgf_undef {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } (hX : ¬MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
          theorem ProbabilityTheory.mgf_nonneg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } :
          theorem ProbabilityTheory.mgf_pos' {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } (hμ : μ 0) (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
          theorem ProbabilityTheory.mgf_pos {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } [MeasureTheory.IsProbabilityMeasure μ] (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
          theorem ProbabilityTheory.mgf_neg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } :
          theorem ProbabilityTheory.cgf_neg {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } :
          theorem ProbabilityTheory.IndepFun.exp_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω} {Y : Ω} (h_indep : ProbabilityTheory.IndepFun X Y μ) (s : ) (t : ) :
          ProbabilityTheory.IndepFun (fun (ω : Ω) => Real.exp (s * X ω)) (fun (ω : Ω) => Real.exp (t * Y ω)) μ

          This is a trivial application of IndepFun.comp but it will come up frequently.

          theorem ProbabilityTheory.IndepFun.mgf_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } {X : Ω} {Y : Ω} (h_indep : ProbabilityTheory.IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (hY : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) :
          theorem ProbabilityTheory.IndepFun.cgf_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } {X : Ω} {Y : Ω} (h_indep : ProbabilityTheory.IndepFun X Y μ) (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (h_int_Y : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) :
          theorem ProbabilityTheory.aestronglyMeasurable_exp_mul_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } {X : Ω} {Y : Ω} (h_int_X : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (h_int_Y : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) :
          MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * (X + Y) ω)) μ
          theorem ProbabilityTheory.aestronglyMeasurable_exp_mul_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } {X : ιΩ} {s : Finset ι} (h_int : is, MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) :
          MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => Real.exp (t * (is, X i) ω)) μ
          theorem ProbabilityTheory.IndepFun.integrable_exp_mul_add {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } {X : Ω} {Y : Ω} (h_indep : ProbabilityTheory.IndepFun X Y μ) (h_int_X : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) (h_int_Y : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) :
          MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * (X + Y) ω)) μ
          theorem ProbabilityTheory.iIndepFun.integrable_exp_mul_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } [MeasureTheory.IsProbabilityMeasure μ] {X : ιΩ} (h_indep : ProbabilityTheory.iIndepFun (fun (i : ι) => inferInstance) X μ) (h_meas : ∀ (i : ι), Measurable (X i)) {s : Finset ι} (h_int : is, MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) :
          MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * (is, X i) ω)) μ
          theorem ProbabilityTheory.iIndepFun.mgf_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } [MeasureTheory.IsProbabilityMeasure μ] {X : ιΩ} (h_indep : ProbabilityTheory.iIndepFun (fun (i : ι) => inferInstance) X μ) (h_meas : ∀ (i : ι), Measurable (X i)) (s : Finset ι) :
          ProbabilityTheory.mgf (is, X i) μ t = is, ProbabilityTheory.mgf (X i) μ t
          theorem ProbabilityTheory.iIndepFun.cgf_sum {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {t : } [MeasureTheory.IsProbabilityMeasure μ] {X : ιΩ} (h_indep : ProbabilityTheory.iIndepFun (fun (i : ι) => inferInstance) X μ) (h_meas : ∀ (i : ι), Measurable (X i)) {s : Finset ι} (h_int : is, MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X i ω)) μ) :
          ProbabilityTheory.cgf (is, X i) μ t = is, ProbabilityTheory.cgf (X i) μ t
          theorem ProbabilityTheory.measure_ge_le_exp_mul_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } [MeasureTheory.IsFiniteMeasure μ] (ε : ) (ht : 0 t) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
          (μ {ω : Ω | ε X ω}).toReal Real.exp (-t * ε) * ProbabilityTheory.mgf X μ t

          Chernoff bound on the upper tail of a real random variable.

          theorem ProbabilityTheory.measure_le_le_exp_mul_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } [MeasureTheory.IsFiniteMeasure μ] (ε : ) (ht : t 0) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
          (μ {ω : Ω | X ω ε}).toReal Real.exp (-t * ε) * ProbabilityTheory.mgf X μ t

          Chernoff bound on the lower tail of a real random variable.

          theorem ProbabilityTheory.measure_ge_le_exp_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } [MeasureTheory.IsFiniteMeasure μ] (ε : ) (ht : 0 t) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
          (μ {ω : Ω | ε X ω}).toReal Real.exp (-t * ε + ProbabilityTheory.cgf X μ t)

          Chernoff bound on the upper tail of a real random variable.

          theorem ProbabilityTheory.measure_le_le_exp_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω} {μ : MeasureTheory.Measure Ω} {t : } [MeasureTheory.IsFiniteMeasure μ] (ε : ) (ht : t 0) (h_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) :
          (μ {ω : Ω | X ω ε}).toReal Real.exp (-t * ε + ProbabilityTheory.cgf X μ t)

          Chernoff bound on the lower tail of a real random variable.