:: A Simple Example for Linear Partial Differential Equations and Its Solution Using the Method of Separation of Variables
:: by Sora Otsuki , Pauline N. Kawamoto and Hiroshi Yamazaki
::
:: Received February 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

LMSIN1: for n being Nat holds sin . (n * PI) = 0

proof end;

theorem DOMP1: :: PDIFFEQ1:1

for m being non zero Element of NAT
for X being Subset of (REAL m)
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_on X,I holds
dom (f `partial| (X,I)) = X

proof end;

registration

cluster [#] REAL -> open ;

coherence
[#] REAL is open

proof end;

cluster [#] (REAL 2) -> open ;

coherence
[#] (REAL 2) is open

proof end;

end;

LMOP3: [#] (REAL 2) = { <*x,t*> where x, t is Real : ( x in [#] REAL & t in [#] REAL ) }

proof end;

LM001: for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for x0 being Real st Z is open & x0 in Z & f is_differentiable_in x0 holds
( f | Z is_differentiable_in x0 & diff (f,x0) = diff ((f | Z),x0) )

proof end;

theorem LM002: :: PDIFFEQ1:2

for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for x0 being Real st Z is open & x0 in Z holds
( ( f is_differentiable_in x0 implies f | Z is_differentiable_in x0 ) & ( f | Z is_differentiable_in x0 implies f is_differentiable_in x0 ) & ( f is_differentiable_in x0 implies diff (f,x0) = diff ((f | Z),x0) ) )

proof end;

theorem LM003: :: PDIFFEQ1:3

for f being PartFunc of REAL,REAL
for X being Subset of REAL st X is open & X c= dom f holds
( f is_differentiable_on X iff f | X is_differentiable_on X )

proof end;

theorem LM00: :: PDIFFEQ1:4

for f being PartFunc of REAL,REAL
for X being Subset of REAL st X is open & X c= dom f & f is_differentiable_on X holds
(f | X) `| X = f `| X

proof end;

theorem DIFF1: :: PDIFFEQ1:5

for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & Z is open & f is_differentiable_on 1,Z holds
( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z )

proof end;

theorem DIFF2: :: PDIFFEQ1:6

for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & Z is open & f is_differentiable_on 2,Z holds
( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z & f `| Z is_differentiable_on Z & (diff (f,Z)) . 2 = (f `| Z) `| Z )

proof end;

LM02: for x, t being Real holds <*x,t*> in REAL 2

proof end;

LM03: for x, t being Real
for z being Element of REAL 2 st z = <*x,t*> holds
( (proj (1,2)) . z = x & (proj (2,2)) . z = t )

proof end;

theorem LM10: :: PDIFFEQ1:7

for X, T being Subset of REAL
for f, g being PartFunc of REAL,REAL st X c= dom f & T c= dom g holds
ex u being PartFunc of (REAL 2),REAL st
( dom u = { <*x,t*> where x, t is Real : ( x in X & t in T ) } & ( for x, t being Real st x in X & t in T holds
u /. <*x,t*> = (f /. x) * (g /. t) ) )

proof end;

theorem LM11: :: PDIFFEQ1:8

for f, g being PartFunc of REAL,REAL
for u being PartFunc of (REAL 2),REAL
for x0, t0 being Real
for z being Element of REAL 2 st dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & ( for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) ) & z = <*x0,t0*> & x0 in dom f & t0 in dom g holds
( u * (reproj (1,z)) = (g /. t0) (#) f & u * (reproj (2,z)) = (f /. x0) (#) g )

proof end;

theorem :: PDIFFEQ1:9

for f, g being PartFunc of REAL,REAL
for u being PartFunc of (REAL 2),REAL
for x0, t0 being Real
for z being Element of REAL 2 st x0 in dom f & t0 in dom g & z = <*x0,t0*> & dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & f is_differentiable_in x0 & ( for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) ) holds
( u is_partial_differentiable_in z,1 & partdiff (u,z,1) = (diff (f,x0)) * (g /. t0) )

proof end;

theorem :: PDIFFEQ1:10

for f, g being PartFunc of REAL,REAL
for u being PartFunc of (REAL 2),REAL
for x0, t0 being Real
for z being Element of REAL 2 st x0 in dom f & t0 in dom g & z = <*x0,t0*> & dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & g is_differentiable_in t0 & ( for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) ) holds
( u is_partial_differentiable_in z,2 & partdiff (u,z,2) = (f /. x0) * (diff (g,t0)) )

proof end;

theorem LM20: :: PDIFFEQ1:11

for X, T being Subset of REAL
for Z being Subset of (REAL 2)
for f, g being PartFunc of REAL,REAL
for u being PartFunc of (REAL 2),REAL st X c= dom f & T c= dom g & X is open & T is open & Z is open & Z = { <*x,t*> where x, t is Real : ( x in X & t in T ) } & dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & f is_differentiable_on X & g is_differentiable_on T & ( for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) ) holds
( u is_partial_differentiable_on Z,<*1*> & ( for x, t being Real st x in X & t in T holds
(u `partial| (Z,<*1*>)) /. <*x,t*> = (diff (f,x)) * (g /. t) ) & u is_partial_differentiable_on Z,<*2*> & ( for x, t being Real st x in X & t in T holds
(u `partial| (Z,<*2*>)) /. <*x,t*> = (f /. x) * (diff (g,t)) ) )

proof end;

theorem LM30: :: PDIFFEQ1:12

