Library mathcomp.analysis.summability

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
Require Reals.
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
From mathcomp Require Import seq fintype bigop ssralg ssrint ssrnum finmap.
From mathcomp Require Import matrix interval zmodp.
Require Import boolp ereal reals.
Require Import Rstruct classical_sets posnum topology normedtype.

Set Implicit Arguments.
Import GRing.Theory Num.Def Num.Theory.

Local Open Scope classical_set_scope.

From mathcomp Require fintype bigop finmap.

Section totally.

Import fintype bigop finmap.
Local Open Scope fset_scope.

Definition totally {I : choiceType} : set (set {fset I}) :=
  filter_from setT (fun A ⇒ [set B | A `<=` B]).

Canonical totally_filter_source {I : choiceType} X :=
  @Filtered.Source X _ {fset I} (fun f ⇒ f @ totally).

Instance totally_filter {I : choiceType} : ProperFilter (@totally I).

Definition partial_sum {I : choiceType} {R : zmodType}
  (x : I → R) (A : {fset I}) : R := \sum_(i : A) x (val i).

Definition sum (I : choiceType) {K : numDomainType} {R : normedModType K}
   (x : I → R) : R := lim (partial_sum x).

Definition summable (I : choiceType) {K : realType} {R : normedModType K}
   (x : I → R) :=
   \∀ M \near +oo%R, \∀ J \near totally,
   (partial_sum (fun i ⇒ `|x i|) J ≤ M)%R.

End totally.