[STATEMENT]
lemma (in grid) error_accumulation:
  fixes x::"(nat \<Rightarrow> real) \<Rightarrow> nat \<Rightarrow> 'a::euclidean_space"
  assumes max_step: "max_stepsize j \<le>
    root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))"
  defines "K \<equiv> {(s, y). \<exists>i \<le> j. s = t i \<and> y \<in> cball (x t i) r}"
  assumes "p > 0"
  assumes lipschitz: "\<And>j. t (Suc j) \<le> T \<Longrightarrow>
  dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar> \<Longrightarrow>
  dist (\<psi> (stepsize j) (t j) (x t j))
     (\<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))
    \<le> L * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)" and "L \<ge> 0"
  assumes consistence_error: "\<And>j. t (Suc j) \<le> T \<Longrightarrow>
    dist (x t (Suc j)) (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) \<le>
    B * stepsize j ^ (p + 1)" and "B \<ge> 0"
  assumes initial_error: "dist (x t 0) x0 \<le>
    B * (exp 1 - 1) * stepsize 0 ^ p / L"
  assumes "t j \<le> T"
  shows "dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le>
    B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
using \<open>t j \<le> T\<close> max_step
[PROOF STATE]
proof (prove)
using this:
t j \<le> T
max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))

goal (1 subgoal):
 1. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
proof (induct j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>t 0 \<le> T; max_stepsize 0 \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t 0) (grid_function (discrete_evolution \<psi>) x0 t 0) \<le> B / L * (exp (L * (t 0 - t 0) + 1) - 1) * max_stepsize 0 ^ p
 2. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
t 0 \<le> T
max_stepsize 0 \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))

goal (2 subgoals):
 1. \<lbrakk>t 0 \<le> T; max_stepsize 0 \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t 0) (grid_function (discrete_evolution \<psi>) x0 t 0) \<le> B / L * (exp (L * (t 0 - t 0) + 1) - 1) * max_stepsize 0 ^ p
 2. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
note initial_error
[PROOF STATE]
proof (state)
this:
dist (x t 0) x0 \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L

goal (2 subgoals):
 1. \<lbrakk>t 0 \<le> T; max_stepsize 0 \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t 0) (grid_function (discrete_evolution \<psi>) x0 t 0) \<le> B / L * (exp (L * (t 0 - t 0) + 1) - 1) * max_stepsize 0 ^ p
 2. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x t 0) x0 \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L

goal (2 subgoals):
 1. \<lbrakk>t 0 \<le> T; max_stepsize 0 \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t 0) (grid_function (discrete_evolution \<psi>) x0 t 0) \<le> B / L * (exp (L * (t 0 - t 0) + 1) - 1) * max_stepsize 0 ^ p
 2. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "B * (exp 1 - 1) * stepsize 0 ^ p / L \<le>
    B * (exp 1 - 1) * max_stepsize 0 ^ p / L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B * (exp 1 - 1) * stepsize 0 ^ p / L \<le> B * (exp 1 - 1) * max_stepsize 0 ^ p / L
[PROOF STEP]
using grid_stepsize_nonneg \<open>B\<ge>0\<close> \<open>L\<ge>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> stepsize ?j
0 \<le> B
0 \<le> L

goal (1 subgoal):
 1. B * (exp 1 - 1) * stepsize 0 ^ p / L \<le> B * (exp 1 - 1) * max_stepsize 0 ^ p / L
[PROOF STEP]
by (auto intro!: max_stepsize_ge_stepsize power_mono mult_left_mono divide_right_mono)
[PROOF STATE]
proof (state)
this:
B * (exp 1 - 1) * stepsize 0 ^ p / L \<le> B * (exp 1 - 1) * max_stepsize 0 ^ p / L

goal (2 subgoals):
 1. \<lbrakk>t 0 \<le> T; max_stepsize 0 \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t 0) (grid_function (discrete_evolution \<psi>) x0 t 0) \<le> B / L * (exp (L * (t 0 - t 0) + 1) - 1) * max_stepsize 0 ^ p
 2. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (x t 0) x0 \<le> B * (exp 1 - 1) * max_stepsize 0 ^ p / L
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
dist (x t 0) x0 \<le> B * (exp 1 - 1) * max_stepsize 0 ^ p / L

goal (1 subgoal):
 1. dist (x t 0) (grid_function (discrete_evolution \<psi>) x0 t 0) \<le> B / L * (exp (L * (t 0 - t 0) + 1) - 1) * max_stepsize 0 ^ p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (x t 0) (grid_function (discrete_evolution \<psi>) x0 t 0) \<le> B / L * (exp (L * (t 0 - t 0) + 1) - 1) * max_stepsize 0 ^ p

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
case (Suc j)
[PROOF STATE]
proof (state)
this:
\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
t (Suc j) \<le> T
max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "t 0 \<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t 0 \<le> T
[PROOF STEP]
using Suc grid_interval_notempty[of "Suc j"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
t (Suc j) \<le> T
max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))
t 0 \<le> t (Suc j)

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
t (Suc j) \<le> T
max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))
[PROOF STEP]
have j_in:"t j \<le> T"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
t (Suc j) \<le> T
max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))

