structure IsDistributionFunction (F : ℝ → ℝ) : Prop

A real function F : ℝ → ℝ is a (cumulative) distribution function if it is monotone non-decreasing, right-continuous, tends to 0 at -∞, and tends to 1 at +∞. These are exactly the distribution functions of probability measures on ℝ.

• mono : Monotone F
• right_continuous (x : ℝ) : ContinuousWithinAt F (Set.Ici x) x
• tendsto_atBot : Filter.Tendsto F Filter.atBot (nhds 0)
• tendsto_atTop : Filter.Tendsto F Filter.atTop (nhds 1)

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

A distribution function is non-negative: 0 ≤ F x for all x ∈ ℝ.

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

A distribution function is bounded above by 1: F x ≤ 1 for all x ∈ ℝ.

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

For any distribution function F and any x ∈ ℝ, F x lies in the unit interval [0, 1].

structure HellySelection.MonotoneRightContinuous : Type

A bundled monotone, right-continuous real function ℝ → ℝ. This is the natural class of subsequential limits arising in Helly's selection theorem.

• toFun : ℝ → ℝ
• mono' : Monotone self.toFun
• right_continuous' (x : ℝ) : ContinuousWithinAt self.toFun (Set.Ici x) x

@[implicit_reducible]

instance HellySelection.MonotoneRightContinuous.instCoeFun : CoeFun MonotoneRightContinuous fun (x : MonotoneRightContinuous) => ℝ → ℝ

Coercion allowing a MonotoneRightContinuous to be applied as a function ℝ → ℝ.

noncomputable def HellySelection.ofMonotone (f : ℝ → ℝ) (hf : Monotone f) : MonotoneRightContinuous

Given any monotone function f : ℝ → ℝ, the right-limit rightLim f is monotone and right-continuous, yielding a canonical MonotoneRightContinuous.

theorem sSup_image_rat_eq (g : ℚ → ℝ) (hg_mono : ∀ (q₁ q₂ : ℚ), q₁ ≤ q₂ → g q₁ ≤ g q₂) (hg_bdd : ∀ (q : ℚ), 0 ≤ g q ∧ g q ≤ 1) (q : ℚ) : sSup (g '' {r : ℚ | ↑r ≤ ↑q}) = g q

For a monotone, [0, 1]-valued function g : ℚ → ℝ, the supremum of g over all rationals r ≤ q equals g q. This is the key bookkeeping step in the proof of Helly's selection theorem, used to define the candidate limit on ℝ from values on ℚ.

theorem helly_selection (F : ℕ → ℝ → ℝ) (hF : ∀ (n : ℕ), IsDistributionFunction (F n)) : ∃ (φ : ℕ → ℕ) (G : HellySelection.MonotoneRightContinuous), StrictMono φ ∧ ∀ (x : ℝ), ContinuousAt G.toFun x → Filter.Tendsto (fun (k : ℕ) => F (φ k) x) Filter.atTop (nhds (G.toFun x))

Helly's selection theorem. Every sequence F : ℕ → ℝ → ℝ of distribution functions has a subsequence F ∘ φ that converges pointwise to a monotone, right-continuous function G : ℝ → ℝ at every continuity point of G. The limit G need not itself be a distribution function (it may lose mass to ±∞), but it is always monotone and right-continuous.