equal
deleted
inserted
replaced
73 qed (insert f, simp) |
73 qed (insert f, simp) |
74 |
74 |
75 lemma (in real_distribution) cmod_char_le_1: "norm (char M t) \<le> 1" |
75 lemma (in real_distribution) cmod_char_le_1: "norm (char M t) \<le> 1" |
76 proof - |
76 proof - |
77 have "norm (char M t) \<le> (\<integral>x. norm (iexp (t * x)) \<partial>M)" |
77 have "norm (char M t) \<le> (\<integral>x. norm (iexp (t * x)) \<partial>M)" |
78 unfolding char_def by (intro integral_norm_bound integrable_iexp) auto |
78 unfolding char_def by (intro integral_norm_bound) |
79 also have "\<dots> \<le> 1" |
79 also have "\<dots> \<le> 1" |
80 by (simp del: of_real_mult) |
80 by (simp del: of_real_mult) |
81 finally show ?thesis . |
81 finally show ?thesis . |
82 qed |
82 qed |
83 |
83 |
316 then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))" |
316 then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))" |
317 by (simp add: integ_c) |
317 by (simp add: integ_c) |
318 also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))" |
318 also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))" |
319 unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c) |
319 unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c) |
320 also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))" |
320 also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))" |
321 by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp |
321 by (intro integral_norm_bound) |
322 also have "\<dots> \<le> expectation (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)" |
322 also have "\<dots> \<le> expectation (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)" |
323 proof (rule integral_mono) |
323 proof (rule integral_mono) |
324 show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))" |
324 show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))" |
325 by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp |
325 by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp |
326 show "integrable M (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)" |
326 show "integrable M (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)" |
360 then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))" |
360 then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))" |
361 by (simp add: integ_c) |
361 by (simp add: integ_c) |
362 also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))" |
362 also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))" |
363 unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c) |
363 unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c) |
364 also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))" |
364 also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))" |
365 by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp |
365 by (rule integral_norm_bound) |
366 also have "\<dots> \<le> expectation (\<lambda>x. min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^(Suc n) / fact (Suc n)))" |
366 also have "\<dots> \<le> expectation (\<lambda>x. min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^(Suc n) / fact (Suc n)))" |
367 (is "_ \<le> expectation ?f") |
367 (is "_ \<le> expectation ?f") |
368 proof (rule integral_mono) |
368 proof (rule integral_mono) |
369 show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))" |
369 show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))" |
370 by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp |
370 by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp |