396 apply (subst Transcendental.ln_less_cancel_iff [symmetric]) |
396 apply (subst Transcendental.ln_less_cancel_iff [symmetric]) |
397 prefer 3 apply (subst ln_realpow) |
397 prefer 3 apply (subst ln_realpow) |
398 using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta> |
398 using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta> |
399 apply (force simp add: field_simps)+ |
399 apply (force simp add: field_simps)+ |
400 done |
400 done |
401 have NN0: "\<And>e. e>0 \<Longrightarrow> (1/(k*\<delta>))^NN e < e" |
401 have NN0: "(1/(k*\<delta>)) ^ (NN e) < e" if "e>0" for e |
402 apply (subst Transcendental.ln_less_cancel_iff [symmetric]) |
402 proof - |
403 prefer 3 apply (subst ln_realpow) |
403 have "0 < ln (real k) + ln \<delta>" |
404 using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta> |
404 using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero by fastforce |
405 apply (force simp add: field_simps ln_div)+ |
405 then have "real (NN e) * ln (1 / (real k * \<delta>)) < ln e" |
406 done |
406 using k\<delta>(1) NN(2) [of e] that by (simp add: ln_div divide_simps) |
|
407 then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e" |
|
408 by (metis exp_less_mono exp_ln that) |
|
409 then show ?thesis |
|
410 by (simp add: \<delta>01(1) \<open>0 < k\<close>) |
|
411 qed |
407 { fix t and e::real |
412 { fix t and e::real |
408 assume "e>0" |
413 assume "e>0" |
409 have "t \<in> S \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> S - U \<Longrightarrow> q (NN e) t < e" |
414 have "t \<in> S \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> S - U \<Longrightarrow> q (NN e) t < e" |
410 proof - |
415 proof - |
411 assume t: "t \<in> S \<inter> V" |
416 assume t: "t \<in> S \<inter> V" |