:: by Kenichi Arai , Ken Wakabayashi and Hiroyuki Okazaki

::

:: Received September 26, 2014

:: Copyright (c) 2014-2017 Association of Mizar Users

definition

let C be non empty set ;

let GF be Field;

let V be VectSp of GF;

let f be PartFunc of C,V;

let r be Element of GF;

deffunc H_{1}( Element of C) -> Element of the carrier of V = r * (f /. $1);

defpred S_{1}[ set ] means $1 in dom f;

ex b_{1} being PartFunc of C,V st

( dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = r * (f /. c) ) )

for b_{1}, b_{2} being PartFunc of C,V st dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} /. c = r * (f /. c) ) & dom b_{2} = dom f & ( for c being Element of C st c in dom b_{2} holds

b_{2} /. c = r * (f /. c) ) holds

b_{1} = b_{2}

end;
let GF be Field;

let V be VectSp of GF;

let f be PartFunc of C,V;

let r be Element of GF;

deffunc H

defpred S

func r (#) f -> PartFunc of C,V means :Def4X: :: VSDIFF_1:def 1

( dom it = dom f & ( for c being Element of C st c in dom it holds

it /. c = r * (f /. c) ) );

existence ( dom it = dom f & ( for c being Element of C st c in dom it holds

it /. c = r * (f /. c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4X defines (#) VSDIFF_1:def 1 :

for C being non empty set

for GF being Field

for V being VectSp of GF

for f being PartFunc of C,V

for r being Element of GF

for b_{6} being PartFunc of C,V holds

( b_{6} = r (#) f iff ( dom b_{6} = dom f & ( for c being Element of C st c in dom b_{6} holds

b_{6} /. c = r * (f /. c) ) ) );

for C being non empty set

for GF being Field

for V being VectSp of GF

for f being PartFunc of C,V

for r being Element of GF

for b

( b

b

registration

let C be non empty set ;

let GF be Field;

let V be VectSp of GF;

let f be Function of C,V;

let r be Element of GF;

coherence

r (#) f is total

end;
let GF be Field;

let V be VectSp of GF;

let f be Function of C,V;

let r be Element of GF;

coherence

r (#) f is total

proof end;

definition

let GF be Field;

let V be VectSp of GF;

let v be Element of V;

let W be Subset of V;

coherence

{ (v + u) where u is Element of V : u in W } is Subset of V

end;
let V be VectSp of GF;

let v be Element of V;

let W be Subset of V;

coherence

{ (v + u) where u is Element of V : u in W } is Subset of V

proof end;

:: deftheorem defines ++ VSDIFF_1:def 2 :

for GF being Field

for V being VectSp of GF

for v being Element of V

for W being Subset of V holds v ++ W = { (v + u) where u is Element of V : u in W } ;

for GF being Field

for V being VectSp of GF

for v being Element of V

for W being Subset of V holds v ++ W = { (v + u) where u is Element of V : u in W } ;

definition

let F, G be Field;

let V be VectSp of F;

let W be VectSp of G;

let f be PartFunc of V,W;

let h be Element of V;

ex b_{1} being PartFunc of V,W st

( dom b_{1} = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds

b_{1} . x = f . (x + h) ) )

for b_{1}, b_{2} being PartFunc of V,W st dom b_{1} = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds

b_{1} . x = f . (x + h) ) & dom b_{2} = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds

b_{2} . x = f . (x + h) ) holds

b_{1} = b_{2}

end;
let V be VectSp of F;

let W be VectSp of G;

let f be PartFunc of V,W;

let h be Element of V;

func Shift (f,h) -> PartFunc of V,W means :Def1: :: VSDIFF_1:def 3

( dom it = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds

it . x = f . (x + h) ) );

existence ( dom it = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds

it . x = f . (x + h) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines Shift VSDIFF_1:def 3 :

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being PartFunc of V,W

for h being Element of V

for b_{7} being PartFunc of V,W holds

( b_{7} = Shift (f,h) iff ( dom b_{7} = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds

b_{7} . x = f . (x + h) ) ) );

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being PartFunc of V,W

for h being Element of V

for b

( b

b

theorem MEASURE624: :: VSDIFF_1:1

for GF being Field

for V being VectSp of GF

for x being Element of V

for A being Subset of V st A = the carrier of V holds

x ++ A = A

for V being VectSp of GF

for x being Element of V

for A being Subset of V st A = the carrier of V holds

x ++ A = A

proof end;

definition

let F, G be Field;

let V be VectSp of F;

let W be VectSp of G;

let f be Function of V,W;

let h be Element of V;

Shift (f,h) is Function of V,W

for b_{1} being Function of V,W holds

( b_{1} = Shift (f,h) iff for x being Element of V holds b_{1} . x = f . (x + h) )

end;
let V be VectSp of F;

let W be VectSp of G;

let f be Function of V,W;

let h be Element of V;

:: original: Shift

redefine func Shift (f,h) -> Function of V,W means :Def2: :: VSDIFF_1:def 4

for x being Element of V holds it . x = f . (x + h);

coherence redefine func Shift (f,h) -> Function of V,W means :Def2: :: VSDIFF_1:def 4

for x being Element of V holds it . x = f . (x + h);

Shift (f,h) is Function of V,W

proof end;

compatibility for b

( b

proof end;

:: deftheorem Def2 defines Shift VSDIFF_1:def 4 :

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for b_{7} being Function of V,W holds

( b_{7} = Shift (f,h) iff for x being Element of V holds b_{7} . x = f . (x + h) );

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for b

( b

definition

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be PartFunc of V,W;

coherence

(Shift (f,h)) - f is PartFunc of V,W ;

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be PartFunc of V,W;

coherence

(Shift (f,h)) - f is PartFunc of V,W ;

:: deftheorem defines fD VSDIFF_1:def 5 :

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being PartFunc of V,W holds fD (f,h) = (Shift (f,h)) - f;

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being PartFunc of V,W holds fD (f,h) = (Shift (f,h)) - f;

registration

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

coherence

fD (f,h) is quasi_total

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

coherence

fD (f,h) is quasi_total

proof end;

definition

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be PartFunc of V,W;

coherence

f - (Shift (f,(- h))) is PartFunc of V,W ;

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be PartFunc of V,W;

coherence

f - (Shift (f,(- h))) is PartFunc of V,W ;

:: deftheorem defines bD VSDIFF_1:def 6 :

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being PartFunc of V,W holds bD (f,h) = f - (Shift (f,(- h)));

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being PartFunc of V,W holds bD (f,h) = f - (Shift (f,(- h)));

registration

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

coherence

bD (f,h) is quasi_total

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

coherence

bD (f,h) is quasi_total

proof end;

definition

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be PartFunc of V,W;

(Shift (f,(((2 * (1. F)) ") * h))) - (Shift (f,(- (((2 * (1. F)) ") * h)))) is PartFunc of V,W ;

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be PartFunc of V,W;

func cD (f,h) -> PartFunc of V,W equals :: VSDIFF_1:def 7

(Shift (f,(((2 * (1. F)) ") * h))) - (Shift (f,(- (((2 * (1. F)) ") * h))));

coherence (Shift (f,(((2 * (1. F)) ") * h))) - (Shift (f,(- (((2 * (1. F)) ") * h))));

(Shift (f,(((2 * (1. F)) ") * h))) - (Shift (f,(- (((2 * (1. F)) ") * h)))) is PartFunc of V,W ;

:: deftheorem defines cD VSDIFF_1:def 7 :

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being PartFunc of V,W holds cD (f,h) = (Shift (f,(((2 * (1. F)) ") * h))) - (Shift (f,(- (((2 * (1. F)) ") * h))));

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being PartFunc of V,W holds cD (f,h) = (Shift (f,(((2 * (1. F)) ") * h))) - (Shift (f,(- (((2 * (1. F)) ") * h))));

