The abstract of the Mizar article:

Bessel's Inequality

by

Hiroshi Yamazaki,

Yasunari Shidama, and

Yatsuka Nakamura

Received January 30, 2003

MML identifier: BHSP_5

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, BHSP_1, PRE_TOPC, NORMSP_1, RLVECT_1, FUNCT_1, ARYTM_1,
      FINSET_1, RELAT_1, BHSP_5, BINOP_1, VECTSP_1, PROB_2, FUZZY_2, SQUARE_1,
      FUNCT_2, FINSEQ_1, SETWISEO, CARD_1, FINSOP_1, DECOMP_1;
 notation TARSKI, SUBSET_1, XBOOLE_0, NUMBERS, XREAL_0, STRUCT_0, REAL_1,
      NAT_1, FUNCT_2, FINSET_1, RELAT_1, PRE_TOPC, RLVECT_1, BHSP_1, SQUARE_1,
      BINOP_1, VECTSP_1, CARD_1, SETWISEO, FUNCT_1, FINSEQ_1, FINSOP_1;
 constructors REAL_1, NAT_1, BHSP_1, PREPOWER, DOMAIN_1, SQUARE_1, SETWISEO,
      BINOP_1, VECTSP_1, FINSOP_1, MEMBERED, PARTFUN1;
 clusters RELSET_1, FINSEQ_1, FUNCT_1, FUNCT_2, FINSET_1, STRUCT_0, MEMBERED,
      NUMBERS, ORDINAL2;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Sum of the result of operation with each element of a set

  reserve X for RealUnitarySpace;

  reserve x, y, y1, y2 for Point of X;
  reserve xd for set;
  reserve i, j, n for Nat;
  reserve DX for non empty set;
  reserve p1, p2 for FinSequence of DX;

theorem :: BHSP_5:1
  p1 is one-to-one & p2 is one-to-one & rng p1 = rng p2 implies
  dom p1 = dom p2 &
  ex P being Permutation of dom p1 st
    p2 = p1*P & dom P = dom p1 & rng P = dom p1;

definition
  let DX be non empty set;
  let f be BinOp of DX such that
 f is commutative associative & f has_a_unity;
  let Y be finite Subset of DX;
    func f ++ Y -> Element of DX means
:: BHSP_5:def 1
    ex p being FinSequence of DX st
     p is one-to-one & rng p = Y & it = f "**" p;
end;

definition let X;
           let Y be finite Subset of X;
  func setop_SUM(Y,X) equals
:: BHSP_5:def 2
     (the add of X) ++ Y if Y <> {}
   otherwise 0.X;
end;

definition let X, x;
           let p be FinSequence;
           let i;
  func PO(i,p,x) equals
:: BHSP_5:def 3
  (the scalar of X).[x,p.i];
end;

definition let DK, DX be non empty set;
           let F be Function of DX, DK;
           let p be FinSequence of DX;
  func Func_Seq(F,p) -> FinSequence of DK equals
:: BHSP_5:def 4
   F*p;
end;

definition
  let DK, DX be non empty set;
  let f be BinOp of DK such that
 f is commutative associative & f has_a_unity;
  let Y be finite Subset of DX;
  let F be Function of DX,DK such that
 Y c= dom F;
  func setopfunc(Y,DX,DK,F,f) -> Element of DK means
:: BHSP_5:def 5
 ex p being FinSequence of DX st p is one-to-one &
    rng p = Y & it = f "**" Func_Seq(F,p);
end;

definition let X, x;
           let Y be finite Subset of X;
 func setop_xPre_PROD(x,Y,X) -> Real means
:: BHSP_5:def 6
      ex p being FinSequence of the carrier of X st p is one-to-one &
    rng p = Y
    & ex q being FinSequence of REAL st dom(q) = dom(p) &
    (for i st i in dom q holds
      q.i = PO(i,p,x)) & it = addreal "**" q;
end;

definition let X, x;
           let Y be finite Subset of X;
  func setop_xPROD(x,Y,X) -> Real equals
:: BHSP_5:def 7
    setop_xPre_PROD(x,Y,X) if Y <> {}
  otherwise 0;
end;

begin :: Orthogonal Family & Orthonormal Family

definition let X;
  mode OrthogonalFamily of X -> Subset of X means
:: BHSP_5:def 8
  for x, y st x in it & y in it & x <> y holds x.|.y = 0;
end;

theorem :: BHSP_5:2
  {} is OrthogonalFamily of X;

definition let X;
  cluster finite OrthogonalFamily of X;
end;

definition let X;
  mode OrthonormalFamily of X -> Subset of X means
:: BHSP_5:def 9
  it is OrthogonalFamily of X & for x st x in it holds x.|.x = 1;
end;

theorem :: BHSP_5:3
  {} is OrthonormalFamily of X;

