Hmmm… I just found NUMINF_2D in seqTheory: (actually it’s me who moved this theorem from util_probTheory here)
[SUMINF_2D] Theorem
⊢ ∀f g h.
(∀m n. 0 ≤ f m n) ∧ (∀n. f n sums g n) ∧ summable g ∧
BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
UNCURRY f ∘ h sums suminf g
sorry for disturbing…
—Chun
> Il giorno 04 ott 2018, alle ore 20:41, Chun Tian (binghe)
> <binghe.l...@gmail.com> ha scritto:
>
> Hi,
>
> suppose I have a function (f :num -> num -> real), and I want to calculate
> the sum of (f i j) on the entire plane, one way is to use double suminf:
> (assuming it is always summable, i.e. any sum is finite)
>
> suminf (λi. suminf (λj. f i j))) (1)
>
> However, there’s another way using single suminf, based on numpairTheory:
>
> suminf (λn. f (nfst n) (nsnd n)) (2)
>
> My question is: how can I prove (1) and (2) are equal, i.e.:
>
> suminf (λi. suminf (λj. f i j))) = suminf (λn. f (nfst n) (nsnd n))
>
> ?
>
> --Chun
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
