\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Pointed
\import Arith.Rat
\import Arith.Real
\import Arith.Real.UpperReal
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Operations
\import Order.Biordered
\import Order.Lattice
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set.Subset
\import Topology.CoverSpace
\import Topology.MetricSpace
\import Topology.TopAbGroup
\import Topology.TopAbGroup.Complete
\import Topology.UniformSpace
\import Topology.UniformSpace.Product
\open RatField(half,half>0)

\class ExPseudoNormedAbGroup \extends ExPseudoMetricSpace, TopAbGroup {
  | norm : E -> ExUpperReal
  | norm_zro : norm zro = 
  | norm_negative {x : E} : norm (negative x) = norm x
  | norm_+ {x y : E} : norm (x + y) <= norm x ExUpperReal.+ norm y
  | norm-dist {x y : E} : dist x y = norm (x - y)

  | +-cont => \new UniformMap (ProductUniformSpace \this \this) \this {
    | func s => s. + s.
    | func-uniform Eu => \case dist-uniform. Eu \with {
      | inP (eps,eps>0,h) => inP (_, metricUniform $ half>0 eps>0, _, metricUniform $ half>0 eps>0, \lam (inP (_, inP (x,idp), _, inP (y,idp), p)) => \case h (x + y) \with {
        | inP (V,EV,g) => inP (_, inP (V, EV, idp), rewrite p \lam {(x',y')} (xx'<eps/2,yy'<eps/2) => g $ rewrite (norm-dist, equation.abGroup : x + y - (x' + y') = x - x' + (y - y')) $ ExUpperReal.U_<= (ExUpperReal.<=_+-char norm_+ (rewrite norm-dist in xx'<eps/2) (rewrite norm-dist in yy'<eps/2)) linarith
        )
      })
    }
  }
  | negative-cont => \new UniformMap {
    | func-uniform Eu => \case dist-uniform. Eu \with {
      | inP (eps,eps>0,h) => dist-uniform. $ inP (eps, eps>0, \lam x => \case h (negative x) \with {
        | inP (U,EU,g) => inP (_, inP $ later (U,EU,idp), \lam {y} d => g {negative y} $ transportInv (ExUpperReal.U {__} eps) (norm-dist *> simplify (pmap norm +-comm) *> norm_negative *> inv norm-dist) d)
      })
    }
  }
  | neighborhood-uniform =>
    \have lem {x} {y} : dist  (x - y) = dist x y => norm-dist *> inv norm_negative *> pmap norm simplify *> inv norm-dist
    \in (\lam Cu => \case dist-uniform. Cu \with {
      | inP (eps,eps>0,h) => inP (OBall eps , OBall-open, OBall-center eps>0, \lam x => \case h x \with {
        | inP (U,CU,g) => inP (U, CU, \lam d => g $ transport (ExUpperReal.U {__} eps) lem d
                              )
      })
    }, \lam (inP (U,Uo,U0,h)) => \case dist_open. Uo U0 \with {
      | inP (eps,eps>0,p) => dist-uniform. $ inP (eps, eps>0, \lam x => \case h x \with {
        | inP (U,CU,g) => inP (U, CU, \lam d => g $ p $ transportInv (ExUpperReal.U {__} eps) lem d)
      })
    })
  | open-top => defaultImpl PrecoverSpace open-top
  | open-inter {U} {V} => defaultImpl PrecoverSpace open-inter {_} {U} {V}
  | open-Union {S} => defaultImpl PrecoverSpace open-Union {_} {S}

  \default dist x y : ExUpperReal => norm (x - y)
  \default norm-dist \as norm-dist-impl {x} {y} : dist x y = norm (x - y) => idp

  \default norm_zro => inv (norm-dist *> pmap norm (pmap (zro +) negative_zro *> zro-right)) *> dist-refl
  \default norm_negative => pmap norm (inv zro-left) *> inv norm-dist *> dist-symm *> norm-dist *> pmap norm (pmap (_ +) negative_zro *> zro-right)
  \default norm_+ => transport (\lam z => norm (_ + z) <= _) negative-isInv $ =_<= (inv norm-dist) <=∘ dist-triang {_} {_} {} <=∘ =_<= (pmap2 (ExUpperReal.+) (norm-dist *> pmap norm (pmap (_ +) negative_zro *> zro-right)) (norm-dist *> pmap norm (pmap ( +) negative-isInv *> zro-left)))

  \default dist-refl => norm-dist *> pmap norm negative-right *> norm_zro
  \default dist-symm => norm-dist *> simplify *> norm_negative *> inv norm-dist
  \default dist-triang => repeat {} (rewrite norm-dist) $ transport (norm __ <= _) simplify norm_+

  \lemma norm_*n_<=_*n {n : Nat} {a : E} : norm (n *n a) <= n ExUpperRealAbMonoid.*n norm a \elim n
    |  => =_<= norm_zro
    | suc n => norm_+ <=∘ <=_+ norm_*n_<=_*n <=-refl

  \lemma norm_*n_<= {n : Nat} {a : E} : norm (n *n a) <= n ExUpperReal.* norm a
    => norm_*n_<=_*n <=∘ ExUpperRealSemigroup.*n_*_<= norm>=0

  \func IsUnbounded : \Prop
    => \Pi (B : Nat) -> ∃ (x : E) (ExUpperReal.fromRat B <= norm x)

  \lemma norm_BigSum {l : Array E} : norm (BigSum l) <= ExUpperRealAbMonoid.BigSum \lam j => norm (l j) \elim l
    | nil => transportInv (`<= _) norm_zro <=-refl
    | x :: l => norm_+ <=∘ <=_+ <=-refl norm_BigSum
}

\lemma norm>=0 {X : ExPseudoNormedAbGroup} {x : X} :  <= norm x
  => rewrite norm_dist dist>=0

\lemma norm_dist {X : ExPseudoNormedAbGroup} {x : X} : norm x = dist  x
  => inv norm_negative *> simplify *> inv norm-dist

\lemma norm_- {X : ExPseudoNormedAbGroup} {x y : X} : norm (x - y) = norm (y - x)
  => pmap norm (inv X.negative-isInv) *> norm_negative *> simplify

\lemma norm_dist-left {X : ExPseudoNormedAbGroup} {x y : X} : norm x <= dist x y + norm y
  => rewrite norm-dist $ transport (norm  __ <= _) simplify norm_+

\lemma norm_dist-right {X : ExPseudoNormedAbGroup} {x y : X} : norm x <= norm y + dist x y
  => rewrite norm-dist $ transport (norm  __ <= _) simplify norm_+

\class ExNormedAbGroup \extends ExPseudoNormedAbGroup, ExMetricSpace {
  | norm-ext {x : E} : norm x = ExUpperRealAbMonoid.zro -> x = 

  \default dist-ext p => fromZero $ norm-ext $ inv norm-dist *> p
  \default norm-ext p => dist-ext $ norm-dist *> pmap norm (pmap (_ +) negative_zro *> zro-right) *> p
}

\class BoundedExPseudoNormedAbGroup \extends ExPseudoNormedAbGroup
  | norm-bounded (x : E) : (norm x).IsBounded

\func bnorm {X : BoundedExPseudoNormedAbGroup} (x : X) : UpperReal \cowith
  | ExUpperReal => norm x
  | U-inh => norm-bounded x

\class PseudoNormedAbGroup \extends BoundedExPseudoNormedAbGroup, PseudoMetricSpace {
  \override norm : E -> Real
  \default dist x y : Real => norm (x - y)
  \default norm-dist \as norm-dist-impl {x} {y} : dist x y = norm (x - y) => idp
  | norm-bounded x => U-inh
}

\func lnorm {X : PseudoNormedAbGroup} (x : X) : Real
  => X.norm x

\lemma lnorm>=0 {X : PseudoNormedAbGroup} {x : X} :  <= X.norm x
  => Real.<=-upper. (later norm>=0)

\lemma lnorm_zro {X : PseudoNormedAbGroup} : lnorm X.zro = RealAbGroup.zro
  => Real.=-upper. (later norm_zro)

\lemma lnorm_+ {X : PseudoNormedAbGroup} {x y : X} : lnorm (x + y) <= lnorm x + lnorm y
  => Real.<=-upper. $ transportInv (_ ExUpperRealAbMonoid.<=) RealAbGroup.+-upper X.norm_+

\lemma lnorm-ldist {X : PseudoNormedAbGroup} {x y : X} : ldist x y = lnorm (x - y)
  => Real.=-upper. (later norm-dist)

\lemma lnorm_BigSum {X : PseudoNormedAbGroup} {l : Array X} : lnorm (X.BigSum l) <= RealAbGroup.BigSum \lam j => lnorm (l j) \elim l
  | nil => transportInv (`<= _) lnorm_zro <=-refl
  | x :: l => lnorm_+ <=∘ <=_+ <=-refl lnorm_BigSum

