Hi Adnan,
| I am working in HOL Light and I want to verify the following theorem
| regarding integrability of a vector function:
|
| *f integrable_on (:real^1) ==> f integrable_on {t | a <= drop t}*
|
| which says that if a function is integrable on (-inf, inf) then it is
| integrable on its subset which looks true to me.
Indeed it is true, but you have put your finger on an unfortunate gap
in the libraries. For the absolute (=Lebesgue) integral, it is basic
that if a function is integrable on a set, it is integrable on any
Lebesgue measurable subset, so the variant with absolute integrability
is easy:
let ADNAN' = prove
(`!f:real^1->real^N a.
f absolutely_integrable_on (:real^1)
==> f absolutely_integrable_on {t | a <= drop t}`,
REPEAT GEN_TAC THEN
MATCH_MP_TAC(ONCE_REWRITE_RULE[IMP_CONJ_ALT]
ABSOLUTELY_INTEGRABLE_ON_LEBESGUE_MEASURABLE_SUBSET) THEN
REWRITE_TAC[SUBSET_UNIV; drop; GSYM real_ge] THEN
SIMP_TAC[LEBESGUE_MEASURABLE_CONVEX; CONVEX_HALFSPACE_COMPONENT_GE]);;
For the general gauge integral it is not the case that a function is
automatically integrable on measurable subsets; in fact this is equivalent
(ABSOLUTELY_INTEGRABLE_ON_LEBESGUE_MEASURABLE_SUBSET_EQ_ALT) to absolute
integrability, as you can see by taking the integrals over {x | f x >= 0}
and {x | f x < 0} and subtracting. But for special subsets like intervals
it is true. Unfortunately this is only proved in the libraries for the
still more special case of compact intervals (INTEGRABLE_ON_SUBINTERVAL).
For your case I can only think of a rather painful manual proof going back
to the basic definitions:
let ADNAN = prove
(`!f:real^1->real^N a.
f integrable_on (:real^1) ==> f integrable_on {t | a <= drop t}`,
REPEAT GEN_TAC THEN
SUBGOAL_THEN `{t | a <= drop t} = IMAGE (\x. lift a + x) {t | &0 <= drop t}`
SUBST1_TAC THENL
[REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM; UNWIND_THM1; DROP_SUB;
LIFT_DROP; VECTOR_ARITH `x:real^N = a + y <=> x - a = y`] THEN
REAL_ARITH_TAC;
SUBST1_TAC(SYM(ISPEC `lift a` TRANSLATION_UNIV)) THEN
REWRITE_TAC[GSYM INTEGRABLE_TRANSLATION] THEN
SPEC_TAC(`\x. (f:real^1->real^N) (lift a + x)`,`f:real^1->real^N`)] THEN
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[INTEGRABLE_ALT] THEN
ONCE_REWRITE_TAC[INTEGRABLE_RESTRICT_INTER; INTEGRAL_RESTRICT_INTER] THEN
REWRITE_TAC[INTER; IN_INTERVAL_1; IN_ELIM_THM] THEN
REWRITE_TAC[CONJ_ASSOC; GSYM REAL_MAX_LE] THEN
ONCE_REWRITE_TAC[MESON[LIFT_DROP] `max a b = drop(lift(max a b))`] THEN
SIMP_TAC[GSYM IN_INTERVAL_1; SET_RULE `{x | x IN s} = s`] THEN CONJ_TAC
THENL
[ASM_MESON_TAC[INTEGRABLE_ON_SUBINTERVAL; SUBSET_UNIV]; ALL_TAC] THEN
X_GEN_TAC `e:real` THEN DISCH_TAC THEN
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INTEGRABLE_ALT]) THEN
DISCH_THEN(MP_TAC o SPEC `e:real` o CONJUNCT2) THEN
ASM_REWRITE_TAC[IN_UNIV; ETA_AX; BALL_1; SUBSET_INTERVAL_1] THEN
REWRITE_TAC[VECTOR_ADD_LID; VECTOR_SUB_LZERO; LIFT_DROP; DROP_NEG] THEN
ONCE_REWRITE_TAC[TAUT `p /\ q <=> ~(p ==> ~q)`] THEN
SIMP_TAC[REAL_ARITH `&0 < B ==> ~(B <= --B) /\ --B < B`] THEN
REWRITE_TAC[NOT_IMP] THEN MATCH_MP_TAC MONO_EXISTS THEN
X_GEN_TAC `B:real` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
MAP_EVERY X_GEN_TAC [`u:real^1`; `v:real^1`; `w:real^1`; `x:real^1`] THEN
STRIP_TAC THEN
SUBGOAL_THEN `max (&0) (drop u) = &0 /\ max (&0) (drop w) = &0`
(CONJUNCTS_THEN SUBST1_TAC) THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`--lift B`; `v:real^1`; `--lift B`; `x:real^1`]) THEN
ASM_REWRITE_TAC[DROP_NEG; LIFT_DROP; REAL_LE_REFL] THEN
MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
FIRST_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
INTEGRABLE_ON_SUBINTERVAL)) THEN
REWRITE_TAC[SUBSET_UNIV] THEN STRIP_TAC THEN
MP_TAC(ISPECL [`f:real^1->real^N`; `--lift B`; `v:real^1`; `vec 0:real^1`]
INTEGRAL_COMBINE) THEN
MP_TAC(ISPECL [`f:real^1->real^N`; `--lift B`; `x:real^1`; `vec 0:real^1`]
INTEGRAL_COMBINE) THEN
ASM_REWRITE_TAC[DROP_VEC; DROP_NEG; LIFT_DROP] THEN
REPEAT
(ANTS_TAC THENL [ASM_REAL_ARITH_TAC; DISCH_THEN(SUBST1_TAC o SYM)]) THEN
REWRITE_TAC[LIFT_NUM] THEN CONV_TAC VECTOR_ARITH);;
I'll think about adding some useful general lemmas to the libraries to
make theorems of this form easier.
John.
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
