\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Reduced
\import Algebra.Semiring
\import Algebra.StrictlyOrdered
\import Arith.Complex
\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
\open Monoid (pow)
\open AddMonoid (*n)
\open Complex \using (iunit \as i)

{- | Squared modulus: $|z|^2 = (\Re z)^2 + (\Im z)^2$. Avoiding the sqrt keeps
     algebraic identities (multiplicativity, Cauchy–Schwarz) pure polynomial. -}
\func cabs2 (z : Complex) : Real
  => z.re * z.re + z.im * z.im

\lemma cabs2>=0 {z : Complex} : ( : Real) <= cabs2 z
  => linarith (RealField.square_>=0 {z.re}, RealField.square_>=0 {z.im})

\lemma cabs2_zro : cabs2 (zro : Complex) = ( : Real)
  => simplify

\lemma cabs2_ide : cabs2 (ide : Complex) = ( : Real)
  => simplify

\lemma cabs2_negative {z : Complex} : cabs2 (negative z) = cabs2 z
  => simplify

{- | The key polynomial identity: $|xy|^2 = |x|^2 \cdot |y|^2$.
     Proof reduces to
     $$(\Re x \cdot \Re y - \Im x \cdot \Im y)^2 + (\Re x \cdot \Im y + \Im x \cdot \Re y)^2
       = ((\Re x)^2 + (\Im x)^2)((\Re y)^2 + (\Im y)^2)$$
     which holds by ring algebra. -}
\lemma cabs2_* {x y : Complex} : cabs2 (x * y) = cabs2 x * cabs2 y
  => equation.cRing

{- | Brahmagupta–Fibonacci / 2-square identity, in the form needed for Cauchy–Schwarz:
     $$((\Re x)^2 + (\Im x)^2)((\Re y)^2 + (\Im y)^2) - (\Re x \cdot \Re y + \Im x \cdot \Im y)^2
       = (\Re x \cdot \Im y - \Im x \cdot \Re y)^2.$$ -}
\lemma cabs2_*_CS {x y : Complex}
  : cabs2 x * cabs2 y - (x.re * y.re + x.im * y.im) * (x.re * y.re + x.im * y.im) =
    (x.re * y.im - x.im * y.re) * (x.re * y.im - x.im * y.re)
  => equation.cRing

{- | Cauchy–Schwarz at the squared level:
     $(\Re x \cdot \Re y + \Im x \cdot \Im y)^2 \leq |x|^2 \cdot |y|^2$. -}
\lemma CS_<= {x y : Complex}
  : (x.re * y.re + x.im * y.im) * (x.re * y.re + x.im * y.im) <= cabs2 x * cabs2 y
  => linarith (cabs2_*_CS {x} {y}, RealField.square_>=0 {x.re * y.im - x.im * y.re})

{- | Modulus: $|z| = \sqrt{(\Re z)^2 + (\Im z)^2}$. -}
\func cabs (z : Complex) : Real
  => sqrt (cabs2 z)

\lemma cabs>=0 {z : Complex} :  <= cabs z
  => sqrt>=0

\lemma cabs_zro : cabs  = 
  => pmap sqrt cabs2_zro *> sqrt_zro

\lemma cabs_ide : cabs  = 
  => pmap sqrt cabs2_ide *> sqrt_ide

\lemma cabs_negative {z : Complex} : cabs (negative z) = cabs z
  => pmap sqrt cabs2_negative

\lemma cabs-square {z : Complex} : cabs z * cabs z = cabs2 z
  => pow_sqrt cabs2>=0

{- | $|\mathrm{fromReal}\ x| = |x|$. The complex modulus of a real-line embedding
     reduces to the real absolute value via $|\mathrm{fromReal}\ x|^2 = x^2$ plus
     $\sqrt{x^2} = |x|$. -}
\lemma cabs_fromReal {x : Real} : cabs x = RealField.abs x
  => simplify *> sqrt_pow_abs

{- | Modulus is multiplicative: $|xy| = |x| \cdot |y|$. Reduce to the squared version
     $|xy|^2 = (|x| \cdot |y|)^2$ and use that both sides are nonneg square roots of the
     same value. -}
\lemma cabs_* {x y : Complex} : cabs (x * y) = cabs x * cabs y
  => sqrt-cancel (cabs>=0 {x * y}) (RealField.<=_*_positive_positive cabs>=0 cabs>=0) $ cabs-square {x * y}
      *> cabs2_*
      *> pmap2 (*) (inv cabs-square) (inv cabs-square)
      *> {Real} equation.cRing

{- | Square-monotonicity inverse on nonneg reals: $s^2 \leq t^2 \implies s \leq t$. -}
\lemma square_<=-cancel {s t : Real} (s>=0 :  <= s) (t>=0 :  <= t) (p : s * s <= t * t) : s <= t
  => \lam t<s => p $ transport2 (__ * t < __ * s) ide-left ide-left $
       RealField.pow_<-monotone {_} {_} {} suc/=0 t>=0 t<s

