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) > <[email protected]> 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)" <[email protected]> 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 > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
