Isabelle中n元求和与L2范数的定义及疑问咨询

一、集合求和符号∑的核心定义 #

Isabelle/HOL里的∑ i∈A. f i是有限集合专属的求和算子，核心定义在Groups_Big库的comm_monoid_add_class模块中，本质是对有限集合内所有元素遍历累加。你查到的10条定理都是基于这个核心定义的衍生规则：

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

其中最核心的关联是Groups_List.comm_monoid_add_class.distinct_sum_list_conv_Sum——它直接把集合求和和列表求和绑定，明确了集合求和的有限累加本质。

二、L2_set_infinite引理的本质原因 #

先看你提到的L2_set定义：

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

以及困惑的引理：

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

这个引理的根源是Isabelle对无穷集合求和的约定：由于∑仅针对有限集合定义，当集合A无穷时，HOL会将这类无意义的求和结果默认设为加法单位元（也就是0）。开平方后自然还是0。

注意：这个L2_set是离散有限集合上的L2范数，和实分析中基于Lebesgue积分的L2空间范数完全不是一回事。如果要形式化实分析中的L2空间，需要使用HOL-Measure或HOL-Analysis中基于测度积分的定义，而非这个简化版的L2_set。

三、学习参考方向 #

• 直接查看Isabelle源码中的Groups_Big.thy，里面有集合求和的完整定义和基础推导
• 参考HOL-Analysis库的L2.thy模块，这里是实分析中L2空间的正式形式化
• 《Programming and Proving in Isabelle/HOL》手册中“Sets and Functions”“Summation”章节，能帮你理清集合求和的基础逻辑

内容的提问来源于stack exchange，提问作者alagris