GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisgaussianparameter_integral

Continuity of a parameter integral

GaussianAnalysis.gaussian.parameter_integrallibrary/gaussian/parameter_integral.v99 lines2 lemmas and theoremssource
Imports 0 library modules and 15 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, 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.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral

Imported by 4
Required by 1 files of the paper proofs

cvg_seqP is the sequential criterion for the limit of a function at a point of a pseudometric space: f x tends to l as x tends to x0 as soon as f (u n) tends to l for every sequence u that tends to x0.

continuity_under_integral_at: if f x y is, for every y in B, continuous in x at x0, and `|f x y| <= g y for x in a neighbourhood of x0 and y in B, with g integrable on B, then x |-> \int[mu]_(y in B) f x y is continuous at x0, by dominated convergence along sequences. MathComp-Analysis states this for a real parameter in an open interval (continuity_under_integral); here the parameter ranges over a pseudometric space, such as 'rV[R]_n.

Main results

ResultsStatementUsed by theories/
cvg_seqP
Sequential criterion for a limit at a point x0 of a pseudometric space: f x tends to l as x tends to x0 as soon as f (u n) tends to l for every sequence u that tends to x0.
continuity_under_integral_at
Continuity of a parameter integral at a point x0 of a pseudometric space: if f x y is continuous in x at x0 for every y in B, and bounded by an integrable g y for x near x0, then x |-> \int_B f x y dmu(y) is continuous at x0. MathComp-Analysis states this for a real parameter in an open interval.Gaussian/Law/LibraryBridge, for Gaussian/Iterated/PolynomialGrowth

Declarations2 exported, 1 local

lemma, theoremdefinitioninstancelocal
sectioncvg_seqP
Context {R : realType} {X : pseudoMetricType R} {V : pseudoMetricType R}.
lemma cvg_seqP main result source, line 35 
forall {R : realType} {X V : pseudoMetricType R} [h : X -> V] [x0 : X] [l : V],
(forall u : nat -> X, u n @[n --> \oo] --> x0 -> h (u n) @[n --> \oo] --> l) ->
h x @[x --> x0] --> l
Main result, as the README states it

Sequential criterion for a limit at a point x0 of a pseudometric space: f x tends to l as x tends to x0 as soon as f (u n) tends to l for every sequence u that tends to x0.

Statement as written in the source
Lemma cvg_seqP (h : X -> V) (x0 : X) (l : V) :
  (forall u : nat -> X, u n @[n --> \oo] --> x0 -> h (u n) @[n --> \oo] --> l) ->
  h x @[x --> x0] --> l.
Used by 1 declaration in 1 file
sectioncontinuity_under_integral_at
Context {R : realType} {X : pseudoMetricType R} d {Y : measurableType d}.
Variable mu : {measure set Y -> \bar R}.
Variables (f : X -> Y -> R) (B : set Y) (x0 : X) (U : set X) (g : Y -> R).
Hypothesis mB : measurable B.
Hypothesis Ux0 : nbhs x0 U.
Hypothesis int_f : forall x, U x -> mu.-integrable B (EFin \o f x).
Hypothesis cf : forall y, B y -> {for x0, continuous (f ^~ y)}.
Hypothesis int_g : mu.-integrable B (EFin \o g).
Hypothesis g_ub : forall x, U x -> forall y, B y -> `|f x y| <= g y.
let cvg_shiftnW section-local source, line 68 
Let cvg_shiftnW {V : pseudoMetricType R} (v : nat -> V) (l : V) N :
  v (n + N)%N @[n --> \oo] --> l -> v @ \oo --> l.

A sequence converges when a shift of it does.

Used by 1 declaration in 1 file
lemma continuity_under_integral_at main result source, line 78 
forall {R : realType} {X : pseudoMetricType R} [d : measure_display] 
  {Y : measurableType d} [mu : measure Y R] [f : X -> Y -> R] [B : set Y] 
  [x0 : X] [U : set X] [g : Y -> R],
d.-measurable B ->
nbhs x0 U ->
(forall x : X, U x -> mu.-integrable B (EFin \o f x)) ->
(forall y : Y, B y -> {for x0, continuous (f^~ y)}) ->
mu.-integrable B (EFin \o g) ->
(forall x : X, U x -> forall y : Y, B y -> `|f x y| <= g y) ->
{for x0, continuous (fun x1 : X => \int[mu]_(y in B) f x1 y)}
Main result, as the README states it

Continuity of a parameter integral at a point x0 of a pseudometric space: if f x y is continuous in x at x0 for every y in B, and bounded by an integrable g y for x near x0, then x |-> \int_B f x y dmu(y) is continuous at x0. MathComp-Analysis states this for a real parameter in an open interval.

Used in theories/ by: Gaussian/Law/LibraryBridge, for Gaussian/Iterated/PolynomialGrowth
Statement as written in the source
Lemma continuity_under_integral_at :
  {for x0, continuous (fun x => \int[mu]_(y in B) f x y)}.
Used by 9 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.