NormedRing

\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\import Arith.Real.InfReal
\import Arith.Real.UpperReal
\import Data.Or
\import Function.Meta
\import Logic
\import Meta
\import Operations
\import Order.Biordered
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.Product
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.Real
\import Topology.TopRing
\import Topology.UniformSpace
\import Topology.UniformSpace.Product
\open Monoid(pow)

\class ExPseudoNormedPseudoRing \extends BoundedExPseudoNormedAbGroup, TopSemigroup, PseudoRing
  | norm_*_<= {x y : E} : norm (x * y) <= norm x ExUpperReal.* norm y
  | *-cont => bilinear-locally-uniform (*) rdistr_- ldistr_- norm_*_<=

\lemma *-locally-uniform {X : ExPseudoNormedPseudoRing} : LocallyUniformMap (X ⨯ X) X (\lam s => s.1 * s.2)
  => bilinear-locally-uniform (*) X.rdistr_- X.ldistr_- norm_*_<=

\class PseudoNormedPseudoRing \extends ExPseudoNormedPseudoRing, PseudoNormedAbGroup

\lemma lnorm_*_<= {X : PseudoNormedPseudoRing} {x y : X} : lnorm (x * y) <= lnorm x * lnorm y
  => Real.<=-upper.2 $ transportInv (_ ExUpperReal.<=) (RealField.*-upper lnorm>=0 lnorm>=0) X.norm_*_<=

\class ExPseudoNormedRing \extends ExPseudoNormedPseudoRing, TopRing
  | norm_ide_<= : norm 1 <= ExUpperReal.fromRat 1

\lemma norm_<=_pow {X : ExPseudoNormedRing} {x : X} {n : Nat} : norm (pow x n) <= ExUpperRealSemigroup.pow (norm x) n \elim n
  | 0 => norm_ide_<=
  | suc n => norm_*_<= <=∘ ExUpperRealSemigroup.<=_* norm_<=_pow <=-refl

\lemma pow-cover {X : ExPseudoNormedRing} (n : Nat) : CoverMap X X (pow __ n) \elim n
  | 0 => CoverMap.const 1
  | suc n => *-locally-uniform CoverMap.∘ ProductCoverSpace.tuple (pow-cover n) CoverMap.id

\class CompleteExNormedRing \extends ExPseudoNormedRing, CompleteExNormedAbGroup

\class PseudoNormedRing \extends ExPseudoNormedRing, PseudoNormedPseudoRing

\lemma lnorm_ide_<= {X : PseudoNormedRing} : X.norm 1 <= 1
  => Real.<=-upper.2 (later norm_ide_<=)

-- | If the norm of 1 is zero, then all bounded elements have zero norm.
\lemma norm_ide=0 {X : ExPseudoNormedRing} (p : X.norm 1 = 0) {x : X} (xb : (norm x).IsBounded) : norm x = 0 \elim xb
  | inP (B,x<B) => pmap norm (inv ide-right) *> <=-antisymmetric (norm_*_<= <=∘ ExUpperRealSemigroup.<=_* (ExUpperReal.<_<= x<B) <=-refl <=∘ =_<= (pmap (B ExUpperRealSemigroup.*) p *> ExUpperReal.*-rat (<=-less $ norm>=0 x<B) <=-refl *> pmap ExUpperReal.fromRat RatField.zro_*-right)) norm>=0

-- | If the norm of 1 is less than 1, then it is zero.
\lemma norm_ide<1 {X : ExPseudoNormedRing} (|1|<1 : (X.norm 1).U 1) : X.norm 1 = 0
  => <=-antisymmetric (\case U-rounded |1|<1 \with {
    | inP (q,|1|<q,q<1) => \lam {eps} eps>0 =>
      \have R => rat_<1_pow-bound q<1 {eps} eps>0
      \in U-closed (aux (norm>=0 |1|<q) q<1 |1|<q) R.2
  }) norm>=0
  \where {
    \protected \lemma aux {q : Rat} (q>0 : q > 0) (q<1 : q < 1) (p : (X.norm 1).U q) {n : Nat} : (X.norm 1).U (pow q n) \elim n
      | 0 => U-closed p q<1
      | suc n => transport (norm __ <= _) ide-left X.norm_*_<= $ ExUpperReal.*_U_<=.2 $ inP (pow q n, aux q>0 q<1 p, RatField.pow>0 q>0, q, p, q>0, <=-refl)
  }

-- | If the norm of 1 is non-zero, then it equals 1.
\lemma norm_ide/=0 {X : ExPseudoNormedRing} (p : X.norm 1 /= 0) : X.norm 1 = 1
  => <=-antisymmetric norm_ide_<= \lam {b} |1|<b => \case LinearOrder.dec<_<= (1 : Rat) b \with {
    | inl r => r
    | inr b<=1 => absurd $ p $ norm_ide<1 $ ExUpperReal.U_<= |1|<b b<=1
  }

\lemma norm_ide-left {X : ExPseudoNormedRing} {x : X} : X.norm 1 * norm x = norm x
  => <=-antisymmetric (transport (_ <=) (ExUpperRealSemigroup.ide-left norm>=0) $ ExUpperRealSemigroup.<=_* norm_ide_<= <=-refl) (transport (norm __ <= _) ide-left norm_*_<=)

