\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.FormalSeries
\import Algebra.Semiring
\import Analysis.FuncLimit
\import Analysis.Series
\import Arith.Nat
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\import Arith.Real.LowerReal
\import Arith.Real.UpperReal
\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 Set.Set
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.Directed
\import Topology.CoverSpace.Product
\import Topology.MetricSpace
\import Topology.MetricSpace.OpenBall
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.Real
\import Topology.NormedAbGroup.Real.Functions
\import Topology.NormedRing
\import Topology.TopAbGroup.Product
\import Topology.TopSpace
\import Topology.UniformSpace
\open Monoid(pow)

\func powerSeries {X : ExPseudoNormedRing} (cs : Nat -> X) (x : X) (n : Nat)
  => cs n * pow x n

\func convRadius {X : ExPseudoNormedRing} (cs : Nat -> X) : LowerReal \cowith
  | L a => ∃ (b : > a) (IsConvUpperSeries \lam j => X.norm (cs j) * pow b j)
  | L-inh => inP (-1, inP (, idp, powerSeries_0))
  | L-closed (inP (b,q<b,h)) q'<q => inP (b, q'<q <∘ q<b, h)
  | L-rounded {a} (inP (b,a<b,h)) => inP (RatField.mid a b, inP (b, RatField.mid<right a<b, h), RatField.mid>left a<b)
  \where {
    \lemma powerSeries_0 : IsConvUpperSeries (\lam n => norm (cs n) * pow RatField.zro n)
      => transportInv IsConvUpperSeries (ext \case \elim __ \with {
        |  => idp
        | suc n => pmap (_ * ExUpperReal.fromRat __) zro_*-right *> ExUpperRealSemigroup.zro_*-right (norm-bounded _)
      }) $ upper-constSeries-conv {norm (cs ) * }

    \lemma <LU-char {x : ExUpperReal} {a : Rat} (x<a : x.U a) (c : IsConvUpperSeries \lam j => norm (cs j) * pow a j) : x <LU convRadius cs
      => \case U-rounded x<a \with {
        | inP (b,x<b,b<a) => inP (b, x<b, inP (a, b<a, c))
      }
  }

\lemma convRadius>=0 {X : ExPseudoNormedRing} {cs : Nat -> X} :  <= convRadius cs
  => \lam q<0 => inP (, q<0, convRadius.powerSeries_0)

\lemma convRadius-absConv {X : ExPseudoNormedRing} (cs : Nat -> X) {x : X} (p : norm x <LU convRadius cs) : IsAbsConvSeries (powerSeries cs x) \elim p
  | inP (a, |x|<a, inP (b,a<b,cc)) => series_<= (\lam j => norm_*_<= <=∘ later (ExUpperRealSemigroup.<=_* <=-refl $ transport (_ <=) (ExUpperRealSemigroup.rat-pow $ <=-less $ norm>=0 |x|<a <∘ a<b) $ X.norm_<=_pow <=∘ ExUpperRealSemigroup.pow_<= (ExUpperReal.<_<= |x|<a <=∘ ExUpperReal.<=-rat. (<=-less a<b)))) cc

