Real

\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.StrictlyOrdered
\import Algebra.Pointed
\import Arith.Rat
\import Arith.Real
\import Arith.Real.LowerReal
\import Arith.Real.UpperReal
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Operations
\import Order.Biordered
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set.Filter
\import Set.Subset
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.Product
\import Topology.CoverSpace.StronglyComplete
\import Topology.MetricSpace
\import Topology.NormedAbGroup
\import Topology.RatherBelow
\open LatticeAbGroup
\open LinearlyOrderedAbGroup
\open RealNormed
\open ProductCoverSpace

\instance RatNormed : NormedAbGroup
  | AbGroup => RatField
  | norm a => abs a
  | norm_zro => pmap ExUpperReal.fromRat abs_zro
  | norm_negative => pmap ExUpperReal.fromRat abs_negative
  | norm_+ => transportInv (_ <=) ExUpperReal.+-rat $ ExUpperReal.<=-rat.1 abs_+
  | norm-ext p => abs_zro-ext $ ExUpperReal.fromRat-inj p

\func rat_real : NormedIsometricMap RatNormed RealNormedAbGroup Real.fromRat \cowith
  | func-+ => inv RealAbGroup.+-rat
  | func-norm-isometry => inv rat_real_abs
  \where {
    \lemma dense : rat_real.IsDense
      => \lam {y} {U} Uo Uy => \case (dist_open {RealNormedAbGroup} {U}).1 Uo Uy \with {
        | inP (eps,eps>0,p) => \case y.LU-focus eps eps>0 \with {
          | inP (x,x<y,y<x+eps) => inP (x, inP (x,idp), p $ real_<_U.1 $ abs_-_< (RealAbGroup.<-diff-mid-conv $ transport (_ <) (inv RealAbGroup.+-rat *> +-comm) $ real_<_U.2 y<x+eps) $ RealAbGroup.to<0 (real_<_L.2 x<y) <∘ rat_real_<.1 eps>0)
        }
      }

    \lemma dense-coverEmbedding : CoverMap.IsDenseEmbedding {rat_real}
      => (dense, rat_real.embedding->coverEmbedding (rat_real.dense->uniformEmbedding dense).2)
  }

