[STATEMENT]
lemma has_contour_integral_linepath_Reals_iff:
  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
  assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
  shows   "(f has_contour_integral I) (linepath a b) \<longleftrightarrow>
             ((\<lambda>x. f (of_real x)) has_integral I) {Re a..Re b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in> \<real>
b \<in> \<real>
Re a < Re b
[PROOF STEP]
have [simp]: "of_real (Re a) = a" "of_real (Re b) = b"
[PROOF STATE]
proof (prove)
using this:
a \<in> \<real>
b \<in> \<real>
Re a < Re b

goal (1 subgoal):
 1. complex_of_real (Re a) = a &&& complex_of_real (Re b) = b
[PROOF STEP]
by (simp_all add: complex_eq_iff)
[PROOF STATE]
proof (state)
this:
complex_of_real (Re a) = a
complex_of_real (Re b) = b

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in> \<real>
b \<in> \<real>
Re a < Re b
[PROOF STEP]
have "a \<noteq> b"
[PROOF STATE]
proof (prove)
using this:
a \<in> \<real>
b \<in> \<real>
Re a < Re b

goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
have "((\<lambda>x. f (of_real x)) has_integral I) (cbox (Re a) (Re b)) \<longleftrightarrow>
          ((\<lambda>x. f (a + b * of_real x - a * of_real x)) has_integral I /\<^sub>R (Re b - Re a)) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (complex_of_real x)) has_integral I) (cbox (Re a) (Re b)) = ((\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x)) has_integral I /\<^sub>R (Re b - Re a)) {0..1}
[PROOF STEP]
by (subst has_integral_affinity_iff [of "Re b - Re a" _ "Re a", symmetric])
       (insert assms, simp_all add: field_simps scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (complex_of_real x)) has_integral I) (cbox (Re a) (Re b)) = ((\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x)) has_integral I /\<^sub>R (Re b - Re a)) {0..1}

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (complex_of_real x)) has_integral I) (cbox (Re a) (Re b)) = ((\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x)) has_integral I /\<^sub>R (Re b - Re a)) {0..1}

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
have "(\<lambda>x. f (a + b * of_real x - a * of_real x)) =
               (\<lambda>x. (f (a + b * of_real x - a * of_real x) * (b - a)) /\<^sub>R (Re b - Re a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x)) = (\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x) * (b - a) /\<^sub>R (Re b - Re a))
[PROOF STEP]
using \<open>a \<noteq> b\<close>
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b

goal (1 subgoal):
 1. (\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x)) = (\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x) * (b - a) /\<^sub>R (Re b - Re a))
[PROOF STEP]
by (auto simp: field_simps fun_eq_iff scaleR_conv_of_real)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x)) = (\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x) * (b - a) /\<^sub>R (Re b - Re a))

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x)) = (\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x) * (b - a) /\<^sub>R (Re b - Re a))

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
have "(\<dots> has_integral I /\<^sub>R (Re b - Re a)) {0..1} \<longleftrightarrow>
               ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x) * (b - a) /\<^sub>R (Re b - Re a)) has_integral I /\<^sub>R (Re b - Re a)) {0..1} = ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> \<real>
b \<in> \<real>
Re a < Re b

goal (1 subgoal):
 1. ((\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x) * (b - a) /\<^sub>R (Re b - Re a)) has_integral I /\<^sub>R (Re b - Re a)) {0..1} = ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}
[PROOF STEP]
by (subst has_integral_cmul_iff) (auto simp: linepath_def scaleR_conv_of_real algebra_simps)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x) * (b - a) /\<^sub>R (Re b - Re a)) has_integral I /\<^sub>R (Re b - Re a)) {0..1} = ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (a + b * complex_of_real x - a * complex_of_real x) * (b - a) /\<^sub>R (Re b - Re a)) has_integral I /\<^sub>R (Re b - Re a)) {0..1} = ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1}

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (f has_contour_integral I) (linepath a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1} = (f has_contour_integral I) (linepath a b)
[PROOF STEP]
unfolding has_contour_integral_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1} = ((\<lambda>x. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})) has_integral I) {0..1}
[PROOF STEP]
by (intro has_integral_cong) (simp add: vector_derivative_linepath_within)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (linepath a b x) * (b - a)) has_integral I) {0..1} = (f has_contour_integral I) (linepath a b)

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. f (complex_of_real x)) has_integral I) (cbox (Re a) (Re b)) = (f has_contour_integral I) (linepath a b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. f (complex_of_real x)) has_integral I) (cbox (Re a) (Re b)) = (f has_contour_integral I) (linepath a b)

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral I) {Re a..Re b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma contour_integrable_linepath_Reals_iff:
  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
  assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
  shows   "(f contour_integrable_on linepath a b) \<longleftrightarrow>
             (\<lambda>x. f (of_real x)) integrable_on {Re a..Re b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f contour_integrable_on linepath a b) = ((\<lambda>x. f (complex_of_real x)) integrable_on {Re a..Re b})
[PROOF STEP]
using has_contour_integral_linepath_Reals_iff[OF assms, of f]
[PROOF STATE]
proof (prove)
using this:
(f has_contour_integral ?I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral ?I) {Re a..Re b}

goal (1 subgoal):
 1. (f contour_integrable_on linepath a b) = ((\<lambda>x. f (complex_of_real x)) integrable_on {Re a..Re b})
[PROOF STEP]
by (auto simp: contour_integrable_on_def integrable_on_def)


[STATEMENT]
lemma contour_integral_linepath_Reals_eq:
  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
  assumes "a \<in> Reals" "b \<in> Reals" "Re a < Re b"
  shows   "contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (of_real x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
proof (cases "f contour_integrable_on linepath a b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
 2. \<not> f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f contour_integrable_on linepath a b

goal (2 subgoals):
 1. f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
 2. \<not> f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on linepath a b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
using has_contour_integral_linepath_Reals_iff[OF assms, of f]
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on linepath a b
(f has_contour_integral ?I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral ?I) {Re a..Re b}

goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
using has_contour_integral_integral has_contour_integral_unique
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on linepath a b
(f has_contour_integral ?I) (linepath a b) = ((\<lambda>x. f (complex_of_real x)) has_integral ?I) {Re a..Re b}
?f contour_integrable_on ?i \<Longrightarrow> (?f has_contour_integral contour_integral ?i ?f) ?i
\<lbrakk>(?f has_contour_integral ?i) ?g; (?f has_contour_integral ?j) ?g\<rbrakk> \<Longrightarrow> ?i = ?j

goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))

goal (1 subgoal):
 1. \<not> f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> f contour_integrable_on linepath a b

goal (1 subgoal):
 1. \<not> f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> f contour_integrable_on linepath a b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
using contour_integrable_linepath_Reals_iff[OF assms, of f]
[PROOF STATE]
proof (prove)
using this:
\<not> f contour_integrable_on linepath a b
(f contour_integrable_on linepath a b) = ((\<lambda>x. f (complex_of_real x)) integrable_on {Re a..Re b})

goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))
[PROOF STEP]
by (simp add: not_integrable_contour_integral not_integrable_integral)
[PROOF STATE]
proof (state)
this:
contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_contour_integral_linepath_same_Im_iff:
  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
  assumes "Im a = Im b" "Re a < Re b"
  shows   "(f has_contour_integral I) (linepath a b) \<longleftrightarrow>
             ((\<lambda>x. f (of_real x + Im a * \<i>)) has_integral I) {Re a..Re b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}
[PROOF STEP]
have deriv: "vector_derivative ((\<lambda>x. x - Im a * \<i>) \<circ> linepath a b) (at y) = b - a" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_derivative ((\<lambda>x. x - complex_of_real (Im a) * \<i>) \<circ> linepath a b) (at y) = b - a
[PROOF STEP]
using linepath_translate_right[of a "-Im a * \<i>" b, symmetric]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. x + complex_of_real (- Im a) * \<i>) \<circ> linepath a b = linepath (a + complex_of_real (- Im a) * \<i>) (b + complex_of_real (- Im a) * \<i>)

