On this page

GaussianAnalysisprobabilitysemicircle_law

The semicircle law

GaussianAnalysis.probability.semicircle_lawlibrary/probability/semicircle_law.v813 lines31 lemmas and theorems, 2 definitionssource

Imports 1 library modules and 28 external

GaussianAnalysis.comparison.normal_linear

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.analysis.trigo, mathcomp.analysis.derive, mathcomp.analysis.realfun, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.numfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.ftc, mathcomp.analysis.charge

Imported by 1

GaussianAnalysis.random_matrix.wigner

Required by 12 files of the paper proofs

The semicircle law of radius r > 0 has the density 2 / (pi r^2) sqrt (r^2 - x^2) on [-r, r] with respect to Lebesgue measure. Its variance is r^2 / 4. Wigner's semicircle law for a GOE matrix scaled by 1 / sqrt d has radius 2, and the law nu of Koehler and Sohn (arXiv 2608.27372, lines 345-349), of density sqrt (2 - x^2) / pi, has radius sqrt 2. As MathComp-Analysis does for normal_pdf m 0, the density at r = 0 is the indicator of [0, 1], so that semicircle_prob r is a probability for every r.

Main results:

Rintegral_sqrt_disk: \int_{-a}^{a} sqrt (a^2 - x^2) dx = pi a^2 / 2 for a > 0, by the substitution x = a sin t (Rintegral_cos2: \int_{-pi/2}^{pi/2} cos^2 = pi / 2).
integral_semicircle_pdf: the density has integral one; hence semicircle_prob r is a probability on measurableTypeR R, and semicircle_prob_dominates: it is absolutely continuous with respect to Lebesgue measure.
ge0_integral_semicircle_prob, integrable_semicircle_prob, integral_semicircle_prob: integrating against semicircle_prob r is integrating against Lebesgue measure with the density, for nonnegative or integrable functions; semicircle_integrable_eq, semicircle_integral_eq: the same for a function g that agrees with f where the density is positive.
semicircle_prob_sym: for r != 0 the law is invariant under x |-> -x.
For r != 0: integrable_semicircle_continuous, integrable_semicircle_pdfM (every continuous function f is integrable, and so is f times the density), Rintegral_semicircle (its integral is the integral of f times the density over [-|r|, |r|]), semicircle_prob_gt0 (every half-line ]b, +oo[ with b < |r| has positive measure), semicircle_restrict (if f times the density is integrable, some measurable g that is f or 0 at each point has g times the density equal to f times the density: f restricted to ]-|r|, |r|[).
semicircle_momentS: E X^(k+2) = (k + 1) r^2 / (k + 4) E X^k, by integration by parts against (r^2 - x^2)^(3/2); semicircle_moment0, semicircle_moment1, semicircle_moment2, semicircle_moment_odd: E 1 = 1, E X = 0, E X^2 = r^2 / 4, and the odd moments vanish. At r = 2 the even moments are the Catalan numbers.
semicircle_pdf_scale, ge0_integral_semicircle_scale: for r, a > 0, the semicircle law of radius a r is the image of the one of radius r under x |-> a x (by the affine change of variables of comparison/normal_linear.v).

`semicircle_pdf r x`	2 / (pi r^2) sqrt (r^2 - x^2), zero outside [-r, r] since Num.sqrt is zero on negative numbers; the indicator of [0, 1] if r = 0
`semicircle_prob r`	the measure with density semicircle_pdf r with respect to Lebesgue measure

Main results