\instance RealNormed : CompleteNormedAbGroup
  | NormedAbGroup => RealNormedAbGroup
  | isStronglyComplete => dense-stronglyComplete (rat_real.dense->weaklyDense rat_real.dense, rat_real.embedding->coverEmbedding (rat_real.dense->uniformEmbedding rat_real.dense).2)
      \lam F => inP (fromCF F, \lam {U} => \case <=<-ball __ \with {
        | inP (eps,eps>0,p) =>
          \let | x => fromCF F
               | x<x+eps => transport (RealAbGroup.`< _) zro-right $ <_+-right x $ rat_real_<.1 eps>0
               | (inP (a, x-eps<a, inP (y1,eps1,eps1>0,Fy1,a<y1-eps1))) => (real_<-rat-char {x - eps} {x}).1 $ RealAbGroup.<-diff-mid-conv x<x+eps
               | (inP (b, inP (y2,eps2,eps2>0,Fy2,y2+eps2<b), b<x+eps)) => (real_<-rat-char {x} {x + eps}).1 x<x+eps
          \in filter-mono (filter-meet Fy1 Fy2) $ (\lam {z} (|y1-z|<eps1,|y2-z|<eps2) => real_<_U.1 $ later $ RealAbGroup.abs_-_<
                (RealAbGroup.<-diff-left $ real_<_U.2 x-eps<a <∘ rat_real_<.1 a<y1-eps1 <∘ rat_real_<.1 (linarith $ abs>=id <∘r |y1-z|<eps1))
                (RealAbGroup.<-diff-mid-conv $ transport (_ <) +-comm $ rat_real_<.1 (transport (_ <) +-comm (RatField.<-diff-mid $ abs>=_- <∘r |y2-z|<eps2) <∘ y2+eps2<b) <∘ real_<_L.2 b<x+eps)) <=∘ ^-1_<= rat_real p
      })
  \where {
    \func RealNormedAbGroup : NormedAbGroup \cowith
      | AbGroup => RealAbGroup
      | norm => abs
      | norm_zro => Real.=-upper.1 abs_zro
      | norm_negative => Real.=-upper.1 abs_negative
      | norm_+ => transport (_ ExUpperRealAbMonoid.<=) RealAbGroup.+-upper $ Real.<=-upper.1 abs_+
      | norm-ext {x} p => abs_zro-ext $ (Real.=-upper {abs x} {0}).2 p

    \func fromCF (F : StronglyRegularCauchyFilter RatNormed) : Real \cowith
      | L a => ∃ (x eps : Rat) (0 < eps) (F (OBall eps x)) (a < x - eps)
      | L-inh => \case cauchyFilter-metric-char.1 F.isCauchyFilter {1} RatField.zro<ide \with {
        | inP (x,FB) => inP (x - 2, inP (x, 1, idp, FB, linarith))
      }
      | L-closed (inP (x,eps,eps>0,FB,q<x-eps)) q'<q => inP (x, eps, eps>0, FB, q'<q <∘ q<x-eps)
      | L-rounded {a} (inP (x,eps,eps>0,FB,a<x-eps)) => inP (RatField.mid a (x - eps), inP (x, eps, eps>0, FB, RatField.mid<right a<x-eps), RatField.mid>left a<x-eps)
      | U b => ∃ (x eps : Rat) (0 < eps) (F (OBall eps x)) (x + eps < b)
      | U-inh => \case cauchyFilter-metric-char.1 F.isCauchyFilter {1} RatField.zro<ide \with {
        | inP (x,FB) => inP (x + 2, inP (x, 1, idp, FB, linarith))
      }
      | U-closed (inP (x,eps,eps>0,FB,x+eps<q)) q<q' => inP (x, eps, eps>0, FB, x+eps<q <∘ q<q')
      | U-rounded {a} (inP (x,eps,eps>0,FB,x+eps<a)) => inP (RatField.mid (x + eps) a, inP (x, eps, eps>0, FB, RatField.mid>left x+eps<a), RatField.mid<right x+eps<a)
      | LU-disjoint (inP (x,eps,eps>0,Feps,q<x-eps)) (inP (y,delta,delta>0,Fdelta,x+eps<q)) => F.isWeaklyProper $ filter-mono (filter-meet Feps Fdelta)
          \lam {z} (xz<eps,yz<delta) => absurd $ linarith $ abs>=id <∘r RatNormed.halving-right xz<eps yz<delta <=-refl
      | LU-focus eps eps>0 => \case cauchyFilter-metric-char.1 F.isCauchyFilter {eps * ratio 1 4} linarith \with {
        | inP (x,FB) => inP (x - eps * ratio 1 2, inP (x, _, linarith, FB, linarith), inP (x, _, linarith, FB, linarith))
      }
  }

\func open-rat-int (a b : Rat) : Set Real
  => \lam (x : Real) => \Sigma (x.L a) (x.U b)

\lemma dense-lift-real-char {X Y : CoverSpace} {f : CoverMap X Y} (fd : f.IsDenseEmbedding) {g : CoverMap X RealNormed} (y : Y) (a b : Rat)
  : open-rat-int a b (cauchy-lift f fd g y) <-> ∃ (a' b' : Rat) (a < a') (b' < b) (V : Set Y) (f ^-1 V ⊆ g ^-1 open-rat-int a' b') (single y <=< V)
  => (\lam (a<z,z<b) => \case L-rounded a<z, U-rounded z<b \with {
    | inP (a',a'<z,a<a'), inP (b',z<b',b'<b) => \case (dense-lift-neighborhood fd y (open-rat-int a' b')).1 (point_<=< a'<z z<b') \with {
      | inP (W,W<=<a'b',V,q,y<=<V) => inP (a', b', a<a', b'<b, V, q <=∘ <=<_<= (<=<_^-1 W<=<a'b'), y<=<V)
    }
  }, \lam (inP (a',b',a<a',b'<b,V,h,y<=<V)) => <=<_<= ((dense-lift-neighborhood fd y (\lam x => open-rat-int a b x)).2 $ inP (open-rat-int a' b', <=<_open-rat-int a<a' b'<b, V, h, y<=<V)) idp)
  \where {
    \open ClosurePrecoverSpace

    \lemma makeRealCover (eps : Rat) (eps>0 : 0 < eps) : RealNormed.isCauchy \lam U => ∃ (a : Rat) (U = open-rat-int a (a + eps))
      => RealNormed.makeCauchy $ inP (RatField.half $ RatField.half eps, linarith, \lam x => \case rat_real.dense (OBall-open {RealNormed}) (OBall-center {RealNormed} $ RatField.half>0 $ RatField.half>0 eps>0) \with {
        | inP (_, inP (q,idp), p) => inP $ later (_, inP (q - eps * ratio 1 2, idp), \lam d =>
          \have qy<eps/2 => real_<_U.2 (RealNormedAbGroup.halving1/2 p d)
          \in (real_<_L.1 $ transport (`< _) RealAbGroup.minus-rat $ RealAbGroup.<-diff-left $ abs>=id <∘r qy<eps/2,
               real_<_U.1 $ transport (_ <) (RealAbGroup.+-rat *> pmap Real.fromRat linarith) $ RealAbGroup.<-diff-mid $ abs>=_- <∘r qy<eps/2))
      })

    \lemma <=<_open-rat-int {a b a' b' : Rat} (a<a' : a < a') (b'<b : b' < b) : open-rat-int a' b' <=< open-rat-int a b
      => closure-subset (makeRealCover ((a' - a) ∧ (b - b')) $ <_meet-univ linarith linarith) \lam {U} (inP (c,p)) => rewrite p $ later \lam (e : Real, ((a'<e,e<b'),(c<e,e<c+eps))) (c<x,x<c+eps) => (L-closed c<x $ linarith (e.LU-less a'<e e<c+eps <∘l <=_+ <=-refl meet-left), U-closed x<c+eps $ <=_+ <=-refl meet-right <∘r linarith (e.LU-less c<e e<b'))

    \lemma point_<=< {x : Real} {a b : Rat} (a<x : x.L a) (x<b : x.U b) : single x <=< open-rat-int a b
      => \case x.L-rounded a<x, x.U-rounded x<b \with {
        | inP (a',a'<x,a<a'), inP (b',x<b',b'<b) => <=<-right (later \lam p => rewriteI p (a'<x,x<b')) (<=<_open-rat-int a<a' b'<b)
      }
  }

