\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.Ring.Boolean
\import Arith.Rat
\import Arith.Real.UpperReal
\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.Filter
\import Set.Subset
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.NormedAbGroup
\import Topology.TopAbGroup
\import Topology.TopAbGroup.Complete
\import Topology.TopSpace
\import Topology.UniformSpace.Complete
\open BooleanRing \hiding (<=)

\class PremeasureRing \extends BooleanRing, TopAbGroup {
  | meas : E -> ExUpperReal
  | meas_zro : meas  = 
  | meas>=0 {x : E} :  ExUpperReal.<= meas x
  | meas-disjoint {x y : E} : x * y =  -> meas (x ∨ y) = meas x ExUpperReal.+ meas y
  | meas-mono {x y : E} : x <= y -> meas x ExUpperReal.<= meas y
  | meas-mono p => transport2 (ExUpperReal.<=) ExUpperRealAbMonoid.zro-left (inv (meas-disjoint (rdistr *> pmap (_ +) (*-assoc *> pmap (_ *) isBooleanRing) *> double=0)) *> pmap meas (inv (split_<= p))) (<=_+ meas>=0 ExUpperRealAbMonoid.<=-refl)
  | meas_+ {x y : E} : meas (x + y) ExUpperReal.<= meas x ExUpperReal.+ meas y
  | meas_+ => transportInv (ExUpperReal.`<= _) (pmap meas +_diff *> meas-disjoint diff_*_diff) $ <=_+ (meas-mono diff_<=) (meas-mono diff_<=)
  | isOpen U => ∀ {x : U} ∃ (a : E) (eps : `> ) ∀ {y : E} ((meas (a * (x + y))).U eps -> U y)
  | open-top _ => inP (, , idp, \lam _ => ())
  | open-inter Uo Vo (Ux,Vx) => \case Uo Ux, Vo Vx \with {
    | inP (a,eps,eps>0,g), inP (b,delta,delta>0,h) => inP (a ∨ b, eps RatField.∧ delta, RatField.<_meet-univ eps>0 delta>0, \lam c =>
      (g $ meas-mono (meet-monotone join-left <=-refl) $ ExUpperReal.U_<= c RatField.meet-left,
       h $ meas-mono (meet-monotone join-right <=-refl) $ ExUpperReal.U_<= c RatField.meet-right))
  }
  | open-Union So (inP (U,SU,Ux)) => \case So SU Ux \with {
    | inP (a,eps,eps>0,h) => inP (a, eps, eps>0, \lam c => inP (U, SU, h c))
  }
  | +-cont => \new ContMap {
    | func-cont Uo {s} Us => \case Uo Us \with {
      | inP (a,eps,eps>0,h) =>
        \let | Ball c z => (meas (a * (c + z))).U (RatField.half eps)
             | Ball-open c : isOpen (Ball c) => \lam {x} => \case U-rounded __ \with {
               | inP (q,cx<q,q<eps/2) => inP (a, _, RatField.to>0 q<eps/2, \lam xy => transport2 (\lam x y => ExUpperReal.U {meas x} y) (inv ldistr *> pmap (a *) (equation.addMonoid {double=0 {_} {x}})) linarith $ ExUpperReal.<=_+-char meas_+ cx<q xy)
             }
             | Ball-center c : Ball c c => transportInv (ExUpperReal.U {__} _) (pmap meas (pmap (a *) double=0 *> zro_*-right) *> meas_zro) (RatField.half>0 eps>0)
        \in inP (Ball s., Ball-open s., Ball-center s., Ball s., Ball-open s., Ball-center s., \lam sx sy => h $ transport2 (\lam x y => ExUpperReal.U {meas x} y) (inv ldistr *> pmap (a *) equation.abMonoid) linarith $ ExUpperReal.<=_+-char meas_+ sx sy)
    }
  }

  \func OBall (a : E) (eps : Rat) (c : E) : Set E => \lam z => (meas (a * (c + z))).U eps

  \lemma OBall-open (a : E) {eps : Rat} {c : E} : isOpen (OBall a eps c) => \lam {x} => \case U-rounded __ \with {
      | inP (q,cx<q,q<eps) => inP (a, _, RatField.to>0 q<eps, \lam xy => transport2 (\lam x y => ExUpperReal.U {meas x} y) (inv ldistr *> pmap (a *) (equation.addMonoid {double=0 {_} {x}})) linarith $ ExUpperReal.<=_+-char meas_+ cx<q xy)
    }

  \lemma OBall-center {a : E} {eps : Rat} (eps>0 :  < eps) {c : E} : OBall a eps c c
    => transportInv (ExUpperReal.U {__} _) (pmap meas (pmap (a *) double=0 *> zro_*-right) *> meas_zro) eps>0

  \lemma OBall-center_<=< {a : E} {eps : Rat} (eps>0 :  < eps) {x : E} : single x <=< OBall a eps x
    => open-char. (OBall-open a) (OBall-center eps>0)

  \func toPseudoNormed : ExPseudoNormedAbGroup \cowith
    | AbGroup => \this
    | norm => meas
    | norm_zro => meas_zro
    | norm_negative => pmap meas negative=id
    | norm_+ => meas_+
}

