:: Several Integrability Formulas of Some Functions, Orthogonal Polynomialsand Norm Functions
:: by Bo Li , Yanping Zhuang , Bing Xie and Pan Wang
::
:: Received October 14, 2008
:: Copyright (c) 2008 Association of Mizar Users
Lm1:
dom (- (exp_R * (AffineMap (- 1),0 ))) = [#] REAL
by FUNCT_2:def 1;
theorem Th1: :: INTEGRA9:1
theorem :: INTEGRA9:2
Lm2:
dom ((1 / 2) (#) (exp_R * (AffineMap 2,0 ))) = [#] REAL
by FUNCT_2:def 1;
theorem Th3: :: INTEGRA9:3
theorem :: INTEGRA9:4
theorem Th5: :: INTEGRA9:5
theorem :: INTEGRA9:6
Lm3:
dom ((- (1 / 2)) (#) (cos * (AffineMap 2,0 ))) = [#] REAL
by FUNCT_2:def 1;
theorem :: INTEGRA9:7
theorem Th8: :: INTEGRA9:8
theorem :: INTEGRA9:9
Lm4:
dom ((1 / 2) (#) (sin * (AffineMap 2,0 ))) = [#] REAL
by FUNCT_2:def 1;
theorem Th10: :: INTEGRA9:10
theorem :: INTEGRA9:11
theorem Th12: :: INTEGRA9:12
theorem :: INTEGRA9:13
theorem :: INTEGRA9:14
theorem :: INTEGRA9:15
theorem Th16: :: INTEGRA9:16
Lm5:
for x being Real holds
( - sin is_differentiable_in x & diff (- sin ),x = - (cos . x) )
theorem Th17: :: INTEGRA9:17
theorem :: INTEGRA9:18
theorem Th19: :: INTEGRA9:19
theorem :: INTEGRA9:20
theorem :: INTEGRA9:21
theorem :: INTEGRA9:22
theorem :: INTEGRA9:23
theorem Th24: :: INTEGRA9:24
theorem :: INTEGRA9:25
theorem Th26: :: INTEGRA9:26
theorem Th27: :: INTEGRA9:27
theorem Th28: :: INTEGRA9:28
theorem :: INTEGRA9:29
:: deftheorem defines |||( INTEGRA9:def 1 :
theorem :: INTEGRA9:30
theorem :: INTEGRA9:31
theorem :: INTEGRA9:32
theorem :: INTEGRA9:33
theorem :: INTEGRA9:34
theorem :: INTEGRA9:35
theorem :: INTEGRA9:36
theorem Th37: :: INTEGRA9:37
for
f,
g being
PartFunc of
REAL ,
REAL for
A being
closed-interval Subset of
REAL st
(f (#) f) || A is
total &
(f (#) g) || A is
total &
(g (#) g) || A is
total &
((f (#) f) || A) | A is
bounded &
((f (#) g) || A) | A is
bounded &
((g (#) g) || A) | A is
bounded &
f (#) f is_integrable_on A &
f (#) g is_integrable_on A &
g (#) g is_integrable_on A holds
|||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)|||
:: deftheorem Def2 defines is_orthogonal_with INTEGRA9:def 2 :
theorem Th38: :: INTEGRA9:38
theorem :: INTEGRA9:39
theorem :: INTEGRA9:40
theorem :: INTEGRA9:41
theorem :: INTEGRA9:42
theorem :: INTEGRA9:43
theorem :: INTEGRA9:44
theorem :: INTEGRA9:45
theorem :: INTEGRA9:46
theorem :: INTEGRA9:47
theorem :: INTEGRA9:48
:: deftheorem defines ||.. INTEGRA9:def 3 :
theorem :: INTEGRA9:49
theorem :: INTEGRA9:50
theorem :: INTEGRA9:51
theorem :: INTEGRA9:52
theorem :: INTEGRA9:53
theorem :: INTEGRA9:54
theorem :: INTEGRA9:55
theorem :: INTEGRA9:56
theorem :: INTEGRA9:57
theorem :: INTEGRA9:58
theorem :: INTEGRA9:59
theorem :: INTEGRA9:60
theorem :: INTEGRA9:61
theorem :: INTEGRA9:62
theorem :: INTEGRA9:63
theorem :: INTEGRA9:64
theorem :: INTEGRA9:65
theorem :: INTEGRA9:66
theorem :: INTEGRA9:67
theorem :: INTEGRA9:68
theorem :: INTEGRA9:69
theorem :: INTEGRA9:70
theorem :: INTEGRA9:71
theorem :: INTEGRA9:72
theorem :: INTEGRA9:73
theorem :: INTEGRA9:74
theorem :: INTEGRA9:75
theorem Th31: :: INTEGRA9:76
theorem :: INTEGRA9:77