GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisfouriercharfun

Characteristic functions of laws on the real line

GaussianAnalysis.fourier.charfunlibrary/fourier/charfun.v831 lines64 lemmas and theorems, 6 definitionssource
Imports 7 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.ring_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.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.analysis.trigo, 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

Imported by 5

MathComp-Analysis has no complex numbers, so the characteristic function t |-> E[exp (i t X)] of a law mu on R is given by its real part cf_re mu and its imaginary part cf_im mu. A pair z : R * R stands for the complex number z.1 + i z.2: cmul is the complex product and cmod the modulus.

Laws on the real line are probabilities on measurableTypeR R, the type on which MathComp-Analysis defines Lebesgue measure and normal_prob. A law nu is the image of a probability P on T under a measurable g : T -> R when P (g @^-1` A) = nu A for every measurable A; then cf_re nu t is the integral of cos (t * g x) against P (cf_image). Independent variables are described by product measures (P1 \x P2, tuple_prod).

The characteristic function of normal_prob m s is exp (- s^2 t^2 / 2) (cos (m t), sin (m t)) (cf_normal): for the standard law, differentiation under the integral and Stein's identity (normal_ibp) give the differential equation y' = - t y.

cmul z wthe complex product of the pairs z and w
cmod zthe modulus sqrt (z.1 ^ 2 + z.2 ^ 2) of the pair z
cf_re mu t\int[mu]_x cos (t * x), the real part of the characteristic function of the law mu at t
cf_im mu t\int[mu]_x sin (t * x), its imaginary part
cf mu tthe pair (cf_re mu t, cf_im mu t)
cf_norm mu tthe modulus of the characteristic function of mu at t

Main results

ResultsStatement
cf_recf_imcfcf_normcmulcmod
The characteristic function of a law mu on R (a probability on measurableTypeR R, the type of normal_prob), without complex numbers: cf_re mu t = E[cos (t X)], cf_im mu t = E[sin (t X)] for X of law mu, the pair cf mu t of the two, and its modulus cf_norm mu t. A pair (a, b) stands for a + i b: cmul is the complex product and cmod the modulus, which is multiplicative (cmodM, cmod_prod).
cf_re0cf_im0cf_norm0cf_reNcf_imNcf_normNcf_re_le1cf_im_le1cf_norm_le1continuous_cf_recontinuous_cf_imcontinuous_cf_norm
cf mu 0 = (1, 0), cf mu (- t) is the conjugate of cf mu t, the modulus is at most one, and the three functions are continuous in t.
cf_imagecf_re_imagecf_im_image
If nu is the law of a measurable g : T -> R under a probability P (P (g @^-1` A) = nu A for measurable A), then cf nu t = (E_P[cos (t g)], E_P[sin (t g)]).
cf_affinecf_norm_affine
The law of a X + b has the characteristic function exp (i b t) cf mu (a t), of modulus cf_norm mu (a t).
cf_prodcf_norm_prodcf_prod_integralcf_iterated
Independent sums: for independent X1, X2 (laws P1, P2, joint law P1 \x P2) and measurable g1, g2, the characteristic function of g1 X1 + g2 X2 is the complex product of those of g1 X1 and g2 X2, so the moduli multiply.
cf_tuple_prodcf_norm_tuple_prodcf_tuple_prod_integral
For x of law tuple_prod mu n (independent coordinates of laws mu 0, ..., mu (n-1)) and reals a k, the characteristic function of \sum_k a_k x_k at t is the complex product of the cf (mu k) (a_k t), and its modulus is the product of the cf_norm (mu k) (a_k t).
cf_symcf_norm_sym
Symmetrization: the law of X - X', for independent X and X' of law mu, has the real characteristic function cf_norm mu t ^ 2.
cf_normalcf_re_normalcf_im_normalcf_norm_normal
For s != 0, the characteristic function of normal_prob m s at t is expR (- (s t)^2 / 2) (cos (m t), sin (m t)), of modulus expR (- (s t)^2 / 2). Proved for the standard law by differentiating under the integral and Stein's identity (normal_ibp), which give y' = - t y, then by cf_affine.
Rintegral_prod_bounded
Fubini for a bounded measurable real function on a product of two probabilities.
is_derive_cos_mulis_derive_sin_mulis_derive_cos_mulris_derive_sin_mulr
Derivatives of s |-> cos (t s), sin (t s), cos (s z) and sin (s z).

Declarations70 exported, 11 local

lemma, theoremdefinitioninstancelocal
sectioncomplex_pair
Context {R : rcfType}.
Implicit Types z w : R * R.
definition cmul main result source, line 60
Type
forall {R : rcfType}, R * R -> R * R -> R * R
Definition
Definition cmul z w : R * R := (z.1 * w.1 - z.2 * w.2, z.1 * w.2 + z.2 * w.1).
Main result

Stated in the README together with cf_re.

Used by 15 declarations in 3 files
definition cmod main result source, line 62
Type
forall {R : rcfType}, R * R -> R
Definition
Definition cmod z : R := Num.sqrt (z.1 ^+ 2 + z.2 ^+ 2).
Main result

Stated in the README together with cf_re.

