Library mathcomp.analysis.altreals.realsum

(* -------------------------------------------------------------------- 
 Copyright (c) - 2015--2016 - IMDEA Software Institute                
 Copyright (c) - 2015--2018 - Inria                                   
 Copyright (c) - 2016--2018 - Polytechnique                           *)

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.classical Require Import boolp.
Require Import xfinmap ereal reals discrete realseq.
From mathcomp.classical Require Import classical_sets functions mathcomp_extra.
Require Import topology.

Set Implicit Arguments.

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope fset_scope.
Local Open Scope ring_scope.

Section Summable.
Variables (T : choiceType) (R : realType) (f : T → R).

Definition summable := ∃ (M : R), ∀ (J : {fset T}),
  \sum_(x : J) `|f (val x)| ≤ M.

Lemma summableP : summable →
  { M | 0 ≤ M & ∀ (J : {fset T}), \sum_(x : J) `|f (val x)| ≤ M }.
End Summable.

Section Sum.
Context {R : realType} {T : choiceType}.

Implicit Types f g : T → R.

Definition fpos f := fun x ⇒ `|Num.max 0 (f x)|.
Definition fneg f := fun x ⇒ `|Num.min 0 (f x)|.

Lemma eq_fpos f g : f =1 g → fpos f =1 fpos g.

Lemma eq_fneg f g : f =1 g → fneg f =1 fneg g.

Lemma fpos0 x : fpos (fun _ : T ⇒ 0) x = 0 :> R.

Lemma fneg0 x : fneg (fun _ : T ⇒ 0) x = 0 :> R.

Lemma fnegN f : fneg (- f) =1 fpos f.

Lemma fposN f : fpos (- f) =1 fneg f.

Lemma fposZ f c : 0 ≤ c → fpos (c \*o f) =1 c \*o fpos f.

Lemma fnegZ f c : 0 ≤ c → fneg (c \*o f) =1 c \*o fneg f.

Lemma fpos_natrM f (n : T → nat) x :
  fpos (fun x ⇒ (n x)%:R × f x) x = (n x)%:R × fpos f x.

Lemma fneg_natrM f (n : T → nat) x :
  fneg (fun x ⇒ (n x)%:R × f x) x = (n x)%:R × fneg f x.

Lemma fneg_ge0 f x : (∀ x, 0 ≤ f x) → fneg f x = 0.

Lemma fpos_ge0 f x : (∀ x, 0 ≤ f x ) → fpos f x = f x.

Lemma ge0_fpos f x : 0 ≤ fpos f x.

Lemma ge0_fneg f x : 0 ≤ fneg f x.

Lemma le_fpos_norm f x : fpos f x ≤ `|f x|.

Lemma le_fpos f1 f2 : f1 <=1 f2 → fpos f1 <=1 fpos f2.

Lemma fposBfneg f x : fpos f x - fneg f x = f x.

Definition psum f : R :=
  (* We need some ticked `image` operator *)
  let S := [set x | ∃ J : {fset T}, x = \sum_(x : J) `|f (val x)| ]%classic in
  if `[<summable f>] then sup S else 0.

Definition sum f : R := psum (fpos f) - psum (fneg f).
End Sum.

Section SummableCountable.
Variable (T : choiceType) (R : realType) (f : T → R).

Lemma summable_countn0 : summable f → countable [pred x | f x != 0].
End SummableCountable.

Section PosCnv.
Context {R : realType}.

Lemma ncvg_mono (u : nat → R) :
    (* {mono u : x y / (x <= y)*)
    (∀ x y, (x ≤ y)%N → u x ≤ u y)
  → exists2 l, (-oo < l)%E & ncvg u l.

Lemma ncvg_mono_bnd (u : nat → R) :
    (* {mono u : x y / (x <= y)*)
    (∀ x y, (x ≤ y)%N → u x ≤ u y)
  → nbounded u → ∃ l, ncvg u l%:E.
End PosCnv.

Section SumTh.
Context {R : realType} (T : choiceType).

Implicit Type S : T → R.

Lemma summable_sup (S : T → R) : summable S → has_sup
  [set x | ∃ J : {fset T}, x = \sum_(j : J) `|S (val j)|]%classic.

Lemma psum_sup S : psum S =
  sup [set x | ∃ J : {fset T}, x = \sum_(x : J) `|S (val x)|]%classic.

Lemma psum_sup_seq S : psum S =
  sup [set x | exists2 J : seq T,
    uniq J & x = \sum_(x <- J) `|S x| ]%classic.

Lemma eq_summable (S1 S2 : T → R) :
  (S1 =1 S2) → summable S1 → summable S2.