Results	Statement
semicircle_pdfsemicircle_probintegral_semicircle_pdfRintegral_sqrt_disk	The semicircle law of radius `r`, of density `2 / (pi r^2) sqrt (r^2 - x^2)` on `[-r, r]`, is a probability (for `r = 0` the density is the indicator of `[0, 1]`, as for `normal_pdf m 0`); the half disk has area `pi a^2 / 2`, computed by the substitution `x = a sin t`.
integral_semicircle_probge0_integral_semicircle_probintegrable_semicircle_probsemicircle_integrable_eqsemicircle_integral_eqRintegral_semicircleintegrable_semicircle_continuousintegrable_semicircle_pdfM	Integrating against the semicircle law is integrating against Lebesgue measure with its density, over `[-\|r\|, \|r\|]`, also for a function `g` that agrees with `f` where the density is positive; every continuous function `f` is integrable, and so is `f` times the density.
semicircle_prob_symsemicircle_prob_gt0semicircle_restrict	For `r != 0` the law is invariant under `x \|-> -x`, every half-line `]b, +oo[` with `b < \|r\|` has positive probability, and a function `f` with `f` times the density integrable has a measurable restriction to `]-\|r\|, \|r\|[` with the same products with the density.
semicircle_momentSsemicircle_moment1semicircle_moment2semicircle_moment_odd	Moments: `E X^(k+2) = (k + 1) r^2 / (k + 4) E X^k` (integration by parts), so the odd moments vanish, `E X^2 = r^2 / 4`, and at `r = 2` the even moments are the Catalan numbers.
semicircle_pdf_scalege0_integral_semicircle_scale	The semicircle laws form a scale family: `a p_{a r}(a x) = p_r(x)`, and `int f(a x) dsigma_r(x) = int f dsigma_{a r}` for `a > 0` and `f >= 0` measurable.

Declarations35 exported, 15 local

sectiondisk_integral

Context {R : realType}.
Local Notation mu := (@lebesgue_measure R).

lemma Rintegral_FTC_R source, line 79

forall {R : realType} [f F : R -> R] [a b : R],
a < b ->
continuous f ->
(forall x : R, is_derive x 1 F (f x)) ->
\int[lebesgue_measure]_(x in `[a, b]) f x = F b - F a

The fundamental theorem of calculus, for an antiderivative on R.

Statement as written in the source

Lemma Rintegral_FTC_R (f F : R -> R) (a b : R) : a < b -> continuous f ->
  (forall x : R, is_derive x 1 F (f x)) ->
  \int[mu]_(x in `[a, b]) f x = F b - F a.

Used by 1 declaration in 1 file

this file: Rintegral_cos2

lemma Rintegral_cos2 source, line 100

forall {R : realType},
\int[lebesgue_measure]_(t in `[- (pi / 2), pi / 2]) cos t ^+ 2 = pi / 2

\int_{-pi/2}^{pi/2} cos^2 = pi / 2.

Statement as written in the source

Lemma Rintegral_cos2 :
  \int[mu]_(t in `[- (pi / 2), pi / 2]) cos t ^+ 2 = pi / 2 :> R.

Used by 1 declaration in 1 file

this file: Rintegral_sqrt_disk

lemma Rintegral_sqrt_disk main result source, line 126

forall {R : realType} [a : R],
0 < a ->
\int[lebesgue_measure]_(x in `[- a, a]) Num.ExtraDef.sqrtr (a ^+ 2 - x ^+ 2) =
pi / 2 * a ^+ 2

The area of the half disk: \int_{-a}^{a} sqrt (a^2 - x^2) dx = pi a^2 / 2, by the substitution x = a sin t.

Main result

Stated in the README together with semicircle_pdf.

Statement as written in the source

Lemma Rintegral_sqrt_disk (a : R) : 0 < a ->
  \int[mu]_(x in `[- a, a]) Num.sqrt (a ^+ 2 - x ^+ 2) = pi / 2 * a ^+ 2.

Used by 1 declaration in 1 file

this file: integral_semicircle_pdf

sectionsemicircle_density

Context {R : realType}.
Local Notation mu := (@lebesgue_measure R).

definition semicircle_pdf main result source, line 192

Type

forall {R : realType}, R -> R -> R

Definition

