Semicircle Distributions over ℝ

We define the real-valued Wigner semicircle distribution.

Main definitions

• semicirclePDFReal: the function μ v x ↦ (1 / (2 * π * v)) * √(4 * v - (x - μ) ^ 2), the probability density function of the semicircle distribution with mean μ and variance v (when v ≠ 0).
• semicirclePDF: the ℝ≥0∞-valued pdf, semicirclePDF μ v x = ENNReal.ofReal (semicirclePDFReal μ v x).
• semicircleReal: the semicircle measure on ℝ, parametrized by mean μ and variance v. If v = 0, this is Measure.dirac μ; otherwise it is the measure with density semicirclePDF μ v against the Lebesgue measure.

Main results

• semicircleReal_add_const, semicircleReal_const_mul: affine transformations of a semicircular random variable stay semicircular, with the mean and variance transformed accordingly.
• integral_id_semicircleReal: the mean of semicircleReal μ v is its mean parameter μ.
• variance_id_semicircleReal: the variance of semicircleReal μ v is its variance parameter v.
• centralMoment_two_mul_semicircleReal: the 2 * n-th central moment of the semicircle distribution equals v ^ n times the n-th Catalan number.
• centralMoment_odd_semicircleReal: the odd central moments of the semicircle distribution vanish.

noncomputable def LeanPool.SemicircleLaw.semicirclePDFReal (μ : ℝ) (v : NNReal) (x : ℝ) : ℝ

Probability density function of the semicircle distribution with mean μ and variance v. Note that the square root of a negative number is defined to be zero.

Equations

• LeanPool.SemicircleLaw.semicirclePDFReal μ v x = 1 / (2 * Real.pi * ↑v) * √(4 * ↑v - (x - μ) ^ 2)

theorem LeanPool.SemicircleLaw.semicirclePDFReal_def (μ : ℝ) (v : NNReal) : semicirclePDFReal μ v = fun (x : ℝ) => 1 / (2 * Real.pi * ↑v) * √(4 * ↑v - (x - μ) ^ 2)

@[simp]

theorem LeanPool.SemicircleLaw.semicirclePDFReal_zero_var (m : ℝ) : semicirclePDFReal m 0 = 0

theorem LeanPool.SemicircleLaw.semicirclePDFReal_nonneg (μ : ℝ) (v : NNReal) (x : ℝ) : 0 ≤ semicirclePDFReal μ v x

The semicircle pdf is nonnegative.

theorem LeanPool.SemicircleLaw.continuous_semicirclePDFReal (μ : ℝ) (v : NNReal) : Continuous (semicirclePDFReal μ v)

The semicircle pdf is continuous.

theorem LeanPool.SemicircleLaw.measurable_semicirclePDFReal (μ : ℝ) (v : NNReal) : Measurable (semicirclePDFReal μ v)

The semicircle pdf is measurable.

theorem LeanPool.SemicircleLaw.stronglyMeasurable_semicirclePDFReal (μ : ℝ) (v : NNReal) : MeasureTheory.StronglyMeasurable (semicirclePDFReal μ v)

The semicircle pdf is strongly measurable.

theorem LeanPool.SemicircleLaw.support_semicirclePDFReal_subset (μ : ℝ) (v : NNReal) : Function.support (semicirclePDFReal μ v) ⊆ Set.Icc (μ - 2 * √↑v) (μ + 2 * √↑v)

The support of the semicircle pdf is contained in [μ - 2√v, μ + 2√v].

theorem LeanPool.SemicircleLaw.integrable_semicirclePDFReal (μ : ℝ) (v : NNReal) : MeasureTheory.Integrable (semicirclePDFReal μ v) MeasureTheory.volume

The semicircle pdf is integrable.

theorem LeanPool.SemicircleLaw.sqrt_semicircle_affine (v : NNReal) {y : ℝ} (hy : y ∈ Set.Icc (-1) 1) : √(4 * ↑v - (2 * √↑v * y) ^ 2) = 2 * √↑v * √(1 - y ^ 2)

theorem LeanPool.SemicircleLaw.integral_sqrt_semicircle_interval (μ : ℝ) {v : NNReal} (hv : v ≠ 0) : ∫ (x : ℝ) in μ - 2 * √↑v..μ + 2 * √↑v, √(4 * ↑v - (x - μ) ^ 2) = 2 * Real.pi * ↑v

The unnormalized semicircle kernel has integral 2 * π * v over its support interval.