goal (1 subgoal):
 1. t j \<le> T
[PROOF STEP]
using grid_mono[of j "Suc j"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
t (Suc j) \<le> T
max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))
j \<le> Suc j \<Longrightarrow> t j \<le> t (Suc j)

goal (1 subgoal):
 1. t j \<le> T
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t j \<le> T

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t j \<le> T

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "max_stepsize j \<le> max_stepsize (Suc j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_stepsize j \<le> max_stepsize (Suc j)
[PROOF STEP]
by (simp add: max_stepsize_mono)
[PROOF STATE]
proof (state)
this:
max_stepsize j \<le> max_stepsize (Suc j)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
t (Suc j) \<le> T
max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))
max_stepsize j \<le> max_stepsize (Suc j)
[PROOF STEP]
have IH1: "max_stepsize j \<le>
    root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
t (Suc j) \<le> T
max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))
max_stepsize j \<le> max_stepsize (Suc j)

goal (1 subgoal):
 1. max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t j \<le> T
max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))
[PROOF STEP]
have
    IH2: "dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)
     \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
using this:
t j \<le> T
max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))

goal (1 subgoal):
 1. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by (rule Suc(1))
[PROOF STATE]
proof (state)
this:
dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) =
    norm (x t (Suc j) -
    (discrete_evolution \<psi>) (t (Suc j)) (t j) (x t j) +
    ((discrete_evolution \<psi>) (t (Suc j)) (t j) (x t j) -
    (discrete_evolution \<psi>) (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) = norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) + (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))
[PROOF STEP]
by (simp add: field_simps dist_norm)
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) = norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) + (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) = norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) + (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "... \<le> norm (x t (Suc j) -
    (discrete_evolution \<psi>) (t (Suc j)) (t j) (x t j)) +
    norm (((discrete_evolution \<psi>) (t (Suc j)) (t j) (x t j) -
    (discrete_evolution \<psi>) (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))"
    (is "_ \<le> _ + ?ej")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) + (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + norm (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))
[PROOF STEP]
by (rule norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) + (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + norm (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) + (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + norm (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "?ej =
    norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j + stepsize j *\<^sub>R
    (\<psi> (stepsize j) (t j) (x t j) -
    \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)) = norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j + stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))
[PROOF STEP]
by (simp add: discrete_evolution_def stepsize_def algebra_simps)
[PROOF STATE]
proof (state)
this:
norm (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)) = norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j + stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j) - discrete_evolution \<psi> (t (Suc j)) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)) = norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j + stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "... \<le>
    norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + norm (stepsize j *\<^sub>R
    (\<psi> (stepsize j) (t j) (x t j) -
    \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j + stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))) \<le> norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + norm (stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))
[PROOF STEP]
by (rule norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j + stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))) \<le> norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + norm (stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j + stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))) \<le> norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + norm (stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "... = norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) +
    stepsize j *
    dist (\<psi> (stepsize j) (t j) (x t j))
    (\<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))"
    (is "_ = _ + _ * ?dj")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + norm (stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))) = norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * dist (\<psi> (stepsize j) (t j) (x t j)) (\<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))
[PROOF STEP]
using grid_stepsize_nonneg
[PROOF STATE]
proof (prove)
using this:
0 \<le> stepsize ?j

goal (1 subgoal):
 1. norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + norm (stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))) = norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * dist (\<psi> (stepsize j) (t j) (x t j)) (\<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))
