Affine images of real laws

For a measure μ on ℝ and real numbers a, b, the law of a + b X for X with law μ is the pushforward μ.map (fun x => a + b * x). This file computes its density and elementary observables in terms of those of μ: the cumulative distribution function, integrability and moments, and the exponential transforms. Once a location-scale identity between two families is known as an equality of measures, these formulas transfer each observable along it.

At a nonzero slope, an original density f becomes |b|⁻¹ f ((x - a) / b). The measure-level change of variables is accompanied by HasPDF, canonical pdf, and Radon–Nikodym derivative forms, so callers can use the result whether their input is presented as a weighted Lebesgue measure, a random variable, or an absolutely continuous law.

The cdf at a positive slope is the cdf of μ at the pulled-back point. At a negative slope the map reverses order, so it is one minus the mass μ gives to the open half-line below the pulled-back point: this left limit of the cdf cannot be replaced by the cdf itself when μ has an atom there. At slope zero the pushforward of a probability measure is the Dirac mass at a, which is Mathlib's MeasureTheory.Measure.map_const.

The variance, moment-generating function and characteristic function computations follow Mathlib's ProbabilityTheory.variance_id_map, ProbabilityTheory.variance_const_add and ProbabilityTheory.variance_const_mul, ProbabilityTheory.mgf_const_add and ProbabilityTheory.mgf_const_mul, and MeasureTheory.charFun_apply_real, which they reduce to.

Main results

• TauCeti.Probability.map_affine_map_affine — affine pushforwards compose, and TauCeti.Probability.neg_map_affine reflects an affine image;
• TauCeti.Probability.support_map_affine — a nonconstant affine pushforward transports the topological support;
• TauCeti.Probability.measurable_map_affine — affine pushforward is jointly measurable in the probability law, intercept, and slope;
• TauCeti.Probability.affineDensity, TauCeti.Probability.map_affine_withDensity_volume — the transformed density and the measure-level change of variables;
• TauCeti.Probability.map_affine_eq_withDensity_pdf, TauCeti.Probability.hasLaw_affine, TauCeti.Probability.hasPDF_affine, TauCeti.Probability.pdf_affine, and TauCeti.Probability.rnDeriv_map_affine — the corresponding random-variable and Radon–Nikodym interfaces;
• TauCeti.Probability.cdf_map_affine_of_pos, TauCeti.Probability.cdf_map_affine_of_neg — the cdf at a positive and at a negative slope;
• TauCeti.Probability.quantile_map_affine_pos, TauCeti.Probability.quantile_map_affine_neg and their upper-quantile counterparts — affine transport of lower and upper quantiles, including the reversal of the level at a negative slope;
• TauCeti.Probability.memLp_id_map_affine_iff — a nonconstant affine image has exactly the absolute moments of the original law;
• TauCeti.Probability.integral_id_map_affine, TauCeti.Probability.variance_id_map_affine — the mean a + b E[X] and the variance b ^ 2 Var[X];
• TauCeti.Probability.moment_id_map_affine, TauCeti.Probability.centralMoment_id_map_affine — raw moments by the binomial expansion, and central moments scaled by b ^ n;
• TauCeti.Probability.mgf_id_map_affine, TauCeti.Probability.integrableExpSet_id_map_affine, TauCeti.Probability.cgf_id_map_affine — the moment-generating function exp (a t) M(b t), its domain {t | b t ∈ D}, and the cumulant-generating function a t + K(b t) on it;
• TauCeti.Probability.mgf_id_neg, TauCeti.Probability.integrableExpSet_id_neg, TauCeti.Probability.cgf_id_neg — the exponential transforms of the reflected law at -t;
• TauCeti.Probability.charFun_map_affine — the characteristic function exp (i a t) φ(b t).

theorem TauCeti.Probability.map_affine_map_affine {μ : MeasureTheory.Measure ℝ} (a b c d : ℝ) : MeasureTheory.Measure.map (fun (y : ℝ) => c + d * y) (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ) = MeasureTheory.Measure.map (fun (x : ℝ) => c + d * a + d * b * x) μ

Composition of affine pushforwards. Applying y ↦ c + d * y after x ↦ a + b * x is the single affine map with intercept c + d * a and slope d * b.

