:: Difference of Function on Vector Space over $\mathbbF$
:: by Kenichi Arai , Ken Wakabayashi and Hiroyuki Okazaki
::
:: Copyright (c) 2014-2018 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 H1( Element of C) -> Element of the carrier of V = r * (f /. $1); defpred S1[ 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
ex b1 being PartFunc of C,V st
( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 /. c = r * (f /. c) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,V st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 /. c = r * (f /. c) ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds
b2 /. c = r * (f /. c) ) holds
b1 = b2
proof end;
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 b6 being PartFunc of C,V holds
( b6 = r (#) f iff ( dom b6 = dom f & ( for c being Element of C st c in dom b6 holds
b6 /. c = r * (f /. c) ) ) );

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
r (#) f is total
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
{ (v + u) where u is Element of V : u in W } is Subset of V
proof end;
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 } ;

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
ex b1 being PartFunc of V,W st
( dom b1 = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds
b1 . x = f . (x + h) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of V,W st dom b1 = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds
b1 . x = f . (x + h) ) & dom b2 = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds
b2 . x = f . (x + h) ) holds
b1 = b2
proof end;
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 b7 being PartFunc of V,W holds
( b7 = Shift (f,h) iff ( dom b7 = (- h) ++ (dom f) & ( for x being Element of V st x in (- h) ++ (dom f) holds
b7 . x = f . (x + h) ) ) );

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
Shift (f,h) is Function of V,W
proof end;
compatibility
for b1 being Function of V,W holds
( b1 = Shift (f,h) iff for x being Element of V holds b1 . x = f . (x + h) )
proof end;
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 b7 being Function of V,W holds
( b7 = Shift (f,h) iff for x being Element of V holds b7 . x = f . (x + h) );

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
(Shift (f,h)) - f is PartFunc of V,W
;
end;

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

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
fD (f,h) is quasi_total
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
f - (Shift (f,(- h))) is PartFunc of V,W
;
end;

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

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
bD (f,h) is quasi_total
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
(Shift (f,(((2 * (1. F)) ") * h))) - (Shift (f,(- (((2 * (1. F)) ") * h)))) is PartFunc of V,W
;
end;

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

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
cD (f,h) is quasi_total
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
ex b1 being Functional_Sequence of the carrier of V, the carrier of W st
( b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = fD ((b1 . n),h) ) )
proof end;
uniqueness
for b1, b2 being Functional_Sequence of the carrier of V, the carrier of W st b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = fD ((b1 . n),h) ) & b2 . 0 = f & ( for n being Nat holds b2 . (n + 1) = fD ((b2 . n),h) ) holds
b1 = b2
proof end;
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 b7 being Functional_Sequence of the carrier of V, the carrier of W holds
( b7 = forward_difference (f,h) iff ( b7 . 0 = f & ( for n being Nat holds b7 . (n + 1) = fD ((b7 . n),h) ) ) );

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
ex b1 being Functional_Sequence of the carrier of V, the carrier of W st
( b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = bD ((b1 . n),h) ) )
proof end;
uniqueness
for b1, b2 being Functional_Sequence of the carrier of V, the carrier of W st b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = bD ((b1 . n),h) ) & b2 . 0 = f & ( for n being Nat holds b2 . (n + 1) = bD ((b2 . n),h) ) holds
b1 = b2
proof end;
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 b7 being Functional_Sequence of the carrier of V, the carrier of W holds
( b7 = backward_difference (f,h) iff ( b7 . 0 = f & ( for n being Nat holds b7 . (n + 1) = bD ((b7 . n),h) ) ) );

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
ex b1 being Functional_Sequence of the carrier of V, the carrier of W st
( b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = bD ((b1 . n),h) ) )
proof end;
uniqueness
for b1, b2 being Functional_Sequence of the carrier of V, the carrier of W st b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = bD ((b1 . n),h) ) & b2 . 0 = f & ( for n being Nat holds b2 . (n + 1) = bD ((b2 . n),h) ) holds
b1 = b2
proof end;
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 b7 being Functional_Sequence of the carrier of V, the carrier of W holds
( b7 = backward_difference (f,h) iff ( b7 . 0 = f & ( for n being Nat holds b7 . (n + 1) = bD ((b7 . n),h) ) ) );

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
ex b1 being Functional_Sequence of the carrier of V, the carrier of W st
( b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = cD ((b1 . n),h) ) )
proof end;
uniqueness
for b1, b2 being Functional_Sequence of the carrier of V, the carrier of W st b1 . 0 = f & ( for n being Nat holds b1 . (n + 1) = cD ((b1 . n),h) ) & b2 . 0 = f & ( for n being Nat holds b2 . (n + 1) = cD ((b2 . n),h) ) holds
b1 = b2
proof end;
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 b7 being Functional_Sequence of the carrier of V, the carrier of W holds
( b7 = central_difference (f,h) iff ( b7 . 0 = f & ( for n being Nat holds b7 . (n + 1) = cD ((b7 . n),h) ) ) );

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;