[PROOF STEP]
by (simp add: dist_norm)
[PROOF STATE]
proof (state)
this:
norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + norm (stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))) = norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * dist (\<psi> (stepsize j) (t j) (x t j)) (\<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + norm (stepsize j *\<^sub>R (\<psi> (stepsize j) (t j) (x t j) - \<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))) = norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * dist (\<psi> (stepsize j) (t j) (x t j)) (\<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j))

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "?dj \<le> L * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (\<psi> (stepsize j) (t j) (x t j)) (\<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)) \<le> L * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)
[PROOF STEP]
proof (intro lipschitz(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t (Suc j) \<le> T
 2. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>
[PROOF STEP]
from IH2
[PROOF STATE]
proof (chain)
picking this:
dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have
      "dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)
      \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
using this:
dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p

goal (2 subgoals):
 1. t (Suc j) \<le> T
 2. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p

goal (2 subgoals):
 1. t (Suc j) \<le> T
 2. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>
[PROOF STEP]
have "... \<le>
      B / L * (exp (L * (T - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (T - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
using \<open>L\<ge>0\<close> \<open>B\<ge>0\<close> \<open>t j \<le> T\<close> max_stepsize_nonneg
[PROOF STATE]
proof (prove)
using this:
0 \<le> L
0 \<le> B
t j \<le> T
0 \<le> max_stepsize ?n

goal (1 subgoal):
 1. B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (T - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by (auto intro!: mult_left_mono mult_right_mono divide_right_mono)
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (T - t 0) + 1) - 1) * max_stepsize j ^ p

goal (2 subgoals):
 1. t (Suc j) \<le> T
 2. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (T - t 0) + 1) - 1) * max_stepsize j ^ p

goal (2 subgoals):
 1. t (Suc j) \<le> T
 2. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>
[PROOF STEP]
have "... \<le> \<bar>r\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B / L * (exp (L * (T - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r\<bar>
[PROOF STEP]
using \<open>B \<ge> 0\<close> max_step max_stepsize_nonneg \<open>L \<ge> 0\<close> \<open>p > 0\<close>
        grid_ge_min
[PROOF STATE]
proof (prove)
using this:
0 \<le> B
max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))
0 \<le> max_stepsize ?n
0 \<le> L
0 < p
t 0 \<le> t ?j

goal (1 subgoal):
 1. B / L * (exp (L * (T - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r\<bar>
[PROOF STEP]
using grid_mono[of 0 j] \<open>t 0 \<le> T\<close> IH1
[PROOF STATE]
proof (prove)
using this:
0 \<le> B
max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))
0 \<le> max_stepsize ?n
0 \<le> L
0 < p
t 0 \<le> t ?j
0 \<le> j \<Longrightarrow> t 0 \<le> t j
t 0 \<le> T
max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))

goal (1 subgoal):
 1. B / L * (exp (L * (T - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r\<bar>
[PROOF STEP]
by (intro stepsize_inverse) auto
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * (T - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r\<bar>

goal (2 subgoals):
 1. t (Suc j) \<le> T
 2. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>
[PROOF STEP]
show
      "dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>"
[PROOF STATE]
proof (prove)
using this:
dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>

goal (1 subgoal):
 1. dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> \<bar>r\<bar>

goal (1 subgoal):
 1. t (Suc j) \<le> T
[PROOF STEP]
qed (insert Suc, simp)
[PROOF STATE]
proof (state)
this:
dist (\<psi> (stepsize j) (t j) (x t j)) (\<psi> (stepsize j) (t j) (grid_function (discrete_evolution \<psi>) x0 t j)) \<le> L * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>xa y. xa \<le> y \<Longrightarrow> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + xa \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + y; \<And>xa y. xa \<le> y \<Longrightarrow> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * xa) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * y)\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * (L * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)))
[PROOF STEP]
have "dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j))
    \<le> norm (x t (Suc j) - (discrete_evolution \<psi>) (t (Suc j)) (t j) (x t j)) +
    (1 + stepsize j * L) *
      dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>xa y. xa \<le> y \<Longrightarrow> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + xa \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + y; \<And>xa y. xa \<le> y \<Longrightarrow> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * xa) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * y)\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * (L * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)))

goal (1 subgoal):
 1. dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)
[PROOF STEP]
using grid_stepsize_nonneg
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>xa y. xa \<le> y \<Longrightarrow> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + xa \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + y; \<And>xa y. xa \<le> y \<Longrightarrow> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * xa) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * y)\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (norm (x t j - grid_function (discrete_evolution \<psi>) x0 t j) + stepsize j * (L * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)))
0 \<le> stepsize ?j

goal (1 subgoal):
 1. dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)
[PROOF STEP]
by (auto simp: algebra_simps mult_right_mono dist_norm)
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "norm (x t (Suc j) - (discrete_evolution \<psi>) (t (Suc j)) (t j) (x t j)) \<le>
    B * stepsize j ^ (p + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) \<le> B * stepsize j ^ (p + 1)
[PROOF STEP]
using consistence_error[OF \<open>t (Suc j) \<le> T\<close>]
[PROOF STATE]
proof (prove)
using this:
dist (x t (Suc j)) (discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) \<le> B * stepsize j ^ (p + 1)

goal (1 subgoal):
 1. norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) \<le> B * stepsize j ^ (p + 1)