theorem TauCeti.Probability.neg_map_affine {μ : MeasureTheory.Measure ℝ} (a b : ℝ) : (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ).neg = MeasureTheory.Measure.map (fun (x : ℝ) => -a + -b * x) μ

Reflection of an affine image. The law of -(a + b X) is the affine image of the law of X with intercept -a and slope -b.

theorem TauCeti.Probability.support_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} (hb : b ≠ 0) : (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ).support = (fun (x : ℝ) => a + b * x) '' μ.support

Support of an affine image. A nonconstant affine pushforward has support equal to the affine image of the original support.

theorem TauCeti.Probability.measurable_map_affine : Measurable fun (p : MeasureTheory.ProbabilityMeasure ℝ × ℝ × ℝ) => MeasureTheory.Measure.map (fun (x : ℝ) => p.2.1 + p.2.2 * x) ↑p.1

Affine pushforward is jointly measurable in the probability law, intercept, and slope.

Densities

noncomputable def TauCeti.Probability.affineDensity (a b : ℝ) (f : ℝ → ENNReal) (y : ℝ) : ENNReal

The density obtained from f by the nonconstant affine change of variables x ↦ a + b * x. For b ≠ 0, this is |b|⁻¹ f ((y - a) / b).

At b = 0 this function is zero; the density transport theorems below deliberately require a nonzero slope because the affine image is then a Dirac measure rather than an absolutely continuous law.

@[simp]

theorem TauCeti.Probability.affineDensity_apply (a b : ℝ) (f : ℝ → ENNReal) (y : ℝ) : affineDensity a b f y = ENNReal.ofReal |b|⁻¹ * f ((y - a) / b)

The value of the density obtained by an affine change of variables.

theorem TauCeti.Probability.measurable_affineDensity {f : ℝ → ENNReal} (hf : Measurable f) (a b : ℝ) : Measurable (affineDensity a b f)

The affine transform of a measurable density is measurable.

theorem TauCeti.Probability.map_affine_withDensity_volume {a b : ℝ} (f : ℝ → ENNReal) (hb : b ≠ 0) : MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) (MeasureTheory.volume.withDensity f) = MeasureTheory.volume.withDensity (affineDensity a b f)

Affine change of variables for a real density. If b ≠ 0, pushing a Lebesgue density f forward by x ↦ a + b * x gives the density |b|⁻¹ f ((y - a) / b).

theorem TauCeti.Probability.rnDeriv_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.SFinite μ] (hb : b ≠ 0) : (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] affineDensity a b (μ.rnDeriv MeasureTheory.volume)

The Radon–Nikodym derivative of a nonconstant affine image of an s-finite real measure is the affine transform of its Radon–Nikodym derivative.

theorem TauCeti.Probability.map_affine_eq_withDensity_pdf {a b : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.HasPDF X P MeasureTheory.volume] (hb : b ≠ 0) : MeasureTheory.Measure.map (fun (ω : Ω) => a + b * X ω) P = MeasureTheory.volume.withDensity (affineDensity a b (MeasureTheory.pdf X P MeasureTheory.volume))

The law of a nonconstant affine transform, expressed using the canonical density of the original random variable.

theorem TauCeti.Probability.hasLaw_affine {a b : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.HasPDF X P MeasureTheory.volume] (hb : b ≠ 0) : ProbabilityTheory.HasLaw (fun (ω : Ω) => a + b * X ω) (MeasureTheory.volume.withDensity (affineDensity a b (MeasureTheory.pdf X P MeasureTheory.volume))) P

A nonconstant affine transform has the law obtained by affinely transporting its canonical density.

theorem TauCeti.Probability.hasPDF_affine {a b : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.HasPDF X P MeasureTheory.volume] (hb : b ≠ 0) : MeasureTheory.HasPDF (fun (ω : Ω) => a + b * X ω) P MeasureTheory.volume

A nonconstant affine transform of a real random variable with a density again has a density.

theorem TauCeti.Probability.pdf_affine {a b : ℝ} {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.HasPDF X P MeasureTheory.volume] (hb : b ≠ 0) : MeasureTheory.pdf (fun (ω : Ω) => a + b * X ω) P MeasureTheory.volume =ᵐ[MeasureTheory.volume] affineDensity a b (MeasureTheory.pdf X P MeasureTheory.volume)

