\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.Ring
\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.Subset
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.Product
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.Real
\import Topology.NormedAbGroup.Real.Functions
\import Topology.NormedRing
\import Topology.TopSpace
\import Topology.UniformSpace
\open Monoid(pow)

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

\lemma powerSeries_0 {cs : Series ExUpperReal} (csb : \Pi (j : Nat) -> ∃ (B : Rat) ((cs j).U B)) : IsConvUpperSeries \lam j => cs j * RatField.pow  j
  => (upperSeries-shift-conv \lam j => ExUpperRealSemigroup.*_>=0). \lam eps>0 => inP (, \lam _ => transportInv (ExUpperReal.U {__} _) ((\peval partialSum _ _) *> AddMonoid.BigSum_zro \lam j => later $ pmap (_ *) (pmap ExUpperReal.fromRat $ RatField.pow_0 suc/=0) *> ExUpperRealSemigroup.zro_*-right (csb _)) eps>0)

\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 \lam j => norm-bounded _))
  | 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)

\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) $ 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, _ => inP (, a<0, powerSeries_0 \lam j => norm-bounded _)
    | 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)
  }

\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 powerSeriesConv-funcConv {X : ExPseudoNormedRing} {cs : Nat -> X} (p : IsPowerSeriesConv cs)
  : IsFuncConvergent \lam n x => partialSum (powerSeries cs __ x) n
  => funcCovergent-metric-char (partialSum-cover \lam j => *-locally-uniform CoverMap.∘ ProductCoverSpace.tuple (CoverMap.const (cs j)) (pow-cover j)) \lam {eps} eps>0 =>
      X.makeCauchy $ uniform-subset (X.metricUniform eps>0) \lam {_} (inP (x,idp)) =>
        \case MTest {\Sigma (y : X) (norm y <= norm x + eps)} (\lam n s => powerSeries cs n s.)
                (\lam n => norm (cs n) * ExUpperRealSemigroup.pow (norm x + eps) n)
                (\lam n s => norm_*_<= <=∘ ExUpperRealSemigroup.<=_* <=-refl (norm_<=_pow <=∘ ExUpperRealSemigroup.pow_<= s.))
                (IsPowerSeriesConv.upper p (ExUpperRealAbMonoid.<=_+-positive norm>=0 $ ExUpperReal.<_<= eps>0) $ TruncP.map (norm-bounded x) \lam (B,|x|<B) => (B + eps, ExUpperRealAbMonoid.<-rat. $ transport (_ <) ExUpperReal.+-rat $ ExUpperRealAbMonoid.<_+-left $ ExUpperRealAbMonoid.<-rat. |x|<B))
                (X.metricUniform $ RatField.half>0 eps>0) \with {
          | inP (N,h) => inP $ later (N, \lam {y} xy<eps N<=n => \case h (y, transport (_ <=) +-comm $ norm_dist-left <=∘ ExUpperRealAbMonoid.<=_+ (transport (`<= _) X.dist-symm $ ExUpperReal.<_<= xy<eps) <=-refl) \with {
            | inP (_, inP (z,idp), g) => X.halving1/2 (g N<=n) (g <=-refl)
          })
        }

\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