\import Algebra.Pointed
\import Arith.Rat
\import Arith.Real.UpperReal
\import Data.Or
\import Equiv
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin
\import Set.Fin.Instances
\import Set.Subset
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.MetricSpace
\import Topology.UniformSpace
\open IsTotallyBounded(IsCover,Cond)
\open ClosurePrecoverSpace

\func IsTotallyBounded (X : CoverSpace) : \Prop
  => Cond X.isCauchy IsCover
  \where {
    \protected \func IsCover {X : \Set} (C : Set (Set X)) => \Pi (x : X) -> ∃ (U : C) (U x)

    \protected \func Cond {X : \Set} (P Q : Set (Set (Set X))) => ∀ {C : P} ∃ (U : Array (Set X)) (Q \lam V => ∃ (W : U) (W = V)) (∀ (V : U) (C V))
  }

\lemma totallyBounded-uniform {X : RegularPreuniformSpace} (Xp : X.IsProperUniform) (Xtb : IsTotallyBounded X) : Cond X.isCauchy isUniform
  => \lam Cc =>
    \have | (inP (D,Dc,f)) => Xtb $ X.<=*-cauchy-regular Cc
          | (inP g) => FinSet.finiteAC f
          | (inP h) => FinSet.finiteAC (\lam j => (g j).)
    \in inP (\lam i => (g i)., uniform-refine (Xp $ X.uniform-inter-big (\lam j => (h j).) (\lam j => (h j).)) \lam {W'} (EW', inP (x,W'x)) => \case Dc x \with {
      | inP (_, inP (j,idp), Dx) => inP (_, inP (j,idp), \case Refines-inter-big (\lam j => (h j).) j EW' \with {
        | inP (W,hW,W'<=W) => W'<=W <=∘ Set.Union-cond (later (hW, (x, (Dx, W'<=W W'x)))) <=∘ (h j).
      })
    }, \lam i => (g i).)

\lemma totallyBounded-cauchy-uniform {X : RegularPreuniformSpace} (Xp : X.IsProperUniform) (Xtb : IsTotallyBounded X) {C : Set (Set X)} (Cc : isCauchy C) : isUniform C
  => \case totallyBounded-uniform Xp Xtb Cc \with {
    | inP (U,Uu,CU) => uniform-refine Uu \lam {_} (inP (j,idp)) => inP (U j, CU j, <=-refl)
  }

\lemma totallyBounded-strong-uniform {X : StronglyRegularPreuniformSpace} (Xp : X.IsWeaklyProperUniform) (Xtb : IsTotallyBounded X) : Cond X.isCauchy isUniform
  => \lam Cc =>
    \have | (inP (V,Vc,g)) => Xtb $ X.s<=*-cauchy-regular Cc
          | (inP h) => FinSet.finiteAC g
    \in inP (\lam i => (h i)., Xp $ uniform-refine (X.uniform-inter-big (\lam j W => (W = Compl (V j)) || (W = (h j).)) (\lam j => (h j).))
              \lam {W} c => \case rewrite CoverInterBig-char in c \with {
                | inP (Ws,We,W=Ws) => \case FinSet.searchFin (\lam j => \Sigma (p : Ws j = (h j).) (We j = byRight p)) (\lam j => cases (We j) \with {
                  | byLeft _ => no \lam q => \case q.
                  | byRight p => yes (p,idp)
                }) \with {
                  | inl (j,(p,_),_) => inP (_, byRight $ inP (j,idp), rewrite (W=Ws, inv p) $ TopMeetSemilattice.BigMeet-cond {_} {Ws} j)
                  | inr f => inP (_, byLeft idp, \lam {x} Wx => \case Vc x \with {
                    | inP (_, inP (j,idp), Vjx) => \case f j (cases (We j) \with {
                      | byLeft q => \case (rewrite q in TopMeetSemilattice.BigMeet-cond {_} {Ws} j (rewrite W=Ws in Wx)) Vjx
                      | byRight p => (p,idp)
                    })
                  })
                }
              }, \lam i => (h i).)

\lemma totallyBounded-cauchy-strong-uniform {X : StronglyRegularPreuniformSpace} (Xp : X.IsWeaklyProperUniform) (Xtb : IsTotallyBounded X) {C : Set (Set X)} (Cc : isCauchy C) : isUniform C
  => \case totallyBounded-strong-uniform Xp Xtb Cc \with {
    | inP (U,Uu,CU) => uniform-refine Uu \lam {_} (inP (j,idp)) => inP (U j, CU j, <=-refl)
  }

\lemma totallyBounded-uniform-char {X : RegularPreuniformSpace} (base : Cond X.isUniform IsCover) : IsTotallyBounded X
  => \lam Cc => totallyBounded-closure base (uniform-cauchy. Cc)
  \where {
    -- This lemma is also true if IsCover is replaced with isCauchy.
    \private \lemma totallyBounded-closure {X : PreuniformSpace} (base : Cond X.isUniform IsCover) {C : Set (Set X)} (Cc : Closure isUniform C)
      : ∃ (D : Array (Set X)) (IsCover \lam V => ∃ (W : D) (W = V)) ∀ (V : D) (C V) \elim Cc
      | closure Cu => base Cu
      | closure-top idp => inP (top :: nil, \lam x => inP (top, inP (, idp), ()), \lam () => idp)
      | closure-refine Dc D<C => \case totallyBounded-closure base Dc \with {
        | inP (U,Uc,DU) => \case FinSet.finiteAC (\lam j => D<C (DU j)) \with {
          | inP V => inP (\lam j => (V j)., \lam x => \case Uc x \with {
            | inP (_, inP (j,idp), Ux) => inP (_, inP (j, idp), (V j). Ux)
          }, \lam j => (V j).)
        }
      }
      | closure-trans {D} Dc {E} Ec idp => \case totallyBounded-closure base Dc \with {
        | inP (V,Vc,DV) => \case FinSet.finiteAC (\lam j => totallyBounded-closure base $ Ec (DV j)) \with {
          | inP W => \have e : QEquiv => SigmaFin.aux {_} {\lam i => (W i)..len} \in inP
            (\lam k => V (e k). ∧ (W (e k).). (e k).,
             \lam x => \case Vc x \with {
               | inP (_, inP (i,idp), Vx) => \case (W i). x \with {
                 | inP (_, inP (j,idp), Wx) => inP (_, inP (e.ret (i,j), idp), rewrite e.f_ret (Vx,Wx))
               }
             },
             \lam k => inP (_, _, DV (e k)., (W _). (e k)., idp))
        }
      }
  }

\func IsCompact (X : CompleteCoverSpace) : \Prop
  => IsTotallyBounded X

\lemma makeUniformMapTB {X Y : RegularPreuniformSpace} (Xp : X.IsProperUniform) (Xtb : IsTotallyBounded X) (f : CoverMap X Y) : UniformMap X Y f \cowith
  | func-uniform Eu => totallyBounded-cauchy-uniform Xp Xtb $ f.func-cover $ Y.makeCauchy Eu

\lemma makeUniformMapSTB {X : StronglyRegularUniformSpace} {Y : RegularPreuniformSpace} (Xp : X.IsWeaklyProperUniform) (Xtb : IsTotallyBounded X) (f : CoverMap X Y) : UniformMap X Y f \cowith
  | func-uniform Eu => totallyBounded-cauchy-strong-uniform Xp Xtb $ f.func-cover $ Y.makeCauchy Eu

-- Totally bounded subsets

\func IsTotallyBoundedSet {X : CoverSpace} (U : Set X) : \Prop
  => IsTotallyBounded $ CoverTransfer {\Sigma (x : X) (U x)} __.

\lemma totallyBoundedSet-char {X : CoverSpace} {U : Set X}
  : IsTotallyBoundedSet U <-> ∀ {C : isCauchy} ∃ (D : Array (Set X)) (∀ {x : U} ∃ (V : D) (V x)) (∀ (V : D) (C V))
  => (\lam f Cc => \case f $ func-cover {PrecoverTransfer-map {\Sigma (x : X) (U x)} __.} Cc \with {
    | inP (D,Dc,Dp) => \case FinSet.finiteAC Dp \with {
      | inP g => inP (\lam j => (g j)., \lam {x} Ux => \case Dc (x,Ux) \with {
        | inP (_, inP (j,idp), Dx) => inP (j, rewrite (g j). in Dx)
      }, \lam j => (g j).)
    }
  }, \lam f Cc => \case f Cc \with {
    | inP (D,Dc,Dp) => \case FinSet.finiteAC Dp \with {
      | inP g => inP (\lam j => (g j)., \lam x => \case Dc x. \with {
        | inP (j,Dx) => inP (_, inP (j,idp), (g j). Dx)
      }, \lam j => (g j).)
    }
  })

\lemma totallyBoundedSet-subset {X : CoverSpace} {U V : Set X} (V<=U : V ⊆ U) (Utb : IsTotallyBoundedSet U) : IsTotallyBoundedSet V
  => totallyBoundedSet-char. \lam Cc => \case totallyBoundedSet-char. Utb Cc \with {
    | inP (D,DU,CD) => inP (D, \lam Vx => DU (V<=U Vx), CD)
  }

\lemma totallyBoundedSet-uniform-char {X : RegularPreuniformSpace} {S : Set X}
  : IsTotallyBoundedSet S <-> ∀ {C : isUniform} ∃ (D : Array (Set X)) (∀ {x : S} ∃ (V : D) (V x)) (∀ (V : D) (C V))
  => (\lam tb Cu => totallyBoundedSet-char. tb $ uniform-cauchy. $ closure Cu,
      \lam tb => totallyBounded-uniform-char {RegularPreuniformTransfer __.} \lam Cu => \case tb Cu \with {
        | inP (D,g,h) => \case FinSet.finiteAC h \with {
          | inP f => inP (\lam j => (f j)., \lam x => \case g x. \with {
            | inP (j,Dx) => inP (_, inP (j, idp), (f j). Dx)
          }, \lam j => (f j).)
        }
      })

\lemma totallyBoundedSet-metric-char {X : ExPseudoMetricSpace} {S : Set X}
  : IsTotallyBoundedSet S <-> ∀ {eps : Rat} ( < eps) ∃ (D : Array X) ∀ {x : S} ∃ (y : D) ((dist y x).U eps)
  => (\lam tb eps>0 => \case totallyBoundedSet-uniform-char. tb (X.metricUniform eps>0) \with {
    | inP (D,DS,h) => \case FinSet.finiteAC h \with {
      | inP g => inP (\lam j => (g j)., \lam Sx => \case DS Sx \with {
        | inP (j,Dx) => inP (j, rewrite (g j). in Dx)
      })
    }
  }, \lam tb => totallyBoundedSet-uniform-char. \lam Cu => \case dist-uniform. Cu \with {
    | inP (eps,eps>0,h) => \case tb eps>0 \with {
      | inP (D,g) => \case FinSet.finiteAC (\lam j => h (D j)) \with {
        | inP f => inP (\lam j => (f j)., \lam Sx => \case g Sx \with {
          | inP (j,d) => inP (j, (f j). d)
        }, \lam j => (f j).)
      }
    }
  })

-- Locally totally bounded spaces

\func IsLocallyUniform {X : PreuniformSpace} (C : Set (Set X)) (E : Set (Set X)) : \Prop
  => ∀ {U : C} (isUniform \lam V => ∃ (W : E) (U ∧ V ⊆ W))

\func IsLocallyUniformSpace (X : PreuniformSpace) : \Prop
  => ∃ (C : X.isUniform) ∀ {E : X.isCauchy} (IsLocallyUniform C E)

\lemma locallyUniform-cauchy {X : PreuniformSpace} {C : Set (Set X)} (Cc : isCauchy C) (E : Set (Set X)) (lu : IsLocallyUniform C E) : isCauchy E
  => cauchy-refine (cauchy-glue Cc {\lam U V => ∃ (W : E) (U ∧ V ⊆ W)} \lam CU => X.makeCauchy $ lu CU) (\lam {_} (inP (U, V, CU, inP (W,EW,p), idp)) => inP (W, EW, p))

\lemma locallyUniform-cover-char {X : StronglyRegularUniformSpace} {C : Set (Set X)} (Cb : ∀ {U : C} (IsTotallyBoundedSet U)) (Cp : ∀ {U : C} ∃ U) {E : Set (Set X)} (Ec : isCauchy E) : IsLocallyUniform C E
  => \lam {U} CU =>
    \have Du => totallyBounded-cauchy-strong-uniform {StronglyRegularUniformTransfer {\Sigma (x : X) (U x)} __.} (PreuniformSpace.inhabited_weaklyProper $ Cp CU) (Cb CU) (PrecoverTransfer.makeCauchy Ec)
    \in uniform-subset Du \lam {V} (inP (_, inP (W,EW,idp), p)) => inP $ later (W, EW, \lam {x} (Ux,Vx) => p {x,Ux} Vx)

\lemma locallyTotallyBounded-locallyUniform {X : StronglyRegularUniformSpace} (Xltb : X.isUniform IsTotallyBoundedSet) (Xd : X.IsProperUniform) : IsLocallyUniformSpace X
  => inP (\lam U => \Sigma (IsTotallyBoundedSet U) (∃ U), Xd Xltb, locallyUniform-cover-char (later __.) (later __.))

\func BallsTotallyBounded (X : ExPseudoMetricSpace) : \Prop
  => \Pi (x : X) {eps : Rat} ->  < eps -> IsTotallyBoundedSet (OBall eps x)

\lemma metric-locallyUniform {X : PseudoMetricSpace} (Xbtb : BallsTotallyBounded X) : IsLocallyUniformSpace X
  => locallyTotallyBounded-locallyUniform (uniform-subset (X.metricUniform RatField.zro<ide) $ later \lam {_} (inP (x,idp)) => Xbtb x RatField.zro<ide) X.metricProperUniform

\lemma locallyUniformMapFromCover {X Y : RegularPreuniformSpace} (Xlu : IsLocallyUniformSpace X) (f : CoverMap X Y) : LocallyUniformMap X Y f \cowith
  | func-locally-uniform Eu => \case Xlu \with {
    | inP (C,Cu,h) => inP (C, Cu, \lam CU => uniform-subset (h (f.func-cover (Y.makeCauchy Eu)) CU) \lam {V} (inP (_, inP (W,EW,idp), p)) => inP $ later (W, EW, p))
  }