\lemma lnorm_- {X : PseudoNormedAbGroup} {x y : X} : lnorm (x - y) = lnorm (y - x)
  => Real.=-upper. $ norm_- {X}

\lemma lnorm_-left {X : PseudoNormedAbGroup} {x y : X} : lnorm x - lnorm y <= lnorm (x - y)
  => transport (_ <=) (+-assoc *> pmap (_ +) negative-right *> zro-right) $ <=_+ (transport (lnorm __ <= _) (+-assoc *> pmap (x +) negative-left *> zro-right) lnorm_+) <=-refl

\lemma lnorm_-right {X : PseudoNormedAbGroup} {x y : X} : lnorm y - lnorm x <= lnorm (x - y)
  => transport (_ <=) lnorm_- lnorm_-left

\lemma lnorm_-_abs {X : PseudoNormedAbGroup} {x y : X} : RealAbGroup.abs (lnorm x - lnorm y) <= lnorm (x - y)
  => join-univ lnorm_-left (simplify lnorm_-right)

\class NormedAbGroup \extends PseudoNormedAbGroup, ExNormedAbGroup

\record UniformNormedAbGroupMap \extends UniformMetricMap, TopAbGroupMap {
  \override Dom : ExPseudoNormedAbGroup
  \override Cod : ExPseudoNormedAbGroup

  | func-norm-uniform : ∀ {eps : Rat} ( < eps) ∃ (delta : Rat) ( < delta) ∀ {x : Dom} ((norm x).U delta -> (norm (func x)).U eps)
  | func-dist-uniform eps>0 => \case func-norm-uniform eps>0 \with {
    | inP (delta,delta>0,h) => inP (delta, delta>0, unfold \lam d => rewrite (norm-dist {Cod}, inv AddGroupHom.func-minus) $ h $ rewriteI (norm-dist {Dom}) d)
  }

  \default func-norm-uniform eps>0 => \case dist_open. (func-cont OBall-open) $ rewrite func-zro $ OBall-center eps>0 \with {
    | inP (delta,delta>0,h) => inP (delta, delta>0, \lam d => rewrite (norm_dist {Cod}, inv func-zro) $ h $ rewrite (norm_dist {Dom}) in d)
  }
}