{- | Cauchy–Schwarz, linear form: $\Re x \cdot \Re y + \Im x \cdot \Im y \leq |x| \cdot |y|$.
     Goes through $|s|$ (real abs of the inner product), which has
     $|s|^2 = s^2 \leq (|x| \cdot |y|)^2$, then sqrt-cancels. -}
\private \lemma CS-linear {x y : Complex} : x.re * y.re + x.im * y.im <= cabs x * cabs y
  => \have | t>=0 :  <= cabs x * cabs y => RealField.<=_*_positive_positive cabs>=0 cabs>=0
           | abs_s_sq : RealField.abs (x.re * y.re + x.im * y.im) * RealField.abs (x.re * y.re + x.im * y.im)
                          = (x.re * y.re + x.im * y.im) * (x.re * y.re + x.im * y.im)
              => inv RealField.abs_* *> RealField.abs-ofPos RealField.square_>=0
           | tt-eq : cabs x * cabs y * (cabs x * cabs y) = cabs2 x * cabs2 y
              => equation.cRing *> {Real} pmap2 (*) cabs-square cabs-square
           | sq<=tt : RealField.abs (x.re * y.re + x.im * y.im) * RealField.abs (x.re * y.re + x.im * y.im)
                        <= cabs x * cabs y * (cabs x * cabs y)
              => transport2 (<=) (inv abs_s_sq) (inv tt-eq) CS_<=
           | abs_s<=t : RealField.abs (x.re * y.re + x.im * y.im) <= cabs x * cabs y
              => square_<=-cancel RealField.abs>=0 t>=0 sq<=tt
     \in RealField.abs>=id <=∘ abs_s<=t

{- | Triangle inequality $|x + y| \leq |x| + |y|$. Squared form:
     $$|x+y|^2 = |x|^2 + 2(\Re x \cdot \Re y + \Im x \cdot \Im y) + |y|^2
       \leq |x|^2 + 2|x||y| + |y|^2 = (|x|+|y|)^2.$$ -}
\lemma cabs_+ {x y : Complex} : cabs (x + y) <= cabs x + cabs y
  => \have | sum>=0 :  <= cabs x + cabs y => linarith (cabs>=0 {x}, cabs>=0 {y})
           | lhs_sq : cabs (x + y) * cabs (x + y) = cabs2 x + cabs2 y +  * (x.re * y.re + x.im * y.im)
              => cabs-square {x + y} *> {Real} equation.cRing
           | rhs_sq : (cabs x + cabs y) * (cabs x + cabs y) = cabs2 x + cabs2 y +  * (cabs x * cabs y)
              => equation.cRing *> {Real} pmap2 (__ + __ + _) cabs-square cabs-square
           | inner-bound : cabs2 x + cabs2 y +  * (x.re * y.re + x.im * y.im)
                        <= cabs2 x + cabs2 y +  * (cabs x * cabs y)
              => linarith (CS-linear {x} {y})
           | sq-bound : cabs (x + y) * cabs (x + y) <= (cabs x + cabs y) * (cabs x + cabs y)
              => transport2 (<=) (inv lhs_sq) (inv rhs_sq) inner-bound
     \in square_<=-cancel (cabs>=0 {x + y}) sum>=0 sq-bound

{- | Reverse of {cabs_zro}: $|c| = 0 \implies c = 0$. Since $|c|^2 = (\Re c)^2 + (\Im c)^2$
     and both squares are nonneg, the sum vanishing forces each to vanish, then field
     reducedness forces each component to zero. -}
\lemma cabs_zro-ext {c : Complex} (p : cabs c = ) : c = 
  => \have | abs2_c=0 : c.re * c.re + c.im * c.im = ( : Real)
              => inv cabs-square *> pmap (* cabs c) p *> RealField.zro_*-left
           | re2=0 : c.re * c.re = ( : Real)
              => linarith (RealField.square_>=0 {c.im}, RealField.square_>=0 {c.re})
           | im2=0 : c.im * c.im = ( : Real)
              => linarith (RealField.square_>=0 {c.im}, RealField.square_>=0 {c.re})
     \in ext (RealField.isReduced re2=0, RealField.isReduced im2=0)

{- | Complex numbers as a normed abelian group, with norm
     $|c| = \sqrt{(\Re c)^2 + (\Im c)^2}$. The metric, uniform, and topological
     structure are auto-derived from the norm. -}
\instance ComplexNormed : NormedAbGroup Complex
  | AbGroup => ComplexField
  | norm => cabs
  | norm_zro => Real.=-upper. cabs_zro
  | norm_negative => Real.=-upper. cabs_negative
  | norm_+ => transport (_ ExUpperRealAbMonoid.<=) RealAbGroup.+-upper $ Real.<=-upper. cabs_+
  | norm-ext {c} p => cabs_zro-ext $ (Real.=-upper {cabs c} {}). p