theorem LeanPool.SemicircleLaw.integral_semicirclePDFReal_eq_one (μ : ℝ) {v : NNReal} (hv : v ≠ 0) : ∫ (x : ℝ), semicirclePDFReal μ v x = 1

The semicircle distribution pdf integrates to 1 when the variance is nonzero.

theorem LeanPool.SemicircleLaw.lintegral_semicirclePDFReal_eq_one (μ : ℝ) {v : NNReal} (hv : v ≠ 0) : ∫⁻ (x : ℝ), ENNReal.ofReal (semicirclePDFReal μ v x) = 1

The semicircle distribution pdf has total mass 1 when the variance is nonzero.

noncomputable def LeanPool.SemicircleLaw.semicirclePDF (μ : ℝ) (v : NNReal) (x : ℝ) : ENNReal

The ℝ≥0∞-valued pdf of a semicircle distribution on ℝ with mean μ and variance v.

Equations

• LeanPool.SemicircleLaw.semicirclePDF μ v x = ENNReal.ofReal (LeanPool.SemicircleLaw.semicirclePDFReal μ v x)

theorem LeanPool.SemicircleLaw.semicirclePDF_def (μ : ℝ) (v : NNReal) : semicirclePDF μ v = fun (x : ℝ) => ENNReal.ofReal (semicirclePDFReal μ v x)

@[simp]

theorem LeanPool.SemicircleLaw.semicirclePDF_zero_var (μ : ℝ) : semicirclePDF μ 0 = 0

@[simp]

theorem LeanPool.SemicircleLaw.toReal_semicirclePDF {μ : ℝ} {v : NNReal} (x : ℝ) : (semicirclePDF μ v x).toReal = semicirclePDFReal μ v x

theorem LeanPool.SemicircleLaw.semicirclePDF_lt_top {μ : ℝ} {v : NNReal} {x : ℝ} : semicirclePDF μ v x < ⊤

theorem LeanPool.SemicircleLaw.semicirclePDF_ne_top {μ : ℝ} {v : NNReal} {x : ℝ} : semicirclePDF μ v x ≠ ⊤

theorem LeanPool.SemicircleLaw.measurable_semicirclePDF (μ : ℝ) (v : NNReal) : Measurable (semicirclePDF μ v)

@[simp]

theorem LeanPool.SemicircleLaw.lintegral_semicirclePDF_eq_one (μ : ℝ) {v : NNReal} (hv : v ≠ 0) : ∫⁻ (x : ℝ), semicirclePDF μ v x = 1

noncomputable def LeanPool.SemicircleLaw.semicircleReal (μ : ℝ) (v : NNReal) : MeasureTheory.Measure ℝ

A semicircle distribution on ℝ with mean μ and variance v.

Equations

• LeanPool.SemicircleLaw.semicircleReal μ v = if v = 0 then MeasureTheory.Measure.dirac μ else MeasureTheory.volume.withDensity (LeanPool.SemicircleLaw.semicirclePDF μ v)

theorem LeanPool.SemicircleLaw.semicircleReal_of_var_ne_zero (μ : ℝ) {v : NNReal} (hv : v ≠ 0) : semicircleReal μ v = MeasureTheory.volume.withDensity (semicirclePDF μ v)

@[simp]

theorem LeanPool.SemicircleLaw.semicircleReal_zero_var (μ : ℝ) : semicircleReal μ 0 = MeasureTheory.Measure.dirac μ

instance LeanPool.SemicircleLaw.instIsProbabilityMeasureSemicircleReal (μ : ℝ) (v : NNReal) : MeasureTheory.IsProbabilityMeasure (semicircleReal μ v)

theorem LeanPool.SemicircleLaw.semicirclePDFReal_eq_zero_of_notMem (μ : ℝ) (v : NNReal) {x : ℝ} (hx : x ∉ Set.Icc (μ - 2 * √↑v) (μ + 2 * √↑v)) : semicirclePDFReal μ v x = 0

The semicircle pdf vanishes outside the support [μ - 2√v, μ + 2√v].

theorem LeanPool.SemicircleLaw.semicirclePDFReal_sub {μ : ℝ} {v : NNReal} (x y : ℝ) : semicirclePDFReal μ v (x - y) = semicirclePDFReal (μ + y) v x

Translating the input translates the mean in the opposite direction.

theorem LeanPool.SemicircleLaw.semicirclePDFReal_add {μ : ℝ} {v : NNReal} (x y : ℝ) : semicirclePDFReal μ v (x + y) = semicirclePDFReal (μ - y) v x