[PROOF STEP]
by (simp add: dist_norm)
[PROOF STATE]
proof (state)
this:
norm (x t (Suc j) - discrete_evolution \<psi> (t (Suc j)) (t j) (x t j)) \<le> B * stepsize j ^ (p + 1)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa \<le> y \<Longrightarrow> xa + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> y + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)) \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)
[PROOF STEP]
have rec:
    "dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j))
      \<le> B * stepsize j ^ (p + 1) +
        (1 + stepsize j * L) *
        dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)"
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa \<le> y \<Longrightarrow> xa + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> y + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)) \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)

goal (1 subgoal):
 1. dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "... \<le> B * stepsize j ^ (p + 1) +
    (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)
[PROOF STEP]
using \<open>B \<ge> 0\<close> IH1 IH2 \<open>t (Suc j) \<le> T\<close> \<open>0\<le>L\<close> grid_stepsize_nonneg
[PROOF STATE]
proof (prove)
using this:
0 \<le> B
max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))
dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
t (Suc j) \<le> T
0 \<le> L
0 \<le> stepsize ?j

goal (1 subgoal):
 1. B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)
[PROOF STEP]
by (intro add_mono mult_left_mono) auto
[PROOF STATE]
proof (state)
this:
B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)
[PROOF STEP]
have "dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j))
    \<le> B * stepsize j ^ (p + 1) +
    (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) *
      max_stepsize j ^ p)"
[PROOF STATE]
proof (prove)
using this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)

goal (1 subgoal):
 1. dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "... \<le> B * stepsize j * max_stepsize j ^ p +
    (1 + stepsize j * L) *
    (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) \<le> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)
[PROOF STEP]
using grid_stepsize_nonneg \<open>B \<ge> 0\<close> grid
[PROOF STATE]
proof (prove)
using this:
0 \<le> stepsize ?j
0 \<le> B
t ?i \<le> t (Suc ?i)

goal (1 subgoal):
 1. B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) \<le> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)
[PROOF STEP]
by (auto intro!: mult_left_mono power_mono
      simp add: max_stepsize_def field_simps)
[PROOF STATE]
proof (state)
this:
B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) \<le> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B * stepsize j ^ (p + 1) + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) \<le> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "... = max_stepsize j ^ p * B / L * (1 + stepsize j * L) *
      (exp (L * (t j - t 0) + 1))
    - max_stepsize j ^ p * B / L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
using \<open>B \<ge> 0\<close> grid_stepsize_nonneg \<open>p > 0\<close> \<open>L\<ge>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> B
0 \<le> stepsize ?j
0 < p
0 \<le> L

goal (1 subgoal):
 1. B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
apply (cases "L \<noteq> 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> B; \<And>j. 0 \<le> stepsize j; 0 < p; 0 \<le> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
 2. \<lbrakk>0 \<le> B; \<And>j. 0 \<le> stepsize j; 0 < p; 0 \<le> L; \<not> L \<noteq> 0\<rbrakk> \<Longrightarrow> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> B; \<And>j. 0 \<le> stepsize j; 0 < p; 0 \<le> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> B; \<And>j. 0 \<le> stepsize j; 0 < p; 0 \<le> L; \<not> L \<noteq> 0\<rbrakk> \<Longrightarrow> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> B; \<And>j. 0 \<le> stepsize j; 0 < p; 0 \<le> L; \<not> L \<noteq> 0\<rbrakk> \<Longrightarrow> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
apply (cases "max_stepsize j = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> B; \<And>j. 0 \<le> stepsize j; 0 < p; 0 \<le> L; \<not> L \<noteq> 0; max_stepsize j = 0\<rbrakk> \<Longrightarrow> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
 2. \<lbrakk>0 \<le> B; \<And>j. 0 \<le> stepsize j; 0 < p; 0 \<le> L; \<not> L \<noteq> 0; max_stepsize j \<noteq> 0\<rbrakk> \<Longrightarrow> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> B; \<And>j. 0 \<le> stepsize j; 0 < p; 0 \<le> L; \<not> L \<noteq> 0; max_stepsize j = 0\<rbrakk> \<Longrightarrow> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> B; \<And>j. 0 \<le> stepsize j; 0 < p; 0 \<le> L; \<not> L \<noteq> 0; max_stepsize j \<noteq> 0\<rbrakk> \<Longrightarrow> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> B; \<And>j. 0 \<le> stepsize j; 0 < p; 0 \<le> L; \<not> L \<noteq> 0; max_stepsize j \<noteq> 0\<rbrakk> \<Longrightarrow> B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
by (metis IH1 abs_not_less_zero abs_of_pos div_0 less_eq_real_def max_stepsize_nonneg
            mult_zero_right real_root_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B * stepsize j * max_stepsize j ^ p + (1 + stepsize j * L) * (B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p) = max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) - max_stepsize j ^ p * B / L

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "B * (max_stepsize j ^ p * (exp (L * (t j - t 0) + 1) *
    (1 + L * (t (Suc j) - t j)))) / L
    \<le> B * (max_stepsize j ^ p * exp (L * (t (Suc j) - t 0) + 1)) / L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B * (max_stepsize j ^ p * (exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)))) / L \<le> B * (max_stepsize j ^ p * exp (L * (t (Suc j) - t 0) + 1)) / L
