AcceptedDefinition

Cumulative distribution function

The distribution function assigns the probability of a threshold event to each real threshold.

Drineas & Mahoney ↗
Source label: def:cumulative-distribution-function

Download Lean file ↓

Definition. The displayed code defines the mathematical object or predicate.

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

The distribution function assigns the probability of a threshold event to each real threshold.

F(a)=\Pr\{X\le a\}

Assumptions & context

A real-valued function X on a probability space and a threshold a determine the event X ≤ a.

Source

Drineas & Mahoney. Lectures on randomized numerical linear algebra.

Source label: def:cumulative-distribution-function

02 / LEAN REPRESENTATION

Definition

Definition. Expand the complete file below to read imports, local definitions and surrounding context.

noncomputable def cumulativeDistributionFunction {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (X : Ω → ℝ) : ℝ → ℝ :=
  fun α => (P {ω | X ω ≤ α}).toReal

Complete Lean file and local definitions

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal

namespace RNLAPhaseB.DM2017.CumulativeDistributionFunction

/-- dm2017::def:cumulative-distribution-function.
Given a random variable `X` (a real-valued function of the sample point `ω` of a
probability space `(Ω, P)`) and a real number `α`, the cumulative distribution
function (CDF) is the function `F(α) = Pr[X ≤ α]`, i.e. the probability of the
event `{ω | X ω ≤ α}`. The probability is reported as a real number, which is the
value of the probability measure `P` on that event. -/
noncomputable def cumulativeDistributionFunction {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (X : Ω → ℝ) : ℝ → ℝ :=
  fun α => (P {ω | X ω ≤ α}).toReal

end RNLAPhaseB.DM2017.CumulativeDistributionFunction

How to read the formalization

The definition evaluates the measure of the threshold event and converts its value to ℝ. This declaration itself contains no omitted proof.

← Back to all statements