:: Real Normed Space
::  by Jan Popio{\l}ek
::
:: Received September 20, 1990
:: Copyright (c) 1990-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 NUMBERS, RLVECT_1, STRUCT_0, SUBSET_1, ALGSTR_0, BINOP_1,
      FUNCT_1, ZFMISC_1, XBOOLE_0, REAL_1, PRE_TOPC, SUPINF_2, RLSUB_1,
      FUNCOP_1, CARD_1, RELAT_1, COMPLEX1, ARYTM_3, XXREAL_0, ARYTM_1, NAT_1,
      TARSKI, SEQ_2, ORDINAL2, NORMSP_1, NORMSP_0, RELAT_2, METRIC_1, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCOP_1, FUNCT_2, BINOP_1,
      RELAT_1, COMSEQ_2, SEQ_2, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC,
      RLVECT_1, RLSUB_1, XXREAL_0, NORMSP_0;
 constructors BINOP_1, DOMAIN_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1,
      SEQ_2, RLSUB_1, VALUED_1, RELSET_1, NORMSP_0, COMSEQ_2;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
      STRUCT_0, RLVECT_1, ALGSTR_0, NORMSP_0, XCMPLX_0, VALUED_0, NAT_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

definition
  struct(RLSStruct, N-ZeroStr) NORMSTR (# carrier -> set,
   ZeroF -> Element of the carrier,
   addF -> BinOp of the carrier, Mult -> Function of [:REAL, the carrier:], the
    carrier, normF -> Function of the carrier, REAL #);
end;

registration
  cluster non empty strict for NORMSTR;
end;

reserve a, b for Real;

definition

  let IT be non empty NORMSTR;
  attr IT is RealNormSpace-like means
:: NORMSP_1:def 1

  for x, y being Point of IT, a holds ||.a * x.|| = |.a.| * ||.x.|| & ||.x + y
  .|| <= ||.x.|| + ||.y.||;
end;

registration
  cluster reflexive discerning RealNormSpace-like vector-distributive
  scalar-distributive scalar-associative scalar-unital Abelian add-associative
    right_zeroed right_complementable strict for non empty NORMSTR;
end;

definition
  mode RealNormSpace is reflexive discerning RealNormSpace-like
  vector-distributive scalar-distributive scalar-associative scalar-unital
  Abelian add-associative right_zeroed right_complementable
   non empty NORMSTR;
end;

reserve RNS for RealNormSpace;
reserve x, y, z, g, g1, g2 for Point of RNS;

theorem :: NORMSP_1:1
  ||.0.RNS.|| = 0;

theorem :: NORMSP_1:2
  ||.-x.|| = ||.x.||;

theorem :: NORMSP_1:3
  ||.x - y.|| <= ||.x.|| + ||.y.||;

theorem :: NORMSP_1:4
  0 <= ||.x.||;

registration
  let RNS,x;
  cluster ||.x.|| -> non negative;
end;

theorem :: NORMSP_1:5
  ||.a * x + b * y.|| <= |.a.| * ||.x.|| + |.b.| * ||.y.||;

theorem :: NORMSP_1:6
  ||.x - y.|| = 0 iff x = y;

theorem :: NORMSP_1:7
  ||.x - y.|| = ||.y - x.||;

theorem :: NORMSP_1:8
  ||.x.|| - ||.y.|| <= ||.x - y.||;

theorem :: NORMSP_1:9
  |.||.x.|| - ||.y.||.| <= ||.x - y.||;

theorem :: NORMSP_1:10
  ||.x - z.|| <= ||.x - y.|| + ||.y - z.||;

theorem :: NORMSP_1:11
  x <> y implies ||.x - y.|| <> 0;

reserve S, S1, S2 for sequence of RNS;
reserve k, n, m, m1, m2 for Nat;
reserve r for Real;
reserve f for Function;
reserve d, s, t for set;

theorem :: NORMSP_1:12
  for RNS being non empty 1-sorted, x being Element of RNS holds f is
  sequence of RNS iff ( dom f = NAT & for d st d in NAT holds f.d is Element of
  RNS );

theorem :: NORMSP_1:13
  for RNS being non empty 1-sorted, x being Element of RNS ex S being
  sequence of RNS st rng S = {x};

theorem :: NORMSP_1:14
  for RNS being non empty 1-sorted, S being sequence of RNS st (ex x
  being Element of RNS st for n being Nat holds S.n = x) ex x being Element of
  RNS st rng S={x};

theorem :: NORMSP_1:15
  for RNS being non empty 1-sorted, S being sequence of RNS st ex x
  being Element of RNS st rng S = {x} holds for n holds S.n = S.(n+1);

theorem :: NORMSP_1:16
  for RNS being non empty 1-sorted, S being sequence of RNS st for n
  holds S.n = S.(n+1) holds for n, k holds S.n = S.(n+k);

theorem :: NORMSP_1:17
  for RNS being non empty 1-sorted, S being sequence of RNS st for n, k
  holds S.n = S.(n+k) holds for n, m holds S.n = S.m;

theorem :: NORMSP_1:18
  for RNS being non empty 1-sorted, S being sequence of RNS st for n, m
  holds S.n = S.m ex x being Element of RNS st for n being Nat holds S.n = x;

definition
  let RNS be non empty addLoopStr;
  let S1, S2 be sequence of RNS;
  func S1 + S2 -> sequence of RNS means
:: NORMSP_1:def 2

  for n holds it.n = S1.n + S2.n;
end;

definition
  let RNS be non empty addLoopStr;
  let S1, S2 be sequence of RNS;
  func S1 - S2 -> sequence of RNS means
:: NORMSP_1:def 3

  for n holds it.n = S1.n - S2.n;
end;

definition
  let RNS be non empty addLoopStr;
  let S be sequence of RNS;
  let x be Element of RNS;
  func S - x -> sequence of RNS means
:: NORMSP_1:def 4

  for n holds it.n = S.n - x;
end;

definition
  let RNS be non empty RLSStruct;
  let S be sequence of RNS;
  let a be Real;
  func a * S -> sequence of RNS means
:: NORMSP_1:def 5

  for n holds it.n = a * S.n;
end;

definition
  let RNS, S;
  attr S is convergent means
:: NORMSP_1:def 6
  ex g st for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r;
end;

theorem :: NORMSP_1:19
  S1 is convergent & S2 is convergent implies S1 + S2 is convergent;

theorem :: NORMSP_1:20
  S1 is convergent & S2 is convergent implies S1 - S2 is convergent;

theorem :: NORMSP_1:21
  S is convergent implies S - x is convergent;

theorem :: NORMSP_1:22
  S is convergent implies a * S is convergent;

theorem :: NORMSP_1:23
  S is convergent implies ||.S.|| is convergent;

definition

  let RNS, S;
  assume
 S is convergent;
  func lim S -> Point of RNS means
:: NORMSP_1:def 7

  for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - it.|| < r;
end;

theorem :: NORMSP_1:24
  S is convergent & lim S = g implies ||.S - g.|| is convergent & lim
  ||.S - g.|| = 0;

theorem :: NORMSP_1:25
  S1 is convergent & S2 is convergent implies lim (S1 + S2) = (lim S1) +
  (lim S2);

theorem :: NORMSP_1:26
  S1 is convergent & S2 is convergent implies lim (S1 - S2) = (lim S1) -
  (lim S2);

theorem :: NORMSP_1:27
  S is convergent implies lim (S - x) = (lim S) - x;

theorem :: NORMSP_1:28
  S is convergent implies lim (a * S) = a * (lim S);