[STATEMENT]
lemma multiplicative_function_mult:
  assumes "multiplicative_function f"  "multiplicative_function g"
  shows   "multiplicative_function (\<lambda>n. f n * g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. f n * g n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f 0 * g 0 = (0::'a)
 2. f 1 * g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
interpret f: multiplicative_function f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f 0 * g 0 = (0::'a)
 2. f 1 * g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
interpret g: multiplicative_function g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function g
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f 0 * g 0 = (0::'a)
 2. f 1 * g 1 = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
show "f 0 * g 0 = 0" "f 1 * g 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 0 * g 0 = (0::'a) &&& f 1 * g 1 = (1::'a)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
f 0 * g 0 = (0::'a)
f 1 * g 1 = (1::'a)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
fix a b :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
assume "a > 1" "b > 1" "coprime a b"
[PROOF STATE]
proof (state)
this:
1 < a
1 < b
coprime a b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
thus "f (a * b) * g (a * b) = (f a * g a) * (f b * g b)"
[PROOF STATE]
proof (prove)
using this:
1 < a
1 < b
coprime a b

goal (1 subgoal):
 1. f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
by (simp_all add: f.mult_coprime g.mult_coprime mult_ac)
[PROOF STATE]
proof (state)
this:
f (a * b) * g (a * b) = f a * g a * (f b * g b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multiplicative_function_inverse:
  fixes f :: "nat \<Rightarrow> 'a :: field"
  assumes "multiplicative_function f"
  shows   "multiplicative_function (\<lambda>n. inverse (f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. inverse (f n))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inverse (f 0) = (0::'a)
 2. inverse (f 1) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
interpret f: multiplicative_function f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inverse (f 0) = (0::'a)
 2. inverse (f 1) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
show "inverse (f 0) = 0" "inverse (f 1) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (f 0) = (0::'a) &&& inverse (f 1) = (1::'a)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
inverse (f 0) = (0::'a)
inverse (f 1) = (1::'a)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
fix a b :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
assume "a > 1" "b > 1" "coprime a b"
[PROOF STATE]
proof (state)
this:
1 < a
1 < b
coprime a b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b; coprime a b\<rbrakk> \<Longrightarrow> inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
thus "inverse (f (a * b)) = inverse (f a) * inverse (f b)"
[PROOF STATE]
proof (prove)
using this:
1 < a
1 < b
coprime a b

goal (1 subgoal):
 1. inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
by (simp_all add: f.mult_coprime field_simps)
[PROOF STATE]
proof (state)
this:
inverse (f (a * b)) = inverse (f a) * inverse (f b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multiplicative_function_divide:
  fixes f :: "nat \<Rightarrow> 'a :: field"
  assumes "multiplicative_function f"  "multiplicative_function g"
  shows   "multiplicative_function (\<lambda>n. f n / g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
have "multiplicative_function (\<lambda>n. f n * inverse (g n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. f n * inverse (g n))
[PROOF STEP]
by (intro multiplicative_function_mult multiplicative_function_inverse assms)
[PROOF STATE]
proof (state)
this:
multiplicative_function (\<lambda>n. f n * inverse (g n))

goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicative_function (\<lambda>n. f n * inverse (g n))

goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
have "(\<lambda>n. f n * inverse (g n)) = (\<lambda>n. f n / g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f n * inverse (g n)) = (\<lambda>n. f n / g n)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n * inverse (g n)) = (\<lambda>n. f n / g n)

goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
multiplicative_function (\<lambda>n. f n / g n)

goal (1 subgoal):
 1. multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
multiplicative_function (\<lambda>n. f n / g n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma completely_multiplicative_function_mult:
  assumes "completely_multiplicative_function f" "completely_multiplicative_function g"
  shows   "completely_multiplicative_function (\<lambda>n. f n * g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function (\<lambda>n. f n * g n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f 0 * g 0 = (0::'a)
 2. f (Suc 0) * g (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
interpret f: completely_multiplicative_function f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f 0 * g 0 = (0::'a)
 2. f (Suc 0) * g (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
interpret g: completely_multiplicative_function g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function g
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f 0 * g 0 = (0::'a)
 2. f (Suc 0) * g (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
show "f 0 * g 0 = 0" "f (Suc 0) * g (Suc 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 0 * g 0 = (0::'a) &&& f (Suc 0) * g (Suc 0) = (1::'a)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
f 0 * g 0 = (0::'a)
f (Suc 0) * g (Suc 0) = (1::'a)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
fix a b :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
assume "a > 1" "b > 1"
[PROOF STATE]
proof (state)
this:
1 < a
1 < b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
thus "f (a * b) * g (a * b) = (f a * g a) * (f b * g b)"
[PROOF STATE]
proof (prove)
using this:
1 < a
1 < b

goal (1 subgoal):
 1. f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOF STEP]
by (simp_all add: f.mult g.mult mult_ac)
[PROOF STATE]
proof (state)
this:
f (a * b) * g (a * b) = f a * g a * (f b * g b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma completely_multiplicative_function_inverse:
  fixes f :: "nat \<Rightarrow> 'a :: field"
  assumes "completely_multiplicative_function f"
  shows   "completely_multiplicative_function (\<lambda>n. inverse (f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function (\<lambda>n. inverse (f n))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inverse (f 0) = (0::'a)
 2. inverse (f (Suc 0)) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
interpret f: completely_multiplicative_function f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inverse (f 0) = (0::'a)
 2. inverse (f (Suc 0)) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
show "inverse (f 0) = 0" "inverse (f (Suc 0)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (f 0) = (0::'a) &&& inverse (f (Suc 0)) = (1::'a)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
inverse (f 0) = (0::'a)
inverse (f (Suc 0)) = (1::'a)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
fix a b :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
assume "a > 1" "b > 1"
[PROOF STATE]
proof (state)
this:
1 < a
1 < b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
thus "inverse (f (a * b)) = inverse (f a) * inverse (f b)"
[PROOF STATE]
proof (prove)
using this:
1 < a
1 < b

goal (1 subgoal):
 1. inverse (f (a * b)) = inverse (f a) * inverse (f b)
[PROOF STEP]
by (simp_all add: f.mult field_simps)
[PROOF STATE]
proof (state)
this:
inverse (f (a * b)) = inverse (f a) * inverse (f b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma completely_multiplicative_function_divide:
  fixes f :: "nat \<Rightarrow> 'a :: field"
  assumes "completely_multiplicative_function f"  "completely_multiplicative_function g"
  shows   "completely_multiplicative_function (\<lambda>n. f n / g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. completely_multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
have "completely_multiplicative_function (\<lambda>n. f n * inverse (g n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function (\<lambda>n. f n * inverse (g n))
[PROOF STEP]
by (intro completely_multiplicative_function_mult
              completely_multiplicative_function_inverse assms)
[PROOF STATE]
proof (state)
this:
completely_multiplicative_function (\<lambda>n. f n * inverse (g n))

goal (1 subgoal):
 1. completely_multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
completely_multiplicative_function (\<lambda>n. f n * inverse (g n))

goal (1 subgoal):
 1. completely_multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
have "(\<lambda>n. f n * inverse (g n)) = (\<lambda>n. f n / g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f n * inverse (g n)) = (\<lambda>n. f n / g n)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n * inverse (g n)) = (\<lambda>n. f n / g n)

goal (1 subgoal):
 1. completely_multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
completely_multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
completely_multiplicative_function (\<lambda>n. f n / g n)

goal (1 subgoal):
 1. completely_multiplicative_function (\<lambda>n. f n / g n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
completely_multiplicative_function (\<lambda>n. f n / g n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in multiplicative_function) completely_multiplicativeI:
  assumes "\<And>p k. prime p \<Longrightarrow> k > 0 \<Longrightarrow> f (p ^ k) = f p ^ k"
  shows   "completely_multiplicative_function f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
fix m n :: nat
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
assume mn: "m > 1" "n > 1"
[PROOF STATE]
proof (state)
this:
1 < m
1 < n

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
define P where "P = prime_factors (m * n)"
[PROOF STATE]
proof (state)
this:
P = prime_factors (m * n)

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
have "f (m * n) = (\<Prod>p\<in>P. f (p ^ multiplicity p (m * n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (m * n) = (\<Prod>p\<in>P. f (p ^ multiplicity p (m * n)))
[PROOF STEP]
using mn
[PROOF STATE]
proof (prove)
using this:
1 < m
1 < n

goal (1 subgoal):
 1. f (m * n) = (\<Prod>p\<in>P. f (p ^ multiplicity p (m * n)))
[PROOF STEP]
by (subst prod_prime_factors) (auto simp: P_def)
[PROOF STATE]
proof (state)
this:
f (m * n) = (\<Prod>p\<in>P. f (p ^ multiplicity p (m * n)))

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (m * n) = (\<Prod>p\<in>P. f (p ^ multiplicity p (m * n)))

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
have "\<dots> = (\<Prod>p\<in>P. f p ^ multiplicity p (m * n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>P. f (p ^ multiplicity p (m * n))) = (\<Prod>p\<in>P. f p ^ multiplicity p (m * n))
[PROOF STEP]
by (intro prod.cong) (auto simp: assms prime_factors_multiplicity P_def)
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>P. f (p ^ multiplicity p (m * n))) = (\<Prod>p\<in>P. f p ^ multiplicity p (m * n))

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>P. f (p ^ multiplicity p (m * n))) = (\<Prod>p\<in>P. f p ^ multiplicity p (m * n))

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
have "\<dots> = (\<Prod>p\<in>P. f p ^ multiplicity p m * f p ^ multiplicity p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>P. f p ^ multiplicity p (m * n)) = (\<Prod>p\<in>P. f p ^ multiplicity p m * f p ^ multiplicity p n)
[PROOF STEP]
by (intro prod.cong refl, subst prime_elem_multiplicity_mult_distrib)
       (use mn in \<open>auto simp: P_def prime_factors_multiplicity power_add\<close>)
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>P. f p ^ multiplicity p (m * n)) = (\<Prod>p\<in>P. f p ^ multiplicity p m * f p ^ multiplicity p n)

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>P. f p ^ multiplicity p (m * n)) = (\<Prod>p\<in>P. f p ^ multiplicity p m * f p ^ multiplicity p n)

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
have "\<dots> = (\<Prod>p\<in>P. f p ^ multiplicity p m) * (\<Prod>p\<in>P. f p ^ multiplicity p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>P. f p ^ multiplicity p m * f p ^ multiplicity p n) = (\<Prod>p\<in>P. f p ^ multiplicity p m) * (\<Prod>p\<in>P. f p ^ multiplicity p n)
[PROOF STEP]
by (rule prod.distrib)
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>P. f p ^ multiplicity p m * f p ^ multiplicity p n) = (\<Prod>p\<in>P. f p ^ multiplicity p m) * (\<Prod>p\<in>P. f p ^ multiplicity p n)

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>P. f p ^ multiplicity p m * f p ^ multiplicity p n) = (\<Prod>p\<in>P. f p ^ multiplicity p m) * (\<Prod>p\<in>P. f p ^ multiplicity p n)

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
have "(\<Prod>p\<in>P. f p ^ multiplicity p m) = (\<Prod>p\<in>prime_factors m. f p ^ multiplicity p m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>P. f p ^ multiplicity p m) = (\<Prod>p\<in>prime_factors m. f p ^ multiplicity p m)
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors (m * n). f p ^ multiplicity p m) = (\<Prod>p\<in>prime_factors m. f p ^ multiplicity p m)
[PROOF STEP]
by (intro prod.mono_neutral_right dvd_prime_factors finite_set_mset)
                       (use mn in \<open>auto simp: prime_factors_multiplicity\<close>)
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>P. f p ^ multiplicity p m) = (\<Prod>p\<in>prime_factors m. f p ^ multiplicity p m)

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>P. f p ^ multiplicity p m) = (\<Prod>p\<in>prime_factors m. f p ^ multiplicity p m)

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
have "\<dots> = (\<Prod>p\<in>prime_factors m. f (p ^ multiplicity p m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors m. f p ^ multiplicity p m) = (\<Prod>p\<in>prime_factors m. f (p ^ multiplicity p m))
[PROOF STEP]
by (intro prod.cong) (auto simp: assms prime_factors_multiplicity)
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>prime_factors m. f p ^ multiplicity p m) = (\<Prod>p\<in>prime_factors m. f (p ^ multiplicity p m))

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>prime_factors m. f p ^ multiplicity p m) = (\<Prod>p\<in>prime_factors m. f (p ^ multiplicity p m))

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
have "\<dots> = f m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors m. f (p ^ multiplicity p m)) = f m
[PROOF STEP]
using mn
[PROOF STATE]
proof (prove)
using this:
1 < m
1 < n

goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors m. f (p ^ multiplicity p m)) = f m
[PROOF STEP]
by (intro prod_prime_factors [symmetric]) auto
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>prime_factors m. f (p ^ multiplicity p m)) = f m

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>prime_factors m. f (p ^ multiplicity p m)) = f m

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
have "(\<Prod>p\<in>P. f p ^ multiplicity p n) = (\<Prod>p\<in>prime_factors n. f p ^ multiplicity p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>P. f p ^ multiplicity p n) = (\<Prod>p\<in>prime_factors n. f p ^ multiplicity p n)
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors (m * n). f p ^ multiplicity p n) = (\<Prod>p\<in>prime_factors n. f p ^ multiplicity p n)
[PROOF STEP]
by (intro prod.mono_neutral_right dvd_prime_factors finite_set_mset)
                       (use mn in \<open>auto simp: prime_factors_multiplicity\<close>)
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>P. f p ^ multiplicity p n) = (\<Prod>p\<in>prime_factors n. f p ^ multiplicity p n)

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>P. f p ^ multiplicity p n) = (\<Prod>p\<in>prime_factors n. f p ^ multiplicity p n)

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
have "\<dots> = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors n. f p ^ multiplicity p n) = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))
[PROOF STEP]
by (intro prod.cong) (auto simp: assms prime_factors_multiplicity)
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>prime_factors n. f p ^ multiplicity p n) = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>prime_factors n. f p ^ multiplicity p n) = (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n))

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
have "\<dots> = f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n)) = f n
[PROOF STEP]
using mn
[PROOF STATE]
proof (prove)
using this:
1 < m
1 < n

goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n)) = f n
[PROOF STEP]
by (intro prod_prime_factors [symmetric]) auto
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>prime_factors n. f (p ^ multiplicity p n)) = f n

