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