Used by 12 declarations in 2 files
lemma cmulE source, line 64 
forall {R : rcfType} (a b c e : R), cmul (a, b) (c, e) = (a * c - b * e, a * e + b * c)
Statement as written in the source
Lemma cmulE a b c e : cmul (a, b) (c, e) = (a * c - b * e, a * e + b * c).
Used by 6 declarations in 3 files
lemma cmulA source, line 67 
forall {R : rcfType}, associative cmul
Statement as written in the source
Lemma cmulA : associative cmul.
lemma cmulC source, line 70 
forall {R : rcfType}, commutative cmul
Statement as written in the source
Lemma cmulC : commutative cmul.
lemma cmul1z source, line 73 
forall {R : rcfType}, left_id (1, 0) cmul
Statement as written in the source
Lemma cmul1z : left_id (1, 0) cmul.
lemma cmod_ge0 source, line 76 
forall {R : rcfType} (z : R * R), 0 <= cmod z
Statement as written in the source
Lemma cmod_ge0 z : 0 <= cmod z.
Used by 1 declaration in 1 file
lemma cmod1 source, line 79 
forall {R : rcfType}, cmod (1, 0) = 1
Statement as written in the source
Lemma cmod1 : cmod (1, 0) = 1.
Used by 1 declaration in 1 file
lemma cmodM source, line 82 
forall {R : rcfType} (z w : R * R), cmod (cmul z w) = cmod z * cmod w
Statement as written in the source
Lemma cmodM z w : cmod (cmul z w) = cmod z * cmod w.
Used by 4 declarations in 2 files
lemma cmod_prod source, line 88 
forall {R : rcfType} [I : Type] (r : seq I) (P : pred I) (F : I -> R * R),
cmod (\big[cmul/(1, 0)]_(i <- r | P i) F i) = \prod_(i <- r | P i) cmod (F i)
Statement as written in the source
Lemma cmod_prod I (r : seq I) (P : pred I) (F : I -> R * R) :
  cmod (\big[cmul/(1, 0)]_(i <- r | P i) F i) =
  \prod_(i <- r | P i) cmod (F i).
Used by 2 declarations in 2 files
lemma cmod_ge_dot source, line 94 
forall {R : rcfType} (a b : R) [u v : R],
u ^+ 2 + v ^+ 2 = 1 -> `|a * u + b * v| <= cmod (a, b)

For a unit vector (u, v), `|a u + b v| is at most the modulus of (a, b).

