Series

\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.FormalSeries
\import Algebra.Ring.FormalSeries.Composition
\import Algebra.Semiring
\import Analysis.FuncLimit
\import Arith.Int
\import Arith.Nat
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\import Arith.Real.UpperReal
\import Data.Array
\import Data.Or
\import Equiv
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Analysis.Limit
\import Set.Fin
\import Set.Partial
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.MetricSpace
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.Real
\import Topology.NormedRing
\import Topology.TopAbGroup
\import Topology.TopAbGroup.Complete
\import Topology.TopAbGroup.Product
\import Topology.TopRing
\import Topology.TopSpace
\import Topology.TopSpace.Product
\open Monoid

\func Series (A : \Set) => Nat -> A

\sfunc partialSum {A : AddMonoid} (S : Series A) (n : Nat) : A
  => A.BigSum \new Array A n \lam j => S j
  \where {
    \lemma =FinSum {A : AbMonoid} {S : Series A} {n : Nat} : partialSum S n = A.FinSum \lam (j : Fin n) => S j
      => (\peval partialSum S n) *> inv A.FinSum=BigSum
  }

\lemma partialSum-empty {A : AddMonoid} {S : Series A} : partialSum S 0 = 0
  => \peval partialSum S 0

\lemma partialSum_1 {A : AddMonoid} {S : Series A} : partialSum S 1 = S 0
  => (\peval partialSum S 1) *> zro-right

\lemma partialSum_<= {A : PosetAddMonoid} {S T : Series A} {n : Nat} (p : \Pi (k : Nat) -> S k <= T k) : partialSum S n <= partialSum T n
  => transport2 (<=) (inv \peval partialSum S n) (inv \peval partialSum T n) (A.BigSum_<= \lam j => p j)

\lemma partialSum_hom {A B : AddMonoid} (f : AddMonoidHom A B) {S : Series A} {n : Nat} : f (partialSum S n) = partialSum (\lam i => f (S i)) n
  => pmap f (\peval partialSum S n) *> f.func-BigSum *> inv \peval partialSum _ n

\lemma partialSum_suc {A : AddMonoid} {S : Series A} {n : Nat} : partialSum S (suc n) = partialSum S n + S n
  => (\peval partialSum S (suc n)) *> A.BigSum_suc-nat {n} {S} *> pmap (+ _) (inv \peval partialSum S n)

-- | $\sum_{n<N} (-f_n) = -\sum_{n<N} f_n$.
\lemma partialSum_negative {A : AbGroup} {f : Series A} {N : Nat}
  : negative (partialSum f N) = partialSum (\lam n => negative (f n)) N  \elim N
  | 0 => pmap negative partialSum-empty *> A.negative_zro *> inv partialSum-empty
  | suc N => pmap negative partialSum_suc *> A.negative_+-comm *> pmap (+ _) partialSum_negative *> inv partialSum_suc

\func IsConvSeries {A : TopAbGroup} (S : Series A) : \Prop
  => IsConvergent (partialSum S)

\func IsSeriesSum {A : AddMonoid} {T : TopSpace A} (S : Series A) (l : A) : \Prop
  => T.IsLimit (partialSum S) l

\lemma seriesSum-fin {A : AddMonoid} {T : TopSpace A} {S : Series A} (n : Nat) (p : \Pi {j : Nat} -> n <= j -> S j = 0)
  : IsSeriesSum S (A.BigSum \new Array A n \lam j => S j)
  => \lam {U} Uo US => inP (n, \lam {k} n<=k => transport U (A.BigSum-subset n<=k (\lam j => pmap S $ inv toFin=id) (\lam j => p) *> inv (\peval partialSum S k)) US)

\lemma seriesSum-conv {A : TopAbGroup} {S : Series A} {l : A} (Sl : IsSeriesSum S l) : IsConvSeries S
  => limit-conv Sl

\func seriesSum {A : CompleteTopAbGroup} (S : Series A) : Partial A
  => limit (partialSum S)

\lemma seriesConv-sum {A : CompleteTopAbGroup} {S : Series A} (Sc : IsConvSeries S) : IsSeriesSum S (seriesSum S Sc)
  => limit-isLimit

\lemma seriesSum-char {A : CompleteTopAbGroup} {S : Series A} {l : A} : (seriesSum S = defined l) <-> IsSeriesSum S l
  => limit-char

-- | Series sums add: $\sum f = a$ and $\sum g = b$ give $\sum (f + g) = a + b$.
\lemma IsSeriesSum_+ {A : TopAbGroup} {f g : Series A} {a b : A} (fa : IsSeriesSum f a) (gb : IsSeriesSum g b)
  : IsSeriesSum (\lam n => f n + g n) (a + b)
  => transport (A.IsLimit __ (a + b))
    (path (\lam i N => inv (partialSum_+ {A} {f} {g} {N}) @ i))
    (cont2-limit fa gb +-cont)

