:: Differentiability of Polynomials over Reals
::  by Artur Korni{\l}owicz
::
:: Received February 23, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies LATTICES, VECTSP_1, POLYNOM1, FDIFF_1, PARTFUN1, NUMBERS, REAL_1,
      RELAT_1, TARSKI, STRUCT_0, FUNCT_1, SUBSET_1, ALGSEQ_1, NAT_1, XXREAL_0,
      SUPINF_2, POLYNOM2, POLYNOM3, POLYNOM5, FUNCSDOM, ARYTM_3, FUNCT_4,
      NEWTON, CARD_1, FUNCT_7, MSAFREE2, MESFUNC1, FINSEQ_1, XBOOLE_0,
      CALCUL_2, PREPOWER, FUNCOP_1, VALUED_0, HURWITZ, ARYTM_1, AFINSQ_1,
      RCOMP_1, REALSET1, POLYNOM4, ORDINAL2, CARD_3, ORDINAL4, GROUP_1,
      VALUED_1, XCMPLX_0, SQUARE_1, ALGSTR_0, RLVECT_1, POLYDIFF;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0,
      XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NAT_1,
      NAT_D, FUNCT_7, NEWTON, PREPOWER, TAYLOR_1, FINSEQ_1, VALUED_0, VALUED_1,
      RCOMP_1, FCONT_1, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, GROUP_1,
      FUNCSDOM, ALGSEQ_1, POLYNOM1, VFUNCT_1, NORMSP_1, POLYNOM3, POLYNOM4,
      POLYNOM5, FDIFF_1, HURWITZ, RATFUNC1;
 constructors RELSET_1, FDIFF_1, BINOP_2, POLYNOM4, POLYNOM5, ALGSEQ_1,
      RATFUNC1, HURWITZ, FCONT_1, NAT_D, FUNCSDOM, RCOMP_1, PARTFUN2, FUNCT_7,
      VFUNCT_1, TAYLOR_1, PREPOWER, NEWTON, ALGSTR_1;
 registrations RELSET_1, FUNCT_2, VECTSP_1, STRUCT_0, XBOOLE_0, RELAT_1,
      FUNCT_1, NAT_1, XREAL_0, NUMBERS, XCMPLX_0, ORDINAL1, POLYNOM3, MEMBERED,
      FUNCOP_1, RATFUNC1, INT_1, POLYNOM5, FINSEQ_1, VALUED_1, VALUED_0,
      FDIFF_1, RCOMP_1, FCONT_3, FUNCT_7, POLYNOM4, VFUNCT_1, RLVECT_1,
      FINSET_1, MOEBIUS2, XXREAL_0, ALGSTR_1;
 requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;


begin :: Preliminaries

reserve c for Complex;
reserve r for Real;
reserve m,n for Nat;
reserve f for complex-valued Function;

theorem :: POLYDIFF:1
  0 + f = f;

theorem :: POLYDIFF:2
  f - 0 = f;

registration
  let f be complex-valued Function;
  reduce 0 + f to f;
  reduce f - 0 to f;
end;

theorem :: POLYDIFF:3
  c + f = ((dom f) --> c) + f;

theorem :: POLYDIFF:4
  f - c = f - ((dom f) --> c);