Statement as written in the source
Lemma cmod_ge_dot a b u v :
  u ^+ 2 + v ^+ 2 = 1 -> `|a * u + b * v| <= cmod (a, b).
Used by 4 declarations in 4 files
sectionmeasurable_trigo
Context {R : realType}.
lemma measurable_idR source, line 109 
forall {R : realType},
measurable_fun [set: measurableTypeR R] (fun x : measurableTypeR R => x : R)

The identity of the real line, from the type measurableTypeR R on which MathComp-Analysis defines Lebesgue measure and normal_prob, to R.

Statement as written in the source
Lemma measurable_idR :
  measurable_fun [set: measurableTypeR R] (fun x : measurableTypeR R => x : R).
Used by 19 declarations in 3 files
lemma measurable_cos source, line 113 
forall {R : realType}, measurable_fun [set: R] cos
Statement as written in the source
Lemma measurable_cos : measurable_fun [set: R] cos.
Used by 1 declaration in 1 file
lemma measurable_sin source, line 116 
forall {R : realType}, measurable_fun [set: R] sin
Statement as written in the source
Lemma measurable_sin : measurable_fun [set: R] sin.
Used by 1 declaration in 1 file
lemma measurable_cos_comp source, line 119 
forall {R : realType} [d : measure_display] [T : measurableType d] [g : T -> R],
measurable_fun [set: T] g -> measurable_fun [set: T] (fun x : T => cos (g x))
Statement as written in the source
Lemma measurable_cos_comp d (T : measurableType d) (g : T -> R) :
  measurable_fun [set: T] g -> measurable_fun [set: T] (fun x => cos (g x)).
Used by 10 declarations in 5 files
lemma measurable_sin_comp source, line 123 
forall {R : realType} [d : measure_display] [T : measurableType d] [g : T -> R],
measurable_fun [set: T] g -> measurable_fun [set: T] (fun x : T => sin (g x))
Statement as written in the source
Lemma measurable_sin_comp d (T : measurableType d) (g : T -> R) :
  measurable_fun [set: T] g -> measurable_fun [set: T] (fun x => sin (g x)).
Used by 7 declarations in 3 files
lemma measurable_cos_mul source, line 127 
forall {R : realType} [d : measure_display] [T : measurableType d] [g : T -> R] (t : R),
measurable_fun [set: T] g -> measurable_fun [set: T] (fun x : T => cos (t * g x))
Statement as written in the source
Lemma measurable_cos_mul d (T : measurableType d) (g : T -> R) (t : R) :
  measurable_fun [set: T] g -> measurable_fun [set: T] (fun x => cos (t * g x)).
Used by 6 declarations in 3 files
lemma measurable_sin_mul source, line 131 
forall {R : realType} [d : measure_display] [T : measurableType d] [g : T -> R] (t : R),
measurable_fun [set: T] g -> measurable_fun [set: T] (fun x : T => sin (t * g x))
Statement as written in the source
Lemma measurable_sin_mul d (T : measurableType d) (g : T -> R) (t : R) :
  measurable_fun [set: T] g -> measurable_fun [set: T] (fun x => sin (t * g x)).
Used by 5 declarations in 1 file
lemma integrable_cos_comp source, line 135 
forall {R : realType} [d : measure_display] [T : measurableType d] 
  (P : probability T R) [g : T -> R],
measurable_fun [set: T] g -> P.-integrable [set: T] (EFin \o (fun x : T => cos (g x)))
Statement as written in the source
Lemma integrable_cos_comp d (T : measurableType d) (P : probability T R)
    (g : T -> R) : measurable_fun [set: T] g ->
  P.-integrable [set: T] (EFin \o (fun x => cos (g x))).
Used by 6 declarations in 4 files
lemma integrable_sin_comp source, line 143 
forall {R : realType} [d : measure_display] [T : measurableType d] 
  (P : probability T R) [g : T -> R],
measurable_fun [set: T] g -> P.-integrable [set: T] (EFin \o (fun x : T => sin (g x)))
Statement as written in the source
Lemma integrable_sin_comp d (T : measurableType d) (P : probability T R)
    (g : T -> R) : measurable_fun [set: T] g ->
  P.-integrable [set: T] (EFin \o (fun x => sin (g x))).
Used by 5 declarations in 3 files
lemma integrable_cos_mul source, line 151 
forall {R : realType} [d : measure_display] [T : measurableType d] 
  (P : probability T R) [g : T -> R] (t : R),
measurable_fun [set: T] g -> P.-integrable [set: T] (EFin \o (fun x : T => cos (t * g x)))
Statement as written in the source
Lemma integrable_cos_mul d (T : measurableType d) (P : probability T R)
    (g : T -> R) (t : R) : measurable_fun [set: T] g ->
  P.-integrable [set: T] (EFin \o (fun x => cos (t * g x))).
Used by 6 declarations in 3 files
lemma integrable_sin_mul source, line 156 
forall {R : realType} [d : measure_display] [T : measurableType d] 
  (P : probability T R) [g : T -> R] (t : R),
measurable_fun [set: T] g -> P.-integrable [set: T] (EFin \o (fun x : T => sin (t * g x)))
Statement as written in the source
Lemma integrable_sin_mul d (T : measurableType d) (P : probability T R)
    (g : T -> R) (t : R) : measurable_fun [set: T] g ->
  P.-integrable [set: T] (EFin \o (fun x => sin (t * g x))).
Used by 7 declarations in 2 files
lemma Rintegral_cos_sin source, line 162 
forall {R : realType} [d : measure_display] [T : measurableType d] 
  (P : probability T R) [g : T -> R] (p q : R),
measurable_fun [set: T] g ->
\int[P]_x (p * cos (g x) + q * sin (g x)) =
p * \int[P]_x cos (g x) + q * \int[P]_x sin (g x)

Integrals of a p cos (g x) + q sin (g x), with constants p and q.

Statement as written in the source
Lemma Rintegral_cos_sin d (T : measurableType d) (P : probability T R)
    (g : T -> R) (p q : R) : measurable_fun [set: T] g ->
  \int[P]_x (p * cos (g x) + q * sin (g x)) =
  p * \int[P]_x cos (g x) + q * \int[P]_x sin (g x).
Used by 5 declarations in 3 files
lemma RintegralN source, line 176 
forall {R : realType} [d : measure_display] [T : measurableType d] 
  [mu : measure T R] [f : T -> R],
mu.-integrable [set: T] (EFin \o f) -> \int[mu]_x - f x = - (\int[mu]_x f x)
Statement as written in the source
Lemma RintegralN d (T : measurableType d) (mu : {measure set T -> \bar R})
    (f : T -> R) :
  mu.-integrable [set: T] (EFin \o f) -> \int[mu]_x (- f x) = - \int[mu]_x f x.
Used by 5 declarations in 3 files
sectioncharfun
Context {R : realType}.
Implicit Types (mu : probability (measurableTypeR R) R) (t : R).
definition cf_re main result source, line 190
Type
forall {R : realType}, probability (measurableTypeR R) R -> R -> R
Definition
Definition cf_re mu t := \int[mu]_x cos (t * x).
Main result, as the README states it

The characteristic function of a law mu on R (a probability on measurableTypeR R, the type of normal_prob), without complex numbers: cf_re mu t = E[cos (t X)], cf_im mu t = E[sin (t X)] for X of law mu, the pair cf mu t of the two, and its modulus cf_norm mu t. A pair (a, b) stands for a + i b: cmul is the complex product and cmod the modulus, which is multiplicative (cmodM, cmod_prod).

Used by 21 declarations in 3 files
definition cf_im main result source, line 192
Type
forall {R : realType}, probability (measurableTypeR R) R -> R -> R
Definition
Definition cf_im mu t := \int[mu]_x sin (t * x).
Main result

Stated in the README together with cf_re.

Used by 18 declarations in 2 files
definition cf main result source, line 194
Type
forall {R : realType}, probability (measurableTypeR R) R -> R -> R * R
Definition
Definition cf mu t : R * R := (cf_re mu t, cf_im mu t).
Main result

Stated in the README together with cf_re.

Used by 14 declarations in 4 files
definition cf_norm main result source, line 196
Type
forall {R : realType},
probability (measurableTypeR R) R ->
R -> join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R
Definition
Definition cf_norm mu t := Num.sqrt (cf_re mu t ^+ 2 + cf_im mu t ^+ 2).
Main result

Stated in the README together with cf_re.

Used by 31 declarations in 5 files
lemma cf_normE source, line 198 
forall {R : realType} (mu : probability (measurableTypeR R) R) (t : R),
cf_norm mu t = cmod (cf mu t)
Statement as written in the source
Lemma cf_normE mu t : cf_norm mu t = cmod (cf mu t).
Used by 8 declarations in 3 files
lemma cf_norm_ge0 source, line 201 
forall {R : realType} (mu : probability (measurableTypeR R) R) (t : R), 0 <= cf_norm mu t
Statement as written in the source
Lemma cf_norm_ge0 mu t : 0 <= cf_norm mu t.
Used by 7 declarations in 4 files
lemma cf_re0 main result source, line 204 
forall {R : realType} (mu : probability (measurableTypeR R) R), cf_re mu 0 = 1
Main result, as the README states it

cf mu 0 = (1, 0), cf mu (- t) is the conjugate of cf mu t, the modulus is at most one, and the three functions are continuous in t.

Statement as written in the source
Lemma cf_re0 mu : cf_re mu 0 = 1.
Used by 2 declarations in 1 file
lemma cf_im0 main result source, line 210 
forall {R : realType} (mu : probability (measurableTypeR R) R), cf_im mu 0 = 0
Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma cf_im0 mu : cf_im mu 0 = 0.
Used by 2 declarations in 1 file
lemma cf_norm0 main result source, line 216 
forall {R : realType} (mu : probability (measurableTypeR R) R), cf_norm mu 0 = 1
Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma cf_norm0 mu : cf_norm mu 0 = 1.
Used by 1 declaration in 1 file
lemma cf_reN main result source, line 219 
forall {R : realType} (mu : probability (measurableTypeR R) R) (t : R),
cf_re mu (- t) = cf_re mu t
Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma cf_reN mu t : cf_re mu (- t) = cf_re mu t.
Used by 1 declaration in 1 file
lemma cf_imN main result source, line 222 
forall {R : realType} (mu : probability (measurableTypeR R) R) (t : R),
cf_im mu (- t) = - cf_im mu t
Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma cf_imN mu t : cf_im mu (- t) = - cf_im mu t.
Used by 1 declaration in 1 file
lemma cf_normN main result source, line 228 
forall {R : realType} (mu : probability (measurableTypeR R) R) (t : R),
cf_norm mu (- t) = cf_norm mu t
Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma cf_normN mu t : cf_norm mu (- t) = cf_norm mu t.
Used by 1 declaration in 1 file
  • GaussianAnalysis.fourier.esseen: esseen
lemma cf_re_le1 main result source, line 231 
forall {R : realType} (mu : probability (measurableTypeR R) R) (t : R), `|cf_re mu t| <= 1
Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma cf_re_le1 mu t : `|cf_re mu t| <= 1.
lemma cf_im_le1 main result source, line 237 
forall {R : realType} (mu : probability (measurableTypeR R) R) (t : R), `|cf_im mu t| <= 1
Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma cf_im_le1 mu t : `|cf_im mu t| <= 1.
lemma cf_norm_le1 main result source, line 246 
forall {R : realType} (mu : probability (measurableTypeR R) R) (t : R), cf_norm mu t <= 1

The modulus is at most one: with c = cf_re mu t and s = cf_im mu t, c^2 + s^2 is the integral of c cos (t x) + s sin (t x), which is at most sqrt (c^2 + s^2) by the Cauchy-Schwarz inequality in the plane.

Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma cf_norm_le1 mu t : cf_norm mu t <= 1.
Used by 3 declarations in 3 files
lemma continuous_cf_re main result source, line 264 
forall {R : realType} [mu : probability (measurableTypeR R) R], continuous (cf_re mu)
Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma continuous_cf_re mu : continuous (cf_re mu).
Used by 2 declarations in 2 files
lemma continuous_cf_im main result source, line 277 
forall {R : realType} [mu : probability (measurableTypeR R) R], continuous (cf_im mu)
Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma continuous_cf_im mu : continuous (cf_im mu).
Used by 1 declaration in 1 file
lemma continuous_cf_norm main result source, line 290 
forall {R : realType} [mu : probability (measurableTypeR R) R], continuous (cf_norm mu)
Main result

Stated in the README together with cf_re0.

Statement as written in the source
Lemma continuous_cf_norm mu : continuous (cf_norm mu).
Used by 5 declarations in 3 files

If nu is the law of g under P, the characteristic function of nu is computed under P.

sectioncharfun_image
Context {R : realType} d (T : measurableType d) (P : probability T R).
Variables (nu : probability (measurableTypeR R) R) (g : T -> R).
Hypothesis mg : measurable_fun [set: T] g.
Hypothesis gnu : forall A : set (measurableTypeR R), measurable A ->
  P (g @^-1` A) = nu A.