goal (1 subgoal):
 1. vector_derivative ((\<lambda>x. x - complex_of_real (Im a) * \<i>) \<circ> linepath a b) (at y) = b - a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vector_derivative ((\<lambda>x. x - complex_of_real (Im a) * \<i>) \<circ> linepath a b) (at ?y) = b - a

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}
[PROOF STEP]
have "(f has_contour_integral I) (linepath a b) \<longleftrightarrow>
          ((\<lambda>x. f (x + Im a * \<i>)) has_contour_integral I) (linepath (a - Im a * \<i>) (b - Im a * \<i>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (x + complex_of_real (Im a) * \<i>)) has_contour_integral I) (linepath (a - complex_of_real (Im a) * \<i>) (b - complex_of_real (Im a) * \<i>))
[PROOF STEP]
using linepath_translate_right[of a "-Im a * \<i>" b] deriv
[PROOF STATE]
proof (prove)
using this:
linepath (a + complex_of_real (- Im a) * \<i>) (b + complex_of_real (- Im a) * \<i>) = (\<lambda>x. x + complex_of_real (- Im a) * \<i>) \<circ> linepath a b
vector_derivative ((\<lambda>x. x - complex_of_real (Im a) * \<i>) \<circ> linepath a b) (at ?y) = b - a

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (x + complex_of_real (Im a) * \<i>)) has_contour_integral I) (linepath (a - complex_of_real (Im a) * \<i>) (b - complex_of_real (Im a) * \<i>))
[PROOF STEP]
by (simp add: has_contour_integral)
[PROOF STATE]
proof (state)
this:
(f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (x + complex_of_real (Im a) * \<i>)) has_contour_integral I) (linepath (a - complex_of_real (Im a) * \<i>) (b - complex_of_real (Im a) * \<i>))

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (x + complex_of_real (Im a) * \<i>)) has_contour_integral I) (linepath (a - complex_of_real (Im a) * \<i>) (b - complex_of_real (Im a) * \<i>))

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ((\<lambda>x. f (x + Im a * \<i>)) has_integral I) {Re a..Re b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. f (x + complex_of_real (Im a) * \<i>)) has_contour_integral I) (linepath (a - complex_of_real (Im a) * \<i>) (b - complex_of_real (Im a) * \<i>)) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Im a = Im b
Re a < Re b

goal (1 subgoal):
 1. ((\<lambda>x. f (x + complex_of_real (Im a) * \<i>)) has_contour_integral I) (linepath (a - complex_of_real (Im a) * \<i>) (b - complex_of_real (Im a) * \<i>)) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}
[PROOF STEP]
by (subst has_contour_integral_linepath_Reals_iff) (auto simp: complex_is_Real_iff)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. f (x + complex_of_real (Im a) * \<i>)) has_contour_integral I) (linepath (a - complex_of_real (Im a) * \<i>) (b - complex_of_real (Im a) * \<i>)) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}

goal (1 subgoal):
 1. (f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(f has_contour_integral I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral I) {Re a..Re b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma contour_integrable_linepath_same_Im_iff:
  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
  assumes "Im a = Im b" "Re a < Re b"
  shows   "(f contour_integrable_on linepath a b) \<longleftrightarrow>
             (\<lambda>x. f (of_real x + Im a * \<i>)) integrable_on {Re a..Re b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f contour_integrable_on linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) integrable_on {Re a..Re b})
[PROOF STEP]
using has_contour_integral_linepath_same_Im_iff[OF assms, of f]
[PROOF STATE]
proof (prove)
using this:
(f has_contour_integral ?I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral ?I) {Re a..Re b}

goal (1 subgoal):
 1. (f contour_integrable_on linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) integrable_on {Re a..Re b})
[PROOF STEP]
by (auto simp: contour_integrable_on_def integrable_on_def)


[STATEMENT]
lemma contour_integral_linepath_same_Im:
  fixes a b :: complex and f :: "complex \<Rightarrow> complex"
  assumes "Im a = Im b" "Re a < Re b"
  shows   "contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (x + Im a * \<i>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
proof (cases "f contour_integrable_on linepath a b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
 2. \<not> f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f contour_integrable_on linepath a b

goal (2 subgoals):
 1. f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
 2. \<not> f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on linepath a b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
using has_contour_integral_linepath_same_Im_iff[OF assms, of f]
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on linepath a b
(f has_contour_integral ?I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral ?I) {Re a..Re b}

goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
using has_contour_integral_integral has_contour_integral_unique
[PROOF STATE]
proof (prove)
using this:
f contour_integrable_on linepath a b
(f has_contour_integral ?I) (linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) has_integral ?I) {Re a..Re b}
?f contour_integrable_on ?i \<Longrightarrow> (?f has_contour_integral contour_integral ?i ?f) ?i
\<lbrakk>(?f has_contour_integral ?i) ?g; (?f has_contour_integral ?j) ?g\<rbrakk> \<Longrightarrow> ?i = ?j

goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))

goal (1 subgoal):
 1. \<not> f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> f contour_integrable_on linepath a b

goal (1 subgoal):
 1. \<not> f contour_integrable_on linepath a b \<Longrightarrow> contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> f contour_integrable_on linepath a b

goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
using contour_integrable_linepath_same_Im_iff[OF assms, of f]
[PROOF STATE]
proof (prove)
using this:
\<not> f contour_integrable_on linepath a b
(f contour_integrable_on linepath a b) = ((\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>)) integrable_on {Re a..Re b})

goal (1 subgoal):
 1. contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))
