{- TODO[server2]: Delete or rewrite this
\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.Ring.Boolean
\import Algebra.Semiring
\import Analysis.Measure.MeasureRing
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\import Arith.Real.InfReal
\import Arith.Real.LowerReal
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\import Order.Lattice
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set.Filter
\import Set.Subset
\import Topology.CoverSpace.Complete
\import Topology.MetricSpace.ExtendedMetricSpace
\import Topology.MetricSpace.ValuedMetricSpace
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.ExtendedNormedAbGroup
\import Topology.NormedAbGroup.ValuedNormedAbGroup
\import Topology.TopSpace
\import Topology.UniformSpace.Complete
\import Topology.UniformSpace.InfReal

\class LowerPseudoNormedAbGroup \extends ValuedPseudoNormedAbGroup
  | V => ExtendedPseudoMetricSpace.LowerRealMetricValueOrder

\class PseudoOuterPremeasureRing \extends BooleanPseudoRing, ValuedPseudoNormedAbGroup
  | V => ExtendedPseudoMetricSpace.LowerRealMetricValueOrder
  | norm-outer-measure {x y : E} : norm (x ∨ y) LowerRealAbMonoid.<= norm x LowerRealAbMonoid.+ norm y
  | norm-outer-mono {x y : E} : x <= y -> norm x LowerRealAbMonoid.<= norm y
  | norm_negative => pmap norm neative=id
  | norm_+ => rewrite +_diff $ norm-outer-measure LowerRealAbMonoid.<=∘ LowerRealAbMonoid.<=_+ (norm-outer-mono diff_<=) (norm-outer-mono diff_<=)

-- TODO: Replace with relative completion
\class ExtendedMeasure \noclassifying (R : LowerPseudoNormedAbGroup) (M : PremeasurePseudoRing) (inc : AddGroupHom M R) (comp : \Pi (a : M) -> norm a LowerRealAbMonoid.<= norm (inc a)) {
  \func IsMeasurable (a : R) : \Prop
    => ∃ (F : ProperFilter M) (R.IsFilterLimit (SetFilter-map inc F) a)

  \lemma measurable-cauchy {F : ProperFilter M} (Fc : IsCauchyFilter (SetFilter-map inc F)) : IsCauchyFilter (SetFilter-map norm F)
    => (cauchyFilter-uniform-char {InfRealUniformSpace}).2 \lam (inP (eps,B,eps>0,V0,CV0,BV0,h)) => \case cauchyFilter-uniform-char.1 Fc (R.metricUniform $ RealAbGroup.lower_<-char.2 $ half>0 eps>0) \with {
      | inP (_, inP (a,idp), Fa) => unfold $ unfold at Fa $ \case F.isProper Fa \with {
        | inP (x,ax<eps/2) =>
          \have aux {y} (ay<eps/2 : dist a (inc y) < half eps) => inf-real_<_LowerReal.2 $ transportInv (`< _) M.norm-dist $ comp _ LowerRealAbMonoid.<∘r transport2 (<) (norm-dist *> inv (pmap norm inc.func-minus)) (inv {LowerReal} RealAbGroup.+-lower *> {LowerReal} half+half) (R.dist-triang <∘r LowerRealAbMonoid.<_+ (transportInv (LowerRealAbMonoid.`< _) dist-symm ax<eps/2) ay<eps/2)
          \in \case inf-real-located {norm x} {B + eps} {B + eps * 2} linarith \with {
            | byLeft |x|>B+eps => inP (V0, CV0, filter-mono Fa \lam {y} ay<eps/2 => unfold (^-1) at ay<eps/2 $ BV0 \case |x|>B+eps \with {
              | inP (B',B+eps<B',B'<|x|) => \case inf-real-located {norm y} {B} {B' - {RealAbGroup} eps} $ linarith (real_<_U.2 B+eps<B') \with {
                | byLeft r => r
                | byRight |y|<B'-eps => absurd $ InfRealAbMonoid.<-irreflexive {B'} $ InfRealAbMonoid.<_L.2 B'<|x| <∘ norm_dist-bound {_} {x} {y} <∘r transport (_ <) (inv RealAbGroup.+-inf *> RealAbGroup.+-comm *> +-assoc *> pmap (B' RealAbGroup.+) negative-left *> RealAbGroup.zro-right) (InfRealAbMonoid.<_+ (aux ay<eps/2) |y|<B'-eps)
              }
            })
            | byRight |x|<B+2eps =>
              \let x' : M.Bounded => (x, inP (_, |x|<B+2eps))
              \in \case h (norm x') \with {
                | inP (U,CU,g) => inP (U, CU, filter-mono Fa \lam {y} ay<eps/2 => unfold (^-1) at ay<eps/2 $ unfolds
                  \let y' : M.Bounded => (y, dist-bounded (aux ay<eps/2) x'.2)
                  \in g {norm y'} $ norm_-_abs {_} {x'} {y'} <∘r real_<_InfReal.2 (later $ transport {InfReal} (`< _) M.norm-dist $ aux ay<eps/2))
              }
          }
      }
    }

  \lemma measure-pair {a : R} (m : IsMeasurable a) : Given (v : InfReal) ∃ (F : ProperFilter M) (R.IsFilterLimit (SetFilter-map inc F) a) (TopSpace.IsFilterLimit (SetFilter-map norm F) v)
    \level \lam (u, inP s1) (v, inP s2) =>
      \have aux {u v : InfReal} {F1 : ProperFilter M} (F1a : R.IsFilterLimit (SetFilter-map inc F1) a) (F1u : TopSpace.IsFilterLimit (SetFilter-map norm F1) u)
                                {F2 : ProperFilter M} (F2a : R.IsFilterLimit (SetFilter-map inc F2) a) (F2v : TopSpace.IsFilterLimit (SetFilter-map norm F2) v)
                                (v<u : v < u) : Empty
        => \let | (inP (q,v<q,q<u)) => v<u
                | (inP (r,r<u,q<r)) => L-rounded q<u
                | eps => r - {RealAbGroup} q
                | eps>0 : 0 < eps => linarith (rat_real_<.1 q<r)
                | v' => inf-real-real v {q} (InfRealAbMonoid.<_U.2 v<q)
           \in F1.isWeaklyProper $ filter-mono (filter-meet (F1a OBall-open $ OBall-center $ (RealAbGroup.lower_<-char {0} {eps * ratio 1 4}).2 linarith) (F1u (infReal-half-open r) (InfRealAbMonoid.<_L.2 r<u))) \lam {x1} VWx1 => absurd $
               F2.isWeaklyProper $ filter-mono (filter-meet (F2a OBall-open $ OBall-center $ (RealAbGroup.lower_<-char {0} {eps * ratio 1 4}).2 linarith) (F2v (infReal-ball-open (half eps) v') (inP (v', idp, rewrite (negative-right,RealAbGroup.abs_zro) $ half>0 eps>0)))) \lam {x2} VWx2 => absurd
                \have | |x1-x2|<eps/2 => comp (x1 - x2) LowerRealAbMonoid.<∘r transport2 (<) (R.norm-dist *> inv (pmap norm inc.func-minus)) (inv {LowerReal} $ (pmap (eps *) (inv RealAbGroup.+-rat) *> ldistr) *> {LowerReal} RealAbGroup.+-lower) (R.dist-triang <∘r LowerRealAbMonoid.<_+ (transport (LowerRealAbMonoid.`< _) dist-symm VWx1.1) VWx2.1)
                      | (inP (|x2|,p2,e2')) => VWx2.2
                      | |x2|<eps/2+v' : |x2| < half eps + v' => linarith (RealAbGroup.abs>=id <∘r e2')
                \in linarith $ usingOnly (real_<_InfReal.2 $ VWx1.2 InfRealAbMonoid.<∘ transportInv (_ <) RealAbGroup.+-inf (simplify in M.norm_+ <∘r InfRealAbMonoid.<_+ (inf-real_<_LowerReal.2 |x1-x2|<eps/2) (rewrite p2 in real_<_InfReal.1 |x2|<eps/2+v')), real_<_U.2 (later v<q) : v' < q)
      \in ext $ <=-antisymmetric (aux s1.2 s1.3 s2.2 s2.3) (aux s2.2 s2.3 s1.2 s1.3)
    \elim m
    | inP (F,al) => \let CF => \new CauchyFilter InfRealUniformSpace {
      | ProperFilter => ProperFilter-map norm F
      | isCauchyFilter {C} => measurable-cauchy (filter-limit-cauchy al) {C}
    } \in (CompleteCoverSpace.filter-point CF, inP (F, al, CompleteCoverSpace.filter-point-limit))

  {-
  \lemma measurable-closed {a b c : R} (op : M -> M -> M) (am : IsMeasurable a) (bm : IsMeasurable b) : IsMeasurable c \elim am, bm
    | inP (F,Fa), inP (G,Gb) =>
      \let H : ProperFilter M => \new ProperFilter {
        | F W => ∃ (U : Set M) (F U) (V : Set M) (G V) ∀ {x : U} {y : V} (W (op x y))
        | filter-mono (inP (U,FU,V,GV,h)) p => inP (U, FU, V, GV, \lam Ux Vy => p (h Ux Vy))
        | filter-top => inP (top, filter-top, top, filter-top, \lam _ _ => ())
        | filter-meet (inP (U,FU,V,GV,h)) (inP (U',FU',V',GV',h')) => inP (U ∧ U', filter-meet FU FU', V ∧ V', filter-meet GV GV', \lam s t => (h s.1 t.1, h' s.2 t.2))
        | isProper {W} (inP (U,FU,V,GV,h)) => \case isProper FU, isProper GV \with {
          | inP (x,Ux), inP (y,Vy) => inP (op x y, h Ux Vy)
        }
      }
      \in inP (H, \lam {W} Wo Wc => inP {?})

  \lemma measurable-closed' {a b : R} (op : R -> R -> R) (am : IsMeasurable a) (bm : IsMeasurable b) : IsMeasurable (op a b) \elim am, bm
    | inP (F,Fa), inP (G,Gb) =>
      \let H : ProperFilter M => \new ProperFilter {
        | F W => ∃ (U : Set M) (F U) (V : Set M) (G V) ∀ {x : U} {y : V} {z} (inc z = op (inc x) (inc y) -> W z)
        | filter-mono (inP (U,FU,V,GV,h)) p => inP (U, FU, V, GV, \lam Ux Vy q => p (h Ux Vy q))
        | filter-top => inP (top, filter-top, top, filter-top, \lam _ _ _ => ())
        | filter-meet (inP (U,FU,V,GV,h)) (inP (U',FU',V',GV',h')) => inP (U ∧ U', filter-meet FU FU', V ∧ V', filter-meet GV GV', \lam s t q => (h s.1 t.1 q, h' s.2 t.2 q))
        | isProper {W} (inP (U,FU,V,GV,h)) => \case isProper FU, isProper GV \with {
          | inP (x,Ux), inP (y,Vy) => inP {?}
        }
      }
      \in inP (H, \lam {W} Wo Wc => inP {?})
  -}
}
-}