The uniform distribution on an interval

uniformMeasure a b is normalized Lebesgue measure on Set.Ioc a b, defined as ProbabilityTheory.cond volume (Set.Ioc a b).

Why cond and not a fresh normalization. Mathlib defines MeasureTheory.pdf.IsUniform X s ℙ μ as μ.map X = ProbabilityTheory.cond μ s. Defining the measure by the same cond makes the bridge isUniform_of_hasLaw_uniformMeasure hold definitionally, so no second normalization convention enters the library and nothing has to be reconciled later.

Boundary. For b ≤ a the interval is empty and uniformMeasure a b is the zero measure (uniformMeasure_eq_zero_of_le), not a probability measure. Every quantitative statement below therefore takes a < b as a hypothesis rather than assuming it silently.

Main definitions

• TauCeti.Probability.uniformMeasure — the uniform law on Set.Ioc a b;
• TauCeti.Probability.uniformPDFReal — the real-valued density. The ℝ≥0∞-valued density is Mathlib's MeasureTheory.pdf.uniformPDF, reused rather than redefined.

Main results

• isProbabilityMeasure_uniformMeasure — it is a probability measure when a < b;
• uniformMeasure_eq_smul, uniformMeasure_apply — its description as a rescaled restriction, and evaluation on a measurable set;
• isUniform_of_hasLaw_uniformMeasure — a variable with this law is uniform in Mathlib's sense;
• uniformMeasure_eq_withDensity and rnDeriv_uniformMeasure — Mathlib's pdf.uniformPDF is the density of this measure, as a withDensity and as the Radon–Nikodym derivative;
• hasPDF_of_hasLaw_uniformMeasure — a variable with this law satisfies HasPDF, i.e. its law is absolutely continuous; the density itself is identified by the two results above;
• uniformPDF_eq_ofReal_uniformPDFReal — the bridge between that density and the real-valued one;
• cdf_uniformMeasure — the cdf is 0 below a, 1 above b, and (x - a) / (b - a) between;
• integral_id_uniformMeasure — the mean is (a + b) / 2;
• variance_id_uniformMeasure — the variance is (b - a) ^ 2 / 12;
• integrableExpSet_id_uniformMeasure — every exponential moment exists, for every pair of endpoints;
• mgf_id_uniformMeasure_zero and mgf_id_uniformMeasure — the moment generating function, split at the removable singularity t = 0;
• mgf_id_uniformMeasure_pos — the mgf is strictly positive, which is what makes the cgf's logarithm meaningful;
• cgf_id_uniformMeasure_zero and cgf_id_uniformMeasure — the cumulant generating function, split the same way;
• charFun_uniformMeasure_zero and charFun_uniformMeasure — the characteristic function, likewise;
• map_uniformMeasure_affine — every uniform law is an affine image of the standard one;
• measurable_uniformMeasure — the family is measurable in its endpoints, so it can be used as a kernel. The other families' parameter measurability is in TauCeti/Probability/Distributions/Measurability.lean.

Implementation

uniformMeasure_eq_smul rewrites cond into (ENNReal.ofReal (b - a))⁻¹ • volume.restrict … by computing volume (Set.Ioc a b); every integral below is then an interval integral times a scalar. The variance goes through ProbabilityTheory.variance_eq_integral, which asks only for AEMeasurable, rather than through the second-moment formula, which would need an MemLp _ 2 side condition.

References

• Roadmap: TauCetiRoadmap/StandardDistributions/README.md, Layer 0, item 3 — the uniform family: its measure, density, cdf, moments, and transforms — together with the uniform case of item 4.
• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 2, 2nd ed., Wiley (1995), ch. 26.

noncomputable def TauCeti.Probability.uniformMeasure (a b : ℝ) : MeasureTheory.Measure ℝ

The uniform probability measure on the interval Set.Ioc a b.

This is normalized Lebesgue measure on Set.Ioc a b when a < b, and the zero measure when b ≤ a. Phrasing it through ProbabilityTheory.cond is what makes it agree definitionally with Mathlib's MeasureTheory.pdf.IsUniform.

Equations

• TauCeti.Probability.uniformMeasure a b = MeasureTheory.volume[|Set.Ioc a b]

@[simp]

