CODEWITHSUNDEEP
isabelle
alagris
alagris

Reputation: 2206

Isabelle n-ary summation and L2 norm

I'm learning Isabelle and I wanted to glance through some examples of how real analysis is formalized.

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

I see this definition


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

I've been trying to find out more about the summation ∑ but I can't find much information on this in manuals. I found results in query

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

but how can I know which one of these is the right definition in this case?

There is also this very surprising lemma.


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

I can't really see why infinite set would have L2 norm equal 0. It looks somewhat like Lebesgue integral with measure f but maybe I'm wrong. If anybody could point me to some resources or explain how this intriguing snippet works, I'd be really grateful.

Upvotes: 0

Views: 52

Answers (1)

alagris
alagris

Reputation: 2206

This symbol is a pretty syntax for sum. It comes from


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

In jEdit it is possible to jump to definition by pressing CTRL and clicking on the term/symbol. Unfortunately this sometimes doesn't work (probably because type unification didn't quite get it right?). If that's the case you might try creating some dummy lemmas and definitions that use this term and hope that at some point jEdit will catch up. Then you can jump straight to definition.

Upvotes: 0

Related Questions