Definition semicircle_pdf (r x : R) : R :=
  if r == 0 then \1_`[0, 1] x
  else 2 / (pi * r ^+ 2) * Num.sqrt (r ^+ 2 - x ^+ 2).

Main result, as the README states it

The semicircle law of radius r, of density 2 / (pi r^2) sqrt (r^2 - x^2) on [-r, r], is a probability (for r = 0 the density is the indicator of [0, 1], as for normal_pdf m 0); the half disk has area pi a^2 / 2, computed by the substitution x = a sin t.

Used by 26 declarations in 1 file

this file: semicircle_pdfE, semicircle_pdf_ge0, semicircle_pdfN, semicircle_pdf_out, continuous_semicircle_pdf, measurable_semicircle_pdf, integral_semicircle_pdf_support, integral_semicircle_pdf, integrable_semicircle_pdf, semicircle_prob, semicircle_prob_dominates, RN_pdf, ge0_integral_semicircle_prob, integrable_semicircle_prob, integral_semicircle_prob, semicircle_integrable_eq, semicircle_integral_eq, semicircle_prob_sym, pdf_out, integrable_semicircle_continuous, integrable_semicircle_pdfM, Rintegral_semicircle, semicircle_prob_gt0, semicircle_restrict, semicircle_pdf_scale, ge0_integral_semicircle_scale

lemma semicircle_pdfE source, line 196

forall {R : realType}
  [r : join_Algebra_ChoiceBaseAddUMagma_between_Algebra_BaseAddUMagma_and_eqtype_Equality R]
  (x : R),
r != 0 -> semicircle_pdf r x = 2 / (pi * r ^+ 2) * Num.ExtraDef.sqrtr (r ^+ 2 - x ^+ 2)

Statement as written in the source

Lemma semicircle_pdfE r x : r != 0 ->
  semicircle_pdf r x = 2 / (pi * r ^+ 2) * Num.sqrt (r ^+ 2 - x ^+ 2).

Used by 8 declarations in 1 file

this file: semicircle_pdfN, semicircle_pdf_out, continuous_semicircle_pdf, integral_semicircle_pdf, moment_I, semicircle_prob_gt0, semicircle_restrict, semicircle_pdf_scale

lemma semicircle_pdf_ge0 source, line 200

forall {R : realType} (r x : R), 0 <= semicircle_pdf r x

Statement as written in the source

Lemma semicircle_pdf_ge0 r x : 0 <= semicircle_pdf r x.

Used by 9 declarations in 1 file

this file: integrable_semicircle_pdf, P_ge0, P_sigma_additive, semicircle_prob_dominates, integrable_semicircle_prob, integral_semicircle_prob, semicircle_prob_sym, semicircle_prob_gt0, ge0_integral_semicircle_scale

lemma semicircle_pdfN source, line 207

forall {R : realType}
  [r : join_Algebra_ChoiceBaseAddUMagma_between_Algebra_BaseAddUMagma_and_eqtype_Equality R]
  (x : R),
r != 0 -> semicircle_pdf r (- x) = semicircle_pdf r x

Statement as written in the source

Lemma semicircle_pdfN r x : r != 0 ->
  semicircle_pdf r (- x) = semicircle_pdf r x.

Used by 1 declaration in 1 file

this file: semicircle_prob_sym

lemma semicircle_pdf_out source, line 211

forall {R : realType}
  [r : join_Algebra_ChoiceBaseAddUMagma_between_Algebra_BaseAddUMagma_and_eqtype_Equality
         (join_Num_NumDomain_between_Order_Preorder_and_GRing_PzSemiRing R)]
  [x : join_Num_NumDomain_between_Order_Preorder_and_GRing_PzSemiRing R],
r != 0 -> r ^+ 2 <= x ^+ 2 -> semicircle_pdf r x = 0

Statement as written in the source

Lemma semicircle_pdf_out r x : r != 0 -> r ^+ 2 <= x ^+ 2 ->
  semicircle_pdf r x = 0.

Used by 3 declarations in 1 file

this file: integral_semicircle_pdf_support, pdf_out, semicircle_restrict

lemma continuous_semicircle_pdf source, line 217

forall {R : realType}
  [r : join_Algebra_ChoiceBaseAddUMagma_between_Algebra_BaseAddUMagma_and_eqtype_Equality R],
r != 0 -> continuous (semicircle_pdf r)

Statement as written in the source

Lemma continuous_semicircle_pdf r : r != 0 -> continuous (semicircle_pdf r).

Used by 4 declarations in 1 file

this file: measurable_semicircle_pdf, integral_semicircle_pdf, integrable_semicircle_continuous, semicircle_restrict

lemma measurable_semicircle_pdf source, line 227

forall {R : realType} (r : R), measurable_fun [set: R] (semicircle_pdf r)

Statement as written in the source

Lemma measurable_semicircle_pdf r : measurable_fun [set: R] (semicircle_pdf r).

Used by 8 declarations in 1 file

this file: integrable_semicircle_pdf, semicircle_prob_dominates, RN_pdf, ge0_integral_semicircle_prob, integrable_semicircle_prob, semicircle_prob_sym, semicircle_prob_gt0, ge0_integral_semicircle_scale

lemma integral_semicircle_pdf_support source, line 236

forall {R : realType}
  [r : join_Algebra_ChoiceBaseAddUMagma_between_Algebra_BaseAddUMagma_and_eqtype_Equality R],
r != 0 ->
(\int[lebesgue_measure]_x (semicircle_pdf r x)%:E)%E =
(\int[lebesgue_measure]_(x in `[(- `|r|)%R, `|r|%R]) (semicircle_pdf r x)%:E)%E

