Isabelle n-ary summation and L2 norm

Question

我正在学习Isabelle，我想浏览一些例子，看看真正的分析是如何形式化的。

https://isabelle.in.tum.de/library/HOL/HOL-Analysis/L2_Norm.html

我看到了这个定义

definition L2_set :: "('a ⇒ real) ⇒ 'a set ⇒ real" where 
"L2_set f A = sqrt (∑ i∈A. (f i)⇧2)"

我一直在试图找到更多关于求和∑，但我在手册中找不到太多的信息。我在查询

中找到结果

found 10 theorem(s):
Set_Interval.card_sum_le_nat_sum: ∑ {0..<card ?S} ≤ ∑ ?S
Groups_List.comm_monoid_add_class.distinct_sum_list_conv_Sum: distinct ?xs ⟹ sum_list ?xs = ∑ (set ?xs)
Set_Interval.gauss_sum_nat: ∑ {0..?n} = ?n * Suc ?n div 2
Groups_Big.comm_monoid_add_class.sum.image_eq: inj_on ?g ?A ⟹ ∑ (?g ` ?A) = sum ?g ?A
Groups_List.sum_list_upt: ?m ≤ ?n ⟹ sum_list [?m..<?n] = ∑ {?m..<?n}
Complex.sum_roots_unity: 1 < ?n ⟹ ∑ {z. z ^ ?n = 1} = 0
Complex.sum_nth_roots: 1 < ?n ⟹ ∑ {z. z ^ ?n = ?c} = 0
Set_Interval.Sum_Icc_nat: ∑ {?m..?n} = (?n * (?n + 1) - ?m * (?m - 1)) div 2
Set_Interval.Sum_Ico_nat: ∑ {?m..<?n} = (?n * (?n - 1) - ?m * (?m - 1)) div 2
Set_Interval.Sum_Icc_int: ?m ≤ ?n ⟹ ∑ {?m..?n} = (?n * (?n + 1) - ?m * (?m - 1)) div 2

但是在这种情况下，我怎么知道哪个是正确的定义呢?

还有一个非常惊人的引理

lemma L2_set_infinite [simp]: "¬ finite A ⟹ L2_set f A = 0"
unfolding L2_set_def by simp

我真的不明白为什么无限集的L2范数等于0。它看起来有点像勒贝格对测度f的积分但也许我错了。如果有人能给我指出一些资源或解释一下这个有趣的片段是如何工作的，我将非常感激。

Answer 1

这个符号是sum的漂亮语法。它来自

subsection ‹Generalized summation over a set›
context comm_monoid_add
begin
sublocale sum: comm_monoid_set plus 0
defines sum = sum.F and sum' = sum.G ..
abbreviation Sum ("∑")
where "∑ ≡ sum (λx. x)"
end

在jEdit中，可以通过按CTRL并单击术语/符号跳转到定义。不幸的是，这有时不起作用(可能是因为类型统一没有完全正确?)如果是这种情况，您可以尝试创建一些使用该术语的虚拟引理和定义，并希望在某个时候jEdit能够赶上来。然后可以直接跳转到定义。