-- | Negation commutes with series sum: $\sum f = a$ gives $\sum (-f) = -a$.
\lemma IsSeriesSum_negative {A : TopAbGroup} {f : Series A} {a : A} (fa : IsSeriesSum f a)
  : IsSeriesSum (\lam n => A.negative (f n)) (A.negative a)
  => transport (A.IsLimit __ (A.negative a))
    (path \lam i N => partialSum_negative {A} {f} {N} i)
    (cont-limit fa negative-cont)

-- | Series subtract: $\sum f = a$ and $\sum g = b$ give $\sum (f - g) = a - b$.
\lemma IsSeriesSum_- {A : TopAbGroup} {f g : Series A} {a b : A} (fa : IsSeriesSum f a) (gb : IsSeriesSum g b)
  : IsSeriesSum (\lam n => f n - g n) (a - b)
  => IsSeriesSum_+ fa (IsSeriesSum_negative gb)

\func midSum {A : AddMonoid} (S : Series A) (n m : Nat) : A \elim n, m
  | 0, m => partialSum S m
  | suc n, 0 => 0
  | suc n, suc m => midSum (\lam j => S (suc j)) n m
  \where {
    \lemma MidFinSet (n m : Nat) : FinSet (\Sigma (k : Nat) (n <= k) (k < m)) (m -' n) \cowith
      | finEq => inP \new QEquiv {
        | f i => (i + n, <=_+ zero<=_ <=-refl, NatSemiring.<_+-left n (fin_< i) <∘l =_<= (+-comm *> <=_exists (<=-less $ -'_< $ zero<=_ <∘r fin_< i)))
        | ret s => toFin (s.1 -' n) $ -'_<-monotone-left s.3 (s.2 <∘r s.3)
        | ret_f i => fin_nat-inj $ toFin=id *> -'+
        | f_sec s => ext $ pmap (+ n) toFin=id *> +-comm *> <=_exists s.2
      }

    \protected \lemma =FinSum {A : AbMonoid} {S : Series A} {n m : Nat}
      : midSum S n m = A.FinSum {MidFinSet n m} (\lam k => S k.1) \elim n, m
      | 0, m => partialSum.=FinSum *> A.FinSum_Equiv2 (later \new QEquiv {
        | f j => (j, zero<=_, fin_< j)
        | ret s => toFin s.1 s.3
        | ret_f j => fin_nat-inj toFin=id
        | f_sec s => ext toFin=id
      }) \lam j => idp
      | suc n, 0 => inv $ A.FinSum_zro $ later \lam s => \case s.2 <∘r s.3
      | suc n, suc m => =FinSum *> A.FinSum_Equiv2 (later \new QEquiv {
        | f s => (suc s.1, suc<=suc s.2, NatOrder.suc<suc s.3)
        | ret s => (s.1 -' 1, transport (<= _) -'0 $ -'-monotone-left s.2, transport (_ <) -'0 $ -'_<-monotone-left s.3 $ suc<=suc zero<=_ <∘r s.2 <∘r s.3)
        | ret_f s => ext -'0
        | f_sec s => ext $ <=_exists {1} $ suc<=suc zero<=_ <=∘ s.2
      }) \lam s => idp
  }

\lemma midSum_hom {A B : AddMonoid} (f : AddMonoidHom A B) {S : Series A} {n m : Nat} : f (midSum S n m) = midSum (\lam i => f (S i)) n m \elim n, m
  | 0, m => partialSum_hom f
  | suc n, 0 => f.func-zro
  | suc n, suc m => midSum_hom f

\func IsConvUpperSeries (S : Series ExUpperReal) : \Prop
  => ∀ {eps : Rat} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> (midSum S N n).U eps)

\func IsAbsConvSeries {A : ExPseudoNormedAbGroup} (S : Series A) : \Prop
  => IsConvUpperSeries \lam j => norm (S j)

\func midSum' {A : AddMonoid} (S : Series A) (n m : Nat) : A
  => partialSum (\lam k => S (n + k)) m

\lemma midSum'_midSum {A : AddMonoid} {S : Series A} {n m : Nat} : midSum' S n m = midSum S n (n + m) \elim n
  | 0 => idp
  | suc n => midSum'_midSum

\lemma midSum_midSum' {A : AddMonoid} {S : Series A} {n m : Nat} : midSum S n m = midSum' S n (m -' n) \elim n, m
  | 0, 0 => idp
  | 0, suc m => idp
  | suc n, 0 => inv partialSum-empty
  | suc n, suc m => midSum_midSum'

\lemma zeroSeries-sum {A : TopAbGroup} : IsSeriesSum (\lam _ => A.zro) 0
  => \lam {U} _ U0 => inP (0, \lam _ => rewrite (\peval partialSum _ _) $ transportInv U A.BigSum_replicate0 U0)

\lemma series-shift-conv {A : TopAbGroup} {S : Series A} : IsConvSeries S <-> IsConvSeries \lam n => S (suc n)
  => (\lam Sc => convergent-topAbGroup-char 2 0 \lam {U} Uo U0 => \case convergent-topAbGroup-char 0 1 Sc Uo U0 \with {
    | inP (N,g) => inP (N, \lam p => transport U (inv (midSum-diff $ suc<=suc p) *> midSum-diff p) $ g id<=suc $ suc<=suc p)
  }, \lam Sc => convergent-topAbGroup-char 2 0 \lam {U} Uo U0 => \case convergent-topAbGroup-char 0 1 Sc Uo U0 \with {
    | inP (N, g) => inP (suc N, \lam {n} => \case \elim n \with {
      | 0 => \lam p => absurd $ p NatOrder.zero<suc
      | suc n => \lam p => transport U (inv (midSum-diff $ suc<=suc.conv p) *> midSum-diff p) $ g <=-refl (suc<=suc.conv p)
    })
  })

\lemma upperSeries-shift-conv {S : Series ExUpperReal} (S>=0 : \Pi (j : Nat) -> 0 <= S j) : IsConvUpperSeries S <-> IsConvUpperSeries \lam n => S (suc n)
  => (\lam c eps>0 => \case c eps>0 \with {
    | inP (M,h) => inP (M, \lam M<=n => midSum_<=-left id<=suc S>=0 $ h (M<=n <=∘ id<=suc))
  }, unshift)
  \where {
    \lemma unshift (c : IsConvUpperSeries \lam n => S (suc n)) : IsConvUpperSeries S
      => \lam eps>0 => \case c eps>0 \with {
        | inP (M,h) => inP (suc M, \lam {n} => \case \elim n \with {
          | 0 => \lam p => absurd linarith
          | suc n => \lam p => h (suc<=suc.conv p)
        })
      }
  }

\lemma upperSeries-shifts-conv {S : Series ExUpperReal} (S>=0 : \Pi (j : Nat) -> 0 <= S j) (N : Nat) : IsConvUpperSeries S <-> IsConvUpperSeries \lam n => S (n + N) \elim N
  | 0 => <->refl
  | suc N => <->trans (upperSeries-shifts-conv S>=0 N) $ upperSeries-shift-conv \lam j => S>=0 (j + N)

\lemma series-shift-absConv {A : ExPseudoNormedAbGroup} {S : Series A} : IsAbsConvSeries S <-> IsAbsConvSeries \lam n => S (suc n)
  => upperSeries-shift-conv \lam j => norm>=0

\lemma series-shifts-absConv {A : ExPseudoNormedAbGroup} {S : Series A} (N : Nat) : IsAbsConvSeries S <-> IsAbsConvSeries \lam n => S (n + N)
  => upperSeries-shifts-conv (\lam j => norm>=0) N

\lemma midSum_suc {A : AddMonoid} {S : Series A} {n : Nat} : midSum S n (suc n) = S n \elim n
  | 0 => (\peval partialSum _ _) *> zro-right
  | suc n => midSum_suc

\lemma midSum-diff {A : AbGroup} {S : Series A} {n m : Nat} (p : n <= m) : midSum S n m = partialSum S m - partialSum S n \elim n, m
  | 0, m => inv $ rewrite (\peval partialSum S _, \peval partialSum S _) $ pmap (_ +) A.negative_zro *> zro-right
  | suc n, 0 => absurd $ p NatOrder.zero<suc
  | suc n, suc m => midSum-diff (suc<=suc.conv p) *> rewrite (\peval partialSum S _, \peval partialSum S _, \peval partialSum _ _, \peval partialSum _ _) (inv A.sum-cancel-left)

\lemma partialSum-split-shifted {A : AddMonoid} {S : Series A} {n q : Nat}
  : partialSum S (n + q) = partialSum S n + partialSum (\lam k => S (n + k)) q \elim q
  | 0 => inv zro-right *> pmap (_ +) (inv partialSum-empty)
  | suc q => partialSum_suc *> pmap (+ _) partialSum-split-shifted *> +-assoc *> pmap (_ +) (inv partialSum_suc)

\lemma partialSum-split {A : AddMonoid} {S : Series A} {n m : Nat} (p : n <= m)
  : partialSum S m = partialSum S n + midSum S n m
  => rewriteI (<=_exists p) $ partialSum-split-shifted *> pmap (partialSum S n +) midSum'_midSum

\lemma midSum_norm {A : ExPseudoNormedAbGroup} {S : Series A} {n m : Nat} : norm (midSum S n m) <= midSum (\lam j => norm (S j)) n m \elim n, m
  | 0, m => rewrite (\peval partialSum _ _, \peval partialSum _ _) A.norm_BigSum
  | suc n, 0 => A.norm_BigSum {nil}
  | suc n, suc m => midSum_norm

\lemma midSum_<=-ldistr {x : ExUpperReal} {b : Series ExUpperReal} (b>=0 : \Pi (j : Nat) -> 0 <= b j) {n m : Nat}
  : midSum (\lam j => x * b j) n m <= x * midSum b n m \elim n, m
  | 0, m => rewrite (\peval partialSum _ _, \peval partialSum _ _) $ BigSum_<=-ldistr \lam j => b>=0 j
  | suc n, 0 => ExUpperRealSemigroup.*_>=0
  | suc n, suc m => midSum_<=-ldistr \lam j => b>=0 (suc j)
  \where {
    \lemma BigSum_<=-ldistr {x : ExUpperReal} {l : Array ExUpperReal} (l>=0 : \Pi (j : Fin l.len) -> 0 <= l j) : AddMonoid.BigSum (\lam j => x * l j) <= x * AddMonoid.BigSum l \elim l
      | nil => ExUpperRealSemigroup.*_>=0
      | a :: l => transportInv (_ <=) (ExUpperRealSemigroup.ldistr (l>=0 0) $ ExUpperRealAbMonoid.BigSum_>=0 \lam j => l>=0 (suc j)) $ <=_+ <=-refl $ BigSum_<=-ldistr \lam j => l>=0 (suc j)
  }

\lemma midSum-split {A : AddMonoid} {b : Series A} {n m k : Nat} (p : n <= m) (q : m <= k) : midSum b n k = midSum b n m + midSum b m k \elim n, m, k
  | 0, 0, k => rewrite (\peval partialSum _ _, \peval partialSum _ _) (inv zro-left)
  | _, suc m, 0 => absurd (q NatOrder.zero<suc)
  | 0, suc m, suc k => (\peval partialSum _ _) *> pmap (_ +) (inv \peval partialSum (\lam j => b (suc j)) _) *> pmap (_ +) (midSum-split zero<=_ $ suc<=suc.conv q) *> pmap (_ + (__ + _)) (\peval partialSum (\lam j => b (suc j)) _) *> inv +-assoc *> pmap (+ _) (inv \peval partialSum _ _)
  | suc n, 0, _ => absurd (p NatOrder.zero<suc)
  | suc n, suc m, suc k => midSum-split (suc<=suc.conv p) (suc<=suc.conv q)

\lemma midSum-degenerate {A : AddMonoid} {b : Series A} {n m : Nat} (m<n : m < n) : midSum b n m = 0 \elim n, m, m<n
  | suc n, 0, NatOrder.zero<suc => idp
  | suc n, suc m, NatOrder.suc<suc m<n => midSum-degenerate m<n

\lemma midSum_<=-left {A : PosetAddMonoid} {b : Series A} {n m k : Nat} (p : n <= m) (s : \Pi (j : Nat) -> 0 <= b j) : midSum b m k <= midSum b n k
  => \case LinearOrder.dec<_<= k m \with {
    | inl k<m => transportInv (<= _) (midSum-degenerate k<m) (midSum>=0 s)
    | inr m<=k => transport2 (<=) zro-left (inv $ midSum-split p m<=k) $ <=_+ (midSum>=0 s) <=-refl
  }

\lemma midSum_<= {A : PosetAddMonoid} {b c : Series A} {n m : Nat} (s : \Pi {j : Nat} -> n <= j -> j < m -> b j <= c j) : midSum b n m <= midSum c n m \elim n, m
  | 0, m => rewrite (\peval partialSum _ _, \peval partialSum _ _) $ A.BigSum_<= \lam j => s zero<=_ (fin_< j)
  | suc n, 0 => <=-refl
  | suc n, suc m => midSum_<= \lam p q => s (suc<=suc p) (NatOrder.suc<suc q)

\lemma midSum_0 {A : AddMonoid} {n m : Nat} : midSum (\lam _ => A.zro) n m = 0 \elim n, m
  | 0, m => (\peval partialSum _ _) *> A.BigSum_replicate0
  | suc n, 0 => idp
  | suc n, suc m => midSum_0

\lemma midSum>=0 {A : PosetAddMonoid} {b : Series A} {n m : Nat} (s : \Pi (j : Nat) -> 0 <= b j) : 0 <= midSum b n m
  => transport (<= _) midSum_0 (midSum_<= \lam _ _ => s _)

\lemma series-conv {A : ExPseudoNormedAbGroup} {S : Series A}
  : IsConvSeries S <-> ∀ {eps : Rat} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> (norm (midSum S N n)).U eps)
  => (\lam p eps>0 => \case convergent-metric-char.1 p eps>0 \with {
    | inP (N,g) => inP (N, \lam q => rewrite (midSum-diff q) $ rewriteI A.norm-dist $ g q)
  }, \lam p => convergent-metric-char.2 \lam eps>0 => \case p eps>0 \with {
    | inP (N,g) => inP (N, \lam q => rewrite (norm-dist, inv (midSum-diff q)) (g q))
  })

\lemma series-conv-real {A : PseudoNormedAbGroup} {S : Series A}
  : IsConvSeries S <-> ∀ {eps : Real} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> A.norm (midSum S N n) < eps)
  => <->trans series-conv $ later (\lam sc eps>0 => \case real_<-rat-char.1 eps>0 \with {
    | inP (eps',eps'>0,eps'<eps) => \case sc eps'>0 \with {
      | inP (N,h) => inP (N, \lam p => real_<_U.2 (h p) <∘ real_<_L.2 eps'<eps)
    }
  }, \lam sc eps>0 => \case sc (rat_real_<.1 eps>0) \with {
    | inP (N,h) => inP (N, \lam p => real_<_U.1 $ h p)
  })

\lemma seriesSum_defined {A : ExPseudoNormedAbGroup} {S : Series A} {a : A}
                         (p : ∀ {eps : Rat} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> (norm (a - partialSum S n)).U eps))
  : IsSeriesSum S a
  => \lam Uo Ua => \case dist_open.1 Uo Ua \with {
    | inP (eps,eps>0,h) => \case p eps>0 \with {
      | inP (N,g) => inP (N, \lam q => h $ rewriteI A.norm-dist in g q)
    }
  }
  \where {
    \lemma conv (p : IsSeriesSum S a)
      : ∀ {eps : Rat} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> (norm (a - partialSum S n)).U eps)
      => \lam {eps} eps>0 => \case limit-metric-char.1 p eps>0 \with {
        | inP (N,g) => inP (N, \lam N<=n => (unfolds, rewrite norm-dist) in g N<=n)
      }
  }

\lemma absConv-isConv {A : ExPseudoNormedAbGroup} {S : Series A} (Sc : IsAbsConvSeries S) : IsConvSeries S
  => series-conv.2 \lam eps>0 => \case Sc eps>0 \with {
    | inP (N,g) => inP (N, \lam p => midSum_norm (g p))
  }

\lemma series-limit {A : TopAbGroup} {S : Series A} (Sc : IsConvSeries S) : A.IsLimit S 0
  => \lam {U} Uo U0 => \case convergent-topAbGroup-char 0 1 Sc Uo U0 \with {
    | inP (N,g) => inP (N, \lam {n} p => transport U (inv (midSum-diff {_} {S} id<=suc) *> midSum_suc) (g p id<=suc))
  }

\lemma real-series_<= {b c : Series Real} (b>=0 : \Pi (j : Nat) -> 0 <= b j) (s : \Pi (j : Nat) -> b j <= c j) (cc : IsConvSeries c) : IsConvSeries b
  => series-conv-real.2 \lam eps>0 => \case series-conv-real.1 cc eps>0 \with {
    | inP (N,g) => inP (N, \lam p => transport2 (<=)
        (inv $ RealField.abs-ofPos $ midSum>=0 b>=0)
        (inv $ RealField.abs-ofPos $ midSum>=0 \lam j => b>=0 j <=∘ s j)
        (midSum_<= \lam {j} _ _ => s j) <∘r g p)
  }

\lemma series_<= {b c : Series ExUpperReal} (s : \Pi (j : Nat) -> b j <= c j) (cc : IsConvUpperSeries c) : IsConvUpperSeries b
  => \lam eps>0 => \case cc eps>0 \with {
    | inP (N,h) => inP (N, \lam p => midSum_<= {ExUpperRealAbMonoid} (\lam _ _ => s _) (h p))
  }

\func IsBoundedUpperSeries (S : Series ExUpperReal) : \Prop
  => ∃ (B : Rat) ∀ n ((S n).U B)
  \where {
    \lemma shifted {N : Nat} (SN : \Pi {n : Nat} -> n < N -> ∃ (S n).U) {B : Rat} (SB : \Pi {n : Nat} -> N <= n -> (S n).U B) : IsBoundedUpperSeries S
      => \case FinSet.finiteAC (\lam j => SN (fin_< j)) \with {
        | inP h => inP (Big (∨) B \lam j => (h j).1, \lam n => \case LinearOrder.dec<_<= n N \with {
          | inl n<N => transport (\lam x => ExUpperReal.U {S x} _) toFin=id $ ExUpperReal.U_<= (h (toFin n n<N)).2 $ RatField.Big_<=_join1 (toFin n n<N)
          | inr N<=n => ExUpperReal.U_<= (SB N<=n) RatField.Big_<=_join0
        })
      }
  }

\lemma convUpper-bounded {S : Series ExUpperReal} (S>=0 : \Pi (n : Nat) -> 0 <= S n) (Sb : \Pi (n : Nat) -> (S n).IsBounded) (Sc : IsConvUpperSeries S)
  : IsBoundedUpperSeries S
  => \case Sc RatField.zro<ide \with {
    | inP (N0, g) => IsBoundedUpperSeries.shifted (\lam {n} _ => Sb n)
      \lam {n} N0<=n => transport (<= _) midSum_suc (midSum_<=-left N0<=n S>=0) $ g (N0<=n <=∘ id<=suc)
  }

\lemma upperSeries-bounded_<= {a b : Series ExUpperReal} (a<=b : \Pi (n : Nat) -> a n <= b n) (bB : IsBoundedUpperSeries b) : IsBoundedUpperSeries a \elim bB
  | inP (B,bB) => inP (B, \lam n => a<=b n (bB n))

\func IsBoundedSeries {A : ExPseudoNormedAbGroup} (S : Series A) : \Prop
  => IsBoundedUpperSeries \lam n => norm (S n)

\lemma series-lim-bound {A : BoundedExPseudoNormedAbGroup} {b : Series A} {l : A} (bl : A.IsLimit b l) : IsBoundedSeries b
  => \case limit-metric-char.1 bl idp, norm-bounded l \with {
    | inP (N,h), inP (B,l<B) => IsBoundedUpperSeries.shifted (\lam _ => norm-bounded _) \lam {j} N<=j =>
      \have t => transport (norm __ <= _) (+-assoc *> pmap (_ +) negative-left *> zro-right) $ A.norm_+ {b j - l} {l}
      \in t $ ExUpperReal.+_U_<=.2 $ inP (1, rewriteI (norm_-, A.norm-dist) (h N<=j), B, l<B, <=-refl)
  }

\lemma series_*-bounded {b c : Series ExUpperReal} (c>=0 : \Pi (j : Nat) -> 0 <= c j) (bB : IsBoundedUpperSeries b) (cc : IsConvUpperSeries c) : IsConvUpperSeries \lam n => b n * c n \elim bB
  | inP (B, bB) =>
    \let | B1 => B ∨ 1
         | B1>0 : 0 < B1 => RatField.zro<ide <∘l join-right
    \in \lam {eps} eps>0 => \case cc {RatField.finv B1 * eps} $ RatField.<_*_positive_positive (RatField.finv>0 $ RatField.zro<ide <∘l join-right) eps>0 \with {
      | inP (N,h) => inP (N, \lam {n} N<=n =>
        \have t : midSum (\lam k => b k * c k) N n <= B1 ExUpperReal.* midSum c N n
                => midSum_<= (\lam {j} jp _ => ExUpperRealSemigroup.<=_* (ExUpperReal.<_<= $ ExUpperReal.U_<= (bB j) join-left) <=-refl) <=∘ midSum_<=-ldistr c>=0
        \in t $ transport ExUpperReal.U (inv *-assoc *> pmap (* eps) (RatField.finv-right $ RatField.>_/= B1>0) *> ide-left) $ later $ ExUpperRealSemigroup.<_*_U-right B1>0 (RatField.<_*_positive_positive (RatField.finv>0 B1>0) eps>0) (h N<=n))
    }

\lemma upperSeries-ldistr {c : Series ExUpperReal} (c>=0 : \Pi (n : Nat) -> 0 <= c n) (cc : IsConvUpperSeries c) {a : ExUpperReal} (ab : a.IsBounded)
  : IsConvUpperSeries (\lam n => a * c n)
  => series_*-bounded c>=0 (TruncP.map ab \lam (q,a<q) => (q, \lam _ => a<q)) cc

\lemma upperSeries-rdistr {c : Series ExUpperReal} (c>=0 : \Pi (n : Nat) -> 0 <= c n) (cc : IsConvUpperSeries c) {a : ExUpperReal} (ab : a.IsBounded)
  : IsConvUpperSeries (\lam n => c n * a)
  => transport IsConvUpperSeries (ext \lam n => *-comm) (upperSeries-ldistr c>=0 cc ab)

\lemma geometric-upper-series-conv {r : ExUpperReal} (r>=0 : 0 <= r) (r<1 : r.U 1) : IsConvUpperSeries (ExUpperRealSemigroup.pow r)
  => \case U-rounded r<1 \with {
    | inP (q,r<q,q<1) => series_<= {_} {pow q __} (\lam j => transport (_ <=) (ExUpperRealSemigroup.rat-pow $ <=-less $ r>=0 r<q) $ ExUpperRealSemigroup.pow_<= (ExUpperReal.<_<= r<q)) \lam {eps} eps>0 =>
      \have B => rat_<1_pow-bound q<1 {eps * (1 - q)} $ RatField.<_*_positive_positive eps>0 linarith
      \in inP (B.1, \lam {n} B<=n => rewrite midSum_midSum' $ ExUpperRealAbMonoid.<-rat.1 $ transport {Series ExUpperReal} (partialSum __ _ < eps) {\lam k => pow q B.1 * pow q k} (later $ ext \lam k => pmap ExUpperReal.fromRat $ inv pow_+) $
            transport (ExUpperRealAbMonoid.< _) (partialSum_hom rat-upperReal) $ ExUpperRealAbMonoid.<-rat.2 $ transportInv (< _) (\peval partialSum _ _) $ later $ transport (< _) (RatField.BigSum-ldistr {pow q B.1} {\new Array Rat (n -' B.1) (pow q __)}) $
            RatField.<=_*_positive-left (<=-less B.2) (RatField.BigSum_>=0 \lam j => RatField.pow>=0 $ <=-less $ r>=0 r<q) <∘r transport2 (<) (inv *-assoc) ide-right (RatField.<_*_positive-right eps>0 $ transportInv (< _) RatField.geometric-partial-sum $ linarith $ RatField.pow>0 $ r>=0 r<q))
  }

\lemma geometric-series-absConv {X : ExPseudoNormedRing} {x : X} (|x|<1 : (norm x).U 1) : IsAbsConvSeries (pow x)
  => series_<= (\lam j => X.norm_<=_pow) $ geometric-upper-series-conv norm>=0 |x|<1

\lemma upper-ratio-test {S : Series ExUpperReal} (S>=0 : \Pi (n : Nat) -> 0 <= S n) (S0b : (S 0).IsBounded)
                        (b : Series Real) (bp : \Pi (n : Nat) -> S (suc n) <= S n * b n)
                        {l : Real} (l<1 : l < 1) (bl : RealNormed.IsLimit b l) : IsConvUpperSeries S
  => \case real_<-char.1 (<_join-univ l<1 RealAbGroup.zro<ide) \with {
    | inP (r,lz<r,r<1) => \case (real_<-rat-char {0} {(r : Real) - l}).1 $ linarith $ usingOnly (join-left <∘r lz<r) \with {
      | inP (q,q>0,q<r-l) => \case bl (OBall-open {_} {q} {l}) $ rewrite RealNormed.dist-refl q>0 \with {
        | inP (N,g) => (upperSeries-shifts-conv S>=0 N).2
          \have r>=0 => join-right <=∘ <=-less lz<r
          \in series_<= (iter-bound (\lam j => S>=0 (j + N)) r>=0 (\lam j => bp (j + N)) (\lam j => linarith (RealAbGroup.abs>=_- <=∘ <=-less (real_<_U.2 $ g $ <=_+ zero<=_ <=-refl), real_<_L.2 q<r-l))) $
          series_*-bounded (\lam j => Real.<=-upper.1 $ RealField.pow>=0 r>=0) (TruncP.map (S-bounded N) \lam (B,p) => (B, \lam _ => p)) $ transport IsConvUpperSeries (path \lam i n => inv (RealField.pow-upper r>=0 {n}) i) $ geometric-upper-series-conv (ExUpperReal.<=-rat.1 $ rat_real_<=.2 r>=0) (rat_real_<.2 r<1)
      }
    }
  }
  \where {
    \lemma iter-bound {f : Series ExUpperReal} {b : Series Real} (f>=0 : \Pi (j : Nat) -> 0 <= f j) {r : Real} (r>=0 : 0 <= r)
                      (bp : \Pi (n : Nat) -> f (suc n) <= f n * b n) (bb : \Pi (n : Nat) -> b n <= r) (j : Nat) : f j <= f 0 * pow r j \elim j
      | 0 => transportInv (_ <=) (ExUpperRealSemigroup.ide-right $ f>=0 0) <=-refl
      | suc j => bp j <=∘ ExUpperRealSemigroup.<=_* <=-refl (Real.<=-upper.1 $ bb j) <=∘ transport (_ <=) (*-assoc *> inv (pmap (_ *) (RealField.*-upper (RealField.pow>=0 r>=0) r>=0))) (ExUpperRealSemigroup.<=_* (iter-bound f>=0 r>=0 bp bb j) <=-refl)

    \private \lemma S-bounded (n : Nat) : ∃ (B : Rat) ((S n).U B) \elim n
      | 0 => S0b
      | suc n => \case S-bounded n, (b n).U-inh \with {
        | inP (B,Sn<B), inP (C,bn<C) => inP (B * (C ∨ 0) + 1, ExUpperRealAbMonoid.<-rat.1 $ bp n <∘r ExUpperRealSemigroup.<=_* (ExUpperReal.<_<= Sn<B) (ExUpperReal.<_<= bn<C <=∘ ExUpperReal.<=-rat.1 join-left) <∘r transportInv (ExUpperRealAbMonoid.< _) (ExUpperReal.*-rat (<=-less $ S>=0 n Sn<B) join-right) (ExUpperRealAbMonoid.<-rat.2 linarith))
      }
  }

\lemma ratio-test {X : BoundedExPseudoNormedAbGroup} {S : Series X} (b : Series Real) (bp : \Pi (n : Nat) -> norm (S (suc n)) <= norm (S n) * b n)
                  {l : Real} (l<1 : l < 1) (bl : RealNormed.IsLimit b l) : IsAbsConvSeries S
  => upper-ratio-test (\lam j => norm>=0) (norm-bounded (S 0)) b bp l<1 bl

\lemma MTest {X : \Set} {Y : ExPseudoNormedAbGroup} (f : Nat -> X -> Y) (M : Series ExUpperReal)
             (Mp : \Pi (n : Nat) (x : X) -> norm (f n x) <= M n) (Mc : IsConvUpperSeries M) : IsUniFuncConvergent \lam n x => partialSum (f __ x) n
  => metric-uni-funcConvergent.2 \lam eps>0 => \case Mc eps>0 \with {
    | inP (N,g) => inP (N, \lam x {n} N<=n => rewrite (dist-symm, norm-dist, norm_-, inv $ midSum-diff {Y} {f __ x} N<=n) $ midSum_norm $ midSum_<= (\lam {j} _ _ => Mp j x) $ g N<=n)
  }

\lemma geometric-series-ratio {S : Series ExUpperReal} (S>=0 : \Pi (n : Nat) -> 0 <= S n) (S0b : (S 0).IsBounded)
                              {eps : Real} (eps>=0 : 0 <= eps)
                              (b : Series Real) (b>=0 : \Pi (n : Nat) -> 0 <= b n) (bp : \Pi (n : Nat) -> S (suc n) <= S n * b n)
                              {l : Real} (l<1 : l * eps < 1) (bl : RealNormed.IsLimit b l)
  : IsConvUpperSeries (\lam n => S n * ExUpperRealSemigroup.pow eps n)
  => upper-ratio-test (\lam n => ExUpperRealSemigroup.*_>=0) (ExUpperReal.*-bounded S0b ExUpperReal.fromRat-bounded) (\lam n => b n * eps)
      (\lam n => later $ rewrite (RealField.*-upper (b>=0 n) eps>=0) (ExUpperRealSemigroup.<=_* (bp n) <=-refl <=∘ =_<= equation.cSemigroup))
      l<1 (cont2-limit bl const-limit *-locally-uniform)

\lemma partialSum-cover {X : CoverSpace} {Y : TopAbGroup} (f : Nat -> CoverMap X Y) (n : Nat) : CoverMap X Y \lam x => partialSum (f __ x) n
  => transportInv (CoverMap X Y) (ext \lam x => \peval partialSum _ _) $ BigSum-cover \lam (j : Fin n) => f j

{- | Monotonicity of $\mathrm{partialSum}$ for non-negative {ExUpperReal}
     series: $n \leq m \implies \mathrm{partialSum}\,S\,n \leq
     \mathrm{partialSum}\,S\,m$. -}
\lemma partialSum-monotone {S : Series ExUpperReal} (S>=0 : \Pi (n : Nat) -> 0 <= S n) {n m : Nat} (p : n <= m)
  : partialSum S n <= partialSum S m
  => transport2 (<=) zro-right (inv (partialSum-split p)) $ <=_+ <=-refl (midSum>=0 S>=0)

-- | {partialSum} distributes over pointwise addition.
\lemma partialSum_+ {A : AbMonoid} {f g : Series A} {N : Nat}
  : partialSum (\lam n => f n + g n) N = partialSum f N + partialSum g N
  => (\peval partialSum (\lam n => f n + g n) N)
     *> AbMonoid.BigSum_+
     *> pmap2 (+) (inv (\peval partialSum f N)) (inv (\peval partialSum g N))

-- | Finite majorant principle: $\|\sum_{k < N} S_k\| \leq \sum_{k < N} \|S_k\|$.
\lemma partialSum_norm_<= {A : ExPseudoNormedAbGroup} {S : Series A} {N : Nat}
  : norm (partialSum S N) ExUpperRealAbMonoid.<= partialSum (\lam k => A.norm (S k)) N \elim N
  | 0 => transport2 (<=) (inv (pmap A.norm partialSum-empty *> A.norm_zro)) (inv partialSum-empty) <=-refl
  | suc N' => rewrite (partialSum_suc {A} {S} {N'}, partialSum_suc {ExUpperRealAbMonoid} {\lam k => A.norm (S k)} {N'})
                      (A.norm_+ <=∘ <=_+ partialSum_norm_<= <=-refl)

\lemma constSeries-seriesSum {A : TopAbGroup} {a : A} : IsSeriesSum (FSeriesRing.coef a) a
  => transport (IsSeriesSum _) zro-right $
      seriesSum-fin 1 \lam {j} le => \case \elim j, \elim le \with {
        | 0, le => absurd (NatSemiring.<-irreflexive (NatOrder.zero<suc NatSemiring.<∘l le))
        | suc _, _ => idp
      }

\lemma upper-constSeries-conv {a : ExUpperReal} : IsConvUpperSeries (FSeriesRing.coef a)
  => \lam eps>0 => inP (1, \lam n>=1 => rewrite (midSum.=FinSum *> {ExUpperReal} AbMonoid.FinSum_zro (later \case \elim __ \with {
    | (0, p, _) => absurd (p NatOrder.zero<suc)
    | (suc _, _, _) => idp
  })) eps>0)

\lemma constSeries-abs-conv {A : ExPseudoNormedAbGroup} {a : A} : IsAbsConvSeries (FSeriesRing.coef a)
  => transportInv IsConvUpperSeries (ext \case \elim __ \with {
    | 0 => idp
    | suc n => A.norm_zro
  }) (upper-constSeries-conv {norm a})

-- | The identity of FormalSubstMonoid sums to $x$ — only the $k=1$ term contributes: $1_A \cdot x = x$
\lemma subst-ide-seriesSum {A : TopRing} (x : A) : IsSeriesSum (\lam k => subst-ide k A.* Monoid.pow x k) x
  => transport (IsSeriesSum _) simplify $ seriesSum-fin 2 \lam {j} => \case \elim j \with {
    | 0 => \lam _ => zro_*-left
    | 1 => \lam p => absurd $ p $ NatOrder.suc<suc NatOrder.zero<suc
    | suc (suc j) => \lam _ => zro_*-left
  }