{- | Complex numbers as a pseudo-valued ring: multiplicative modulus
     $|xy| = |x| \cdot |y|$ plus $|1| = 1$. The ExPseudoNormedRing plumbing
     (`norm_*_<=`, `norm_ide_<=`, `*-cont` via the bilinear-locally-uniform
     default) all follow from these. -}
\instance ComplexValuedRing : PseudoValuedRing Complex
  | PseudoNormedAbGroup => ComplexNormed
  | Ring => ComplexField
  | norm_* => Real.=-upper. cabs_* *> RealField.*-upper cabs>=0 cabs>=0
  | norm_ide => Real.=-upper. cabs_ide

{- | Real part dominated by modulus: $|\Re c| \leq |c|$. Proved by squaring:
     $(|\Re c|)^2 = (\Re c)^2 \leq (\Re c)^2 + (\Im c)^2 = |c|^2$, then `square_<=-cancel`. -}
\lemma cabs_re_<= {c : Complex} : RealField.abs c.re <= cabs c
  => square_<=-cancel abs>=0 cabs>=0 $ transport2 (<=)
      (zro-right *> inv (RealField.abs-ofPos RealField.square_>=0) *> RealField.abs_*)
      (inv cabs-square)
      (<=_+ <=-refl RealField.square_>=0)

\lemma cabs_im_<= {c : Complex} : RealField.abs c.im <= cabs c
  => square_<=-cancel RealField.abs>=0 cabs>=0 $ transport2 (<=)
      (zro-left *> inv (RealField.abs-ofPos RealField.square_>=0) *> RealField.abs_*)
      (inv cabs-square)
      (<=_+ RealField.square_>=0 <=-refl)

{- | The real-part projection $\Re : \mathbb{C} \to \mathbb{R}$ as a
     non-expansive (1-Lipschitz) normed-group map. -}
\func Re : NormedAbGroupMap ComplexNormed RealNormed \cowith
  | func c => c.re
  | func-+ => idp
  | func-norm => Real.<=-upper. cabs_re_<=

{- | The imaginary-part projection $\Im : \mathbb{C} \to \mathbb{R}$ as a
     non-expansive (1-Lipschitz) normed-group map. -}
\func Im : NormedAbGroupMap ComplexNormed RealNormed \cowith
  | func c => c.im
  | func-+ => idp
  | func-norm => Real.<=-upper. cabs_im_<=

{- | $\mathrm{fromReal} : \mathbb{R} \to \mathbb{C}$ as an isometric normed-group
     map. Preserves addition (`fromReal_+`) and norm exactly (`abs_fromReal`),
     hence in particular a `CoverMap`. -}
\func fromRealMap : NormedIsometricMap RealNormed ComplexNormed Complex.fromReal \cowith
  | func-+ => fromReal_+
  | func-norm-isometry => Real.=-upper. cabs_fromReal

{- | $|i|^2 = 1$. By definition of `i` and ring arithmetic. -}
\lemma cabs2_i : cabs2 i = 
  => simplify

{- | $|i| = 1$. The imaginary unit has unit modulus. -}
\lemma abs_i : cabs i = 
  => pmap sqrt cabs2_i *> sqrt_ide

{- | $|i \cdot z| = |z|$. Follows from `abs_*` and $|i| = 1$. -}
\lemma cabs_i_* {z : Complex} : cabs (i * z) = cabs z
  => cabs_* *> pmap (* _) abs_i *> ide-left

{- | Multiplication by $i$ as an isometric normed-group map. -}
\func mulIMap : NormedIsometricMap ComplexNormed ComplexNormed (i *) \cowith
  | func-+ => ldistr
  | func-norm-isometry => Real.=-upper. cabs_i_*

{- | $|\overline{z}|^2 = |z|^2$. The imaginary part gets negated, but $(-x)^2 = x^2$. -}
\lemma cabs2_conj {z : Complex} : cabs2 (conj z) = cabs2 z
  => pmap (z.re * z.re +) (Ring.negative_*-left *> pmap negative Ring.negative_*-right *> AddGroup.negative-isInv)

{- | $|\overline{z}| = |z|$. The complex modulus is invariant under conjugation. -}
\lemma cabs_conj {z : Complex} : cabs (conj z) = cabs z
  => pmap sqrt cabs2_conj

{- | Conjugation $\overline{\cdot} : \mathbb{C} \to \mathbb{C}$ as an isometric
     normed-group map. -}
\func conjMap : NormedIsometricMap ComplexNormed ComplexNormed conj \cowith
  | func-+ => conj_+
  | func-norm-isometry => Real.=-upper. cabs_conj