\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.Ring
\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 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.TopSpace
\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

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

\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

\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 = )
  : 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

\func midSum {A : AddMonoid} (S : Series A) (n m : Nat) : A \elim n, m
  | , m => partialSum S m
  | suc n,  => 
  | suc n, suc m => midSum (\lam j => S (suc j)) n m

\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
  | , m => partialSum_hom f
  | suc n,  => f.func-zro
  | suc n, suc m => midSum_hom f

\func IsConvUpperSeries (S : Series ExUpperReal) : \Prop
  => ∀ {eps : Rat} ( < 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
  |  => 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
  | ,  => idp
  | , suc m => idp
  | suc n,  => inv partialSum-empty
  | suc n, suc m => midSum_midSum'

\lemma zeroSeries-sum {A : TopAbGroup} : IsSeriesSum (\lam _ => A.zro) 
  => \lam {U} _ U0 => inP (, \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   \lam {U} Uo U0 => \case convergent-topAbGroup-char   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   \lam {U} Uo U0 => \case convergent-topAbGroup-char   Sc Uo U0 \with {
    | inP (N, g) => inP (suc N, \lam {n} => \case \elim n \with {
      |  => \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) ->  <= 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))
  }, \lam c eps>0 => \case c eps>0 \with {
    | inP (M,h) => inP (suc M, \lam {n} => \case \elim n \with {
      |  => \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) ->  <= S j) (N : Nat) : IsConvUpperSeries S <-> IsConvUpperSeries \lam n => S (n + N) \elim N
  |  => <->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
  |  => (\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
  | , m => inv $ rewrite (\peval partialSum S _, \peval partialSum S _) $ pmap (_ +) A.negative_zro *> zro-right
  | suc n,  => 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 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
  | , m => rewrite (\peval partialSum _ _, \peval partialSum _ _) A.norm_BigSum
  | suc n,  => A.norm_BigSum {nil}
  | suc n, suc m => midSum_norm

\lemma midSum_<=-ldistr {x : ExUpperReal} {b : Series ExUpperReal} (b>=0 : \Pi (j : Nat) ->  <= b j) {n m : Nat}
  : midSum (\lam j => x * b j) n m <= x * midSum b n m \elim n, m
  | , m => rewrite (\peval partialSum _ _, \peval partialSum _ _) $ BigSum_<=-ldistr \lam j => b>=0 j
  | suc n,  => 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) ->  <= 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 ) $ 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
  | , , k => rewrite (\peval partialSum _ _, \peval partialSum _ _) (inv zro-left)
  | _, suc m,  => absurd (q NatOrder.zero<suc)
  | , 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, , _ => 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 =  \elim n, m, m<n
  | suc n, , 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) ->  <= 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
  | , m => rewrite (\peval partialSum _ _, \peval partialSum _ _) $ A.BigSum_<= \lam j => s zero<=_ (fin_< j)
  | suc n,  => <=-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 =  \elim n, m
  | , m => (\peval partialSum _ _) *> A.BigSum_replicate0
  | suc n,  => idp
  | suc n, suc m => midSum_0

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

\lemma series-conv {A : ExPseudoNormedAbGroup} {S : Series A}
  : IsConvSeries S <-> ∀ {eps : Rat} ( < eps) ∃ (N : Nat) ∀ {n} (N <= n -> (norm (midSum S N n)).U eps)
  => (\lam p eps>0 => \case convergent-metric-char. 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. \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} ( < 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. eps>0 \with {
    | inP (eps',eps'>0,eps'<eps) => \case sc eps'>0 \with {
      | inP (N,h) => inP (N, \lam p => real_<_U. (h p) <∘ real_<_L. eps'<eps)
    }
  }, \lam sc eps>0 => \case sc (rat_real_<. eps>0) \with {
    | inP (N,h) => inP (N, \lam p => real_<_U. $ h p)
  })

\lemma seriesSum_defined {A : CompleteExNormedAbGroup} {S : Series A} {a : A}
                         (p : ∀ {eps : Rat} ( < eps) ∃ (N : Nat) ∀ {n} (N <= n -> (norm (a - partialSum S n)).U eps))
  : seriesSum S = defined a
  => seriesSum-char. \lam Uo Ua => \case dist_open. 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 : seriesSum S = defined a) : ∀ {eps : Rat} ( < eps) ∃ (N : Nat) ∀ {n} (N <= n -> (norm (a - partialSum S n)).U eps)
      => \lam eps>0 => \case seriesConv-sum (defined-ext.isDefined {_} {seriesSum S} p) OBall-open $ unfold OBall $ rewrite (defined-ext.value {_} {seriesSum S} p, A.dist-refl) eps>0 \with {
        | inP (N,g) => inP (N, \lam q => rewriteI A.norm-dist (g q))
      }
  }

