[STATEMENT]
lemma onorm_Sup_on_ball:
  includes notation_norm
  assumes \<open>r > 0\<close>
  shows "\<parallel>f\<parallel> \<le> Sup ( (\<lambda>x. \<parallel>f *\<^sub>v x\<parallel>) ` (ball x r) ) / r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
text \<open>
  Explanation: Let \<^term>\<open>f\<close> be a bounded operator and let \<^term>\<open>x\<close> be a point. For any \<^term>\<open>r > 0\<close>,
  the operator norm of \<^term>\<open>f\<close> is bounded above by the supremum of $f$ applied to the open ball of
  radius \<^term>\<open>r\<close> around \<^term>\<open>x\<close>, divided by \<^term>\<open>r\<close>.
\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have bdd_above_3: \<open>bdd_above ((\<lambda>x. \<parallel>f *\<^sub>v x\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>x. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bdd_above ((\<lambda>x. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
obtain M where \<open>\<And> \<xi>.  \<parallel>f *\<^sub>v \<xi>\<parallel> \<le> M * norm \<xi>\<close> and \<open>M \<ge> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>M. \<lbrakk>\<And>\<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel> \<le> M * \<parallel>\<xi>\<parallel>; 0 \<le> M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using norm_blinfun norm_ge_zero
[PROOF STATE]
proof (prove)
using this:
\<parallel>?f *\<^sub>v ?x\<parallel> \<le> \<parallel>?f\<parallel> * \<parallel>?x\<parallel>
0 \<le> \<parallel>?x\<parallel>

goal (1 subgoal):
 1. (\<And>M. \<lbrakk>\<And>\<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel> \<le> M * \<parallel>\<xi>\<parallel>; 0 \<le> M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<parallel>f *\<^sub>v ?\<xi>\<parallel> \<le> M * \<parallel>?\<xi>\<parallel>
0 \<le> M

goal (1 subgoal):
 1. bdd_above ((\<lambda>x. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
hence \<open>\<And> \<xi>. \<xi> \<in> ball 0 r \<Longrightarrow> \<parallel>f *\<^sub>v \<xi>\<parallel> \<le> M * r\<close>
[PROOF STATE]
proof (prove)
using this:
\<parallel>f *\<^sub>v ?\<xi>\<parallel> \<le> M * \<parallel>?\<xi>\<parallel>
0 \<le> M

goal (1 subgoal):
 1. \<And>\<xi>. \<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v \<xi>\<parallel> \<le> M * r
[PROOF STEP]
using \<open>r > 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<parallel>f *\<^sub>v ?\<xi>\<parallel> \<le> M * \<parallel>?\<xi>\<parallel>
0 \<le> M
0 < r

goal (1 subgoal):
 1. \<And>\<xi>. \<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v \<xi>\<parallel> \<le> M * r
[PROOF STEP]
by (smt mem_ball_0 mult_left_mono)
[PROOF STATE]
proof (state)
this:
?\<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v ?\<xi>\<parallel> \<le> M * r

goal (1 subgoal):
 1. bdd_above ((\<lambda>x. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v ?\<xi>\<parallel> \<le> M * r

goal (1 subgoal):
 1. bdd_above ((\<lambda>x. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by (meson bdd_aboveI2)
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>x. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::'a) r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>x. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have bdd_above_2: \<open>bdd_above ((\<lambda> \<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
have \<open>bdd_above ((\<lambda> \<xi>. \<parallel>f *\<^sub>v x\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::'c) r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::?'c1) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::?'c1) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
have \<open>bdd_above ((\<lambda> \<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
using bdd_above_3
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>x. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::?'c1) r)
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
have \<open>bdd_above ((\<lambda> \<xi>. \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v x\<parallel>) ` ball (0::?'c1) r)
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by (rule bdd_above_plus)
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
obtain M where \<open>\<And> \<xi>. \<xi> \<in> ball 0 r \<Longrightarrow> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel> \<le> M\<close>
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. (\<And>M. (\<And>\<xi>. \<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel> \<le> M) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding bdd_above_def
[PROOF STATE]
proof (prove)
using this:
\<exists>M. \<forall>x\<in>(\<lambda>\<xi>. \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel>) ` ball (0::'a) r. x \<le> M

goal (1 subgoal):
 1. (\<And>M. (\<And>\<xi>. \<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel> \<le> M) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson image_eqI)
[PROOF STATE]
proof (state)
this:
?\<xi>1 \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v ?\<xi>1\<parallel> \<le> M

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<xi>1 \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v ?\<xi>1\<parallel> \<le> M

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
have \<open>\<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel>\<close> for \<xi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
by (simp add: blinfun.add_right norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
\<parallel>f *\<^sub>v (x + ?\<xi>1)\<parallel> \<le> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v ?\<xi>1\<parallel>

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<xi>1 \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v ?\<xi>1\<parallel> \<le> M
\<parallel>f *\<^sub>v (x + ?\<xi>1)\<parallel> \<le> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v ?\<xi>1\<parallel>
[PROOF STEP]
have \<open>\<And> \<xi>. \<xi> \<in> ball 0 r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> M\<close>
[PROOF STATE]
proof (prove)
using this:
?\<xi>1 \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v ?\<xi>1\<parallel> \<le> M
\<parallel>f *\<^sub>v (x + ?\<xi>1)\<parallel> \<le> \<parallel>f *\<^sub>v x\<parallel> + \<parallel>f *\<^sub>v ?\<xi>1\<parallel>

goal (1 subgoal):
 1. \<And>\<xi>. \<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> M
[PROOF STEP]
by (simp add: blinfun.add_right norm_triangle_le)
[PROOF STATE]
proof (state)
this:
?\<xi>1 \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v (x + ?\<xi>1)\<parallel> \<le> M

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<xi>1 \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v (x + ?\<xi>1)\<parallel> \<le> M

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by (meson bdd_aboveI2)
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have bdd_above_4: \<open>bdd_above ((\<lambda> \<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
obtain K where K_def: \<open>\<And> \<xi>. \<xi> \<in> ball 0 r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> K\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>K. (\<And>\<xi>. \<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> K) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using  \<open>bdd_above ((\<lambda> \<xi>. norm (f (x + \<xi>))) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. (\<And>K. (\<And>\<xi>. \<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> K) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding bdd_above_def
[PROOF STATE]
proof (prove)
using this:
\<exists>M. \<forall>x\<in>(\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r. x \<le> M

goal (1 subgoal):
 1. (\<And>K. (\<And>\<xi>. \<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> K) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson image_eqI)
[PROOF STATE]
proof (state)
this:
?\<xi> \<in> ball (0::'a) r \<Longrightarrow> \<parallel>f *\<^sub>v (x + ?\<xi>)\<parallel> \<le> K

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
have \<open>\<xi> \<in> ball (0::'a) r \<Longrightarrow> -\<xi> \<in> ball 0 r\<close> for \<xi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<xi> \<in> ball (0::'a) r \<Longrightarrow> - \<xi> \<in> ball (0::'a) r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?\<xi> \<in> ball (0::'a) r \<Longrightarrow> - ?\<xi> \<in> ball (0::'a) r

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<xi> \<in> ball (0::'a) r \<Longrightarrow> - ?\<xi> \<in> ball (0::'a) r

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by (metis K_def ab_group_add_class.ab_diff_conv_add_uminus bdd_aboveI2)
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have bdd_above_1: \<open>bdd_above ((\<lambda> \<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>  \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
have \<open>bdd_above ((\<lambda> \<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
using bdd_above_2
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
have \<open>bdd_above ((\<lambda> \<xi>.  \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
using bdd_above_4
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
unfolding max_def
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. if \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> then \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> else \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r); bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)\<rbrakk> \<Longrightarrow> bdd_above ((\<lambda>xa. \<parallel>f *\<^sub>v (x - xa)\<parallel>) ` (ball (0::'a) r \<inter> {\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>}))
 2. \<lbrakk>bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r); bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)\<rbrakk> \<Longrightarrow> bdd_above ((\<lambda>xa. \<parallel>f *\<^sub>v (x + xa)\<parallel>) ` (ball (0::'a) r \<inter> {\<xi>. \<not> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>}))
[PROOF STEP]
apply (meson bdd_above_Int1 bdd_above_mono image_Int_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r); bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)\<rbrakk> \<Longrightarrow> bdd_above ((\<lambda>xa. \<parallel>f *\<^sub>v (x + xa)\<parallel>) ` (ball (0::'a) r \<inter> {\<xi>. \<not> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<le> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>}))
[PROOF STEP]
by (meson bdd_above_Int1 bdd_above_mono image_Int_subset)
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have bdd_above_6: \<open>bdd_above ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bdd_above ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)
[PROOF STEP]
have \<open>bounded (ball x r)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded (ball x r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bounded (ball x r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)
[PROOF STEP]
hence \<open>bounded ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)\<close>
[PROOF STATE]
proof (prove)
using this:
bounded (ball x r)

goal (1 subgoal):
 1. bounded ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)
[PROOF STEP]
by (metis (no_types) add.left_neutral bdd_above_2 bdd_above_norm bounded_norm_comp
          image_add_ball image_image)
[PROOF STATE]
proof (state)
this:
bounded ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bounded ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)
[PROOF STEP]
by (simp add: bounded_imp_bdd_above)
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have norm_1: \<open>(\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball 0 r = (\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r = (\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r
[PROOF STEP]
by (metis add.right_neutral ball_translation image_image)
[PROOF STATE]
proof (state)
this:
(\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r = (\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have bdd_above_5: \<open>bdd_above ((\<lambda>\<xi>. norm (f (x + \<xi>))) ` ball 0 r)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by (simp add: bdd_above_2)
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have norm_2: \<open>\<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball 0 r\<close> for \<xi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
assume \<open>\<parallel>\<xi>\<parallel> < r\<close>
[PROOF STATE]
proof (state)
this:
\<parallel>\<xi>\<parallel> < r

goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
hence \<open>\<xi> \<in> ball (0::'a) r\<close>
[PROOF STATE]
proof (prove)
using this:
\<parallel>\<xi>\<parallel> < r

goal (1 subgoal):
 1. \<xi> \<in> ball (0::'a) r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<xi> \<in> ball (0::'a) r

goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
hence \<open>-\<xi> \<in> ball (0::'a) r\<close>
[PROOF STATE]
proof (prove)
using this:
\<xi> \<in> ball (0::'a) r

goal (1 subgoal):
 1. - \<xi> \<in> ball (0::'a) r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- \<xi> \<in> ball (0::'a) r

goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
- \<xi> \<in> ball (0::'a) r

goal (1 subgoal):
 1. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
by (metis (no_types, lifting) ab_group_add_class.ab_diff_conv_add_uminus image_iff)
[PROOF STATE]
proof (state)
this:
\<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<parallel>?\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - ?\<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have norm_2': \<open>\<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball 0 r\<close> for \<xi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
assume \<open>norm \<xi> < r\<close>
[PROOF STATE]
proof (state)
this:
\<parallel>\<xi>\<parallel> < r

goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
hence \<open>\<xi> \<in> ball (0::'a) r\<close>
[PROOF STATE]
proof (prove)
using this:
\<parallel>\<xi>\<parallel> < r

goal (1 subgoal):
 1. \<xi> \<in> ball (0::'a) r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<xi> \<in> ball (0::'a) r

goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
hence \<open>-\<xi> \<in> ball (0::'a) r\<close>
[PROOF STATE]
proof (prove)
using this:
\<xi> \<in> ball (0::'a) r

goal (1 subgoal):
 1. - \<xi> \<in> ball (0::'a) r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- \<xi> \<in> ball (0::'a) r

goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
- \<xi> \<in> ball (0::'a) r

goal (1 subgoal):
 1. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
by (metis (no_types, lifting) diff_minus_eq_add image_iff)
[PROOF STATE]
proof (state)
this:
\<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<parallel>?\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + ?\<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have bdd_above_6: \<open>bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball 0 r)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by (simp add: bdd_above_4)
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have Sup_2: \<open>(SUP \<xi>\<in>ball 0 r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) =
                 max (SUP \<xi>\<in>ball 0 r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball 0 r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
have \<open>ball (0::'a) r \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ball (0::'a) r \<noteq> {}
[PROOF STEP]
using \<open>r > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r

goal (1 subgoal):
 1. ball (0::'a) r \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ball (0::'a) r \<noteq> {}

goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ball (0::'a) r \<noteq> {}

goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
have \<open>bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball 0 r)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
using bdd_above_5
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
have \<open>bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball 0 r)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
using bdd_above_6
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ball (0::'a) r \<noteq> {}
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ball (0::'a) r \<noteq> {}
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
using max_Sup
[PROOF STATE]
proof (prove)
using this:
ball (0::'a) r \<noteq> {}
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r)
bdd_above ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
\<lbrakk>?X \<noteq> {}; bdd_above (?f ` ?X); bdd_above (?g ` ?X)\<rbrakk> \<Longrightarrow> Sup (pointwise_max ?f ?g ` ?X) = max (Sup (?f ` ?X)) (Sup (?g ` ?X))

goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
by (metis (mono_tags, lifting) Banach_Steinhaus_Missing.pointwise_max_def image_cong)
[PROOF STATE]
proof (state)
this:
(SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have Sup_3': \<open>\<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball 0 r\<close> for \<xi>::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
by (simp add: norm_2')
[PROOF STATE]
proof (state)
this:
\<parallel>?\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + ?\<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have Sup_3'': \<open>\<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball 0 r\<close> for \<xi>::'a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
by (simp add: norm_2)
[PROOF STATE]
proof (state)
this:
\<parallel>?\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - ?\<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have Sup_3: \<open>max (SUP \<xi>\<in>ball 0 r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball 0 r.  \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) =
        (SUP \<xi>\<in>ball 0 r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)
[PROOF STEP]
have \<open>(\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` (ball 0 r) = (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` (ball 0 r)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r = (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<xi>. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r
 2. \<And>\<xi>. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
using Sup_3'
[PROOF STATE]
proof (prove)
using this:
\<parallel>?\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + ?\<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r

goal (2 subgoals):
 1. \<And>\<xi>. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r
 2. \<And>\<xi>. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<xi>. \<lbrakk>\<parallel>\<xi>\<parallel> < r; \<And>\<xi>. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r\<rbrakk> \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
using Sup_3''
[PROOF STATE]
proof (prove)
using this:
\<parallel>?\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x - ?\<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r

goal (1 subgoal):
 1. \<And>\<xi>. \<lbrakk>\<parallel>\<xi>\<parallel> < r; \<And>\<xi>. \<parallel>\<xi>\<parallel> < r \<Longrightarrow> \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r\<rbrakk> \<Longrightarrow> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel> \<in> (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r = (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r

goal (1 subgoal):
 1. max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)
[PROOF STEP]
hence \<open>Sup ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` (ball 0 r))=Sup ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` ball (0::'a) r = (\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r

goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)

goal (1 subgoal):
 1. max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)

goal (1 subgoal):
 1. max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have Sup_1: \<open>Sup ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` (ball 0 r)) \<le> Sup ( (\<lambda>\<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel>) ` (ball x r) )\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
have \<open>(\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) \<xi> \<le> max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>\<close> for \<xi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f *\<^sub>v \<xi>\<parallel> \<le> max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>
[PROOF STEP]
apply(rule linear_plus_norm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear ((*\<^sub>v) f)
[PROOF STEP]
apply (rule bounded_linear.linear)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_linear ((*\<^sub>v) f)
[PROOF STEP]
by (simp add: blinfun.bounded_linear_right)
[PROOF STATE]
proof (state)
this:
\<parallel>f *\<^sub>v ?\<xi>\<parallel> \<le> max \<parallel>f *\<^sub>v (x + ?\<xi>)\<parallel> \<parallel>f *\<^sub>v (x - ?\<xi>)\<parallel>

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<parallel>f *\<^sub>v ?\<xi>\<parallel> \<le> max \<parallel>f *\<^sub>v (x + ?\<xi>)\<parallel> \<parallel>f *\<^sub>v (x - ?\<xi>)\<parallel>

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
have \<open>bdd_above ((\<lambda> \<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>  \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
using bdd_above_1
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
have \<open>ball (0::'a) r \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ball (0::'a) r \<noteq> {}
[PROOF STEP]
using \<open>r > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r

goal (1 subgoal):
 1. ball (0::'a) r \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ball (0::'a) r \<noteq> {}

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<parallel>f *\<^sub>v ?\<xi>\<parallel> \<le> max \<parallel>f *\<^sub>v (x + ?\<xi>)\<parallel> \<parallel>f *\<^sub>v (x - ?\<xi>)\<parallel>
bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
ball (0::'a) r \<noteq> {}
[PROOF STEP]
have \<open>Sup ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` (ball 0 r)) \<le>
                     Sup ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
using this:
\<parallel>f *\<^sub>v ?\<xi>\<parallel> \<le> max \<parallel>f *\<^sub>v (x + ?\<xi>)\<parallel> \<parallel>f *\<^sub>v (x - ?\<xi>)\<parallel>
bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
ball (0::'a) r \<noteq> {}

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
using cSUP_mono
[PROOF STATE]
proof (prove)
using this:
\<parallel>f *\<^sub>v ?\<xi>\<parallel> \<le> max \<parallel>f *\<^sub>v (x + ?\<xi>)\<parallel> \<parallel>f *\<^sub>v (x - ?\<xi>)\<parallel>
bdd_above ((\<lambda>\<xi>. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` ball (0::'a) r)
ball (0::'a) r \<noteq> {}
\<lbrakk>?A \<noteq> {}; bdd_above (?g ` ?B); \<And>n. n \<in> ?A \<Longrightarrow> \<exists>m\<in>?B. ?f n \<le> ?g m\<rbrakk> \<Longrightarrow> Sup (?f ` ?A) \<le> Sup (?g ` ?B)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
(SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
have \<open>\<dots> = max (Sup ((\<lambda>\<xi>.  \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` (ball 0 r)))
                        (Sup ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) ` (ball 0 r)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
using Sup_2
[PROOF STATE]
proof (prove)
using this:
(SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)

goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(SUP \<xi>\<in>ball (0::'a) r. max \<parallel>f *\<^sub>v (x + \<xi>)\<parallel> \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
have \<open>\<dots> = Sup ((\<lambda>\<xi>. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) ` (ball 0 r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)
[PROOF STEP]
using Sup_3
[PROOF STATE]
proof (prove)
using this:
max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)

goal (1 subgoal):
 1. max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
max (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x - \<xi>)\<parallel>) = (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
have \<open>\<dots> = Sup ((\<lambda>\<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel>) ` (ball x r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) = (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
by (metis  add.right_neutral ball_translation image_image)
[PROOF STATE]
proof (state)
this:
(SUP \<xi>\<in>ball (0::'a) r. \<parallel>f *\<^sub>v (x + \<xi>)\<parallel>) = (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have \<open>\<parallel>f\<parallel> = (SUP x\<in>ball 0 r. \<parallel>f *\<^sub>v x\<parallel>) / r\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel> = (SUP x\<in>ball (0::'a) r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
using \<open>0 < r\<close> onorm_r
[PROOF STATE]
proof (prove)
using this:
0 < r
0 < ?r \<Longrightarrow> \<parallel>?f\<parallel> = (SUP x\<in>ball (0::?'a) ?r. \<parallel>?f *\<^sub>v x\<parallel>) / ?r

goal (1 subgoal):
 1. \<parallel>f\<parallel> = (SUP x\<in>ball (0::'a) r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<parallel>f\<parallel> = (SUP x\<in>ball (0::'a) r. \<parallel>f *\<^sub>v x\<parallel>) / r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<parallel>f\<parallel> = (SUP x\<in>ball (0::'a) r. \<parallel>f *\<^sub>v x\<parallel>) / r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
have \<open>Sup ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` (ball 0 r)) / r \<le> Sup ((\<lambda>\<xi>. \<parallel>f *\<^sub>v \<xi>\<parallel>) ` (ball x r)) / r\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) / r \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>) / r
[PROOF STEP]
using Sup_1 \<open>0 < r\<close> divide_right_mono
[PROOF STATE]
proof (prove)
using this:
(SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
0 < r
\<lbrakk>?a \<le> ?b; (0::?'a) \<le> ?c\<rbrakk> \<Longrightarrow> ?a / ?c \<le> ?b / ?c

goal (1 subgoal):
 1. (SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) / r \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>) / r
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) / r \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>) / r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<parallel>f\<parallel> = (SUP x\<in>ball (0::'a) r. \<parallel>f *\<^sub>v x\<parallel>) / r
(SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) / r \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>) / r
[PROOF STEP]
have \<open>\<parallel>f\<parallel> \<le> Sup ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r) / r\<close>
[PROOF STATE]
proof (prove)
using this:
\<parallel>f\<parallel> = (SUP x\<in>ball (0::'a) r. \<parallel>f *\<^sub>v x\<parallel>) / r
(SUP t\<in>ball (0::'a) r. \<parallel>f *\<^sub>v t\<parallel>) / r \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>) / r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP t\<in>ball x r. \<parallel>f *\<^sub>v t\<parallel>) / r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>f\<parallel> \<le> (SUP t\<in>ball x r. \<parallel>f *\<^sub>v t\<parallel>) / r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<parallel>f\<parallel> \<le> (SUP t\<in>ball x r. \<parallel>f *\<^sub>v t\<parallel>) / r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>f\<parallel> \<le> (SUP x\<in>ball x r. \<parallel>f *\<^sub>v x\<parallel>) / r

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma onorm_Sup_on_ball':
  includes notation_norm
  assumes \<open>r > 0\<close> and \<open>\<tau> < 1\<close>
  shows \<open>\<exists>\<xi>\<in>ball x r.  \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
text \<open>
  In the proof of Banach-Steinhaus theorem, we will use this variation of the
  lemma @{text onorm_Sup_on_ball}.

  Explanation: Let \<^term>\<open>f\<close> be a bounded operator, let \<^term>\<open>x\<close> be a point and let \<^term>\<open>r\<close> be a
  positive real number. For any real number \<^term>\<open>\<tau> < 1\<close>, there is a point \<^term>\<open>\<xi>\<close> in the open ball
  of radius \<^term>\<open>r\<close> around \<^term>\<open>x\<close> such that \<^term>\<open>\<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>\<close>.
\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
proof(cases  \<open>f = 0\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f = 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
 2. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f = 0

goal (2 subgoals):
 1. f = 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
 2. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f = 0

goal (1 subgoal):
 1. \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
by (metis assms(1) centre_in_ball mult_zero_right norm_zero order_refl
        zero_blinfun.rep_eq)
[PROOF STATE]
proof (state)
this:
\<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f \<noteq> 0

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
have bdd_above_1: \<open>bdd_above ((\<lambda>t. \<parallel>(*\<^sub>v) f t\<parallel>) ` ball x r)\<close> for f::\<open>'a \<Rightarrow>\<^sub>L 'b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)
[PROOF STEP]
using assms(1) bounded_linear_image
[PROOF STATE]
proof (prove)
using this:
0 < r
\<lbrakk>bounded ?S; bounded_linear ?f\<rbrakk> \<Longrightarrow> bounded (?f ` ?S)

goal (1 subgoal):
 1. bdd_above ((\<lambda>t. \<parallel>f *\<^sub>v t\<parallel>) ` ball x r)
[PROOF STEP]
by (simp add: bounded_linear_image
        blinfun.bounded_linear_right bounded_imp_bdd_above bounded_norm_comp)
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>t. \<parallel>?f *\<^sub>v t\<parallel>) ` ball x r)

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
have  \<open>norm f > 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<parallel>f\<parallel>
[PROOF STEP]
using \<open>f \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0

goal (1 subgoal):
 1. 0 < \<parallel>f\<parallel>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < \<parallel>f\<parallel>

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
have \<open>norm f \<le>  Sup ( (\<lambda>\<xi>.  \<parallel>(*\<^sub>v) f \<xi>\<parallel>) ` (ball x r) ) / r\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>) / r
[PROOF STEP]
using \<open>r > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r

goal (1 subgoal):
 1. \<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>) / r
[PROOF STEP]
by (simp add: onorm_Sup_on_ball)
[PROOF STATE]
proof (state)
this:
\<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>) / r

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
hence \<open>r * norm f \<le>  Sup ( (\<lambda>\<xi>.  \<parallel>(*\<^sub>v) f \<xi>\<parallel>) ` (ball x r) )\<close>
[PROOF STATE]
proof (prove)
using this:
\<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>) / r

goal (1 subgoal):
 1. r * \<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
using \<open>0 < r\<close>
[PROOF STATE]
proof (prove)
using this:
\<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>) / r
0 < r

goal (1 subgoal):
 1. r * \<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
[PROOF STEP]
by (smt divide_strict_right_mono nonzero_mult_div_cancel_left)
[PROOF STATE]
proof (state)
this:
r * \<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r * \<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
have \<open>\<tau> * r * norm f < r * norm f\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> * r * \<parallel>f\<parallel> < r * \<parallel>f\<parallel>
[PROOF STEP]
using  \<open>\<tau> < 1\<close>
[PROOF STATE]
proof (prove)
using this:
\<tau> < 1

goal (1 subgoal):
 1. \<tau> * r * \<parallel>f\<parallel> < r * \<parallel>f\<parallel>
[PROOF STEP]
using \<open>0 < norm f\<close> \<open>0 < r\<close>
[PROOF STATE]
proof (prove)
using this:
\<tau> < 1
0 < \<parallel>f\<parallel>
0 < r

goal (1 subgoal):
 1. \<tau> * r * \<parallel>f\<parallel> < r * \<parallel>f\<parallel>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau> * r * \<parallel>f\<parallel> < r * \<parallel>f\<parallel>

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r * \<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
\<tau> * r * \<parallel>f\<parallel> < r * \<parallel>f\<parallel>
[PROOF STEP]
have \<open>\<tau> * r * norm f < Sup ( (norm \<circ> ((*\<^sub>v) f)) ` (ball x r) )\<close>
[PROOF STATE]
proof (prove)
using this:
r * \<parallel>f\<parallel> \<le> (SUP \<xi>\<in>ball x r. \<parallel>f *\<^sub>v \<xi>\<parallel>)
\<tau> * r * \<parallel>f\<parallel> < r * \<parallel>f\<parallel>

goal (1 subgoal):
 1. \<tau> * r * \<parallel>f\<parallel> < Sup ((norm \<circ> (*\<^sub>v) f) ` ball x r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<tau> * r * \<parallel>f\<parallel> < Sup ((norm \<circ> (*\<^sub>v) f) ` ball x r)

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<tau> * r * \<parallel>f\<parallel> < Sup ((norm \<circ> (*\<^sub>v) f) ` ball x r)

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
have \<open>(norm \<circ> ( (*\<^sub>v) f)) ` (ball x r) \<noteq> {}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (norm \<circ> (*\<^sub>v) f) ` ball x r \<noteq> {}
[PROOF STEP]
using \<open>0 < r\<close>
[PROOF STATE]
proof (prove)
using this:
0 < r

goal (1 subgoal):
 1. (norm \<circ> (*\<^sub>v) f) ` ball x r \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(norm \<circ> (*\<^sub>v) f) ` ball x r \<noteq> {}

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(norm \<circ> (*\<^sub>v) f) ` ball x r \<noteq> {}

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
have \<open>bdd_above ((norm \<circ> ( (*\<^sub>v) f)) ` (ball x r))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((norm \<circ> (*\<^sub>v) f) ` ball x r)
[PROOF STEP]
using bdd_above_1
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>t. \<parallel>?f *\<^sub>v t\<parallel>) ` ball x r)

goal (1 subgoal):
 1. bdd_above ((norm \<circ> (*\<^sub>v) f) ` ball x r)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x r f. \<lbrakk>\<And>f. bounded_linear f \<Longrightarrow> bdd_above ((\<lambda>t. \<parallel>f t\<parallel>) ` ball x r); bounded_linear f\<rbrakk> \<Longrightarrow> bdd_above ((norm \<circ> f) ` ball x r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bdd_above ((norm \<circ> (*\<^sub>v) f) ` ball x r)

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<tau> * r * \<parallel>f\<parallel> < Sup ((norm \<circ> (*\<^sub>v) f) ` ball x r)
(norm \<circ> (*\<^sub>v) f) ` ball x r \<noteq> {}
bdd_above ((norm \<circ> (*\<^sub>v) f) ` ball x r)
[PROOF STEP]
have \<open>\<exists>t \<in> (norm \<circ> ( (*\<^sub>v) f)) ` (ball x r). \<tau> * r * norm f < t\<close>
[PROOF STATE]
proof (prove)
using this:
\<tau> * r * \<parallel>f\<parallel> < Sup ((norm \<circ> (*\<^sub>v) f) ` ball x r)
(norm \<circ> (*\<^sub>v) f) ` ball x r \<noteq> {}
bdd_above ((norm \<circ> (*\<^sub>v) f) ` ball x r)

goal (1 subgoal):
 1. \<exists>t\<in>(norm \<circ> (*\<^sub>v) f) ` ball x r. \<tau> * r * \<parallel>f\<parallel> < t
[PROOF STEP]
by (simp add: less_cSup_iff)
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>(norm \<circ> (*\<^sub>v) f) ` ball x r. \<tau> * r * \<parallel>f\<parallel> < t

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>t\<in>(norm \<circ> (*\<^sub>v) f) ` ball x r. \<tau> * r * \<parallel>f\<parallel> < t

goal (1 subgoal):
 1. \<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>
[PROOF STEP]
by (smt comp_def image_iff)
[PROOF STATE]
proof (state)
this:
\<exists>\<xi>\<in>ball x r. \<tau> * r * \<parallel>f\<parallel> \<le> \<parallel>f *\<^sub>v \<xi>\<parallel>

goal:
No subgoals!
[PROOF STEP]
qed