GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysiscomparisongauss_rotation

Rotation invariance of Gaussian measures

GaussianAnalysis.comparison.gauss_rotationlibrary/comparison/gauss_rotation.v511 lines17 lemmas and theoremssource
Imports 4 library modules and 26 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.interval, mathcomp.algebra.matrix, 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 2

Lebesgue measure on the plane is invariant under the shears (x, y) |-> (x + a y, y) and (x, y) |-> (x, y + b x), by Fubini and the invariance of Lebesgue measure on the line under translations. A rotation of angle different from pi is a product of three shears, so Lebesgue measure on the plane is rotation invariant (ge0_integral_rotation2). The standard Gaussian measure on the plane, normal_prob 0 1 \x normal_prob 0 1, has a rotation invariant density, so it is rotation invariant (normal2_rotation).

For c^2 + s^2 = 1 and independent x and y of law gauss n, the pair (c x - s y, s x + c y) has the law of (x, y) (ge0_integral_gauss2_rotation, gauss2_rotation): rotating pairwise the coordinates of two independent standard Gaussian vectors preserves their joint law. In particular c x + s y has law gauss n (ge0_integral_gauss_lincomb).

Main results

ResultsStatement
ge0_integral_rotation2
Lebesgue measure on the plane is invariant under rotations (each is a product of three shears).
normal2_rotation
The standard Gaussian measure on the plane is invariant under rotations.
ge0_integral_gauss2_rotationgauss2_rotationge0_integral_gauss_lincombintegral_gauss2_rotation
For independent x, y of law gauss n and c^2 + s^2 = 1, the pair (c x - s y, s x + c y) has the law of (x, y); in particular c x + s y has law gauss n.

Declarations17 exported

lemma, theoremdefinitioninstancelocal
sectionlebesgue2_shear
Context {R : realType}.
Local Notation mu := (@lebesgue_measure R).
Local Open Scope ereal_scope.
lemma ge0_integral_shear1 source, line 47 
forall {R : realType} [h : R * R -> \bar R] (a : R),
measurable_fun [set: R * R] h ->
(forall p : R * R, (0%R <= h p)%E) ->
(\int[lebesgue_measure \x lebesgue_measure]_p h ((p.1 + a * p.2)%R, p.2))%E =
(\int[lebesgue_measure \x lebesgue_measure]_p h p)%E
Statement as written in the source
Lemma ge0_integral_shear1 (h : R * R -> \bar R) (a : R) :
    measurable_fun [set: R * R] h -> (forall p, 0 <= h p) ->
  \int[mu \x mu]_p h (p.1 + a * p.2, p.2)%R = \int[mu \x mu]_p h p.
Used by 1 declaration in 1 file
lemma ge0_integral_shear2 source, line 68 
forall {R : realType} [h : R * R -> \bar R] (b : R),
measurable_fun [set: R * R] h ->
(forall p : R * R, (0%R <= h p)%E) ->
(\int[lebesgue_measure \x lebesgue_measure]_p h (p.1, (p.2 + b * p.1)%R))%E =
(\int[lebesgue_measure \x lebesgue_measure]_p h p)%E
Statement as written in the source
Lemma ge0_integral_shear2 (h : R * R -> \bar R) (b : R) :
    measurable_fun [set: R * R] h -> (forall p, 0 <= h p) ->
  \int[mu \x mu]_p h (p.1, p.2 + b * p.1)%R = \int[mu \x mu]_p h p.
Used by 1 declaration in 1 file
lemma ge0_integral_oppr2 source, line 89 
forall {R : realType} [h : R * R -> \bar R],
measurable_fun [set: R * R] h ->
(forall p : R * R, (0%R <= h p)%E) ->
(\int[lebesgue_measure \x lebesgue_measure]_p h ((- p.1)%R, (- p.2)%R))%E =
(\int[lebesgue_measure \x lebesgue_measure]_p h p)%E
Statement as written in the source
Lemma ge0_integral_oppr2 (h : R * R -> \bar R) :
    measurable_fun [set: R * R] h -> (forall p, 0 <= h p) ->
  \int[mu \x mu]_p h (- p.1, - p.2)%R = \int[mu \x mu]_p h p.
Used by 1 declaration in 1 file
lemma ge0_integral_rotation2 main result source, line 120 
forall {R : realType} [h : R * R -> \bar R] [c s : R],
c ^+ 2 + s ^+ 2 = 1 ->
measurable_fun [set: R * R] h ->
(forall p : R * R, (0%R <= h p)%E) ->
(\int[lebesgue_measure \x lebesgue_measure]_p
    h ((c * p.1 - s * p.2)%R, (s * p.1 + c * p.2)%R))%E =
