Library probsa.util.bigop_inf
(* ---------------------------------- Prosa --------------------------------- *)
Require Export prosa.util.ssrlia.
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export notation boolp etime iota bigop indicator.
(* ---------------------------------- Main ---------------------------------- *)
Lemma SeriesC_scal_l :
∀ {X : countType} (c : R) (f : X → R),
∑[∞]_{x <- X} c × f x = c × ∑[∞]_{x <- X} f x.
Lemma SeriesC_pos :
∀ {X : countType} (f : X → R),
(∀ x, 0 ≤ f x) →
0 ≤ ∑[∞]_{i<-_} f i.
Lemma is_seriesC_bump (A : countType) (x' : A) f :
is_series (countable_sum (λ x, if x == x' then f x else 0)) (f x').
Lemma SeriesCf_bump :
∀ (A : countType) (x' : A) (f : _), ∑[∞]_{x<-A}(if x == x' then f x else 0) = f x'.
Definition is_some {X} (o : option X) : bool :=
if o is Some _ then true else false.
Require Export prosa.util.ssrlia.
(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export notation boolp etime iota bigop indicator.
(* ---------------------------------- Main ---------------------------------- *)
Lemma SeriesC_scal_l :
∀ {X : countType} (c : R) (f : X → R),
∑[∞]_{x <- X} c × f x = c × ∑[∞]_{x <- X} f x.
Lemma SeriesC_pos :
∀ {X : countType} (f : X → R),
(∀ x, 0 ≤ f x) →
0 ≤ ∑[∞]_{i<-_} f i.
Lemma is_seriesC_bump (A : countType) (x' : A) f :
is_series (countable_sum (λ x, if x == x' then f x else 0)) (f x').
Lemma SeriesCf_bump :
∀ (A : countType) (x' : A) (f : _), ∑[∞]_{x<-A}(if x == x' then f x else 0) = f x'.
Definition is_some {X} (o : option X) : bool :=
if o is Some _ then true else false.
"Pickle bijection" defines a very strong type of equivalence
between two count-types. Recall that count-types are types that
contain elements that can be enumerated with natural numbers. The
fact that x : X is "pickle" equivalent to y : Y means that
there is a natural number i such that x is i-th element of
X and y is i-th element of Y. Such an equivalence is
useful when both types are very similar but technically
different.
Definition pickle_bij {X Y : countType} (x : X) (y : Y) :=
∃ i, (@pickle_inv X i = Some x) ∧ (@pickle_inv Y i = Some y).
∃ i, (@pickle_inv X i = Some x) ∧ (@pickle_inv Y i = Some y).