theorem TauCeti.Probability.uniformMeasure_eq_zero_of_le {a b : ℝ} (hba : b ≤ a) : uniformMeasure a b = 0

On a degenerate interval the uniform measure is the zero measure, not a probability measure.

theorem TauCeti.Probability.uniformMeasure_eq_smul {a b : ℝ} : uniformMeasure a b = (ENNReal.ofReal (b - a))⁻¹ • MeasureTheory.volume.restrict (Set.Ioc a b)

The uniform measure is Lebesgue measure restricted to Set.Ioc a b and rescaled by the interval length.

theorem TauCeti.Probability.uniformMeasure_apply {a b : ℝ} {s : Set ℝ} (hs : MeasurableSet s) : (uniformMeasure a b) s = (ENNReal.ofReal (b - a))⁻¹ * MeasureTheory.volume (s ∩ Set.Ioc a b)

Evaluation of the uniform measure on a measurable set.

theorem TauCeti.Probability.isProbabilityMeasure_uniformMeasure {a b : ℝ} (hab : a < b) : MeasureTheory.IsProbabilityMeasure (uniformMeasure a b)

On a nondegenerate interval the uniform measure is a probability measure.

theorem TauCeti.Probability.isUniform_of_hasLaw_uniformMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {a b : ℝ} (hX : ProbabilityTheory.HasLaw X (uniformMeasure a b) P) : MeasureTheory.pdf.IsUniform X (Set.Ioc a b) P MeasureTheory.volume

A random variable with the uniform law is uniform in Mathlib's sense.

This holds by definition: both sides are ProbabilityTheory.cond volume (Set.Ioc a b).

The probability density function

Mathlib already supplies the ℝ≥0∞-valued density of a uniform law as MeasureTheory.pdf.uniformPDF s x μ = s.indicator ((μ s)⁻¹ • 1) x, so none is introduced here — the roadmap is explicit that no second pdf abstraction should enter the library. What is missing is the real-valued form and the interval-specific identifications, which is what this section adds.

noncomputable def TauCeti.Probability.uniformPDFReal (a b x : ℝ) : ℝ

The real-valued density of the uniform distribution on Set.Ioc a b.

Mathlib's MeasureTheory.pdf.uniformPDF is ℝ≥0∞-valued; this is the real-valued companion, and uniformPDF_eq_ofReal_uniformPDFReal relates the two.

Equations

• TauCeti.Probability.uniformPDFReal a b x = if x ∈ Set.Ioc a b then (b - a)⁻¹ else 0

@[simp]

theorem TauCeti.Probability.uniformPDFReal_of_mem {a b x : ℝ} (hx : x ∈ Set.Ioc a b) : uniformPDFReal a b x = (b - a)⁻¹

Inside the interval the real-valued density is the reciprocal of its length.

@[simp]

theorem TauCeti.Probability.uniformPDFReal_of_notMem {a b x : ℝ} (hx : x ∉ Set.Ioc a b) : uniformPDFReal a b x = 0

Outside the interval the real-valued density vanishes.

theorem TauCeti.Probability.measurable_uniformPDFReal {a b : ℝ} : Measurable (uniformPDFReal a b)

The real-valued uniform density is measurable.

theorem TauCeti.Probability.uniformPDF_eq_ofReal_uniformPDFReal {a b : ℝ} (x : ℝ) : MeasureTheory.pdf.uniformPDF (Set.Ioc a b) x MeasureTheory.volume = ENNReal.ofReal (uniformPDFReal a b x)

Mathlib's uniform density is the real one pushed into ℝ≥0∞.

No nondegeneracy hypothesis: inside the interval membership already forces a < b, and outside both sides vanish.

theorem TauCeti.Probability.measurable_uniformPDF_Ioc_volume {a b : ℝ} : Measurable fun (x : ℝ) => MeasureTheory.pdf.uniformPDF (Set.Ioc a b) x MeasureTheory.volume

Mathlib's uniform density on Set.Ioc a b, against volume, is measurable.

theorem TauCeti.Probability.uniformMeasure_eq_withDensity {a b : ℝ} : uniformMeasure a b = MeasureTheory.volume.withDensity fun (x : ℝ) => MeasureTheory.pdf.uniformPDF (Set.Ioc a b) x MeasureTheory.volume