[PROOF STEP]
using \<open>L \<ge> 0\<close> \<open>B \<ge> 0\<close> max_stepsize_nonneg
[PROOF STATE]
proof (prove)
using this:
0 \<le> L
0 \<le> B
0 \<le> max_stepsize ?n

goal (1 subgoal):
 1. B * (max_stepsize j ^ p * (exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)))) / L \<le> B * (max_stepsize j ^ p * exp (L * (t (Suc j) - t 0) + 1)) / L
[PROOF STEP]
proof (intro divide_right_mono mult_left_mono)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t (Suc j) - t 0) + 1)
 2. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> max_stepsize j ^ p
 3. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> B
 4. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> L
[PROOF STEP]
have "exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le>
      exp (L * (t j - t 0) + 1) * exp (stepsize j * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t j - t 0) + 1) * exp (stepsize j * L)
[PROOF STEP]
unfolding stepsize_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (L * (t j - t 0) + 1) * (1 + L * stepsize j) \<le> exp (L * (t j - t 0) + 1) * exp (stepsize j * L)
[PROOF STEP]
by (auto simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t j - t 0) + 1) * exp (stepsize j * L)

goal (4 subgoals):
 1. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t (Suc j) - t 0) + 1)
 2. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> max_stepsize j ^ p
 3. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> B
 4. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> L
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t j - t 0) + 1) * exp (stepsize j * L)

goal (4 subgoals):
 1. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t (Suc j) - t 0) + 1)
 2. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> max_stepsize j ^ p
 3. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> B
 4. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> L
[PROOF STEP]
have "... \<le> exp (L * (t (Suc j) - t 0) + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp (L * (t j - t 0) + 1) * exp (stepsize j * L) \<le> exp (L * (t (Suc j) - t 0) + 1)
[PROOF STEP]
by (simp add: mult_exp_exp stepsize_def algebra_simps)
[PROOF STATE]
proof (state)
this:
exp (L * (t j - t 0) + 1) * exp (stepsize j * L) \<le> exp (L * (t (Suc j) - t 0) + 1)

goal (4 subgoals):
 1. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t (Suc j) - t 0) + 1)
 2. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> max_stepsize j ^ p
 3. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> B
 4. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> L
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t (Suc j) - t 0) + 1)
[PROOF STEP]
show "exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le>
      exp (L * (t (Suc j) - t 0) + 1)"
[PROOF STATE]
proof (prove)
using this:
exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t (Suc j) - t 0) + 1)

goal (1 subgoal):
 1. exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t (Suc j) - t 0) + 1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)) \<le> exp (L * (t (Suc j) - t 0) + 1)

goal (3 subgoals):
 1. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> max_stepsize j ^ p
 2. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> B
 3. \<lbrakk>0 \<le> L; 0 \<le> B; \<And>n. 0 \<le> max_stepsize n\<rbrakk> \<Longrightarrow> 0 \<le> L
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
B * (max_stepsize j ^ p * (exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)))) / L \<le> B * (max_stepsize j ^ p * exp (L * (t (Suc j) - t 0) + 1)) / L

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
hence "max_stepsize j ^ p * B / L * (1 + stepsize j * L) *
    exp (L * (t j - t 0) + 1) \<le>
    max_stepsize j ^ p * B / L * exp (L * (t (Suc j) - t 0) + 1)"
[PROOF STATE]
proof (prove)
using this:
B * (max_stepsize j ^ p * (exp (L * (t j - t 0) + 1) * (1 + L * (t (Suc j) - t j)))) / L \<le> B * (max_stepsize j ^ p * exp (L * (t (Suc j) - t 0) + 1)) / L

goal (1 subgoal):
 1. max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) \<le> max_stepsize j ^ p * B / L * exp (L * (t (Suc j) - t 0) + 1)
[PROOF STEP]
by (simp add: stepsize_def ac_simps)
[PROOF STATE]
proof (state)
this:
max_stepsize j ^ p * B / L * (1 + stepsize j * L) * exp (L * (t j - t 0) + 1) \<le> max_stepsize j ^ p * B / L * exp (L * (t (Suc j) - t 0) + 1)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> x - max_stepsize j ^ p * B / L \<le> y - max_stepsize j ^ p * B / L) \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> max_stepsize j ^ p * B / L * exp (L * (t (Suc j) - t 0) + 1) - max_stepsize j ^ p * B / L
[PROOF STEP]
have "dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j))
    \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) *
    max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> x - max_stepsize j ^ p * B / L \<le> y - max_stepsize j ^ p * B / L) \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> max_stepsize j ^ p * B / L * exp (L * (t (Suc j) - t 0) + 1) - max_stepsize j ^ p * B / L

