Module mathcomp.analysis.showcase.summability
From HB Require Import structures.From mathcomp Require Import all_ssreflect_compat 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.
This file proposes a replacement for the definition `summable` (file
`realsum.v`).
Set 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
{ : choiceType} : set_system {fset I} :=NGenCInfty.G : set (set nat) NGenCInfty.G is not universe polymorphic NGenCInfty.G is transparent Expands to: Constant mathcomp.analysis.measurable_realfun.NGenCInfty.G Declared in library mathcomp.analysis.measurable_realfun, line 1180, characters 11-12
Source code
filter_from setT (fun => [set | A `<=` B]).
Instance
totally_filter
Source code
{ : choiceType} : ProperFilter (@totally I).Source code
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.
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
{ : choiceType} { : zmodType}Source code
( : I -> R) ( : {fset I}) : R := \sum_( : A) x (val i).
Definition
sum
Source code
( : choiceType) { : numDomainType} { : normedModType K}Source code
( : I -> R) : R := lim (partial_sum x @ totally).
Definition
summable
Source code
( : choiceType) { : realType} { : normedModType K}Source code
( : I -> R) :=
\forall \near +oo%R, \forall \near totally,
(partial_sum (fun => `|x i|) J <= M)%R.
End totally.