\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.StrictlyOrdered
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\import Arith.Real.UpperReal
\import Function.Meta
\import Logic
\import Meta
\import Operations
\import Order.Biordered
\import Order.Lattice
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Topology.CoverSpace.Complete
\import Topology.MetricSpace
\import Topology.MetricSpace.ManhattanProduct
\import Topology.MetricSpace.UpperReal
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.Real
\import Topology.UniformSpace
\import Topology.UniformSpace.Product

\lemma lnorm-metric {X : PseudoNormedAbGroup} : MetricMap X RealNormed X.norm \cowith
  | func-dist => rewrite (X.norm-dist,RealNormed.norm-dist) $ Real.<=-upper. $ join-univ lnorm_-left $ simplify lnorm_-right

\lemma dist-uniform-map {X : ExPseudoMetricSpace} : UniformMap (X ⨯ X) ExUpperRealMetric (\lam s => dist s. s.) \cowith
  | func-uniform Eu => \case dist-uniform. Eu \with {
    | inP (eps,eps>0,h) => inP (_, X.metricUniform {eps * ratio  } linarith, _, X.metricUniform {eps * ratio  } linarith, \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (X.dist x x') \with {
      | inP (W,EW,g) => inP (_, inP (W, EW, idp), \lam {(y,y')} (xy<eps/4,x'y'<eps/4) => g $ inP (eps * ratio   + eps * ratio  , linarith, linarith,
          X.dist-triang <=∘ transport (`<= _) +-comm (<=_+ X.dist-triang <=-refl <=∘ transportInv (`<= _) +-assoc (<=_+ <=-refl $ transport (_ <=) ExUpperReal.+-rat $ <=-less $ ExUpperRealAbMonoid.<_+ (transport (`< _) dist-symm $ ExUpperRealAbMonoid.<-rat. x'y'<eps/4) (ExUpperRealAbMonoid.<-rat. xy<eps/4))),
          X.dist-triang <=∘ transport (`<= _) +-comm (<=_+ X.dist-triang <=-refl <=∘ transportInv (`<= _) +-assoc (<=_+ <=-refl $ transport (_ <=) ExUpperReal.+-rat $ <=-less $ ExUpperRealAbMonoid.<_+ (ExUpperRealAbMonoid.<-rat. x'y'<eps/4) (transport (`< _) dist-symm $ ExUpperRealAbMonoid.<-rat. xy<eps/4)))))
    })
  }

\lemma norm-metric-map {X : ExPseudoNormedAbGroup} : MetricMap X ExUpperRealMetric norm \cowith
  | func-dist => \lam xy<b => \case U-rounded xy<b \with {
    | inP (a,xy<a,a<b) => inP (a, a<b, <=-less $ dist>=0 xy<a, norm_dist-right <=∘ <=_+ <=-refl (ExUpperReal.<_<= xy<a), norm_dist-right <=∘ <=_+ <=-refl (rewrite dist-symm $ ExUpperReal.<_<= xy<a))
  }

\lemma bnorm-metric-map {X : BoundedExPseudoNormedAbGroup} : MetricMap X UpperRealMetric bnorm \cowith
  | func-dist => norm-metric-map.func-dist

\lemma ldist-uniform-map {X : PseudoMetricSpace} : UniformMap (X ⨯ X) RealNormed (\lam s => X.dist s. s.) \cowith
  | func-uniform Eu => \case dist-uniform. Eu \with {
    | inP (eps,eps>0,h) => inP (_, X.metricUniform (RatField.half>0 eps>0), _, X.metricUniform (RatField.half>0 eps>0), \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (X.dist x x') \with {
      | inP (W,EW,g) => inP (_, inP (W, EW, idp), \lam {(y,y')} (xy<eps/2,x'y'<eps/2) => g $ real_<_U. $ <_join-univ
          (linarith (real_<_U. xy<eps/2, real_<_U. x'y'<eps/2, RealAbGroup.half+half, ldist-triang {X} {x} {y} {x'}, ldist-triang {X} {y} {y'} {x'}, ldist-symm {X} {x'} {y'}))
          (linarith (real_<_U. xy<eps/2, real_<_U. x'y'<eps/2, RealAbGroup.half+half, ldist-triang {X} {y} {x} {y'}, ldist-triang {X} {x} {x'} {y'}, ldist-symm {X} {x} {y})))
    })
  }

\lemma upper-meet-uniform : UniformMap (ExUpperRealMetric ⨯ ExUpperRealMetric) ExUpperRealMetric \lam s => s. ∧ s. \cowith
  | func-uniform Eu => \case dist-uniform. Eu \with {
    | inP (eps,eps>0,h) => inP (_, ExUpperRealMetric.metricUniform eps>0, _, ExUpperRealMetric.metricUniform eps>0, \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (x ∧ x') \with {
      | inP (W,EW,g) => inP (_, inP (W,EW,idp), \lam {(y,y')} (inP (a,a<eps,a>=0,x<=y+a,y<=x+a), inP (b,b<eps,b>=0,x'<=y'+b,y'<=x'+b)) => g $ inP (a ∨ b, <_join-univ a<eps b<eps, a>=0 <=∘ join-left,
          transportInv (_ <=) meet_+-right $ meet-univ (meet-left <=∘ x<=y+a <=∘ <=_+ <=-refl (ExUpperReal.<=-rat. join-left)) (meet-right <=∘ x'<=y'+b <=∘ <=_+ <=-refl (ExUpperReal.<=-rat. join-right)),
          transportInv (_ <=) meet_+-right $ meet-univ (meet-left <=∘ y<=x+a <=∘ <=_+ <=-refl (ExUpperReal.<=-rat. join-left)) (meet-right <=∘ y'<=x'+b <=∘ <=_+ <=-refl (ExUpperReal.<=-rat. join-right))))
    })
  }

\lemma real-meet-uniform : UniformMap (RealNormed ⨯ RealNormed) RealNormed \lam s => s. ∧ s. \cowith
  | func-uniform Eu => \case dist-uniform. Eu \with {
    | inP (eps,eps>0,h) => inP (_, RealNormed.metricUniform eps>0, _, RealNormed.metricUniform eps>0, \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (x ∧ x') \with {
      | inP (W,EW,g) => inP (_, inP (W, EW, idp), \lam {(y,y')} (xy<eps,x'y'<eps) => g $ real_<_U. $ RealAbGroup.abs_-_<
          (unfold (-) $ rewrite (RealAbGroup.meet_negative, join_+-left) $ <_join-univ
            (RealAbGroup.<=_+ meet-left <=-refl <∘r RealAbGroup.abs>=id <∘r real_<_U. xy<eps)
            (RealAbGroup.<=_+ meet-right <=-refl <∘r RealAbGroup.abs>=id <∘r real_<_U. x'y'<eps))
          (unfold (-) $ rewrite (RealAbGroup.meet_negative, join_+-left) $ <_join-univ
            (RealAbGroup.<=_+ meet-left <=-refl <∘r RealAbGroup.abs>=_- <∘r real_<_U. xy<eps)
            (RealAbGroup.<=_+ meet-right <=-refl <∘r RealAbGroup.abs>=_- <∘r real_<_U. x'y'<eps)))
    })
  }

\lemma upper-join-uniform : UniformMap (ExUpperRealMetric ⨯ ExUpperRealMetric) ExUpperRealMetric \lam s => s. ∨ s. \cowith
  | func-uniform Eu => \case dist-uniform. Eu \with {
    | inP (eps,eps>0,h) => inP (_, ExUpperRealMetric.metricUniform eps>0, _, ExUpperRealMetric.metricUniform eps>0, \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (x ∨ x') \with {
      | inP (W,EW,g) => inP (_, inP (W,EW,idp), \lam {(y,y')} (inP (a,a<eps,a>=0,x<=y+a,y<=x+a), inP (b,b<eps,b>=0,x'<=y'+b,y'<=x'+b)) => g $ inP (a ∨ b, <_join-univ a<eps b<eps, a>=0 <=∘ join-left,
          join-univ (x<=y+a <=∘ <=_+ join-left (ExUpperReal.<=-rat. join-left)) (x'<=y'+b <=∘ <=_+ join-right (ExUpperReal.<=-rat. join-right)),
          join-univ (y<=x+a <=∘ <=_+ join-left (ExUpperReal.<=-rat. join-left)) (y'<=x'+b <=∘ <=_+ join-right (ExUpperReal.<=-rat. join-right))))
    })
  }

\lemma real-join-uniform : UniformMap (RealNormed ⨯ RealNormed) RealNormed \lam s => s. ∨ s. \cowith
  | func-uniform Eu => \case dist-uniform. Eu \with {
    | inP (eps,eps>0,h) => inP (_, RealNormed.metricUniform eps>0, _, RealNormed.metricUniform eps>0, \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (x ∨ x') \with {
      | inP (W,EW,g) => inP (_, inP (W, EW, idp), \lam {(y,y')} (xy<eps,x'y'<eps) => g $ real_<_U. $ RealAbGroup.abs_-_<
          (unfold (-) $ rewrite (RealAbGroup.join_negative, join_+-right) $ <_join-univ
            (<=_+ <=-refl meet-left <∘r RealAbGroup.abs>=id <∘r real_<_U. xy<eps)
            (<=_+ <=-refl meet-right <∘r RealAbGroup.abs>=id <∘r real_<_U. x'y'<eps))
          (unfold (-) $ rewrite (RealAbGroup.join_negative, join_+-right) $ <_join-univ
            (<=_+ <=-refl meet-left <∘r RealAbGroup.abs>=_- <∘r real_<_U. xy<eps)
            (<=_+ <=-refl meet-right <∘r RealAbGroup.abs>=_- <∘r real_<_U. x'y'<eps)))
    })
  }

\lemma upper-+-uniform : MetricMap (ManhattanProductPseudoMetricSpace ExUpperRealMetric ExUpperRealMetric) ExUpperRealMetric \lam s => s. + s. \cowith
  | func-dist {x} {y} {d} xy<d => \case ExUpperReal.+_U. xy<d \with {
    | inP (a,x1y1<a,b,x2y2<b,a+b<d) => inP (a + b, a+b<d, RatField.<=_+-positive (<=-less $ dist>=0 {ExUpperRealMetric} x1y1<a) (<=-less $ dist>=0 {ExUpperRealMetric} x2y2<b),
        ExUpperRealAbMonoid.<=_+ (ExUpperRealMetric.dist-left x1y1<a) (ExUpperRealMetric.dist-left x2y2<b) <=∘ transport (_ <= _ + __) ExUpperReal.+-rat (=_<= equation.abMonoid),
        ExUpperRealAbMonoid.<=_+  (ExUpperRealMetric.dist-right x1y1<a)  (ExUpperRealMetric.dist-right x2y2<b) <=∘ transport (_ <= _ + __) ExUpperReal.+-rat (=_<= equation.abMonoid))
  }

\lemma upper-*-left-uniform {a : ExUpperReal} (aB : a.IsBounded) : UniformMetricMap ExUpperRealMetric ExUpperRealMetric (a *) \cowith
  | func-dist-uniform {eps} eps>0 => \case \elim aB \with {
    | inP (B,a<B) => inP (RatField.finv (B ∨ ) * eps, RatField.<_*_positive_positive (RatField.finv>0 $ zro<ide <∘l join-right) eps>0, \lam (inP (b,bp,b>=0,x<=x'+b,x'<=x+b)) =>
      \have lem {x x' : ExUpperReal} (x<=x'+b : x <= x' + b) => ExUpperRealSemigroup.<=_* <=-refl x<=x'+b <=∘ ExUpperRealSemigroup.ldistr_<= <=∘ ExUpperRealAbMonoid.<=_+ <=-refl (transport (_ <=) (ExUpperReal.*-rat (<=-less zro<ide <=∘ join-right) b>=0) $ ExUpperRealSemigroup.<=_* (ExUpperReal.<_<= $ ExUpperReal.U_<= a<B join-left) <=-refl)
      \in inP ((B ∨ ) * b, RatField.<_*_positive-right (zro<ide <∘l join-right) bp <∘l =_<= (inv *-assoc *> pmap (`* eps) (RatField.finv-right $ RatField.>_/= $ zro<ide <∘l join-right) *> ide-left), <=_*-positive (<=-less zro<ide <=∘ join-right) b>=0, lem x<=x'+b, lem x'<=x+b))
  }

\lemma upper-*-right-uniform {a : ExUpperReal} (aB : a.IsBounded) : UniformMetricMap ExUpperRealMetric ExUpperRealMetric (`* a)
  => transport (UniformMetricMap ExUpperRealMetric ExUpperRealMetric) (ext \lam b => *-comm) (upper-*-left-uniform aB)

\lemma upper-*-locally-uniform : LocallyUniformMap (ManhattanProductPseudoMetricSpace UpperRealMetric UpperRealMetric) UpperRealMetric (\lam s => s. * s.)
  => LocallyUniformMetricMap.makeLocallyUniformMap2 (*) \lam {eps} eps>0 => inP (, idp, \lam x0 y0 => \case x0.U-inh_>0, y0.U-inh_>0 \with {
    | inP (x0b,x0<x0b,x0b>0), inP (y0b,y0<y0b,y0b>0) => \case ExUpperRealSemigroup.div-lb-rat {(y0b +  + ) + (x0b +  + )} (inP (, idp, <=-rat. linarith)) $ <-rat. (RatField.half>0 eps>0) \with {
      | inP (gamma,gamma>0,gamma-m) => inP (gamma ∧ , <_meet-univ gamma>0 zro<ide, \lam {x} {x'} {y} {y'} (inP x0x<1) (inP y0y<1) (inP xx'<gamma) (inP yy'<gamma) =>
        \have | x<=x0b+1 => transport (_ <=) +-rat $ x0x<1. <=∘ <=_+ (<_<= x0<x0b) (<=-rat. (<=-less x0x<1.))
              | y<=y0b+1 : y ExUpperReal.<= y0b +  => transport (_ <=) +-rat $ y0y<1. <=∘ <=_+ (<_<= y0<y0b) (<=-rat. (<=-less y0y<1.))
        \in transport (ExUpperReal.`<= _) (pmap (ExUpperReal.`* _) (inv +-rat) *> ExUpperRealSemigroup.rdistr (<=-rat. linarith) (<=-rat. linarith)) at gamma-m $
            unfold $ rewrite (UpperRealSemigroup.*-ex,UpperRealSemigroup.*-ex) $ inP (RatField.half eps, RatField.half<id eps>0, <=-less $ RatField.half>0 eps>0,
              <=_* <=-refl yy'<gamma. <=∘ ldistr_<= <=∘ <=_+ (<=_* xx'<gamma. <=-refl <=∘ rdistr_<=) <=-refl <=∘ =_<= +-assoc <=∘ <=_+ <=-refl (<=_+ (=_<= *-comm <=∘ <=_* (transport (_ <=) +-rat $ yy'<gamma. <=∘ <=_+ y<=y0b+1 (<=-rat. $ <=-less yy'<gamma. <=∘ meet-right)) (<=-rat. $ <=-less xx'<gamma. <=∘ meet-left)) (<=_* (x<=x0b+1 <=∘ <=-rat. linarith) (<=-rat. $ <=-less yy'<gamma. <=∘ meet-left)) <=∘ gamma-m),
              <=_* <=-refl yy'<gamma. <=∘ ldistr_<= <=∘ <=_+ (<=_* xx'<gamma. <=-refl <=∘ rdistr_<=) <=-refl <=∘ =_<= +-assoc <=∘ <=_+ <=-refl (<=_+ (=_<= *-comm <=∘ <=_* (y<=y0b+1 <=∘ <=-rat. linarith) (<=-rat. $ <=-less xx'<gamma. <=∘ meet-left)) (<=_* (transport (_ <=) +-rat $ xx'<gamma. <=∘ <=_+ x<=x0b+1 (<=-rat. $ <=-less xx'<gamma. <=∘ meet-right)) (<=-rat. $ <=-less yy'<gamma. <=∘ meet-left)) <=∘ gamma-m)))
    }
  })
  \where {
    \open ExUpperReal(<=-rat,+-rat,U_<=,<_<=)
    \open ExUpperRealAbMonoid(<-rat,<_+,<_+-left)
    \open ExUpperRealSemigroup(<=_*,ldistr_<=,rdistr_<=)
  }

\lemma ex-upper-*-locally-uniform : LocallyUniformMap (ManhattanProductPseudoMetricSpace UpperRealMetric UpperRealMetric) ExUpperRealMetric (\lam s => s. ExUpperReal.* s.)
  => transport (LocallyUniformMap (ManhattanProductPseudoMetricSpace UpperRealMetric UpperRealMetric) ExUpperRealMetric) (ext \lam s => UpperRealSemigroup.*-ex) upper-*-locally-uniform