goal (1 subgoal):
 1. dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
have "... \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) *
    max_stepsize (Suc j) ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
using \<open>B\<ge>0\<close>\<open>L\<ge>0\<close> max_stepsize_nonneg
[PROOF STATE]
proof (prove)
using this:
0 \<le> B
0 \<le> L
0 \<le> max_stepsize ?n

goal (1 subgoal):
 1. B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
by (intro mult_left_mono power_mono max_stepsize_mono)
       (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg add_nonneg_nonneg grid_mono)
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>t j \<le> T; max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t j) (grid_function (discrete_evolution \<psi>) x0 t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p; t (Suc j) \<le> T; max_stepsize (Suc j) \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (T - t 0) + 1) - 1))\<rbrakk> \<Longrightarrow> dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p

goal (1 subgoal):
 1. dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dist (x t (Suc j)) (grid_function (discrete_evolution \<psi>) x0 t (Suc j)) \<le> B / L * (exp (L * (t (Suc j) - t 0) + 1) - 1) * max_stepsize (Suc j) ^ p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_step_mono_r:
  assumes "\<bar>s\<bar> \<ge> \<bar>r\<bar>" "L \<ge> 0" "B \<ge> 0" "t1 \<ge> t 0" "0 < p" "t j \<le> t1"
  shows "max_stepsize j \<le>
    root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_stepsize j \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max_stepsize j \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
from max_step \<open>t j \<le> t1\<close>
[PROOF STATE]
proof (chain)
picking this:
t ?j \<le> t1 \<Longrightarrow> max_stepsize ?j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
t j \<le> t1
[PROOF STEP]
have "max_stepsize j \<le>
    root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))"
[PROOF STATE]
proof (prove)
using this:
t ?j \<le> t1 \<Longrightarrow> max_stepsize ?j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
t j \<le> t1

goal (1 subgoal):
 1. max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))

goal (1 subgoal):
 1. max_stepsize j \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))

goal (1 subgoal):
 1. max_stepsize j \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
have "... \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1)) \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<bar>r\<bar> \<le> \<bar>s\<bar>
0 \<le> L
0 \<le> B
t 0 \<le> t1
0 < p
t j \<le> t1

goal (1 subgoal):
 1. root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1)) \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
apply (cases "B = 0", force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<bar>r\<bar> \<le> \<bar>s\<bar>; 0 \<le> L; 0 \<le> B; t 0 \<le> t1; 0 < p; t j \<le> t1; B \<noteq> 0\<rbrakk> \<Longrightarrow> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1)) \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
apply (cases "L = 0", force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<bar>r\<bar> \<le> \<bar>s\<bar>; 0 \<le> L; 0 \<le> B; t 0 \<le> t1; 0 < p; t j \<le> t1; B \<noteq> 0; L \<noteq> 0\<rbrakk> \<Longrightarrow> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1)) \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
by (auto simp add: mult_le_cancel_left1
             intro!: divide_right_mono add_increasing mult_left_mono)
[PROOF STATE]
proof (state)
this:
root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1)) \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))

goal (1 subgoal):
 1. max_stepsize j \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
max_stepsize j \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
show "max_stepsize j \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))"
[PROOF STATE]
proof (prove)
using this:
max_stepsize j \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))

goal (1 subgoal):
 1. max_stepsize j \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
max_stepsize j \<le> root p (\<bar>s\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in convergent_one_step) convergence:
  assumes "t j \<le> t1"
  shows "dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le>
        B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
from order_pos consistent_nonneg lipschitz_nonneg
[PROOF STATE]
proof (chain)
picking this:
0 < p
0 \<le> B
0 \<le> L
[PROOF STEP]
have "p > 0" "B \<ge> 0" "L \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 < p
0 \<le> B
0 \<le> L

goal (1 subgoal):
 1. 0 < p &&& 0 \<le> B &&& 0 \<le> L
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < p
0 \<le> B
0 \<le> L

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
from consistent
[PROOF STATE]
proof (chain)
picking this:
?s \<in> {t0..t1} \<Longrightarrow> consistent x ?s t1 B p incr
[PROOF STEP]
have consistence_error: "dist (x (t j + stepsize j))
      (discrete_evolution incr (t j + stepsize j) (t j) (x (t j)))
      \<le> B * (stepsize j ^ (p + 1))"
      if "t (Suc j) \<le> t1" for j :: nat
[PROOF STATE]
proof (prove)
using this:
?s \<in> {t0..t1} \<Longrightarrow> consistent x ?s t1 B p incr