[PROOF STEP]
by (simp add: not_integrable_contour_integral not_integrable_integral)
[PROOF STATE]
proof (state)
this:
contour_integral (linepath a b) f = integral {Re a..Re b} (\<lambda>x. f (complex_of_real x + complex_of_real (Im a) * \<i>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma continuous_on_compact_bound:
  assumes "compact A" "continuous_on A f"
  obtains B where "B \<ge> 0" "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. \<lbrakk>0 \<le> B; \<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>B. \<lbrakk>0 \<le> B; \<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms(2,1)
[PROOF STATE]
proof (chain)
picking this:
continuous_on A f
compact A
[PROOF STEP]
have "compact (f ` A)"
[PROOF STATE]
proof (prove)
using this:
continuous_on A f
compact A

goal (1 subgoal):
 1. compact (f ` A)
[PROOF STEP]
by (rule compact_continuous_image)
[PROOF STATE]
proof (state)
this:
compact (f ` A)

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>0 \<le> B; \<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
compact (f ` A)
[PROOF STEP]
obtain B where "\<forall>x\<in>A. norm (f x) \<le> B"
[PROOF STATE]
proof (prove)
using this:
compact (f ` A)

goal (1 subgoal):
 1. (\<And>B. \<forall>x\<in>A. norm (f x) \<le> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest!: compact_imp_bounded simp: bounded_iff)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>A. norm (f x) \<le> B

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>0 \<le> B; \<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "max B 0 \<ge> 0" and "\<forall>x\<in>A. norm (f x) \<le> max B 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. norm (f x) \<le> B

goal (1 subgoal):
 1. 0 \<le> max B 0 &&& \<forall>x\<in>A. norm (f x) \<le> max B 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> max B 0
\<forall>x\<in>A. norm (f x) \<le> max B 0

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>0 \<le> B; \<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> max B 0
\<forall>x\<in>A. norm (f x) \<le> max B 0

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 \<le> max B 0
\<forall>x\<in>A. norm (f x) \<le> max B 0
\<lbrakk>0 \<le> ?B; \<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> ?B\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma open_contains_cbox:
  fixes x :: "'a :: euclidean_space"
  assumes "open A" "x \<in> A"
  obtains a b where "cbox a b \<subseteq> A" "x \<in> box a b" "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>cbox a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>cbox a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
open A
x \<in> A
[PROOF STEP]
obtain R where R: "R > 0" "ball x R \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
open A
x \<in> A

goal (1 subgoal):
 1. (\<And>R. \<lbrakk>0 < R; ball x R \<subseteq> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: open_contains_ball)
[PROOF STATE]
proof (state)
this:
0 < R
ball x R \<subseteq> A

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>cbox a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define r :: real where "r = R / (2 * sqrt DIM('a))"
[PROOF STATE]
proof (state)
this:
r = R / (2 * sqrt (real DIM('a)))

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>cbox a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>R > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < R
[PROOF STEP]
have [simp]: "r > 0"
[PROOF STATE]
proof (prove)
using this:
0 < R

goal (1 subgoal):
 1. 0 < r
[PROOF STEP]
by (auto simp: r_def)
[PROOF STATE]
proof (state)
this:
0 < r

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>cbox a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define d :: 'a where "d = r *\<^sub>R Topology_Euclidean_Space.One"
[PROOF STATE]
proof (state)
this:
d = r *\<^sub>R One

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>cbox a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "cbox (x - d) (x + d) \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cbox (x - d) (x + d) \<subseteq> A
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
assume y: "y \<in> cbox (x - d) (x + d)"
[PROOF STATE]
proof (state)
this:
y \<in> cbox (x - d) (x + d)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)
[PROOF STEP]
by (subst euclidean_dist_l2) (auto simp: L2_set_def)
[PROOF STATE]
proof (state)
this:
dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y \<in> cbox (x - d) (x + d)
[PROOF STEP]
have "sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2) \<le> sqrt (\<Sum>i\<in>(Basis::'a set). r\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
y \<in> cbox (x - d) (x + d)

goal (1 subgoal):
 1. sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2) \<le> sqrt (\<Sum>i\<in>Basis. r\<^sup>2)
[PROOF STEP]
by (intro real_sqrt_le_mono sum_mono power_mono)
         (auto simp: dist_norm d_def cbox_def algebra_simps)
[PROOF STATE]
proof (state)
this:
sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2) \<le> sqrt (\<Sum>i\<in>Basis. r\<^sup>2)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2) \<le> sqrt (\<Sum>i\<in>Basis. r\<^sup>2)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
have "\<dots> = sqrt (DIM('a) * r\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (\<Sum>i\<in>Basis. r\<^sup>2) = sqrt (real DIM('a) * r\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqrt (\<Sum>i\<in>Basis. r\<^sup>2) = sqrt (real DIM('a) * r\<^sup>2)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sqrt (\<Sum>i\<in>Basis. r\<^sup>2) = sqrt (real DIM('a) * r\<^sup>2)

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
have "DIM('a) * r\<^sup>2 = (R / 2) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real DIM('a) * r\<^sup>2 = (R / 2)\<^sup>2
[PROOF STEP]
by (simp add: r_def power_divide)
[PROOF STATE]
proof (state)
this:
real DIM('a) * r\<^sup>2 = (R / 2)\<^sup>2

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real DIM('a) * r\<^sup>2 = (R / 2)\<^sup>2

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
have "sqrt \<dots> = R / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt ((R / 2)\<^sup>2) = R / 2
[PROOF STEP]
using \<open>R > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < R

goal (1 subgoal):
 1. sqrt ((R / 2)\<^sup>2) = R / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqrt ((R / 2)\<^sup>2) = R / 2

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sqrt ((R / 2)\<^sup>2) = R / 2

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
from \<open>R > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < R
[PROOF STEP]
have "\<dots> < R"
[PROOF STATE]
proof (prove)
using this:
0 < R

goal (1 subgoal):
 1. R / 2 < R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
R / 2 < R

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x y < R
[PROOF STEP]
have "y \<in> ball x R"
[PROOF STATE]
proof (prove)
using this:
dist x y < R

goal (1 subgoal):
 1. y \<in> ball x R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<in> ball x R

goal (1 subgoal):
 1. \<And>xa. xa \<in> cbox (x - d) (x + d) \<Longrightarrow> xa \<in> A
[PROOF STEP]
with R
[PROOF STATE]
proof (chain)
picking this:
0 < R
ball x R \<subseteq> A
y \<in> ball x R
[PROOF STEP]
show "y \<in> A"
[PROOF STATE]
proof (prove)
using this:
0 < R
ball x R \<subseteq> A
y \<in> ball x R

goal (1 subgoal):
 1. y \<in> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cbox (x - d) (x + d) \<subseteq> A

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>cbox a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cbox (x - d) (x + d) \<subseteq> A

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of "x - d" "x + d"]
[PROOF STATE]
proof (prove)
using this:
cbox (x - d) (x + d) \<subseteq> A
\<lbrakk>cbox (x - d) (x + d) \<subseteq> A; x \<in> box (x - d) (x + d); \<forall>i\<in>Basis. (x - d) \<bullet> i < (x + d) \<bullet> i\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto simp: algebra_simps d_def box_def)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma open_contains_box:
  fixes x :: "'a :: euclidean_space"
  assumes "open A" "x \<in> A"
  obtains a b where "box a b \<subseteq> A" "x \<in> box a b" "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>box a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>box a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
open A
x \<in> A
[PROOF STEP]
obtain a b where "cbox a b \<subseteq> A" "x \<in> box a b" "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
[PROOF STATE]
proof (prove)
using this:
open A
x \<in> A

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>cbox a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule open_contains_cbox)
[PROOF STATE]
proof (state)
this:
cbox a b \<subseteq> A
x \<in> box a b
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>box a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that[of a b] box_subset_cbox[of a b]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>box a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis
box a b \<subseteq> cbox a b
cbox a b \<subseteq> A
x \<in> box a b
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>box a b \<subseteq> A; x \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis
box a b \<subseteq> cbox a b
cbox a b \<subseteq> A
x \<in> box a b
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma analytic_onE_box:
  assumes "f analytic_on A" "s \<in> A"
  obtains a b where "Re a < Re b" "Im a < Im b" "s \<in> box a b" "f analytic_on box a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>Re a < Re b; Im a < Im b; s \<in> box a b; f analytic_on box a b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>Re a < Re b; Im a < Im b; s \<in> box a b; f analytic_on box a b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
f analytic_on A
s \<in> A
[PROOF STEP]
obtain r where r: "r > 0" "f holomorphic_on ball s r"
[PROOF STATE]
proof (prove)
using this:
f analytic_on A
s \<in> A

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>0 < r; f holomorphic_on ball s r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: analytic_on_def)
[PROOF STATE]
proof (state)
this:
0 < r
f holomorphic_on ball s r

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>Re a < Re b; Im a < Im b; s \<in> box a b; f analytic_on box a b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with open_contains_box[of "ball s r" s]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>open (ball s r); s \<in> ball s r; \<And>a b. \<lbrakk>box a b \<subseteq> ball s r; s \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
0 < r
f holomorphic_on ball s r
[PROOF STEP]
obtain a b
    where "box a b \<subseteq> ball s r" "s \<in> box a b" "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>open (ball s r); s \<in> ball s r; \<And>a b. \<lbrakk>box a b \<subseteq> ball s r; s \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
0 < r
f holomorphic_on ball s r

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>box a b \<subseteq> ball s r; s \<in> box a b; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
box a b \<subseteq> ball s r
s \<in> box a b
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>Re a < Re b; Im a < Im b; s \<in> box a b; f analytic_on box a b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
box a b \<subseteq> ball s r
s \<in> box a b
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>Re a < Re b; Im a < Im b; s \<in> box a b; f analytic_on box a b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from r
[PROOF STATE]
proof (chain)
picking this:
0 < r
f holomorphic_on ball s r
[PROOF STEP]
have "f analytic_on ball s r"
[PROOF STATE]
proof (prove)
using this:
0 < r
f holomorphic_on ball s r

goal (1 subgoal):
 1. f analytic_on ball s r
[PROOF STEP]
by (simp add: analytic_on_open)
[PROOF STATE]
proof (state)
this:
f analytic_on ball s r

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>Re a < Re b; Im a < Im b; s \<in> box a b; f analytic_on box a b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
box a b \<subseteq> ball s r
s \<in> box a b
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i
f analytic_on ball s r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
box a b \<subseteq> ball s r
s \<in> box a b
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i
f analytic_on ball s r

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of a b] analytic_on_subset[of _ "ball s r" "box a b"]
[PROOF STATE]
proof (prove)
using this:
box a b \<subseteq> ball s r
s \<in> box a b
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i
f analytic_on ball s r
\<lbrakk>Re a < Re b; Im a < Im b; s \<in> box a b; f analytic_on box a b\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?f analytic_on ball s r; box a b \<subseteq> ball s r\<rbrakk> \<Longrightarrow> ?f analytic_on box a b

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto simp: Basis_complex_def)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inner_image_box:
  assumes "(i :: 'a :: euclidean_space) \<in> Basis"
  assumes "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
  shows   "(\<lambda>x. x \<bullet> i) ` box a b = {a \<bullet> i<..<b \<bullet> i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x \<bullet> i) ` box a b = {a \<bullet> i<..<b \<bullet> i}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