lemma cf_re_image main result source, line 315 
forall {R : realType} [d : measure_display] [T : measurableType d] 
  [P : probability T R] [nu : probability (measurableTypeR R) R] 
  [g : T -> R],
measurable_fun [set: T] g ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> P (g @^-1` A) = nu A) ->
forall t : R, cf_re nu t = \int[P]_x cos (t * g x)
Main result

Stated in the README together with cf_image.

Statement as written in the source
Lemma cf_re_image t : cf_re nu t = \int[P]_x cos (t * g x).
Used by 1 declaration in 1 file
lemma cf_im_image main result source, line 322 
forall {R : realType} [d : measure_display] [T : measurableType d] 
  [P : probability T R] [nu : probability (measurableTypeR R) R] 
  [g : T -> R],
measurable_fun [set: T] g ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> P (g @^-1` A) = nu A) ->
forall t : R, cf_im nu t = \int[P]_x sin (t * g x)
Main result

Stated in the README together with cf_image.

Statement as written in the source
Lemma cf_im_image t : cf_im nu t = \int[P]_x sin (t * g x).
Used by 1 declaration in 1 file
lemma cf_image main result source, line 329 
forall {R : realType} [d : measure_display] [T : measurableType d] 
  [P : probability T R] [nu : probability (measurableTypeR R) R] 
  [g : T -> R],
measurable_fun [set: T] g ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> P (g @^-1` A) = nu A) ->
forall t : R, cf nu t = (\int[P]_x cos (t * g x), \int[P]_x sin (t * g x))
Main result, as the README states it

If nu is the law of a measurable g : T -> R under a probability P (P (g @^-1` A) = nu A for measurable A), then cf nu t = (E_P[cos (t g)], E_P[sin (t g)]).

Statement as written in the source
Lemma cf_image t :
  cf nu t = (\int[P]_x cos (t * g x), \int[P]_x sin (t * g x)).
Used by 5 declarations in 2 files
sectioncharfun_affine
Context {R : realType}.
Implicit Types (mu nu : probability (measurableTypeR R) R) (a b t : R).
lemma cf_affine main result source, line 341 
forall {R : realType} [mu nu : probability (measurableTypeR R) R] [a b : R],
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 mu ((fun x : R => a * x + b) @^-1` A) = nu A) ->
forall t : R, cf nu t = cmul (cos (b * t), sin (b * t)) (cf mu (a * t))

The law of a X + b: its characteristic function at t is exp (i b t) times that of X at a t.

Main result, as the README states it

The law of a X + b has the characteristic function exp (i b t) cf mu (a t), of modulus cf_norm mu (a t).

Statement as written in the source
Lemma cf_affine mu nu a b :
    (forall A : set (measurableTypeR R), measurable A ->
      mu ((fun x => a * x + b) @^-1` A) = nu A) ->
  forall t, cf nu t = cmul (cos (b * t), sin (b * t)) (cf mu (a * t)).