goal (1 subgoal):
 1. dist (x (t j + stepsize j)) (discrete_evolution incr (t j + stepsize j) (t j) (x (t j))) \<le> B * stepsize j ^ (p + 1)
[PROOF STEP]
apply (rule consistentD [OF _ grid_stepsize_nonneg])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. t j \<in> {t0..t1}
 2. t j + stepsize j \<le> t1
[PROOF STEP]
using \<open>t (Suc j) \<le> t1\<close> grid_mono[of j "Suc j"] grid_from grid_interval_notempty
[PROOF STATE]
proof (prove)
using this:
t (Suc j) \<le> t1
j \<le> Suc j \<Longrightarrow> t j \<le> t (Suc j)
t0 = t 0
t 0 \<le> t ?n

goal (2 subgoals):
 1. t j \<in> {t0..t1}
 2. t j + stepsize j \<le> t1
[PROOF STEP]
by (auto simp add: stepsize_def)
[PROOF STATE]
proof (state)
this:
t (Suc ?j) \<le> t1 \<Longrightarrow> dist (x (t ?j + stepsize ?j)) (discrete_evolution incr (t ?j + stepsize ?j) (t ?j) (x (t ?j))) \<le> B * stepsize ?j ^ (p + 1)

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have lipschitz_grid: "dist (incr (stepsize j) (t j) (x (t j)))
    (incr (stepsize j) (t j)
    (grid_function (discrete_evolution incr) (x (t 0)) t j))
    \<le> L *
    dist (x (t j))
    (grid_function (discrete_evolution incr) (x (t 0)) t j)"
    if "t (Suc j) \<le> t1"
    and in_K: "dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>"
    for j :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
from in_K
[PROOF STATE]
proof (chain)
picking this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>
[PROOF STEP]
have "stepsize j \<in> {0..t1 - t j}"
[PROOF STATE]
proof (prove)
using this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>

goal (1 subgoal):
 1. stepsize j \<in> {0..t1 - t j}
[PROOF STEP]
using grid_stepsize_nonneg grid_mono \<open>t (Suc j) \<le> t1\<close>
[PROOF STATE]
proof (prove)
using this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>
0 \<le> stepsize ?j
?j \<le> ?n \<Longrightarrow> t ?j \<le> t ?n
t (Suc j) \<le> t1

goal (1 subgoal):
 1. stepsize j \<in> {0..t1 - t j}
[PROOF STEP]
by (simp add: stepsize_def)
[PROOF STATE]
proof (state)
this:
stepsize j \<in> {0..t1 - t j}

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stepsize j \<in> {0..t1 - t j}

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
have t: "t j \<in> {t 0..t1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t j \<in> {t 0..t1}
[PROOF STEP]
using grid[of j] \<open>t (Suc j) \<le> t1\<close>
      grid_mono[of j "Suc j"] grid_ge_min
[PROOF STATE]
proof (prove)
using this:
t j \<le> t (Suc j)
t (Suc j) \<le> t1
j \<le> Suc j \<Longrightarrow> t j \<le> t (Suc j)
t 0 \<le> t ?j

goal (1 subgoal):
 1. t j \<in> {t 0..t1}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t j \<in> {t 0..t1}

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t j \<in> {t 0..t1}

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
have "x (t j) \<in> cball (x (t j)) \<bar>r\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x (t j) \<in> cball (x (t j)) \<bar>r\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x (t j) \<in> cball (x (t j)) \<bar>r\<bar>

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x (t j) \<in> cball (x (t j)) \<bar>r\<bar>

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
have  "grid_function (discrete_evolution incr) (x (t 0)) t j \<in>
      cball (x (t j)) \<bar>r\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. grid_function (discrete_evolution incr) (x (t 0)) t j \<in> cball (x (t j)) \<bar>r\<bar>
[PROOF STEP]
using in_K mem_cball
[PROOF STATE]
proof (prove)
using this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>
(?y \<in> cball ?x ?e) = (dist ?x ?y \<le> ?e)

goal (1 subgoal):
 1. grid_function (discrete_evolution incr) (x (t 0)) t j \<in> cball (x (t j)) \<bar>r\<bar>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