Lemma eq_summableb (S1 S2 : T → R) :
  (S1 =1 S2) → `[< summable S2 >] = `[< summable S1 >].

Lemma eq_ppsum (F1 F2 : {fset T} → R) : F1 =1 F2 →
  (sup [set x | ∃ J, x = F1 J] = sup [set x | ∃ J, x = F2 J])%classic.

Lemma eq_psum (F1 F2 : T → R) : F1 =1 F2 → psum F1 = psum F2.

Lemma eq_sum (F1 F2 : T → R) : F1 =1 F2 → sum F1 = sum F2.

Lemma le_summable (F1 F2 : T → R) :
  (∀ x, 0 ≤ F1 x ≤ F2 x) → summable F2 → summable F1.

Lemma le_psum (F1 F2 : T → R) :
  (∀ x, 0 ≤ F1 x ≤ F2 x) → summable F2 → psum F1 ≤ psum F2.

Lemma psum_out S : ¬ summable S → psum S = 0.

Lemma psumE S : (∀ x, 0 ≤ S x) → summable S → psum S =
  sup [set x | ∃ J : {fset T}, x = \sum_(j : J) S (val j)]%classic.

Lemma psum_absE S : summable S → psum S =
  sup [set x | ∃ J : {fset T}, x = \sum_(j : J) `|S (val j)|]%classic.

Lemma summable_seqP S :
  summable S ↔ (exists2 M, 0 ≤ M &
    ∀ s : seq T, uniq s → \sum_(x <- s) `|S x| ≤ M).

Lemma gerfin_psum S (J : {fset T}) :
  summable S → \sum_(j : J) `|S (val j)| ≤ psum S.

Lemma gerfinseq_psum S (r : seq T) :
  uniq r → summable S → \sum_(j <- r) `|S j| ≤ psum S.

Lemma psum_le S z :
  (∀ J, uniq J → \sum_(j <- J) `|S j| ≤ z) → psum S ≤ z.

Lemma lt_psum (F : T → R) l :
  summable F → l < psum F →
    ∃ J : {fset T}, l < \sum_(j : J) `|F (val j)|.
End SumTh.

Lemma max_sup {R : realType} x (E : set R) :
  (E `&` ubound E)%classic x → sup E = x.

Section FinSumTh.
Context {R : realType} (I : finType).

Lemma summable_fin (f : I → R) : summable f.

Lemma psum_fin (f : I → R) : psum f = \sum_i `|f i|.
End FinSumTh.

Section PSumGe.
Context {R : realType} (T : choiceType).

Variable (S : T → R).

Lemma ger_big_psum r : uniq r → summable S →
  \sum_(x <- r) `|S x| ≤ psum S.

Lemma ger1_psum x : summable S → `|S x| ≤ psum S.

Lemma ge0_psum : 0 ≤ psum S.
End PSumGe.

Section PSumNatGe.
Context {R : realType}.

Variable (S : nat → R) (smS : summable S).

Lemma ger_big_ord_psum n : \sum_(i < n) `|S i| ≤ psum S.
End PSumNatGe.

Section PSumCnv.
Context {R : realType}.

Variable (S : nat → R).

Hypothesis ge0_S : (∀ n, 0 ≤ S n).
Hypothesis smS : summable S.

Lemma ptsum_homo x y : (x ≤ y)%N → (\sum_(i < x) S i ≤ \sum_(i < y) S i).

Lemma psummable_ptbounded : nbounded (fun n ⇒ \sum_(i < n) S i).

Lemma ncvg_sum : ncvg (fun n ⇒ \sum_(i < n) S i) (psum S)%:E.

Lemma sum_ncvg l :
  ncvg (fun n ⇒ \sum_(i < n) S i) l%:E → summable S.
End PSumCnv.

Section PSumAsLim.
Context {R : realType} {T : choiceType}.

Variable (S : T → R) (P : nat → {fset T}).

Hypothesis ge0_S : (∀ x, 0 ≤ S x).
Hypothesis smS : summable S.
Hypothesis homo_P : ∀ n m, (n ≤ m)%N → (P n `<=` P m).
Hypothesis cover_P : ∀ x, S x != 0 → ∃ n, x \in P n.

Lemma psum_as_lim : psum S = fine (nlim (fun n ⇒ \sum_(j : P n) (S (val j)))).
End PSumAsLim.

Section SummableAlg.
Context {R : realType} (T : choiceType) (I : Type).

Lemma summable_addrC (S1 S2 : T → R) :
  summable (S1 \+ S2) → summable (S2 \+ S1).

Lemma summable_mulrC (S1 S2 : T → R) :
  summable (S1 \* S2) → summable (S2 \* S1).

Lemma summable_abs (S : T → R) : summable \`|S| ↔ summable S.

Lemma summable0 : summable (fun _ : T ⇒ 0 : R).

Lemma summableD (S1 S2 : T → R) :
  summable S1 → summable S2 → summable (S1 \+ S2).

Lemma summableN (S : T → R) : summable S → summable (- S).

Lemma summablebN (S : T → R) :
  `[< summable (- S)>] = `[< summable S >].

Lemma summablebDl (S1 S2 : T → R) : summable S1 →
  `[< summable (S1 \+ S2) >] = `[< summable S2 >].

Lemma summablebDr (S1 S2 : T → R) : summable S2 →
  `[< summable (S1 \+ S2) >] = `[< summable S1 >].

Lemma summableZ (S : T → R) c : summable S → summable (c \*o S).

Lemma summableZr (S : T → R) (c : R) :
  summable S → summable (c \o× S).

Lemma summableMl (S1 S2 : T → R) :
  (∃ M, ∀ x, `|S1 x| ≤ M) → summable S2 → summable (S1 \* S2).