assume x: "x \<in> {a \<bullet> i<..<b \<bullet> i}"
[PROOF STATE]
proof (state)
this:
x \<in> {a \<bullet> i<..<b \<bullet> i}

goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
let ?y = "(\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) *\<^sub>R j)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
from x assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> {a \<bullet> i<..<b \<bullet> i}
i \<in> Basis
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i
[PROOF STEP]
have "?y \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` box a b"
[PROOF STATE]
proof (prove)
using this:
x \<in> {a \<bullet> i<..<b \<bullet> i}
i \<in> Basis
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i

goal (1 subgoal):
 1. (\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) *\<^sub>R j) \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
by (intro imageI) (auto simp: box_def algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) *\<^sub>R j) \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` box a b

goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) *\<^sub>R j) \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` box a b

goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
have "?y \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) * (j \<bullet> i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) *\<^sub>R j) \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) * (j \<bullet> i))
[PROOF STEP]
by (simp add: inner_sum_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) *\<^sub>R j) \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) * (j \<bullet> i))

goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) *\<^sub>R j) \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) * (j \<bullet> i))

goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
have "\<dots> = (\<Sum>j\<in>Basis. if i = j then x else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) * (j \<bullet> i)) = (\<Sum>j\<in>Basis. if i = j then x else 0)
[PROOF STEP]
by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) * (j \<bullet> i)) = (\<Sum>j\<in>Basis. if i = j then x else 0)

goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else (a + b) \<bullet> j / 2) * (j \<bullet> i)) = (\<Sum>j\<in>Basis. if i = j then x else 0)

goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
have "\<dots> = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>Basis. if i = j then x else 0) = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> Basis
\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i

goal (1 subgoal):
 1. (\<Sum>j\<in>Basis. if i = j then x else 0) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. if i = j then x else 0) = x

goal (2 subgoals):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i<..<b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
show "x \<in> (\<lambda>x. x \<bullet> i) ` box a b"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>x. x \<bullet> i) ` box a b

goal (1 subgoal):
 1. x \<in> (\<lambda>x. x \<bullet> i) ` box a b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>x. x \<bullet> i) ` box a b

goal (1 subgoal):
 1. \<And>x xa. xa \<in> box a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i<..<b \<bullet> i}
[PROOF STEP]
qed (insert assms, auto simp: box_def)


[STATEMENT]
lemma Re_image_box:
  assumes "Re a < Re b" "Im a < Im b"
  shows   "Re ` box a b = {Re a<..<Re b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re ` box a b = {Re a<..<Re b}
[PROOF STEP]
using inner_image_box[of "1::complex" a b] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 \<in> Basis; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> (\<lambda>x. x \<bullet> 1) ` box a b = {a \<bullet> 1<..<b \<bullet> 1}
Re a < Re b
Im a < Im b

goal (1 subgoal):
 1. Re ` box a b = {Re a<..<Re b}
[PROOF STEP]
by (auto simp: Basis_complex_def)


[STATEMENT]
lemma Im_image_box:
  assumes "Re a < Re b" "Im a < Im b"
  shows   "Im ` box a b = {Im a<..<Im b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im ` box a b = {Im a<..<Im b}
[PROOF STEP]
using inner_image_box[of "\<i>::complex" a b] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<i> \<in> Basis; \<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i\<rbrakk> \<Longrightarrow> (\<lambda>x. x \<bullet> \<i>) ` box a b = {a \<bullet> \<i><..<b \<bullet> \<i>}
Re a < Re b
Im a < Im b

goal (1 subgoal):
 1. Im ` box a b = {Im a<..<Im b}
[PROOF STEP]
by (auto simp: Basis_complex_def)


[STATEMENT]
lemma inner_image_cbox:
  assumes "(i :: 'a :: euclidean_space) \<in> Basis"
  assumes "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
  shows   "(\<lambda>x. x \<bullet> i) ` cbox a b = {a \<bullet> i..b \<bullet> i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x \<bullet> i) ` cbox a b = {a \<bullet> i..b \<bullet> i}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
assume x: "x \<in> {a \<bullet> i..b \<bullet> i}"
[PROOF STATE]
proof (state)
this:
x \<in> {a \<bullet> i..b \<bullet> i}

goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
let ?y = "(\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) *\<^sub>R j)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
from x assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> {a \<bullet> i..b \<bullet> i}
i \<in> Basis
\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i
[PROOF STEP]
have "?y \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` cbox a b"
[PROOF STATE]
proof (prove)
using this:
x \<in> {a \<bullet> i..b \<bullet> i}
i \<in> Basis
\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i

goal (1 subgoal):
 1. (\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) *\<^sub>R j) \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
by (intro imageI) (auto simp: cbox_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) *\<^sub>R j) \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` cbox a b

goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) *\<^sub>R j) \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` cbox a b

goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
have "?y \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) * (j \<bullet> i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) *\<^sub>R j) \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) * (j \<bullet> i))
[PROOF STEP]
by (simp add: inner_sum_left)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) *\<^sub>R j) \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) * (j \<bullet> i))

goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) *\<^sub>R j) \<bullet> i = (\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) * (j \<bullet> i))

goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
have "\<dots> = (\<Sum>j\<in>Basis. if i = j then x else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) * (j \<bullet> i)) = (\<Sum>j\<in>Basis. if i = j then x else 0)
[PROOF STEP]
by (intro sum.cong) (auto simp: inner_not_same_Basis assms)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) * (j \<bullet> i)) = (\<Sum>j\<in>Basis. if i = j then x else 0)

goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. (if i = j then x else a \<bullet> j) * (j \<bullet> i)) = (\<Sum>j\<in>Basis. if i = j then x else 0)

goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
have "\<dots> = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>Basis. if i = j then x else 0) = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> Basis
\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i

goal (1 subgoal):
 1. (\<Sum>j\<in>Basis. if i = j then x else 0) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>Basis. if i = j then x else 0) = x

goal (2 subgoals):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
 2. \<And>x. x \<in> {a \<bullet> i..b \<bullet> i} \<Longrightarrow> x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
show "x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b"
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b

