Library probsa.util.bigop_inf

Require Export prosa.util.ssrlia.

From probsa.util Require Export notation boolp etime iota bigop indicator.

Lemma SeriesC_scal_l :
  ∀ {X : countType} (c : R) (f : X → R),
    ∑[∞]_{x <- X } c × f x = c × ∑[∞]_{x <- X } f x.
Proof.
  intros; erewrite Series_ext; last first.
  { by intros ?; rewrite countable_sum_scal_l. }
  by rewrite Series_scal_l.
Qed.

Lemma SeriesC_pos :
  ∀ {X : countType} (f : X → R),
    (∀ x, 0 ≤ f x ) →
    0 ≤ ∑[∞]_{i <-_} f i.
Proof.
  move ⇒ X f GE; apply Series_pos ⇒ n.
  by rewrite /countable_sum; destruct pickle_inv ⇒ //=; [apply Rle_ge | nra].
Qed.

Lemma is_seriesC_bump (A : countType) (x' : A) f :
  is_series (countable_sum (λ x , if x == x' then f x else 0)) (f x').
Proof.
  eapply is_series_ext; last apply (is_series_bump (pickle x')).
  intros n ⇒ //=.
  destruct (eq_nat_dec n (pickle x')) as [Heq|Hneq].
  - rewrite /countable_sum. subst. by rewrite pickleK_inv //= eq_refl.
  - rewrite /countable_sum//=. case_eq (@pickle_inv A n).
    × intros s Heq ⇒ //=. case: ifP.
      ** move /eqP; intros; subst. exfalso.
         apply Hneq. symmetry; apply pickle_inv_some_inv; eauto.
      ** done.
    × rewrite //=.
Qed.

Lemma SeriesCf_bump :
  ∀ (A : countType) (x' : A) (f : _), ∑[∞]_{x <-A }(if x == x' then f x else 0) = f x'.
Proof. by intros; apply is_series_unique, is_seriesC_bump. Qed.

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 ).

Using the pickle-equivalence, we can compare two infinite sums between two different count-types X and Y.

Theorem leq_SeriesC :
  ∀ {X Y : countType} (f : X → R) (g : Y → R),
    ex_series (countable_sum [eta f ]) →
    ex_series (countable_sum [eta g ]) →
    (∀ i, is_some (@pickle_inv X i) ↔ is_some (@pickle_inv Y i)) →
    (∀ x y, pickle_bij x y → f x ≤ g y ) →
    ∑[∞]_{x <- X } f x ≤ ∑[∞]_{y <- Y } g y.
Proof.
  intros × EXf EXg EQUI LE.
  apply Series_le'; (try done) ⇒ i; rewrite /countable_sum.
  case EQx: (@pickle_inv X i) ⇒ [ix|]; case EQy: (@pickle_inv Y i) ⇒ [iy|].
  - by eapply LE; ∃ i; eauto.
  - by specialize (EQUI i); rewrite EQx EQy in EQUI;
    case EQUI as [A B]; unfold is_some in A, B; exfalso; auto.
  - by specialize (EQUI i); rewrite EQx EQy in EQUI;
    case EQUI as [A B]; unfold is_some in A, B; exfalso; auto.
  - by apply Rge_refl.
Qed.