\lemma meas-<=<-ball {X : PremeasureRing} {x : X} {U : Set X} (x<=<U : single x <=< U) : ∃ (a : X) (eps : `> ) (X.OBall a eps x ⊆ U)
  => \case X.interior x<=<U \with {
    | inP (a,eps,eps>0,h) => inP (a, eps, eps>0, \lam {y} p => <=<_<= (h p) idp)
  }

\class MeasureRing \extends PremeasureRing, SeparatedCoverSpace {
  | meas-ext {x : E} : meas x = ExUpperRealAbMonoid.zro -> x = 

  \default isSeparatedCoverSpace {x} {y} f => fromZero $ meas-ext $ ExUpperRealAbMonoid.<=-antisymmetric (\lam {b} b>0 => \case f $ makeCauchy $ topAbUniform (OBall-open (x - y)) $ OBall-center (RatField.half>0 b>0) \with {
    | inP (_, inP (z,idp), (Ux,Uy)) => transport2 (\lam x y => ExUpperReal.U {meas x} y) (inv ldistr *> pmap (_ *) (equation.abMonoid {double=0,negative=id}) *> isBooleanRing) linarith $ ExUpperReal.<=_+-char meas_+ Ux Uy
  }) meas>=0
  \default meas-ext p => isSeparatedCoverSpace $ SeparatedCoverSpace.separated-char   \lam x<=<U => \case meas-<=<-ball x<=<U \with {
    | inP (a,eps,eps>0,h) => h $ transportInv (ExUpperReal.U {__} _) {_} {} (ExUpperRealAbMonoid.<=-antisymmetric (meas-mono meet-right ExUpperRealAbMonoid.<=∘ =_<= (pmap meas zro-right *> p)) meas>=0) eps>0
  }

  \func toNormed : ExNormedAbGroup \cowith
    | ExPseudoNormedAbGroup => toPseudoNormed
    | norm-ext => meas-ext
}

\lemma meas-modular {X : PremeasureRing} {x y : X} : meas x + meas y = meas (x ∨ y) + meas (x ∧ y)
  => pmap (_ +) (pmap meas (later $ split *> pmap (_ ∨) *-comm) *> meas-disjoint (inv *-assoc *> pmap (`* y) diff_* *> X.zro_*-left)) *> inv +-assoc *> inv (pmap (`+ _) $ pmap meas (<=-antisymmetric (join-univ join-left $ transportInv (`<= _) split $ join-univ join-right $ meet-right <=∘ join-left) $ join-univ join-left $ diff_<= <=∘ join-right) *> X.meas-disjoint (*-comm *> diff_*))

\lemma cauchyFilter-measure-char {X : PremeasureRing} {F : SetFilter X} : IsCauchyFilter F <-> ∀ a {eps : `> } ∃ (x : X) (F (X.OBall a eps x))
  => <->trans cauchyFilter-uniform-char $ later (\lam f a eps>0 => \case f $ X.topAbUniform (X.OBall-open a) (X.OBall-center eps>0) \with {
    | inP (_, inP (x, idp), FB) => inP (x, transport F (ext \lam y => pmap (\lam z => ExUpperReal.U {meas (a * z)} _) $ zro-left *> pmap (x +) negative=id) FB)
  }, \lam f Cu => \case neighborhood-uniform. Cu \with {
    | inP (U,Uo,U0,h) => \case Uo U0 \with {
      | inP (a,eps,eps>0,g) => \case f a eps>0 \with {
        | inP (x,Fx) => \case h x \with {
          | inP (V,CV,UV) => inP (V, CV, filter-mono Fx \lam {y} xy => UV $ g $ transportInv (\lam z => ExUpperReal.U {meas (a * z)} eps) (zro-left *> pmap (x +) negative=id) xy)
        }
      }
    }
  })

\class CompleteMeasureRing \extends MeasureRing, CompleteTopAbGroup {
  | isCompleteMeasure (F : ProperFilter E) : ∀ a {eps : `> } ∃ (x : E) (F (OBall a eps x)) -> ∃ (x : E) ∀ a {eps : `> } (F (OBall a eps x))

  \default isComplete F => \case isCompleteMeasure F (cauchyFilter-measure-char. F.isCauchyFilter) \with {
    | inP (x,h) => inP (x, \lam {U} x<=<U => \case meas-<=<-ball x<=<U \with {
      | inP (a,eps,eps>0,Up) => filter-mono (h a eps>0) Up
    })
  }
  \default isCompleteMeasure F Fc =>
    \have F' => \new CauchyFilter \this {
      | ProperFilter => F
      | isCauchyFilter => cauchyFilter-measure-char. Fc
    }
    \in \case isComplete (regCF F') \with {
      | inP (x,xF) => inP (x, \lam a eps>0 => regCF_<= {_} {F'} $ xF $ OBall-center_<=< eps>0)
    }

  \func toCompleteNormed : CompleteExNormedAbGroup \cowith
    | ExNormedAbGroup => toNormed
    | isCompleteMetric F Fc => \case isCompleteMeasure F (\lam a eps>0 => TruncP.map (Fc eps>0) \lam (x,Fx) => (x, filter-mono Fx \lam {y} => meas-mono $ meet-right <=∘ =_<= (pmap (x +) $ inv negative=id))) \with {
      | inP (x,h) => inP (x, \lam {eps} eps>0 => \case Fc {eps RatField.* ratio  } linarith \with {
        | inP (x0,F1) => filter-mono (filter-meet (filter-meet F1 $ h x0 {eps RatField.* ratio  } linarith) $ h x (RatField.half>0 eps>0)) \lam {y} ((p1,p2),p3) =>
          meas-mono (meet_<=' equation.bRing) $ transport ExUpperReal.U {_} {eps} linarith $ ExUpperReal.<=_+-char meas_+ (ExUpperReal.<=_+-char meas_+ p1 p2) p3
      })
    }
}