\lemma norm_ide-right {X : ExPseudoNormedRing} {x : X} : X.norm x * X.norm 1 = norm x
  => <=-antisymmetric (transport (_ <=) (ExUpperRealSemigroup.ide-right norm>=0) $ ExUpperRealSemigroup.<=_* <=-refl norm_ide_<=) (transport (norm __ <= _) ide-right norm_*_<=)

-- | The norm of 1 is either 0 or 1.
\lemma norm_zro_ide {X : PseudoNormedRing} : (X.norm 1 = (0 : Real)) || (X.norm 1 = (1 : Real))
  => \case LU-located {X.norm 1} {0} {1} idp \with {
    | byLeft p => byRight $ Real.=-upper.2 $ later $ norm_ide/=0 \lam q => \case rewrite ((Real.=-upper {X.norm 1} {0}).2 q) p
    | byRight p => byLeft $ Real.=-upper.2 $ later $ norm_ide<1 p
  }

\lemma lnorm_<=_pow {X : PseudoNormedRing} {x : X} {n : Nat} : lnorm (pow x n) <= pow (lnorm x) n \elim n
  | 0 => lnorm_ide_<=
  | suc n => lnorm_*_<= <=∘ RealField.<=_*_positive-left lnorm_<=_pow lnorm>=0

\class ExPseudoValuedPseudoRing \extends ExPseudoNormedPseudoRing
  | norm_* {x y : E} : norm (x * y) = norm x ExUpperReal.* norm y
  | norm_*_<= => =_<= norm_*

\lemma lnorm_* {X : PseudoValuedRing} {x y : X} : lnorm (x * y) = lnorm x * lnorm y
  => Real.=-upper.2 $ later norm_* *> inv (RealField.*-upper lnorm>=0 lnorm>=0)

\class ExPseudoValuedRing \extends ExPseudoValuedPseudoRing, ExPseudoNormedRing, Ring {
  | norm_ide : norm 1 = ExUpperReal.fromRat 1
  | norm_ide_<= => =_<= norm_ide

  \lemma norm_Inv-cancel-left {x : E} (d : Monoid.Inv x) {y z : ExUpperReal} (y>=0 : 0 <= y) (z>=0 : 0 <= z) (p : norm x ExUpperRealSemigroup.* y = norm x ExUpperRealSemigroup.* z) : y = z
    => inv (pmap (ExUpperRealSemigroup.`* _) (inv norm_* *> pmap norm d.inv-left *> norm_ide) *> ExUpperRealSemigroup.ide-left y>=0) *> ExUpperRealSemigroup.*-assoc *> pmap (ExUpperRealSemigroup.* _) p *> inv ExUpperRealSemigroup.*-assoc *> pmap (ExUpperRealSemigroup.`* _) (inv norm_* *> pmap norm d.inv-left *> norm_ide) *> ExUpperRealSemigroup.ide-left z>=0

  \lemma norm_Inv-cancel-right {x y : ExUpperReal} (x>=0 : 0 <= x) (y>=0 : 0 <= y) {z : E} (d : Monoid.Inv z) (p : x ExUpperRealSemigroup.* norm z = y ExUpperRealSemigroup.* norm z) : x = y
    => norm_Inv-cancel-left d x>=0 y>=0 (*-comm *> p *> *-comm)
}

\lemma norm_pow {X : ExPseudoValuedRing} {x : X} {n : Nat} : norm (pow x n) = ExUpperRealSemigroup.pow (norm x) n \elim n
  | 0 => norm_ide
  | suc n => norm_* *> pmap (`* _) norm_pow

\class PseudoValuedRing \extends PseudoNormedRing, ExPseudoValuedRing

\lemma lnorm_ide {X : PseudoValuedRing} : X.norm 1 = 1
  => (Real.=-upper {_} {1}).2 (later norm_ide)

\lemma lnorm_pow {X : PseudoValuedRing} {x : X} {n : Nat} : lnorm (pow x n) = pow (lnorm x) n \elim n
  | 0 => lnorm_ide
  | suc n => lnorm_* *> pmap (`* _) lnorm_pow

\func RatValue => ExPseudoValuedRing { | E => Rat | * => RatField.* | ide => RatField.ide | + => RatField.+ | negative => RatField.negative }

\instance RatValuedRing : PseudoValuedRing Rat
  | PseudoNormedAbGroup => RatNormed
  | Ring => RatField
  | norm_* => pmap ExUpperReal.fromRat RatField.abs_* *> inv (ExUpperReal.*-rat RatField.abs>=0 RatField.abs>=0)
  | norm_ide => idp

\class CompleteValuedRing \extends PseudoValuedRing, CompleteExNormedRing, CompleteNormedAbGroup

\class CompleteValuedCRing \extends CompleteValuedRing, CRing

\instance RealValuedRing : CompleteValuedCRing Real
  | CompleteNormedAbGroup => RealNormed
  | CRing => RealField
  | norm_* => Real.=-upper.1 RealField.abs_* *> RealField.*-upper RealAbGroup.abs>=0 RealAbGroup.abs>=0
  | norm_ide => RealField.abs-ofPos $ LinearOrder.<_<= RealAbGroup.zro<ide