goal (3 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
 3. \<And>a b. \<lbrakk>1 < a; 1 < b\<rbrakk> \<Longrightarrow> f (a * b) = f a * f b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f (m * n) = f m * f n
[PROOF STEP]
show "f (m * n) = f m * f n"
[PROOF STATE]
proof (prove)
using this:
f (m * n) = f m * f n

goal (1 subgoal):
 1. f (m * n) = f m * f n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f (m * n) = f m * f n

goal (2 subgoals):
 1. f 0 = (0::'a)
 2. f (Suc 0) = (1::'a)
[PROOF STEP]
qed auto


[STATEMENT]
lemma ind_0 [simp]: "ind P 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind P 0 = (0::'a)
[PROOF STEP]
by (simp add: ind_def)


[STATEMENT]
lemma ind_nonzero: "n > 0 \<Longrightarrow> ind P n = (if P n then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> ind P n = (if P n then 1::'a else (0::'a))
[PROOF STEP]
by (simp add: ind_def)


[STATEMENT]
lemma ind_True [simp]: "P n \<Longrightarrow> n > 0 \<Longrightarrow> ind P n = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P n; 0 < n\<rbrakk> \<Longrightarrow> ind P n = (1::'a)
[PROOF STEP]
by (simp add: ind_nonzero)


[STATEMENT]
lemma ind_False [simp]: "\<not>P n \<Longrightarrow> n > 0 \<Longrightarrow> ind P n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P n; 0 < n\<rbrakk> \<Longrightarrow> ind P n = (0::'a)
[PROOF STEP]
by (simp add: ind_nonzero)


[STATEMENT]
lemma ind_eq_1_iff: "ind P n = 1 \<longleftrightarrow> n > 0 \<and> P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ind P n = (1::'a)) = (0 < n \<and> P n)
[PROOF STEP]
by (simp add: ind_def)


[STATEMENT]
lemma ind_eq_0_iff: "ind P n = 0 \<longleftrightarrow> n = 0 \<or> \<not>P n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ind P n = (0::'a)) = (n = 0 \<or> \<not> P n)
[PROOF STEP]
by (simp add: ind_def)


[STATEMENT]
lemma multiplicative_function_ind [intro?]:
  assumes "P 1" "\<And>a b. a > 1 \<Longrightarrow> b > 1 \<Longrightarrow> coprime a b \<Longrightarrow> P (a * b) \<longleftrightarrow> P a \<and> P b"
  shows   "multiplicative_function (ind P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicative_function (ind P)
[PROOF STEP]
by standard (insert assms, auto simp: ind_nonzero)


[STATEMENT]
lemma f_nonpos[simp]: "x \<le> 0 \<Longrightarrow> f x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> 0 \<Longrightarrow> f x = 0
[PROOF STEP]
by (auto simp: f_def)


[STATEMENT]
lemma exp_inv_limit_0_right:
  "((\<lambda>(t::real). exp(-inverse t)) \<longlongrightarrow> 0) (at_right 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. exp (- inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
apply (rule filterlim_compose[where g = exp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (exp \<longlongrightarrow> 0) ?F2.0
 2. LIM x at_right 0. - inverse x :> ?F2.0
[PROOF STEP]
apply (rule exp_at_bot)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM x at_right 0. - inverse x :> at_bot
[PROOF STEP]
apply (rule filterlim_compose[where g = uminus])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. filterlim uminus at_bot ?F2.4
 2. filterlim inverse ?F2.4 (at_right 0)
[PROOF STEP]
apply (rule filterlim_uminus_at_bot_at_top)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filterlim inverse at_top (at_right 0)
[PROOF STEP]
by (rule filterlim_inverse_at_top_right)


[STATEMENT]
lemma "\<forall>\<^sub>F t in at_right 0. ((\<lambda>x. inverse (x ^ Suc k)) has_real_derivative
  - (inverse (t ^ Suc k) * ((1 + real k) * t ^ k) * inverse (t ^ Suc k))) (at t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F t in at_right 0. ((\<lambda>x. inverse (x ^ Suc k)) has_real_derivative - (inverse (t ^ Suc k) * ((1 + real k) * t ^ k) * inverse (t ^ Suc k))) (at t)
[PROOF STEP]
unfolding eventually_at_filter
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds 0. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> ((\<lambda>x. inverse (x ^ Suc k)) has_real_derivative - (inverse (x ^ Suc k) * ((1 + real k) * x ^ k) * inverse (x ^ Suc k))) (at x)
[PROOF STEP]
by (auto simp del: power_Suc intro!: derivative_eq_intros eventuallyI)


[STATEMENT]
lemma exp_inv_limit_0_right_gen':
  "((\<lambda>(t::real). inverse (t ^ k) / exp(inverse t)) \<longlongrightarrow> 0) (at_right 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ((\<lambda>t. inverse (t ^ 0) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
 2. \<And>k. ((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0) \<Longrightarrow> ((\<lambda>t. inverse (t ^ Suc k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. ((\<lambda>t. inverse (t ^ 0) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
 2. \<And>k. ((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0) \<Longrightarrow> ((\<lambda>t. inverse (t ^ Suc k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. inverse (t ^ 0) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
using exp_inv_limit_0_right
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. exp (- inverse t)) \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. ((\<lambda>t. inverse (t ^ 0) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
by (auto simp: exp_minus inverse_eq_divide)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. inverse (t ^ 0) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. \<And>k. ((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0) \<Longrightarrow> ((\<lambda>t. inverse (t ^ Suc k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. ((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0) \<Longrightarrow> ((\<lambda>t. inverse (t ^ Suc k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. \<And>k. ((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0) \<Longrightarrow> ((\<lambda>t. inverse (t ^ Suc k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
have df: "\<forall>\<^sub>F t in at_right 0. ((\<lambda>x. inverse (x ^ Suc k)) has_real_derivative
    - (inverse (t ^ k) * ((1 + real k)) * (inverse t ^ 2))) (at t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F t in at_right 0. ((\<lambda>x. inverse (x ^ Suc k)) has_real_derivative - (inverse (t ^ k) * (1 + real k) * (inverse t)\<^sup>2)) (at t)
[PROOF STEP]
unfolding eventually_at_filter
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds 0. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> ((\<lambda>x. inverse (x ^ Suc k)) has_real_derivative - (inverse (x ^ k) * (1 + real k) * (inverse x)\<^sup>2)) (at x)
[PROOF STEP]
apply (auto simp del: power_Suc intro!: derivative_eq_intros eventuallyI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. 0 < x \<Longrightarrow> inverse (x ^ Suc k) * (x ^ k * inverse (x ^ Suc k)) = inverse (x ^ k) * (inverse x)\<^sup>2
[PROOF STEP]
by (auto simp: power2_eq_square)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F t in at_right 0. ((\<lambda>x. inverse (x ^ Suc k)) has_real_derivative - (inverse (t ^ k) * (1 + real k) * (inverse t)\<^sup>2)) (at t)

goal (1 subgoal):
 1. \<And>k. ((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0) \<Longrightarrow> ((\<lambda>t. inverse (t ^ Suc k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
have dg: "\<forall>\<^sub>F t in at_right 0. ((\<lambda>x. exp (inverse x)) has_real_derivative
    - (exp (inverse t) * (inverse t ^ 2))) (at t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F t in at_right 0. ((\<lambda>x. exp (inverse x)) has_real_derivative - (exp (inverse t) * (inverse t)\<^sup>2)) (at t)
[PROOF STEP]
unfolding eventually_at_filter
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in nhds 0. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> ((\<lambda>x. exp (inverse x)) has_real_derivative - (exp (inverse x) * (inverse x)\<^sup>2)) (at x)
[PROOF STEP]
by (auto simp del: power_Suc intro!: derivative_eq_intros eventuallyI simp: power2_eq_square)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F t in at_right 0. ((\<lambda>x. exp (inverse x)) has_real_derivative - (exp (inverse t) * (inverse t)\<^sup>2)) (at t)

goal (1 subgoal):
 1. \<And>k. ((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0) \<Longrightarrow> ((\<lambda>t. inverse (t ^ Suc k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. inverse (t ^ Suc k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
apply (rule lhopital_right_0_at_top [OF _ _ df dg])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. LIM t at_right 0. exp (inverse t) :> at_top
 2. \<forall>\<^sub>F t in at_right 0. - (exp (inverse t) * (inverse t)\<^sup>2) \<noteq> 0
 3. ((\<lambda>t. - (inverse (t ^ k) * (1 + real k) * (inverse t)\<^sup>2) / - (exp (inverse t) * (inverse t)\<^sup>2)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
apply (rule filterlim_compose[where g = exp])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. filterlim exp at_top ?F2.6
 2. filterlim inverse ?F2.6 (at_right 0)
 3. \<forall>\<^sub>F t in at_right 0. - (exp (inverse t) * (inverse t)\<^sup>2) \<noteq> 0
 4. ((\<lambda>t. - (inverse (t ^ k) * (1 + real k) * (inverse t)\<^sup>2) / - (exp (inverse t) * (inverse t)\<^sup>2)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
apply (rule exp_at_top)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. filterlim inverse at_top (at_right 0)
 2. \<forall>\<^sub>F t in at_right 0. - (exp (inverse t) * (inverse t)\<^sup>2) \<noteq> 0
 3. ((\<lambda>t. - (inverse (t ^ k) * (1 + real k) * (inverse t)\<^sup>2) / - (exp (inverse t) * (inverse t)\<^sup>2)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
apply (rule filterlim_inverse_at_top_right)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>\<^sub>F t in at_right 0. - (exp (inverse t) * (inverse t)\<^sup>2) \<noteq> 0
 2. ((\<lambda>t. - (inverse (t ^ k) * (1 + real k) * (inverse t)\<^sup>2) / - (exp (inverse t) * (inverse t)\<^sup>2)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F t in at_right 0. - (exp (inverse t) * (inverse t)\<^sup>2) \<noteq> 0
[PROOF STEP]
by (auto simp: eventually_at_filter)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. - (inverse (t ^ k) * (1 + real k) * (inverse t)\<^sup>2) / - (exp (inverse t) * (inverse t)\<^sup>2)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. - (inverse (t ^ k) * (1 + real k) * (inverse t)\<^sup>2) / - (exp (inverse t) * (inverse t)\<^sup>2)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
apply (rule Lim_transform_eventually[where f = "\<lambda>x. (1 + real k) * (inverse (x ^ k) / exp (inverse x))"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((\<lambda>x. (1 + real k) * (inverse (x ^ k) / exp (inverse x))) \<longlongrightarrow> 0) (at_right 0)
 2. \<forall>\<^sub>F x in at_right 0. (1 + real k) * (inverse (x ^ k) / exp (inverse x)) = - (inverse (x ^ k) * (1 + real k) * (inverse x)\<^sup>2) / - (exp (inverse x) * (inverse x)\<^sup>2)
[PROOF STEP]
using Suc.hyps tendsto_mult_right_zero
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)
(?f \<longlongrightarrow> (0::?'a)) ?F \<Longrightarrow> ((\<lambda>x. ?c * ?f x) \<longlongrightarrow> (0::?'a)) ?F

goal (2 subgoals):
 1. ((\<lambda>x. (1 + real k) * (inverse (x ^ k) / exp (inverse x))) \<longlongrightarrow> 0) (at_right 0)
 2. \<forall>\<^sub>F x in at_right 0. (1 + real k) * (inverse (x ^ k) / exp (inverse x)) = - (inverse (x ^ k) * (1 + real k) * (inverse x)\<^sup>2) / - (exp (inverse x) * (inverse x)\<^sup>2)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_right 0. (1 + real k) * (inverse (x ^ k) / exp (inverse x)) = - (inverse (x ^ k) * (1 + real k) * (inverse x)\<^sup>2) / - (exp (inverse x) * (inverse x)\<^sup>2)
[PROOF STEP]
by (auto simp: eventually_at_filter)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((\<lambda>t. inverse (t ^ Suc k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_inv_limit_0_right_gen:
  "((\<lambda>(t::real). exp(-inverse t) / t ^ k) \<longlongrightarrow> 0) (at_right 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. exp (- inverse t) / t ^ k) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
using exp_inv_limit_0_right_gen'[of k]
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. inverse (t ^ k) / exp (inverse t)) \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. ((\<lambda>t. exp (- inverse t) / t ^ k) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
by (metis (no_types, lifting) Groups.mult_ac(2) Lim_cong_within divide_inverse exp_minus)


[STATEMENT]
lemma f_limit_0_right: "(f \<longlongrightarrow> 0) (at_right 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
have "\<forall>\<^sub>F t in at_right 0. (t::real) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually ((<) 0) (at_right 0)
[PROOF STEP]
by (rule eventually_at_right_less)
[PROOF STATE]
proof (state)
this:
eventually ((<) 0) (at_right 0)

goal (1 subgoal):
 1. (f \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eventually ((<) 0) (at_right 0)
[PROOF STEP]
have "\<forall>\<^sub>F t in at_right 0. exp(-inverse t) = f t"
[PROOF STATE]
proof (prove)
using this:
eventually ((<) 0) (at_right 0)

goal (1 subgoal):
 1. \<forall>\<^sub>F t in at_right 0. exp (- inverse t) = f t
[PROOF STEP]
by (eventually_elim) (auto simp: f_def)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F t in at_right 0. exp (- inverse t) = f t

goal (1 subgoal):
 1. (f \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F t in at_right 0. exp (- inverse t) = f t

goal (1 subgoal):
 1. (f \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
have "((\<lambda>(t::real). exp(-inverse t)) \<longlongrightarrow> 0) (at_right 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. exp (- inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
by (rule exp_inv_limit_0_right)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. exp (- inverse t)) \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. (f \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F t in at_right 0. exp (- inverse t) = f t
((\<lambda>t. exp (- inverse t)) \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F t in at_right 0. exp (- inverse t) = f t
((\<lambda>t. exp (- inverse t)) \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. (f \<longlongrightarrow> 0) (at_right 0)
[PROOF STEP]
by (blast intro: Lim_transform_eventually)
[PROOF STATE]
proof (state)
this:
(f \<longlongrightarrow> 0) (at_right 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_limit_0: "(f \<longlongrightarrow> 0) (at 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<midarrow>0\<rightarrow> 0
[PROOF STEP]
using _ f_limit_0_right
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
(f \<longlongrightarrow> 0) (at_right 0)

goal (1 subgoal):
 1. f \<midarrow>0\<rightarrow> 0
[PROOF STEP]
proof (rule filterlim_split_at_real)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f \<longlongrightarrow> 0) (at_left 0)
[PROOF STEP]
have "\<forall>\<^sub>F t in at_left 0. 0 = f t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F t in at_left 0. 0 = f t
[PROOF STEP]
by (auto simp: f_def eventually_at_filter)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F t in at_left 0. 0 = f t

goal (1 subgoal):
 1. (f \<longlongrightarrow> 0) (at_left 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F t in at_left 0. 0 = f t
[PROOF STEP]
show "(f \<longlongrightarrow> 0) (at_left 0)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F t in at_left 0. 0 = f t

goal (1 subgoal):
 1. (f \<longlongrightarrow> 0) (at_left 0)
[PROOF STEP]
by (blast intro: Lim_transform_eventually)
[PROOF STATE]
proof (state)
this:
(f \<longlongrightarrow> 0) (at_left 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_tendsto: "(f \<longlongrightarrow> f x) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
consider "x = 0" | "x < 0" | "x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = 0 \<Longrightarrow> thesis; x < 0 \<Longrightarrow> thesis; 0 < x \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = 0 \<Longrightarrow> ?thesis; x < 0 \<Longrightarrow> ?thesis; 0 < x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x = 0 \<Longrightarrow> ?thesis; x < 0 \<Longrightarrow> ?thesis; 0 < x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = 0 \<Longrightarrow> ?thesis; x < 0 \<Longrightarrow> ?thesis; 0 < x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x = 0 \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
 2. x < 0 \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
 3. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
x = 0

goal (3 subgoals):
 1. x = 0 \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
 2. x < 0 \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
 3. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
by (auto simp: f_limit_0 f_def)
[PROOF STATE]
proof (state)
this:
f \<midarrow>x\<rightarrow> f x

goal (2 subgoals):
 1. x < 0 \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
 2. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < 0 \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
 2. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
x < 0

goal (2 subgoals):
 1. x < 0 \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
 2. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
have "\<forall>\<^sub>F t in at x. t < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F t in at x. t < 0
[PROOF STEP]
apply (rule order_tendstoD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<lambda>x. x) \<midarrow>x\<rightarrow> ?y
 2. ?y < 0
[PROOF STEP]
by (rule tendsto_intros) fact
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F t in at x. t < 0

goal (2 subgoals):
 1. x < 0 \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
 2. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F t in at x. t < 0
[PROOF STEP]
have "\<forall>\<^sub>F t in at x. 0 = f t"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F t in at x. t < 0

goal (1 subgoal):
 1. \<forall>\<^sub>F t in at x. 0 = f t
[PROOF STEP]
by (eventually_elim) (auto simp: f_def)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F t in at x. 0 = f t

goal (2 subgoals):
 1. x < 0 \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
 2. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F t in at x. 0 = f t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F t in at x. 0 = f t

goal (1 subgoal):
 1. f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
using \<open>x < 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F t in at x. 0 = f t
x < 0

goal (1 subgoal):
 1. f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
by (auto simp: f_def intro: Lim_transform_eventually)
[PROOF STATE]
proof (state)
this:
f \<midarrow>x\<rightarrow> f x

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
0 < x

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
have "\<forall>\<^sub>F t in at x. t > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually ((<) 0) (at x)
[PROOF STEP]
apply (rule order_tendstoD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<lambda>x. x) \<midarrow>x\<rightarrow> ?y
 2. 0 < ?y
[PROOF STEP]
by (rule tendsto_intros) fact
[PROOF STATE]
proof (state)
this:
eventually ((<) 0) (at x)

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eventually ((<) 0) (at x)
[PROOF STEP]
have "\<forall>\<^sub>F t in at x. exp(-inverse t) = f t"
[PROOF STATE]
proof (prove)
using this:
eventually ((<) 0) (at x)

goal (1 subgoal):
 1. \<forall>\<^sub>F t in at x. exp (- inverse t) = f t
[PROOF STEP]
by (eventually_elim) (auto simp: f_def)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F t in at x. exp (- inverse t) = f t

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F t in at x. exp (- inverse t) = f t

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
have "(\<lambda>t. exp (- inverse t)) \<midarrow>x\<rightarrow> f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>t. exp (- inverse t)) \<midarrow>x\<rightarrow> f x
[PROOF STEP]
using \<open>x > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. (\<lambda>t. exp (- inverse t)) \<midarrow>x\<rightarrow> f x
[PROOF STEP]
by (auto simp: f_def tendsto_intros )
[PROOF STATE]
proof (state)
this:
(\<lambda>t. exp (- inverse t)) \<midarrow>x\<rightarrow> f x

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F t in at x. exp (- inverse t) = f t
(\<lambda>t. exp (- inverse t)) \<midarrow>x\<rightarrow> f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F t in at x. exp (- inverse t) = f t
(\<lambda>t. exp (- inverse t)) \<midarrow>x\<rightarrow> f x

goal (1 subgoal):
 1. f \<midarrow>x\<rightarrow> f x
[PROOF STEP]
by (blast intro: Lim_transform_eventually)
[PROOF STATE]
proof (state)
this:
f \<midarrow>x\<rightarrow> f x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f \<midarrow>x\<rightarrow> f x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_continuous: "continuous_on S f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S f
[PROOF STEP]
using f_tendsto continuous_on continuous_on_subset subset_UNIV
[PROOF STATE]
proof (prove)
using this:
f \<midarrow>?x\<rightarrow> f ?x
continuous_on ?s ?f = (\<forall>x\<in>?s. (?f \<longlongrightarrow> ?f x) (at x within ?s))
\<lbrakk>continuous_on ?s ?f; ?t \<subseteq> ?s\<rbrakk> \<Longrightarrow> continuous_on ?t ?f
?A \<subseteq> UNIV

goal (1 subgoal):
 1. continuous_on S f
[PROOF STEP]
by metis


[STATEMENT]
lemma continuous_on_real_polynomial_function:
  "continuous_on S p" if "real_polynomial_function p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S p
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
real_polynomial_function p

goal (1 subgoal):
 1. continuous_on S p
[PROOF STEP]
by induction (auto intro: continuous_intros linear_continuous_on)


[STATEMENT]
lemma f_nth_derivative_is_poly:
  "higher_differentiable_on {0<..} f k \<and>
   (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / (t ^ (2 * k)) * exp(-inverse t)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)))
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. higher_differentiable_on {0<..} f 0 \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative 0 f t 1 = p t / t ^ (2 * 0) * exp (- inverse t)))
 2. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. higher_differentiable_on {0<..} f 0 \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative 0 f t 1 = p t / t ^ (2 * 0) * exp (- inverse t)))
 2. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on {0<..} f 0 \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative 0 f t 1 = p t / t ^ (2 * 0) * exp (- inverse t)))
[PROOF STEP]
apply (auto simp: higher_differentiable_on.simps f_continuous)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. real_polynomial_function p \<and> (\<forall>t>0. f t = p t * exp (- inverse t))
[PROOF STEP]
by (auto simp: f_def)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {0<..} f 0 \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative 0 f t 1 = p t / t ^ (2 * 0) * exp (- inverse t)))

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)))

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
obtain p where fk: "higher_differentiable_on {0<..} f k"
    and p1: "real_polynomial_function p"
    and p2: "\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>higher_differentiable_on {0<..} f k; real_polynomial_function p; \<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)))

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>higher_differentiable_on {0<..} f k; real_polynomial_function p; \<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {0<..} f k
real_polynomial_function p
\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
obtain p' where p'1: "real_polynomial_function p'"
    and p'2: "\<forall>t. (p has_real_derivative (p' t)) (at t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>real_polynomial_function p'; \<forall>t. (p has_real_derivative p' t) (at t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using has_real_derivative_polynomial_function[of p] p1
[PROOF STATE]
proof (prove)
using this:
real_polynomial_function p \<Longrightarrow> \<exists>p'. real_polynomial_function p' \<and> (\<forall>x. (p has_real_derivative p' x) (at x))
real_polynomial_function p

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>real_polynomial_function p'; \<forall>t. (p has_real_derivative p' t) (at t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_polynomial_function p'
\<forall>t. (p has_real_derivative p' t) (at t)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
define rp where "rp t = (t\<^sup>2 * p' t - 2 * real k * t * p t + p t)" for t
[PROOF STATE]
proof (state)
this:
rp ?t = ?t\<^sup>2 * p' ?t - 2 * real k * ?t * p ?t + p ?t

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have rp: "real_polynomial_function rp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_polynomial_function rp
[PROOF STEP]
unfolding rp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_polynomial_function (\<lambda>t. t\<^sup>2 * p' t - 2 * real k * t * p t + p t)
[PROOF STEP]
by (auto intro!: real_polynomial_function.intros(2-) real_polynomial_function_diff
        p1 p'1 simp: power2_eq_square)
[PROOF STATE]
proof (state)
this:
real_polynomial_function rp

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real_polynomial_function rp

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have fk': "(\<lambda>x. nth_derivative k f x 1) differentiable at t" (is ?a)
    "frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 =
        rp t * (exp (-inverse t) / t^(2*k+2))" (is ?b)
    if "0 < t" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at t &&& frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t * (exp (- inverse t) / t ^ (2 * k + 2))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at t
 2. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t * (exp (- inverse t) / t ^ (2 * k + 2))
[PROOF STEP]
from p'2 that
[PROOF STATE]
proof (chain)
picking this:
\<forall>t. (p has_real_derivative p' t) (at t)
0 < t
[PROOF STEP]
have dp: "(p has_derivative ((*) (p' t))) (at t within {0<..})"
[PROOF STATE]
proof (prove)
using this:
\<forall>t. (p has_real_derivative p' t) (at t)
0 < t

goal (1 subgoal):
 1. (p has_derivative (*) (p' t)) (at t within {0<..})
[PROOF STEP]
by (auto simp: at_within_open[of _ "{0<..}"] has_field_derivative_def ac_simps)
[PROOF STATE]
proof (state)
this:
(p has_derivative (*) (p' t)) (at t within {0<..})

goal (2 subgoals):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at t
 2. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t * (exp (- inverse t) / t ^ (2 * k + 2))
[PROOF STEP]
have "((\<lambda>t. p t / t ^ (2 * k) * exp (- inverse t)) has_derivative
      (\<lambda>v. v * rp t * (exp (-inverse t) / t^(2*k+2)))) (at t within {0<..})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. p t / t ^ (2 * k) * exp (- inverse t)) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t within {0<..})
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
0 < t

goal (1 subgoal):
 1. ((\<lambda>t. p t / t ^ (2 * k) * exp (- inverse t)) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t within {0<..})
[PROOF STEP]
apply (auto intro!: derivative_eq_intros dp ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. 0 < t \<Longrightarrow> ((p t * (inverse t * h * inverse t * exp (- inverse t)) + p' t * h * exp (- inverse t)) * t ^ (2 * k) - p t * exp (- inverse t) * (2 * real k * h * t ^ (2 * k - Suc 0))) / (t ^ (2 * k) * t ^ (2 * k)) = h * rp t * exp (- inverse t) / (t * (t * t ^ (2 * k)))
[PROOF STEP]
apply (simp add: divide_simps algebra_simps rp_def power2_eq_square)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. 0 < t \<Longrightarrow> h = 0 \<or> k = 0 \<or> p t = 0 \<or> t ^ (k * 2) = t * t ^ (k * 2 - Suc 0)
[PROOF STEP]
by (metis Suc_pred mult_is_0 neq0_conv power_Suc zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. p t / t ^ (2 * k) * exp (- inverse t)) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t within {0<..})

goal (2 subgoals):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at t
 2. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t * (exp (- inverse t) / t ^ (2 * k + 2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>t. p t / t ^ (2 * k) * exp (- inverse t)) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t within {0<..})
[PROOF STEP]
have "((\<lambda>x. nth_derivative k f x 1) has_derivative
      (\<lambda>v. v * rp t * (exp (-inverse t) / t^(2*k+2)))) (at t within {0<..})"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. p t / t ^ (2 * k) * exp (- inverse t)) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t within {0<..})

goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t within {0<..})
[PROOF STEP]
apply (rule has_derivative_transform_within[OF _ zero_less_one])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. t \<in> {0<..}
 2. \<And>x'. \<lbrakk>x' \<in> {0<..}; dist x' t < 1\<rbrakk> \<Longrightarrow> p x' / x' ^ (2 * k) * exp (- inverse x') = nth_derivative k f x' 1
[PROOF STEP]
using that p2
[PROOF STATE]
proof (prove)
using this:
0 < t
\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t)

goal (2 subgoals):
 1. t \<in> {0<..}
 2. \<And>x'. \<lbrakk>x' \<in> {0<..}; dist x' t < 1\<rbrakk> \<Longrightarrow> p x' / x' ^ (2 * k) * exp (- inverse x') = nth_derivative k f x' 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t within {0<..})

goal (2 subgoals):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at t
 2. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t * (exp (- inverse t) / t ^ (2 * k + 2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t within {0<..})
[PROOF STEP]
have "((\<lambda>x. nth_derivative k f x 1) has_derivative
      (\<lambda>v. v * rp t * (exp (-inverse t) / t^(2*k+2)))) (at t)"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t within {0<..})

goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t within {0<..})
0 < t

goal (1 subgoal):
 1. ((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t)
[PROOF STEP]
by (auto simp: at_within_open[of _ "{0<..}"])
[PROOF STATE]
proof (state)
this:
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t)

goal (2 subgoals):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at t
 2. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t * (exp (- inverse t) / t ^ (2 * k + 2))
[PROOF STEP]
from frechet_derivative_at'[OF this] this
[PROOF STATE]
proof (chain)
picking this:
frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) = (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t)
[PROOF STEP]
show ?a ?b
[PROOF STATE]
proof (prove)
using this:
frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) = (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))
((\<lambda>x. nth_derivative k f x 1) has_derivative (\<lambda>v. v * rp t * (exp (- inverse t) / t ^ (2 * k + 2)))) (at t)

goal (1 subgoal):
 1. (\<lambda>x. nth_derivative k f x 1) differentiable at t &&& frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t * (exp (- inverse t) / t ^ (2 * k + 2))
[PROOF STEP]
by (auto simp: differentiable_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. nth_derivative k f x 1) differentiable at t
frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t * (exp (- inverse t) / t ^ (2 * k + 2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?t \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at ?t
0 < ?t \<Longrightarrow> frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at ?t) 1 = rp ?t * (exp (- inverse ?t) / ?t ^ (2 * k + 2))

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have hdS: "higher_differentiable_on {0<..} f (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on {0<..} f (Suc k)
[PROOF STEP]
apply (subst higher_differentiable_on_real_Suc')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. open {0<..}
 2. (\<forall>v. continuous_on {0<..} (\<lambda>x. nth_derivative (Suc k) f x 1)) \<and> (\<forall>x\<in>{0<..}. \<forall>v. (\<lambda>x. nth_derivative k f x 1) differentiable at x) \<and> higher_differentiable_on {0<..} f k
[PROOF STEP]
apply (auto simp: fk fk' frechet_derivative_nth_derivative_commute[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0<..} (\<lambda>x. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at x) 1)
[PROOF STEP]
apply (subst continuous_on_cong[OF refl])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {0<..} \<Longrightarrow> frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at x) 1 = ?g9 x
 2. continuous_on {0<..} ?g9
[PROOF STEP]
apply (rule fk')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {0<..} \<Longrightarrow> 0 < x
 2. continuous_on {0<..} (\<lambda>x. rp x * (exp (- inverse x) / x ^ (2 * k + 2)))
[PROOF STEP]
by (auto intro!: continuous_intros p'1 p1 rp
        intro: continuous_on_real_polynomial_function)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {0<..} f (Suc k)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {0<..} f (Suc k)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
have "nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * (Suc k)) * exp (- inverse t)"
    if "t > 0" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * Suc k) * exp (- inverse t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * Suc k) * exp (- inverse t)
[PROOF STEP]
have "nth_derivative (Suc k) f t 1 = frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_derivative (Suc k) f t 1 = frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1
[PROOF STEP]
by (simp add: frechet_derivative_nth_derivative_commute)
[PROOF STATE]
proof (state)
this:
nth_derivative (Suc k) f t 1 = frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1

goal (1 subgoal):
 1. nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * Suc k) * exp (- inverse t)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nth_derivative (Suc k) f t 1 = frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1

goal (1 subgoal):
 1. nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * Suc k) * exp (- inverse t)
[PROOF STEP]
have "\<dots> = rp t / t^(2*k+2) * (exp (-inverse t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t / t ^ (2 * k + 2) * exp (- inverse t)
[PROOF STEP]
using fk'[OF \<open>t > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. nth_derivative k f x 1) differentiable at t
frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t * (exp (- inverse t) / t ^ (2 * k + 2))

goal (1 subgoal):
 1. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t / t ^ (2 * k + 2) * exp (- inverse t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = rp t / t ^ (2 * k + 2) * exp (- inverse t)

goal (1 subgoal):
 1. nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * Suc k) * exp (- inverse t)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * k + 2) * exp (- inverse t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * k + 2) * exp (- inverse t)

goal (1 subgoal):
 1. nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * Suc k) * exp (- inverse t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nth_derivative (Suc k) f t 1 = rp t / t ^ (2 * Suc k) * exp (- inverse t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?t \<Longrightarrow> nth_derivative (Suc k) f ?t 1 = rp ?t / ?t ^ (2 * Suc k) * exp (- inverse ?t)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {0<..} f k \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative k f t 1 = p t / t ^ (2 * k) * exp (- inverse t))) \<Longrightarrow> higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real_polynomial_function rp
higher_differentiable_on {0<..} f (Suc k)
0 < ?t \<Longrightarrow> nth_derivative (Suc k) f ?t 1 = rp ?t / ?t ^ (2 * Suc k) * exp (- inverse ?t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
real_polynomial_function rp
higher_differentiable_on {0<..} f (Suc k)
0 < ?t \<Longrightarrow> nth_derivative (Suc k) f ?t 1 = rp ?t / ?t ^ (2 * Suc k) * exp (- inverse ?t)

goal (1 subgoal):
 1. higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {0<..} f (Suc k) \<and> (\<exists>p. real_polynomial_function p \<and> (\<forall>t>0. nth_derivative (Suc k) f t 1 = p t / t ^ (2 * Suc k) * exp (- inverse t)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f_has_derivative_at_neg:
  " x < 0 \<Longrightarrow> (f has_derivative (\<lambda>x. 0)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < 0 \<Longrightarrow> (f has_derivative (\<lambda>x. 0)) (at x)
[PROOF STEP]
by (rule has_derivative_transform_within_open[where f="\<lambda>x. 0" and s="{..<0}"])
    (auto simp: f_def)


[STATEMENT]
lemma f_differentiable_at_neg:
  "x < 0 \<Longrightarrow> f differentiable at x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < 0 \<Longrightarrow> f differentiable at x
[PROOF STEP]
using f_has_derivative_at_neg
[PROOF STATE]
proof (prove)
using this:
?x < 0 \<Longrightarrow> (f has_derivative (\<lambda>x. 0)) (at ?x)

goal (1 subgoal):
 1. x < 0 \<Longrightarrow> f differentiable at x
[PROOF STEP]
by (auto simp: differentiable_def)


[STATEMENT]
lemma frechet_derivative_f_at_neg:
  "x \<in> {..<0} \<Longrightarrow> frechet_derivative f (at x) = (\<lambda>x. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {..<0} \<Longrightarrow> frechet_derivative f (at x) = (\<lambda>x. 0)
[PROOF STEP]
by (rule frechet_derivative_at') (rule f_has_derivative_at_neg, simp)


[STATEMENT]
lemma f_nth_derivative_lt_0:
  "higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0)
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. higher_differentiable_on {..<0} f 0 \<and> (\<forall>t<0. nth_derivative 0 f t 1 = 0)
 2. \<And>k. higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0) \<Longrightarrow> higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. higher_differentiable_on {..<0} f 0 \<and> (\<forall>t<0. nth_derivative 0 f t 1 = 0)
 2. \<And>k. higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0) \<Longrightarrow> higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
[PROOF STEP]
have rewr: "a \<in> {..<0} \<Longrightarrow> \<not>0 < a" for a::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {..<0} \<Longrightarrow> \<not> 0 < a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?a \<in> {..<0} \<Longrightarrow> \<not> 0 < ?a

goal (2 subgoals):
 1. higher_differentiable_on {..<0} f 0 \<and> (\<forall>t<0. nth_derivative 0 f t 1 = 0)
 2. \<And>k. higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0) \<Longrightarrow> higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on {..<0} f 0 \<and> (\<forall>t<0. nth_derivative 0 f t 1 = 0)
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps f_def rewr
        simp del: lessThan_iff
        cong: continuous_on_cong)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {..<0} f 0 \<and> (\<forall>t<0. nth_derivative 0 f t 1 = 0)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0) \<Longrightarrow> higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0) \<Longrightarrow> higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0)

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0) \<Longrightarrow> higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
[PROOF STEP]
have "t < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at t" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at t
[PROOF STEP]
by (rule differentiable_eqI[where g=0 and X="{..<0}"])
      (auto simp: zero_fun_def frechet_derivative_const Suc.IH)
[PROOF STATE]
proof (state)
this:
?t < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at ?t

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0) \<Longrightarrow> higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?t < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at ?t
[PROOF STEP]
have "frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = 0" if "t < 0" for t
[PROOF STATE]
proof (prove)
using this:
?t < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at ?t

goal (1 subgoal):
 1. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = 0
[PROOF STEP]
using that Suc.IH
[PROOF STATE]
proof (prove)
using this:
?t < 0 \<Longrightarrow> (\<lambda>x. nth_derivative k f x 1) differentiable at ?t
t < 0
higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0)

goal (1 subgoal):
 1. frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at t) 1 = 0
[PROOF STEP]
by (subst frechet_derivative_transform_within_open[where X="{..<0}" and g =0])
      (auto simp: frechet_derivative_zero_fun)
[PROOF STATE]
proof (state)
this:
?t < 0 \<Longrightarrow> frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at ?t) 1 = 0

goal (1 subgoal):
 1. \<And>k. higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0) \<Longrightarrow> higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0)
?t < 0 \<Longrightarrow> frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at ?t) 1 = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on {..<0} f k \<and> (\<forall>t<0. nth_derivative k f t 1 = 0)
?t < 0 \<Longrightarrow> frechet_derivative (\<lambda>x. nth_derivative k f x 1) (at ?t) 1 = 0

goal (1 subgoal):
 1. higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)
[PROOF STEP]
by (auto simp: higher_differentiable_on.simps f_differentiable_at_neg
        frechet_derivative_f_at_neg zero_fun_def
        simp flip: frechet_derivative_nth_derivative_commute
        simp del: lessThan_iff
        intro!: higher_differentiable_on_const
        cong: higher_differentiable_on_cong)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on {..<0} f (Suc k) \<and> (\<forall>t<0. nth_derivative (Suc k) f t 1 = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma netlimit_at_left: "netlimit (at_left x) = x" for x::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. netlimit (at_left x) = x
[PROOF STEP]
by (rule Lim_ident_at) simp


[STATEMENT]
lemma netlimit_at_right: "netlimit (at_right x) = x" for x::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. netlimit (at_right x) = x
[PROOF STEP]
by (rule Lim_ident_at) simp


[STATEMENT]
lemma has_derivative_split_at:
  "(g has_derivative g') (at x)"
  if
    "(g has_derivative g') (at_left x)"
    "(g has_derivative g') (at_right x)"
  for x::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g has_derivative g') (at x)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(g has_derivative g') (at_left x)
(g has_derivative g') (at_right x)

goal (1 subgoal):
 1. (g has_derivative g') (at x)
[PROOF STEP]
unfolding has_derivative_def netlimit_at netlimit_at_right netlimit_at_left
[PROOF STATE]
proof (prove)
using this:
bounded_linear g' \<and> ((\<lambda>y. (g y - g x - g' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> (0::'a)) (at_left x)
bounded_linear g' \<and> ((\<lambda>y. (g y - g x - g' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> (0::'a)) (at_right x)

goal (1 subgoal):
 1. bounded_linear g' \<and> (\<lambda>y. (g y - g x - g' (y - x)) /\<^sub>R norm (y - x)) \<midarrow>x\<rightarrow> (0::'a)
[PROOF STEP]
by (auto intro: filterlim_split_at)


[STATEMENT]
lemma has_derivative_at_left_at_right':
  "(g has_derivative g') (at x)"
  if
    "(g has_derivative g') (at x within {..x})"
    "(g has_derivative g') (at x within {x..})"
  for x::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g has_derivative g') (at x)
[PROOF STEP]
apply (rule has_derivative_split_at)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (g has_derivative g') (at_left x)
 2. (g has_derivative g') (at_right x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g has_derivative g') (at_left x)
[PROOF STEP]
by (rule has_derivative_subset) (fact, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g has_derivative g') (at_right x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g has_derivative g') (at_right x)
[PROOF STEP]
by (rule has_derivative_subset) (fact, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma real_polynomial_function_tendsto:
  "(p \<longlongrightarrow> p x) (at x within X)" if "real_polynomial_function p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<longlongrightarrow> p x) (at x within X)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
real_polynomial_function p

goal (1 subgoal):
 1. (p \<longlongrightarrow> p x) (at x within X)
[PROOF STEP]
by (induction p) (auto intro!: tendsto_eq_intros intro: bounded_linear.tendsto)