Distribution functions and quantiles

Cumulative distribution functions and their continuity points, quantile functions and inverse transform sampling, medians, and joint laws.

• Cumulative distribution function
• Median of a distribution
• Quantile function and inverse transform sampling

TheoremJoint law of two random variables on a rectangle#✓fully proved

Let \(P\) be a measure on a measurable space \(\Omega\), and let \(X : \Omega \to \mathcal{X}\) and \(Y : \Omega \to \mathcal{Y}\) be \(P\)-almost everywhere measurable maps into measurable spaces. For measurable sets \(s \subseteq \mathcal{X}\) and \(t \subseteq \mathcal{Y}\), the pushforward of \(P\) under \(\omega \mapsto (X(\omega), Y(\omega))\) gives \(s \times t\) the measure \(P(\{\omega : X(\omega) \in s \text{ and } Y(\omega) \in t\})\).

When \(P\) is a probability measure this pushforward is the joint law of \(X\) and \(Y\), and the value is the probability that both events occur.

theorem map_prodMk_apply_prod
    {Ω 𝓧 𝓨 : Type*} [MeasurableSpace Ω]
    [MeasurableSpace 𝓧] [MeasurableSpace 𝓨]
    {X : Ω → 𝓧} {Y : Ω → 𝓨} {P : Measure Ω}
    (hX : AEMeasurable X P) (hY : AEMeasurable Y P)
    {s : Set 𝓧} {t : Set 𝓨} (hs : MeasurableSet s) (ht : MeasurableSet t) :
    P.map (fun ω => (X ω, Y ω)) (s ×ˢ t) = P (X ⁻¹' s ∩ Y ⁻¹' t)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.