Library Coq.Reals.PSeries_reg
Uniform convergence
Normal convergence
In a complete space, normal convergence implies uniform convergence
Each limit of a sequence of functions which converges uniformly is continue
Continuity and normal convergence
As R is complete, normal convergence implies that (fn) is simply-uniformly convergent
Lemma CVN_R_CVS :
forall fn:
nat -> R -> R,
CVN_R fn -> forall x:
R,
{ l:R | Un_cv (
fun N:
nat =>
SP fn N x)
l }.
Lemma CVU_cv :
forall f g c d,
CVU f g c d ->
forall x,
Boule c d x -> Un_cv (
fun n =>
f n x) (
g x).
Lemma CVU_ext_lim :
forall f g1 g2 c d,
CVU f g1 c d -> (forall x,
Boule c d x -> g1 x = g2 x) ->
CVU f g2 c d.
Lemma CVU_derivable :
forall f f' g g' c d,
CVU f' g' c d ->
(forall x,
Boule c d x -> Un_cv (
fun n =>
f n x) (
g x)
) ->
(forall n x,
Boule c d x -> derivable_pt_lim (
f n)
x (
f' n x)
) ->
forall x,
Boule c d x -> derivable_pt_lim g x (
g' x).