\import Algebra.Group
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.QModule
\import Algebra.Ring
\import Algebra.Ring.Reduced
\import Algebra.Semiring
\import Algebra.StrictlyOrdered
\import Arith.Complex
\import Arith.Complex.Norm
\import Arith.Nat
\import Arith.Real
\import Arith.Real.Field
\import Arith.Real.Root
\import Arith.Real.UpperReal
\import Function.Meta
\import Logic
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Arith.Rat
\import Order.Lattice
\import Set.Filter
\import Set.Set
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.MetricSpace
\import Topology.BanachAlgebra
\import Topology.BanachSpace
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.Real
\import Topology.NormedRing
\import Topology.StoneCStarAlgebra (RealStoneC*Algebra_fromRat)
\open Monoid (pow)
\open AddMonoid (*n)
\open LatticeAbGroup

{- | Reverse one-sided inequality: $|c| \leq |\Re c| + |\Im c|$. Combined with
     `abs_re_<=` / `abs_im_<=` this exhibits $|\cdot|$ and the product sup-norm
     as equivalent (within a factor of 2), which is the load-bearing fact for
     any cover-space equivalence between $\mathbb{C}$ and $\mathbb{R} \times \mathbb{R}$. -}
\lemma cabs_<=_re_+_im {c : Complex} : cabs c <= abs c.re + abs c.im
  => \have | sum>=0 :  <= abs c.re + abs c.im
              => linarith (abs>=0 {_} {c.re}, abs>=0 {_} {c.im})
           | abs_re_sq : abs c.re * abs c.re = c.re * c.re
              => inv RealField.abs_* *> abs-ofPos RealField.square_>=0
           | abs_im_sq : abs c.im * abs c.im = c.im * c.im
              => inv RealField.abs_* *> abs-ofPos RealField.square_>=0
           | cross>=0 :  <= abs c.re * abs c.im
              => RealField.<=_*_positive_positive abs>=0 abs>=0
           | rhs-expand : (abs c.re + abs c.im) * (abs c.re + abs c.im)
                        = abs c.re * abs c.re +  * (abs c.re * abs c.im) + abs c.im * abs c.im
              => equation.cRing
           | sq-bound : cabs c * cabs c <= (abs c.re + abs c.im) * (abs c.re + abs c.im)
              => transport (<= _) (inv cabs-square) linarith
     \in square_<=-cancel cabs>=0 sum>=0 sq-bound

{- | Completeness of $\mathbb{C}$ via $\Re$ / $\Im$ pushforward to $\mathbb{R}$
     (which is complete). For a Complex Cauchy filter $F$: push forward via
     $\Re$ and $\Im$ to get Real Cauchy filters, each converging to some
     $r_0$ / $i_0$ by Real completeness; the witness is
     $\mathrm{mkComplex}\,(r_0, i_0)$. The convergence proof bounds Complex
     $\varepsilon$-neighborhoods by Real $\varepsilon/2$-rectangles via
     `abs_<=_re_+_im`, then filter-meet on the two Real preimages. -}
\instance ComplexComplete : CompleteExNormedAbGroup
  | ExNormedAbGroup => ComplexNormed
  | isCompleteMetric F balls =>
    \let | F' => \new CauchyFilter ComplexNormed {
                   | ProperFilter => F
                   | isCauchyFilter => cauchyFilter-metric-char. balls
                 }
         | Fr : CauchyFilter RealNormed => Re.func-cauchy F'
         | Fi : CauchyFilter RealNormed => Im.func-cauchy F'
         | (inP (r0, hr)) => RealNormed.isComplete (regCF Fr)
         | (inP (i0, hi)) => RealNormed.isComplete (regCF Fi)
    \in inP (\new Complex r0 i0, \lam {eps} eps>0 =>
          \let | h>0 => RatField.half>0 eps>0
               | hr2 : F (Re ^-1 OBall (RatField.half eps) r0)
                  => regCF_<= {_} {Fr} (hr (OBall-center_<=< h>0))
               | hi2 : F (Im ^-1 OBall (RatField.half eps) i0)
                  => regCF_<= {_} {Fi} (hi (OBall-center_<=< h>0))
          \in filter-mono (filter-meet hr2 hi2) \lam {c} (re_in, im_in) =>
            \have | step1 : cabs ((\new Complex r0 i0) - c) ExUpperRealAbMonoid.<= RealField.abs (r0 - c.re) ExUpperReal.+ RealField.abs (i0 - c.im)
                      => transport (_ ExUpperRealAbMonoid.<=) RealAbGroup.+-upper $ Real.<=-upper. $ cabs_<=_re_+_im {(\new Complex r0 i0) - c}
                  | step2 : (RealField.abs (r0 - c.re) ExUpperReal.+ RealField.abs (i0 - c.im)).U eps
                      => ExUpperReal.+_U_<=. $ inP (RatField.half eps, re_in, RatField.half eps, im_in, linarith)
            \in step1 step2)