Used by 2 declarations in 1 file
lemma cf_norm_affine main result source, line 364 
forall {R : realType} [mu nu : probability (measurableTypeR R) R] [a b : R],
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 mu ((fun x : R => a * x + b) @^-1` A) = nu A) ->
forall t : R, cf_norm nu t = cf_norm mu (a * t)
Main result

Stated in the README together with cf_affine.

Statement as written in the source
Lemma cf_norm_affine mu nu a b :
    (forall A : set (measurableTypeR R), measurable A ->
      mu ((fun x => a * x + b) @^-1` A) = nu A) ->
  forall t, cf_norm nu t = cf_norm mu (a * t).
sectioncharfun_independent
Context {R : realType}.
lemma Rintegral_prod_bounded main result source, line 381 
forall {R : realType} [d1 d2 : measure_display] [T1 : measurableType d1]
  [T2 : measurableType d2] (P1 : probability T1 R) (P2 : probability T2 R)
  [F : T1 * T2 -> R] [C : R],
measurable_fun [set: T1 * T2] F ->
(forall p : T1 * T2, `|F p| <= C) ->
\int[(P1 \x P2)%E]_p F p = \int[P1]_x \int[P2]_y F (x, y)

Fubini for bounded measurable functions on a product of probabilities.

Main result, as the README states it

Fubini for a bounded measurable real function on a product of two probabilities.

Statement as written in the source
Lemma Rintegral_prod_bounded d1 d2 (T1 : measurableType d1)
    (T2 : measurableType d2) (P1 : probability T1 R) (P2 : probability T2 R)
    (F : T1 * T2 -> R) (C : R) :
  measurable_fun [set: T1 * T2] F -> (forall p, `|F p| <= C) ->
  \int[(P1 \x P2)%E]_p F p = \int[P1]_x \int[P2]_y F (x, y).
Used by 1 declaration in 1 file
lemma cf_iterated main result source, line 396 
forall {R : realType} [d1 d2 : measure_display] [T1 : measurableType d1]
  [T2 : measurableType d2] (P1 : probability T1 R) (P2 : probability T2 R) 
  [g1 : T1 -> R] [g2 : T2 -> R],
measurable_fun [set: T1] g1 ->
measurable_fun [set: T2] g2 ->
forall t : R,
(\int[P1]_x \int[P2]_y cos (t * (g1 x + g2 y)),
 \int[P1]_x \int[P2]_y sin (t * (g1 x + g2 y))) =
cmul (\int[P1]_x cos (t * g1 x), \int[P1]_x sin (t * g1 x))
  (\int[P2]_y cos (t * g2 y), \int[P2]_y sin (t * g2 y))

Independent sums: the characteristic function of g1 X1 + g2 X2, for independent X1 and X2, is the complex product of those of g1 X1 and of g2 X2. First for iterated integrals, then for the product measure.

Main result

Stated in the README together with cf_prod.

Statement as written in the source
Lemma cf_iterated d1 d2 (T1 : measurableType d1) (T2 : measurableType d2)
    (P1 : probability T1 R) (P2 : probability T2 R) (g1 : T1 -> R)
    (g2 : T2 -> R) :
    measurable_fun [set: T1] g1 -> measurable_fun [set: T2] g2 ->
  forall t,
  (\int[P1]_x \int[P2]_y cos (t * (g1 x + g2 y)),
   \int[P1]_x \int[P2]_y sin (t * (g1 x + g2 y))) =
  cmul (\int[P1]_x cos (t * g1 x), \int[P1]_x sin (t * g1 x))
    (\int[P2]_y cos (t * g2 y), \int[P2]_y sin (t * g2 y)).
Used by 2 declarations in 1 file
lemma cf_prod_integral main result source, line 429 
forall {R : realType} [d1 d2 : measure_display] [T1 : measurableType d1]
  [T2 : measurableType d2] (P1 : probability T1 R) (P2 : probability T2 R) 
  [g1 : T1 -> R] [g2 : T2 -> R],
measurable_fun [set: T1] g1 ->
measurable_fun [set: T2] g2 ->
forall t : R,
(\int[(P1 \x P2)%E]_p cos (t * (g1 p.1 + g2 p.2)),
 \int[(P1 \x P2)%E]_p sin (t * (g1 p.1 + g2 p.2))) =
cmul (\int[P1]_x cos (t * g1 x), \int[P1]_x sin (t * g1 x))
  (\int[P2]_y cos (t * g2 y), \int[P2]_y sin (t * g2 y))
Main result

Stated in the README together with cf_prod.

Statement as written in the source
Lemma cf_prod_integral d1 d2 (T1 : measurableType d1) (T2 : measurableType d2)
    (P1 : probability T1 R) (P2 : probability T2 R) (g1 : T1 -> R)
    (g2 : T2 -> R) :
    measurable_fun [set: T1] g1 -> measurable_fun [set: T2] g2 ->
  forall t,
  (\int[(P1 \x P2)%E]_p cos (t * (g1 p.1 + g2 p.2)),
   \int[(P1 \x P2)%E]_p sin (t * (g1 p.1 + g2 p.2))) =
  cmul (\int[P1]_x cos (t * g1 x), \int[P1]_x sin (t * g1 x))
    (\int[P2]_y cos (t * g2 y), \int[P2]_y sin (t * g2 y)).
Used by 4 declarations in 3 files
lemma cf_prod main result source, line 449 
forall {R : realType} [d1 d2 : measure_display] [T1 : measurableType d1]
  [T2 : measurableType d2] [P1 : probability T1 R] [P2 : probability T2 R] 
  [g1 : T1 -> R] [g2 : T2 -> R] [nu1 nu2 nu : probability (measurableTypeR R) R],
