Hi,
I think the expressions you mentioned are equivalent. I might have wrong
details..
Following explanation is for "integral" but I think it is applicable for
the case of "real_integral"
In general, we can split the infinite interval into two intervals
namely 0 to positive infinity {t| &0 <= t} and negative infinity to 0- {t|
t < &0}.
Then union of {t| &0 <= t} U {t| t < &0} = {x | T} or (:real).
Just to check I proved the following (proof is given at the end):
!f. f integrable_on {x | &0 <= drop x} /\
f integrable_on {x | drop x < &0}
==> integral {x | &0 <= drop x} f + integral {x | drop x < &0} f =
integral {x | T} f
Furthermore, it further can be defined using the limit at pos_infinity and
neg_infinity. For example (hol_light/multivariate/):
HAS_INTEGRAL_LIM_AT_POSINFINITY;;
val it : thm =
|- !f l.
(f has_integral l) {t | &0 <= drop t} <=>
(!a. f integrable_on interval [vec 0,a]) /\
((\a. integral (interval [vec 0,lift a]) f) --> l) at_posinfinity
Proof of the above mentioned split theorem:
let INTEGRAL_NEG_POS_INFINITY_SPLIT = prove(
` !f. f integrable_on {x | &0 <= drop x} /\
f integrable_on {x | drop x < &0} ==>
integral {x | &0 <= drop x} f + integral {x | drop x < &0}
f =
integral {x|T} f`,
IMP_REWRITE_TAC[GSYM INTEGRAL_UNION] THEN
SIMP_TAC[INTER;UNION;negligible;indicator;IN_ELIM_THM;
REAL_FIELD `&0 <= drop x /\ drop x < &0 <=> F`;
REAL_FIELD `&0 <= drop x \/ drop x < &0 <=> T`;HAS_INTEGRAL_0]);;
Best Regards,
-Umair
---------------------
*Umair Siddique *
*PhD Candidate, *
*Hardware Verification Group (HVG),*
*Concordia University, Montreal*
> Date: Wed, 13 Aug 2014 13:12:46 -0700
> From: Mohamed yousri soliman <[email protected]>
> Subject: [Hol-info] Integration from neg-infinity to pos-infinity,
> real functions
> To: [email protected]
> Message-ID:
> <
> call2dmjvjme3tqd+kxxfeqp7-kd17zrp7pkq+hflzz89jjz...@mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Dear All,
>
>
> I would like to know if the following definition in HOL Light
>
> `real_integral {x:real| T} f `
>
> is equivalent to int_{\-inf}^{\inf} f(x) dx.
>
> Note: math formula written in latex.
>
> Regards
>
>
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
