noncomputable def MeasureTheory.quantile (μ : Measure ↑unitInterval) [IsProbabilityMeasure μ] (i : ↑unitInterval) : ↑unitInterval

The quantile distribution function (i.e., the inverse of cdf).

Equations

• MeasureTheory.quantile μ i = sInf {r : ↑unitInterval | i ≤ MeasureTheory.cdf✝ μ r}

theorem MeasureTheory.measurable_quantile {A : Type u_1} [MeasurableSpace A] {μ : A → Measure ↑unitInterval} [∀ (x : A), IsProbabilityMeasure (μ x)] (hμ : Measurable μ) {f : A → ↑unitInterval} (hf : Measurable f) : Measurable fun (x : A) => quantile (μ x) (f x)

@[simp]

theorem MeasureTheory.Measure.eq_quantile_volume (μ : Measure ↑unitInterval) [IsProbabilityMeasure μ] : map (quantile μ) volume = μ