Library mathcomp.analysis.summability

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
Require Reals.
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
From mathcomp Require Import interval zmodp.
From mathcomp.classical Require Import boolp classical_sets.
Require Import ereal reals.
Require Import Rstruct signed 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.