The uniform measure is Lebesgue measure weighted by Mathlib's uniform density.

No a < b hypothesis is needed: on a degenerate interval both sides are the zero measure.

theorem TauCeti.Probability.hasPDF_of_hasLaw_uniformMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {a b : ℝ} (hX : ProbabilityTheory.HasLaw X (uniformMeasure a b) P) : MeasureTheory.HasPDF X P MeasureTheory.volume

A random variable with the uniform law admits a density: its law is absolutely continuous with respect to Lebesgue measure.

This gives HasPDF only. Which density it is, is uniformMeasure_eq_withDensity; on a degenerate interval the law is the zero measure, so no probability-measure claim is made here.

theorem TauCeti.Probability.rnDeriv_uniformMeasure {a b : ℝ} : (uniformMeasure a b).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] fun (x : ℝ) => MeasureTheory.pdf.uniformPDF (Set.Ioc a b) x MeasureTheory.volume

The Radon-Nikodym derivative of the uniform measure against Lebesgue measure is its density.

The cumulative distribution function, mean and variance

theorem TauCeti.Probability.cdf_uniformMeasure {a b : ℝ} (hab : a < b) (x : ℝ) : ↑(ProbabilityTheory.cdf (uniformMeasure a b)) x = if x ≤ a then 0 else if b ≤ x then 1 else (x - a) / (b - a)

The cumulative distribution function of the uniform distribution rises linearly across the interval and is constant outside it.

theorem TauCeti.Probability.integral_id_uniformMeasure {a b : ℝ} (hab : a < b) : ∫ (x : ℝ), x ∂uniformMeasure a b = (a + b) / 2

The mean of the uniform distribution on Set.Ioc a b is the midpoint (a + b) / 2.

theorem TauCeti.Probability.variance_id_uniformMeasure {a b : ℝ} (hab : a < b) : ProbabilityTheory.variance id (uniformMeasure a b) = (b - a) ^ 2 / 12

The variance of the uniform distribution on Set.Ioc a b is (b - a) ^ 2 / 12.

Exponential transforms

The uniform law has bounded support, so every exponential moment exists and the moment generating function is finite on all of ℝ. The formulas split at t = 0: the quotient (exp (t * b) - exp (t * a)) / ((b - a) * t) has a removable singularity there, and rather than push a proof through it the value 1 is given directly.

theorem TauCeti.Probability.ae_mem_Ioc_uniformMeasure {a b : ℝ} : ∀ᵐ (x : ℝ) ∂uniformMeasure a b, x ∈ Set.Ioc a b

The uniform law is carried by its interval.

instance TauCeti.Probability.isFiniteMeasure_uniformMeasure {a b : ℝ} : MeasureTheory.IsFiniteMeasure (uniformMeasure a b)

The uniform law is finite for every pair of endpoints: a probability measure when a < b, and the zero measure otherwise.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_uniformMeasure {a b : ℝ} : ProbabilityTheory.integrableExpSet id (uniformMeasure a b) = Set.univ

Every exponential moment of the uniform law exists.

The support is bounded, so exp (t * x) is bounded above by exp (|t| * max |a| |b|) almost everywhere, and the measure is finite. No hypothesis on the endpoints is needed.

theorem TauCeti.Probability.mgf_id_uniformMeasure_zero {a b : ℝ} (hab : a < b) : ProbabilityTheory.mgf id (uniformMeasure a b) 0 = 1

The moment generating function of the uniform law at 0 is 1.

Deliberately not @[simp]: simp already rewrites mgf id μ 0 to μ.real Set.univ, so this left-hand side is not in normal form and the repo's simpNF linter rejects the annotation. For a probability measure simp then closes the goal on its own, which makes the annotation redundant as well as ill-formed.

theorem TauCeti.Probability.mgf_id_uniformMeasure {a b t : ℝ} (hab : a < b) (ht : t ≠ 0) : ProbabilityTheory.mgf id (uniformMeasure a b) t = (Real.exp (t * b) - Real.exp (t * a)) / ((b - a) * t)

The moment generating function of the uniform law, away from the removable singularity.

The cumulant generating function