\lemma convRadius-div {X : ExPseudoValuedRing} (cs : Nat -> X) {x : X} (p : IsConvSeries (powerSeries cs x))
                      {a : Rat} (a<|x| : a ExUpperRealAbMonoid.< norm x) : (convRadius cs).L a
  => \case LinearOrder.dec<_<= a , \elim a<|x| \with {
    | inl a<0, _ => convRadius>=0 a<0
    | inr a>=0, inP (c,a<c,c<=|x|) => \case isDense a<c \with {
      | inP (b,a<b,b<c) =>
        \have bc'>=0 => <=-less $ RatField.<_*_positive_positive (a>=0 <∘r a<b) $ RatField.finv>0 (a>=0 <∘r a<c)
        \in inP (b, a<b, transport IsConvUpperSeries {\lam j => norm (cs j) * pow c j * ExUpperRealSemigroup.pow (b * RatField.finv c) j}
                (later $ ext \lam n => *-assoc *> pmap (_ *) (pmap (_ *) (ExUpperRealSemigroup.rat-pow bc'>=0) *> ExUpperReal.*-rat (<=-less $ RatField.pow>0 $ a>=0 <∘r a<c) (RatField.pow>=0 bc'>=0) *> pmap ExUpperReal.fromRat (inv RatField.pow_*-comm *> pmap (pow __ n) (*-comm *> *-assoc *> pmap (b *) (RatField.finv-left $ RatField.>_/= $ a>=0 <∘r a<c) *> ide-right))))
                (series_*-bounded (\lam j => ExUpperRealSemigroup.pow_>=0) (upperSeries-bounded_<= {_} {\lam n => norm (cs n * pow x n)}
                    (\lam n => ExUpperRealSemigroup.<=_* {_} {_} {pow c n} <=-refl (transport2 (<=) (ExUpperRealSemigroup.rat-pow $ <=-less $ a>=0 <∘r a<c) (inv norm_pow) $ ExUpperRealSemigroup.pow_<= c<=|x|) <=∘ =_<= (inv X.norm_*)) $ series-lim-bound $ series-limit p) $
                  geometric-upper-series-conv (ExUpperReal.<=-rat. bc'>=0) $ transport (< _) *-comm $ RatField.<_rotate-left (a>=0 <∘r a<c) $ transportInv (b <) ide-right b<c))
    }
  }

\type IsPowerSeriesConv {X : ExPseudoNormedRing} (cs : Nat -> X) : \Prop
  => \Pi {a : Rat} ->  <= a -> IsConvUpperSeries (\lam n => norm (cs n) * pow a n)
  \where {
    \protected \lemma upper (cc : IsPowerSeriesConv cs) {a : ExUpperReal} (a>=0 :  <= a) (aB : ∃ (B : Rat) (a.U B)) : IsConvUpperSeries \lam n => norm (cs n) * ExUpperRealSemigroup.pow a n \elim aB
      | inP (B,a<B) => series_<= (\lam n => ExUpperRealSemigroup.<=_* <=-refl (transport (_ <=) (ExUpperRealSemigroup.rat-pow $ <=-less $ a>=0 a<B) $ ExUpperRealSemigroup.pow_<= $ ExUpperReal.<_<= a<B)) $ cc $ <=-less $ a>=0 a<B

    \protected \lemma atPoint (cc : IsPowerSeriesConv cs) {x : X} : IsConvUpperSeries \lam n => norm (cs n) * ExUpperRealSemigroup.pow (norm x) n
      => upper cc norm>=0 (norm-bounded x)

    \protected \lemma char : IsPowerSeriesConv cs <-> (convRadius cs = LowerReal.infinity)
      => (\lam psc => exts \lam q => propExt (\lam _ => ()) \lam _ => inP ((q + ) ∨ , linarith <∘l join-left, psc join-right),
          \lam cri {a} a>=0 => \case propExt.conv (path \lam i => (cri i).L a) () \with {
            | inP (b,a<b,psc) => series_<= (\lam n => ExUpperRealSemigroup.<=_* <=-refl (ExUpperReal.<=-rat. $ RatField.pow_<=-monotone a>=0 $ <=-less a<b)) psc
          })

    \lemma toConvRadius_<LU (psc : IsPowerSeriesConv cs) {x : X} : dist  x <LU convRadius cs
      => transport2 (<LU) norm_dist (inv $ char. psc) \case norm-bounded x \with {
        | inP (q,x<q) => inP (q, x<q, ())
      }
  }

\lemma powerSeriesConv-absConv {X : ExPseudoNormedRing} {cs : Nat -> X} (p : IsPowerSeriesConv cs) {x : X} : IsAbsConvSeries (powerSeries cs x)
  => \case norm-bounded x \with {
    | inP (B,|x|<B) => convRadius-absConv cs $ inP (B, |x|<B, inP (B + , linarith, p $ linarith $ norm>=0 |x|<B))
  }

\lemma powerSeries-absConv {X : ExPseudoNormedRing} {cs : Nat -> X} {x : X}
                           (cu : IsConvUpperSeries \lam n => norm (cs n) * ExUpperRealSemigroup.pow (norm x) n)
  : IsAbsConvSeries (powerSeries cs x)
  => series_<= (\lam n => norm_*_<= ExUpperRealAbMonoid.<=∘ ExUpperRealSemigroup.<=_* <=-refl (X.norm_<=_pow {x} {n})) cu


\lemma powerSeriesConv-funcConv {X : ExPseudoNormedRing} (cs : Nat -> X)
  : IsFuncConvergent {_} {OpenBallCoverSpace  (convRadius cs)} \lam n x => partialSum (powerSeries cs x.) n
  => funcCovergent-metric-char {_} {OpenBallCoverSpace  (convRadius cs)} {_} {\lam n x => partialSum (powerSeries cs x.) n}
      (partialSum-cover \lam j => *-locally-uniform ∘ tuple (const (cs j)) (X.pow-cover j ∘ func))
      \lam eps>0 => closure-subset makeBasicCover2 \lam {_} (inP (_, inP ((q, inP (r,q<r,conv)),idp), idp)) => \case conv eps>0 \with {
        | inP (N,h) => inP (N, \lam cx<q N<=n => rewrite (norm-dist, inv (midSum-diff N<=n)) $ midSum_norm $ midSum_<= {ExUpperRealAbMonoid}
          (\lam {j} N<=j j<n => norm_*_<= ExUpperRealAbMonoid.<=∘ <=_* <=-refl (X.norm_<=_pow {_} {j} <=∘ pow_<= (=_<= norm_dist
            <=∘ ExUpperReal.<_<= (U-closed cx<q q<r)) <=∘ =_<= (rat-pow $ <=-less $ dist>=0 cx<q <∘ q<r))) (h N<=n))
      }
  \where {
    \open ProductCoverSpace (tuple)
    \open CoverMap (∘, const)
    \open OpenBallCoverSpace
    \open ClosurePrecoverSpace
    \open ExUpperRealSemigroup
  }

-- | The sum of a power series inside its radius of convergence.
\sfunc powerSeriesSum {X : CompleteExNormedRing} (cs : Nat -> X) (x : X) (xc : dist  x <LU convRadius cs) : X
  => seriesSum (powerSeries cs x) $ funcConv-pointwise {_} {OpenBallCoverSpace  (convRadius cs)}
      (\lam n x => partialSum (powerSeries cs x.) n) (powerSeriesConv-funcConv cs) {x,xc}

-- | {powerSeriesSum} is a cover map.
\lemma powerSeriesSum-cover {X : CompleteExNormedRing} {cs : Nat -> X}
  : CoverMap (OpenBallCoverSpace  (convRadius cs)) X (\lam s => powerSeriesSum cs s. s.)
  => transportInv (CoverMap _ X) (ext \lam s => \peval powerSeriesSum cs s. s.) $
      funcLimit {_} {OpenBallCoverSpace  (convRadius cs)} (\lam n x => partialSum (powerSeries cs x.) n) (powerSeriesConv-funcConv cs)

-- | {powerSeriesSum} is indeed the sum of the series.
\lemma powerSeriesSum-isSum {X : CompleteExNormedRing} {cs : Nat -> X} {x : X} {xc : dist  x <LU convRadius cs}
  : IsSeriesSum (powerSeries cs x) (powerSeriesSum cs x xc)
  => transportInv (IsSeriesSum _) (\peval powerSeriesSum cs x xc) (seriesConv-sum _)


-- | The total version of {powerSeriesConv-funcConv}.
\lemma powerSeriesConv-funcConv-total {X : ExPseudoNormedRing} {cs : Nat -> X} (psc : IsPowerSeriesConv cs)
  : IsFuncConvergent \lam n x => partialSum (powerSeries cs x) n
  => powerSeriesConv-funcConv cs CoverMap.∘ ProductCoverSpace.prod {DirectedCoverSpace NatBSemilattice} {_} {_} {OpenBallCoverSpace  (convRadius cs)} CoverMap.id
      (OpenBallCoverSpace.infinity-inv-cover X.distBounded $ IsPowerSeriesConv.char. psc)

-- | The total version of {powerSeriesSum}.
\sfunc powerSeriesSum-total {X : CompleteExNormedRing} (cs : Nat -> X) (psc : IsPowerSeriesConv cs) (x : X) : X
  => powerSeriesSum cs x (IsPowerSeriesConv.toConvRadius_<LU psc)

-- | {powerSeriesSum-total} is a cover map.
\lemma powerSeriesSum-total-cover {X : CompleteExNormedRing} {cs : Nat -> X} (psc : IsPowerSeriesConv cs)
  : CoverMap X X (powerSeriesSum-total cs psc)
  => transportInv (CoverMap X X) (ext \lam x => \peval powerSeriesSum-total cs psc x) $
      powerSeriesSum-cover CoverMap.∘ OpenBallCoverSpace.infinity-inv-cover X.distBounded (IsPowerSeriesConv.char. psc)

-- | {powerSeriesSum-total} is indeed the sum of the series.
\lemma powerSeriesSum-total-isSum {X : CompleteExNormedRing} {cs : Nat -> X} {x : X} {psc : IsPowerSeriesConv cs}
  : IsSeriesSum (powerSeries cs x) (powerSeriesSum-total cs psc x)
  => transportInv (IsSeriesSum _) (\peval powerSeriesSum-total cs psc x) powerSeriesSum-isSum


\lemma powerSeries-unbounded-conv {X : ExPseudoValuedRing} (Xu : X.IsUnbounded) {cs : Nat -> X} (Sc : \Pi (x : X) -> IsConvSeries (powerSeries cs x)) : IsPowerSeriesConv cs
  => \lam {a} a>=0 => \case Real.natBounded {a} \with {
    | inP (B,a<B) => \case Xu B \with {
      | inP (x,B<=|x|) => \case convRadius-div cs (Sc x) (ExUpperRealAbMonoid.<-rat. a<B <∘l B<=|x|) \with {
        | inP (b,a<b,bB) => series_<= (\lam n => ExUpperRealSemigroup.<=_* <=-refl (ExUpperReal.<=-rat. $ RatField.pow_<=-monotone a>=0 $ <=-less a<b)) bB
      }
    }
  }

\lemma power-ratio-test {X : ExPseudoNormedRing} {c : Series X} {b : Series Real} (bp : \Pi (n : Nat) -> norm (c (suc n)) <= norm (c n) * b n)
                        {l : Real} (bl : RealNormed.IsLimit b l) {a : Rat} (a>=0 :  <= a) (la<1 : l * a < ) : IsConvUpperSeries \lam j => norm (c j) * pow a j
  => upper-ratio-test (\lam n => ExUpperRealSemigroup.*_>=0) (rewrite (ExUpperRealSemigroup.ide-right norm>=0) (norm-bounded (c ))) (\lam n => b n * a)
    (\lam n => <=_* (bp n) <=-refl <=∘ transport2 (<=) (inv *-assoc) (inv *-assoc) (<=_* <=-refl $
      transport2 (<=) (*-comm *> *-assoc *> pmap (_ *) (*-comm *> ExUpperReal.*-rat (RatField.pow>=0 a>=0) a>=0)) (inv ExUpperRealSemigroup.*_join) $
      <=_* join-left $ transport (_ <=) (inv (RealField.*-upper join-right (rat_real_<=. a>=0)) *>
        RealField.join_*-right (rat_real_<=. a>=0) *> pmap (_ RealAbGroup.∨) RealField.zro_*-left *> RealAbGroup.join-upper) $ <=_* (Real.<=-upper. join-left) <=-refl))
    la<1 (cont-limit bl $ RealField.*-cover CoverMap.∘ ProductCoverSpace.tuple CoverMap.id (CoverMap.const (Real.fromRat a)))
  \where \open ExUpperRealSemigroup(<=_*)

\lemma power-ratio-test-inf {X : ExPseudoNormedRing} {cs : Series X} (b : Series Real)
                            (bp : \Pi (n : Nat) -> norm (cs (suc n)) <= norm (cs n) * b n) (bl : RealNormed.IsLimit b ) : IsPowerSeriesConv cs
  => \lam a>=0 => power-ratio-test bp bl a>=0 $ rewrite Ring.zro_*-left RealAbGroup.zro<ide

{- | Pointwise compatibility of convolution with {powerSeries}: when $x$
     commutes with all coefficients,
     $$(a_{\text{ps}} \star b_{\text{ps}})_n = (a \star b)_n \cdot x^n,$$
     where $a_{\text{ps}}\,k = a_k \cdot x^k$ is `powerSeries a x`. -}
\lemma conv-powerSeries {A : ExPseudoNormedRing} {a b : FSeries A} {x : A} (xc : A.IsCentral x) {n : Nat}
  : (FSeriesRing A).* (powerSeries a x) (powerSeries b x) n = powerSeries (a * b) x n
  => A.FinSum-ext (\lam s => equation.monoid {A.IsCentral_pow xc {s.} (b s.), inv A.pow_+ *> pmap (pow x) s.}) *> inv A.FinSum-rdistr