Hi Adnan,
| I am working in HOL Light and I want to prove the following theorem
| regarding integral:
|
| !b. f absolutely_integrable_on interval [lift a,lift b]
| ==> (?k. ((\b. real_integral (real_interval [a,b])
| (\t. norm (f (lift t)))) ---> k) at_posinfinity)
|
| which says that if a function is absolutely integrable on [a, infinity),
| i.e., the norm of function f is convergent then integral of fucntion's norm
| over the same interval approaches to some limit value k which is actually
| true.
I think you'll need to change the hypothesis from just the existence
of the integral over [a,b] for every b to explicitly saying that the
integral over [a,infinity) exists. (Otherwise, for example, the
identity function would be a counterexample.) For that semi-infinite
interval you'll have to use something like {t | a <= drop t}, since
there is no nicer notation pre-defined.
As for the proof, there is already a closely related theorem called
HAS_INTEGRAL_LIM_AT_POSINFINITY. But looking at your problem made me
realize that it is a bit less general than it should be: it assumes
the interval is [0,infinity) not a general [a,infinity). So let's
first generalize that a bit (maybe I will install this version into
the libraries):
let HAS_INTEGRAL_LIM_AT_POSINFINITY_GEN = prove
(`!f a l:real^N.
(f has_integral l) {t | a <= drop t} <=>
(!b. f integrable_on interval[lift a,lift b]) /\
((\b. integral (interval[lift a,lift b]) f) --> l) at_posinfinity`,
REPEAT GEN_TAC THEN
SUBGOAL_THEN
`{t | a <= drop t} = IMAGE (\x. lift a + x) {t | &0 <= drop t}`
SUBST1_TAC THENL
[CONV_TAC SYM_CONV THEN MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN
REWRITE_TAC[IN_ELIM_THM; DROP_ADD; LIFT_DROP; REAL_LE_ADDR] THEN
MESON_TAC[VECTOR_SUB_ADD2];
REWRITE_TAC[GSYM HAS_INTEGRAL_TRANSLATION]] THEN
REWRITE_TAC[HAS_INTEGRAL_LIM_AT_POSINFINITY] THEN
REWRITE_TAC[INTEGRABLE_TRANSLATION; INTEGRAL_TRANSLATION] THEN
REWRITE_TAC[GSYM INTERVAL_TRANSLATION; VECTOR_ADD_RID] THEN
REWRITE_TAC[FORALL_LIFT; GSYM LIFT_ADD] THEN
MP_TAC(MESON[REAL_SUB_ADD2] `!P. (!b:real. P(a + b)) <=> (!b. P b)`) THEN
SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN
MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
DISCH_TAC THEN
REWRITE_TAC[LIM_AT_POSINFINITY; real_ge] THEN
EQ_TAC THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_TAC `b:real`) THEN EXISTS_TAC `abs a + abs b:real` THEN
X_GEN_TAC `c:real` THEN DISCH_TAC THENL
[SUBST1_TAC(REAL_ARITH `c:real = a + (c - a)`) THEN
REWRITE_TAC[GSYM LIFT_ADD];
ALL_TAC] THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REAL_ARITH_TAC);;
With that as a lemma, your result is more or less just a matter of
using the definition of absolute integrability and tweaking a few
types between R^1 and R. Here is my version:
let ADNAN_LEMMA = prove
(`!f:real^1->real^1 a.
f absolutely_integrable_on {t | a <= drop t}
==> ?k. ((\b. real_integral (real_interval[a,b])
(\t. norm(f(lift t))))
---> k) at_posinfinity`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
ABSOLUTELY_INTEGRABLE_IMP_LIFT_NORM_INTEGRABLE) THEN
DISCH_THEN(MP_TAC o MATCH_MP INTEGRABLE_INTEGRAL) THEN
REWRITE_TAC[HAS_INTEGRAL_LIM_AT_POSINFINITY_GEN] THEN
SIMP_TAC[REAL_INTEGRAL; REAL_INTEGRABLE_ON; o_DEF; LIFT_DROP;
IMAGE_LIFT_REAL_INTERVAL] THEN
REWRITE_TAC[REAL_TENDSTO; o_DEF] THEN MESON_TAC[]);;
John.
------------------------------------------------------------------------------
Site24x7 APM Insight: Get Deep Visibility into Application Performance
APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
Monitor end-to-end web transactions and take corrective actions now
Troubleshoot faster and improve end-user experience. Signup Now!
http://pubads.g.doubleclick.net/gampad/clk?id=267308311&iu=/4140
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
