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
totally : forall {I : choiceType}, set_system {fset I} totally is not universe polymorphic Arguments totally {I} _ totally is transparent Expands to: Constant mathcomp.analysis.showcase.summability.totally Declared in library mathcomp.analysis.showcase.summability, line 29, characters 11-18
Source code {ISource code : choiceType} : set_system {fset I} :=
filter_from setT (fun ASource code => [set BSource code | A `<=` B]).
Instance totally_filterSource code {ISource code : choiceType} : ProperFilter (@totally I).
Proof.
apply: filter_fromT_filter; first by exists fset0.
by move=> A B /=; exists (A `|` B) => P /=; rewrite fsubUset => /andP[].
Qed.
Definition partial_sum
partial_sum : forall {I : choiceType} {R : GRing.Zmodule.Exports.zmodType}, (I -> R) -> {fset I} -> R partial_sum is not universe polymorphic Arguments partial_sum {I R} x%_function_scope A partial_sum is transparent Expands to: Constant mathcomp.analysis.showcase.summability.partial_sum Declared in library mathcomp.analysis.showcase.summability, line 39, characters 11-22
Source code {ISource code : choiceType} {RSource code : zmodType}
(xSource code : I -> R) (ASource code : {fset I}) : R := \sum_(iSource code : A) x (val i).
Definition sum
sum : forall [I : choiceType] {K : numDomainType} {R : normedModType K}, (I -> R) -> R sum is not universe polymorphic Arguments sum [I] {K R} x%_function_scope sum is transparent Expands to: Constant mathcomp.analysis.showcase.summability.sum Declared in library mathcomp.analysis.showcase.summability, line 42, characters 11-14
Source code (ISource code : choiceType) {KSource code : numDomainType} {RSource code : normedModType K}
(xSource code : I -> R) : R := lim (partial_sum x @ totally).
Definition summable
summable : forall [I : choiceType] {K : realType} {R : normedModType K}, (I -> R) -> Prop summable is not universe polymorphic Arguments summable [I] {K R} x%_function_scope summable is transparent Expands to: Constant mathcomp.analysis.showcase.summability.summable Declared in library mathcomp.analysis.showcase.summability, line 45, characters 11-19
Source code (ISource code : choiceType) {KSource code : realType} {RSource code : normedModType K}
(xSource code : I -> R) :=
\forall MSource code \near +oo%R, \forall JSource code \near totally,
(partial_sum (fun iSource code => `|x i|) J <= M)%R.
End totally.