measurable_fun [set: T1] g1 ->
measurable_fun [set: T2] g2 ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> P1 (g1 @^-1` A) = nu1 A) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> P2 (g2 @^-1` A) = nu2 A) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 (P1 \x P2)%E ((fun p : T1 * T2 => g1 p.1 + g2 p.2) @^-1` A) = nu A) ->
forall t : R, cf nu t = cmul (cf nu1 t) (cf nu2 t)
Main result, as the README states it

Independent sums: for independent X1, X2 (laws P1, P2, joint law P1 \x P2) and measurable g1, g2, the characteristic function of g1 X1 + g2 X2 is the complex product of those of g1 X1 and g2 X2, so the moduli multiply.

Statement as written in the source
Lemma cf_prod d1 d2 (T1 : measurableType d1) (T2 : measurableType d2)
    (P1 : probability T1 R) (P2 : probability T2 R) (g1 : T1 -> R)
    (g2 : T2 -> R) (nu1 nu2 nu : probability (measurableTypeR R) R) :
    measurable_fun [set: T1] g1 -> measurable_fun [set: T2] g2 ->
    (forall A : set (measurableTypeR R), measurable A ->
      P1 (g1 @^-1` A) = nu1 A) ->
    (forall A : set (measurableTypeR R), measurable A ->
      P2 (g2 @^-1` A) = nu2 A) ->
    (forall A : set (measurableTypeR R), measurable A ->
      (P1 \x P2)%E ((fun p => g1 p.1 + g2 p.2)%R @^-1` A) = nu A) ->
  forall t, cf nu t = cmul (cf nu1 t) (cf nu2 t).
Used by 1 declaration in 1 file
lemma cf_norm_prod main result source, line 468 
forall {R : realType} [d1 d2 : measure_display] [T1 : measurableType d1]
  [T2 : measurableType d2] [P1 : probability T1 R] [P2 : probability T2 R] 
  [g1 : T1 -> R] [g2 : T2 -> R] [nu1 nu2 nu : probability (measurableTypeR R) R],
measurable_fun [set: T1] g1 ->
measurable_fun [set: T2] g2 ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> P1 (g1 @^-1` A) = nu1 A) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A -> P2 (g2 @^-1` A) = nu2 A) ->
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 (P1 \x P2)%E ((fun p : T1 * T2 => g1 p.1 + g2 p.2) @^-1` A) = nu A) ->
forall t : R, cf_norm nu t = cf_norm nu1 t * cf_norm nu2 t
Main result

Stated in the README together with cf_prod.

Statement as written in the source
Lemma cf_norm_prod d1 d2 (T1 : measurableType d1) (T2 : measurableType d2)
    (P1 : probability T1 R) (P2 : probability T2 R) (g1 : T1 -> R)
    (g2 : T2 -> R) (nu1 nu2 nu : probability (measurableTypeR R) R) :
    measurable_fun [set: T1] g1 -> measurable_fun [set: T2] g2 ->
    (forall A : set (measurableTypeR R), measurable A ->
      P1 (g1 @^-1` A) = nu1 A) ->
    (forall A : set (measurableTypeR R), measurable A ->
      P2 (g2 @^-1` A) = nu2 A) ->
    (forall A : set (measurableTypeR R), measurable A ->
      (P1 \x P2)%E ((fun p => g1 p.1 + g2 p.2)%R @^-1` A) = nu A) ->
  forall t, (cf_norm nu t = cf_norm nu1 t * cf_norm nu2 t)%R.
sectioncharfun_tuple_prod
Context {R : realType}.
Implicit Types (mu : nat -> probability (measurableTypeR R) R) (a : nat -> R).
lemma measurable_tuple_lincomb source, line 490 
forall {R : realType} [n : nat] (a : nat -> R),
measurable_fun [set: n.-tuple (measurableTypeR R)]
  (fun x : n.-tuple _ =>
   \sum_(k < n) a k * tnth x k)
Statement as written in the source
Lemma measurable_tuple_lincomb n a :
  measurable_fun [set: n.-tuple (measurableTypeR R)]
    (fun x => \sum_(k < n) a k * tnth x k).
Used by 2 declarations in 1 file
let tuple_lincomb_cons section-local source, line 498 
Let tuple_lincomb_cons n a (s : measurableTypeR R)
    (ts : n.-tuple (measurableTypeR R)) :
  \sum_(k < n.+1) a k * tnth (tuple_cons (s, ts)) k =
  a 0%N * s + \sum_(k < n) a k.+1 * tnth ts k.
Used by 1 declaration in 1 file
lemma cf_tuple_prod_integral main result source, line 510 
forall {R : realType} (mu : nat -> probability (measurableTypeR R) R) 
  (n : nat) (a : nat -> R) (t : R),
(\int[tuple_prod mu n]_x cos (t * \sum_(k < n) a k * tnth x k),
 \int[tuple_prod mu n]_x sin (t * \sum_(k < n) a k * tnth x k)) =
\big[cmul/(1, 0)]_(k < n) cf (mu k) (a k * t)

Independent coordinates: for x of law tuple_prod mu n, the characteristic function of \sum_k a_k x_k at t is the complex product of the characteristic functions of the laws mu k at a_k t.

Main result

Stated in the README together with cf_tuple_prod.

Statement as written in the source
Lemma cf_tuple_prod_integral mu n a t :
  (\int[tuple_prod mu n]_x cos (t * \sum_(k < n) a k * tnth x k),
   \int[tuple_prod mu n]_x sin (t * \sum_(k < n) a k * tnth x k)) =
  \big[cmul/(1, 0)]_(k < n) cf (mu k) (a k * t).