\lemma absConv-isConv {A : ExPseudoNormedAbGroup} {S : Series A} (Sc : IsAbsConvSeries S) : IsConvSeries S
  => series-conv. \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 
  => \lam {U} Uo U0 => \case convergent-topAbGroup-char   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) ->  <= b j) (s : \Pi (j : Nat) -> b j <= c j) (cc : IsConvSeries c) : IsConvSeries b
  => series-conv-real. \lam eps>0 => \case series-conv-real. 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)., \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)). $ RatField.Big_<=_join1 (toFin n n<N)
          | inr N<=n => ExUpperReal.U_<= (SB N<=n) RatField.Big_<=_join0
        })
      }
  }

\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. 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_<=. $ inP (, rewriteI (norm_-, A.norm-dist) (h N<=j), B, l<B, <=-refl)
  }

\lemma series_*-bounded {b c : Series ExUpperReal} (c>=0 : \Pi (j : Nat) ->  <= c j) (bB : IsBoundedUpperSeries b) (cc : IsConvUpperSeries c) : IsConvUpperSeries \lam n => b n * c n \elim bB
  | inP (B, bB) =>
    \let | B1 => B ∨ 
         | B1>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 geometric-upper-series-conv {r : ExUpperReal} (r>=0 :  <= r) (r<1 : r.U ) : 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 * ( - q)} $ RatField.<_*_positive_positive eps>0 linarith
      \in inP (B., \lam {n} B<=n => rewrite midSum_midSum' $ ExUpperRealAbMonoid.<-rat. $ transport {Series ExUpperReal} (partialSum __ _ < eps) {\lam k => pow q B. * pow q k} (later $ ext \lam k => pmap ExUpperReal.fromRat $ inv pow_+) $
            transport (ExUpperRealAbMonoid.`< _) (partialSum_hom rat-upperReal) $ ExUpperRealAbMonoid.<-rat. $ transportInv (`< _) (\peval partialSum _ _) $ later $ transport (`< _) (RatField.BigSum-ldistr {pow q B.} {\new Array Rat (n -' B.) (pow q __)}) $
            RatField.<=_*_positive-left (<=-less B.) (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 ) : IsAbsConvSeries (pow x)
  => series_<= (\lam j => norm_<=_pow) $ geometric-upper-series-conv norm>=0 |x|<1

\lemma upper-ratio-test {S : Series ExUpperReal} (S>=0 : \Pi (n : Nat) ->  <= S n) (S0b : ∃ (B : Rat) ((S ).U B))
                        (b : Series Real) (bp : \Pi (n : Nat) -> S (suc n) <= S n * b n)
                        {l : Real} (l<1 : l < ) (bl : RealNormed.IsLimit b l) : IsConvUpperSeries S
  => \case real_<-char. (<_join-univ l<1 RealAbGroup.zro<ide) \with {
    | inP (r,lz<r,r<1) => \case (real_<-rat-char {} {(r : Real) - l}). $ 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).
          \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. $ g $ <=_+ zero<=_ <=-refl), real_<_L. q<r-l))) $
          series_*-bounded (\lam j => Real.<=-upper. $ 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. $ rat_real_<=. r>=0) (rat_real_<. r<1)
      }
    }
  }
  \where {
    \lemma iter-bound {f : Nat -> ExUpperReal} {b : Nat -> Real} (f>=0 : \Pi (j : Nat) ->  <= f j) {r : Real} (r>=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  * pow r j \elim j
      |  => transportInv (_ <=) (ExUpperRealSemigroup.ide-right $ f>=0 ) <=-refl
      | suc j => bp j <=∘ ExUpperRealSemigroup.<=_* <=-refl (Real.<=-upper. $ 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
      |  => S0b
      | suc n => \case S-bounded n, (b n).U-inh \with {
        | inP (B,Sn<B), inP (C,bn<C) => inP (B * (C ∨ ) + , ExUpperRealAbMonoid.<-rat. $ bp n <∘r ExUpperRealSemigroup.<=_* (ExUpperReal.<_<= Sn<B) (ExUpperReal.<_<= bn<C <=∘ ExUpperReal.<=-rat. join-left) <∘r transportInv (ExUpperRealAbMonoid.`< _) (ExUpperReal.*-rat (<=-less $ S>=0 n Sn<B) join-right) (ExUpperRealAbMonoid.<-rat. 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 < ) (bl : RealNormed.IsLimit b l) : IsAbsConvSeries S
  => upper-ratio-test (\lam j => norm>=0) (norm-bounded (S )) 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. \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 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