{- | $\mathbb{C}$ as a complete extended-normed ring. Follows directly from the
     ring and metric-completeness instances above. -}
\instance ComplexCompleteRing : CompleteExNormedRing
  | ExPseudoNormedRing => ComplexValuedRing
  | CompleteExNormedAbGroup => ComplexComplete

{- | Norm doubling: $|c + c| = 2|c|$. The load-bearing inequality
     $\|c\| + \|c\| \leq \|c + c\|$ of `RealPreBanachSpace.norm-double`. -}
\lemma cabs_+-double {c : Complex} : cabs c + cabs c = cabs (c + c)
  => \have | abs2-cc : cabs2 (c + c) =  * cabs2 c => equation.cRing
           | lhs-sq : (cabs c + cabs c) * (cabs c + cabs c) =  * cabs2 c
              => equation.cRing *> {Real} pmap ( *) (cabs-square {c})
           | rhs-sq : cabs (c + c) * cabs (c + c) =  * cabs2 c
              => cabs-square {c + c} *> abs2-cc
     \in sqrt-cancel (linarith (cabs>=0 {c})) (cabs>=0 {c + c}) (lhs-sq *> inv rhs-sq)

{- | $\mathbb{C}$ as a real Banach algebra. Caps the Step-2 chain:
     `ComplexCompleteRing` plus `isDivisible` (componentwise via
     `complex-div-cancel`) and `norm-double` (Real-form `abs_+-double` lifted
     to `ExUpperReal`). -}
\instance ComplexBanach : RealBanachAlgebra Complex
  | CompleteExNormedRing => ComplexCompleteRing
  | isDivisible a {n} n/=0 => inP (\new Complex (RatField.finv n *c a.re) (RatField.finv n *c a.im), complex-div-cancel n/=0)
  | norm-double {c} => =_<= (inv RealAbGroup.+-upper *> Real.=-upper. cabs_+-double)
  \where {
    {- | Divisibility helper for `RealPreBanachSpace.isDivisible` on $\mathbb{C}$:
         dividing each component by $n$ in $\mathbb{R}$ and then $n \cdot n$-ing
         recovers the original. -}
    \lemma real-div-cancel {x : Real} {n : Nat} (n/=0 : n /= ) : n *n (RatField.finv n *c x) = x
      => inv RealField.natCoef_*c *> inv *c-assoc *> pmap (*c x) (RatField.finv-right $ natRat/=0 n/=0) *> ide_*c

    {- | Componentwise extension to $\mathbb{C}$: dividing each component of $a$
         by $n$ and then applying $n \cdot n$ recovers $a$. The action $n \cdot n\,c$
         for Complex is componentwise via `Re` / `Im`'s `func-*n` (each being an
         `AddGroupHom`). -}
    \lemma complex-div-cancel {a : Complex} {n : Nat} (n/=0 : n /= )
      : n *n (\new Complex (RatField.finv n RealField.*c a.re) (RatField.finv n RealField.*c a.im)) = a
      => ext (Re.func-*n *> real-div-cancel n/=0, Im.func-*n *> real-div-cancel n/=0)
  }

-- | {conj} fixes $\mathrm{fromRat}\ r$ on `ComplexBanach`.
\lemma conj_fromRat {r : Rat} : conj (ComplexBanach.fromRat r) = ComplexBanach.fromRat r
  => func-*q {_} {_} {conjAddHom} *> pmap (r QModule.*q) conj_ide

\lemma complexBanach-fromRat {r : Rat} : ComplexBanach.fromRat r = Complex.fromReal (Real.fromRat r)
  => inv (func-*q {_} {_} {fromRealMap}) *> pmap Complex.fromReal (RealStoneC*Algebra_fromRat r)