definition let X;
  cluster finite OrthonormalFamily of X;
end;

theorem :: BHSP_5:4
    x = 0.X iff (for y holds x.|.y = 0);

begin :: Bessel's inequality
:: parallelogram law
theorem :: BHSP_5:5
    ||.x+y.||^2 + ||.x-y.||^2 = 2*||.x.||^2 + 2*||.y.||^2;

:: The Pythagorean theorem
theorem :: BHSP_5:6
    x, y are_orthogonal implies ||.x+y.||^2 = ||.x.||^2 + ||.y.||^2;

theorem :: BHSP_5:7
  for p be FinSequence of the carrier of X
    st (len p >=1 &
      for i,j st (i in dom p & j in dom p & i <> j)
        holds (the scalar of X).[p.i,p.j]=0)
  for q be FinSequence of REAL
    st dom p = dom q &
      (for i st i in dom q holds q.i = (the scalar of X).[(p.i),(p.i)])
        holds ((the add of X) "**" p).|. ((the add of X) "**" p)
        = addreal "**" q;

theorem :: BHSP_5:8
  for p be FinSequence of the carrier of X st len p >= 1
  for q be FinSequence of REAL st dom p = dom q &
      (for i st i in dom q holds q.i = (the scalar of X).[x,p.i])
  holds x.|.((the add of X) "**" p) = addreal "**" q;

theorem :: BHSP_5:9
  for S be finite non empty Subset of X
  for F be Function of the carrier of X, the carrier of X
      st (S c= dom F & (for y1,y2 st y1 in S & y2 in S & y1 <> y2
        holds (the scalar of X).[F.y1,F.y2] = 0))
  for H be Function of the carrier of X, REAL
     st S c= dom H & (for y st y in S holds
       H.y= (the scalar of X).[F.y,F.y])
  for p be FinSequence of the carrier of X
     st p is one-to-one & rng p = S holds
  (the scalar of X).[(the add of X) "**" Func_Seq(F,p),
                     (the add of X) "**" Func_Seq(F,p)]
  = addreal "**" Func_Seq(H,p);

theorem :: BHSP_5:10
  for S be finite non empty Subset of X
  for F be Function of the carrier of X, the carrier of X st S c= dom F
  for H be Function of the carrier of X, REAL
       st S c= dom H & (for y st y in S holds
          H.y = (the scalar of X).[x,F.y])
  for p be FinSequence of the carrier of X
          st p is one-to-one & rng p = S
  holds (the scalar of X).[x,(the add of X) "**" Func_Seq(F,p) ]
          = addreal "**" Func_Seq(H,p);

theorem :: BHSP_5:11
  for X st the add of X is commutative associative &
    the add of X has_a_unity
  for x
  for S be finite OrthonormalFamily of X st S is non empty
  for H be Function of the carrier of X, REAL st
    S c= dom H & (for y st y in S holds H.y= (x.|.y)^2)
  for F be Function of the carrier of X, the carrier of X st
    S c= dom F & (for y st y in S holds F.y = (x.|.y)*y) holds
    x.|.setopfunc(S, the carrier of X, the carrier of X, F, the add of X)
      = setopfunc(S, the carrier of X, REAL, H, addreal);

theorem :: BHSP_5:12
  for X st the add of X is commutative associative & the add of X has_a_unity
  for x
  for S be finite OrthonormalFamily of X st S is non empty
  for F be Function of the carrier of X, the carrier of X
    st S c= dom F & (for y st y in S holds F.y = (x.|.y)*y)
  for H be Function of the carrier of X, REAL
    st S c= dom H & (for y st y in S holds H.y= (x.|.y)^2) holds
    setopfunc(S, the carrier of X, the carrier of X, F, the add of X)
      .|. setopfunc(S, the carrier of X, the carrier of X, F, the add of X)
    = setopfunc(S, the carrier of X, REAL, H, addreal);

theorem :: BHSP_5:13
    for X st the add of X is commutative associative &
    the add of X has_a_unity
  for x
  for S be finite OrthonormalFamily of X st S is non empty
  for H be Function of the carrier of X, REAL
    st S c= dom H & (for y st y in S holds H.y = (x.|.y)^2) holds
  setopfunc(S, the carrier of X, REAL, H, addreal) <= ||.x.||^2;

theorem :: BHSP_5:14
    for DK, DX be non empty set
  for f be BinOp of DK st f is commutative associative & f has_a_unity
  for Y1, Y2 be finite Subset of DX st Y1 misses Y2
  for F be Function of DX, DK st Y1 c= dom F & Y2 c= dom F
  for Z be finite Subset of DX st Z = Y1 \/ Y2
  holds
  setopfunc(Z,DX,DK,F,f)
    = f.(setopfunc(Y1,DX,DK,F,f), setopfunc(Y2,DX,DK,F,f));