GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisgaussiannormal_integral

Integrals against the normal law

GaussianAnalysis.gaussian.normal_integrallibrary/gaussian/normal_integral.v175 lines6 lemmas and theoremssource
Imports 0 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.arithmetic_tactic, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.classical.cardinality, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.algebra.interval, mathcomp.algebra.interval_inference, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.analysis.numfun, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_stieltjes_measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.charge, mathcomp.analysis.probability_theory.probability

Imported by 25
Required by 4 files of the paper proofs

MathComp-Analysis defines normal_prob m s as the measure with density normal_pdf m s against Lebesgue measure. This file turns that definition into a formula for integrals (integral_normal_prob) and proves that the powers, hence the functions of polynomial growth, are integrable against the standard normal law, with mean 0.

Main results

ResultsStatement
integral_normal_probintegrable_normal_prob
Integrating against normal_prob m s is integrating against Lebesgue measure with the density normal_pdf m s, for nonnegative or integrable functions.
integrable_normal_exprnintegrable_normal_poly
Every power |x|^k, hence every measurable function bounded by C (1 + |x|^k), is integrable against the standard normal law.

Declarations6 exported, 2 local

lemma, theoremdefinitioninstancelocal
sectionnormal_density
Context {R : realType} (m s : R).
Local Notation mu := (@lebesgue_measure R).
Local Notation P := (normal_prob m s).
let measurable_pdf section-local source, line 36 
Let measurable_pdf : measurable_fun [set: measurableTypeR R]
  (fun x => (normal_pdf m s x)%:E).
let RN_pdf section-local source, line 40 
Let RN_pdf : ae_eq mu [set: R] (Radon_Nikodym_SigmaFinite.f P mu)
  (fun x => (normal_pdf m s x)%:E).
Used by 1 declaration in 1 file
lemma ge0_integral_normal_prob source, line 50 
forall {R : realType} (m s : R) [f : R -> \bar R],
(forall x : R, (0%R <= f x)%E) ->
measurable_fun [set: R] f ->
(\int[normal_prob m s]_x f x)%E =
(\int[lebesgue_measure]_x (f x * (normal_pdf m s x)%:E))%E
Statement as written in the source
Lemma ge0_integral_normal_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 * (normal_pdf m s x)%:E))%E.
Used by 10 declarations in 9 files
lemma integrable_normal_prob main result source, line 65 
forall {R : realType} (m s : R) [f : R -> \bar R],
measurable_fun [set: R] f ->
(normal_prob m s).-integrable [set: R] f <->
lebesgue_measure.-integrable [set: R]
  (fun
     x : g_sigma_algebraType
           (R.-ocitv).-measurable =>
   (f x * (normal_pdf m s x)%:E)%E)
Main result

Stated in the README together with integral_normal_prob.

Statement as written in the source
Lemma integrable_normal_prob (f : R -> \bar R) : measurable_fun [set: R] f ->
  P.-integrable [set: R] f <->
  mu.-integrable [set: R] (fun x => f x * (normal_pdf m s x)%:E)%E.
Used by 3 declarations in 3 files
lemma integral_normal_prob main result source, line 83 
forall {R : realType} [m s : R] [f : R -> \bar R],
(normal_prob m s).-integrable [set: R] f ->
(\int[normal_prob m s]_x f x)%E =
(\int[lebesgue_measure]_x (f x * (normal_pdf m s x)%:E))%E
Main result, as the README states it

Integrating against normal_prob m s is integrating against Lebesgue measure with the density normal_pdf m s, for nonnegative or integrable functions.

Statement as written in the source
Lemma integral_normal_prob (f : R -> \bar R) : P.-integrable [set: R] f ->
  (\int[P]_x f x = \int[mu]_x (f x * (normal_pdf m s x)%:E))%E.
Used by 3 declarations in 3 files
sectionstandard_normal_moments
Context {R : realType}.
Local Notation mu := (@lebesgue_measure R).
Local Notation N := (@normal_prob R 0 1).
lemma exprn_le_expR source, line 105 
forall {R : realType} (x : R) (k : nat), `|x| ^+ k <= (k`! * 4 ^ k)%:R * expR (x ^+ 2 / 4)
Statement as written in the source
Lemma exprn_le_expR (x : R) k :
  `|x| ^+ k <= (k`! * 4 ^ k)%:R * expR (x ^+ 2 / 4).
Used by 2 declarations in 2 files
lemma integrable_normal_exprn main result source, line 129 
forall {R : realType} (k : nat),
(normal_prob 0 1).-integrable [set: R]
  (fun
     x : g_sigma_algebraType
           (R.-ocitv).-measurable =>
   (`|x| ^+ k)%:E)
Main result, as the README states it

Every power |x|^k, hence every measurable function bounded by C (1 + |x|^k), is integrable against the standard normal law.

Statement as written in the source
Lemma integrable_normal_exprn k :
  N.-integrable [set: R] (fun x => (`|x| ^+ k)%:E).
Used by 3 declarations in 3 files
lemma integrable_normal_poly main result source, line 161 
forall {R : realType} [f : R -> R] [C : R] [k : nat],
measurable_fun [set: R] f ->
(forall x : R, `|f x| <= C * (1 + `|x| ^+ k)) ->
(normal_prob 0 1).-integrable [set: R] (EFin \o f)
Main result

Stated in the README together with integrable_normal_exprn.

Statement as written in the source
Lemma integrable_normal_poly (f : R -> R) (C : R) k :
  measurable_fun [set: R] f -> (forall x, `|f x| <= C * (1 + `|x| ^+ k)) ->
  N.-integrable [set: R] (EFin \o f).
Used by 14 declarations in 4 files
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.