Fair enough. It seems clear that this is not a huge problem (using a function
such as this outside of its intended domain is a bad idea), but on the other
hand, it also seems clear that needlessly having it return the wrong value is a
bug.
Having said all that, getting suminf (\x. -1) to return -1 doesn't seem much of
a win: the sum of an infinite sequence of -1s is hardly -1.
I think it would be better style to use new_specification so as to avoid giving
a specific value when the argument is not always positive.
Michael
On 20/9/19, 09:51, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
In fact, even for arbitrary functions with both positive and negative
values, if the partial sum ever reached +/-Inf, further adding finite values on
the other side cannot “pull” the result back to “normal”. For instance, suppose
at some moment the partial sum is +inf, adding any normal reals will not change
it, it’s then not allowed to add -Inf on it, because under the textbook
definition of `+`, PosInf + NegInf is unspecified. Thus, in some sense the
suminf of possible limiting values has a very different behavior with the real
version.
Chun
Inviato da iPad
> Il giorno 20 set 2019, alle ore 01:33, Chun Tian (binghe)
<binghe.l...@gmail.com> ha scritto:
>
> Hi,
>
> The extreal version of `suminf` is only “correct” and equivalent with the
real version when the involved function is positive - the partial sum is
mono-increasing. Its relatively simple definition serves the current need (in
measure and probability theories). Fully mimicking the real version requires a
(full) porting of seqTheory (and limTheory, netsTheory, eventually
metricTheory) to extreals, which is an almost impossible task in my opinion.
>
> Besides, I think it’s also not needed to do so, because if the sum limit
never reaches +Inf, one can just reduce the work back to the ‘suminf’ of reals.
On the hand, If the partial sum ever reached +Inf, assuming it’s monotonic,
then the limit value must be also +Inf, it’s reduced to a finite sum.
>
> Chun
>
>> Il giorno 20 set 2019, alle ore 01:00, Norrish, Michael (Data61, Acton)
<michael.norr...@data61.csiro.au> ha scritto:
>>
>> The definition of suminf over the reals (in seqTheory) is completely
different; is it clear that the extreal version can't mimic the original?
>>
>> Michael
>>
>> On 18/9/19, 06:18, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
>>
>> Hi,
>>
>> I occasionally found that HOL's current definition of ext_suminf
(extrealTheory) has a bug:
>>
>> [ext_suminf_def] Definition
>> ⊢ ∀f. suminf f = sup (IMAGE (λn. ∑ f (count n)) 𝕌(:num))
>>
>> The purpose of `suminf f` is to calculate an infinite sum: f(0) + f(1)
+ .... To make the resulting summation "meaningful", all lemmas about
ext_suminf assume that (!n. 0 <= f n) (f is positive). This also indeed how
it's used in all applications. For instance, one lemma says, if f is positive,
so is `suminf f`:
>>
>> [ext_suminf_pos] Theorem
>> ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f
>>
>> However, I found that the above lemma can be proved even without
knowing anything of `f`, see the following proofs:
>>
>> Theorem ext_suminf_pos_bug :
>> !f. 0 <= ext_suminf f
>> Proof
>> RW_TAC std_ss [ext_suminf_def]
>>>> MATCH_MP_TAC le_sup_imp'
>>>> REWRITE_TAC [IN_IMAGE, IN_UNIV]
>>>> Q.EXISTS_TAC `0` >> BETA_TAC
>>>> REWRITE_TAC [COUNT_ZERO, EXTREAL_SUM_IMAGE_EMPTY]
>> QED
>>
>> where [le_sup_imp'] is a version of [le_sup_imp] before applying
IN_APP:
>>
>> [le_sup_imp'] Theorem
>>
>> ⊢ ∀p x. x ∈ p ⇒ x ≤ sup p
>>
>> For the reason, ext_suminf is actually calculating the sup of the
following values:
>>
>> 0
>> f(0)
>> f(0) + f(1)
>> f(0) + f(1) + f(2)
>> ...
>>
>> The first line (0) comes from `count 0 = {}` where `0 IN univ(:num)`,
then SUM_IMAGE f {} = 0.
>>
>> Now consider f = (\n. -1), the above list of values are: 0, -1, -2, -3
.... But since the sup of a set containing 0 is at least 0, the `suminf f` in
this case will be 0 (instead of the correct value -1). This is why `0 <=
suminf f` holds for whatever f.
>>
>> I believe Isabelle's suminf (in Extended_Real.thy) has the same
problem (but I can't find its definition, correct me if I'm wrong here), i.e.
the following theorem holds even without the "assumes":
>>
>> lemma suminf_0_le:
>> fixes f :: "nat ⇒ ereal"
>> assumes "⋀n. 0 ≤ f n"
>> shows "0 ≤ (∑n. f n)"
>> using suminf_upper[of f 0, OF assms]
>> by simp
>>
>> The solution is quite obvious. I'm going to fix HOL's definition of
ext_suminf with the following one:
>>
>> val ext_suminf_def = Define
>> `ext_suminf f = sup (IMAGE (\n. SIGMA f (count (SUC n))) UNIV)`;
>>
>> That is, using `SUC n` intead of `n` to eliminate the fake base case
(0). I believe this change only causes minor incompatibilities.
>>
>> Any comment?
>>
>> Regards,
>>
>> Chun Tian
>>
>>
>>
>>
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
