Library Coq.Reals.PSeries_reg
Uniform convergence
Definition CVU (
fn:nat ->
R ->
R) (
f:R ->
R) (
x:R)
(
r:posreal) :
Prop :=
forall eps:R,
0 <
eps ->
exists N :
nat,
(
forall (
n:nat) (
y:R),
(
N <=
n)%nat ->
Boule x r y ->
Rabs (
f y -
fn n y) <
eps).
Normal convergence
Definition CVN_r (
fn:nat ->
R ->
R) (
r:posreal) :
Type :=
{
An:nat ->
R &
{
l:R |
Un_cv (
fun n:nat =>
sum_f_R0 (
fun k:nat =>
Rabs (
An k))
n)
l /\
(
forall (
n:nat) (
y:R),
Boule 0
r y ->
Rabs (
fn n y) <=
An n) } }.
Definition CVN_R (
fn:nat ->
R ->
R) :
Type :=
forall r:posreal,
CVN_r fn r.
Definition SFL (
fn:nat ->
R ->
R)
(
cv:forall
x:R, {
l:R |
Un_cv (
fun N:nat =>
SP fn N x)
l })
(
y:R) :
R :=
let (
a,_) :=
cv y in a.
In a complete space, normal convergence implies uniform convergence
Lemma CVN_CVU :
forall (
fn:nat ->
R ->
R)
(
cv:forall
x:R, {
l:R |
Un_cv (
fun N:nat =>
SP fn N x)
l })
(
r:posreal),
CVN_r fn r ->
CVU (
fun n:nat =>
SP fn n) (
SFL fn cv) 0
r.
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