--- a/CONTRIBUTORS Thu Apr 18 11:39:51 2024 +0200
+++ b/CONTRIBUTORS Thu Apr 18 15:20:24 2024 +0200
@@ -14,6 +14,9 @@
* March 2024: Manuel Eberl
Weierstraß Factorization Theorem in HOL-Complex_Analysis.
+* March 2024: Ata Keskin
+ Analysis lemmas drawn from the Martingales AFP entry.
+
* March 2024: Anthony Bordg, Manuel Eberl, Wenda Li, Larry Paulson
New and more general definition of meromorphicity in HOL-Complex_Analysis.
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu Apr 18 11:39:51 2024 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Thu Apr 18 15:20:24 2024 +0200
@@ -2,6 +2,7 @@
Author: Amine Chaieb, University of Cambridge
Author: Robert Himmelmann, TU Muenchen
Author: Brian Huffman, Portland State University
+ Author: Ata Keskin, TU Muenchen
*)
chapter \<open>Elementary Metric Spaces\<close>
--- a/src/HOL/Analysis/Set_Integral.thy Thu Apr 18 11:39:51 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Thu Apr 18 15:20:24 2024 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Analysis/Set_Integral.thy
Author: Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr
+ Author: Ata Keskin, TU Muenchen
Notation and useful facts for working with integrals over a set.