Translating the input translates the mean in the opposite direction.

theorem LeanPool.SemicircleLaw.semicirclePDFReal_inv_mul {μ : ℝ} {v : NNReal} {c : ℝ} (hc : c ≠ 0) (x : ℝ) : semicirclePDFReal μ v (c⁻¹ * x) = |c| * semicirclePDFReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v) x

Scaling the input rescales both the mean and variance parameters of the density.

theorem LeanPool.SemicircleLaw.semicirclePDFReal_mul {μ : ℝ} {v : NNReal} {c : ℝ} (hc : c ≠ 0) (x : ℝ) : semicirclePDFReal μ v (c * x) = |c⁻¹| * semicirclePDFReal (c⁻¹ * μ) (NNReal.mk (c ^ 2)⁻¹ ⋯ * v) x

Scaling the input rescales both the mean and variance parameters of the density.

theorem LeanPool.SemicircleLaw.semicirclePDF_nonneg (μ : ℝ) (v : NNReal) (x : ℝ) : 0 ≤ semicirclePDF μ v x

The ℝ≥0∞-valued semicircle density is nonnegative.

theorem LeanPool.SemicircleLaw.support_semicirclePDF_subset (μ : ℝ) (v : NNReal) : Function.support (semicirclePDF μ v) ⊆ Set.Icc (μ - 2 * √↑v) (μ + 2 * √↑v)

The support of the ℝ≥0∞-valued semicircle density is contained in its support interval.

theorem LeanPool.SemicircleLaw.semicirclePDF_eq_zero_of_notMem (μ : ℝ) (v : NNReal) {x : ℝ} (hx : x ∉ Set.Icc (μ - 2 * √↑v) (μ + 2 * √↑v)) : semicirclePDF μ v x = 0

The ℝ≥0∞-valued semicircle density vanishes outside its support interval.

theorem LeanPool.SemicircleLaw.noAtoms_semicircleReal {μ : ℝ} {v : NNReal} (hv : v ≠ 0) : MeasureTheory.NoAtoms (semicircleReal μ v)

The semicircle measure has no atoms when the variance is nonzero.

theorem LeanPool.SemicircleLaw.semicircleReal_apply (μ : ℝ) {v : NNReal} (hv : v ≠ 0) (s : Set ℝ) : (semicircleReal μ v) s = ∫⁻ (x : ℝ) in s, semicirclePDF μ v x

The semicircle measure of a set is the set integral of the density when v ≠ 0.

theorem LeanPool.SemicircleLaw.semicircleReal_apply_eq_integral (μ : ℝ) {v : NNReal} (hv : v ≠ 0) (s : Set ℝ) : (semicircleReal μ v) s = ENNReal.ofReal (∫ (x : ℝ) in s, semicirclePDFReal μ v x)

The semicircle measure of a set as a real integral of the density when v ≠ 0.

theorem LeanPool.SemicircleLaw.semicircleReal_absolutelyContinuous (μ : ℝ) {v : NNReal} (hv : v ≠ 0) : (semicircleReal μ v).AbsolutelyContinuous MeasureTheory.volume

The semicircle measure is absolutely continuous with respect to the Lebesgue measure when the variance is nonzero.

theorem LeanPool.SemicircleLaw.rnDeriv_semicircleReal (μ : ℝ) (v : NNReal) : (semicircleReal μ v).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] semicirclePDF μ v

The Radon-Nikodym derivative of the semicircle measure with respect to the Lebesgue measure equals the pdf almost everywhere when the variance is nonzero.

theorem LeanPool.SemicircleLaw.integral_semicircleReal_eq_integral_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : ℝ} {v : NNReal} {f : ℝ → E} (hv : v ≠ 0) : ∫ (x : ℝ), f x ∂semicircleReal μ v = ∫ (x : ℝ), semicirclePDFReal μ v x • f x

Integrating against a non-degenerate semicircle measure is integrating against its density.

