Top source

Module mathcomp.analysis.showcase.summability

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrint ssrnum finmap matrix.
From mathcomp Require Import interval zmodp.
From mathcomp Require Import boolp classical_sets.
From mathcomp Require Import ereal reals topology normedtype.


Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
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

---

Source code

{

I

---

Source code

: choiceType} : set_system {fset I} :=
  filter_from setT (fun

A

---

Source code

=> [set

B

---

Source code

| A `<=` B]).

Instance

totally_filter

---

Source code

{

I

---

Source code

: choiceType} : ProperFilter (@totally I).

Proof.

eapply filter_from_proper; last by move=> A _; exists A; rewrite /= fsubset_refl.
apply: filter_fromT_filter; first by exists fset0.
by move=> A B /=; exists (A `|` B) => P /=; rewrite fsubUset => /andP[].
Qed.

Definition

partial_sum

---

Source code

{

I

---

Source code

: choiceType} {

R

---

Source code

: zmodType}
  (

x

---

Source code

: I -> R) (

A

---

Source code

: {fset I}) : R := \sum_(

i

---

Source code

: A) x (val i).

Definition

sum

---

Source code

(

I

---

Source code

: choiceType) {

K

---

Source code

: numDomainType} {

R

---

Source code

: normedModType K}
   (

x

---

Source code

: I -> R) : R := lim (partial_sum x @ totally).

Definition

summable

---

Source code

(

I

---

Source code

: choiceType) {

K

---

Source code

: realType} {

R

---

Source code

: normedModType K}
   (

x

---

Source code

: I -> R) :=
   \forall

M

---

Source code

\near +oo%R, \forall

J

---

Source code

\near totally,
   (partial_sum (fun

i

---

Source code

=> `|x i|) J <= M)%R.

End totally.