diff -r 2cd0dd4de9c3 -r b98f1057da0e src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Aug 06 18:14:45 2024 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue Aug 06 22:47:44 2024 +0100
@@ -2512,6 +2512,16 @@
     by (smt (verit) AE_I2 borel_measurable_count_space density_cong ennreal_neg point_measure_def)
 qed
 
+lemma integral_uniform_count_measure:
+  assumes "finite A" 
+  shows "integral\<^sup>L (uniform_count_measure A) f = sum f A / (card A)"
+proof -
+  have "integral\<^sup>L (uniform_count_measure A) f = (\<Sum>x\<in>A. f x / card A)" 
+    using assms by (simp add: uniform_count_measure_def lebesgue_integral_point_measure_finite)
+  with assms show ?thesis
+    by (simp add: sum_divide_distrib nn_integral_count_space_finite)
+qed
+
 subsection \<open>Lebesgue integration on \<^const>\<open>null_measure\<close>\<close>
 
 lemma has_bochner_integral_null_measure_iff[iff]: