The Rademacher distribution

The Rademacher law is the probability measure on ℝ assigning equal mass to -1 and 1. This file gives its masses and support, cumulative distribution and quantile, natural moments, and moment- and characteristic-function formulas, and the fact that a variable with this law is almost surely ±1.

noncomputable def TauCeti.Probability.rademacherMeasure : MeasureTheory.Measure ℝ

The Rademacher law, assigning probability 1 / 2 to each of -1 and 1.

theorem TauCeti.Probability.rademacherMeasure_eq : rademacherMeasure = (1 / 2) • MeasureTheory.Measure.dirac (-1) + (1 / 2) • MeasureTheory.Measure.dirac 1

The Rademacher law is the equally weighted sum of the Dirac masses at -1 and 1.

instance TauCeti.Probability.instIsProbabilityMeasureRealRademacherMeasure : MeasureTheory.IsProbabilityMeasure rademacherMeasure

The Rademacher law is a probability measure.

theorem TauCeti.Probability.rademacherMeasure_map_neg : MeasureTheory.Measure.map (fun (x : ℝ) => -x) rademacherMeasure = rademacherMeasure

The Rademacher law is invariant under reflection in the origin.

instance TauCeti.Probability.instIsNegInvariantRealRademacherMeasure : rademacherMeasure.IsNegInvariant

The Rademacher law is invariant under negation.

theorem TauCeti.Probability.integral_rademacherMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : ℝ → E) : ∫ (x : ℝ), f x ∂rademacherMeasure = (1 / 2) • f (-1) + (1 / 2) • f 1

Integration against the Rademacher law is the average of evaluation at -1 and 1.

@[simp]

theorem TauCeti.Probability.integrable_rademacherMeasure {E : Type u_1} [NormedAddCommGroup E] (f : ℝ → E) : MeasureTheory.Integrable f rademacherMeasure

Every function is integrable with respect to the finitely supported Rademacher law.

@[simp]

theorem TauCeti.Probability.rademacherMeasure_singleton (x : ℝ) : rademacherMeasure {x} = if x = -1 ∨ x = 1 then 1 / 2 else 0

Each of the two atoms of the Rademacher law has mass 1 / 2, and every other singleton has mass zero.

@[simp]

theorem TauCeti.Probability.support_rademacherMeasure : rademacherMeasure.support = {-1, 1}

The topological support of the Rademacher law consists exactly of its two atoms.

@[simp]

theorem TauCeti.Probability.cdf_rademacherMeasure (x : ℝ) : ↑(ProbabilityTheory.cdf rademacherMeasure) x = if x < -1 then 0 else if x < 1 then 1 / 2 else 1

The cumulative distribution function of the Rademacher law.

@[simp]

theorem TauCeti.Probability.quantile_rademacherMeasure {u : ℝ} (hu : u ∈ Set.Ioo 0 1) : rademacherMeasure.quantile u = if u ≤ 1 / 2 then -1 else 1

The interior lower quantile of the Rademacher law is -1 on the lower half of the unit interval and 1 on the upper half.

theorem TauCeti.Probability.tendsto_quantile_rademacherMeasure_nhdsGT_zero : Filter.Tendsto rademacherMeasure.quantile (nhdsWithin 0 (Set.Ioi 0)) (nhds (-1))

The lower quantile tends to the lower endpoint of the Rademacher support as the level tends to zero from above.

theorem TauCeti.Probability.tendsto_quantile_rademacherMeasure_nhdsLT_one : Filter.Tendsto rademacherMeasure.quantile (nhdsWithin 1 (Set.Iio 1)) (nhds 1)

The lower quantile tends to the upper endpoint of the Rademacher support as the level tends to one from below.

theorem TauCeti.Probability.integrable_pow_rademacherMeasure (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ n) rademacherMeasure

Every natural power is integrable under the Rademacher law.

@[simp]

theorem TauCeti.Probability.integral_pow_rademacherMeasure (n : ℕ) : ∫ (x : ℝ), x ^ n ∂rademacherMeasure = if Even n then 1 else 0

The nth raw moment of the Rademacher law is one for even n and zero for odd n.

@[simp]

theorem TauCeti.Probability.integral_id_rademacherMeasure : ∫ (x : ℝ), x ∂rademacherMeasure = 0

The Rademacher law is centered.

@[simp]

theorem TauCeti.Probability.variance_id_rademacherMeasure : ProbabilityTheory.variance id rademacherMeasure = 1

The variance of the Rademacher law is one.

theorem TauCeti.Probability.integrable_exp_mul_id_rademacherMeasure (t : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) rademacherMeasure

Every exponential moment of the Rademacher law is integrable.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_rademacherMeasure : ProbabilityTheory.integrableExpSet id rademacherMeasure = Set.univ

The exponential-integrability domain of the Rademacher law is all of ℝ.

@[simp]

theorem TauCeti.Probability.mgf_id_rademacherMeasure (t : ℝ) : ProbabilityTheory.mgf id rademacherMeasure t = Real.cosh t

The moment-generating function of the Rademacher law is the hyperbolic cosine.

@[simp]

theorem TauCeti.Probability.cgf_id_rademacherMeasure (t : ℝ) : ProbabilityTheory.cgf id rademacherMeasure t = Real.log (Real.cosh t)

The cumulant-generating function of the Rademacher law is the logarithm of the hyperbolic cosine.

@[simp]

theorem TauCeti.Probability.charFun_rademacherMeasure (t : ℝ) : MeasureTheory.charFun rademacherMeasure t = ↑(Real.cos t)

The characteristic function of the Rademacher law is the cosine.

theorem TauCeti.Probability.aemeasurable_of_map_eq_rademacherMeasure {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ε : Ω → ℝ} (h : MeasureTheory.Measure.map ε μ = rademacherMeasure) : AEMeasurable ε μ

A random variable with the Rademacher law is almost everywhere measurable: an unmeasurable pushforward is 0 or a Dirac mass, and neither charges both atoms ±1.

theorem TauCeti.Probability.ae_eq_one_or_eq_neg_one_of_map_eq_rademacherMeasure {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ε : Ω → ℝ} (h : MeasureTheory.Measure.map ε μ = rademacherMeasure) : ∀ᵐ (ω : Ω) ∂μ, ε ω = 1 ∨ ε ω = -1

A random variable with the Rademacher law equals ±1 almost surely.