:: 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
::
:: 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
coherence
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,())) /. <*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,())) /. <*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,())) . 2) /. t) = ((c ^2) * (((diff (f,())) . 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)),())) /. <*x,t*> = (((diff (f,())) . 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)),())) /. <*x,t*> = (f /. x) * (((diff (g,())) . 2) /. t) ) & ( for x, t being Real holds (u partial| (([#] (REAL 2)),())) /. <*x,t*> = (c ^2) * ((u partial| (([#] (REAL 2)),())) /. <*x,t*>) ) )
proof end;

LM410: for A, e being Real
for f being PartFunc of REAL,REAL st f = A (#) (cos * (e (#) (id ()))) holds
( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f | ()) . 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 ()))) holds
( f is_differentiable_on [#] REAL & ( for x being Real st x in [#] REAL holds
(f | ()) . 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 | ()) . 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 | ()) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) & ((f | ()) | ()) . x = - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) & (((diff (f,())) . 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,())) . 2) /. t) = ((c ^2) * (((diff (f,())) . 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,())) . 2) /. t) = ((c ^2) * (((diff (f,())) . 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)),())) /. <*x,t*> = (((diff (f,())) . 2) /. x) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u partial| (([#] (REAL 2)),())) /. <*x,t*> = (f /. x) * (((diff (g,())) . 2) /. t) ) & ( for x, t being Real holds (u partial| (([#] (REAL 2)),())) /. <*x,t*> = (c ^2) * ((u partial| (([#] (REAL 2)),())) /. <*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)),())) /. <*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)),())) /. <*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)),())) /. <*x,t*> = (c ^2) * ((u partial| (([#] (REAL 2)),())) /. <*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)),())) /. <*x,t*> = (c ^2) * ((u partial| (([#] (REAL 2)),())) /. <*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)),())) /. <*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)),())) /. <*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)),())) /. <*x,t*> = (c ^2) * ((u partial| (([#] (REAL 2)),())) /. <*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,())) /. <*x,t*> = (c ^2) * ((u partial| (Z,())) /. <*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,())) /. <*x,t*> = (c ^2) * ((v partial| (Z,())) /. <*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,())) /. <*x,t*> = (c ^2) * (((u + v) partial| (Z,())) /. <*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,())) /. <*x,t*> = (c ^2) * (((u . i) partial| (Z,())) /. <*x,t*>) ) ) ) holds
for i being Nat holds
( Z c= dom (() . i) & () . i is_partial_differentiable_on Z,<*1*> ^ <*1*> & () . i is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((() . i) partial| (Z,())) /. <*x,t*> = (c ^2) * (((() . i) partial| (Z,())) /. <*x,t*>) ) )
proof end;