theorem MeasurableEmbedding.semicircleReal_comap_apply {μ : ℝ} {v : NNReal} (hv : v ≠ 0) {f : ℝ → ℝ} (hf : MeasurableEmbedding f) {f' : ℝ → ℝ} (h_deriv : ∀ (x : ℝ), HasDerivAt f (f' x) x) {s : Set ℝ} (hs : MeasurableSet s) : (MeasureTheory.Measure.comap f (LeanPool.SemicircleLaw.semicircleReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * LeanPool.SemicircleLaw.semicirclePDFReal μ v (f x))

theorem MeasurableEquiv.semicircleReal_map_symm_apply {μ : ℝ} {v : NNReal} (hv : v ≠ 0) (f : ℝ ≃ᵐ ℝ) {f' : ℝ → ℝ} (h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x) {s : Set ℝ} (hs : MeasurableSet s) : (MeasureTheory.Measure.map (⇑f.symm) (LeanPool.SemicircleLaw.semicircleReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * LeanPool.SemicircleLaw.semicirclePDFReal μ v (f x))

theorem LeanPool.SemicircleLaw.semicircleReal_map_add_const {μ : ℝ} {v : NNReal} (y : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => x + y) (semicircleReal μ v) = semicircleReal (μ + y) v

The map of a semicircle distribution by addition of a constant is semicircular.

theorem LeanPool.SemicircleLaw.semicircleReal_map_const_add {μ : ℝ} {v : NNReal} (y : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => y + x) (semicircleReal μ v) = semicircleReal (μ + y) v

The map of a semicircle distribution by addition of a constant is semicircular.

theorem LeanPool.SemicircleLaw.semicircleReal_map_const_mul {μ : ℝ} {v : NNReal} (c : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => c * x) (semicircleReal μ v) = semicircleReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

The map of a semicircle distribution by multiplication by a constant is semicircular.

theorem LeanPool.SemicircleLaw.semicircleReal_map_mul_const {μ : ℝ} {v : NNReal} (c : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => x * c) (semicircleReal μ v) = semicircleReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)

The map of a semicircle distribution by multiplication by a constant is semicircular.

theorem LeanPool.SemicircleLaw.semicircleReal_map_neg {μ : ℝ} {v : NNReal} : MeasureTheory.Measure.map (fun (x : ℝ) => -x) (semicircleReal μ v) = semicircleReal (-μ) v

theorem LeanPool.SemicircleLaw.semicircleReal_map_div_const {μ : ℝ} {v : NNReal} (c : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => x / c) (semicircleReal μ v) = semicircleReal (μ / c) (v / NNReal.mk (c ^ 2) ⋯)

The map of a semicircle distribution by division by a constant is semicircular.

theorem LeanPool.SemicircleLaw.semicircleReal_map_sub_const {μ : ℝ} {v : NNReal} (y : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => x - y) (semicircleReal μ v) = semicircleReal (μ - y) v

theorem LeanPool.SemicircleLaw.semicircleReal_map_const_sub {μ : ℝ} {v : NNReal} (y : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => y - x) (semicircleReal μ v) = semicircleReal (y - μ) v

theorem LeanPool.SemicircleLaw.semicircleReal_add_const {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (semicircleReal μ v) P) (y : ℝ) : ProbabilityTheory.HasLaw (fun (ω : Ω) => X ω + y) (semicircleReal (μ + y) v) P

If X has semicircular law with mean μ and variance v, then X + y has semicircular law with mean μ + y and variance v.

theorem LeanPool.SemicircleLaw.semicircleReal_const_add {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (semicircleReal μ v) P) (y : ℝ) : ProbabilityTheory.HasLaw (fun (ω : Ω) => y + X ω) (semicircleReal (μ + y) v) P

If X has semicircular law with mean μ and variance v, then y + X has semicircular law with mean μ + y and variance v.

theorem LeanPool.SemicircleLaw.semicircleReal_sub_const {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (semicircleReal μ v) P) (y : ℝ) : ProbabilityTheory.HasLaw (fun (ω : Ω) => X ω - y) (semicircleReal (μ - y) v) P

If X has semicircular law with mean μ and variance v, then X - y has semicircular law with mean μ - y and variance v.

theorem LeanPool.SemicircleLaw.semicircleReal_const_mul {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (semicircleReal μ v) P) (c : ℝ) : ProbabilityTheory.HasLaw (fun (ω : Ω) => c * X ω) (semicircleReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)) P

If X has semicircular law with mean μ and variance v, then c * X has semicircular law with mean c * μ and variance c ^ 2 * v.

theorem LeanPool.SemicircleLaw.semicircleReal_mul_const {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (semicircleReal μ v) P) (c : ℝ) : ProbabilityTheory.HasLaw (fun (ω : Ω) => X ω * c) (semicircleReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)) P

If X has semicircular law with mean μ and variance v, then X * c has semicircular law with mean c * μ and variance c ^ 2 * v.

theorem LeanPool.SemicircleLaw.semicircleReal_neg {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (semicircleReal μ v) P) : ProbabilityTheory.HasLaw (-X) (semicircleReal (-μ) v) P

theorem LeanPool.SemicircleLaw.semicircleReal_div_const {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (semicircleReal μ v) P) (c : ℝ) : ProbabilityTheory.HasLaw (fun (ω : Ω) => X ω / c) (semicircleReal (μ / c) (v / NNReal.mk (c ^ 2) ⋯)) P

If X has semicircular law with mean μ and variance v, then X / c has semicircular law with mean μ / c and variance v / c ^ 2.

theorem LeanPool.SemicircleLaw.semicircleReal_const_sub {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hX : ProbabilityTheory.HasLaw X (semicircleReal μ v) P) (y : ℝ) : ProbabilityTheory.HasLaw (fun (ω : Ω) => y - X ω) (semicircleReal (y - μ) v) P

theorem LeanPool.SemicircleLaw.ae_abs_id_le_semicircleReal {μ : ℝ} {v : NNReal} : ∀ᵐ (x : ℝ) ∂semicircleReal μ v, |id x| ≤ |μ| + 2 * √↑v

The identity is almost surely bounded under a semicircle distribution.

theorem LeanPool.SemicircleLaw.memLp_id_semicircleReal {μ : ℝ} {v : NNReal} (p : NNReal) : MeasureTheory.MemLp id (↑p) (semicircleReal μ v)

All finite moments of a real semicircle distribution are finite.

theorem LeanPool.SemicircleLaw.memLp_id_semicircleReal' {μ : ℝ} {v : NNReal} (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp id p (semicircleReal μ v)

All finite moments of a real semicircle distribution are finite.

@[simp]

theorem LeanPool.SemicircleLaw.support_semicirclePDF {μ : ℝ} {v : NNReal} (hv : v ≠ 0) : Function.support (semicirclePDF μ v) = Set.Ioo (μ - 2 * √↑v) (μ + 2 * √↑v)

The support of the semicircle pdf with mean μ and variance v is the open interval (μ - 2√v, μ + 2√v).

theorem LeanPool.SemicircleLaw.semicirclePDF_toReal (μ : ℝ) (v : NNReal) (x : ℝ) (h₀ : 0 ≤ semicirclePDFReal μ v x) : (ENNReal.ofReal (semicirclePDFReal μ v x)).toReal = semicirclePDFReal μ v x

The real part of the ℝ≥0∞-valued semicircle density coincides with the real-valued density, when the latter is nonnegative.

theorem LeanPool.SemicircleLaw.measurable_ofNNReal : Measurable ENNReal.ofNNReal

The canonical inclusion of ℝ≥0 into ℝ≥0∞ is measurable.

theorem LeanPool.SemicircleLaw.integral_cos_pow_even (n : ℕ) : ∫ (x : ℝ) in 0..Real.pi, Real.cos x ^ (2 * n) = Real.pi * ∏ k ∈ Finset.range n, (2 * ↑k + 1) / (2 * (↑k + 1))

The integral of an even power of cosine over [0, π], as a Wallis-type product.

theorem LeanPool.SemicircleLaw.prod_two_mul_factorial (n : ℕ) : ∏ x ∈ Finset.range n, 2 * (↑x + 1) = 2 ^ n * ↑n.factorial

The product ∏_{x < n} 2 * (x + 1) equals 2 ^ n * n!.

theorem LeanPool.SemicircleLaw.prod_odd_over_even_central_choose (n : ℕ) : (∏ x ∈ Finset.range n, (2 * ↑x + 1)) / ∏ x ∈ Finset.range n, 2 * (↑x + 1) = ↑((2 * n).choose n) / 2 ^ (2 * n)

The Wallis product ratio equals the central binomial coefficient divided by 4 ^ n.

theorem LeanPool.SemicircleLaw.catalan_recur (n : ℕ) : (n + 2) * catalan (n + 1) = (4 * n + 2) * catalan n

The Catalan numbers satisfy the recurrence (n + 2) * C_{n+1} = (4n + 2) * C_n.

theorem LeanPool.SemicircleLaw.integral_even_pow_mul_sqrt_eq_cos_diff (n : ℕ) : ∫ (x : ℝ) in -2..2, x ^ (2 * n) * √(4 - x ^ 2) = 2 ^ (2 * n + 2) * ((∫ (x : ℝ) in 0..Real.pi, Real.cos x ^ (2 * n)) - ∫ (x : ℝ) in 0..Real.pi, Real.cos x ^ (2 * n + 2))

Reduction of ∫_{-2}^{2} x ^ (2n) √(4 - x ^ 2) to a difference of even cosine-power integrals over [0, π].

@[simp]

theorem LeanPool.SemicircleLaw.integral_id_semicircleReal {μ : ℝ} {v : NNReal} : ∫ (x : ℝ), x ∂semicircleReal μ v = μ

The mean of a real semicircle distribution semicircleReal μ v is its mean parameter μ.

theorem LeanPool.SemicircleLaw.integral_scaled_semicircle_eq (v : NNReal) (n : ℕ) (hv : v ≠ 0) : 1 / (2 * Real.pi * ↑v) * ∫ (x : ℝ) in -2 * √↑v..2 * √↑v, x ^ (2 * n) * √(4 * ↑v - x ^ 2) = ↑v ^ n / (2 * Real.pi) * ∫ (x : ℝ) in -2..2, x ^ (2 * n) * √(4 - x ^ 2)

The substitution x ↦ x * √v rescales the centered semicircle moment integral to the standard interval [-2, 2].

theorem LeanPool.SemicircleLaw.wallis_prod_diff_eq_catalan (n : ℕ) : 2 ^ (2 * n + 1) * (∏ i ∈ Finset.range n, (2 * ↑i + 1) / (2 * (↑i + 1)) - ∏ i ∈ Finset.range (n + 1), (2 * ↑i + 1) / (2 * (↑i + 1))) = ↑(catalan n)

The Wallis product telescopes: 2 ^ (2n+1) times the difference of consecutive Wallis partial products equals the n-th Catalan number.

theorem LeanPool.SemicircleLaw.integral_centered_pow_semicircleReal (μ : ℝ) (v : NNReal) (n : ℕ) (hv : v ≠ 0) : ∫ (x : ℝ), (x - μ) ^ (2 * n) ∂semicircleReal μ v = 1 / (2 * Real.pi * ↑v) * ∫ (x : ℝ) in -2 * √↑v..2 * √↑v, x ^ (2 * n) * √(4 * ↑v - x ^ 2)

The centered 2 * n-th power integral against the semicircle measure, rewritten as a weighted integral of the unnormalized kernel over its centered support interval.

theorem LeanPool.SemicircleLaw.centralMoment_fun_two_mul_semicircleReal (μ : ℝ) (v : NNReal) (n : ℕ) : ProbabilityTheory.centralMoment (fun (x : ℝ) => x) (2 * n) (semicircleReal μ v) = ↑v ^ n * ↑(catalan n)

The 2 * n-th central moment of the semicircle distribution equals v ^ n times the n-th Catalan number.

theorem LeanPool.SemicircleLaw.centralMoment_two_mul_semicircleReal (μ : ℝ) (v : NNReal) (n : ℕ) : ProbabilityTheory.centralMoment id (2 * n) (semicircleReal μ v) = ↑v ^ n * ↑(catalan n)

The 2 * n-th central moment of the identity equals v ^ n times the n-th Catalan number.

@[simp]

theorem LeanPool.SemicircleLaw.variance_id_semicircleReal {μ : ℝ} {v : NNReal} : ProbabilityTheory.variance id (semicircleReal μ v) = ↑v

The variance of a real semicircle distribution semicircleReal μ v is its variance parameter v.

@[simp]

theorem LeanPool.SemicircleLaw.variance_fun_id_semicircleReal {μ : ℝ} {v : NNReal} : ProbabilityTheory.variance (fun (x : ℝ) => x) (semicircleReal μ v) = ↑v

The variance of a real semicircle distribution semicircleReal μ v is its variance parameter v.

theorem LeanPool.SemicircleLaw.centralMoment_fun_odd_semicircleReal (μ : ℝ) (v : NNReal) (n : ℕ) : ProbabilityTheory.centralMoment (fun (x : ℝ) => x) (2 * n + 1) (semicircleReal μ v) = 0

The odd central moments of the semicircle distribution vanish.

theorem LeanPool.SemicircleLaw.centralMoment_odd_semicircleReal (μ : ℝ) (v : NNReal) (n : ℕ) : ProbabilityTheory.centralMoment id (2 * n + 1) (semicircleReal μ v) = 0

The odd central moments of the identity vanish.