goal (1 subgoal):
 1. x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<in> (\<lambda>x. x \<bullet> i) ` cbox a b

goal (1 subgoal):
 1. \<And>x xa. xa \<in> cbox a b \<Longrightarrow> xa \<bullet> i \<in> {a \<bullet> i..b \<bullet> i}
[PROOF STEP]
qed (insert assms, auto simp: cbox_def)


[STATEMENT]
lemma Re_image_cbox:
  assumes "Re a \<le> Re b" "Im a \<le> Im b"
  shows   "Re ` cbox a b = {Re a..Re b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re ` cbox a b = {Re a..Re b}
[PROOF STEP]
using inner_image_cbox[of "1::complex" a b] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 \<in> Basis; \<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i\<rbrakk> \<Longrightarrow> (\<lambda>x. x \<bullet> 1) ` cbox a b = {a \<bullet> 1..b \<bullet> 1}
Re a \<le> Re b
Im a \<le> Im b

goal (1 subgoal):
 1. Re ` cbox a b = {Re a..Re b}
[PROOF STEP]
by (auto simp: Basis_complex_def)


[STATEMENT]
lemma Im_image_cbox:
  assumes "Re a \<le> Re b" "Im a \<le> Im b"
  shows   "Im ` cbox a b = {Im a..Im b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im ` cbox a b = {Im a..Im b}
[PROOF STEP]
using inner_image_cbox[of "\<i>::complex" a b] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<i> \<in> Basis; \<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i\<rbrakk> \<Longrightarrow> (\<lambda>x. x \<bullet> \<i>) ` cbox a b = {a \<bullet> \<i>..b \<bullet> \<i>}
Re a \<le> Re b
Im a \<le> Im b

goal (1 subgoal):
 1. Im ` cbox a b = {Im a..Im b}
[PROOF STEP]
by (auto simp: Basis_complex_def)


[STATEMENT]
lemma analytic_onE_cball:
  assumes "f analytic_on A" "s \<in> A" "ub > (0::real)"
  obtains R where "R > 0" "R < ub" "f analytic_on cball s R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>R. \<lbrakk>0 < R; R < ub; f analytic_on cball s R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>R. \<lbrakk>0 < R; R < ub; f analytic_on cball s R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
f analytic_on A
s \<in> A
0 < ub
[PROOF STEP]
obtain r where "r > 0" "f holomorphic_on ball s r"
[PROOF STATE]
proof (prove)
using this:
f analytic_on A
s \<in> A
0 < ub

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>0 < r; f holomorphic_on ball s r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: analytic_on_def)
[PROOF STATE]
proof (state)
this:
0 < r
f holomorphic_on ball s r

goal (1 subgoal):
 1. (\<And>R. \<lbrakk>0 < R; R < ub; f analytic_on cball s R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "f analytic_on ball s r"
[PROOF STATE]
proof (prove)
using this:
0 < r
f holomorphic_on ball s r

goal (1 subgoal):
 1. f analytic_on ball s r
[PROOF STEP]
by (simp add: analytic_on_open)
[PROOF STATE]
proof (state)
this:
f analytic_on ball s r

goal (1 subgoal):
 1. (\<And>R. \<lbrakk>0 < R; R < ub; f analytic_on cball s R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "f analytic_on cball s (min (ub / 2) (r / 2))"
[PROOF STATE]
proof (prove)
using this:
f analytic_on ball s r

goal (1 subgoal):
 1. f analytic_on cball s (min (ub / 2) (r / 2))
[PROOF STEP]
by (rule analytic_on_subset, subst cball_subset_ball_iff) (use \<open>r > 0\<close> in auto)
[PROOF STATE]
proof (state)
this:
f analytic_on cball s (min (ub / 2) (r / 2))

goal (1 subgoal):
 1. (\<And>R. \<lbrakk>0 < R; R < ub; f analytic_on cball s R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f analytic_on cball s (min (ub / 2) (r / 2))

goal (1 subgoal):
 1. (\<And>R. \<lbrakk>0 < R; R < ub; f analytic_on cball s R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "min (ub / 2) (r / 2) > 0" and "min (ub / 2) (r / 2) < ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < min (ub / 2) (r / 2) &&& min (ub / 2) (r / 2) < ub
[PROOF STEP]
using \<open>r > 0\<close> and \<open>ub > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r
0 < ub

goal (1 subgoal):
 1. 0 < min (ub / 2) (r / 2) &&& min (ub / 2) (r / 2) < ub
[PROOF STEP]
by (auto simp: min_def)
[PROOF STATE]
proof (state)
this:
0 < min (ub / 2) (r / 2)
min (ub / 2) (r / 2) < ub

goal (1 subgoal):
 1. (\<And>R. \<lbrakk>0 < R; R < ub; f analytic_on cball s R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f analytic_on cball s (min (ub / 2) (r / 2))
0 < min (ub / 2) (r / 2)
min (ub / 2) (r / 2) < ub
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f analytic_on cball s (min (ub / 2) (r / 2))
0 < min (ub / 2) (r / 2)
min (ub / 2) (r / 2) < ub

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of "min (ub / 2) (r / 2)"]
[PROOF STATE]
proof (prove)
using this:
f analytic_on cball s (min (ub / 2) (r / 2))
0 < min (ub / 2) (r / 2)
min (ub / 2) (r / 2) < ub
\<lbrakk>0 < min (ub / 2) (r / 2); min (ub / 2) (r / 2) < ub; f analytic_on cball s (min (ub / 2) (r / 2))\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma logderiv_zeta_analytic: "(\<lambda>s. deriv zeta s / zeta s) analytic_on {s. Re s \<ge> 1} - {1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. deriv zeta s / zeta s) analytic_on {s. 1 \<le> Re s} - {1}
[PROOF STEP]
using zeta_Re_ge_1_nonzero
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 \<le> Re ?s; ?s \<noteq> 1\<rbrakk> \<Longrightarrow> zeta ?s \<noteq> 0

goal (1 subgoal):
 1. (\<lambda>s. deriv zeta s / zeta s) analytic_on {s. 1 \<le> Re s} - {1}
[PROOF STEP]
by (auto intro!: analytic_intros)


[STATEMENT]
lemma cis_pi_half [simp]: "cis (pi / 2) = \<i>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (pi / 2) = \<i>
[PROOF STEP]
by (simp add: complex_eq_iff)


[STATEMENT]
lemma mult_real_sqrt: "x \<ge> 0 \<Longrightarrow> x * sqrt y = sqrt (x ^ 2 * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> x \<Longrightarrow> x * sqrt y = sqrt (x\<^sup>2 * y)
[PROOF STEP]
by (simp add: real_sqrt_mult)


[STATEMENT]
lemma arcsin_pos: "x \<in> {0<..1} \<Longrightarrow> arcsin x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {0<..1} \<Longrightarrow> 0 < arcsin x
[PROOF STEP]
using arcsin_less_arcsin[of 0 x]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>- 1 \<le> 0; 0 < x; x \<le> 1\<rbrakk> \<Longrightarrow> arcsin 0 < arcsin x

goal (1 subgoal):
 1. x \<in> {0<..1} \<Longrightarrow> 0 < arcsin x
[PROOF STEP]
by simp


[STATEMENT]
lemma residue_simple':
  assumes "open s" "0 \<in> s" "f holomorphic_on s"
  shows   "residue (\<lambda>w. f w / w) 0 = f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. residue (\<lambda>w. f w / w) 0 = f 0
[PROOF STEP]
using residue_simple[of s 0 f] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>open s; 0 \<in> s; f holomorphic_on s\<rbrakk> \<Longrightarrow> residue (\<lambda>w. f w / (w - 0)) 0 = f 0
open s
0 \<in> s
f holomorphic_on s

goal (1 subgoal):
 1. residue (\<lambda>w. f w / w) 0 = f 0
[PROOF STEP]
by simp


[STATEMENT]
lemma fds_converges_cong:
  assumes "eventually (\<lambda>n. fds_nth f n = fds_nth g n) at_top" "s = s'"
  shows   "fds_converges f s \<longleftrightarrow> fds_converges g s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_converges f s = fds_converges g s'
[PROOF STEP]
unfolding fds_converges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. fds_nth f n / nat_power n s) = summable (\<lambda>n. fds_nth g n / nat_power n s')
[PROOF STEP]
by (intro summable_cong eventually_mono[OF assms(1)]) (simp_all add: assms)


[STATEMENT]
lemma fds_abs_converges_cong:
  assumes "eventually (\<lambda>n. fds_nth f n = fds_nth g n) at_top" "s = s'"
  shows   "fds_abs_converges f s \<longleftrightarrow> fds_abs_converges g s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges f s = fds_abs_converges g s'
[PROOF STEP]
unfolding fds_abs_converges_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. norm (fds_nth f n / nat_power n s)) = summable (\<lambda>n. norm (fds_nth g n / nat_power n s'))
[PROOF STEP]
by (intro summable_cong eventually_mono[OF assms(1)]) (simp_all add: assms)


[STATEMENT]
lemma conv_abscissa_cong:
  assumes "eventually (\<lambda>n. fds_nth f n = fds_nth g n) at_top"
  shows   "conv_abscissa f = conv_abscissa g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conv_abscissa f = conv_abscissa g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. conv_abscissa f = conv_abscissa g
[PROOF STEP]
have "fds_converges f = fds_converges g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_converges f = fds_converges g
[PROOF STEP]
by (intro ext fds_converges_cong assms refl)
[PROOF STATE]
proof (state)
this:
fds_converges f = fds_converges g

goal (1 subgoal):
 1. conv_abscissa f = conv_abscissa g
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fds_converges f = fds_converges g

goal (1 subgoal):
 1. conv_abscissa f = conv_abscissa g
[PROOF STEP]
by (simp add: conv_abscissa_def)
[PROOF STATE]
proof (state)
this:
conv_abscissa f = conv_abscissa g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_conv_abscissa_cong:
  assumes "eventually (\<lambda>n. fds_nth f n = fds_nth g n) at_top"
  shows   "abs_conv_abscissa f = abs_conv_abscissa g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_conv_abscissa f = abs_conv_abscissa g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. abs_conv_abscissa f = abs_conv_abscissa g
[PROOF STEP]
have "fds_abs_converges f = fds_abs_converges g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges f = fds_abs_converges g
[PROOF STEP]
by (intro ext fds_abs_converges_cong assms refl)
[PROOF STATE]
proof (state)
this:
fds_abs_converges f = fds_abs_converges g

goal (1 subgoal):
 1. abs_conv_abscissa f = abs_conv_abscissa g
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fds_abs_converges f = fds_abs_converges g

goal (1 subgoal):
 1. abs_conv_abscissa f = abs_conv_abscissa g
[PROOF STEP]
by (simp add: abs_conv_abscissa_def)
[PROOF STATE]
proof (state)
this:
abs_conv_abscissa f = abs_conv_abscissa g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fds_nth_remainder: "fds_nth (fds_remainder m f) = (\<lambda>n. if n > m then fds_nth f n else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_nth (fds_remainder m f) = (\<lambda>n. if m < n then fds_nth f n else (0::'a))
[PROOF STEP]
by (simp add: fds_remainder_def fds_subseries_def fds_nth_fds')


[STATEMENT]
lemma fds_converges_remainder_iff [simp]:
  "fds_converges (fds_remainder m f) s \<longleftrightarrow> fds_converges f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_converges (fds_remainder m f) s = fds_converges f s
[PROOF STEP]
by (intro fds_converges_cong eventually_mono[OF eventually_gt_at_top[of m]])
     (auto simp: fds_nth_remainder)


[STATEMENT]
lemma fds_abs_converges_remainder_iff [simp]:
  "fds_abs_converges (fds_remainder m f) s \<longleftrightarrow> fds_abs_converges f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_abs_converges (fds_remainder m f) s = fds_abs_converges f s
[PROOF STEP]
by (intro fds_abs_converges_cong eventually_mono[OF eventually_gt_at_top[of m]])
     (auto simp: fds_nth_remainder)


[STATEMENT]
lemma fds_converges_remainder [intro]:
        "fds_converges f s \<Longrightarrow> fds_converges (fds_remainder m f) s"
  and fds_abs_converges_remainder [intro]:
        "fds_abs_converges f s \<Longrightarrow> fds_abs_converges (fds_remainder m f) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fds_converges f s \<Longrightarrow> fds_converges (fds_remainder m f) s) &&& (fds_abs_converges f s \<Longrightarrow> fds_abs_converges (fds_remainder m f) s)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma conv_abscissa_remainder [simp]:
  "conv_abscissa (fds_remainder m f) = conv_abscissa f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conv_abscissa (fds_remainder m f) = conv_abscissa f
[PROOF STEP]
by (intro conv_abscissa_cong eventually_mono[OF eventually_gt_at_top[of m]])
     (auto simp: fds_nth_remainder)


[STATEMENT]
lemma abs_conv_abscissa_remainder [simp]:
  "abs_conv_abscissa (fds_remainder m f) = abs_conv_abscissa f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_conv_abscissa (fds_remainder m f) = abs_conv_abscissa f
[PROOF STEP]
by (intro abs_conv_abscissa_cong eventually_mono[OF eventually_gt_at_top[of m]])
     (auto simp: fds_nth_remainder)


[STATEMENT]
lemma eval_fds_remainder:
   "eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)"
    (is "_ = suminf (\<lambda>n. ?f (n + Suc m))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
proof (cases "fds_converges f s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
 2. \<not> fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> fds_converges f s

goal (2 subgoals):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
 2. \<not> fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
hence "\<not>fds_converges (fds_remainder m f) s"
[PROOF STATE]
proof (prove)
using this:
\<not> fds_converges f s

goal (1 subgoal):
 1. \<not> fds_converges (fds_remainder m f) s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> fds_converges (fds_remainder m f) s

goal (2 subgoals):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
 2. \<not> fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
hence "(\<lambda>x. (\<lambda>n. fds_nth (fds_remainder m f) n / nat_power n s) sums x) = (\<lambda>_. False)"
[PROOF STATE]
proof (prove)
using this:
\<not> fds_converges (fds_remainder m f) s

goal (1 subgoal):
 1. (sums) (\<lambda>n. fds_nth (fds_remainder m f) n / nat_power n s) = (\<lambda>_. False)
[PROOF STEP]
by (auto simp: fds_converges_def summable_def)
[PROOF STATE]
proof (state)
this:
(sums) (\<lambda>n. fds_nth (fds_remainder m f) n / nat_power n s) = (\<lambda>_. False)

goal (2 subgoals):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
 2. \<not> fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
hence "eval_fds (fds_remainder m f) s = (THE _. False)"
[PROOF STATE]
proof (prove)
using this:
(sums) (\<lambda>n. fds_nth (fds_remainder m f) n / nat_power n s) = (\<lambda>_. False)

goal (1 subgoal):
 1. eval_fds (fds_remainder m f) s = (THE uu_. False)
[PROOF STEP]
by (simp add: eval_fds_def suminf_def)
[PROOF STATE]
proof (state)
this:
eval_fds (fds_remainder m f) s = (THE uu_. False)

goal (2 subgoals):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
 2. \<not> fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval_fds (fds_remainder m f) s = (THE uu_. False)

goal (2 subgoals):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
 2. \<not> fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> fds_converges f s
[PROOF STEP]
have "\<not>summable (\<lambda>n. ?f (n + Suc m))"
[PROOF STATE]
proof (prove)
using this:
\<not> fds_converges f s

goal (1 subgoal):
 1. \<not> summable (\<lambda>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
unfolding fds_converges_def
[PROOF STATE]
proof (prove)
using this:
\<not> summable (\<lambda>n. fds_nth f n / nat_power n s)

goal (1 subgoal):
 1. \<not> summable (\<lambda>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
by (subst summable_iff_shift) auto
[PROOF STATE]
proof (state)
this:
\<not> summable (\<lambda>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)

goal (2 subgoals):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
 2. \<not> fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
hence "(\<lambda>x. (\<lambda>n. ?f (n + Suc m)) sums x) = (\<lambda>_. False)"
[PROOF STATE]
proof (prove)
using this:
\<not> summable (\<lambda>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)

goal (1 subgoal):
 1. (sums) (\<lambda>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s) = (\<lambda>_. False)
[PROOF STEP]
by (auto simp: summable_def)
[PROOF STATE]
proof (state)
this:
(sums) (\<lambda>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s) = (\<lambda>_. False)

goal (2 subgoals):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
 2. \<not> fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
hence "suminf (\<lambda>n. ?f (n + Suc m)) = (THE _. False)"
[PROOF STATE]
proof (prove)
using this:
(sums) (\<lambda>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s) = (\<lambda>_. False)

goal (1 subgoal):
 1. (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s) = (THE uu_. False)
[PROOF STEP]
by (simp add: suminf_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s) = (THE uu_. False)

goal (2 subgoals):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
 2. \<not> fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval_fds (fds_remainder m f) s = (THE uu_. False)
(\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s) = (THE uu_. False)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval_fds (fds_remainder m f) s = (THE uu_. False)
(\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s) = (THE uu_. False)

goal (1 subgoal):
 1. eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)

goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
fds_converges f s

goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
hence *: "fds_converges (fds_remainder m f) s"
[PROOF STATE]
proof (prove)
using this:
fds_converges f s

goal (1 subgoal):
 1. fds_converges (fds_remainder m f) s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fds_converges (fds_remainder m f) s

goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
have "eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s)
[PROOF STEP]
unfolding eval_fds_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s) = (\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s)

goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s)

goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
have "\<dots> = (\<Sum>n. fds_nth (fds_remainder m f) (n + Suc m) / nat_power (n + Suc m) s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s) = (\<Sum>n. fds_nth (fds_remainder m f) (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
fds_converges (fds_remainder m f) s

goal (1 subgoal):
 1. (\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s) = (\<Sum>n. fds_nth (fds_remainder m f) (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
unfolding fds_converges_def
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. fds_nth (fds_remainder m f) n / nat_power n s)

goal (1 subgoal):
 1. (\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s) = (\<Sum>n. fds_nth (fds_remainder m f) (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
by (subst suminf_minus_initial_segment) (auto simp: fds_nth_remainder)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s) = (\<Sum>n. fds_nth (fds_remainder m f) (n + Suc m) / nat_power (n + Suc m) s)

goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. fds_nth (fds_remainder m f) n / nat_power n s) = (\<Sum>n. fds_nth (fds_remainder m f) (n + Suc m) / nat_power (n + Suc m) s)

goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
have "(\<lambda>n. fds_nth (fds_remainder m f) (n + Suc m)) = (\<lambda>n. fds_nth f (n + Suc m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. fds_nth (fds_remainder m f) (n + Suc m)) = (\<lambda>n. fds_nth f (n + Suc m))
[PROOF STEP]
by (intro ext) (auto simp: fds_nth_remainder)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. fds_nth (fds_remainder m f) (n + Suc m)) = (\<lambda>n. fds_nth f (n + Suc m))

goal (1 subgoal):
 1. fds_converges f s \<Longrightarrow> eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)

goal (1 subgoal):
 1. eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eval_fds (fds_remainder m f) s = (\<Sum>n. fds_nth f (n + Suc m) / nat_power (n + Suc m) s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fds_truncate_plus_remainder: "fds_truncate m f + fds_remainder m f = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_truncate m f + fds_remainder m f = f
[PROOF STEP]
by (intro fds_eqI) (auto simp: fds_truncate_def fds_remainder_def fds_subseries_def)


[STATEMENT]
lemma holomorphic_fds_eval' [holomorphic_intros]:
  assumes "g holomorphic_on A" "\<And>x. x \<in> A \<Longrightarrow> Re (g x) > conv_abscissa f"
  shows   "(\<lambda>x. eval_fds f (g x)) holomorphic_on A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. eval_fds f (g x)) holomorphic_on A
[PROOF STEP]
using holomorphic_on_compose_gen[OF assms(1) holomorphic_fds_eval[OF order.refl, of f]] assms(2)
[PROOF STATE]
proof (prove)
using this:
g ` A \<subseteq> {z. conv_abscissa f < ereal (Re z)} \<Longrightarrow> eval_fds f \<circ> g holomorphic_on A
?x \<in> A \<Longrightarrow> conv_abscissa f < ereal (Re (g ?x))

goal (1 subgoal):
 1. (\<lambda>x. eval_fds f (g x)) holomorphic_on A
[PROOF STEP]
by (auto simp: o_def)


[STATEMENT]
lemma analytic_fds_eval' [analytic_intros]:
  assumes "g analytic_on A" "\<And>x. x \<in> A \<Longrightarrow> Re (g x) > conv_abscissa f"
  shows   "(\<lambda>x. eval_fds f (g x)) analytic_on A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. eval_fds f (g x)) analytic_on A
[PROOF STEP]
using analytic_on_compose_gen[OF assms(1) analytic_fds_eval[OF order.refl, of f]] assms(2)
[PROOF STATE]
proof (prove)
using this:
(\<And>z. z \<in> A \<Longrightarrow> g z \<in> {z. conv_abscissa f < ereal (Re z)}) \<Longrightarrow> eval_fds f \<circ> g analytic_on A
?x \<in> A \<Longrightarrow> conv_abscissa f < ereal (Re (g ?x))

goal (1 subgoal):
 1. (\<lambda>x. eval_fds f (g x)) analytic_on A
[PROOF STEP]
by (auto simp: o_def)


[STATEMENT]
lemma homotopic_loopsI:
  fixes h :: "real \<times> real \<Rightarrow> _"
  assumes "continuous_on ({0..1} \<times> {0..1}) h"
          "h ` ({0..1} \<times> {0..1}) \<subseteq> s"
          "\<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = p x"
          "\<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = q x"
          "\<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)"
  shows   "homotopic_loops s p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homotopic_loops s p q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on ({0..1} \<times> {0..1}) h
h ` ({0..1} \<times> {0..1}) \<subseteq> s
?x \<in> {0..1} \<Longrightarrow> h (0, ?x) = p ?x
?x \<in> {0..1} \<Longrightarrow> h (1, ?x) = q ?x
?x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair ?x) = pathstart (h \<circ> Pair ?x)

goal (1 subgoal):
 1. homotopic_loops s p q
[PROOF STEP]
unfolding homotopic_loops
[PROOF STATE]
proof (prove)
using this:
continuous_on ({0..1} \<times> {0..1}) h
h ` ({0..1} \<times> {0..1}) \<subseteq> s
?x \<in> {0..1} \<Longrightarrow> h (0, ?x) = p ?x
?x \<in> {0..1} \<Longrightarrow> h (1, ?x) = q ?x
?x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair ?x) = pathstart (h \<circ> Pair ?x)

goal (1 subgoal):
 1. \<exists>h. continuous_on ({0..1} \<times> {0..1}) h \<and> h ` ({0..1} \<times> {0..1}) \<subseteq> s \<and> (\<forall>x\<in>{0..1}. h (0, x) = p x) \<and> (\<forall>x\<in>{0..1}. h (1, x) = q x) \<and> (\<forall>t\<in>{0..1}. pathfinish (h \<circ> Pair t) = pathstart (h \<circ> Pair t))
[PROOF STEP]
by (intro exI[of _ h]) auto


[STATEMENT]
lemma continuous_on_linepath [continuous_intros]:
  assumes "continuous_on A a" "continuous_on A b" "continuous_on A f"
  shows   "continuous_on A (\<lambda>x. linepath (a x) (b x) (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on A (\<lambda>x. linepath (a x) (b x) (f x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on A a
continuous_on A b
continuous_on A f

goal (1 subgoal):
 1. continuous_on A (\<lambda>x. linepath (a x) (b x) (f x))
[PROOF STEP]
by (auto simp: linepath_def intro!: continuous_intros assms)


[STATEMENT]
lemma continuous_on_part_circlepath [continuous_intros]:
  assumes "continuous_on A c" "continuous_on A r" "continuous_on A a" "continuous_on A b"
          "continuous_on A f"
  shows   "continuous_on A (\<lambda>x. part_circlepath (c x) (r x) (a x) (b x) (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on A (\<lambda>x. part_circlepath (c x) (r x) (a x) (b x) (f x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on A c
continuous_on A r
continuous_on A a
continuous_on A b
continuous_on A f

goal (1 subgoal):
 1. continuous_on A (\<lambda>x. part_circlepath (c x) (r x) (a x) (b x) (f x))
[PROOF STEP]
by (auto simp: part_circlepath_def intro!: continuous_intros assms)


[STATEMENT]
lemma homotopic_loops_part_circlepath:
  assumes "sphere c r \<subseteq> A" and "r \<ge> 0" and
          "b1 = a1 + 2 * of_int k * pi" and "b2 = a2 + 2 * of_int k * pi"
  shows   "homotopic_loops A (part_circlepath c r a1 b1) (part_circlepath c r a2 b2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homotopic_loops A (part_circlepath c r a1 b1) (part_circlepath c r a2 b2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. homotopic_loops A (part_circlepath c r a1 b1) (part_circlepath c r a2 b2)
[PROOF STEP]
define h where "h = (\<lambda>(x,y). part_circlepath c r (linepath a1 a2 x) (linepath b1 b2 x) y)"
[PROOF STATE]
proof (state)
this:
h = (\<lambda>(x, y). part_circlepath c r (linepath a1 a2 x) (linepath b1 b2 x) y)

goal (1 subgoal):
 1. homotopic_loops A (part_circlepath c r a1 b1) (part_circlepath c r a2 b2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homotopic_loops A (part_circlepath c r a1 b1) (part_circlepath c r a2 b2)
[PROOF STEP]
proof (rule homotopic_loopsI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. continuous_on ({0..1} \<times> {0..1}) ?h
 2. ?h ` ({0..1} \<times> {0..1}) \<subseteq> A
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> ?h (0, x) = part_circlepath c r a1 b1 x
 4. \<And>x. x \<in> {0..1} \<Longrightarrow> ?h (1, x) = part_circlepath c r a2 b2 x
 5. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (?h \<circ> Pair x) = pathstart (?h \<circ> Pair x)
[PROOF STEP]
show "continuous_on ({0..1} \<times> {0..1}) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on ({0..1} \<times> {0..1}) h
[PROOF STEP]
by (auto simp: h_def case_prod_unfold intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
continuous_on ({0..1} \<times> {0..1}) h

goal (4 subgoals):
 1. h ` ({0..1} \<times> {0..1}) \<subseteq> A
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = part_circlepath c r a1 b1 x
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = part_circlepath c r a2 b2 x
 4. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. h ` ({0..1} \<times> {0..1}) \<subseteq> A
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = part_circlepath c r a1 b1 x
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = part_circlepath c r a2 b2 x
 4. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
sphere c r \<subseteq> A
0 \<le> r
b1 = a1 + 2 * real_of_int k * pi
b2 = a2 + 2 * real_of_int k * pi
[PROOF STEP]
have "h ` ({0..1} \<times> {0..1}) \<subseteq> sphere c r"
[PROOF STATE]
proof (prove)
using this:
sphere c r \<subseteq> A
0 \<le> r
b1 = a1 + 2 * real_of_int k * pi
b2 = a2 + 2 * real_of_int k * pi

goal (1 subgoal):
 1. h ` ({0..1} \<times> {0..1}) \<subseteq> sphere c r
[PROOF STEP]
by (auto simp: h_def part_circlepath_def dist_norm norm_mult)
[PROOF STATE]
proof (state)
this:
h ` ({0..1} \<times> {0..1}) \<subseteq> sphere c r

goal (4 subgoals):
 1. h ` ({0..1} \<times> {0..1}) \<subseteq> A
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = part_circlepath c r a1 b1 x
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = part_circlepath c r a2 b2 x
 4. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
h ` ({0..1} \<times> {0..1}) \<subseteq> sphere c r

goal (4 subgoals):
 1. h ` ({0..1} \<times> {0..1}) \<subseteq> A
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = part_circlepath c r a1 b1 x
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = part_circlepath c r a2 b2 x
 4. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
have "\<dots> \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sphere c r \<subseteq> A
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
sphere c r \<subseteq> A

goal (4 subgoals):
 1. h ` ({0..1} \<times> {0..1}) \<subseteq> A
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = part_circlepath c r a1 b1 x
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = part_circlepath c r a2 b2 x
 4. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
h ` ({0..1} \<times> {0..1}) \<subseteq> A
[PROOF STEP]
show "h ` ({0..1} \<times> {0..1}) \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
h ` ({0..1} \<times> {0..1}) \<subseteq> A

goal (1 subgoal):
 1. h ` ({0..1} \<times> {0..1}) \<subseteq> A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
h ` ({0..1} \<times> {0..1}) \<subseteq> A

goal (3 subgoals):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = part_circlepath c r a1 b1 x
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = part_circlepath c r a2 b2 x
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = part_circlepath c r a1 b1 x
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = part_circlepath c r a2 b2 x
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
fix x :: real
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = part_circlepath c r a1 b1 x
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = part_circlepath c r a2 b2 x
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
assume x: "x \<in> {0..1}"
[PROOF STATE]
proof (state)
this:
x \<in> {0..1}

goal (3 subgoals):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = part_circlepath c r a1 b1 x
 2. \<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = part_circlepath c r a2 b2 x
 3. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
show "h (0, x) = part_circlepath c r a1 b1 x" and "h (1, x) = part_circlepath c r a2 b2 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h (0, x) = part_circlepath c r a1 b1 x &&& h (1, x) = part_circlepath c r a2 b2 x
[PROOF STEP]
by (simp_all add: h_def linepath_def)
[PROOF STATE]
proof (state)
this:
h (0, x) = part_circlepath c r a1 b1 x
h (1, x) = part_circlepath c r a2 b2 x

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
have "cis (pi * (real_of_int k * 2)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (pi * (real_of_int k * 2)) = 1
[PROOF STEP]
using cis.plus_of_int[of 0 k]
[PROOF STATE]
proof (prove)
using this:
cis (0 + real_of_int k * (2 * pi)) = cis 0

goal (1 subgoal):
 1. cis (pi * (real_of_int k * 2)) = 1
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
cis (pi * (real_of_int k * 2)) = 1

goal (1 subgoal):
 1. \<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
thus "pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)"
[PROOF STATE]
proof (prove)
using this:
cis (pi * (real_of_int k * 2)) = 1

goal (1 subgoal):
 1. pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)
[PROOF STEP]
by (simp add: h_def o_def exp_eq_polar linepath_def algebra_simps
                    cis_mult [symmetric] cis_divide [symmetric] assms)
[PROOF STATE]
proof (state)
this:
pathfinish (h \<circ> Pair x) = pathstart (h \<circ> Pair x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
homotopic_loops A (part_circlepath c r a1 b1) (part_circlepath c r a2 b2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma homotopic_pathsI:
  fixes h :: "real \<times> real \<Rightarrow> _"
  assumes "continuous_on ({0..1} \<times> {0..1}) h"
  assumes "h ` ({0..1} \<times> {0..1}) \<subseteq> s"
  assumes "\<And>x. x \<in> {0..1} \<Longrightarrow> h (0, x) = p x"
  assumes "\<And>x. x \<in> {0..1} \<Longrightarrow> h (1, x) = q x"
  assumes "\<And>x. x \<in> {0..1} \<Longrightarrow> pathstart (h \<circ> Pair x) = pathstart p"
  assumes "\<And>x. x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair x) = pathfinish p"
  shows   "homotopic_paths s p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. homotopic_paths s p q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on ({0..1} \<times> {0..1}) h
h ` ({0..1} \<times> {0..1}) \<subseteq> s
?x \<in> {0..1} \<Longrightarrow> h (0, ?x) = p ?x
?x \<in> {0..1} \<Longrightarrow> h (1, ?x) = q ?x
?x \<in> {0..1} \<Longrightarrow> pathstart (h \<circ> Pair ?x) = pathstart p
?x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair ?x) = pathfinish p

goal (1 subgoal):
 1. homotopic_paths s p q
[PROOF STEP]
unfolding homotopic_paths
[PROOF STATE]
proof (prove)
using this:
continuous_on ({0..1} \<times> {0..1}) h
h ` ({0..1} \<times> {0..1}) \<subseteq> s
?x \<in> {0..1} \<Longrightarrow> h (0, ?x) = p ?x
?x \<in> {0..1} \<Longrightarrow> h (1, ?x) = q ?x
?x \<in> {0..1} \<Longrightarrow> pathstart (h \<circ> Pair ?x) = pathstart p
?x \<in> {0..1} \<Longrightarrow> pathfinish (h \<circ> Pair ?x) = pathfinish p

goal (1 subgoal):
 1. \<exists>h. continuous_on ({0..1} \<times> {0..1}) h \<and> h ` ({0..1} \<times> {0..1}) \<subseteq> s \<and> (\<forall>x\<in>{0..1}. h (0, x) = p x) \<and> (\<forall>x\<in>{0..1}. h (1, x) = q x) \<and> (\<forall>t\<in>{0..1}. pathstart (h \<circ> Pair t) = pathstart p \<and> pathfinish (h \<circ> Pair t) = pathfinish p)
[PROOF STEP]
by (intro exI[of _ h]) auto


[STATEMENT]
lemma part_circlepath_conv_subpath:
  "part_circlepath c r a b = subpath (a / (2*pi)) (b / (2*pi)) (circlepath c r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part_circlepath c r a b = subpath (a / (2 * pi)) (b / (2 * pi)) (circlepath c r)
[PROOF STEP]
by (simp add: part_circlepath_def circlepath_def subpath_def linepath_def algebra_simps exp_eq_polar)