\lemma <=<-open-int {x : Real} {U : Set Real} (p : single x <=< U) : ∃ (a b : Rat) (x.L a) (x.U b) ∀ (y : Real) (y.L a -> y.U b -> U y)
  => \case <=<-ball p \with {
    | inP (eps,eps>0,q) => \case (real_<-rat-char {x - eps} {x}).1 $ transport (_ <) zro-right $ <_+-right x $ RealAbGroup.positive_negative $ rat_real_<.1 eps>0, (real_<-rat-char {x} {x + eps}).1 $ transport (`< _) zro-right $ <_+-right x $ rat_real_<.1 eps>0 \with {
      | inP (a,x-eps<a,a<x), inP (b,x<b,b<x+eps) => inP (a, b, a<x, x<b, \lam y a<y y<b => q $ real_<_U.1 $ abs_-_< (RealAbGroup.<-diff-left $ real_<_U.2 x-eps<a <∘ real_<_L.2 a<y) $ RealAbGroup.<-diff-mid-conv $ transport (_ <) +-comm $ real_<_U.2 y<b <∘ real_<_L.2 b<x+eps)
    }
  }

\func real-lift2 {X : CompleteCoverSpace} (f : CoverMap (RatNormed ⨯ RatNormed) X) : CoverMap (RealNormed ⨯ RealNormed) X
  => dense-lift (prod rat_real rat_real) (prod.isDenseEmbedding rat_real.dense-coverEmbedding rat_real.dense-coverEmbedding) f

\lemma real-lift2-char {f : CoverMap (RatNormed ⨯ RatNormed) RealNormed} {x y : Real} (a b : Rat)
  : open-rat-int a b (real-lift2 f (x,y)) <-> ∃ (a' b' c1 d1 c2 d2 : Rat) (a < a') (b' < b) (x.L c1) (x.U d1) (y.L c2) (y.U d2) (\Pi {x y : Rat} -> \Sigma (c1 < x) (x < d1) -> \Sigma (c2 < y) (y < d2) -> open-rat-int a' b' (f (x,y)))
  => <->trans (dense-lift-real-char {RatNormed ⨯ RatNormed} {_} {prod rat_real rat_real} (prod.isDenseEmbedding rat_real.dense-coverEmbedding rat_real.dense-coverEmbedding) (x,y) a b) $ later
      (\lam (inP (a',b',a<a',b'<b,V,q,xy<=<V)) => \case prod-neighborhood.1 xy<=<V \with {
        | inP (U,V,x<=<U,y<=<V,h) => \case <=<-open-int x<=<U, <=<-open-int y<=<V \with {
          | inP (c1,d1,c1<x,x<d1,p1), inP (c2,d2,c2<y,y<d2,p2) => inP (a', b', c1, d1, c2, d2, a<a', b'<b, c1<x, x<d1, c2<y, y<d2, \lam {x'} {y'} (c1<x',x'<d1) (c2<y',y'<d2) => q $ h (p1 x' c1<x' x'<d1) (p2 y' c2<y' y'<d2))
        }
      }, \lam (inP (a',b',c1,d1,c2,d2,a<a',b'<b,c1<x,x<d1,c2<y,y<d2,q)) => inP (a', b', a<a', b'<b, \lam z => \Sigma (open-rat-int c1 d1 z.1) (open-rat-int c2 d2 z.2),
          \lam s => q s.1 s.2, RatherBelow.<=<_meet-same (<=<-right (later \lam s => pmap __.1 s) $ <=<_^-1 {_} {_} {proj1} $ dense-lift-real-char.point_<=< c1<x x<d1) (<=<-right (later \lam s => pmap __.2 s) $ <=<_^-1 {_} {_} {proj2} $ dense-lift-real-char.point_<=< c2<y y<d2)))

\lemma real-dist>0 {x y : Real} (xy>0 : 0 < ldist x y) : x < y || y < x
  => \case real-located {y} {x} {x + ldist x y} $ transport (`< _) zro-right $ <_+-right x xy>0 \with {
    | byLeft x<y => byLeft x<y
    | byRight y<x+d => byRight
      \have d=x-y => LinearOrder.join/=right {RealAbGroup} \lam p => <-irreflexive $ (rewriteI p in y<x+d) <∘l transportInv (`<= _) (pmap (x +) RealAbGroup.negative_- *> +-comm *> +-assoc *> pmap (y +) negative-left *> zro-right) <=-refl
      \in RealAbGroup.from>0 (rewrite d=x-y in xy>0)
  }