(\int[lebesgue_measure \x lebesgue_measure]_p h p)%E
Main result, as the README states it

Lebesgue measure on the plane is invariant under rotations (each is a product of three shears).

Statement as written in the source
Lemma ge0_integral_rotation2 (h : R * R -> \bar R) (c s : R) :
    (c ^+ 2 + s ^+ 2 = 1)%R ->
    measurable_fun [set: R * R] h -> (forall p, 0 <= h p) ->
  \int[mu \x mu]_p h (c * p.1 - s * p.2, s * p.1 + c * p.2)%R =
  \int[mu \x mu]_p h p.
Used by 1 declaration in 1 file
sectionnormal2
Context {R : realType}.
Local Notation mu := (@lebesgue_measure R).
Local Notation N := (@normal_prob R 0 1).
Local Notation phi := (@normal_pdf R 0 1).
Local Open Scope ereal_scope.
lemma ge0_integral_normal2 source, line 168 
forall {R : realType} [h : R * R -> \bar R],
measurable_fun [set: R * R] h ->
(forall p : R * R, (0%R <= h p)%E) ->
(\int[normal_prob 0 1 \x normal_prob 0 1]_p h p)%E =
(\int[lebesgue_measure \x lebesgue_measure]_p
    (h p * (normal_pdf 0 1 p.1 * normal_pdf 0 1 p.2)%:E))%E
Statement as written in the source
Lemma ge0_integral_normal2 (h : R * R -> \bar R) :
    measurable_fun [set: R * R] h -> (forall p, 0 <= h p) ->
  \int[N \x N]_p h p = \int[mu \x mu]_p (h p * (phi p.1 * phi p.2)%:E).
Used by 1 declaration in 1 file
lemma normal_pdf01_rotation source, line 199 
forall {R : realType} [c s : R] (x y : R),
c ^+ 2 + s ^+ 2 = 1 ->
normal_pdf 0 1 (c * x - s * y) * normal_pdf 0 1 (s * x + c * y) =
normal_pdf 0 1 x * normal_pdf 0 1 y
Statement as written in the source
Lemma normal_pdf01_rotation (c s x y : R) : (c ^+ 2 + s ^+ 2 = 1)%R ->
  (phi (c * x - s * y) * phi (s * x + c * y) = phi x * phi y)%R.
Used by 1 declaration in 1 file
theorem ge0_integral_normal2_rotation source, line 208 
forall {R : realType} [h : R * R -> \bar R] [c s : R],
c ^+ 2 + s ^+ 2 = 1 ->
measurable_fun [set: R * R] h ->
(forall p : R * R, (0%R <= h p)%E) ->
(\int[normal_prob 0 1 \x normal_prob 0 1]_p
    h ((c * p.1 - s * p.2)%R, (s * p.1 + c * p.2)%R))%E =
(\int[normal_prob 0 1 \x normal_prob 0 1]_p h p)%E
Statement as written in the source
Theorem ge0_integral_normal2_rotation (h : R * R -> \bar R) (c s : R) :
    (c ^+ 2 + s ^+ 2 = 1)%R ->
    measurable_fun [set: R * R] h -> (forall p, 0 <= h p) ->
  \int[N \x N]_p h (c * p.1 - s * p.2, s * p.1 + c * p.2)%R =
  \int[N \x N]_p h p.
Used by 2 declarations in 1 file
theorem normal2_rotation main result source, line 235 
forall {R : realType} [c s : R] [B : set (R * R)],
c ^+ 2 + s ^+ 2 = 1 ->
((default_measure_display, default_measure_display).-prod).-measurable B ->
(normal_prob 0 1 \x normal_prob 0 1)%E
  ((fun p : R * R => (c * p.1 - s * p.2, s * p.1 + c * p.2)) @^-1` B) =
(normal_prob 0 1 \x normal_prob 0 1)%E B
Main result, as the README states it

The standard Gaussian measure on the plane is invariant under rotations.

Statement as written in the source
Theorem normal2_rotation (c s : R) (B : set (R * R)) :
    (c ^+ 2 + s ^+ 2 = 1)%R -> measurable B ->
  (N \x N) ((fun p : R * R => (c * p.1 - s * p.2, s * p.1 + c * p.2)%R) @^-1` B) =
  (N \x N) B.
