# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1713442054 -3600
# Node ID e414bcc5a39ea6d196e3ac41e25e492e146c05e2
# Parent  ef2134570abb6090fa65107661ec8c3f4ffc06e0
Acknowledgement of Ata Keskin for his Martingales material

diff -r ef2134570abb -r e414bcc5a39e CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Apr 17 23:22:32 2024 +0200
+++ b/CONTRIBUTORS	Thu Apr 18 13:07:34 2024 +0100
@@ -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.
 
diff -r ef2134570abb -r e414bcc5a39e src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed Apr 17 23:22:32 2024 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Apr 18 13:07:34 2024 +0100
@@ -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>
diff -r ef2134570abb -r e414bcc5a39e src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Wed Apr 17 23:22:32 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Thu Apr 18 13:07:34 2024 +0100
@@ -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.