The cgf is the real logarithm of the mgf, so it is only meaningful once the mgf is known to be strictly positive. That positivity is proved here rather than assumed: mgf_id_uniformMeasure_pos follows from mgf_pos, whose integrability hypothesis is exactly what integrableExpSet_id_uniformMeasure supplies.

theorem TauCeti.Probability.integrable_exp_mul_id_uniformMeasure {a b t : ℝ} : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (uniformMeasure a b)

Every exponential moment of the uniform law is integrable, read off the exponential-moment set.

theorem TauCeti.Probability.mgf_id_uniformMeasure_pos {a b : ℝ} (hab : a < b) (t : ℝ) : 0 < ProbabilityTheory.mgf id (uniformMeasure a b) t

The moment generating function of the uniform law is strictly positive.

This is what makes the cgf's logarithm meaningful; it is not a side remark.

theorem TauCeti.Probability.cgf_id_uniformMeasure_zero {a b : ℝ} (hab : a < b) : ProbabilityTheory.cgf id (uniformMeasure a b) 0 = 0

The cumulant generating function of the uniform law at 0 is 0.

theorem TauCeti.Probability.cgf_id_uniformMeasure {a b t : ℝ} (hab : a < b) (ht : t ≠ 0) : ProbabilityTheory.cgf id (uniformMeasure a b) t = Real.log ((Real.exp (t * b) - Real.exp (t * a)) / ((b - a) * t))

The cumulant generating function of the uniform law, away from the removable singularity.

The argument of the logarithm is positive by mgf_id_uniformMeasure_pos.

The characteristic function

Kept clear of the real mgf development above: this is a complex-valued calculation, and the only thing it borrows is uniformMeasure_eq_smul. It splits at t = 0 for the same reason the mgf does — the quotient has a removable singularity there.

theorem TauCeti.Probability.charFun_uniformMeasure_zero {a b : ℝ} (hab : a < b) : MeasureTheory.charFun (uniformMeasure a b) 0 = 1

The characteristic function of the uniform law at 0 is 1.

theorem TauCeti.Probability.charFun_uniformMeasure {a b t : ℝ} (hab : a < b) (ht : t ≠ 0) : MeasureTheory.charFun (uniformMeasure a b) t = (Complex.exp (Complex.I * ↑b * ↑t) - Complex.exp (Complex.I * ↑a * ↑t)) / (Complex.I * ↑(b - a) * ↑t)

The characteristic function of the uniform law, away from the removable singularity.

Affine transport

Every uniform law is an affine image of the standard one on Set.Ioc 0 1. This is what lets a statement proved for uniformMeasure 0 1 be transported to a general interval instead of reproved, and it is the scalar case of the change-of-variables pattern the later families reuse.

The two supporting lemmas are private: both are generic facts about Lebesgue measure and affine maps with no uniform-distribution content, and exposing them from a distribution-specific module would put them in the wrong place. If a later target needs either publicly, relocating it to a general measure module is its own focused change.

theorem TauCeti.Probability.map_uniformMeasure_affine {a b : ℝ} (hab : a < b) : MeasureTheory.Measure.map (fun (x : ℝ) => a + (b - a) * x) (uniformMeasure 0 1) = uniformMeasure a b

Every uniform law is an affine image of the standard one.

Measurability in the endpoints

theorem TauCeti.Probability.measurable_uncurry_uniformPDF : Measurable fun (q : (ℝ × ℝ) × ℝ) => MeasureTheory.pdf.uniformPDF (Set.Ioc q.1.1 q.1.2) q.2 MeasureTheory.volume

Mathlib's uniform density on Set.Ioc a b is measurable jointly in the two endpoints and the point.

This is the input MeasureTheory.measurable_withDensity needs; measurable_uniformPDF_Ioc_volume fixes the endpoints and is too weak for it.

theorem TauCeti.Probability.measurable_uniformMeasure : Measurable fun (p : ℝ × ℝ) => uniformMeasure p.1 p.2

The uniform family is measurable in its endpoints.

With MeasureTheory.Measure carrying the Giry measurable structure, this is what lets a uniform law with random endpoints be assembled into a ProbabilityTheory.Kernel. No a < b hypothesis: on a degenerate interval the value is the zero measure, which is where the map is constant.