Helly's selection theorem

StructureDistribution function#✓fully proved

A nondecreasing, right-continuous function \(F : \mathbb{R} \to \mathbb{R}\) (a Stieltjes function) is a (cumulative) distribution function if \(F(x) \to 0\) as \(x \to -\infty\) and \(F(x) \to 1\) as \(x \to +\infty\).

These are exactly the distribution functions of probability measures on \(\mathbb{R}\).

structure IsDistributionFunction (F : StieltjesFunction ℝ) : Prop where
  tendsto_atBot : Tendsto F atBot (𝓝 0)
  tendsto_atTop : Tendsto F atTop (𝓝 1)

Used by 4

Used byHelly's selection theorem · Distribution functions are at most one · Distribution functions take values in the unit interval · Distribution functions are nonnegative

TheoremDistribution functions are nonnegative#✓fully proved

If \(F\) is a distribution function on \(\mathbb{R}\), then \(0 \le F(x)\) for every \(x \in \mathbb{R}\).

theorem IsDistributionFunction.nonneg {F : StieltjesFunction ℝ}
    (hF : IsDistributionFunction F) (x : ℝ) :
    0 ≤ F x

Uses 1 · Used by 2

Statement usesDistribution function

Used byHelly's selection theorem · Distribution functions take values in the unit interval

TheoremDistribution functions are at most one#✓fully proved

If \(F\) is a distribution function on \(\mathbb{R}\), then \(F(x) \le 1\) for every \(x \in \mathbb{R}\).

theorem IsDistributionFunction.le_one {F : StieltjesFunction ℝ}
    (hF : IsDistributionFunction F) (x : ℝ) :
    F x ≤ 1

Uses 1 · Used by 2

Statement usesDistribution function

Used byHelly's selection theorem · Distribution functions take values in the unit interval

TheoremDistribution functions take values in the unit interval#✓fully proved

If \(F\) is a distribution function on \(\mathbb{R}\), then \(F(x) \in [0, 1]\) for every \(x \in \mathbb{R}\).

theorem IsDistributionFunction.mem_Icc {F : StieltjesFunction ℝ}
    (hF : IsDistributionFunction F) (x : ℝ) :
    F x ∈ Icc (0 : ℝ) 1

Uses 3

Statement usesDistribution function

Proof usesDistribution functions are at most one · Distribution functions are nonnegative

TheoremHelly's selection theorem#✓fully proved

Let \((F_n)_{n \in \mathbb{N}}\) be a sequence of distribution functions on \(\mathbb{R}\). Then there are a strictly increasing map \(\varphi : \mathbb{N} \to \mathbb{N}\) and a nondecreasing, right-continuous function \(G : \mathbb{R} \to \mathbb{R}\) such that \(F_{\varphi(k)}(x) \to G(x)\) as \(k \to \infty\) at every point \(x \in \mathbb{R}\) at which \(G\) is continuous.

The limit \(G\) need not itself be a distribution function: it may lose mass to \(\pm\infty\).

theorem helly_selection (F : ℕ → StieltjesFunction ℝ)
    (hF : ∀ n, IsDistributionFunction (F n)) :
    ∃ (φ : ℕ → ℕ) (G : StieltjesFunction ℝ),
      StrictMono φ ∧
      ∀ x, ContinuousAt (↑G) x → Tendsto (fun k => F (φ k) x) atTop (𝓝 (G x))

Uses 3

Statement usesDistribution function

Proof usesDistribution functions are at most one · Distribution functions are nonnegative

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.