Used by 2 declarations in 2 files
lemma cf_tuple_prod main result source, line 550 
forall {R : realType} [mu : nat -> probability (measurableTypeR R) R] 
  [n : nat] [a : nat -> R] [nu : probability (measurableTypeR R) R],
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 tuple_prod mu n ((fun x : n.-tuple R => \sum_(k < n) a k * tnth x k) @^-1` A) = nu A) ->
forall t : R, cf nu t = \big[cmul/(1, 0)]_(k < n) cf (mu k) (a k * t)
Main result, as the README states it

For x of law tuple_prod mu n (independent coordinates of laws mu 0, ..., mu (n-1)) and reals a k, the characteristic function of \sum_k a_k x_k at t is the complex product of the cf (mu k) (a_k t), and its modulus is the product of the cf_norm (mu k) (a_k t).

Statement as written in the source
Lemma cf_tuple_prod mu n a (nu : probability (measurableTypeR R) R) :
    (forall A : set (measurableTypeR R), measurable A ->
      tuple_prod mu n ((fun x => \sum_(k < n) a k * tnth x k) @^-1` A) =
      nu A) ->
  forall t, cf nu t = \big[cmul/(1, 0)]_(k < n) cf (mu k) (a k * t).
Used by 2 declarations in 2 files
lemma cf_norm_tuple_prod main result source, line 560 
forall {R : realType} [mu : nat -> probability (measurableTypeR R) R] 
  [n : nat] [a : nat -> R] [nu : probability (measurableTypeR R) R],
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 tuple_prod mu n ((fun x : n.-tuple R => \sum_(k < n) a k * tnth x k) @^-1` A) = nu A) ->
forall t : R, cf_norm nu t = \prod_(k < n) cf_norm (mu k) (a k * t)
Main result

Stated in the README together with cf_tuple_prod.

Statement as written in the source
Lemma cf_norm_tuple_prod mu n a (nu : probability (measurableTypeR R) R) :
    (forall A : set (measurableTypeR R), measurable A ->
      tuple_prod mu n ((fun x => \sum_(k < n) a k * tnth x k) @^-1` A) =
      nu A) ->
  forall t, cf_norm nu t = \prod_(k < n) cf_norm (mu k) (a k * t).
Used by 1 declaration in 1 file
sectioncharfun_symmetrization
Context {R : realType}.
Implicit Types (mu nu : probability (measurableTypeR R) R).
lemma cf_sym main result source, line 575 
forall {R : realType} [mu nu : probability (measurableTypeR R) R],
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 (mu \x mu)%E ((fun p : R * R => p.1 - p.2 : R) @^-1` A) = nu A) ->
forall t : R, cf nu t = (cf_norm mu t ^+ 2, 0)

The law of X - X', for independent X and X' of law mu, has the real characteristic function |cf mu|^2.

Main result, as the README states it

Symmetrization: the law of X - X', for independent X and X' of law mu, has the real characteristic function cf_norm mu t ^ 2.

Statement as written in the source
Lemma cf_sym mu nu :
    (forall A : set (measurableTypeR R), measurable A ->
      (mu \x mu)%E ((fun p => p.1 - p.2 : R) @^-1` A) = nu A) ->
  forall t, cf nu t = (cf_norm mu t ^+ 2, 0).
Used by 2 declarations in 2 files
lemma cf_norm_sym main result source, line 597 
forall {R : realType} [mu nu : probability (measurableTypeR R) R],
(forall A : set (measurableTypeR R),
 (((R.-ocitv).-measurable).-sigma).-measurable A ->
 (mu \x mu)%E ((fun p : R * R => p.1 - p.2 : R) @^-1` A) = nu A) ->
forall t : R, cf_norm nu t = cf_norm mu t ^+ 2
Main result

Stated in the README together with cf_sym.

Statement as written in the source
Lemma cf_norm_sym mu nu :
    (forall A : set (measurableTypeR R), measurable A ->
      (mu \x mu)%E ((fun p => p.1 - p.2 : R) @^-1` A) = nu A) ->
  forall t, cf_norm nu t = cf_norm mu t ^+ 2.
sectiontrig_derive
Context {R : realType}.
lemma is_derive_mull source, line 611 
forall {R : realType} (k x : R), is_derive x 1 [eta  *%R k] k
Statement as written in the source
Lemma is_derive_mull (k x : R) : is_derive x 1 (fun s : R => k * s) k.
Used by 3 declarations in 1 file
lemma is_derive_mulr source, line 617 
forall {R : realType} (k x : R), is_derive x 1 ( *%R^~ k) k
Statement as written in the source
Lemma is_derive_mulr (k x : R) : is_derive x 1 (fun s : R => s * k) k.
Used by 3 declarations in 2 files
lemma is_derive_cos_mul main result source, line 625 
forall {R : realType} (t x : R),
is_derive x 1 (fun s : R => cos (t * s))
  (- (t * sin (t * x)))

Derivatives of s |-> cos (t s), sin (t s), cos (s z) and sin (s z).

Main result, as the README states it

Derivatives of s |-> cos (t s), sin (t s), cos (s z) and sin (s z).

Statement as written in the source
Lemma is_derive_cos_mul (t x : R) :
  is_derive x 1 (fun s => cos (t * s)) (- (t * sin (t * x))).
Used by 1 declaration in 1 file
lemma is_derive_sin_mul main result source, line 633 
forall {R : realType} (t x : R),
is_derive x 1 (fun s : R => sin (t * s))
  (t * cos (t * x))
Main result

Stated in the README together with is_derive_cos_mul.

Statement as written in the source
Lemma is_derive_sin_mul (t x : R) :
  is_derive x 1 (fun s => sin (t * s)) (t * cos (t * x)).
Used by 1 declaration in 1 file
lemma is_derive_cos_mulr main result source, line 641 
forall {R : realType} (z t : R),
is_derive t 1 (fun s : R => cos (s * z))
  (- (z * sin (t * z)))
Main result

Stated in the README together with is_derive_cos_mul.

Statement as written in the source
Lemma is_derive_cos_mulr (z t : R) :
  is_derive t 1 (fun s => cos (s * z)) (- (z * sin (t * z))).
Used by 3 declarations in 2 files
lemma is_derive_sin_mulr main result source, line 649 
forall {R : realType} (z t : R),
is_derive t 1 (fun s : R => sin (s * z))
  (z * cos (t * z))
Main result

Stated in the README together with is_derive_cos_mul.

Statement as written in the source
Lemma is_derive_sin_mulr (z t : R) :
  is_derive t 1 (fun s => sin (s * z)) (z * cos (t * z)).
Used by 2 declarations in 2 files
sectioncharfun_normal
Context {R : realType}.
Local Notation N := (@normal_prob R 0 1).
let integrable_normal_abs section-local source, line 663 
Let integrable_normal_abs :
  N.-integrable [set: R] (EFin \o (fun x : R => `|x|)).
Used by 3 declarations in 1 file
let integrable_normal_mul_bounded section-local source, line 670 
Let integrable_normal_mul_bounded (f : R -> R) :
  measurable_fun [set: R] f -> (forall x, `|f x| <= 1) ->
  N.-integrable [set: R] (EFin \o (fun x => x * f x)).
Used by 1 declaration in 1 file
let itv_t section-local source, line 680 
Let itv_t (t : R) : t \in `]t - 1, t + 1[.
Used by 2 declarations in 1 file
let derive_cf_re_normal section-local source, line 683 
Let derive_cf_re_normal (t : R) :
  is_derive t 1 (cf_re N) (\int[N]_x (- (x * sin (t * x)))).
Used by 1 declaration in 1 file
let derive_cf_im_normal section-local source, line 697 
Let derive_cf_im_normal (t : R) :
  is_derive t 1 (cf_im N) (\int[N]_x (x * cos (t * x))).
Used by 1 declaration in 1 file
let continuous_mul_cos section-local source, line 713 
Let continuous_mul_cos (t : R) : continuous (fun x : R => t * cos (t * x)).

Stein's identity gives E[x sin (t x)] = t E[cos (t x)] and E[x cos (t x)] = - t E[sin (t x)].

Used by 1 declaration in 1 file
let continuous_mul_sin section-local source, line 721 
Let continuous_mul_sin (t : R) : continuous (fun x : R => - (t * sin (t * x))).
Used by 1 declaration in 1 file
let normal_x_sin section-local source, line 731 
Let normal_x_sin (t : R) : \int[N]_x (x * sin (t * x)) = t * cf_re N t.
Used by 1 declaration in 1 file
let normal_x_cos section-local source, line 744 
Let normal_x_cos (t : R) : \int[N]_x (x * cos (t * x)) = - t * cf_im N t.
Used by 1 declaration in 1 file
let gauss_ode section-local source, line 760 
Let gauss_ode (y : R -> R) : (forall t : R, is_derive t 1 y (- t * y t)) ->
  forall t : R, y t = y 0 * expR (- t ^+ 2 / 2).

A solution of y' = - t y is t |-> y 0 * expR (- t ^ 2 / 2).

Used by 2 declarations in 1 file
lemma cf_re_normal01 source, line 784 
forall {R : realType} (t : R), cf_re (normal_prob 0 1) t = expR (- t ^+ 2 / 2)
Statement as written in the source
Lemma cf_re_normal01 (t : R) : cf_re N t = expR (- t ^+ 2 / 2).
Used by 2 declarations in 2 files
lemma cf_im_normal01 source, line 794 
forall {R : realType} (t : R), cf_im (normal_prob 0 1) t = 0
Statement as written in the source
Lemma cf_im_normal01 (t : R) : cf_im N t = 0.
Used by 1 declaration in 1 file
lemma cf_normal main result source, line 801 
forall {R : realType} (m : R) [s : R],
s != 0 ->
forall t : R,
cf (normal_prob m s) t =
(expR (- (s * t) ^+ 2 / 2) * cos (m * t), expR (- (s * t) ^+ 2 / 2) * sin (m * t))
Main result, as the README states it

For s != 0, the characteristic function of normal_prob m s at t is expR (- (s t)^2 / 2) (cos (m t), sin (m t)), of modulus expR (- (s t)^2 / 2). Proved for the standard law by differentiating under the integral and Stein's identity (normal_ibp), which give y' = - t y, then by cf_affine.

Statement as written in the source
Lemma cf_normal (m s : R) : s != 0 -> forall t : R,
  cf (normal_prob m s) t =
  (expR (- (s * t) ^+ 2 / 2) * cos (m * t),
   expR (- (s * t) ^+ 2 / 2) * sin (m * t)).
Used by 4 declarations in 2 files
lemma cf_norm_normal main result source, line 815 
forall {R : realType} (m : R) [s : R],
s != 0 -> forall t : R, cf_norm (normal_prob m s) t = expR (- (s * t) ^+ 2 / 2)
Main result

Stated in the README together with cf_normal.

Statement as written in the source
Lemma cf_norm_normal (m s : R) : s != 0 -> forall t : R,
  cf_norm (normal_prob m s) t = expR (- (s * t) ^+ 2 / 2).
lemma cf_re_normal main result source, line 823 
forall {R : realType} (m : R) [s : R],
s != 0 -> forall t : R, cf_re (normal_prob m s) t = expR (- (s * t) ^+ 2 / 2) * cos (m * t)
Main result

Stated in the README together with cf_normal.

Statement as written in the source
Lemma cf_re_normal (m s : R) : s != 0 -> forall t : R,
  cf_re (normal_prob m s) t = expR (- (s * t) ^+ 2 / 2) * cos (m * t).
lemma cf_im_normal main result source, line 827 
forall {R : realType} (m : R) [s : R],
s != 0 -> forall t : R, cf_im (normal_prob m s) t = expR (- (s * t) ^+ 2 / 2) * sin (m * t)
Main result

Stated in the README together with cf_normal.

Statement as written in the source
Lemma cf_im_normal (m s : R) : s != 0 -> forall t : R,
  cf_im (normal_prob m s) t = expR (- (s * t) ^+ 2 / 2) * sin (m * t).
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.