Standardized random variables [UPSTREAM]

The standardization of a real random variable X under a measure μ is its deviation from the mean in standard deviations, (X - μ[X]) / √Var[X; μ]; under the uniform measure on a finite set of observations these are the z-scores. Standardization keeps the order of the values, centres them, scales them to unit variance, and forgets any positive affine change of units.

Main definitions

• ProbabilityTheory.standardize: the standardized random variable.

Main statements

• integral_standardize, variance_standardize: standardized values have mean 0 and, when X is not almost surely constant, variance 1.
• standardize_const_mul_add_const: standardization is invariant under X ↦ a * X + b for 0 < a.
• sign_integral_standardize: under a subpopulation ν ≪ μ the mean standardized value has the sign of ν[X] - μ[X].

Implementation notes

The order lemmas assume 0 < Var[X; μ], as mathlib's division lemmas assume a positive divisor; when the variance is 0 the standardization is constantly 0.

noncomputable def ProbabilityTheory.standardize {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : Ω → ℝ

The standardization of X under μ is its deviation from the mean in standard deviations.

Equations

• ProbabilityTheory.standardize X μ ω = (X ω - ∫ (x : Ω), X x ∂μ) / √(ProbabilityTheory.variance X μ)

theorem ProbabilityTheory.standardize_apply {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (ω : Ω) : standardize X μ ω = (X ω - ∫ (x : Ω), X x ∂μ) / √(variance X μ)

theorem ProbabilityTheory.standardize_le_standardize_iff {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (h : 0 < variance X μ) {ω ω' : Ω} : standardize X μ ω ≤ standardize X μ ω' ↔ X ω ≤ X ω'

theorem ProbabilityTheory.standardize_lt_standardize_iff {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (h : 0 < variance X μ) {ω ω' : Ω} : standardize X μ ω < standardize X μ ω' ↔ X ω < X ω'

theorem ProbabilityTheory.one_lt_standardize_iff {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (h : 0 < variance X μ) {ω : Ω} : 1 < standardize X μ ω ↔ ∫ (x : Ω), X x ∂μ + √(variance X μ) < X ω

theorem ProbabilityTheory.standardize_neg_iff {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (h : 0 < variance X μ) {ω : Ω} : standardize X μ ω < 0 ↔ X ω < ∫ (x : Ω), X x ∂μ

theorem ProbabilityTheory.standardize_const_mul_add_const {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) {a : ℝ} (ha : 0 < a) (b : ℝ) : standardize (fun (ω : Ω) => a * X ω + b) μ = standardize X μ

Standardization is invariant under a positive affine change of units.

theorem ProbabilityTheory.integral_standardize_eq {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ ν : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsProbabilityMeasure ν] (hX : MeasureTheory.Integrable X ν) : ∫ (x : Ω), standardize X μ x ∂ν = (∫ (x : Ω), X x ∂ν - ∫ (x : Ω), X x ∂μ) / √(variance X μ)

The mean of the standardized values under a probability measure ν is the standardized mean under ν.

theorem ProbabilityTheory.integral_standardize {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) : ∫ (x : Ω), standardize X μ x ∂μ = 0

Standardized values average to 0.

theorem ProbabilityTheory.variance_standardize {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) (h : 0 < variance X μ) : variance (standardize X μ) μ = 1

Standardized values have unit variance.

theorem ProbabilityTheory.sign_integral_standardize {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ ν : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hX : MeasureTheory.MemLp X 2 μ) [MeasureTheory.IsProbabilityMeasure ν] (hνμ : ν.AbsolutelyContinuous μ) (hXν : MeasureTheory.Integrable X ν) : SignType.sign (∫ (x : Ω), standardize X μ x ∂ν) = SignType.sign (∫ (x : Ω), X x ∂ν - ∫ (x : Ω), X x ∂μ)

Under a measure ν ≪ μ the mean standardized value has the sign of ν[X] - μ[X].