Series

\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\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 Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Analysis.Limit
\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 OrderedField
\open Monoid \hiding (equals)
\open LinearlyOrderedSemiring

\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

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

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

\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 Sc

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

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

\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-topAbGruop-char 2 0 \lam {U} Uo U0 => \case convergent-topAbGruop-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-topAbGruop-char 2 0 \lam {U} Uo U0 => \case convergent-topAbGruop-char 0 1 Sc Uo U0 \with {
    | inP (N, g) => inP (suc N, \lam {n} => \case \elim n \with {
      | 0 => \lam p => absurd $ p NatSemiring.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 series-shifts-conv {A : TopAbGroup} {S : Series A} (N : Nat) : IsConvSeries S <-> IsConvSeries \lam n => S (n + N) \elim N
  | 0 => <->refl
  | suc N => <->trans (series-shifts-conv N) series-shift-conv

\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

\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 NatSemiring.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 : PseudoNormedAbGroup} {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 {R : Ring} {x : R} {b : Series R} {n m : Nat} : x * midSum b n m = midSum (\lam j => x * b j) n m \elim n, m
  | 0, m => rewrite (\peval partialSum _ _, \peval partialSum _ _) R.BigSum-ldistr
  | suc n, 0 => zro_*-right
  | suc n, suc m => midSum-ldistr

\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 NatSemiring.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 NatSemiring.zero<suc)
  | suc n, suc m, suc k => midSum-split (suc<=suc.conv p) (suc<=suc.conv q)

\lemma midSum_<= {A : LinearlyOrderedAbMonoid} {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) (NatSemiring.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 : LinearlyOrderedAbMonoid} {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 : PseudoNormedAbGroup} {S : Series A}
                   (p : ∀ {eps : Real} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> norm (midSum S N n) < eps))
  : IsConvSeries S
  => convergent-metric-char 1 0 \lam eps>0 => \case p eps>0 \with {
    | inP (N,g) => inP (N, \lam q => rewrite (norm-dist, inv (midSum-diff q)) (g q))
  }
  \where {
    \protected \lemma conv (p : IsConvSeries S) : ∀ {eps : Real} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> norm (midSum S N n) < eps)
      => \lam eps>0 => \case convergent-metric-char 0 1 p eps>0 \with {
        | inP (N,g) => inP (N, \lam q => rewrite (midSum-diff q, inv norm-dist) (g q))
      }
  }

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

\lemma absConv-isConv {A : PseudoNormedAbGroup} {S : Series A} (Sc : IsAbsConvSeries S) : IsConvSeries S
  => series-conv \lam eps>0 => \case series-conv.conv Sc eps>0 \with {
    | inP (N,g) => inP (N, \lam p => midSum_norm <∘r RealAbGroup.abs>=id <∘r g p)
  }

\lemma series-limit {A : TopAbGroup} {S : Series A} (Sc : IsConvSeries S) : A.IsLimit S 0
  => \lam {U} Uo U0 => \case convergent-topAbGruop-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 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 \lam eps>0 => \case series-conv.conv 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_<=-abs {A : PseudoNormedAbGroup} {b c : Series A} (s : \Pi (j : Nat) -> norm (b j) <= norm (c j)) (cc : IsAbsConvSeries c) : IsAbsConvSeries b
  => series_<= (\lam j => norm>=0) s cc

\lemma series_*_lim {A : PseudoNormedRing} {b c : Series A} {l : A} (bl : A.IsLimit b l) (cc : IsAbsConvSeries c) : IsAbsConvSeries \lam n => b n * c n
  => series-conv \lam {eps} eps>0 =>
      \have | delta1>0 : 0 < norm l + 1 => linarith norm>=0
            | delta2>0 : 0 < pinv delta1>0 * eps => OrderedSemiring.<_*_positive_positive (pinv>0 delta1>0) eps>0
      \in \case limit-metric-char.1 bl RealAbGroup.zro<ide, series-conv.conv cc delta2>0 \with {
        | inP (N,g), inP (M,h) => inP (N ∨ M, \lam p => midSum_norm {_} {_} {N ∨ M} <∘r
            transport2 (<=) zro-left (inv $ midSum-split join-right p) (RealField.<=_+ (midSum>=0 \lam j => <=_*_positive_positive (LinearOrder.<_<= delta1>0) norm>=0) $
                midSum_<= \lam {j} p' _ => transportInv (`<= _) (RealField.abs-ofPos norm>=0) (A.norm_*_<= <=∘ <=_*_positive-left (linarith $ norm_-right <∘r transport (`< 1) A.norm-dist (g $ join-left <=∘ p')) norm>=0)) <∘r
            (rewrite (pinv-right,ide-left,midSum-ldistr) in transportInv (_ <) RealField.*-assoc (RealField.<_*_positive-right delta1>0 $ RealField.abs>=id <∘r h (join-right <=∘ p))))
      }