Lemma summableMr (S1 S2 : T → R) :
  (∃ M, ∀ x, `|S2 x| ≤ M) → summable S1 → summable (S1 \* S2).

Lemma summableM (S1 S2 : T → R) :
  summable S1 → summable S2 → summable (S1 \* S2).

Lemma summable_fpos (f : T → R) :
  summable f → summable (fpos f).

Lemma summable_fneg (f : T → R) :
  summable f → summable (fneg f).

Lemma summable_condl (S : T → R) (P : pred T) :
  summable S → summable (fun x ⇒ (P x)%:R × S x).

Lemma summable_condr (S : T → R) (P : pred T) :
  summable S → summable (fun x ⇒ S x × (P x)%:R).

Lemma summable_of_bd (S : T → R) (d : R) :
  (∀ J, uniq J → \sum_(x <- J) `|S x| ≤ d) →
    summable S ∧ psum S ≤ d.

Lemma summable_sum (F : I → T → R) (P : pred I) r :
    (∀ i, P i → summable (F i))
  → summable (fun x ⇒ \sum_(i <- r | P i) F i x).

End SummableAlg.

Section StdSum.
Context {R : realType} (T : choiceType) (I : Type).

Implicit Type S : T → R.

Lemma psum0 : psum (fun _ : T ⇒ 0) = 0 :> R.

Lemma psum_eq0 (f : T → R) : (∀ x, f x = 0) → psum f = 0.

Lemma eq0_psum (f : T → R) :
  summable f → psum f = 0 → (∀ x : T, f x = 0).

Lemma neq0_psum (f : T → R) : psum f ≠ 0 → ∃ x : T, f x ≠ 0.

Lemma psum_abs (S : T → R) : psum \`|S| = psum S.

Lemma eq_psum_abs (S1 S2 : T → R) :
  \`|S1| =1 \`|S2| → psum S1 = psum S2.

Lemma le_psum_abs (S1 S2 : T → R) :
  (∀ x, `|S1 x| ≤ `|S2 x|) → summable S2 → psum S1 ≤ psum S2.

Lemma le_psum_condl (S : T → R) (P : pred T) :
  summable S → psum (fun x ⇒ (P x)%:R × S x) ≤ psum S.

Lemma le_psum_condr (S : T → R) (P : pred T) :
  summable S → psum (fun x ⇒ S x × (P x)%:R) ≤ psum S.

Lemma psumN (S : T → R) : psum (- S) = psum S.

Lemma psumD S1 S2 :
    (∀ x, 0 ≤ S1 x) → (∀ x, 0 ≤ S2 x)
  → summable S1 → summable S2
  → psum (S1 \+ S2) = (psum S1 + psum S2).

Lemma __admitted__psumB S1 S2 :
    (∀ x, 0 ≤ S2 x ≤ S1 x) → summable S1
  → psum (S1 \- S2) = (psum S1 - psum S2).

Lemma psumZ S c : 0 ≤ c → psum (c \*o S) = c × psum S.

Lemma psumZr S c :
  0 ≤ c → psum (c \o× S) = psum S × c.

Lemma psum_bigop (F : I → T → R) P r :
    (∀ i x, 0 ≤ F i x) → (∀ i, summable (F i)) →
  \sum_(i <- r | P i) psum (F i) =
    psum (fun x ⇒ \sum_(i <- r | P i) F i x).

Lemma psumID S (P : pred T) :
  summable S → psum S =
    psum (fun x ⇒ (P x)%:R × S x) + psum (fun x ⇒ (~~P x)%:R × S x).

Lemma psum_finseq S (r : seq.seq T) :
    uniq r → {subset [pred x | S x != 0] ≤ r}
  → psum S = \sum_(x <- r) `|S x|.