sectiongauss2_cons
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
Local Open Scope ereal_scope.
lemma ge0_integral_gauss2_cons source, line 264 
forall {R : realType} [n : nat] [F : 'rV_n.+1 * 'rV_n.+1 -> \bar R],
measurable_fun [set: 'rV_n.+1 * 'rV_n.+1] F ->
(forall p : 'rV_n.+1 * 'rV_n.+1, (0%R <= F p)%E) ->
(\int[gauss n.+1 \x gauss n.+1]_p F p)%E =
(\int[normal_prob 0 1 \x normal_prob 0 1]_q
    \int[gauss n \x gauss n]_r F (rV_cons (q.1, r.1), rV_cons (q.2, r.2)))%E
Statement as written in the source
Lemma ge0_integral_gauss2_cons n (F : 'rV[R]_n.+1 * 'rV[R]_n.+1 -> \bar R) :
    measurable_fun [set: 'rV[R]_n.+1 * 'rV[R]_n.+1] F -> (forall p, 0 <= F p) ->
  \int[gauss n.+1 \x gauss n.+1]_p F p =
  \int[N \x N]_q \int[gauss n \x gauss n]_r
    F (rV_cons (q.1, r.1), rV_cons (q.2, r.2)).
Used by 1 declaration in 1 file
lemma rV_cons_lin source, line 343 
forall {R : realType} [n : nat] (c s a b : R) (u v : 'rV_n),
c *: rV_cons (a, u) + s *: rV_cons (b, v) = rV_cons (c * a + s * b, c *: u + s *: v)
Statement as written in the source
Lemma rV_cons_lin n (c s a b : R) (u v : 'rV[R]_n) :
  (c *: rV_cons (a, u) + s *: rV_cons (b, v) =
   rV_cons ((c * a + s * b)%R, c *: u + s *: v))%R.
Used by 2 declarations in 1 file
lemma rV_cons_lincomb source, line 351 
forall {R : realType} [n : nat] (c s a b : R) (u v : 'rV_n),
c *: rV_cons (a, u) - s *: rV_cons (b, v) = rV_cons (c * a - s * b, c *: u - s *: v)
Statement as written in the source
Lemma rV_cons_lincomb n (c s a b : R) (u v : 'rV[R]_n) :
  (c *: rV_cons (a, u) - s *: rV_cons (b, v) =
   rV_cons ((c * a - s * b)%R, c *: u - s *: v))%R.
Used by 1 declaration in 1 file
theorem ge0_integral_gauss2_rotation main result source, line 356 
forall {R : realType} [n : nat] [c s : R] [f : 'rV_n * 'rV_n -> \bar R],
c ^+ 2 + s ^+ 2 = 1 ->
measurable_fun [set: 'rV_n * 'rV_n] f ->
(forall p : 'rV_n * 'rV_n, (0%R <= f p)%E) ->
(\int[gauss n \x gauss n]_p f ((c *: p.1 - s *: p.2)%R, (s *: p.1 + c *: p.2)%R))%E =
(\int[gauss n \x gauss n]_p f p)%E
Main result, as the README states it

For independent x, y of law gauss n and c^2 + s^2 = 1, the pair (c x - s y, s x + c y) has the law of (x, y); in particular c x + s y has law gauss n.

Statement as written in the source
Theorem ge0_integral_gauss2_rotation n (c s : R)
    (f : 'rV[R]_n * 'rV[R]_n -> \bar R) :
    (c ^+ 2 + s ^+ 2 = 1)%R -> measurable_fun [set: 'rV[R]_n * 'rV[R]_n] f ->
    (forall p, 0 <= f p) ->
  \int[gauss n \x gauss n]_p f (c *: p.1 - s *: p.2, s *: p.1 + c *: p.2)%R =
  \int[gauss n \x gauss n]_p f p.
Used by 4 declarations in 1 file
corollary gauss2_rotation main result source, line 426 
forall {R : realType} [n : nat] [c s : R] [E : set ('rV_n * 'rV_n)],
c ^+ 2 + s ^+ 2 = 1 ->
((measure_matrix_display default_measure_display,
  measure_matrix_display default_measure_display).-prod).-measurable E ->
(gauss n \x gauss n)%E
  ((fun p : 'rV_n * 'rV_n => (c *: p.1 - s *: p.2, s *: p.1 + c *: p.2)) @^-1` E) =
(gauss n \x gauss n)%E E
Main result

Stated in the README together with ge0_integral_gauss2_rotation.

Statement as written in the source
Corollary gauss2_rotation n (c s : R) (E : set ('rV[R]_n * 'rV[R]_n)) :
    (c ^+ 2 + s ^+ 2 = 1)%R -> measurable E ->
  (gauss n \x gauss n)
    ((fun p : 'rV[R]_n * 'rV[R]_n => (c *: p.1 - s *: p.2, s *: p.1 + c *: p.2)%R)
       @^-1` E) = (gauss n \x gauss n) E.
corollary ge0_integral_gauss_lincomb main result source, line 452 
forall {R : realType} [n : nat] [c s : R] [f : 'rV_n -> \bar R],
c ^+ 2 + s ^+ 2 = 1 ->
measurable_fun [set: 'rV_n] f ->
(forall x : 'rV_n, (0%R <= f x)%E) ->
(\int[gauss n \x gauss n]_p f (c *: p.1 + s *: p.2)%R)%E = (\int[gauss n]_x f x)%E
Main result

Stated in the README together with ge0_integral_gauss2_rotation.

Statement as written in the source
Corollary ge0_integral_gauss_lincomb n (c s : R) (f : 'rV[R]_n -> \bar R) :
    (c ^+ 2 + s ^+ 2 = 1)%R -> measurable_fun [set: 'rV[R]_n] f ->
    (forall x, 0 <= f x) ->
  \int[gauss n \x gauss n]_p f (c *: p.1 + s *: p.2)%R = \int[gauss n]_x f x.
Used by 1 declaration in 1 file
lemma measurable_gauss2_rot source, line 468 
forall {R : realType} [n : nat] (c s : R),
measurable_fun [set: 'rV_n * 'rV_n]
  (fun p : 'rV_n * 'rV_n => (c *: p.1 - s *: p.2, s *: p.1 + c *: p.2))
Statement as written in the source
Lemma measurable_gauss2_rot n (c s : R) :
  measurable_fun [set: 'rV[R]_n * 'rV[R]_n]
    (fun p : 'rV[R]_n * 'rV[R]_n => (c *: p.1 - s *: p.2, s *: p.1 + c *: p.2)%R).
Used by 1 declaration in 1 file
corollary integrable_gauss2_rotation source, line 481 
forall {R : realType} [n : nat] [c s : R] [f : 'rV_n * 'rV_n -> \bar R],
c ^+ 2 + s ^+ 2 = 1 ->
(gauss n \x gauss n)%E.-integrable
  [set: ('rV_n * 'rV_n)] f ->
(gauss n \x gauss n)%E.-integrable
  [set: ('rV_n * 'rV_n)]
  (fun p : ('rV_n * 'rV_n) =>
   f (c *: p.1 - s *: p.2, s *: p.1 + c *: p.2))
Statement as written in the source
Corollary integrable_gauss2_rotation n (c s : R) (f : 'rV[R]_n * 'rV[R]_n -> \bar R) :
    (c ^+ 2 + s ^+ 2 = 1)%R ->
    (gauss n \x gauss n).-integrable setT f ->
  (gauss n \x gauss n).-integrable setT
    (fun p => f (c *: p.1 - s *: p.2, s *: p.1 + c *: p.2)%R).
corollary integral_gauss2_rotation main result source, line 495 
forall {R : realType} [n : nat] [c s : R] [f : 'rV_n * 'rV_n -> \bar R],
c ^+ 2 + s ^+ 2 = 1 ->
(gauss n \x gauss n)%E.-integrable
  [set: ('rV_n * 'rV_n)] f ->
(\int[gauss n \x gauss n]_p f ((c *: p.1 - s *: p.2)%R, (s *: p.1 + c *: p.2)%R))%E =
(\int[gauss n \x gauss n]_p f p)%E
Main result

Stated in the README together with ge0_integral_gauss2_rotation.

Statement as written in the source
Corollary integral_gauss2_rotation n (c s : R) (f : 'rV[R]_n * 'rV[R]_n -> \bar R) :
    (c ^+ 2 + s ^+ 2 = 1)%R ->
    (gauss n \x gauss n).-integrable setT f ->
  \int[gauss n \x gauss n]_p f (c *: p.1 - s *: p.2, s *: p.1 + c *: p.2)%R =
  \int[gauss n \x gauss n]_p f p.
Used by 1 declaration in 1 file
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.