\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Pointed
\import Arith.Nat
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\import Arith.Real.UpperReal
\import Function.Meta
\import Logic
\import Logic.Meta
\import Logic.TFAE
\import Meta
\import Order.Biordered
\import Order.Directed
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set.Filter
\import Set.Partial
\import Set.Subset
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.Directed
\import Topology.MetricSpace
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.Real
\import Topology.TopAbGroup
\import Topology.TopRing
\import Topology.TopSpace
\import Topology.UniformSpace

\func IsConvergent {I : DirectedSet} {X : CoverSpace} (f : I -> X) : \Prop
  => CoverMap (DirectedCoverSpace I) X f

\lemma convergent-char {I : DirectedSet} {X : CoverSpace} {f : I -> X} (p : ∀ {C : X.isCauchy} ∃ (U : C) (N : I) ∀ {n} (N <= n -> U (f n))) : IsConvergent f
  => regPrecoverSpace-extend-coverMap \new PrecoverMap {
    | func => f
    | func-cover Dc => \case p Dc \with {
      | inP (U,DU,N,g) => later (inP (_, inP (U, DU, idp), N, g), \lam n => \case cauchy-cover Dc (f n) \with {
        | inP (V,DV,Vfn) => inP (_, inP (V, DV, idp), Vfn)
      })
    }
  }
  \where
    \protected \lemma conv {I : DirectedSet} {X : CoverSpace} {f : I -> X} (fc : IsConvergent f) : ∀ {C : X.isCauchy} ∃ (U : C) (N : I) ∀ {n} (N <= n -> U (f n))
      => \lam Cc => \case (func-cover {regPrecoverSpace} $ func-cover {fc} Cc). \with {
        | inP (_, inP (_, inP (U, CU, idp), idp), N, g) => inP (U, CU, N, g)
      }

\lemma limit-conv {I : DirectedSet} {X : CoverSpace} {f : I -> X} {l : X} (fl : X.IsLimit f l) : IsConvergent f
  => convergent-char \lam Cc => \case X.cauchy-regular-cover Cc l \with {
    | inP (U,CU,l<=<U) => \case fl (X.interior {U}) l<=<U \with {
      | inP (N,g) => inP (U, CU, N, \lam p => <=<_<= (g p) idp)
    }
  }

\func limit {I : DirectedSet} {X : CompleteCoverSpace} (f : I -> X) : Partial X \cowith
  | isDefined => IsConvergent f
  | value fc => completion-lift fc infPoint
  \where {
    \func infPoint {I : DirectedSet} : Completion (DirectedCoverSpace I)
      => CompleteCoverSpace.filter-point $ completion.func-cauchy EventualityFilter

    \protected \lemma char (fc : CoverMap (DirectedCoverSpace I) X)
      : limit fc fc = CompleteCoverSpace.filter-point (fc.func-cauchy EventualityFilter)
      => completion-lift-natural EventualityFilter
  }

\lemma limit-isLimit {I : DirectedSet} {X : CompleteCoverSpace} {f : I -> X} {fc : IsConvergent f} : X.IsLimit f (limit f fc)
  => rewrite (limit.char fc) \lam Uo Ul => CompleteCoverSpace.filter-point-sub (X.open-char. Uo Ul)

\lemma limit-char {I : DirectedSet} {X : CompleteCoverSpace} {f : I -> X} {l : X} : (limit f = defined l) <-> X.IsLimit f l
  => (\lam p => rewriteI (defined-ext.value {_} {limit f} p) limit-isLimit,
      \lam fl => defined-ext {_} {limit f} (limit-conv fl) $ inv $ isSeparatedCoverSpace $ SeparatedCoverSpace.separated-char   \lam {U} l<=<U => \case <=<-inter l<=<U \with {
        | inP (U',l<=<U',U'<=<U) => \case fl X.interior l<=<U' \with {
          | inP (N,g) => transportInv U (limit.char (limit-conv fl)) $ <=<_<= (CompleteCoverSpace.filter-point-elem U'<=<U $ inP $ later (N, \lam p => <=<_<= (g p) idp)) idp
        }
      })

\lemma limit-apply {I : DirectedSet} {X Y : CompleteCoverSpace} {f : I -> X} {fc : IsConvergent f} {g : X -> Y} (gc : CoverMap X Y g)
  : g (limit f fc) = limit (\lam i => g (f i)) (gc CoverMap.∘ fc)
  => Y.limit-unique (cont-limit limit-isLimit gc) limit-isLimit

\lemma limit-ext {I : DirectedSet} {X : CompleteCoverSpace} (f g : I -> X) {fc : IsConvergent f} {gc : IsConvergent g} (p : \Pi (i : I) -> f i = g i) : limit f fc = limit g gc
  => X.limit-unique limit-isLimit $ transportInv (X.IsLimit __ (limit g gc)) (ext p) limit-isLimit

\lemma convergent-uniform-char {I : DirectedSet} {X : RegularPreuniformSpace} {f : I -> X} (p : ∀ {C : X.isUniform} ∃ (U : C) (N : I) ∀ {n} (N <= n -> U (f n))) : IsConvergent f
  => convergent-char \lam Cc => \case ClosurePrecoverSpace.closure-filter (\new SetFilter X {
    | F U => ∃ (N : I) ∀ {n} (N <= n -> U (f n))
    | filter-mono (inP (N,g)) p => inP (N, \lam q => p (g q))
    | filter-top => \case I.isInhabitted \with {
      | inP N => inP (N, \lam _ => ())
    }
    | filter-meet (inP (N,g)) (inP (M,h)) => \case isDirected N M \with {
      | inP (L,N<=L,M<=L) => inP (L, \lam L<=n => (g $ N<=L <=∘ L<=n, h $ M<=L <=∘ L<=n))
    }
  }) (\lam Cu => \case p Cu \with {
    | inP (U,CU,N,g) => inP (U, CU, inP (N,g))
  }) (uniform-cauchy. Cc) \with {
    | inP (U, CU, inP (N,g)) => inP (U, CU, N, g)
  }
  \where
    \protected \lemma conv {I : DirectedSet} {X : RegularPreuniformSpace} {f : I -> X} (fc : IsConvergent f) : ∀ {C : X.isUniform} ∃ (U : C) (N : I) ∀ {n} (N <= n -> U (f n))
      => \lam Cu => convergent-char.conv fc (X.makeCauchy Cu)

\lemma convergent-topAbGroup-char {I : DirectedSet} {X : TopAbGroup} {f : I -> X} : TFAE (
    IsConvergent f,
    ∀ {U : X.isOpen} (U ) ∃ (N : I) ∀ {n m} (N <= n -> n <= m -> U (f m - f n)),
    ∀ {U : X.isOpen} (U ) ∃ (N : I) ∀ {n} (N <= n -> U (f n - f N))
  ) => TFAE.cycle (
    \lam fc {U} Uo U0 => \case X.shrink Uo U0 \with {
      | inP (V,Vo,V0,g) => \case convergent-uniform-char.conv fc $ X.topAbUniform (negative-cont.func-cont Vo) (simplify V0) \with {
        | inP (_, inP (x, idp), N, h) => inP (N, \lam p q => transport U simplify $ g (h $ p <=∘ q) (h p))
      }
    },
    \lam fc Uo U0 => \case fc Uo U0 \with {
      | inP (N,g) => inP (N, \lam p => g <=-refl p)
    },
    \lam fc => convergent-uniform-char \lam Cu => \case neighborhood-uniform. Cu \with {
      | inP (U,Uo,U0,h) => \case fc (negative-cont.func-cont Uo) (simplify U0) \with {
        | inP (N,g) => \case h (f N) \with {
          | inP (V,CV,UV) => inP (V, CV, N, \lam p => UV $ simplify in g p)
        }
      }
    })

\lemma convergent-metric-char {I : DirectedSet} {X : ExPseudoMetricSpace} {f : I -> X}
  : IsConvergent f <-> ∀ {eps : Rat} ( < eps) ∃ (N : I) ∀ {n} (N <= n -> (dist (f n) (f N)).U eps)
  => (\lam fc eps>0 => \case convergent-uniform-char.conv fc $ X.metricUniform (RatField.half>0 eps>0) \with {
    | inP (_, inP (x, idp), N, g) => inP (N, \lam p => X.halving1/2 (g p) (g <=-refl))
  },
  \lam fc => convergent-uniform-char \lam Cu => \case X.dist-uniform. Cu \with {
    | inP (eps,eps>0,h) => \case fc eps>0 \with {
      | inP (N,g) => \case h (f N) \with {
        | inP (V,CV,dV) => inP (V, CV, N, \lam p => dV $ rewrite X.dist-symm $ g p)
      }
    }
  })
  \where {
    \protected \lemma double (fc : IsConvergent f) {eps : Rat} (eps>0 :  < eps) : ∃ (N : I) ∀ {n m} (N <= n -> N <= m -> (dist (f n) (f m)).U eps)
      => \case convergent-metric-char. fc (RatField.half>0 eps>0) \with {
        | inP (N,h) => inP (N, \lam N<=n N<=m => X.halving1/2 (rewrite dist-symm in h N<=n) (rewrite dist-symm in h N<=m))
      }
  }

\lemma convergent-metric-real {I : DirectedSet} {X : PseudoMetricSpace} {f : I -> X}
  : IsConvergent f <-> ∀ {eps : Real} ( < eps) ∃ (N : I) ∀ {n} (N <= n -> X.dist (f n) (f N) < eps)
  => <->trans convergent-metric-char $ later (\lam fc eps>0 => \case real_<-rat-char. eps>0 \with {
    | inP (eps',eps'>0,eps'<eps) => \case fc eps'>0 \with {
      | inP (N,h) => inP (N, \lam p => real_<_U. (h p) <∘ real_<_L. eps'<eps)
    }
  }, \lam fc eps>0 => \case fc (rat_real_<. eps>0) \with {
    | inP (N,h) => inP (N, \lam p => real_<_U. $ h p)
  })

\lemma limit-metric-char {I : DirectedSet} {X : ExPseudoMetricSpace} {f : I -> X} {l : X}
  : X.IsLimit f l <-> ∀ {eps} ( < eps) ∃ (N : I) ∀ {n} (N <= n -> (dist l (f n)).U eps)
  => (\lam fl eps>0 => fl OBall-open (OBall-center eps>0),
      \lam fl Uo U0 => \case dist_open. Uo U0 \with {
        | inP (eps,eps>0,q) => \case fl eps>0 \with {
          | inP (N,g) => inP (N, \lam p => q (g p))
        }
      })

\lemma nat-limit-metric {X : ExPseudoMetricSpace} {f : Nat -> X} {l : X} (fb : (dist l (f )).IsBounded) {d : ExUpperReal} (d>=0 :  <= d) (d<1 : d.U ) (dp : \Pi (n : Nat) -> dist l (f (suc n)) <= d * dist l (f n)) : X.IsLimit f l \elim fb
  | inP (B,lf0<B) => \case U-rounded d<1 \with {
    | inP (q,d<q,q<1) => limit-metric-char. \lam {eps} eps>0 =>
      \have N => rat_<1_pow-bound q<1 {eps * RatField.finv B} $ RatField.<_*_positive_positive eps>0 $ RatField.finv>0 $ dist>=0 lf0<B
      \in inP (N., \lam {n} p => induction lf0<B {q} (<=-less $ d>=0 d<q) (\lam k => dp k <=∘ ExUpperRealSemigroup.<=_* (ExUpperReal.<_<= d<q) <=-refl) n $ RatField.<=_*_positive-left (RatField.pow_<=-degree (<=-less $ d>=0 d<q) (<=-less q<1) p) (<=-less $ dist>=0 lf0<B) <∘r RatField.<_rotate-right-conv (dist>=0 lf0<B) N.)
  }
  \where {
    \private \lemma induction {B : Rat} (fB : (dist l (f )).U B) {q : Rat} (q>=0 :  <= q) (dq : \Pi (n : Nat) -> dist l (f (suc n)) <= ExUpperReal.fromRat q * dist l (f n)) (n : Nat) : dist l (f n) <= RatField.pow q n * B \elim n
      |  => ExUpperReal.<_<= fB <=∘ =_<= (inv $ pmap ExUpperReal.fromRat ide-left)
      | suc n => dq n <=∘ ExUpperRealSemigroup.<=_* <=-refl (induction fB q>=0 dq n) <=∘ =_<= (ExUpperReal.*-rat q>=0 (RatField.<=_*-positive (RatField.pow>=0 q>=0) $ <=-less $ dist>=0 fB) *> pmap ExUpperReal.fromRat (inv *-assoc *> pmap (`* B) RatField.pow-left))
  }

\lemma limit-metric-real {I : DirectedSet} {X : PseudoMetricSpace} {f : I -> X} {l : X}
  : X.IsLimit f l <-> ∀ {eps} ( < eps) ∃ (N : I) ∀ {n} (N <= n -> X.dist l (f n) < eps)
  => <->trans limit-metric-char $ later (\lam fc eps>0 => \case real_<-rat-char. eps>0 \with {
    | inP (eps',eps'>0,eps'<eps) => \case fc eps'>0 \with {
      | inP (N,h) => inP (N, \lam p => real_<_U. (h p) <∘ real_<_L. eps'<eps)
    }
  }, \lam fc eps>0 => \case fc (rat_real_<. eps>0) \with {
    | inP (N,h) => inP (N, \lam p => real_<_U. $ h p)
  })

\lemma convergent-compose {I : DirectedSet} {X Y : CoverSpace} {f : I -> X} (fc : IsConvergent f) (g : CoverMap X Y) : IsConvergent \lam n => g (f n)
  => g CoverMap.∘ fc

\func SubPointDirectedSet {X : TopSpace} {U : Set X} (a : X) (Ua : X.IsLimitPoint a U) : DirectedSet \cowith
  | E => Given (V : isOpen) (V a) (x : X) (V x) (U x)
  | <= S T => T. ⊆ S.
  | <=-refl => <=-refl
  | <=-transitive p q => q <=∘ p
  | isInhabitted => \case Ua open-top () \with {
    | inP (x,Ux,_) => inP (top, open-top, (), x, (), Ux)
  }
  | isDirected (V,Vo,Va,_,_,_) (W,Wo,Wa,_,_,_) => \case Ua (open-inter Vo Wo) (Va,Wa) \with {
    | inP (z,Uz,(Vz,Wz)) => inP ((V ∧ W, open-inter Vo Wo, (Va,Wa), z, (Vz,Wz), Uz), meet-left, meet-right)
  }
  \where {
    \lemma limit-comp {I : DirectedSet} {X Y : TopSpace} {S : Set X} {lx : X} (Sa : X.IsLimitPoint lx S)
                      {f : I -> X} (Sf : \Pi (n : I) -> S (f n)) (fl : X.IsLimit f lx) {g : Set.Total S -> Y}
                      {ly : Y} (gl : Y.IsLimit {SubPointDirectedSet lx Sa} (\lam h => g (h.,h.)) ly) : Y.IsLimit (\lam n => g (f n, Sf n)) ly
      => \lam Vo Vly => \case (limit-char Sa \lam s => g (s.,s.)). gl Vo Vly \with {
        | inP (U,Uo,Ulx,e) => \case fl Uo Ulx \with {
          | inP (N,d) => inP (N, \lam {n} p => e (d p) (Sf n))
        }
      }

    \protected \func map {X Y : TopSpace} (f : ContMap X Y) (g : Y -> X) (h : \Pi (y : Y) -> f (g y) = y) (a : Y)
                         {U : Set Y} (Ua : Y.IsLimitPoint a U) {b : X} (p : g a = b) {V : Set X} (Vb : X.IsLimitPoint b V)
                         (UV : \Pi {y : Y} -> U y -> V (g y)) (d : SubPointDirectedSet a Ua) : SubPointDirectedSet b Vb
      => (f ^-1 d., f.func-cont d., transportInv d. (pmap f (inv p) *> h a) d., g d., transportInv d. (h d.) d., UV d.)

    \lemma limit-id {X : TopSpace} {U : Set X} {a : X} (Ua : X.IsLimitPoint a U) : X.IsLimit {SubPointDirectedSet a Ua} (\lam h => h.) a
      => \lam {V} Vo Va => \case Ua Vo Va \with {
        | inP (b,Ub,Vb) => inP ((V, Vo, Va, b, Vb, Ub), \lam {h} p => p h.)
      }

    \lemma limit-char {X Y : TopSpace} {S : Set X} {a : X} (Sa : X.IsLimitPoint a S) (f : (\Sigma (x : X) (S x)) -> Y) {y : Y}
      : Y.IsLimit {SubPointDirectedSet a Sa} (\lam h => f (h.,h.)) y <-> ∀ {V : Y.isOpen} (V y) ∃ (U : X.isOpen) (Ua : U a) ∀ {h : U} (Sh : S h) (V (f (h,Sh)))
      => (\lam fc {V} Vo Vy => \case fc Vo Vy \with {
        | inP ((U,Uo,Ua,_,_,_),g) => inP (U, Uo, Ua, \lam {h} Uh Sh => g {U,Uo,Ua,h,Uh,Sh} <=-refl)
      }, \lam fc {V} Vo Vy => \case fc Vo Vy \with {
        | inP (U,Uo,Ua,g) => \case Sa Uo Ua \with {
          | inP (b,Sb,Ub) => inP ((U,Uo,Ua,b,Ub,Sb), \lam {h} p => g (p h.) h.)
        }
      })
  }

\func InvDirectedSet {R : NearSkewField} {S : Set R} (So : isOpen S) (S0 : S ) : DirectedSet
  => SubPointDirectedSet {R} {(\lam h => Monoid.Inv h) ∧ S}  (aux So S0)
  \where {
    \private \lemma aux (So : isOpen S) (S0 : S ) : R.IsLimitPoint  ((\lam h => Monoid.Inv h) ∧ S)
      => \lam Vo V0 => \case inv-dense (open-inter So Vo) (S0,V0) \with {
        | inP (y,yi,(Sy,Vy)) => inP (y,(yi,Sy),Vy)
      }

    \lemma limit-id (So : isOpen S) (S0 : S ) : R.IsLimit {InvDirectedSet So S0} (\lam h => h.) 
      => SubPointDirectedSet.limit-id (aux So S0)

    \lemma limit-char {Y : TopSpace} (So : isOpen S) (S0 : S ) {f : \Pi (h : Monoid.Inv {R}) -> S h -> Y} {y : Y}
      : Y.IsLimit {InvDirectedSet So S0} (\lam h => f h.. h..) y <-> ∀ {V : Y.isOpen} (V y) ∃ (U : R.isOpen) (Ua : U ) ∀ {h : U} (s : \Sigma (Monoid.Inv h) (S h)) (V (f s. s.))
      => SubPointDirectedSet.limit-char (aux So S0) \lam h => f h.. h..
  }