Statement as written in the source

Lemma integral_semicircle_pdf_support r : r != 0 ->
  (\int[mu]_x (semicircle_pdf r x)%:E =
   \int[mu]_(x in `[(- `|r|)%R, `|r|%R]) (semicircle_pdf r x)%:E)%E.

Used by 1 declaration in 1 file

this file: integral_semicircle_pdf

lemma integral_semicircle_pdf main result source, line 250

forall {R : realType} (r : R), (\int[lebesgue_measure]_x (semicircle_pdf r x)%:E)%E = 1%E

Main result

Stated in the README together with semicircle_pdf.

Statement as written in the source

Lemma integral_semicircle_pdf r : (\int[mu]_x (semicircle_pdf r x)%:E = 1)%E.

Used by 2 declarations in 1 file

this file: integrable_semicircle_pdf, P_setT

lemma integrable_semicircle_pdf source, line 278

forall {R : realType} (r : R),
lebesgue_measure.-integrable [set: R]
  (fun
     x : g_sigma_algebraType
           (R.-ocitv).-measurable =>
   (semicircle_pdf r x)%:E)

Statement as written in the source

Lemma integrable_semicircle_pdf r :
  mu.-integrable [set: R] (fun x => (semicircle_pdf r x)%:E).

Used by 1 declaration in 1 file

this file: P_sigma_additive

definition semicircle_prob main result source, line 289

Type

forall {R : realType}, R -> set (measurableTypeR R) -> \bar R

Definition

Definition semicircle_prob {R : realType} (r : R) :
    set (measurableTypeR R) -> \bar R :=
  fun V => (\int[lebesgue_measure]_(x in V) (semicircle_pdf r x)%:E)%E.

Main result

Stated in the README together with semicircle_pdf.

Used by 35 declarations in 2 files

this file: P0, P_ge0, P_sigma_additive, instance at line 321, P_setT, instance at line 326, semicircle_prob_dominates, RN_pdf, ge0_integral_semicircle_prob, integrable_semicircle_prob, integral_semicircle_prob, semicircle_integrable_eq, semicircle_integral_eq, semicircle_prob_sym, integrable_semicircle_continuous, Rintegral_semicircle, moment_I, semicircle_momentS, semicircle_moment0, semicircle_moment2, semicircle_moment_odd, semicircle_moment1, semicircle_prob_gt0, ge0_integral_semicircle_scale
GaussianAnalysis.random_matrix.wigner: semicircle_catalan, goe_moment_cvg, goe_clip_cvg, integrable_semicircle_poly, semicircle_poly, semicircle_clip, goe_stat_clip_mean_cvg, wigner, semicircle_near, wigner_uniform, wigner_uniform_inf

HB declares canonical projections that the structures of the measure already provide; the warning says so. The setting lasts until the end of this file and is not exported.

Set Warnings "-redundant-canonical-projection".

sectionsemicircle_probability

Context {R : realType} (r : R).
Local Notation mu := (@lebesgue_measure R).
Local Notation P := (semicircle_prob r).

let P0 section-local source, line 303

Let P0 : P set0 = 0%E.

Used by 1 declaration in 1 file

this file: instance at line 321

let P_ge0 section-local source, line 306

Let P_ge0 A : (0 <= P A)%E.

Used by 1 declaration in 1 file

this file: instance at line 321

let P_sigma_additive section-local source, line 311

Let P_sigma_additive : semi_sigma_additive P.

Used by 1 declaration in 1 file

this file: instance at line 321

instance instance at line 321 source, line 321

HB.instance Definition _ := isMeasure.Build _ _ _ P P0 P_ge0 P_sigma_additive.

let P_setT section-local source, line 323

Let P_setT : P [set: _] = 1%E.

Used by 1 declaration in 1 file

this file: instance at line 326

instance instance at line 326 source, line 326

HB.instance Definition _ := @Measure_isProbability.Build _ _ R P P_setT.

lemma semicircle_prob_dominates source, line 328

forall {R : realType} (r : R), semicircle_prob r `<< lebesgue_measure

Statement as written in the source

Lemma semicircle_prob_dominates : P `<< mu.

Used by 2 declarations in 1 file

this file: RN_pdf, ge0_integral_semicircle_prob

sectionsemicircle_integral

Context {R : realType} (r : R).
Local Notation mu := (@lebesgue_measure R).
Local Notation P := (semicircle_prob r).

let RN_pdf section-local source, line 345

Let RN_pdf : ae_eq mu [set: R] (Radon_Nikodym_SigmaFinite.f P mu)
  (fun x => (semicircle_pdf r x)%:E).

Used by 1 declaration in 1 file

this file: ge0_integral_semicircle_prob

lemma ge0_integral_semicircle_prob main result source, line 356

forall {R : realType} (r : R) [f : R -> \bar R],
(forall x : R, (0%R <= f x)%E) ->
measurable_fun [set: R] f ->
(\int[semicircle_prob r]_x f x)%E =
(\int[lebesgue_measure]_x (f x * (semicircle_pdf r x)%:E))%E

Main result

Stated in the README together with integral_semicircle_prob.

Statement as written in the source

Lemma ge0_integral_semicircle_prob (f : R -> \bar R) :
  (forall x, (0 <= f x)%E) -> measurable_fun [set: R] f ->
  (\int[P]_x f x = \int[mu]_x (f x * (semicircle_pdf r x)%:E))%E.

Used by 3 declarations in 1 file

this file: integrable_semicircle_prob, integral_semicircle_prob, ge0_integral_semicircle_scale

lemma integrable_semicircle_prob main result source, line 372

forall {R : realType} (r : R) [f : R -> \bar R],
measurable_fun [set: R] f ->
(semicircle_prob r).-integrable [set: R] f <->
lebesgue_measure.-integrable [set: R]
  (fun
     x : g_sigma_algebraType
           (R.-ocitv).-measurable =>
   (f x * (semicircle_pdf r x)%:E)%E)

Main result

Stated in the README together with integral_semicircle_prob.

Statement as written in the source

Lemma integrable_semicircle_prob (f : R -> \bar R) :
  measurable_fun [set: R] f ->
  P.-integrable [set: R] f <->
  mu.-integrable [set: R] (fun x => f x * (semicircle_pdf r x)%:E)%E.

Used by 3 declarations in 1 file

this file: semicircle_integrable_eq, integrable_semicircle_continuous, integrable_semicircle_pdfM

lemma integral_semicircle_prob main result source, line 392

forall {R : realType} [r : R] [f : R -> \bar R],
(semicircle_prob r).-integrable [set: R] f ->
(\int[semicircle_prob r]_x f x)%E =
(\int[lebesgue_measure]_x (f x * (semicircle_pdf r x)%:E))%E

Main result, as the README states it

Integrating against the semicircle law is integrating against Lebesgue measure with its density, over [-|r|, |r|], also for a function g that agrees with f where the density is positive; every continuous function f is integrable, and so is f times the density.

Statement as written in the source

Lemma integral_semicircle_prob (f : R -> \bar R) :
  P.-integrable [set: R] f ->
  (\int[P]_x f x = \int[mu]_x (f x * (semicircle_pdf r x)%:E))%E.

Used by 2 declarations in 1 file

this file: semicircle_integral_eq, Rintegral_semicircle

lemma semicircle_integrable_eq main result source, line 409

forall {R : realType} [r : R] [f g : R -> R],
measurable_fun [set: R] g ->
(forall x : R, g x * semicircle_pdf r x = f x * semicircle_pdf r x) ->
lebesgue_measure.-integrable [set: R]
  (fun
     x : g_sigma_algebraType
           (R.-ocitv).-measurable =>
   (f x * semicircle_pdf r x)%:E) ->
(semicircle_prob r).-integrable [set: R] (EFin \o g)

Main result

Stated in the README together with integral_semicircle_prob.

Statement as written in the source

Lemma semicircle_integrable_eq (f g : R -> R) : measurable_fun [set: R] g ->
  (forall x, g x * semicircle_pdf r x = f x * semicircle_pdf r x) ->
  mu.-integrable [set: R] (fun x => (f x * semicircle_pdf r x)%:E) ->
  P.-integrable [set: R] (EFin \o g).

lemma semicircle_integral_eq main result source, line 418

forall {R : realType} [r : R] [f g : R -> R],
(semicircle_prob r).-integrable [set: R] (EFin \o g) ->
(forall x : R, g x * semicircle_pdf r x = f x * semicircle_pdf r x) ->
\int[semicircle_prob r]_x g x = \int[lebesgue_measure]_x (f x * semicircle_pdf r x)

Main result

Stated in the README together with integral_semicircle_prob.

Statement as written in the source

Lemma semicircle_integral_eq (f g : R -> R) : P.-integrable [set: R] (EFin \o g) ->
  (forall x, g x * semicircle_pdf r x = f x * semicircle_pdf r x) ->
  \int[P]_x g x = \int[mu]_x (f x * semicircle_pdf r x).

lemma semicircle_prob_sym main result source, line 426

forall {R : realType} [r : R] [A : set (measurableTypeR R)],
r != 0 ->
(((R.-ocitv).-measurable).-sigma).-measurable A ->
semicircle_prob r ([eta -%R] @^-1` A) = semicircle_prob r A

Main result, as the README states it

For r != 0 the law is invariant under x |-> -x, every half-line ]b, +oo[ with b < |r| has positive probability, and a function f with f times the density integrable has a measurable restriction to ]-|r|, |r|[ with the same products with the density.

Statement as written in the source

Lemma semicircle_prob_sym (A : set (measurableTypeR R)) : r != 0 ->
  measurable A -> P ((fun x => - x) @^-1` A) = P A.

sectionsemicircle_support

Context {R : realType} (r : R).
Hypothesis r0 : r != 0.
Local Notation mu := (@lebesgue_measure R).
Local Notation P := (semicircle_prob r).
Local Notation a := `|r|.

let a0 section-local source, line 450

Let a0 : 0 < a.

Used by 1 declaration in 1 file

this file: I_odd

let ra section-local source, line 452

Let ra : r ^+ 2 = a ^+ 2.

Used by 4 declarations in 1 file

this file: moment_I, semicircle_momentS, semicircle_prob_gt0, semicircle_restrict

let pdf_out section-local source, line 454

Let pdf_out (x : R) : x \notin `[- a, a] -> semicircle_pdf r x = 0.

Used by 2 declarations in 1 file

this file: integrable_semicircle_continuous, Rintegral_semicircle

let csqrt section-local source, line 464

Let csqrt : continuous (fun x : R => Num.sqrt (a ^+ 2 - x ^+ 2)).

Used by 2 declarations in 1 file

this file: cI, I_rec

lemma integrable_semicircle_continuous main result source, line 470

forall {R : realType} [r : R],
r != 0 ->
forall [f : R -> R], continuous f -> (semicircle_prob r).-integrable [set: R] (EFin \o f)

Main result

Stated in the README together with integral_semicircle_prob.

Statement as written in the source

Lemma integrable_semicircle_continuous (f : R -> R) : continuous f ->
  P.-integrable [set: R] (EFin \o f).

Used by 7 declarations in 2 files

this file: integrable_semicircle_pdfM, moment_I
GaussianAnalysis.random_matrix.wigner: integrable_semicircle_poly, semicircle_poly, semicircle_clip, goe_stat_clip_mean_cvg, semicircle_near

lemma integrable_semicircle_pdfM main result source, line 487

forall {R : realType} [r : R],
r != 0 ->
forall [f : R -> R],
continuous f ->
lebesgue_measure.-integrable [set: R]
  (fun
     x : g_sigma_algebraType
           (R.-ocitv).-measurable =>
   (f x * semicircle_pdf r x)%:E)

Main result

Stated in the README together with integral_semicircle_prob.

Statement as written in the source

Lemma integrable_semicircle_pdfM (f : R -> R) : continuous f ->
  mu.-integrable [set: R] (fun x => (f x * semicircle_pdf r x)%:E).

lemma Rintegral_semicircle main result source, line 497

forall {R : realType} [r : R],
r != 0 ->
forall [f : R -> R],
(semicircle_prob r).-integrable [set: R] (EFin \o f) ->
\int[semicircle_prob r]_x f x =
\int[lebesgue_measure]_(x in `[- `|r|, `|r|]) (f x * semicircle_pdf r x)

Main result

Stated in the README together with integral_semicircle_prob.

Statement as written in the source

Lemma Rintegral_semicircle (f : R -> R) : P.-integrable [set: R] (EFin \o f) ->
  \int[P]_x f x = \int[mu]_(x in `[- a, a]) (f x * semicircle_pdf r x).

Used by 2 declarations in 2 files

this file: moment_I
GaussianAnalysis.random_matrix.wigner: semicircle_clip

let I section-local source, line 506

Let I k := \int[mu]_(x in `[- a, a]) (x ^+ k * Num.sqrt (a ^+ 2 - x ^+ 2)).

Used by 3 declarations in 1 file

this file: I_rec, moment_I, I_odd

let cI section-local source, line 508

Let cI k : continuous (fun x : R => x ^+ k * Num.sqrt (a ^+ 2 - x ^+ 2)).

Used by 3 declarations in 1 file

this file: iI, I_rec, I_odd

let iI section-local source, line 511

Let iI k : mu.-integrable `[- a, a]
  (EFin \o (fun x : R => x ^+ k * Num.sqrt (a ^+ 2 - x ^+ 2))).

let I_rec section-local source, line 518

Let I_rec k : I k.+2 = k.+1%:R * a ^+ 2 / k.+4%:R * I k.

Used by 1 declaration in 1 file

this file: semicircle_momentS

let moment_I section-local source, line 615

Let moment_I k : \int[P]_x ((x : R) ^+ k) = 2 / (pi * a ^+ 2) * I k.

Used by 2 declarations in 1 file

this file: semicircle_momentS, semicircle_moment_odd

lemma semicircle_momentS main result source, line 623

forall {R : realType} [r : R],
r != 0 ->
forall k : nat,
\int[semicircle_prob r]_x (x : R) ^+ k.+2 =
k.+1%:R * r ^+ 2 / k.+4%:R * \int[semicircle_prob r]_x (x : R) ^+ k

Main result, as the README states it

Moments: E X^(k+2) = (k + 1) r^2 / (k + 4) E X^k (integration by parts), so the odd moments vanish, E X^2 = r^2 / 4, and at r = 2 the even moments are the Catalan numbers.

Statement as written in the source

Lemma semicircle_momentS k : \int[P]_x ((x : R) ^+ k.+2) =
  k.+1%:R * r ^+ 2 / k.+4%:R * \int[P]_x ((x : R) ^+ k).

Used by 2 declarations in 2 files

this file: semicircle_moment2
GaussianAnalysis.random_matrix.wigner: semicircle_catalan

lemma semicircle_moment0 source, line 627

forall {R : realType} (r : R), \int[semicircle_prob r]_x (x : R) ^+ 0 = 1

Statement as written in the source

Lemma semicircle_moment0 : \int[P]_x ((x : R) ^+ 0) = 1.

Used by 3 declarations in 2 files

this file: semicircle_moment2
GaussianAnalysis.random_matrix.wigner: semicircle_catalan, goe_moment_cvg

lemma semicircle_moment2 main result source, line 633

forall {R : realType} [r : R],
r != 0 -> \int[semicircle_prob r]_x (x : R) ^+ 2 = r ^+ 2 / 4

Main result

Stated in the README together with semicircle_momentS.

Statement as written in the source

Lemma semicircle_moment2 : \int[P]_x ((x : R) ^+ 2) = r ^+ 2 / 4.

let I_odd section-local source, line 636

Let I_odd k : I k.*2.+1 = 0.

Used by 1 declaration in 1 file

this file: semicircle_moment_odd

lemma semicircle_moment_odd main result source, line 664

forall {R : realType} [r : R],
r != 0 -> forall k : nat, \int[semicircle_prob r]_x (x : R) ^+ k.*2.+1 = 0

Main result

Stated in the README together with semicircle_momentS.

Statement as written in the source

Lemma semicircle_moment_odd k : \int[P]_x ((x : R) ^+ k.*2.+1) = 0.

Used by 3 declarations in 2 files

this file: semicircle_moment1
GaussianAnalysis.random_matrix.wigner: semicircle_catalan, goe_moment_cvg

lemma semicircle_moment1 main result source, line 667

forall {R : realType} [r : R], r != 0 -> \int[semicircle_prob r]_x (x : R) = 0

Main result

Stated in the README together with semicircle_momentS.

Statement as written in the source

Lemma semicircle_moment1 : \int[P]_x (x : R) = 0.

lemma semicircle_prob_gt0 main result source, line 672

forall {R : realType} [r : R],
r != 0 -> forall [b : R], b < `|r| -> (0%R < semicircle_prob r `]b, +oo[)%E

Main result

Stated in the README together with semicircle_prob_sym.

Statement as written in the source

Lemma semicircle_prob_gt0 (b : R) : b < a -> (0 < P `]b, +oo[%classic)%E.

lemma semicircle_restrict main result source, line 727

forall {R : realType} [r : R],
r != 0 ->
forall [f : R -> R],
lebesgue_measure.-integrable [set: R]
  (fun
     x : g_sigma_algebraType
           (R.-ocitv).-measurable =>
   (f x * semicircle_pdf r x)%:E) ->
exists g : R -> R,
  [/\ measurable_fun [set: R] g,
      forall x : R, g x * semicircle_pdf r x = f x * semicircle_pdf r x
    & forall x : R, g x = 0 \/ g x = f x]

Main result

Stated in the README together with semicircle_prob_sym.

Statement as written in the source

Lemma semicircle_restrict (f : R -> R) :
  mu.-integrable [set: R] (fun x => (f x * semicircle_pdf r x)%:E) ->
  exists g : R -> R, [/\ measurable_fun [set: R] g,
    forall x, g x * semicircle_pdf r x = f x * semicircle_pdf r x &
    forall x, g x = 0 \/ g x = f x].

sectionsemicircle_scale

Context {R : realType}.
Local Notation mu := (@lebesgue_measure R).

lemma semicircle_pdf_scale main result source, line 767

forall {R : realType} [r a : R] (x : R),
0 < r -> 0 < a -> a * semicircle_pdf (a * r) (a * x) = semicircle_pdf r x

Main result, as the README states it

The semicircle laws form a scale family: a p_{a r}(a x) = p_r(x), and int f(a x) dsigma_r(x) = int f dsigma_{a r} for a > 0 and f >= 0 measurable.

Statement as written in the source

Lemma semicircle_pdf_scale (r a x : R) : 0 < r -> 0 < a ->
  a * semicircle_pdf (a * r) (a * x) = semicircle_pdf r x.

Used by 1 declaration in 1 file

this file: ge0_integral_semicircle_scale

lemma ge0_integral_semicircle_scale main result source, line 785

forall {R : realType} [r a : R] [f : R -> \bar R],
0 < r ->
0 < a ->
(forall x : R, (0%R <= f x)%E) ->
measurable_fun [set: R] f ->
(\int[semicircle_prob r]_x f (a * x)%R)%E = (\int[semicircle_prob (a * r)]_x f x)%E

The semicircle law of radius a r is the image of the one of radius r under x |-> a x.

Main result

Stated in the README together with semicircle_pdf_scale.

Statement as written in the source

Lemma ge0_integral_semicircle_scale (r a : R) (f : R -> \bar R) :
  0 < r -> 0 < a -> (forall x, (0 <= f x)%E) -> measurable_fun [set: R] f ->
  (\int[semicircle_prob r]_x f (a * x)%R =
   \int[semicircle_prob (a * r)%R]_x f x)%E.

Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.