The canonical density of a nonconstant affine transform is |b|⁻¹ pdf X P ((y - a) / b).

Cumulative distribution functions

theorem TauCeti.Probability.cdf_map_affine_of_pos {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hb : 0 < b) (x : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (y : ℝ) => a + b * y) μ)) x = ↑(ProbabilityTheory.cdf μ) ((x - a) / b)

At a positive slope, the cdf of the affine image is the cdf of μ at the pulled-back point (x - a) / b.

theorem TauCeti.Probability.cdf_map_affine_of_neg {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hb : b < 0) (x : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (y : ℝ) => a + b * y) μ)) x = 1 - μ.real (Set.Iio ((x - a) / b))

At a negative slope, the cdf of the affine image is one minus the mass μ gives to the open half-line below the pulled-back point (x - a) / b, that is, one minus the left limit of the cdf of μ there.

Quantiles

theorem TauCeti.Probability.measureReal_Iio_map_affine_of_pos {μ : MeasureTheory.Measure ℝ} {a b : ℝ} (hb : 0 < b) (x : ℝ) : (MeasureTheory.Measure.map (fun (y : ℝ) => a + b * y) μ).real (Set.Iio x) = μ.real (Set.Iio ((x - a) / b))

At a positive slope, the mass strictly below a point under an affine image is the mass strictly below its pulled-back point.

theorem TauCeti.Probability.measureReal_Iio_map_affine_of_neg {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hb : b < 0) (x : ℝ) : (MeasureTheory.Measure.map (fun (y : ℝ) => a + b * y) μ).real (Set.Iio x) = 1 - ↑(ProbabilityTheory.cdf μ) ((x - a) / b)

At a negative slope, the mass strictly below a point under an affine image is one minus the cdf at its pulled-back point.

@[simp]

theorem TauCeti.Probability.quantile_map_affine_pos {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] {u : ℝ} (hb : 0 < b) (h0 : 0 < u) (h1 : u < 1) : (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ).quantile u = a + b * μ.quantile u

A positive affine map carries lower quantiles to lower quantiles.

@[simp]

theorem TauCeti.Probability.upperQuantile_map_affine_pos {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] {u : ℝ} (hb : 0 < b) (h0 : 0 < u) (h1 : u < 1) : (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ).upperQuantile u = a + b * μ.upperQuantile u

A positive affine map carries upper quantiles to upper quantiles.

@[simp]

theorem TauCeti.Probability.quantile_map_affine_neg {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] {u : ℝ} (hb : b < 0) (h0 : 0 < u) (h1 : u < 1) : (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ).quantile u = a + b * μ.upperQuantile (1 - u)

A negative affine map carries lower quantiles to reflected upper quantiles. The upper quantile is necessary when the original cdf has a plateau at level 1 - u.

@[simp]

theorem TauCeti.Probability.upperQuantile_map_affine_neg {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] {u : ℝ} (hb : b < 0) (h0 : 0 < u) (h1 : u < 1) : (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ).upperQuantile u = a + b * μ.quantile (1 - u)

A negative affine map carries upper quantiles to reflected lower quantiles.

theorem TauCeti.Probability.quantile_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] {u : ℝ} (h0 : 0 < u) (h1 : u < 1) : (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ).quantile u = if 0 < b then a + b * μ.quantile u else if b = 0 then a else a + b * μ.upperQuantile (1 - u)

The lower quantile of an affine image, including positive, zero, and negative slopes.

theorem TauCeti.Probability.upperQuantile_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] {u : ℝ} (h0 : 0 < u) (h1 : u < 1) : (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ).upperQuantile u = if 0 < b then a + b * μ.upperQuantile u else if b = 0 then a else a + b * μ.quantile (1 - u)

The upper quantile of an affine image, including positive, zero, and negative slopes.

Integrability and moments

theorem TauCeti.Probability.memLp_id_map_affine_iff {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hb : b ≠ 0) {p : ENNReal} : MeasureTheory.MemLp id p (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ) ↔ MeasureTheory.MemLp id p μ

Absolute moments of an affine image. For a nonzero slope, the affine image of a finite measure has a finite p-th absolute moment exactly when the original measure does.

theorem TauCeti.Probability.integral_id_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : MeasureTheory.Integrable id μ) : ∫ (x : ℝ), x ∂MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ = a + b * ∫ (x : ℝ), x ∂μ

Mean of an affine image. If μ is a probability measure with integrable identity, then the mean of a + b X is a + b E[X].

theorem TauCeti.Probability.variance_id_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] : ProbabilityTheory.variance id (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ) = b ^ 2 * ProbabilityTheory.variance id μ

Variance of an affine image. The variance of a + b X is b ^ 2 Var[X]. No moment hypothesis is needed: both sides vanish when X is not square-integrable and b ≠ 0.

theorem TauCeti.Probability.moment_id_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsFiniteMeasure μ] {n : ℕ} (h : MeasureTheory.Integrable (fun (x : ℝ) => |x| ^ n) μ) : ProbabilityTheory.moment id n (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ) = ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * a ^ (n - k) * b ^ k * ProbabilityTheory.moment id k μ

Raw moments of an affine image. If μ is a finite measure with finite n-th absolute moment, then the n-th moment of a + b X is the binomial expansion ∑ k ≤ n, (n choose k) a ^ (n - k) b ^ k E[X ^ k].

theorem TauCeti.Probability.centralMoment_id_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : MeasureTheory.Integrable id μ) (n : ℕ) : ProbabilityTheory.centralMoment id n (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ) = b ^ n * ProbabilityTheory.centralMoment id n μ

Central moments of an affine image. If μ is a probability measure with integrable identity, then the n-th central moment of a + b X is b ^ n times that of X.

Exponential transforms

theorem TauCeti.Probability.mgf_id_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} (t : ℝ) : ProbabilityTheory.mgf id (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ) t = Real.exp (a * t) * ProbabilityTheory.mgf id μ (b * t)

Moment-generating function of an affine image. M_{a + bX}(t) = exp (a t) M_X(b t).

theorem TauCeti.Probability.integrableExpSet_id_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} : ProbabilityTheory.integrableExpSet id (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ) = (fun (t : ℝ) => b * t) ⁻¹' ProbabilityTheory.integrableExpSet id μ

Exponential-integrability domain of an affine image. a + b X has a finite exponential moment at t exactly when X has one at b t.

theorem TauCeti.Probability.cgf_id_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} [NeZero μ] {t : ℝ} (ht : b * t ∈ ProbabilityTheory.integrableExpSet id μ) : ProbabilityTheory.cgf id (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ) t = a * t + ProbabilityTheory.cgf id μ (b * t)

Cumulant-generating function of an affine image. On the exponential-integrability domain, K_{a + bX}(t) = a t + K_X(b t).

theorem TauCeti.Probability.mgf_id_neg {μ : MeasureTheory.Measure ℝ} (t : ℝ) : ProbabilityTheory.mgf id μ.neg t = ProbabilityTheory.mgf id μ (-t)

Moment-generating function of the reflected law. M_{-X}(t) = M_X(-t).

theorem TauCeti.Probability.integrableExpSet_id_neg {μ : MeasureTheory.Measure ℝ} : ProbabilityTheory.integrableExpSet id μ.neg = Neg.neg ⁻¹' ProbabilityTheory.integrableExpSet id μ

Exponential-integrability domain of the reflected law. -X has a finite exponential moment at t exactly when X has one at -t.

theorem TauCeti.Probability.cgf_id_neg {μ : MeasureTheory.Measure ℝ} (t : ℝ) : ProbabilityTheory.cgf id μ.neg t = ProbabilityTheory.cgf id μ (-t)

Cumulant-generating function of the reflected law. K_{-X}(t) = K_X(-t).

theorem TauCeti.Probability.charFun_map_affine {μ : MeasureTheory.Measure ℝ} {a b : ℝ} (t : ℝ) : MeasureTheory.charFun (MeasureTheory.Measure.map (fun (x : ℝ) => a + b * x) μ) t = Complex.exp (↑a * ↑t * Complex.I) * MeasureTheory.charFun μ (b * t)

Characteristic function of an affine image. φ_{a + bX}(t) = exp (i a t) φ_X(b t).