\record NormedAbGroupMap \extends UniformNormedAbGroupMap, MetricMap {
  \override Dom : ExPseudoNormedAbGroup
  \override Cod : ExPseudoNormedAbGroup

  | func-norm {x : Dom} : norm (func x) <= norm x
  | func-norm-uniform {eps} eps>0 => inP (eps, eps>0, func-norm __)
  | func-dist => unfold $ rewrite (norm-dist {Dom}, norm-dist {Cod}, inv AddGroupHom.func-minus) func-norm
}

\record NormedIsometricMap \extends NormedAbGroupMap, IsometricMap {
  \override Dom : ExPseudoNormedAbGroup
  \override Cod : ExPseudoNormedAbGroup

  | func-norm-isometry {x : Dom} : norm (func x) = norm x
  | func-norm => =_<= func-norm-isometry

  \default func-isometry => norm-dist *> pmap norm (inv func-minus) *> func-norm-isometry *> inv norm-dist
  \default func-norm-isometry => norm_dist *> pmap (dist __ _) (inv func-zro) *> func-isometry *> inv norm_dist
}

\class CompleteExNormedAbGroup \extends ExNormedAbGroup, CompleteExMetricSpace, CompleteTopAbGroup

\class CompleteNormedAbGroup \extends CompleteExNormedAbGroup, NormedAbGroup, CompleteMetricSpace