\lemma geometric-series-conv {x : Real} (p : RealAbGroup.abs x < 1) : seriesSum (pow x) = defined (pinv (diff-pos p))
  => generalized (RealField.pos#0 $ linarith $ RealField.abs>=id <∘r p) p
  \where {
    \lemma pow_+1-bound {e : Real} (e>=0 : 0 <= e) {n : Nat} : 1 + e * n <= pow (e + 1) n \elim n
      | 0 => simplify <=-refl
      | suc n => later (rewrite (inv (RealAbGroup.+-rat {n} {1}), ldistr, ldistr, rdistr) $
          linarith (<=_*_positive_positive (<=_*_positive_positive e>=0 $ rat_real_<=.1 $ fromInt_<= $ pos<=pos zero<=_) e>=0 : 0 <= e * n * e)) <=∘ <=_*_positive-left (pow_+1-bound e>=0) linarith

    \lemma pow_>1-bound {b : Real} (b>1 : 1 < b) (B : Nat) : ∃ (n : Nat) ((B : Real) < pow b n) \elim B
      | 0 => inP (0, RealAbGroup.zro<ide)
      | 1 => inP (1, rewrite ide-left b>1)
      | 2 => \have b-1>0 : 0 < b - 1 => linarith
             \in \case Real.natBounded {pinv b-1>0} \with {
               | inP (n,nb) => inP (n, rewrite (linarith : b = (b - 1) + 1, linarith : Real.fromRat 2 = (1 : Real) + 1) $
                  <_+-right 1 (transport (`< _) (pinv-right b-1>0) $ later $ <_*_positive-right b-1>0 $ real_<_U.2 nb) <∘l pow_+1-bound (LinearOrder.<_<= b-1>0))
             }
      | suc (suc (suc B)) => \case pow_>1-bound b>1 (suc (suc B)) \with {
        | inP (N,p) => inP (N + N, rewrite pow_+ $ later (rewrite RealField.*-rat $ real_<_L.2 $ fromInt_< linarith) <∘
            <_*_positive-right (real_<_L.2 $ later idp) p <∘ <_*_positive-left p (RealField.pow>0 linarith))
      }

    \lemma pow_1/2-bound {n : Nat} : RealField.pow (ratio 1 2) n <= RealField.pinv {suc n} (real_<_L.2 $ later idp) \elim n
      | 0 => transportInv (_ <=) pinv_ide <=-refl
      | suc n => <=_*_positive-left pow_1/2-bound linarith <=∘
          \have zro<2 : RealField.zro < Real.fromRat 2 => linarith
          \in rewrite (inv (RealField.pos-inv_rat zro<2), pinv_*) $ pinv_<= (real_<_L.2 $ later idp) (RealField.<_*_positive_positive (real_<_L.2 $ later idp) zro<2) $
                later $ rewrite RealField.*-rat $ rat_real_<=.1 linarith

    \lemma pow_<1-bound {a : Real} (a<1 : a < 1) {eps : Real} (eps>0 : 0 < eps) : ∃ (n : Nat) (pow a n < eps)
      => \case Real.natBounded {pinv eps>0} \with {
        | inP (B,Bb) => \case real-located {a} {0} {ratio 1 2} (real_<_L.2 $ later idp) \with {
          | byLeft a>0 => \case pow_>1-bound {pinv a>0} (pinv>1 a>0 a<1) B \with {
            | inP (n,p) => inP (n, pinv_<-conv (RealField.pow>0 a>0) eps>0 $ real_<_U.2 Bb <∘ transport (_ <) (pinv_pow a>0) p)
          }
          | byRight a<1/2 => \case real-located {a} {RealField.negative (ratio 1 2)} {0} linarith \with {
            | byLeft a>-1/2 => inP (B, RealField.abs>=id <∘r transportInv (`< _) OrderedRing.abs_pow
                (pow_<=-monotone RealField.abs>=0 (join-univ (LinearOrder.<_<= a<1/2) (LinearOrder.<_<= $ RealField.negative_<-left a>-1/2)) <∘r
                  pow_1/2-bound <∘r transport (_ <) (pinv_pos-inv eps>0)
                    (pinv_< (pinv>0 eps>0) (real_<_L.2 $ later idp) $ real_<_U.2 Bb <∘ real_<_L.2 (fromInt_< $ pos<pos id<suc))))
            | byRight a<0 => inP (1, transportInv (`< _) ide-left $ a<0 <∘ eps>0)
          }
        }
      }

    \protected \lemma generalized {X : CompleteValuedRing} {x : X} (xi : Inv (1 - x)) (|x|<1 : norm x < 1) : seriesSum (pow x) = defined xi.inv
      => seriesSum_defined {_} {pow x} \lam {eps} eps>0 =>
          \have |1-x|>0 : 0 < norm (1 - x) => linarith norm_ide <∘l norm_-left
          \in \case pow_<1-bound |x|<1 {eps * norm (1 - x)} $ RealField.<_*_positive_positive eps>0 |1-x|>0 \with {
            | inP (N,q) => inP (N, later \lam N<=n => rewrite (\peval partialSum _ _, X.geometric-partial-sum) $ norm_*_<= <∘r <=_*_positive-left norm_<=_pow norm>=0 <∘r
                transport (_ <) (*-assoc *> pmap (_ *) (inv norm_* *> pmap norm xi.inv-right *> norm_ide) *> ide-right) (<_*_positive-left (pow_<=-degree norm>=0 (LinearOrder.<_<= |x|<1) N<=n <∘r q) $
                  <_*_positive-cancel-right (LinearOrder.<_<= |1-x|>0) $ transport2 (<) (inv zro_*-left) (inv norm_ide *> pmap norm (inv xi.inv-left) *> norm_*) zro<ide))
          }

    \protected \lemma diff-pos {x y : Real} (p : RealAbGroup.abs x < y) : 0 < y - x
      => linarith $ RealAbGroup.abs>=id {x}
  }

\lemma geometric-series-absConv {X : PseudoNormedRing} {x : X} (p : norm x < 1) : IsAbsConvSeries (pow x)
  => series_<= (\lam j => norm>=0) (\lam j => norm_<=_pow) $ defined-ext.isDefined $ geometric-series-conv $ rewrite (RealField.abs-ofPos norm>=0) p

\lemma ratio-test {X : PseudoNormedAbGroup} {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
  => \case real_<-char.1 (LinearOrder.<_join-univ l<1 zro<ide) \with {
    | inP (r,lz<r,r<1) => \case bl (OBall-open {_} {r - l} {l}) (rewrite dist-refl $ linarith (usingOnly (join-left <∘r lz<r))) \with {
      | inP (N,g) => (series-shifts-conv N).2
          \have r>=0 => join-right <=∘ LinearOrder.<_<= lz<r
          \in series_<= (\lam j => norm>=0) (iter-bound (\lam j => norm>=0) r>=0 (\lam j => bp (j + N))
                  (\lam j => linarith (usingOnly (RealAbGroup.abs>=_- <=∘ LinearOrder.<_<= (rewrite norm-dist in g (NatSemiring.<=_+ zero<=_ <=-refl)))))) $
                absConv-isConv $ series_*_lim const-limit $ geometric-series-absConv $ later $ rewrite (RealAbGroup.abs-ofPos r>=0) r<1
    }
  }
  \where {
    \lemma iter-bound {f b : Nat -> 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 => rewrite ide-right <=-refl
      | suc j => bp j <=∘ <=_*_positive-right (f>=0 j) (bb j) <=∘ transport (_ <=) *-assoc (<=_*_positive-left (iter-bound f>=0 r>=0 bp bb j) r>=0)
  }

\lemma MTest {X : \Set} {Y : PseudoNormedAbGroup} (f : Nat -> X -> Y) (M : Nat -> Real)
             (Mp : \Pi (n : Nat) (x : X) -> norm (f n x) <= M n) (Mc : IsConvSeries M) : IsUniFuncConvergent \lam n x => partialSum (f __ x) n
  => \lam Du => \case dist-uniform.1 Du \with {
    | inP (eps,eps>0,h) => \case series-conv.conv Mc eps>0 \with {
      | inP (N,g) => inP (N, \lam x => \case h (partialSum (f __ x) N) \with {
        | inP (V,DV,Vg) => inP (V, DV, \lam p => Vg $ rewrite (norm-dist, norm_-, inv $ midSum-diff {_} {f __ x} p) $
            rewrite (RealAbGroup.abs-ofPos $ midSum>=0 \lam j => norm>=0 <=∘ Mp j x) (midSum_norm <=∘ midSum_<= \lam _ _ => Mp _ x) <∘r g p)
      })
    }
  }

\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