A little more material from the Fourier AFP entry, and the correction of two very slow proof lines

--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Wed Sep 25 21:39:43 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Thu Sep 26 12:24:02 2019 +0100
@@ -58,7 +58,7 @@
         and sub3: "\<And>C. \<lbrakk>C \<in> \<D>; \<not> disjnt C D\<rbrakk> \<Longrightarrow> C \<subseteq> cbox a3 b3"
       proof -
         obtain k a b where ab: "D = cbox a b" and k: "\<And>i. i \<in> Basis \<Longrightarrow> b\<bullet>i - a\<bullet>i = k"
-          using less.prems \<open>D \<in> \<D>\<close> by blast
+          using less.prems \<open>D \<in> \<D>\<close> by meson
         then have eqk: "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i \<longleftrightarrow> k \<ge> 0"
           by force
         show thesis
@@ -72,7 +72,7 @@
           show "C \<subseteq> cbox ?a ?b" if "C \<in> \<D>" and CD: "\<not> disjnt C D" for C
           proof -
             obtain k' a' b' where ab': "C = cbox a' b'" and k': "\<And>i. i \<in> Basis \<Longrightarrow> b'\<bullet>i - a'\<bullet>i = k'"
-              using less.prems \<open>C \<in> \<D>\<close> by blast
+              using less.prems \<open>C \<in> \<D>\<close> by meson
             then have eqk': "\<And>i. i \<in> Basis \<Longrightarrow> a' \<bullet> i \<le> b' \<bullet> i \<longleftrightarrow> k' \<ge> 0"
               by force
             show ?thesis
@@ -1706,4 +1706,38 @@
     by (meson \<open>a \<le> c\<close> \<open>c \<le> b\<close> has_bochner_integral_combine has_bochner_integral_iff i j)
 qed
 
+lemma has_bochner_integral_null [intro]:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "N \<in> null_sets lebesgue"
+  shows "has_bochner_integral (lebesgue_on N) f 0"
+  unfolding has_bochner_integral_iff \<comment>\<open>strange that the proof's so long\<close>
+proof
+  show "integrable (lebesgue_on N) f"
+  proof (subst integrable_restrict_space)
+    show "N \<inter> space lebesgue \<in> sets lebesgue"
+      using assms by force
+    show "integrable lebesgue (\<lambda>x. indicat_real N x *\<^sub>R f x)"
+    proof (rule integrable_cong_AE_imp)
+      show "integrable lebesgue (\<lambda>x. 0)"
+        by simp
+      show *: "AE x in lebesgue. 0 = indicat_real N x *\<^sub>R f x"
+        using assms
+        by (simp add: indicator_def completion.null_sets_iff_AE eventually_mono)
+      show "(\<lambda>x. indicat_real N x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+        by (auto intro: borel_measurable_AE [OF _ *])
+    qed
+  qed
+  show "integral\<^sup>L (lebesgue_on N) f = 0"
+  proof (rule integral_eq_zero_AE)
+    show "AE x in lebesgue_on N. f x = 0"
+      by (rule AE_I' [where N=N]) (auto simp: assms null_setsD2 null_sets_restrict_space)
+  qed
+qed
+
+lemma has_bochner_integral_null_eq[simp]:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "N \<in> null_sets lebesgue"
+  shows "has_bochner_integral (lebesgue_on N) f i \<longleftrightarrow> i = 0"
+  using assms has_bochner_integral_eq by blast
+
 end

--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 25 21:39:43 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 26 12:24:02 2019 +0100
@@ -2768,6 +2768,52 @@
     by (simp add: integral_unique)
 qed
 
+lemma has_integral_sin_nx: "((\<lambda>x. sin(real_of_int n * x)) has_integral 0) {-pi..pi}"
+proof (cases "n = 0")
+  case False
+  have "((\<lambda>x. sin (n * x)) has_integral (- cos (n * pi)/n - - cos (n * - pi)/n)) {-pi..pi}"
+  proof (rule fundamental_theorem_of_calculus)
+    show "((\<lambda>x. - cos (n * x) / n) has_vector_derivative sin (n * a)) (at a within {-pi..pi})"
+      if "a \<in> {-pi..pi}" for a :: real
+      using that False
+      apply (simp only: has_vector_derivative_def)
+      apply (rule derivative_eq_intros | force)+
+      done
+  qed auto
+  then show ?thesis
+    by simp
+qed auto
+
+lemma integral_sin_nx:
+   "integral {-pi..pi} (\<lambda>x. sin(x * real_of_int n)) = 0"
+  using has_integral_sin_nx [of n] by (force simp: mult.commute)
+
+lemma has_integral_cos_nx:
+  "((\<lambda>x. cos(real_of_int n * x)) has_integral (if n = 0 then 2 * pi else 0)) {-pi..pi}"
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    using has_integral_const_real [of "1::real" "-pi" pi] by auto
+next
+  case False
+  have "((\<lambda>x. cos (n * x)) has_integral (sin (n * pi)/n - sin (n * - pi)/n)) {-pi..pi}"
+  proof (rule fundamental_theorem_of_calculus)
+    show "((\<lambda>x. sin (n * x) / n) has_vector_derivative cos (n * x)) (at x within {-pi..pi})"
+      if "x \<in> {-pi..pi}"
+      for x :: real
+      using that False
+      apply (simp only: has_vector_derivative_def)
+      apply (rule derivative_eq_intros | force)+
+      done
+  qed auto
+  with False show ?thesis
+    by (simp add: mult.commute)
+qed
+
+lemma integral_cos_nx:
+   "integral {-pi..pi} (\<lambda>x. cos(x * real_of_int n)) = (if n = 0 then 2 * pi else 0)"
+  using has_integral_cos_nx [of n] by (force simp: mult.commute)
+
 
 subsection \<open>Taylor series expansion\<close>