End StdSum.

#[deprecated(since="mathcomp-analysis 0.6.2",
  note="lacks proof, use __admitted__psumB explicitly if you really want to")]
Notation psumB := __admitted__psumB.

Section PSumReindex.
Context {R : realType} {T U : choiceType}.
Context (S : T → R) (P : pred T) (h : U → T).

Lemma reindex_psum_onto h' :
     (∀ x, S x != 0 → x \in P)
  → (∀ i, i \in P → omap h (h' i) = Some i)
  → (∀ i, h i \in P → h' (h i) = Some i)
  → psum S = psum (fun x : U ⇒ S (h x)).

Lemma reindex_psum :
     (∀ x, S x != 0 → x \in P)
  → {on P, bijective h}
  → psum S = psum (fun x : U ⇒ S (h x)).
End PSumReindex.

Section PSumPartition.
Context {R : realType} {T U : choiceType} (f : T → U).

Let C y := `[< ∃ x : T, f x == y >].

Lemma partition_psum (S : T → R) : summable S →
  psum S = psum (fun y ⇒ psum (fun x ⇒ S x × (f x == y)%:R)).

Lemma partition_psum_cond (S : T → R) : summable S →
  psum S = psum (fun y ⇒ (C y)%:R × psum (fun x ⇒ S x × (f x == y)%:R)).
End PSumPartition.

Section PSumPair.
Context {R : realType} {T U : choiceType}.

Lemma psum_pair (S : T × U → R) : summable S →
  psum S = psum (fun x ⇒ psum (fun y ⇒ S (x, y))).

Lemma psum_pair_swap (S : T × U → R) : summable S →
  psum S = psum (fun y ⇒ psum (fun x ⇒ S (x, y))).
End PSumPair.

Section SupInterchange.
Context {R : realType} {T U : Type}.

Lemma __admitted__interchange_sup (S : T → U → R) :
    (∀ x, has_sup [set r | ∃ y, r = S x y])
  → has_sup [set r | ∃ x, r = sup [set r | ∃ y, r = S x y]]
→ sup [set r | ∃ x, r = sup [set r | ∃ y, r = S x y]]
= sup [set r | ∃ y, r == sup [set r | ∃ x, r = S x y]].
End SupInterchange.

#[deprecated(since="mathcomp-analysis 0.6.2",
  note="lacks proof, use __admitted__interchange_sup explicitly if you really want to use this lemma")]
Notation interchange_sup := __admitted__interchange_sup.

Section PSumInterchange.
Context {R : realType} {T U : choiceType}.

Lemma __admitted__interchange_psum (S : T → U → R) :
    (∀ x, summable (S x))
  → summable (fun x ⇒ psum (fun y ⇒ S x y))
  → psum (fun x ⇒ psum (fun y ⇒ S x y)) = psum (fun y ⇒ psum (fun x ⇒ S x y)).
End PSumInterchange.

#[deprecated(since="mathcomp-analysis 0.6.2",
  note="lacks proof, use __admitted__interchange_psum explicitly if you really want to use this lemma")]
Notation interchange_psum := __admitted__interchange_psum.

Section SumTheory.
Context {R : realType} {T : choiceType}.

Implicit Types (S : T → R).

Lemma psum_sum S : (∀ x, 0 ≤ S x) → psum S = sum S.

Lemma le_sum S1 S2 :
  summable S1 → summable S2 → (S1 <=1 S2) →
    sum S1 ≤ sum S2.

Lemma sum0 : sum (fun _ : T ⇒ 0) = 0 :> R.

Lemma sumN S : sum (- S) = - sum S.

Lemma sumZ S c : sum (c \*o S) = c × sum S.

Lemma sumID S (P : pred T) :
  summable S → sum S =
    sum (fun x ⇒ (P x)%:R × S x) + sum (fun x ⇒ (~~ P x)%:R × S x).

Lemma sum_finseq S (r : seq T) :
  uniq r → {subset [pred x | S x != 0] ≤ r} →
    sum S = \sum_(x <- r) S x.

Lemma sum_seq1 S x : (∀ y, S y != 0 → x == y) → sum S = S x.

End SumTheory.

Arguments sum_seq1 {R T} [S] x _.