Documentation

BGW.Probability.SkorokhodRepresentationReal

Real-valued Skorokhod representation by quantiles #

The common probability space is the open unit interval with Lebesgue measure. Quantiles are characterized against the actual CDF, so their pushforward laws are the original measures. Adapted from the real quantile proof in PoissonDeclumping/Probability/Skorokhod.lean of the author's arXiv:2607.22291v1 formalization (local project, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd, Apache-2.0), to permit convergence of CDFs on a dense set, including limits with atoms. Reference: P. Billingsley, Convergence of Probability Measures, 2nd ed., 1999, proof of Theorem 6.7 (the real case by quantiles).

source
noncomputable def BGW.Probability.RealCoupling.unitProbability :
MeasureTheory.Measure ℝ

Lebesgue probability on the open unit interval.

Equations
Instances For
    source
    instance BGW.Probability.RealCoupling.instIsProbabilityMeasureRealUnitProbability :
    MeasureTheory.IsProbabilityMeasure unitProbability

    Lebesgue measure restricted to the open unit interval has total mass one.

    source
    noncomputable def BGW.Probability.RealCoupling.quantile (μ : MeasureTheory.Measure ℝ) (u : ℝ) :
    ℝ

    The lower quantile, with harmless totalization outside 0 < u < 1.

    Equations
    Instances For
      source
      theorem BGW.Probability.RealCoupling.quantile_le_iff (μ : MeasureTheory.Measure ℝ) {u x : ℝ} (hu0 : 0 < u) (hu1 : u < 1) :
      quantile μ u ≤ x ↔ u ≤ ↑(ProbabilityTheory.cdf μ) x

      Quantile/CDF equivalence, including CDF jumps.

      source
      theorem BGW.Probability.RealCoupling.quantile_monotoneOn (μ : MeasureTheory.Measure ℝ) :
      MonotoneOn (quantile μ) (Set.Ioo 0 1)

      Quantiles are monotone on their probability-parameter domain.

      source
      theorem BGW.Probability.RealCoupling.quantile_aemeasurable (μ : MeasureTheory.Measure ℝ) :
      AEMeasurable (quantile μ) unitProbability

      Quantiles are measurable for the common probability measure.

      source
      theorem BGW.Probability.RealCoupling.map_quantile (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] :
      MeasureTheory.Measure.map (quantile μ) unitProbability = μ

      The quantile transforms Lebesgue probability on (0,1) into the original real law.

      source
      theorem BGW.Probability.RealCoupling.tendsto_quantile_of_continuousWithinAt (μ : ℕ → MeasureTheory.Measure ℝ) (ν : MeasureTheory.Measure ℝ) {D : Set ℝ} (hD : Dense D) (hcdf : ∀ x ∈ D, Filter.Tendsto (fun (n : ℕ) => ↑(ProbabilityTheory.cdf (μ n)) x) Filter.atTop (nhds (↑(ProbabilityTheory.cdf ν) x))) {u : ℝ} (hu : u ∈ Set.Ioo 0 1) (hcont : ContinuousWithinAt (quantile ν) (Set.Ioo 0 1) u) :
      Filter.Tendsto (fun (n : ℕ) => quantile (μ n) u) Filter.atTop (nhds (quantile ν u))

      Pointwise CDF convergence gives quantile convergence at every continuity point of the limit quantile in the open unit interval.

      source
      theorem BGW.Probability.RealCoupling.exists_real_coupling (μ : ℕ → MeasureTheory.Measure ℝ) (ν : MeasureTheory.Measure ℝ) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] [MeasureTheory.IsProbabilityMeasure ν] {D : Set ℝ} (hD : Dense D) (hcdf : ∀ x ∈ D, Filter.Tendsto (fun (n : ℕ) => ↑(ProbabilityTheory.cdf (μ n)) x) Filter.atTop (nhds (↑(ProbabilityTheory.cdf ν) x))) :
      ∃ (X : ℕ → ℝ → ℝ) (Y : ℝ → ℝ), (∀ (n : ℕ), AEMeasurable (X n) unitProbability ∧ MeasureTheory.Measure.map (X n) unitProbability = μ n) ∧ AEMeasurable Y unitProbability ∧ MeasureTheory.Measure.map Y unitProbability = ν ∧ ∀ᵐ (u : ℝ) ∂unitProbability, Filter.Tendsto (fun (n : ℕ) => X n u) Filter.atTop (nhds (Y u))

      Real-valued Skorokhod representation on an explicit common probability space. The input CDF convergence is required only on a dense set.

      source
      theorem BGW.Probability.RealCoupling.exists_measurable_real_coupling (μ : ℕ → MeasureTheory.Measure ℝ) (ν : MeasureTheory.Measure ℝ) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] [MeasureTheory.IsProbabilityMeasure ν] {D : Set ℝ} (hD : Dense D) (hcdf : ∀ x ∈ D, Filter.Tendsto (fun (n : ℕ) => ↑(ProbabilityTheory.cdf (μ n)) x) Filter.atTop (nhds (↑(ProbabilityTheory.cdf ν) x))) :
      ∃ (X : ℕ → ℝ → ℝ) (Y : ℝ → ℝ), (∀ (n : ℕ), Measurable (X n) ∧ MeasureTheory.Measure.map (X n) unitProbability = μ n) ∧ Measurable Y ∧ MeasureTheory.Measure.map Y unitProbability = ν ∧ ∀ᵐ (u : ℝ) ∂unitProbability, Filter.Tendsto (fun (n : ℕ) => X n u) Filter.atTop (nhds (Y u))

      The same representation with globally measurable versions of every random variable.

      source
      theorem BGW.Probability.RealCoupling.exists_measurable_coupling_of_tendsto {P : ℕ → MeasureTheory.ProbabilityMeasure ℝ} {Q : MeasureTheory.ProbabilityMeasure ℝ} (h : Filter.Tendsto P Filter.atTop (nhds Q)) :
      ∃ (X : ℕ → ℝ → ℝ) (Y : ℝ → ℝ), (∀ (n : ℕ), Measurable (X n) ∧ MeasureTheory.Measure.map (X n) unitProbability = ↑(P n)) ∧ Measurable Y ∧ MeasureTheory.Measure.map Y unitProbability = ↑Q ∧ ∀ᵐ (u : ℝ) ∂unitProbability, Filter.Tendsto (fun (n : ℕ) => X n u) Filter.atTop (nhds (Y u))

      Weak convergence of real probability laws admits measurable almost surely convergent versions on the real line equipped with Lebesgue measure restricted to (0,1).