On this page

Linear images of normal laws

GaussianAnalysis.comparison.normal_linearlibrary/comparison/normal_linear.v246 lines9 lemmas and theoremssource

Imports 2 library modules and 25 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_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.measure_theory.measure, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.numfun, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.analysis.probability_theory.normal_distribution

Imported by 11

Lebesgue measure on the line, pushed forward by x |-> a x + b with a != 0, is |a|^-1 times Lebesgue measure (lebesgue_measure_affine, ge0_integral_lebesgue_affine). Hence the image of normal_prob m s under x |-> a x + b is normal_prob (a m + b) (a s) (normal_prob_affine), and a linear combination a X + b Y of independent normal variables X and Y, with b != 0, is normal (normal_prob_lincomb): its law is normal_prob (a m1 + b m2) (sqrt (a^2 s1^2 + b^2 s2^2)) when X and Y have laws normal_prob m1 s1 and normal_prob m2 s2. The proof computes the convolution of the two densities (normal_pdf_conv).

Laws are compared on measurable sets only: normal_prob m s A is the Lebesgue integral of normal_pdf m s over A, which MathComp-Analysis defines for every set A.

Main results

Results	Statement
lebesgue_measure_affinege0_integral_lebesgue_affine	Under `x \|-> a x + b` with `a != 0`, Lebesgue measure on the line is multiplied by `\|a\|^-1`.
normal_prob_affine	The image of `normal_prob m s` under `x \|-> a x + b`, `a != 0`, is `normal_prob (a m + b) (a s)`.
normal_prob_lincomb	If `X` and `Y` are independent, of laws `normal_prob m1 s1` and `normal_prob m2 s2`, and `b != 0`, then `a X + b Y` has law `normal_prob (a m1 + b m2) (sqrt (a^2 s1^2 + b^2 s2^2))`.

Declarations9 exported

sectionlebesgue_affine

Context {R : realType}.
Local Notation mu := (@lebesgue_measure R).
Implicit Types a b c d : R.

lemma measurable_affine source, line 46

forall {R : realType} (a b : R),
measurable_fun [set: R]
  (fun x : R => a * x + b)

Statement as written in the source

Lemma measurable_affine a b : measurable_fun [set: R] (fun x => a * x + b).

Used by 6 declarations in 4 files

GaussianAnalysis.gaussian.lebesgue_rV: lebesgue_rV_shift, lebesgue_rV_scale
GaussianAnalysis.probability.semicircle_law: ge0_integral_semicircle_scale
this file: lebesgue_measure_affine, ge0_integral_lebesgue_affine
GaussianAnalysis.comparison.gauss_linear: gauss_mxdot

lemma affine_preimage_itv_pos source, line 49

forall {R : realType} [a : R] (b c d : R),
0 < a -> (fun x : R => a * x + b) @^-1` `]c, d] = `](c - b) / a, (d - b) / a]%classic

Statement as written in the source

Lemma affine_preimage_itv_pos a b c d : 0 < a ->
  (fun x => a * x + b) @^-1` `]c, d] = `](c - b) / a, (d - b) / a]%classic.

Used by 1 declaration in 1 file

this file: lebesgue_measure_affine

lemma affine_preimage_itv_neg source, line 57

forall {R : realType} [a : R] (b c d : R),
a < 0 -> (fun x : R => a * x + b) @^-1` `]c, d] = `[(d - b) / a, (c - b) / a[%classic

Statement as written in the source

Lemma affine_preimage_itv_neg a b c d : a < 0 ->
  (fun x => a * x + b) @^-1` `]c, d] = `[(d - b) / a, (c - b) / a[%classic.

Used by 1 declaration in 1 file

this file: lebesgue_measure_affine

lemma lebesgue_measure_affine main result source, line 65

forall {R : realType} [a : R] (b : R)
  [A : set R],
a != 0 ->
'measurable A ->
lebesgue_measure ((fun x : R => a * x + b) @^-1` A) = ((`|a|^-1)%:E * lebesgue_measure A)%E

Main result, as the README states it

Under x |-> a x + b with a != 0, Lebesgue measure on the line is multiplied by |a|^-1.

Statement as written in the source

Lemma lebesgue_measure_affine a b A : a != 0 -> measurable A ->
  mu ((fun x => a * x + b) @^-1` A) = ((`|a|^-1)%:E * mu A)%E.

Used by 3 declarations in 2 files

GaussianAnalysis.gaussian.lebesgue_rV: lebesgue_rV_shift, lebesgue_rV_scale
this file: ge0_integral_lebesgue_affine

lemma ge0_integral_lebesgue_affine main result source, line 93

forall {R : realType} [a : R] (b : R) [h : R -> \bar R],
a != 0 ->
measurable_fun [set: R] h ->
(forall x : R, (0%R <= h x)%E) ->
(\int[lebesgue_measure]_x h (a * x + b)%R)%E =
((`|a|^-1)%:E * \int[lebesgue_measure]_x h x)%E

Main result

Stated in the README together with lebesgue_measure_affine.

Statement as written in the source

Lemma ge0_integral_lebesgue_affine a b (h : R -> \bar R) : a != 0 ->
    measurable_fun [set: R] h -> (forall x, (0 <= h x)%E) ->
  (\int[mu]_x h (a * x + b)%R = (`|a|^-1)%:E * \int[mu]_x h x)%E.

