VSDIFF_1: Difference of Function on Vector Space over $\mathbbF$

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₁( Element of C) -> Element of the carrier of V = r * (f /. $1);
defpred S₁[ set ] means $1 in dom f;

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

proof end;

uniqueness

proof end;

end;

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

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;

cluster r (#) f -> total ;

coherence

proof end;

end;

definition

let GF be Field;
let V be VectSp of GF;
let v be Element of V;
let W be Subset of V;

func v ++ W -> Subset of V equals :: VSDIFF_1:def 2
{ (v + u) where u is Element of V : u in W } ;

coherence

proof end;

end;

:: deftheorem defines ++ VSDIFF_1:def 2 :

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;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Shift VSDIFF_1:def 3 :

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

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;

:: 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

proof end;

compatibility

proof end;

end;

:: deftheorem Def2 defines Shift VSDIFF_1:def 4 :

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;

func fD (f,h) -> PartFunc of V,W equals :: VSDIFF_1:def 5
(Shift (f,h)) - f;

coherence ;

end;

:: deftheorem defines fD VSDIFF_1:def 5 :

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;

cluster fD (f,h) -> quasi_total ;

coherence

proof end;

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;

func bD (f,h) -> PartFunc of V,W equals :: VSDIFF_1:def 6
f - (Shift (f,(- h)));

coherence ;

end;

:: deftheorem defines bD VSDIFF_1:def 6 :

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;

cluster bD (f,h) -> quasi_total ;

coherence

proof end;

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;

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 ;

end;

:: deftheorem defines cD VSDIFF_1:def 7 :

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;

cluster cD (f,h) -> quasi_total ;

coherence

proof end;

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;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines forward_difference VSDIFF_1:def 8 :

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;

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)

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

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)

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))

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)))

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

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)

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)

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)

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))

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)

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;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines backward_difference VSDIFF_1:def 9 :

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;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines backward_difference VSDIFF_1:def 10 :

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;

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

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

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)

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)

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)

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))

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)

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;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines central_difference VSDIFF_1:def 11 :

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;

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

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

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)

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)

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)

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))

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)

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))

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))

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))

proof end;