for X, T being Subset of REAL
for Z being Subset of (REAL 2)
for f, g being PartFunc of REAL,REAL
for u being PartFunc of (REAL 2),REAL st X c= dom f & T c= dom g & X is open & T is open & Z is open & Z = { <*x,t*> where x, t is Real : ( x in X & t in T ) } & dom u = { <*x,t*> where x, t is Real : ( x in dom f & t in dom g ) } & f is_differentiable_on 2,X & g is_differentiable_on 2,T & ( for x, t being Real st x in dom f & t in dom g holds
u /. <*x,t*> = (f /. x) * (g /. t) ) holds
( u is_partial_differentiable_on Z,<*1*> ^ <*1*> & ( for x, t being Real st x in X & t in T holds
(u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,X)) . 2) /. x) * (g /. t) ) & u is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st x in X & t in T holds
(u `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,T)) . 2) /. t) ) )

proof end;

theorem LM40: :: PDIFFEQ1:13

for f, g being Function of REAL,REAL
for u being PartFunc of (REAL 2),REAL
for c being Real st f is_differentiable_on 2, [#] REAL & g is_differentiable_on 2, [#] REAL & dom u = [#] (REAL 2) & ( for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t) ) & ( for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) ) holds
( u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )

proof end;

LM410: for A, e being Real
for f being PartFunc of REAL,REAL st f = A (#) (cos * (e (#) (id ([#] REAL)))) holds
( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f `| ([#] REAL)) . x = - ((A * e) * (sin . (e * x))) ) )

proof end;

LM411: for A, e being Real
for f being PartFunc of REAL,REAL st f = A (#) (sin * (e (#) (id ([#] REAL)))) holds
( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f `| ([#] REAL)) . x = (A * e) * (cos . (e * x)) ) )

proof end;

theorem LM412: :: PDIFFEQ1:14

for A, B, e being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) ) holds
( f is_differentiable_on [#] REAL & ( for x being Real holds (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) ) )

proof end;

theorem LM41: :: PDIFFEQ1:15

for A, B, e being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) ) holds
( f is_differentiable_on 2, [#] REAL & ( for x being Real holds
( (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) & ((f `| ([#] REAL)) `| ([#] REAL)) . x = - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) & (((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0 ) ) )

proof end;

theorem LM42: :: PDIFFEQ1:16

for A, B, e being Real ex f being Function of REAL,REAL st
for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x)))

proof end;

theorem LM43: :: PDIFFEQ1:17

for A, B, C, d, c, e being Real
for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) ) & ( for t being Real holds g . t = (C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))) ) holds
for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t)

proof end;

theorem LM50: :: PDIFFEQ1:18

for c being Real
for f, g being Function of REAL,REAL
for u being Function of (REAL 2),REAL st f is_differentiable_on 2, [#] REAL & g is_differentiable_on 2, [#] REAL & ( for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) ) & ( for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t) ) holds
( u is_partial_differentiable_on [#] (REAL 2),<*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = (diff (f,x)) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = (f /. x) * (diff (g,t)) ) & f is_differentiable_on 2, [#] REAL & g is_differentiable_on 2, [#] REAL & u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )

proof end;

theorem Th10: :: PDIFFEQ1:19

for A, B, C, d, e, c being Real
for u being Function of (REAL 2),REAL st ( for x, t being Real holds u /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))) ) holds
( u is_partial_differentiable_on [#] (REAL 2),<*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((- ((A * e) * (sin . (e * x)))) + ((B * e) * (cos . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((- ((C * (e * c)) * (sin . ((e * c) * t)))) + ((d * (e * c)) * (cos . ((e * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real holds
( (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - (((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - ((((e * c) ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) ) ) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )

proof end;

theorem :: PDIFFEQ1:20

for c being Real ex u being PartFunc of (REAL 2),REAL st
( u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )

proof end;

theorem :: PDIFFEQ1:21

for C, d, c being Real
for n being Nat
for u being Function of (REAL 2),REAL st ( for x, t being Real holds u /. <*x,t*> = (sin . ((n * PI) * x)) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t)))) ) holds
( u is_partial_differentiable_on [#] (REAL 2),<*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((n * PI) * (cos . ((n * PI) * x))) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = (sin . ((n * PI) * x)) * ((- ((C * ((n * PI) * c)) * (sin . (((n * PI) * c) * t)))) + ((d * ((n * PI) * c)) * (cos . (((n * PI) * c) * t)))) ) & u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real holds
( (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - ((((n * PI) ^2) * (sin . ((n * PI) * x))) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t))))) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - (((((n * PI) * c) ^2) * (sin . ((n * PI) * x))) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t))))) ) ) ) & ( for t being Real holds
( u /. <*0,t*> = 0 & u /. <*1,t*> = 0 ) ) & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )

proof end;

theorem Th30Y: :: PDIFFEQ1:22

for u, v being PartFunc of (REAL 2),REAL
for Z being Subset of (REAL 2)
for c being Real st Z is open & Z c= dom u & Z c= dom v & u is_partial_differentiable_on Z,<*1*> ^ <*1*> & u is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(u `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) & v is_partial_differentiable_on Z,<*1*> ^ <*1*> & v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(v `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((v `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) holds
( Z c= dom (u + v) & u + v is_partial_differentiable_on Z,<*1*> ^ <*1*> & u + v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) )

proof end;

theorem :: PDIFFEQ1:23

for u being Functional_Sequence of (REAL 2),REAL
for Z being Subset of (REAL 2)
for c being Real st Z is open & ( for i being Nat holds
( Z c= dom (u . i) & dom (u . i) = dom (u . 0) & u . i is_partial_differentiable_on Z,<*1*> ^ <*1*> & u . i is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((u . i) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u . i) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) ) ) holds
for i being Nat holds
( Z c= dom ((Partial_Sums u) . i) & (Partial_Sums u) . i is_partial_differentiable_on Z,<*1*> ^ <*1*> & (Partial_Sums u) . i is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(((Partial_Sums u) . i) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((((Partial_Sums u) . i) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) )

proof end;