Used by 9 declarations in 7 files

GaussianAnalysis.probability.semicircle_law: ge0_integral_semicircle_scale
this file: normal_prob_affine
GaussianAnalysis.comparison.gauss_rotation: ge0_integral_shear1, ge0_integral_shear2, ge0_integral_oppr2
GaussianAnalysis.comparison.gauss_shift: ge0_integral_normal_shift
GaussianAnalysis.fourier.esseen: integral_gauss_half_le
GaussianAnalysis.fourier.gauss_factor: gauss_factor_scaled_le
GaussianAnalysis.fourier.small_ball: cf_rV_regularized_le

sectionnormal_affine

Context {R : realType}.
Local Notation mu := (@lebesgue_measure R).
Implicit Types m s a b x : R.

lemma normal_pdf_affine source, line 115

forall {R : realType} (m : R) [s a : R] (b x : R),
a != 0 -> s != 0 -> normal_pdf m s x = `|a| * normal_pdf (a * m + b) (a * s) (a * x + b)

Statement as written in the source

Lemma normal_pdf_affine m s a b x : a != 0 -> s != 0 ->
  normal_pdf m s x = `|a| * normal_pdf (a * m + b) (a * s) (a * x + b).

Used by 1 declaration in 1 file

this file: normal_prob_affine

lemma normal_prob_affine main result source, line 130

forall {R : realType} (m : R) [s a : R] (b : R)
  [A : set R],
a != 0 ->
s != 0 ->
'measurable A ->
normal_prob m s ((fun x : R => a * x + b) @^-1` A) = normal_prob (a * m + b) (a * s) A

Main result, as the README states it

The image of normal_prob m s under x |-> a x + b, a != 0, is normal_prob (a m + b) (a s).

Statement as written in the source

Lemma normal_prob_affine m s a b A : a != 0 -> s != 0 -> measurable A ->
  normal_prob m s ((fun x => a * x + b) @^-1` A) =
  normal_prob (a * m + b) (a * s) A.

Used by 4 declarations in 4 files

this file: normal_prob_lincomb
GaussianAnalysis.comparison.gauss_linear: gauss_mxdot
GaussianAnalysis.comparison.ornstein_uhlenbeck: mehler_kernel_integral
GaussianAnalysis.fourier.charfun: cf_normal

lemma normal_pdf_conv source, line 160

forall {R : realType} (m1 : R) [s1 : R] (m2 : R) [s2 : R] (a : R) [b : R] (x z : R),
s1 != 0 ->
s2 != 0 ->
b != 0 ->
let S0 := Num.ExtraDef.sqrtr (a ^+ 2 * s1 ^+ 2 + b ^+ 2 * s2 ^+ 2) in
normal_pdf m1 s1 x * normal_pdf (b * m2 + a * x) (b * s2) z =
normal_pdf (a * m1 + b * m2) S0 z *
normal_pdf ((m1 * b ^+ 2 * s2 ^+ 2 + a * (z - b * m2) * s1 ^+ 2) / S0 ^+ 2)
  (s1 * b * s2 / S0) x

Statement as written in the source

Lemma normal_pdf_conv m1 s1 m2 s2 a b x z : s1 != 0 -> s2 != 0 -> b != 0 ->
  let S := Num.sqrt (a ^+ 2 * s1 ^+ 2 + b ^+ 2 * s2 ^+ 2) in
  normal_pdf m1 s1 x * normal_pdf (b * m2 + a * x) (b * s2) z =
  normal_pdf (a * m1 + b * m2) S z *
  normal_pdf ((m1 * b ^+ 2 * s2 ^+ 2 + a * (z - b * m2) * s1 ^+ 2) / S ^+ 2)
    (s1 * b * s2 / S) x.

Used by 1 declaration in 1 file

this file: normal_prob_lincomb

lemma normal_prob_lincomb main result source, line 188

forall {R : realType} (m1 : R) [s1 : R] (m2 : R) [s2 : R] (a : R) 
  [b : R] [A : set R],
s1 != 0 ->
s2 != 0 ->
b != 0 ->
'measurable A ->
(normal_prob m1 s1 \x normal_prob m2 s2)%E [set p | A (a * p.1 + b * p.2)] =
normal_prob (a * m1 + b * m2) (Num.ExtraDef.sqrtr (a ^+ 2 * s1 ^+ 2 + b ^+ 2 * s2 ^+ 2)) A

Main result, as the README states it

If X and Y are independent, of laws normal_prob m1 s1 and normal_prob m2 s2, and b != 0, then a X + b Y has law normal_prob (a m1 + b m2) (sqrt (a^2 s1^2 + b^2 s2^2)).

Statement as written in the source

Lemma normal_prob_lincomb m1 s1 m2 s2 a b A :
    s1 != 0 -> s2 != 0 -> b != 0 -> measurable A ->
  ((normal_prob m1 s1 \x normal_prob m2 s2) [set p | A (a * p.1 + b * p.2)%R] =
   normal_prob (a * m1 + b * m2)
     (Num.sqrt (a ^+ 2 * s1 ^+ 2 + b ^+ 2 * s2 ^+ 2)) A)%E.

Used by 2 declarations in 2 files

GaussianAnalysis.comparison.gauss_linear: gauss_mxdot
GaussianAnalysis.comparison.ornstein_uhlenbeck: integral_mehler

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.