\import Algebra.Group
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Module.LinearMap
\import Algebra.Monoid
\import Algebra.Pointed
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Operations
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.Subset
\import Topology.TopAbGroup
\import Topology.TopModule
\import Topology.TopRing
\import Topology.TopSpace
\import Topology.TopSpace.Product
\open IsDerivQuot
\open ContMap
\open ProductTopSpace

\func IsDerivQuot {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {U : Set X} (f : Set.Total U -> Y) (f' : DerivDom U -> Y) : \Prop
  => ∀ {x : X} (Ux : U x) {h : R} {a : X} (Ua : U (x + h *c a)) (h *c f' ((x,(h,a)),(Ux,Ua)) = f (x + h *c a, Ua) - f (x,Ux))
  \where {
    \func DerivDom (U : Set X) => TopSub {X ⨯ (RingTopLModule R ⨯ X)} \lam s => \Sigma (U s.) (U (s. + s.. *c s..))

    \protected \lemma unique (f : Set.Total U -> Y) (Uo : isOpen U) (f'1 f'2 : ContMap (DerivDom U) Y) (d1 : IsDerivQuot f f'1) (d2 : IsDerivQuot f f'2) {s : DerivDom U} : f'1 s = f'2 s \elim s
      | ((x,(h,a)),(Ux,Ua)) =>
          \have ec => TopTransfer-lift (tuple (const x) (tuple id (const a)) ∘ TopTransfer-map __.) (\lam h => later (Ux,h.))
          \in nearField-map-unique (func-cont {+-cont ∘ tuple (const x) (*c-cont ∘ tuple id (const a))} Uo) (f'1 ∘ ec) (f'2 ∘ ec) (\lam Uh => d1 Ux Uh *> inv (d2 Ux Uh)) Ua

    \lemma isDeriv (f : Set.Total U -> Y) (f' : ContMap (DerivDom U) Y) (Uo : isOpen U) (d : HasDeriv Uo f) (c : IsDerivQuot f f') {x : X} (Ux : U x) (a : X)
      : deriv Uo f d (x,Ux) a = f' ((x,(,a)), deriv.atZero {R} {X} {U} {x,Ux})
      => unique f Uo (deriv-quot.deriv-tuple Uo f d). f' (deriv-quot.deriv-tuple Uo f d). c
  }

\func HasDeriv {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {U : Set X} (Uo : isOpen U) (f : Set.Total U -> Y)
  => ∃ (f' : ContMap (DerivDom U) Y) (IsDerivQuot f f')

\lemma HasDeriv-cont {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {U : Set X} {Uo : isOpen U}
                     {f : Set.Total U -> Y} (d : HasDeriv Uo f) : ContMap (TopSub U) Y f \cowith
  | func-cont {V} Vo => \case \elim d \with {
    | inP (f',f'd) => TopSpace.cover-open {TopSub U} \lam {x} Vfx =>
        \have fc : ContMap (TopSub U) Y f => transport (ContMap (TopSub U) Y)
            (ext \lam y => pmap (`+ _) (inv ide_*c *> f'd x. (\box rewrite ide_*c $ simplify y.)) *> simplify (pmap f $ ext $ rewrite ide_*c simplify))
            (+-cont ∘ tuple (f' ∘ TopSub-func (tuple (const x.) (tuple (const ) (+-cont ∘ tuple id (const (negative x.))))) \lam {y} Uy => unfold (x., rewrite ide_*c $ simplify Uy)) (const (f x)))
        \in inP (f ^-1 V, fc.func-cont Vo, Vfx, <=-refl)
  }

\func deriv-quot {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {U : Set X} (Uo : isOpen U) (f : Set.Total U -> Y) (d : HasDeriv Uo f) (x : DerivDom U) : Y
  => (deriv-tuple Uo f d). x
  \where {
    \lemma deriv-tuple {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {U : Set X} (Uo : isOpen U) (f : Set.Total U -> Y) (d : HasDeriv Uo f)
      : \Sigma (f' : ContMap (DerivDom U) Y) (IsDerivQuot f f')
        \level \lam u v => ext $ exts \lam s => IsDerivQuot.unique f Uo u. v. u. v. \elim d
      | inP r => r
  }

\lemma deriv-isQuot {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {U : Set X} {Uo : isOpen U}
                    {f : Set.Total U -> Y} (d : HasDeriv Uo f) : IsDerivQuot f (deriv-quot Uo f d)
  => (deriv-quot.deriv-tuple Uo f d).

\lemma deriv-quot-cont {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {U : Set X} {Uo : isOpen U} {f : Set.Total U -> Y}
                       (gx : ContMap R X) (gh : ContMap R R) (ga : ContMap R X) (d : HasDeriv Uo f)
                       {V : Set R} (Vc : ∀ {h : V} Given (U (gx h)) (U (gx h + gh h *c ga h)))
  : ContMap (TopSub V) Y (\lam h => deriv-quot Uo f d ((gx h., (gh h., ga h.)), Vc h.))
  => (deriv-quot.deriv-tuple Uo f d). ∘ TopSub-func (tuple gx (tuple gh ga)) Vc

\func deriv {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {U : Set X} (Uo : isOpen U) (f : Set.Total U -> Y) (d : HasDeriv Uo f) (x : Set.Total U) : LinearMap X Y \cowith
  | func a => deriv-quot Uo f d ((x.,(,a)), atZero)
  | func-+ {a} {b} =>
    \have u3 {h} u => transport U (pmap (_ +) (X.*c-ldistr {h}) *> inv +-assoc) u
    \in nearField-map-unique (open-inter (func-cont {+-cont ∘ tuple (const x.) (*c-cont ∘ tuple id (const (a + b)))} Uo)
                                         (func-cont {+-cont ∘ tuple (const x.) (*c-cont ∘ tuple id (const a))} Uo))
          (deriv-quot-cont (const x.) id (const (a + b)) d \lam u => later (x., u.))
          (+-cont ∘ tuple (deriv-quot-cont (const x.) id (const a) d \lam u => later (x., u.))
                          (deriv-quot-cont (+-cont ∘ tuple (const x.) (*c-cont ∘ tuple id (const a))) id (const b) d \lam u => later (u., u3 u.)))
          (\lam {h} u => deriv-isQuot d x. u. *> simplify (+-comm *> pmap (_ + f __) (ext $ pmap (_ +) *c-ldistr *> inv +-assoc)) *> inv (*c-ldistr *> pmap2 (+) (deriv-isQuot d x. u.) (deriv-isQuot d u. (u3 u.))))
          {} (transportInv U (pmap (_ +) X.*c_zro-left *> zro-right) x., transportInv U (pmap (_ +) X.*c_zro-left *> zro-right) x.)
        *> pmap (_ + deriv-quot Uo f d __) (ext $ ext (pmap (_ +) X.*c_zro-left *> zro-right, idp))
  | func-*c {r} {a} => (unfold, unfold, unfold, rewrite R.zro_*-left) in nearField-map-unique (func-cont {+-cont ∘ tuple (const x.) (*c-cont ∘ tuple id (const (r *c a)))} Uo)
                        (deriv-quot-cont (const x.) id (const (r *c a)) d \lam u => (x., u))
                        (*c-cont ∘ tuple (const r) (deriv-quot-cont (const x.) (*-cont ∘ tuple id (const r)) (const a) d \lam u => \box (x., transportInv (\lam y => U (x. + y)) *c-assoc u)))
                        (\lam u => deriv-isQuot d x. u *> pmap (f __ - _) (ext $ pmap (_ +) (inv *c-assoc)) *> inv (deriv-isQuot d x. $ transportInv (\lam y => U (x. + y)) *c-assoc u) *> *c-assoc)
                        {} (transportInv U (pmap (_ +) X.*c_zro-left *> zro-right) x.)
  \where {
    \protected \lemma atZero {x : Set.Total U} {a : X}
      => (((x.,(,a)), (x., transportInv U (pmap (_ +) X.*c_zro-left *> zro-right) x.)) : DerivDom U).
  }

\func HasTDeriv {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} (f : X -> Y)
  => HasDeriv open-top \lam s => f s.
  \where {
    \protected \lemma make (f' : ContMap (ProductTopSpace X (ProductTopSpace R X)) Y) (d : IsTDerivQuot f f') : HasTDeriv f
      => inP (f' ∘ TopTransfer-map __., \lam _ _ => d)
  }

\func tderiv-quot {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} (f : X -> Y) (d : HasTDeriv f) (x : X) (h : R) (a : X) : Y
  => deriv-quot open-top (\lam s => f s.) d ((x,(h,a)),((),()))

\func IsTDerivQuot {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} (f : X -> Y) (f' : \Sigma X (\Sigma R X) -> Y) : \Prop
  => ∀ {x : X} {h : R} {a : X} (h *c f' (x,(h,a)) = f (x + h *c a) - f x)
  \where {
    \lemma isTDeriv (f' : ContMap (ProductTopSpace X (ProductTopSpace R X)) Y) (d : HasTDeriv f) (c : IsTDerivQuot f f') (x a : X) : tderiv f d x a = f' (x,(,a))
      => IsDerivQuot.isDeriv _ (f' ∘ TopTransfer-map __.) open-top d (\lam _ _ => c) () a
  }

\lemma tderiv-isQuot {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {f : X -> Y} (d : HasTDeriv f) {x : X} {h : R} {a : X}
  : h *c tderiv-quot f d x h a = f (x + h *c a) - f x
  => deriv-isQuot d () ()

\lemma tderiv-quot-cont {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {f : X -> Y}
                        (gx : ContMap R X) (gh : ContMap R R) (ga : ContMap R X) (d : HasTDeriv f)
  : ContMap R Y (\lam h => tderiv-quot f d (gx h) (gh h) (ga h))
  => deriv-quot-cont gx gh ga d {top} (\lam _ => ((),())) ∘ TopTransfer-lift id (\lam _ => ())

\func tderiv {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} (f : X -> Y) (d : HasTDeriv f) (x : X) : LinearMap X Y
  => deriv open-top (\lam s => f s.) d (x,())

\lemma deriv_linear {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} (f : LinearMap X Y) (fc : ContMap X Y f) (x a : X) : tderiv f has_deriv x a = f a
  => IsTDerivQuot.isTDeriv (fc ∘ proj2 ∘ proj2) has_deriv deriv-quot_linear x a
  \where {
    \lemma deriv-quot_linear : IsTDerivQuot f (\lam s => f s..)
      => \lam {x} {h} {a} => inv $ pmap (`- _) f.func-+ *> simplify f.func-*c

    \lemma has_deriv : HasTDeriv f
      => HasTDeriv.make (fc ∘ proj2 ∘ proj2) deriv-quot_linear
  }

\lemma deriv_const {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} (y : Y) (x a : X) : tderiv (\lam _ => y) has_deriv x a = 
  => IsTDerivQuot.isTDeriv (const ) has_deriv deriv-quot_const x a
  \where {
    \lemma deriv-quot_const : IsTDerivQuot {R} {X} (\lam _ => y) (\lam _ => )
      => \lam {x} {h} {a} => Y.*c_zro-right *> inv negative-right

    \lemma has_deriv : HasTDeriv {R} {X} (\lam _ => y)
      => HasTDeriv.make (const ) deriv-quot_const
  }

\lemma deriv_+ {R : NearSkewField} {X : TopLModule R} {Y : HausdorffTopLModule R} {U : Set X} (Uo : isOpen U)
               (f g : Set.Total U -> Y) (d1 : HasDeriv Uo f) (d2 : HasDeriv Uo g) {x : X} (Ux : U x) (a : X)
  : deriv Uo (\lam x => f x + g x) has_deriv (x,Ux) a = deriv Uo f d1 (x,Ux) a + deriv Uo g d2 (x,Ux) a
  => IsDerivQuot.isDeriv (\lam x => f x + g x) isCont Uo has_deriv deriv-quot_+ Ux a
  \where {
    \lemma deriv-quot_+ : IsDerivQuot (\lam x => f x + g x) (\lam s => deriv-quot Uo f d1 s + deriv-quot Uo g d2 s) =>
      \lam Ux Ua => *c-ldistr *> pmap2 (+) (deriv-isQuot d1 Ux Ua) (deriv-isQuot d2 Ux Ua) *> equation *> pmap (_ +) (inv AddGroup.negative_+)

    \lemma isCont => +-cont ∘ tuple (deriv-quot.deriv-tuple Uo f d1). (deriv-quot.deriv-tuple Uo g d2).

    \lemma has_deriv : HasDeriv Uo (\lam x => f x + g x)
      => inP (isCont, deriv-quot_+)
  }

\lemma deriv_*c {R : NearField} {X : TopLModule R} {Y : HausdorffTopLModule R} {U : Set X} (Uo : isOpen U)
                     (f : Set.Total U -> Y) (d : HasDeriv Uo f) (c : R) {x : X} (Ux : U x) (a : X)
  : deriv Uo (\lam x => c *c f x) has_deriv (x,Ux) a = c *c deriv Uo f d (x,Ux) a
  => IsDerivQuot.isDeriv (\lam x => c *c f x) isCont Uo has_deriv deriv-quot_*c Ux a
  \where {
    \lemma deriv-quot_*c : IsDerivQuot (\lam x => c *c f x) (\lam s => c *c deriv-quot Uo f d s)
      => \lam Ux Ua => inv *c-assoc *> pmap (`*c _) *-comm *> *c-assoc *> pmap (c *c) (deriv-isQuot d Ux Ua) *> Y.*c-ldistr_-

    \lemma isCont => *c-cont ∘ tuple (const c) (deriv-quot.deriv-tuple Uo f d).

    \lemma has_deriv : HasDeriv Uo (\lam x => c *c f x)
      => inP (isCont, deriv-quot_*c)
  }

\lemma deriv-quot_bilinear {R : NearSkewField} {X : TopLModule R} {X1 X2 Y : HausdorffTopLModule R} {U : Set X} (Uo : isOpen U)
                           (b : BilinearMap X1 X2 Y) (f : Set.Total U -> X1) (g : Set.Total U -> X2) (d1 : HasDeriv Uo f) (d2 : HasDeriv Uo g)
  : IsDerivQuot (\lam x => b (f x) (g x)) (\lam s => b (deriv-quot Uo f d1 s) (g (s.. + s... *c s..., s..)) + b (f (s..,s..)) (deriv-quot Uo g d2 s))
  => \lam Ux Ua => *c-ldistr *> pmap2 (+) (inv b.linear-left.func-*c *> pmap (b __ _) (deriv-isQuot d1 Ux Ua) *> b.linear-left.func-minus)
                                          (inv b.linear-right.func-*c *> pmap (b _) (deriv-isQuot d2 Ux Ua) *> b.linear-right.func-minus) *> simplify