-- | A bilinear map bounded by the product of norms is locally uniform.
\lemma bilinear-locally-uniform {A B : BoundedExPseudoNormedAbGroup} {C : ExPseudoNormedAbGroup} (f : A -> B -> C)
                                (fl : \Pi {a a' : A} {b : B} -> f (a - a') b = f a b - f a' b)
                                (fr : \Pi {a : A} {b b' : B} -> f a (b - b') = f a b - f a b')
                                (norm_*_<= : \Pi {x : A} {y : B} -> norm (f x y) <= norm x * norm y)
  : LocallyUniformMap (A ⨯ B) C (\lam s => f s. s.)
  => LocallyUniformMetricMap.makeLocallyUniformMap2 f \lam {eps} eps>0 => inP (, idp, \lam x0 y0 => \case norm-bounded x0, norm-bounded y0 \with {
    | inP (x0b,|x0|<x0b), inP (y0b,|y0|<y0b) => \case ExUpperRealSemigroup.div-lb-rat {(x0b + ) + (y0b +  + )} {Real.fromRat eps} (inP (, idp, <=-rat. $ linarith (norm>=0 |x0|<x0b, norm>=0 |y0|<y0b))) (<-rat. eps>0) \with {
      | inP (gamma,gamma>0,gamma-m) => inP (gamma ∧ , <_meet-univ gamma>0 RatField.zro<ide, \lam {x} {x'} {y} {y'} x0x<1 y0y<1 xx'<gamma yy'<gamma =>
        rewrite norm-dist at xx'<gamma $ rewrite norm-dist at yy'<gamma $ rewrite norm-dist at x0x<1 $ rewrite norm-dist at y0y<1 $ rewrite norm-dist $
        <-rat. $ transport (norm __ < eps) (pmap2 (+) fr fl *> simplify : f x (y - y') + f (x - x') y' = f x y - f x' y') $ norm_+ <∘r
          <=_+ norm_*_<= norm_*_<= <∘r transport (_ + __ < _) *-comm (<=_+ (ExUpperRealSemigroup.<=_* <=-refl $ <=-less $ <-rat. yy'<gamma) (ExUpperRealSemigroup.<=_* <=-refl (<=-less $ <-rat. xx'<gamma)) <∘r
          transport (`< _) (ExUpperRealSemigroup.rdistr norm>=0 norm>=0) (ExUpperRealSemigroup.<=_* <=-refl (<=-rat. meet-left) <∘r ExUpperRealSemigroup.<_*-left' (
            \have lem {X : ExPseudoNormedAbGroup} {x1 x2 : X} (d : (norm (x1 - x2)).U ) : norm x2 <= norm x1 +  => transport (_ <= _ + __) norm_- (=_<= (pmap norm equation.abGroup) <=∘ norm_+) <=∘ <=_+ <=-refl (<=-less $ <-rat. d)
            \in <=_+ (lem x0x<1) (lem (U_<= yy'<gamma meet-right) <=∘ <=_+ (lem y0y<1) <=-refl) <∘r transport (_ <) +-rat (<_+ (transport (_ <) +-rat $ <_+-left $ <-rat. |x0|<x0b) $ transport (_ < ) +-rat $ <_+-left $ transport (_ <) +-rat $ <_+-left $ <-rat. |y0|<y0b)) (ExUpperRealAbMonoid.<=_+-positive norm>=0 norm>=0) gamma>0 <∘l gamma-m)))
    }
  })
  \where {
    \open ExUpperReal(<=-rat,+-rat,U_<=)
    \open ExUpperRealAbMonoid(<-rat,<_+,<_+-left)
  }