\import Algebra.Field
\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Ordered
\import Analysis.FuncLimit
\import Analysis.PowerSeries
\import Analysis.Series
\import Arith.Int
\import Arith.Nat
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\import Combinatorics.Factorial
\import Function.Meta
\import Logic
\import Meta
\import Order.LinearOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Topology.CoverSpace.Complete
\import Topology.MetricSpace
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.Real
\import Topology.NormedRing

\sfunc expR : CoverMap RealNormed RealNormed
  => funcLimit (\lam n x => partialSum (powerSeries (\lam n => Real.fromRat $ RatField.finv (fac n)) __ x) n) (powerSeriesConv-funcConv exp-series-conv)
  \where {
    \lemma exp-series-conv : IsPowerSeriesConv \lam n => Real.fromRat $ RatField.finv (fac n)
      => power-ratio-test-inf _ (\lam n => Real.fromRat $ RatField.finv (suc n)) (\lam n => later $
          rewrite (RealAbGroup.abs-ofPos $ rat_real_<=. $ LinearOrder.<_<= $ RatField.finv>0 $ fromInt_< $ pos<pos $ fac>0 {suc n},
                   RealAbGroup.abs-ofPos $ rat_real_<=. $ LinearOrder.<_<= $ RatField.finv>0 $ fromInt_< $ pos<pos fac>0) $
           RealAbGroup.=_<= $ pmap Real.fromRat (pmap (\lam x => finv (Rat.fromInt (pos x))) *-comm *> RatField.finv_* {fac n} {suc n} *> *-comm) *> inv RealField.*-rat) inv-limit

    \lemma inv-limit : RealNormed.IsLimit (\lam n => RatField.finv (suc n)) 
      => \lam Uo U0 => \case (dist_open {RealNormed}). Uo U0 \with {
        | inP (eps,eps>0,h) => \case UpperReal.natBounded {OrderedField.pinv eps>0} \with {
          | inP (N,p) => inP (N, \lam N<=n => h $ transportInv (`< _) (norm-dist *> norm_-) $ unfold (-) $
              \have lem => real_<_L. $ RatField.<-char $ pos<pos $ transport (`< _) *-comm NatSemiring.zero<suc
              \in rewrite (AddGroup.negative_zro, zro-right, RealField.abs-ofPos $ LinearOrder.<_<= lem) $ transport2 (<) ide-right
                  (inv *-assoc *> pmap (`* _) (RealField.*-rat *> pmap Real.fromRat (RatField.finv-left \lam p => suc/=0 $ unpos $ pmap ratNom p)) *> ide-left) $
                RealField.<_*_positive-right lem $ transport (`< _) (RealField.pinv-left eps>0) $ <_*_positive-left (real_<_U. p <∘ real_<_U. (fromInt_< (pos<pos $ N<=n <∘r id<suc))) eps>0)
        }
      }
  }