src/HOL/Probability/Characteristic_Functions.thy

     (2*\<bar>t\<bar>^n / fact n) * expectation (\<lambda>x. \<bar>x\<bar>^n)" (is "cmod (char M t - ?t1) \<le> _")
 proof -
   have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
     by (intro integrable_const_bound) auto
   
-  def c \<equiv> "\<lambda>k x. (ii * t)^k / fact k * complex_of_real (x^k)"
+  define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x
   have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
     unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
   
   have "k \<le> n \<Longrightarrow> expectation (c k) = (\<i>*t) ^ k * (expectation (\<lambda>x. x ^ k)) / fact k" for k
     unfolding c_def integral_mult_right_zero integral_complex_of_real by simp

     (is "cmod (char M t - ?t1) \<le> _")
 proof -
   have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
     by (intro integrable_const_bound) auto
   
-  def c \<equiv> "\<lambda>k x. (ii * t)^k / fact k * complex_of_real (x^k)"
+  define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x
   have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
     unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
 
   have *: "min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^Suc n / fact (Suc n)) =
       \<bar>t\<bar>^n / fact (Suc n) * min (2 * \<bar>x\<bar>^n * real (Suc n)) (\<bar>t\<bar> * \<bar>x\<bar>^(Suc n))" for x