Distributional formulas for Dirac measures

This file records the cumulative distribution and the lower and upper quantile functions of a real Dirac measure, and the exponential-integrability domain and cumulant-generating function of a real-valued statistic under a Dirac measure. The moment-generating function is already available in Mathlib as ProbabilityTheory.mgf_dirac'.

Main results

• TauCeti.Probability.cdf_dirac — the cdf of a real Dirac measure;
• MeasureTheory.Measure.quantile_dirac and MeasureTheory.Measure.upperQuantile_dirac — the lower and upper quantile functions of a Dirac measure;
• TauCeti.Probability.integrableExpSet_dirac — every exponential moment exists under a Dirac measure;
• TauCeti.Probability.cgf_dirac' — the cumulant-generating function under a Dirac measure.

@[simp]

theorem TauCeti.Probability.cdf_dirac (a x : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.dirac a)) x = if a ≤ x then 1 else 0

The cumulative distribution function of a Dirac measure is a step function.

@[simp]

theorem TauCeti.Probability.integrableExpSet_dirac {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (X : Ω → ℝ) (ω : Ω) : ProbabilityTheory.integrableExpSet X (MeasureTheory.Measure.dirac ω) = Set.univ

Every exponential moment of a Dirac measure exists.

@[simp]

theorem TauCeti.Probability.cgf_dirac' {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (X : Ω → ℝ) (ω : Ω) (t : ℝ) : ProbabilityTheory.cgf X (MeasureTheory.Measure.dirac ω) t = t * X ω

The cumulant-generating function of a Dirac measure is linear.

@[simp]

theorem MeasureTheory.Measure.quantile_dirac (a : ℝ) {t : ℝ} (h0 : 0 < t) (h1 : t ≤ 1) : (dirac a).quantile t = a

At every level in Ioc 0 1, including the endpoint level 1, the quantile function of a Dirac law is its atom.

@[simp]

theorem MeasureTheory.Measure.upperQuantile_dirac (a : ℝ) {t : ℝ} (h0 : 0 ≤ t) (h1 : t < 1) : (dirac a).upperQuantile t = a

At every level in Ico 0 1, including the endpoint level 0, the upper quantile function of a Dirac law is its atom.