LeanPool.QuasiBorelSpaces.MeasureTheory.Quantile

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.MeasureTheory.Quantile.

noncomputable def MeasureTheory.cdf (μ : Measure ↑unitInterval) (i : ↑unitInterval) : ↑unitInterval

The cumulative distribution function as a map from the unit interval to itself.

Equations

• MeasureTheory.cdf μ i = ⟨↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map Subtype.val μ)) ↑i, ⋯⟩

noncomputable def MeasureTheory.quantile (μ : Measure ↑unitInterval) (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 = μ