registration

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

coherence

cD (f,h) is quasi_total

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

coherence

cD (f,h) is quasi_total

proof end;

definition

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

ex b_{1} being Functional_Sequence of the carrier of V, the carrier of W st

( b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = fD ((b_{1} . n),h) ) )

for b_{1}, b_{2} being Functional_Sequence of the carrier of V, the carrier of W st b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = fD ((b_{1} . n),h) ) & b_{2} . 0 = f & ( for n being Nat holds b_{2} . (n + 1) = fD ((b_{2} . n),h) ) holds

b_{1} = b_{2}

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

func forward_difference (f,h) -> Functional_Sequence of the carrier of V, the carrier of W means :Def6: :: VSDIFF_1:def 8

( it . 0 = f & ( for n being Nat holds it . (n + 1) = fD ((it . n),h) ) );

existence ( it . 0 = f & ( for n being Nat holds it . (n + 1) = fD ((it . n),h) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines forward_difference VSDIFF_1:def 8 :

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being Function of V,W

for b_{7} being Functional_Sequence of the carrier of V, the carrier of W holds

( b_{7} = forward_difference (f,h) iff ( b_{7} . 0 = f & ( for n being Nat holds b_{7} . (n + 1) = fD ((b_{7} . n),h) ) ) );

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being Function of V,W

for b

( b

notation

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

synonym fdif (f,h) for forward_difference (f,h);

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

synonym fdif (f,h) for forward_difference (f,h);

theorem Th01: :: VSDIFF_1:2

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for x, h being Element of V

for f being PartFunc of V,W st x in dom f & x + h in dom f holds

(fD (f,h)) /. x = (f /. (x + h)) - (f /. x)

for V being VectSp of F

for W being VectSp of G

for x, h being Element of V

for f being PartFunc of V,W st x in dom f & x + h in dom f holds

(fD (f,h)) /. x = (f /. (x + h)) - (f /. x)

proof end;

theorem Th2: :: VSDIFF_1:3

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat holds (fdif (f,h)) . n is Function of V,W

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat holds (fdif (f,h)) . n is Function of V,W

proof end;

theorem Th3: :: VSDIFF_1:4

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds (fD (f,h)) /. x = (f /. (x + h)) - (f /. x)

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds (fD (f,h)) /. x = (f /. (x + h)) - (f /. x)

proof end;

theorem Th4: :: VSDIFF_1:5

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds (bD (f,h)) /. x = (f /. x) - (f /. (x - h))

proof end;

theorem Th5: :: VSDIFF_1:6

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds (cD (f,h)) /. x = (f /. (x + (((2 * (1. F)) ") * h))) - (f /. (x - (((2 * (1. F)) ") * h)))

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds (cD (f,h)) /. x = (f /. (x + (((2 * (1. F)) ") * h))) - (f /. (x - (((2 * (1. F)) ") * h)))

proof end;

theorem :: VSDIFF_1:7

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat st f is constant holds

for x being Element of V holds ((fdif (f,h)) . (n + 1)) /. x = 0. W

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat st f is constant holds

for x being Element of V holds ((fdif (f,h)) . (n + 1)) /. x = 0. W

proof end;

theorem Th7: :: VSDIFF_1:8

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for r being Element of G

for n being Nat holds ((fdif ((r (#) f),h)) . (n + 1)) /. x = r * (((fdif (f,h)) . (n + 1)) /. x)

proof end;

theorem Th8: :: VSDIFF_1:9

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((fdif ((f1 + f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) + (((fdif (f2,h)) . (n + 1)) /. x)

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((fdif ((f1 + f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) + (((fdif (f2,h)) . (n + 1)) /. x)

proof end;

theorem :: VSDIFF_1:10

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((fdif ((f1 - f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) - (((fdif (f2,h)) . (n + 1)) /. x)

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((fdif ((f1 - f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) - (((fdif (f2,h)) . (n + 1)) /. x)

proof end;

theorem :: VSDIFF_1:11

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for r1, r2 being Element of G

for n being Nat holds ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (f2,h)) . (n + 1)) /. x))

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for r1, r2 being Element of G

for n being Nat holds ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (f2,h)) . (n + 1)) /. x))

proof end;

theorem :: VSDIFF_1:12

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds ((fdif (f,h)) . 1) /. x = ((Shift (f,h)) /. x) - (f /. x)

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds ((fdif (f,h)) . 1) /. x = ((Shift (f,h)) /. x) - (f /. x)

proof end;

definition

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

ex b_{1} being Functional_Sequence of the carrier of V, the carrier of W st

( b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = bD ((b_{1} . n),h) ) )

for b_{1}, b_{2} being Functional_Sequence of the carrier of V, the carrier of W st b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = bD ((b_{1} . n),h) ) & b_{2} . 0 = f & ( for n being Nat holds b_{2} . (n + 1) = bD ((b_{2} . n),h) ) holds

b_{1} = b_{2}

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

func backward_difference (f,h) -> Functional_Sequence of the carrier of V, the carrier of W means :: VSDIFF_1:def 9

( it . 0 = f & ( for n being Nat holds it . (n + 1) = bD ((it . n),h) ) );

existence ( it . 0 = f & ( for n being Nat holds it . (n + 1) = bD ((it . n),h) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines backward_difference VSDIFF_1:def 9 :

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being Function of V,W

for b_{7} being Functional_Sequence of the carrier of V, the carrier of W holds

( b_{7} = backward_difference (f,h) iff ( b_{7} . 0 = f & ( for n being Nat holds b_{7} . (n + 1) = bD ((b_{7} . n),h) ) ) );

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being Function of V,W

for b

( b

definition

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

ex b_{1} being Functional_Sequence of the carrier of V, the carrier of W st

( b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = bD ((b_{1} . n),h) ) )

for b_{1}, b_{2} being Functional_Sequence of the carrier of V, the carrier of W st b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = bD ((b_{1} . n),h) ) & b_{2} . 0 = f & ( for n being Nat holds b_{2} . (n + 1) = bD ((b_{2} . n),h) ) holds

b_{1} = b_{2}

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

func backward_difference (f,h) -> Functional_Sequence of the carrier of V, the carrier of W means :Def7: :: VSDIFF_1:def 10

( it . 0 = f & ( for n being Nat holds it . (n + 1) = bD ((it . n),h) ) );

existence ( it . 0 = f & ( for n being Nat holds it . (n + 1) = bD ((it . n),h) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines backward_difference VSDIFF_1:def 10 :

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being Function of V,W

for b_{7} being Functional_Sequence of the carrier of V, the carrier of W holds

( b_{7} = backward_difference (f,h) iff ( b_{7} . 0 = f & ( for n being Nat holds b_{7} . (n + 1) = bD ((b_{7} . n),h) ) ) );

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being Function of V,W

for b

( b

notation

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

synonym bdif (f,h) for backward_difference (f,h);

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be Function of V,W;

synonym bdif (f,h) for backward_difference (f,h);

theorem Th12: :: VSDIFF_1:13

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat holds (bdif (f,h)) . n is Function of V,W

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat holds (bdif (f,h)) . n is Function of V,W

proof end;

theorem :: VSDIFF_1:14

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat st f is constant holds

for x being Element of V holds ((bdif (f,h)) . (n + 1)) /. x = 0. W

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat st f is constant holds

for x being Element of V holds ((bdif (f,h)) . (n + 1)) /. x = 0. W

proof end;

theorem Th14: :: VSDIFF_1:15

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for r being Element of G

for n being Nat holds ((bdif ((r (#) f),h)) . (n + 1)) /. x = r * (((bdif (f,h)) . (n + 1)) /. x)

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for r being Element of G

for n being Nat holds ((bdif ((r (#) f),h)) . (n + 1)) /. x = r * (((bdif (f,h)) . (n + 1)) /. x)

proof end;

theorem Th15: :: VSDIFF_1:16

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((bdif ((f1 + f2),h)) . (n + 1)) /. x = (((bdif (f1,h)) . (n + 1)) /. x) + (((bdif (f2,h)) . (n + 1)) /. x)

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((bdif ((f1 + f2),h)) . (n + 1)) /. x = (((bdif (f1,h)) . (n + 1)) /. x) + (((bdif (f2,h)) . (n + 1)) /. x)

proof end;

theorem :: VSDIFF_1:17

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((bdif ((f1 - f2),h)) . (n + 1)) /. x = (((bdif (f1,h)) . (n + 1)) /. x) - (((bdif (f2,h)) . (n + 1)) /. x)

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((bdif ((f1 - f2),h)) . (n + 1)) /. x = (((bdif (f1,h)) . (n + 1)) /. x) - (((bdif (f2,h)) . (n + 1)) /. x)

proof end;

theorem :: VSDIFF_1:18

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for r1, r2 being Element of G

for n being Nat holds ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x))

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for r1, r2 being Element of G

for n being Nat holds ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x))

proof end;

theorem :: VSDIFF_1:19

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds ((bdif (f,h)) . 1) /. x = (f /. x) - ((Shift (f,(- h))) /. x)

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds ((bdif (f,h)) . 1) /. x = (f /. x) - ((Shift (f,(- h))) /. x)

proof end;

definition

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be PartFunc of V,W;

ex b_{1} being Functional_Sequence of the carrier of V, the carrier of W st

( b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = cD ((b_{1} . n),h) ) )

for b_{1}, b_{2} being Functional_Sequence of the carrier of V, the carrier of W st b_{1} . 0 = f & ( for n being Nat holds b_{1} . (n + 1) = cD ((b_{1} . n),h) ) & b_{2} . 0 = f & ( for n being Nat holds b_{2} . (n + 1) = cD ((b_{2} . n),h) ) holds

b_{1} = b_{2}

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be PartFunc of V,W;

func central_difference (f,h) -> Functional_Sequence of the carrier of V, the carrier of W means :Def8: :: VSDIFF_1:def 11

( it . 0 = f & ( for n being Nat holds it . (n + 1) = cD ((it . n),h) ) );

existence ( it . 0 = f & ( for n being Nat holds it . (n + 1) = cD ((it . n),h) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines central_difference VSDIFF_1:def 11 :

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being PartFunc of V,W

for b_{7} being Functional_Sequence of the carrier of V, the carrier of W holds

( b_{7} = central_difference (f,h) iff ( b_{7} . 0 = f & ( for n being Nat holds b_{7} . (n + 1) = cD ((b_{7} . n),h) ) ) );

for F, G being Field

for V being VectSp of F

for h being Element of V

for W being VectSp of G

for f being PartFunc of V,W

for b

( b

notation

let F, G be Field;

let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be PartFunc of V,W;

synonym cdif (f,h) for central_difference (f,h);

end;
let V be VectSp of F;

let h be Element of V;

let W be VectSp of G;

let f be PartFunc of V,W;

synonym cdif (f,h) for central_difference (f,h);

theorem Th19: :: VSDIFF_1:20

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat holds (cdif (f,h)) . n is Function of V,W

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat holds (cdif (f,h)) . n is Function of V,W

proof end;

theorem :: VSDIFF_1:21

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat st f is constant holds

for x being Element of V holds ((cdif (f,h)) . (n + 1)) /. x = 0. W

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for h being Element of V

for n being Nat st f is constant holds

for x being Element of V holds ((cdif (f,h)) . (n + 1)) /. x = 0. W

proof end;

theorem Th21: :: VSDIFF_1:22

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for r being Element of G

for n being Nat holds ((cdif ((r (#) f),h)) . (n + 1)) /. x = r * (((cdif (f,h)) . (n + 1)) /. x)

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for r being Element of G

for n being Nat holds ((cdif ((r (#) f),h)) . (n + 1)) /. x = r * (((cdif (f,h)) . (n + 1)) /. x)

proof end;

theorem Th22: :: VSDIFF_1:23

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((cdif ((f1 + f2),h)) . (n + 1)) /. x = (((cdif (f1,h)) . (n + 1)) /. x) + (((cdif (f2,h)) . (n + 1)) /. x)

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((cdif ((f1 + f2),h)) . (n + 1)) /. x = (((cdif (f1,h)) . (n + 1)) /. x) + (((cdif (f2,h)) . (n + 1)) /. x)

proof end;

theorem :: VSDIFF_1:24

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((cdif ((f1 - f2),h)) . (n + 1)) /. x = (((cdif (f1,h)) . (n + 1)) /. x) - (((cdif (f2,h)) . (n + 1)) /. x)

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for n being Nat holds ((cdif ((f1 - f2),h)) . (n + 1)) /. x = (((cdif (f1,h)) . (n + 1)) /. x) - (((cdif (f2,h)) . (n + 1)) /. x)

proof end;

theorem :: VSDIFF_1:25

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for r1, r2 being Element of G

for n being Nat holds ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (f2,h)) . (n + 1)) /. x))

for V being VectSp of F

for W being VectSp of G

for f1, f2 being Function of V,W

for x, h being Element of V

for r1, r2 being Element of G

for n being Nat holds ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (f2,h)) . (n + 1)) /. x))

proof end;

theorem :: VSDIFF_1:26

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds ((cdif (f,h)) . 1) /. x = ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. x)

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V holds ((cdif (f,h)) . 1) /. x = ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. x)

proof end;

theorem :: VSDIFF_1:27

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for n being Nat holds ((fdif (f,h)) . n) /. x = ((bdif (f,h)) . n) /. (x + (n * h))

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for n being Nat holds ((fdif (f,h)) . n) /. x = ((bdif (f,h)) . n) /. (x + (n * h))

proof end;

theorem LAST0: :: VSDIFF_1:28

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for n being Nat st 1. F <> - (1. F) holds

((fdif (f,h)) . (2 * n)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * h))

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for n being Nat st 1. F <> - (1. F) holds

((fdif (f,h)) . (2 * n)) /. x = ((cdif (f,h)) . (2 * n)) /. (x + (n * h))

proof end;

theorem :: VSDIFF_1:29

for F, G being Field

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for n being Nat st 1. F <> - (1. F) holds

((fdif (f,h)) . ((2 * n) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h))

for V being VectSp of F

for W being VectSp of G

for f being Function of V,W

for x, h being Element of V

for n being Nat st 1. F <> - (1. F) holds

((fdif (f,h)) . ((2 * n) + 1)) /. x = ((cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * (1. F)) ") * h))

proof end;