theorem :: POLYDIFF:5
  c (#) f = ((dom f) --> c) (#) f;

theorem :: POLYDIFF:6
  f + ((dom f) --> 0) = f;

theorem :: POLYDIFF:7
  f - ((dom f) --> 0) = f;

theorem :: POLYDIFF:8
  #Z 0 = REAL --> 1;

begin :: Differentiability of real functions

registration
  cluster differentiable -> continuous for Function of REAL,REAL;
end;

definition
  let f be differentiable Function of REAL,REAL;
  func f`| -> Function of REAL,REAL equals
:: POLYDIFF:def 1
  f `| REAL;
end;

theorem :: POLYDIFF:9
  for f being Function of REAL,REAL holds
  f is differentiable iff for r holds f is_differentiable_in r;

theorem :: POLYDIFF:10
  for f being differentiable Function of REAL,REAL holds f`|.r = diff(f,r);

definition
  let f be Function of REAL,REAL;
  redefine attr f is differentiable means
:: POLYDIFF:def 2
  for r holds f is_differentiable_in r;
end;

registration
  cluster constant -> differentiable for Function of REAL,REAL;
end;

theorem :: POLYDIFF:11
  for f being constant Function of REAL,REAL holds
  f`| = REAL --> 0;

registration
  cluster id REAL -> differentiable for Function of REAL,REAL;
end;

theorem :: POLYDIFF:12
  (id REAL)`| = REAL --> 1;

registration
  let n;
  cluster #Z n -> differentiable;
end;

theorem :: POLYDIFF:13
  ( #Z n) `| = n (#) #Z (n-1);

reserve f,g for differentiable Function of REAL,REAL;

registration
  let f,g;
  cluster f + g -> differentiable for Function of REAL,REAL;
  cluster f - g -> differentiable for Function of REAL,REAL;
  cluster f (#) g -> differentiable for Function of REAL,REAL;
end;

registration
  let f,r;
  cluster r+f -> differentiable for Function of REAL,REAL;
  cluster r(#)f -> differentiable for Function of REAL,REAL;
  cluster f-r -> differentiable for Function of REAL,REAL;
end;

registration
  let f;
  cluster -f -> differentiable for Function of REAL,REAL;
  cluster f^2 -> differentiable for Function of REAL,REAL;
end;

theorem :: POLYDIFF:14
  (f+g)`| = f`| + g`|;

theorem :: POLYDIFF:15
  (f-g)`| = f`| - g`|;

theorem :: POLYDIFF:16
  (f(#)g)`| = g(#)(f`|) + f(#)(g`|);

theorem :: POLYDIFF:17
  (r+f)`| = f`|;

theorem :: POLYDIFF:18
  (f-r)`| = f`|;

theorem :: POLYDIFF:19
  (r(#)f)`| = r(#)(f`|);

theorem :: POLYDIFF:20
  (-f)`| = -(f`|);

begin :: Polynomials

reserve L for non empty ZeroStr;
reserve x for Element of L;

theorem :: POLYDIFF:21
  for f being (the carrier of L)-valued Function
  for a being object holds
  Support(f+*(a,x)) c= Support f \/ {a};

registration
  let L,x;
  let f be finite-Support sequence of L;
  let a be object;
  cluster f+*(a,x) -> finite-Support for sequence of L;
end;

theorem :: POLYDIFF:22
  for p being Polynomial of L st p <> 0_.L holds len p-'1 = len p-1;

registration
  let L be non empty ZeroStr;
  let x be Element of L;
  cluster <%x%> -> constant;
  cluster <%x,0.L%> -> constant;
end;

theorem :: POLYDIFF:23
  for L being non empty ZeroStr
  for p being constant Polynomial of L holds
  p = 0_.L or p = <%p.0%>;

definition
  let L,x,n;
  func seq(n,x) -> sequence of L equals
:: POLYDIFF:def 3
  0_.L+*(n,x);
end;

registration
  let L,x,n;
  cluster seq(n,x) -> finite-Support;
end;

theorem :: POLYDIFF:24
  seq(n,x).n = x;

theorem :: POLYDIFF:25
  m <> n implies seq(n,x).m = 0.L;

theorem :: POLYDIFF:26
  n+1 is_at_least_length_of seq(n,x);

theorem :: POLYDIFF:27
  x <> 0.L implies len seq(n,x) = n+1;

theorem :: POLYDIFF:28
  seq(n,0.L) = 0_.L;

theorem :: POLYDIFF:29
  for L being right_zeroed non empty addLoopStr, x,y being Element of L holds
  seq(n,x) + seq(n,y) = seq(n,x+y);

theorem :: POLYDIFF:30
  for L being add-associative right_zeroed right_complementable
        non empty addLoopStr
  for x being Element of L holds
  -seq(n,x) = seq(n,-x);

theorem :: POLYDIFF:31
  for L being add-associative right_zeroed right_complementable
        non empty addLoopStr
  for x,y being Element of L holds
  seq(n,x) - seq(n,y) = seq(n,x-y);

definition
  let L be non empty ZeroStr;
  let p be sequence of L;
  let n;
  func p||n -> sequence of L equals
:: POLYDIFF:def 4
  p +* (n,0.L);
end;

registration
  let L be non empty ZeroStr;
  let p be Polynomial of L;
  let n;
  cluster p||n -> finite-Support;
end;

theorem :: POLYDIFF:32
  for L being non empty ZeroStr, p being sequence of L holds
  (p||n).n = 0.L;

theorem :: POLYDIFF:33
  for L being non empty ZeroStr, p being sequence of L holds
  m <> n implies (p||n).m = p.m;

theorem :: POLYDIFF:34
  for L being non empty ZeroStr holds (0_.L) || n = 0_.L;

registration
  let L be non empty ZeroStr;
  let n;
  reduce (0_.L) || n to 0_.L;
end;

theorem :: POLYDIFF:35
  for L being non empty ZeroStr, p being Polynomial of L holds
  n > len p-'1 implies p||n = p;

theorem :: POLYDIFF:36
  for L being non empty ZeroStr, p being Polynomial of L holds
  p <> 0_.L implies len(p||(len p-'1)) < len p;

theorem :: POLYDIFF:37
  for L being add-associative right_zeroed right_complementable
      non empty addLoopStr
  for p being Polynomial of L holds
  p||(len p-'1) + Leading-Monomial p = p;

registration
  let L be non empty ZeroStr;
  let p be constant Polynomial of L;
  cluster Leading-Monomial(p) -> constant;
end;

theorem :: POLYDIFF:38
  for L being add-associative right_zeroed right_complementable
              distributive unital non empty doubleLoopStr
  for x,y being Element of L holds
  eval(seq(n,x),y) = seq(n,x).n * power(y,n);

begin :: Differentiability of polynomials over reals

reserve p,q for Polynomial of F_Real;

theorem :: POLYDIFF:39
  for r being Element of F_Real holds power(r,n) = r|^n;

theorem :: POLYDIFF:40
  #Z n = FPower(1.F_Real,n);

theorem :: POLYDIFF:41
  for r being Element of F_Real holds
  FPower(r,n+1) = FPower(r,n)(#)id(REAL);

theorem :: POLYDIFF:42
  for r being Element of F_Real holds
  FPower(r,n) is differentiable Function of REAL,REAL;

theorem :: POLYDIFF:43
  for r being Element of F_Real holds power(r,n) = ( #Z n).r;

definition
  let p;
  func poly_diff(p) -> sequence of F_Real means
:: POLYDIFF:def 5
  for n being Nat holds it.n = p.(n+1) * (n+1);
end;

registration
  let p;
  cluster poly_diff(p) -> finite-Support;
end;

theorem :: POLYDIFF:44
  p <> 0_.F_Real implies len poly_diff(p) = len p - 1;

theorem :: POLYDIFF:45
  p <> 0_.F_Real implies len p = len poly_diff(p) + 1;

theorem :: POLYDIFF:46
  for p being constant Polynomial of F_Real holds poly_diff(p) = 0_.F_Real;

theorem :: POLYDIFF:47
  poly_diff(p+q) = poly_diff(p) + poly_diff(q);

theorem :: POLYDIFF:48
  poly_diff(-p) = -poly_diff(p);

theorem :: POLYDIFF:49
  poly_diff(p-q) = poly_diff(p) - poly_diff(q);

theorem :: POLYDIFF:50
  poly_diff(Leading-Monomial p) =
   0_.F_Real +* (len p-'2,(p.(len p-'1))*(len p-'1));

theorem :: POLYDIFF:51
  for r,s being Element of F_Real holds poly_diff(<%r,s%>) = <%s%>;

definition
  let p;
  func Eval(p) -> Function of REAL,REAL equals
:: POLYDIFF:def 6
  Polynomial-Function(F_Real,p);
end;

registration
  let p;
  cluster Eval(p) -> differentiable;
end;

theorem :: POLYDIFF:52
  Eval(0_.F_Real) = REAL --> 0;

theorem :: POLYDIFF:53
  for r being Element of F_Real holds Eval(<%r%>) = REAL --> r;

theorem :: POLYDIFF:54
  p is constant implies Eval(p)`| = REAL --> 0;

theorem :: POLYDIFF:55
  Eval(p+q) = Eval(p) + Eval(q);

theorem :: POLYDIFF:56
  Eval(-p) = -Eval(p);

theorem :: POLYDIFF:57
  Eval(p-q) = Eval(p) - Eval(q);

theorem :: POLYDIFF:58
  Eval(Leading-Monomial p) = FPower(p.(len p-'1),len p-'1);

theorem :: POLYDIFF:59
  Eval(Leading-Monomial p) = p.(len p-'1) (#) #Z(len p-'1);

theorem :: POLYDIFF:60
  for r being Element of F_Real holds Eval(seq(n,r)) = r (#) #Z n;

theorem :: POLYDIFF:61
  (Eval(p))`| = Eval(poly_diff(p));

registration
  let p;
  cluster (Eval p)`| -> differentiable;
end;