Documentation

Mathlib.Probability.Kernel.Disintegration.CondCdf

Conditional cumulative distribution function #

Given ρ : Measure (α × ℝ), we define the conditional cumulative distribution function (conditional cdf) of ρ. It is a function condCDF ρ : α → ℝ → ℝ such that if ρ is a finite measure, then for all a : α condCDF ρ a is monotone and right-continuous with limit 0 at -∞ and limit 1 at +∞, and such that for all x : ℝ, a ↦ condCDF ρ a x is measurable. For all x : ℝ and measurable set s, that function satisfies ∫⁻ a in s, ennreal.of_real (condCDF ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x).

condCDF is build from the more general tools about kernel CDFs developed in the file Probability.Kernel.Disintegration.CdfToKernel. In that file, we build a function α × β → StieltjesFunction (which is α × β → ℝ → ℝ with additional properties) from a function α × β → ℚ → ℝ. The restriction to allows to prove some properties like measurability more easily. Here we apply that construction to the case β = Unit and then drop β to build condCDF : α → StieltjesFunction.

Main definitions #

Main statements #

noncomputable def MeasureTheory.Measure.IicSnd {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) :

Measure on α such that for a measurable set s, ρ.IicSnd r s = ρ (s ×ˢ Iic r).

Equations
Instances For
    theorem MeasureTheory.Measure.IicSnd_apply {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) {s : Set α} (hs : MeasurableSet s) :
    (ρ.IicSnd r) s = ρ (s ×ˢ Set.Iic r)
    theorem MeasureTheory.Measure.IicSnd_univ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) :
    (ρ.IicSnd r) Set.univ = ρ (Set.univ ×ˢ Set.Iic r)
    theorem MeasureTheory.Measure.IicSnd_mono {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) {r : } {r' : } (h_le : r r') :
    ρ.IicSnd r ρ.IicSnd r'
    theorem MeasureTheory.Measure.IicSnd_le_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) :
    ρ.IicSnd r ρ.fst
    theorem MeasureTheory.Measure.IicSnd_ac_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) :
    (ρ.IicSnd r).AbsolutelyContinuous ρ.fst
    theorem MeasureTheory.Measure.iInf_IicSnd_gt {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (t : ) {s : Set α} (hs : MeasurableSet s) [MeasureTheory.IsFiniteMeasure ρ] :
    ⨅ (r : { r' : // t < r' }), (ρ.IicSnd r) s = (ρ.IicSnd t) s
    theorem MeasureTheory.Measure.tendsto_IicSnd_atTop {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) {s : Set α} (hs : MeasurableSet s) :
    Filter.Tendsto (fun (r : ) => (ρ.IicSnd r) s) Filter.atTop (nhds (ρ.fst s))
    theorem MeasureTheory.Measure.tendsto_IicSnd_atBot {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) [MeasureTheory.IsFiniteMeasure ρ] {s : Set α} (hs : MeasurableSet s) :
    Filter.Tendsto (fun (r : ) => (ρ.IicSnd r) s) Filter.atBot (nhds 0)

    Auxiliary definitions #

    We build towards the definition of ProbabilityTheory.condCDF. We first define ProbabilityTheory.preCDF, a function defined on α × ℚ with the properties of a cdf almost everywhere.

    noncomputable def ProbabilityTheory.preCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) :
    αENNReal

    preCDF is the Radon-Nikodym derivative of ρ.IicSnd with respect to ρ.fst at each r : ℚ. This function ℚ → α → ℝ≥0∞ is such that for almost all a : α, the function ℚ → ℝ≥0∞ satisfies the properties of a cdf (monotone with limit 0 at -∞ and 1 at +∞, right-continuous).

    We define this function on and not because is countable, which allows us to prove properties of the form ∀ᵐ a ∂ρ.fst, ∀ q, P (preCDF q a), instead of the weaker ∀ q, ∀ᵐ a ∂ρ.fst, P (preCDF q a).

    Equations
    Instances For
      theorem ProbabilityTheory.measurable_preCDF' {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × )} :
      Measurable fun (a : α) (r : ) => (ProbabilityTheory.preCDF ρ r a).toReal
      theorem ProbabilityTheory.withDensity_preCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) [MeasureTheory.IsFiniteMeasure ρ] :
      ρ.fst.withDensity (ProbabilityTheory.preCDF ρ r) = ρ.IicSnd r
      theorem ProbabilityTheory.set_lintegral_preCDF_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) {s : Set α} (hs : MeasurableSet s) [MeasureTheory.IsFiniteMeasure ρ] :
      ∫⁻ (x : α) in s, ProbabilityTheory.preCDF ρ r xρ.fst = (ρ.IicSnd r) s
      theorem ProbabilityTheory.lintegral_preCDF_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) [MeasureTheory.IsFiniteMeasure ρ] :
      ∫⁻ (x : α), ProbabilityTheory.preCDF ρ r xρ.fst = (ρ.IicSnd r) Set.univ
      theorem ProbabilityTheory.monotone_preCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) [MeasureTheory.IsFiniteMeasure ρ] :
      ∀ᵐ (a : α) ∂ρ.fst, Monotone fun (r : ) => ProbabilityTheory.preCDF ρ r a
      theorem ProbabilityTheory.preCDF_le_one {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) [MeasureTheory.IsFiniteMeasure ρ] :
      ∀ᵐ (a : α) ∂ρ.fst, ∀ (r : ), ProbabilityTheory.preCDF ρ r a 1
      theorem ProbabilityTheory.setIntegral_preCDF_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) {s : Set α} (hs : MeasurableSet s) [MeasureTheory.IsFiniteMeasure ρ] :
      ∫ (x : α) in s, (ProbabilityTheory.preCDF ρ r x).toRealρ.fst = ((ρ.IicSnd r) s).toReal
      @[deprecated ProbabilityTheory.setIntegral_preCDF_fst]
      theorem ProbabilityTheory.set_integral_preCDF_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) {s : Set α} (hs : MeasurableSet s) [MeasureTheory.IsFiniteMeasure ρ] :
      ∫ (x : α) in s, (ProbabilityTheory.preCDF ρ r x).toRealρ.fst = ((ρ.IicSnd r) s).toReal

      Alias of ProbabilityTheory.setIntegral_preCDF_fst.

      theorem ProbabilityTheory.integral_preCDF_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (r : ) [MeasureTheory.IsFiniteMeasure ρ] :
      ∫ (x : α), (ProbabilityTheory.preCDF ρ r x).toRealρ.fst = ((ρ.IicSnd r) Set.univ).toReal

      Conditional cdf #

      noncomputable def ProbabilityTheory.condCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (a : α) :

      Conditional cdf of the measure given the value on α, as a Stieltjes function.

      Equations
      Instances For
        theorem ProbabilityTheory.condCDF_nonneg {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (a : α) (r : ) :

        The conditional cdf is non-negative for all a : α.

        theorem ProbabilityTheory.condCDF_le_one {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (a : α) (x : ) :

        The conditional cdf is lower or equal to 1 for all a : α.

        theorem ProbabilityTheory.tendsto_condCDF_atBot {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (a : α) :
        Filter.Tendsto ((ProbabilityTheory.condCDF ρ a)) Filter.atBot (nhds 0)

        The conditional cdf tends to 0 at -∞ for all a : α.

        theorem ProbabilityTheory.tendsto_condCDF_atTop {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (a : α) :
        Filter.Tendsto ((ProbabilityTheory.condCDF ρ a)) Filter.atTop (nhds 1)

        The conditional cdf tends to 1 at +∞ for all a : α.

        theorem ProbabilityTheory.condCDF_ae_eq {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) [MeasureTheory.IsFiniteMeasure ρ] (r : ) :
        (fun (a : α) => (ProbabilityTheory.condCDF ρ a) r) =ᵐ[ρ.fst] fun (a : α) => (ProbabilityTheory.preCDF ρ r a).toReal
        theorem ProbabilityTheory.measurable_condCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (x : ) :
        Measurable fun (a : α) => (ProbabilityTheory.condCDF ρ a) x

        The conditional cdf is a measurable function of a : α for all x : ℝ.

        The conditional cdf is a strongly measurable function of a : α for all x : ℝ.

        theorem ProbabilityTheory.set_lintegral_condCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) [MeasureTheory.IsFiniteMeasure ρ] (x : ) {s : Set α} (hs : MeasurableSet s) :
        ∫⁻ (a : α) in s, ENNReal.ofReal ((ProbabilityTheory.condCDF ρ a) x)ρ.fst = ρ (s ×ˢ Set.Iic x)
        theorem ProbabilityTheory.lintegral_condCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) [MeasureTheory.IsFiniteMeasure ρ] (x : ) :
        ∫⁻ (a : α), ENNReal.ofReal ((ProbabilityTheory.condCDF ρ a) x)ρ.fst = ρ (Set.univ ×ˢ Set.Iic x)
        theorem ProbabilityTheory.setIntegral_condCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) [MeasureTheory.IsFiniteMeasure ρ] (x : ) {s : Set α} (hs : MeasurableSet s) :
        ∫ (a : α) in s, (ProbabilityTheory.condCDF ρ a) xρ.fst = (ρ (s ×ˢ Set.Iic x)).toReal
        @[deprecated ProbabilityTheory.setIntegral_condCDF]
        theorem ProbabilityTheory.set_integral_condCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) [MeasureTheory.IsFiniteMeasure ρ] (x : ) {s : Set α} (hs : MeasurableSet s) :
        ∫ (a : α) in s, (ProbabilityTheory.condCDF ρ a) xρ.fst = (ρ (s ×ˢ Set.Iic x)).toReal

        Alias of ProbabilityTheory.setIntegral_condCDF.

        theorem ProbabilityTheory.integral_condCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) [MeasureTheory.IsFiniteMeasure ρ] (x : ) :
        ∫ (a : α), (ProbabilityTheory.condCDF ρ a) xρ.fst = (ρ (Set.univ ×ˢ Set.Iic x)).toReal
        theorem ProbabilityTheory.measure_condCDF_univ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × )) (a : α) :
        (ProbabilityTheory.condCDF ρ a).measure Set.univ = 1

        The function a ↦ (condCDF ρ a).measure is measurable.