AcceptedDefinition with auxiliary statements (proofs omitted)

Probability mass function

The mass at a real value is the probability that a random variable equals that value.

Drineas & Mahoney ↗
Source label: def:probability-mass-function

Definition. The displayed code defines the mathematical object or predicate. Auxiliary statements shown alongside the definition have omitted proofs (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

The mass at a real value is the probability that a random variable equals that value.

f(a)=\Pr\{X=a\}

Assumptions & context

X is measurable on a probability space; the definition is indexed by a real value a.

Source

Drineas & Mahoney. Lectures on randomized numerical linear algebra.

Source label: def:probability-mass-function

02 / LEAN REPRESENTATION

Definition

Definition with auxiliary statements (proofs omitted). Expand the complete file below to read imports, local definitions and surrounding context.

noncomputable def probabilityMassFunction {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (X : Ω → ℝ) (_hX : Measurable X) :
    ℝ → ℝ≥0∞ :=
  fun α => P {ω | X ω = α}

theorem probabilityMassFunction_apply {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (X : Ω → ℝ) (hX : Measurable X) (α : ℝ) :
    probabilityMassFunction P X hX α = P {ω | X ω = α} := by sorry

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.ProbabilityMassFunction

/-- dm2017 `def:probability-mass-function`: given a (real-valued) random variable `X`
on a probability space `(Ω, P)` and a real number `α`, the probability mass function
(PMF) is the function `f(α) = Pr[X = α]`, i.e. the probability of the event
`{ω | X ω = α}`. Probabilities are measured in `ℝ≥0∞`, the value type of a measure.
Measurability of `X` records that `X` is a random variable. -/
noncomputable def probabilityMassFunction {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (X : Ω → ℝ) (_hX : Measurable X) :
    ℝ → ℝ≥0∞ :=
  fun α => P {ω | X ω = α}

/-- The defining equation `f(α) = Pr[X = α]` of the PMF, for every real `α`. -/
theorem probabilityMassFunction_apply {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (X : Ω → ℝ) (hX : Measurable X) (α : ℝ) :
    probabilityMassFunction P X hX α = P {ω | X ω = α} := by sorry

end RNLAPhaseB.DM2017.ProbabilityMassFunction

How to read the formalization

Values are represented in ℝ≥0∞. The file also states the defining equation as a theorem with an omitted proof.

← Back to all statements