grid_function (discrete_evolution incr) (x (t 0)) t j \<in> cball (x (t j)) \<bar>r\<bar>

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
stepsize j \<in> {0..t1 - t j}
t j \<in> {t 0..t1}
x (t j) \<in> cball (x (t j)) \<bar>r\<bar>
grid_function (discrete_evolution incr) (x (t 0)) t j \<in> cball (x (t j)) \<bar>r\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stepsize j \<in> {0..t1 - t j}
t j \<in> {t 0..t1}
x (t j) \<in> cball (x (t j)) \<bar>r\<bar>
grid_function (discrete_evolution incr) (x (t 0)) t j \<in> cball (x (t j)) \<bar>r\<bar>

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
using lipschitz_incr grid_from
[PROOF STATE]
proof (prove)
using this:
stepsize j \<in> {0..t1 - t j}
t j \<in> {t 0..t1}
x (t j) \<in> cball (x (t j)) \<bar>r\<bar>
grid_function (discrete_evolution incr) (x (t 0)) t j \<in> cball (x (t j)) \<bar>r\<bar>
\<lbrakk>?s \<in> {t0..t1}; ?h \<in> {0..t1 - ?s}\<rbrakk> \<Longrightarrow> L-lipschitz_on (cball (x ?s) \<bar>r\<bar>) (incr ?h ?s)
t0 = t 0

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
unfolding lipschitz_on_def
[PROOF STATE]
proof (prove)
using this:
stepsize j \<in> {0..t1 - t j}
t j \<in> {t 0..t1}
x (t j) \<in> cball (x (t j)) \<bar>r\<bar>
grid_function (discrete_evolution incr) (x (t 0)) t j \<in> cball (x (t j)) \<bar>r\<bar>
\<lbrakk>?s \<in> {t0..t1}; ?h \<in> {0..t1 - ?s}\<rbrakk> \<Longrightarrow> 0 \<le> L \<and> (\<forall>xa\<in>cball (x ?s) \<bar>r\<bar>. \<forall>y\<in>cball (x ?s) \<bar>r\<bar>. dist (incr ?h ?s xa) (incr ?h ?s y) \<le> L * dist xa y)
t0 = t 0

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dist (incr (stepsize j) (t j) (x (t j))) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>t (Suc ?j) \<le> t1; dist (x (t ?j)) (grid_function (discrete_evolution incr) (x (t 0)) t ?j) \<le> \<bar>r\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize ?j) (t ?j) (x (t ?j))) (incr (stepsize ?j) (t ?j) (grid_function (discrete_evolution incr) (x (t 0)) t ?j)) \<le> L * dist (x (t ?j)) (grid_function (discrete_evolution incr) (x (t 0)) t ?j)

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have
    "dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le>
    (B / L * (exp (L * (t j - t 0) + 1) - 1)) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
using \<open>p > 0\<close> \<open>L \<ge> 0\<close> \<open>B \<ge> 0\<close> \<open>t j \<le> t1\<close>
      max_stepsize_nonneg
      consistence_error lipschitz_grid
[PROOF STATE]
proof (prove)
using this:
0 < p
0 \<le> L
0 \<le> B
t j \<le> t1
0 \<le> max_stepsize ?n
t (Suc ?j) \<le> t1 \<Longrightarrow> dist (x (t ?j + stepsize ?j)) (discrete_evolution incr (t ?j + stepsize ?j) (t ?j) (x (t ?j))) \<le> B * stepsize ?j ^ (p + 1)
\<lbrakk>t (Suc ?j) \<le> t1; dist (x (t ?j)) (grid_function (discrete_evolution incr) (x (t 0)) t ?j) \<le> \<bar>r\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize ?j) (t ?j) (x (t ?j))) (incr (stepsize ?j) (t ?j) (grid_function (discrete_evolution incr) (x (t 0)) t ?j)) \<le> L * dist (x (t ?j)) (grid_function (discrete_evolution incr) (x (t 0)) t ?j)

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by (intro error_accumulation[OF max_step]) (auto intro!:
      divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power grid_mono
      simp add: lipschitz_on_def stepsize_def)
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have "... \<le>
    (B / L * (exp (L * (t1 - t 0) + 1) - 1)) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
using \<open>t j \<le> t1\<close> \<open>0\<le>L\<close> \<open>0\<le>B\<close> max_stepsize_nonneg
[PROOF STATE]
proof (prove)
using this:
t j \<le> t1
0 \<le> L
0 \<le> B
0 \<le> max_stepsize ?n

goal (1 subgoal):
 1. B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by (auto intro!: divide_right_mono mult_right_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma t0_le: "t i \<le> t1 \<Longrightarrow> t 0 \<le> t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t i \<le> t1 \<Longrightarrow> t 0 \<le> t1
[PROOF STEP]
by (metis grid_interval_notempty order.trans)


[STATEMENT]
lemma max_step_r:
  assumes "t j \<le> t1"
  shows "max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
using consistent_nonneg lipschitz_nonneg grid_interval_notempty order_pos assms
    grid_mono[of 0 j, simplified]
[PROOF STATE]
proof (prove)
using this:
0 \<le> B
0 \<le> L
t 0 \<le> t ?n
0 < p
t j \<le> t1
t 0 \<le> t j

goal (1 subgoal):
 1. max_stepsize j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
[PROOF STEP]
by (intro max_step_mono_r) (auto simp: t0_le)