[STATEMENT]
lemma local_lipschitz_transfer[transfer_rule]:
  "(rel_set A ===> rel_set B ===> (A ===> B ===> C) ===> (=)) local_lipschitz local_lipschitz"
  if [transfer_rule]: "bi_total A" "bi_unique A" "bi_total B" "bi_unique B"
    "(A ===> A ===> (=)) dist dist"
    "(B ===> B ===> (=)) dist dist"
    "(C ===> C ===> (=)) dist dist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> rel_set B ===> (A ===> B ===> C) ===> (=)) local_lipschitz local_lipschitz
[PROOF STEP]
unfolding local_lipschitz_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> rel_set B ===> (A ===> B ===> C) ===> (=)) (\<lambda>T X f. \<forall>x\<in>X. \<forall>t\<in>T. \<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t)) (\<lambda>T X f. \<forall>x\<in>X. \<forall>t\<in>T. \<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma filterlim_transfer[transfer_rule]:
  "((A ===> B) ===> rel_filter B ===> rel_filter A ===> (=)) filterlim filterlim"
  if [transfer_rule]: "bi_unique B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> B) ===> rel_filter B ===> rel_filter A ===> (=)) filterlim filterlim
[PROOF STEP]
unfolding filterlim_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> B) ===> rel_filter B ===> rel_filter A ===> (=)) (\<lambda>f F2 F1. \<forall>P. eventually P F2 \<longrightarrow> (\<forall>\<^sub>F x in F1. P (f x))) (\<lambda>f F2 F1. \<forall>P. eventually P F2 \<longrightarrow> (\<forall>\<^sub>F x in F1. P (f x)))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma nhds_transfer[transfer_rule]:
  "(A ===> rel_filter A) nhds nhds"
  if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> rel_filter A) nhds nhds
[PROOF STEP]
unfolding nhds_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> rel_filter A) (\<lambda>a. Inf (principal ` {S. open S \<and> a \<in> S})) (\<lambda>a. Inf (principal ` {S. open S \<and> a \<in> S}))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma at_within_transfer[transfer_rule]:
  "(A ===> rel_set A ===> rel_filter A) at_within at_within"
  if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> rel_set A ===> rel_filter A) at_within at_within
[PROOF STEP]
unfolding at_within_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> rel_set A ===> rel_filter A) (\<lambda>a s. inf (nhds a) (principal (s - {a}))) (\<lambda>a s. inf (nhds a) (principal (s - {a})))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma continuous_on_transfer[transfer_rule]:
  "(rel_set A ===> (A ===> B) ===> (=)) continuous_on continuous_on"
  if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
    "bi_unique B" "bi_total B" "(rel_set B ===> (=)) open open"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (A ===> B) ===> (=)) continuous_on continuous_on
[PROOF STEP]
unfolding continuous_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (A ===> B) ===> (=)) (\<lambda>s f. \<forall>x\<in>s. (f \<longlongrightarrow> f x) (at x within s)) (\<lambda>s f. \<forall>x\<in>s. (f \<longlongrightarrow> f x) (at x within s))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma is_interval_transfer[transfer_rule]: "(rel_set A ===> (=)) is_interval is_interval"
  if [transfer_rule]: "bi_unique A" "bi_total A" "(A ===> A ===> (=)) inner inner" "(rel_set A) Basis Basis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (=)) is_interval is_interval
[PROOF STEP]
unfolding is_interval_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (=)) (\<lambda>s. \<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i \<or> b \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> a \<bullet> i) \<longrightarrow> x \<in> s) (\<lambda>s. \<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i \<or> b \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> a \<bullet> i) \<longrightarrow> x \<in> s)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma additive_transfer[transfer_rule]:
  "((B ===> A) ===> (=)) Modules.additive Modules.additive"
  if [transfer_rule]:
    "bi_unique A"
    "bi_total B"
    "(A ===> A ===> A) (+) (+)"
    "(B ===> B ===> B) (+) (+)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((B ===> A) ===> (=)) Modules.additive Modules.additive
[PROOF STEP]
unfolding Modules.additive_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((B ===> A) ===> (=)) (\<lambda>f. \<forall>x y. f (x + y) = f x + f y) (\<lambda>f. \<forall>x y. f (x + y) = f x + f y)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma linear_transfer[transfer_rule]: "((B ===> A) ===> (=)) linear linear"
  if [transfer_rule]:
    "bi_unique A"
    "bi_total B"
    "(A ===> A ===> A) (+) (+)"
    "((=) ===> A ===> A) (*\<^sub>R) (*\<^sub>R)"
    "(B ===> B ===> B) (+) (+)"
    "((=) ===> B ===> B) (*\<^sub>R) (*\<^sub>R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((B ===> A) ===> (=)) linear linear
[PROOF STEP]
unfolding linear_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((B ===> A) ===> (=)) (\<lambda>f. (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>R x) = c *\<^sub>R f x)) (\<lambda>f. (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>R x) = c *\<^sub>R f x))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma bounded_linear_transfer[transfer_rule]: "((B ===> A) ===> (=)) bounded_linear bounded_linear"
  if [transfer_rule]:
    "bi_unique A"
    "bi_total B"
    "(A ===> A ===> A) (+) (+)"
    "((=) ===> A ===> A) (*\<^sub>R) (*\<^sub>R)"
    "(B ===> B ===> B) (+) (+)"
    "((=) ===> B ===> B) (*\<^sub>R) (*\<^sub>R)"
    "(A ===> (=)) norm norm"
    "(B ===> (=)) norm norm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((B ===> A) ===> (=)) bounded_linear bounded_linear
[PROOF STEP]
unfolding bounded_linear_def bounded_linear_axioms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((B ===> A) ===> (=)) (\<lambda>f. linear f \<and> (\<exists>K. \<forall>x. norm (f x) \<le> norm x * K)) (\<lambda>f. linear f \<and> (\<exists>K. \<forall>x. norm (f x) \<le> norm x * K))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma Pi_transfer[transfer_rule]: "(rel_set B ===> (B ===> rel_set A) ===> rel_set (B ===> A)) FuncSet.Pi FuncSet.Pi"
  if [transfer_rule]: "bi_unique A" "bi_total A" "bi_unique B" "bi_total B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set B ===> (B ===> rel_set A) ===> rel_set (B ===> A)) Pi Pi
[PROOF STEP]
unfolding FuncSet.Pi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set B ===> (B ===> rel_set A) ===> rel_set (B ===> A)) (\<lambda>A B. {f. \<forall>x. x \<in> A \<longrightarrow> f x \<in> B x}) (\<lambda>A B. {f. \<forall>x. x \<in> A \<longrightarrow> f x \<in> B x})
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma bi_unique_rel_blinfun[transfer_rule]:
  "bi_total A \<Longrightarrow> bi_unique B \<Longrightarrow> bi_unique (rel_blinfun A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_blinfun A B)
[PROOF STEP]
using bi_unique_fun[of A B]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (A ===> B)

goal (1 subgoal):
 1. \<lbrakk>bi_total A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_blinfun A B)
[PROOF STEP]
unfolding bi_unique_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bi_total A; (\<forall>x y z. B x y \<longrightarrow> B x z \<longrightarrow> y = z) \<and> (\<forall>x y z. B x z \<longrightarrow> B y z \<longrightarrow> x = y)\<rbrakk> \<Longrightarrow> (\<forall>x y z. (A ===> B) x y \<longrightarrow> (A ===> B) x z \<longrightarrow> y = z) \<and> (\<forall>x y z. (A ===> B) x z \<longrightarrow> (A ===> B) y z \<longrightarrow> x = y)

goal (1 subgoal):
 1. \<lbrakk>bi_total A; (\<forall>x y z. B x y \<longrightarrow> B x z \<longrightarrow> y = z) \<and> (\<forall>x y z. B x z \<longrightarrow> B y z \<longrightarrow> x = y)\<rbrakk> \<Longrightarrow> (\<forall>x y z. rel_blinfun A B x y \<longrightarrow> rel_blinfun A B x z \<longrightarrow> y = z) \<and> (\<forall>x y z. rel_blinfun A B x z \<longrightarrow> rel_blinfun A B y z \<longrightarrow> x = y)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma bi_total_rel_blinfun[transfer_rule]:
  "bi_total (rel_blinfun A B)"
  if
    "bi_unique A" "bi_total B" (* really? *)
    "bi_unique B" "bi_total A"
    "(B ===> B ===> B) (+) (+)"
    "((=) ===> B ===> B) (*\<^sub>R) (*\<^sub>R)"
    "(A ===> A ===> A) (+) (+)"
    "((=) ===> A ===> A) (*\<^sub>R) (*\<^sub>R)"
    "(B ===> (=)) norm norm"
    "(A ===> (=)) norm norm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bi_total (rel_blinfun A B)
[PROOF STEP]
using bounded_linear_transfer[OF that(3-)]
[PROOF STATE]
proof (prove)
using this:
((A ===> B) ===> (=)) bounded_linear bounded_linear

goal (1 subgoal):
 1. bi_total (rel_blinfun A B)
[PROOF STEP]
using bi_total_fun[OF that(1,2)]
[PROOF STATE]
proof (prove)
using this:
((A ===> B) ===> (=)) bounded_linear bounded_linear
bi_total (A ===> B)

goal (1 subgoal):
 1. bi_total (rel_blinfun A B)
[PROOF STEP]
unfolding bi_total_def
[PROOF STATE]
proof (prove)
using this:
((A ===> B) ===> (=)) bounded_linear bounded_linear
(\<forall>x. Ex ((A ===> B) x)) \<and> (\<forall>y. \<exists>x. (A ===> B) x y)

goal (1 subgoal):
 1. (\<forall>x. Ex (rel_blinfun A B x)) \<and> (\<forall>y. \<exists>x. rel_blinfun A B x y)
[PROOF STEP]
apply (transfer fixing: A B)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((A ===> B) ===> (=)) bounded_linear bounded_linear; (\<forall>x. Ex ((A ===> B) x)) \<and> (\<forall>y. \<exists>x. (A ===> B) x y)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>Collect bounded_linear. Bex (Collect bounded_linear) ((A ===> B) x)) \<and> (\<forall>y\<in>Collect bounded_linear. \<exists>x\<in>Collect bounded_linear. (A ===> B) x y)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>((A ===> B) ===> (=)) bounded_linear bounded_linear; \<forall>x. Ex ((A ===> B) x); \<forall>y. \<exists>x. (A ===> B) x y; bounded_linear x\<rbrakk> \<Longrightarrow> \<exists>xa. bounded_linear xa \<and> (A ===> B) x xa
 2. \<And>y. \<lbrakk>((A ===> B) ===> (=)) bounded_linear bounded_linear; \<forall>x. Ex ((A ===> B) x); \<forall>y. \<exists>x. (A ===> B) x y; bounded_linear y\<rbrakk> \<Longrightarrow> \<exists>x. bounded_linear x \<and> (A ===> B) x y
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((A ===> B) ===> (=)) bounded_linear bounded_linear; \<forall>x. Ex ((A ===> B) x); \<forall>y. \<exists>x. (A ===> B) x y; bounded_linear x\<rbrakk> \<Longrightarrow> \<exists>xa. bounded_linear xa \<and> (A ===> B) x xa
[PROOF STEP]
apply (drule spec[where x=x])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((A ===> B) ===> (=)) bounded_linear bounded_linear; \<forall>y. \<exists>x. (A ===> B) x y; bounded_linear x; Ex ((A ===> B) x)\<rbrakk> \<Longrightarrow> \<exists>xa. bounded_linear xa \<and> (A ===> B) x xa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>((A ===> B) ===> (=)) bounded_linear bounded_linear; \<forall>y. \<exists>x. (A ===> B) x y; bounded_linear x; (A ===> B) x xa\<rbrakk> \<Longrightarrow> \<exists>xa. bounded_linear xa \<and> (A ===> B) x xa
[PROOF STEP]
apply (drule rel_funD, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>y. \<exists>x. (A ===> B) x y; bounded_linear x; (A ===> B) x xa; bounded_linear x = bounded_linear xa\<rbrakk> \<Longrightarrow> \<exists>xa. bounded_linear xa \<and> (A ===> B) x xa
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>((A ===> B) ===> (=)) bounded_linear bounded_linear; \<forall>x. Ex ((A ===> B) x); \<forall>y. \<exists>x. (A ===> B) x y; bounded_linear y\<rbrakk> \<Longrightarrow> \<exists>x. bounded_linear x \<and> (A ===> B) x y
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((A ===> B) ===> (=)) bounded_linear bounded_linear; \<forall>x. Ex ((A ===> B) x); \<forall>y. \<exists>x. (A ===> B) x y; bounded_linear x\<rbrakk> \<Longrightarrow> \<exists>xa. bounded_linear xa \<and> (A ===> B) xa x
[PROOF STEP]
apply (drule spec[where x=x])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((A ===> B) ===> (=)) bounded_linear bounded_linear; \<forall>x. Ex ((A ===> B) x); bounded_linear x; \<exists>xa. (A ===> B) xa x\<rbrakk> \<Longrightarrow> \<exists>xa. bounded_linear xa \<and> (A ===> B) xa x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>((A ===> B) ===> (=)) bounded_linear bounded_linear; \<forall>x. Ex ((A ===> B) x); bounded_linear x; (A ===> B) xa x\<rbrakk> \<Longrightarrow> \<exists>xa. bounded_linear xa \<and> (A ===> B) xa x
[PROOF STEP]
apply (drule rel_funD, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>x. Ex ((A ===> B) x); bounded_linear x; (A ===> B) xa x; bounded_linear xa = bounded_linear x\<rbrakk> \<Longrightarrow> \<exists>xa. bounded_linear xa \<and> (A ===> B) xa x
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma blinfun_apply_transfer[transfer_rule]:
  "(rel_blinfun A B ===> A ===> B) blinfun_apply blinfun_apply"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_blinfun A B ===> A ===> B) blinfun_apply blinfun_apply
[PROOF STEP]
by (auto simp: rel_blinfun_def)


[STATEMENT]
lemma norm_blinfun_transfer[transfer_rule]: "(rel_blinfun A A ===> (=)) norm norm"
  if [transfer_rule]: "(A ===> (=)) norm norm" "(rel_set A) UNIV UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_blinfun A A ===> (=)) norm norm
[PROOF STEP]
unfolding norm_blinfun.rep_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_blinfun A A ===> (=)) (\<lambda>x. onorm (blinfun_apply x)) (\<lambda>x. onorm (blinfun_apply x))
[PROOF STEP]
unfolding onorm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_blinfun A A ===> (=)) (\<lambda>x. SUP xa. norm (blinfun_apply x xa) / norm xa) (\<lambda>x. SUP xa. norm (blinfun_apply x xa) / norm xa)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma minus_blinfun_transfer[transfer_rule]:
  "(rel_blinfun A B ===> rel_blinfun A B ===> rel_blinfun A B) (-) (-)"
  if "(B ===> B ===> B) (-) (-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_blinfun A B ===> rel_blinfun A B ===> rel_blinfun A B) (-) (-)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(B ===> B ===> B) (-) (-)

goal (1 subgoal):
 1. (rel_blinfun A B ===> rel_blinfun A B ===> rel_blinfun A B) (-) (-)
[PROOF STEP]
apply (auto simp: rel_blinfun_def blinfun.bilinear_simps
      intro!: rel_funI dest: rel_funD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya xb yb. \<lbrakk>(B ===> B ===> B) (-) (-); (A ===> B) (blinfun_apply x) (blinfun_apply y); (A ===> B) (blinfun_apply xa) (blinfun_apply ya); A xb yb\<rbrakk> \<Longrightarrow> B (blinfun_apply x xb - blinfun_apply xa xb) (blinfun_apply y yb - blinfun_apply ya yb)
[PROOF STEP]
by (metis rel_funD)


[STATEMENT]
lemma compose_blinfun_transfer[transfer_rule]:"(rel_blinfun A B ===> rel_blinfun C A ===> rel_blinfun C B) (o\<^sub>L) (o\<^sub>L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_blinfun A B ===> rel_blinfun C A ===> rel_blinfun C B) (o\<^sub>L) (o\<^sub>L)
[PROOF STEP]
apply (auto simp: rel_blinfun_def blinfun.bilinear_simps
      intro!: rel_funI dest: rel_funD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya xb yb. \<lbrakk>(A ===> B) (blinfun_apply x) (blinfun_apply y); (C ===> A) (blinfun_apply xa) (blinfun_apply ya); C xb yb\<rbrakk> \<Longrightarrow> B (blinfun_apply x (blinfun_apply xa xb)) (blinfun_apply y (blinfun_apply ya yb))
[PROOF STEP]
by (metis rel_funD)


[STATEMENT]
lemma derivative_quotient_bound:
  assumes g_deriv_on: "(g has_vderiv_on g') {a .. b}"
  assumes frac_le: "\<And>t. t \<in> {a .. b} \<Longrightarrow> g' t / g t \<le> K"
  assumes g'_cont: "continuous_on {a .. b} g'"
  assumes g_pos: "\<And>t. t \<in> {a .. b} \<Longrightarrow> g t > 0"
  assumes t_in: "t \<in> {a .. b}"
  shows "g t \<le> g a * exp (K * (t - a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
have g_deriv: "\<And>t. t \<in> {a .. b} \<Longrightarrow> (g has_real_derivative g' t) (at t within {a .. b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' t) (at t within {a..b})
[PROOF STEP]
using g_deriv_on
[PROOF STATE]
proof (prove)
using this:
(g has_vderiv_on g') {a..b}

goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' t) (at t within {a..b})
[PROOF STEP]
by (auto simp: has_vderiv_on_def has_real_derivative_iff_has_vector_derivative[symmetric])
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' ?t) (at ?t within {a..b})

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(g has_vderiv_on g') {a..b}
?t \<in> {a..b} \<Longrightarrow> g' ?t / g ?t \<le> K
continuous_on {a..b} g'
?t \<in> {a..b} \<Longrightarrow> 0 < g ?t
t \<in> {a..b}
[PROOF STEP]
have g_nonzero: "\<And>t. t \<in> {a .. b} \<Longrightarrow> g t \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
(g has_vderiv_on g') {a..b}
?t \<in> {a..b} \<Longrightarrow> g' ?t / g ?t \<le> K
continuous_on {a..b} g'
?t \<in> {a..b} \<Longrightarrow> 0 < g ?t
t \<in> {a..b}

goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> g t \<noteq> 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> g ?t \<noteq> 0

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
have frac_integrable: "\<And>t. t \<in> {a .. b} \<Longrightarrow> (\<lambda>t. g' t / g t) integrable_on {a..t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> (\<lambda>t. g' t / g t) integrable_on {a..t}
[PROOF STEP]
by (force simp: g_nonzero intro: assms has_field_derivative_subset[OF g_deriv]
      continuous_on_subset[OF g'_cont] continuous_intros integrable_continuous_real
      continuous_on_subset[OF vderiv_on_continuous_on[OF g_deriv_on]])
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> (\<lambda>t. g' t / g t) integrable_on {a..?t}

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
have "\<And>t. t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g t) - ln (g a)) {a .. t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g t) - ln (g a)) {a..t}
[PROOF STEP]
by (rule fundamental_theorem_of_calculus)
      (auto intro!: derivative_eq_intros assms has_field_derivative_subset[OF g_deriv]
        simp: has_real_derivative_iff_has_vector_derivative[symmetric])
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g ?t) - ln (g a)) {a..?t}

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
hence *: "\<And>t. t \<in> {a .. b} \<Longrightarrow> ln (g t) - ln (g a) = integral {a .. t} (\<lambda>t. g' t / g t)"
[PROOF STATE]
proof (prove)
using this:
?t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g ?t) - ln (g a)) {a..?t}

goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> ln (g t) - ln (g a) = integral {a..t} (\<lambda>t. g' t / g t)
[PROOF STEP]
using integrable_integral[OF frac_integrable]
[PROOF STATE]
proof (prove)
using this:
?t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g ?t) - ln (g a)) {a..?t}
?t1 \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral integral {a..?t1} (\<lambda>t. g' t / g t)) {a..?t1}

goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> ln (g t) - ln (g a) = integral {a..t} (\<lambda>t. g' t / g t)
[PROOF STEP]
by (rule has_integral_unique[where f = "\<lambda>t. g' t / g t"])
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> ln (g ?t) - ln (g a) = integral {a..?t} (\<lambda>t. g' t / g t)

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
from * t_in
[PROOF STATE]
proof (chain)
picking this:
?t \<in> {a..b} \<Longrightarrow> ln (g ?t) - ln (g a) = integral {a..?t} (\<lambda>t. g' t / g t)
t \<in> {a..b}
[PROOF STEP]
have "ln (g t) - ln (g a) = integral {a .. t} (\<lambda>t. g' t / g t)"
[PROOF STATE]
proof (prove)
using this:
?t \<in> {a..b} \<Longrightarrow> ln (g ?t) - ln (g a) = integral {a..?t} (\<lambda>t. g' t / g t)
t \<in> {a..b}

goal (1 subgoal):
 1. ln (g t) - ln (g a) = integral {a..t} (\<lambda>t. g' t / g t)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ln (g t) - ln (g a) = integral {a..t} (\<lambda>t. g' t / g t)

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ln (g t) - ln (g a) = integral {a..t} (\<lambda>t. g' t / g t)

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
have "\<dots> \<le> integral {a .. t} (\<lambda>_. K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {a..t} (\<lambda>t. g' t / g t) \<le> integral {a..t} (\<lambda>_. K)
[PROOF STEP]
using \<open>t \<in> {a .. b}\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}

goal (1 subgoal):
 1. integral {a..t} (\<lambda>t. g' t / g t) \<le> integral {a..t} (\<lambda>_. K)
[PROOF STEP]
by (intro integral_le) (auto intro!: frac_integrable frac_le integral_le)
[PROOF STATE]
proof (state)
this:
integral {a..t} (\<lambda>t. g' t / g t) \<le> integral {a..t} (\<lambda>_. K)

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {a..t} (\<lambda>t. g' t / g t) \<le> integral {a..t} (\<lambda>_. K)

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
have "\<dots> = K * (t - a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {a..t} (\<lambda>_. K) = K * (t - a)
[PROOF STEP]
using \<open>t \<in> {a .. b}\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}

goal (1 subgoal):
 1. integral {a..t} (\<lambda>_. K) = K * (t - a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
integral {a..t} (\<lambda>_. K) = K * (t - a)

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ln (g t) - ln (g a) \<le> K * (t - a)
[PROOF STEP]
have "ln (g t) \<le> K * (t - a) + ln (g a)" (is "?lhs \<le> ?rhs")
[PROOF STATE]
proof (prove)
using this:
ln (g t) - ln (g a) \<le> K * (t - a)

goal (1 subgoal):
 1. ln (g t) \<le> K * (t - a) + ln (g a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ln (g t) \<le> K * (t - a) + ln (g a)

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
hence "exp ?lhs \<le> exp ?rhs"
[PROOF STATE]
proof (prove)
using this:
ln (g t) \<le> K * (t - a) + ln (g a)

goal (1 subgoal):
 1. exp (ln (g t)) \<le> exp (K * (t - a) + ln (g a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exp (ln (g t)) \<le> exp (K * (t - a) + ln (g a))

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exp (ln (g t)) \<le> exp (K * (t - a) + ln (g a))

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
using \<open>t \<in> {a .. b}\<close> g_pos
[PROOF STATE]
proof (prove)
using this:
exp (ln (g t)) \<le> exp (K * (t - a) + ln (g a))
t \<in> {a..b}
?t \<in> {a..b} \<Longrightarrow> 0 < g ?t

goal (1 subgoal):
 1. g t \<le> g a * exp (K * (t - a))
[PROOF STEP]
by (simp add: ac_simps exp_add del: exp_le_cancel_iff)
[PROOF STATE]
proof (state)
this:
g t \<le> g a * exp (K * (t - a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma derivative_quotient_bound_left:
  assumes g_deriv_on: "(g has_vderiv_on g') {a .. b}"
  assumes frac_ge: "\<And>t. t \<in> {a .. b} \<Longrightarrow> K \<le> g' t / g t"
  assumes g'_cont: "continuous_on {a .. b} g'"
  assumes g_pos: "\<And>t. t \<in> {a .. b} \<Longrightarrow> g t > 0"
  assumes t_in: "t \<in> {a..b}"
  shows "g t \<le> g b * exp (K * (t - b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
have g_deriv: "\<And>t. t \<in> {a .. b} \<Longrightarrow> (g has_real_derivative g' t) (at t within {a .. b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' t) (at t within {a..b})
[PROOF STEP]
using g_deriv_on
[PROOF STATE]
proof (prove)
using this:
(g has_vderiv_on g') {a..b}

goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' t) (at t within {a..b})
[PROOF STEP]
by (auto simp: has_vderiv_on_def has_real_derivative_iff_has_vector_derivative[symmetric])
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' ?t) (at ?t within {a..b})

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(g has_vderiv_on g') {a..b}
?t \<in> {a..b} \<Longrightarrow> K \<le> g' ?t / g ?t
continuous_on {a..b} g'
?t \<in> {a..b} \<Longrightarrow> 0 < g ?t
t \<in> {a..b}
[PROOF STEP]
have g_nonzero: "\<And>t. t \<in> {a..b} \<Longrightarrow> g t \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
(g has_vderiv_on g') {a..b}
?t \<in> {a..b} \<Longrightarrow> K \<le> g' ?t / g ?t
continuous_on {a..b} g'
?t \<in> {a..b} \<Longrightarrow> 0 < g ?t
t \<in> {a..b}

goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> g t \<noteq> 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> g ?t \<noteq> 0

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
have frac_integrable: "\<And>t. t \<in> {a .. b} \<Longrightarrow> (\<lambda>t. g' t / g t) integrable_on {t..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> (\<lambda>t. g' t / g t) integrable_on {t..b}
[PROOF STEP]
by (force simp: g_nonzero intro: assms has_field_derivative_subset[OF g_deriv]
      continuous_on_subset[OF g'_cont] continuous_intros integrable_continuous_real
      continuous_on_subset[OF vderiv_on_continuous_on[OF g_deriv_on]])
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> (\<lambda>t. g' t / g t) integrable_on {?t..b}

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
have "\<And>t. t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g b) - ln (g t)) {t..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g b) - ln (g t)) {t..b}
[PROOF STEP]
by (rule fundamental_theorem_of_calculus)
      (auto intro!: derivative_eq_intros assms has_field_derivative_subset[OF g_deriv]
        simp: has_real_derivative_iff_has_vector_derivative[symmetric])
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g b) - ln (g ?t)) {?t..b}

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
hence *: "\<And>t. t \<in> {a..b} \<Longrightarrow> ln (g b) - ln (g t) = integral {t..b} (\<lambda>t. g' t / g t)"
[PROOF STATE]
proof (prove)
using this:
?t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g b) - ln (g ?t)) {?t..b}

goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> ln (g b) - ln (g t) = integral {t..b} (\<lambda>t. g' t / g t)
[PROOF STEP]
using integrable_integral[OF frac_integrable]
[PROOF STATE]
proof (prove)
using this:
?t \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral ln (g b) - ln (g ?t)) {?t..b}
?t1 \<in> {a..b} \<Longrightarrow> ((\<lambda>t. g' t / g t) has_integral integral {?t1..b} (\<lambda>t. g' t / g t)) {?t1..b}

goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> ln (g b) - ln (g t) = integral {t..b} (\<lambda>t. g' t / g t)
[PROOF STEP]
by (rule has_integral_unique[where f = "\<lambda>t. g' t / g t"])
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> ln (g b) - ln (g ?t) = integral {?t..b} (\<lambda>t. g' t / g t)

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
have "K * (b - t) = integral {t..b} (\<lambda>_. K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K * (b - t) = integral {t..b} (\<lambda>_. K)
[PROOF STEP]
using \<open>t \<in> {a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}

goal (1 subgoal):
 1. K * (b - t) = integral {t..b} (\<lambda>_. K)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
K * (b - t) = integral {t..b} (\<lambda>_. K)

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
K * (b - t) = integral {t..b} (\<lambda>_. K)

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
have "... \<le> integral {t..b} (\<lambda>t. g' t / g t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {t..b} (\<lambda>_. K) \<le> integral {t..b} (\<lambda>t. g' t / g t)
[PROOF STEP]
using \<open>t \<in> {a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}

goal (1 subgoal):
 1. integral {t..b} (\<lambda>_. K) \<le> integral {t..b} (\<lambda>t. g' t / g t)
[PROOF STEP]
by (intro integral_le) (auto intro!: frac_integrable frac_ge integral_le)
[PROOF STATE]
proof (state)
this:
integral {t..b} (\<lambda>_. K) \<le> integral {t..b} (\<lambda>t. g' t / g t)

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {t..b} (\<lambda>_. K) \<le> integral {t..b} (\<lambda>t. g' t / g t)

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
have "... = ln (g b) - ln (g t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {t..b} (\<lambda>t. g' t / g t) = ln (g b) - ln (g t)
[PROOF STEP]
using * t_in
[PROOF STATE]
proof (prove)
using this:
?t \<in> {a..b} \<Longrightarrow> ln (g b) - ln (g ?t) = integral {?t..b} (\<lambda>t. g' t / g t)
t \<in> {a..b}

goal (1 subgoal):
 1. integral {t..b} (\<lambda>t. g' t / g t) = ln (g b) - ln (g t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
integral {t..b} (\<lambda>t. g' t / g t) = ln (g b) - ln (g t)

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
K * (b - t) \<le> ln (g b) - ln (g t)
[PROOF STEP]
have "K * (b - t) + ln (g t) \<le> ln (g b)" (is "?lhs \<le> ?rhs")
[PROOF STATE]
proof (prove)
using this:
K * (b - t) \<le> ln (g b) - ln (g t)

goal (1 subgoal):
 1. K * (b - t) + ln (g t) \<le> ln (g b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
K * (b - t) + ln (g t) \<le> ln (g b)

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
hence "exp ?lhs \<le> exp ?rhs"
[PROOF STATE]
proof (prove)
using this:
K * (b - t) + ln (g t) \<le> ln (g b)

goal (1 subgoal):
 1. exp (K * (b - t) + ln (g t)) \<le> exp (ln (g b))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exp (K * (b - t) + ln (g t)) \<le> exp (ln (g b))

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
hence "g t * exp (K * (b - t)) \<le> g b"
[PROOF STATE]
proof (prove)
using this:
exp (K * (b - t) + ln (g t)) \<le> exp (ln (g b))

goal (1 subgoal):
 1. g t * exp (K * (b - t)) \<le> g b
[PROOF STEP]
using \<open>t \<in> {a..b}\<close> g_pos
[PROOF STATE]
proof (prove)
using this:
exp (K * (b - t) + ln (g t)) \<le> exp (ln (g b))
t \<in> {a..b}
?t \<in> {a..b} \<Longrightarrow> 0 < g ?t

goal (1 subgoal):
 1. g t * exp (K * (b - t)) \<le> g b
[PROOF STEP]
by (simp add: ac_simps exp_add del: exp_le_cancel_iff)
[PROOF STATE]
proof (state)
this:
g t * exp (K * (b - t)) \<le> g b

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
hence "g t / exp (K * (t - b)) \<le> g b"
[PROOF STATE]
proof (prove)
using this:
g t * exp (K * (b - t)) \<le> g b

goal (1 subgoal):
 1. g t / exp (K * (t - b)) \<le> g b
[PROOF STEP]
by (simp add: algebra_simps exp_diff)
[PROOF STATE]
proof (state)
this:
g t / exp (K * (t - b)) \<le> g b

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
g t / exp (K * (t - b)) \<le> g b

goal (1 subgoal):
 1. g t \<le> g b * exp (K * (t - b))
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
g t \<le> g b * exp (K * (t - b))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gronwall_general:
  fixes g K C a b and t::real
  defines "G \<equiv> \<lambda>t. C + K * integral {a..t} (\<lambda>s. g s)"
  assumes g_le_G: "\<And>t. t \<in> {a..b} \<Longrightarrow> g t \<le> G t"
  assumes g_cont: "continuous_on {a..b} g"
  assumes g_nonneg: "\<And>t. t \<in> {a..b} \<Longrightarrow> 0 \<le> g t"
  assumes pos: "0 < C" "K > 0"
  assumes "t \<in> {a..b}"
  shows "g t \<le> C * exp (K * (t - a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
have G_pos: "\<And>t. t \<in> {a..b} \<Longrightarrow> 0 < G t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> 0 < G t
[PROOF STEP]
by (auto simp: G_def intro!: add_pos_nonneg mult_nonneg_nonneg Henstock_Kurzweil_Integration.integral_nonneg
      integrable_continuous_real assms intro: less_imp_le continuous_on_subset)
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> 0 < G ?t

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
have "g t \<le> G t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> G t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
G \<equiv> \<lambda>t. C + K * integral {a..t} g
?t \<in> {a..b} \<Longrightarrow> g ?t \<le> G ?t
continuous_on {a..b} g
?t \<in> {a..b} \<Longrightarrow> 0 \<le> g ?t
0 < C
0 < K
t \<in> {a..b}

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

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
g t \<le> G t

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
g t \<le> G t

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
have "(G has_vderiv_on (\<lambda>t. K * g t)) {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G has_vderiv_on (\<lambda>t. K * g t)) {a..b}
[PROOF STEP]
by (auto intro!: derivative_eq_intros integral_has_vector_derivative g_cont
        simp add: G_def has_vderiv_on_def)
[PROOF STATE]
proof (state)
this:
(G has_vderiv_on (\<lambda>t. K * g t)) {a..b}

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(G has_vderiv_on (\<lambda>t. K * g t)) {a..b}

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(G has_vderiv_on (\<lambda>t. K * g t)) {a..b}

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
assume "t \<in> {a..b}"
[PROOF STATE]
proof (state)
this:
t \<in> {a..b}

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
hence "K * g t / G t \<le> K * G t / G t"
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}

goal (1 subgoal):
 1. K * g t / G t \<le> K * G t / G t
[PROOF STEP]
using pos g_le_G G_pos
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}
0 < C
0 < K
?t \<in> {a..b} \<Longrightarrow> g ?t \<le> G ?t
?t \<in> {a..b} \<Longrightarrow> 0 < G ?t

goal (1 subgoal):
 1. K * g t / G t \<le> K * G t / G t
[PROOF STEP]
by (intro divide_right_mono mult_left_mono) (auto intro!: less_imp_le)
[PROOF STATE]
proof (state)
this:
K * g t / G t \<le> K * G t / G t

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
K * g t / G t \<le> K * G t / G t

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
have "\<dots> = K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K * G t / G t = K
[PROOF STEP]
using G_pos[of t] \<open>t \<in> {a .. b}\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b} \<Longrightarrow> 0 < G t
t \<in> {a..b}

goal (1 subgoal):
 1. K * G t / G t = K
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
K * G t / G t = K

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
K * g t / G t \<le> K
[PROOF STEP]
have "K * g t / G t \<le> K"
[PROOF STATE]
proof (prove)
using this:
K * g t / G t \<le> K

goal (1 subgoal):
 1. K * g t / G t \<le> K
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
K * g t / G t \<le> K

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?ta2 \<in> {a..b} \<Longrightarrow> K * g ?ta2 / G ?ta2 \<le> K

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(G has_vderiv_on (\<lambda>t. K * g t)) {a..b}
?ta2 \<in> {a..b} \<Longrightarrow> K * g ?ta2 / G ?ta2 \<le> K
[PROOF STEP]
have "G t \<le> G a * exp (K * (t - a))"
[PROOF STATE]
proof (prove)
using this:
(G has_vderiv_on (\<lambda>t. K * g t)) {a..b}
?ta2 \<in> {a..b} \<Longrightarrow> K * g ?ta2 / G ?ta2 \<le> K

goal (1 subgoal):
 1. G t \<le> G a * exp (K * (t - a))
[PROOF STEP]
apply (rule derivative_quotient_bound)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> t \<in> {a..b}
 2. continuous_on {a..b} (\<lambda>t. K * g t)
 3. \<And>t. t \<in> {a..b} \<Longrightarrow> 0 < G t
 4. t \<in> {a..b}
[PROOF STEP]
using \<open>t \<in> {a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}

goal (4 subgoals):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> t \<in> {a..b}
 2. continuous_on {a..b} (\<lambda>t. K * g t)
 3. \<And>t. t \<in> {a..b} \<Longrightarrow> 0 < G t
 4. t \<in> {a..b}
[PROOF STEP]
by (auto intro!: continuous_intros g_cont G_pos simp: field_simps pos)
[PROOF STATE]
proof (state)
this:
G t \<le> G a * exp (K * (t - a))

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
G t \<le> G a * exp (K * (t - a))

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
G t \<le> G a * exp (K * (t - a))

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
have "G a = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G a = C
[PROOF STEP]
by (simp add: G_def)
[PROOF STATE]
proof (state)
this:
G a = C

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
g t \<le> C * exp (K * (t - a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g t \<le> C * exp (K * (t - a))

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g t \<le> C * exp (K * (t - a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gronwall_general_left:
  fixes g K C a b and t::real
  defines "G \<equiv> \<lambda>t. C + K * integral {t..b} (\<lambda>s. g s)"
  assumes g_le_G: "\<And>t. t \<in> {a..b} \<Longrightarrow> g t \<le> G t"
  assumes g_cont: "continuous_on {a..b} g"
  assumes g_nonneg: "\<And>t. t \<in> {a..b} \<Longrightarrow> 0 \<le> g t"
  assumes pos: "0 < C" "K > 0"
  assumes "t \<in> {a..b}"
  shows "g t \<le> C * exp (-K * (t - b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
have G_pos: "\<And>t. t \<in> {a..b} \<Longrightarrow> 0 < G t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> 0 < G t
[PROOF STEP]
by (auto simp: G_def intro!: add_pos_nonneg mult_nonneg_nonneg Henstock_Kurzweil_Integration.integral_nonneg
      integrable_continuous_real assms intro: less_imp_le continuous_on_subset)
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> 0 < G ?t

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
have "g t \<le> G t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> G t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
G \<equiv> \<lambda>t. C + K * integral {t..b} g
?t \<in> {a..b} \<Longrightarrow> g ?t \<le> G ?t
continuous_on {a..b} g
?t \<in> {a..b} \<Longrightarrow> 0 \<le> g ?t
0 < C
0 < K
t \<in> {a..b}

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

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
g t \<le> G t

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
g t \<le> G t

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
have "(G has_vderiv_on (\<lambda>t. -K * g t)) {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G has_vderiv_on (\<lambda>t. - K * g t)) {a..b}
[PROOF STEP]
by (auto intro!: derivative_eq_intros g_cont integral_has_vector_derivative'
          simp add: G_def has_vderiv_on_def)
[PROOF STATE]
proof (state)
this:
(G has_vderiv_on (\<lambda>t. - K * g t)) {a..b}

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(G has_vderiv_on (\<lambda>t. - K * g t)) {a..b}

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(G has_vderiv_on (\<lambda>t. - K * g t)) {a..b}

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
assume "t \<in> {a..b}"
[PROOF STATE]
proof (state)
this:
t \<in> {a..b}

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
hence "K * g t / G t \<le> K * G t / G t"
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}

goal (1 subgoal):
 1. K * g t / G t \<le> K * G t / G t
[PROOF STEP]
using pos g_le_G G_pos
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}
0 < C
0 < K
?t \<in> {a..b} \<Longrightarrow> g ?t \<le> G ?t
?t \<in> {a..b} \<Longrightarrow> 0 < G ?t

goal (1 subgoal):
 1. K * g t / G t \<le> K * G t / G t
[PROOF STEP]
by (intro divide_right_mono mult_left_mono) (auto intro!: less_imp_le)
[PROOF STATE]
proof (state)
this:
K * g t / G t \<le> K * G t / G t

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
K * g t / G t \<le> K * G t / G t

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
have "\<dots> = K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K * G t / G t = K
[PROOF STEP]
using G_pos[of t] \<open>t \<in> {a .. b}\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b} \<Longrightarrow> 0 < G t
t \<in> {a..b}

goal (1 subgoal):
 1. K * G t / G t = K
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
K * G t / G t = K

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
K * g t / G t \<le> K
[PROOF STEP]
have "K * g t / G t \<le> K"
[PROOF STATE]
proof (prove)
using this:
K * g t / G t \<le> K

goal (1 subgoal):
 1. K * g t / G t \<le> K
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
K * g t / G t \<le> K

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
hence "-K \<le> -K * g t / G t"
[PROOF STATE]
proof (prove)
using this:
K * g t / G t \<le> K

goal (1 subgoal):
 1. - K \<le> - K * g t / G t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- K \<le> - K * g t / G t

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?ta2 \<in> {a..b} \<Longrightarrow> - K \<le> - K * g ?ta2 / G ?ta2

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(G has_vderiv_on (\<lambda>t. - K * g t)) {a..b}
?ta2 \<in> {a..b} \<Longrightarrow> - K \<le> - K * g ?ta2 / G ?ta2
[PROOF STEP]
have "G t \<le> G b * exp (-K * (t - b))"
[PROOF STATE]
proof (prove)
using this:
(G has_vderiv_on (\<lambda>t. - K * g t)) {a..b}
?ta2 \<in> {a..b} \<Longrightarrow> - K \<le> - K * g ?ta2 / G ?ta2

goal (1 subgoal):
 1. G t \<le> G b * exp (- K * (t - b))
[PROOF STEP]
apply (rule derivative_quotient_bound_left)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> t \<in> {a..b}
 2. continuous_on {a..b} (\<lambda>t. - K * g t)
 3. \<And>t. t \<in> {a..b} \<Longrightarrow> 0 < G t
 4. t \<in> {a..b}
[PROOF STEP]
using \<open>t \<in> {a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}

goal (4 subgoals):
 1. \<And>t. t \<in> {a..b} \<Longrightarrow> t \<in> {a..b}
 2. continuous_on {a..b} (\<lambda>t. - K * g t)
 3. \<And>t. t \<in> {a..b} \<Longrightarrow> 0 < G t
 4. t \<in> {a..b}
[PROOF STEP]
by (auto intro!: continuous_intros g_cont G_pos simp: field_simps pos)
[PROOF STATE]
proof (state)
this:
G t \<le> G b * exp (- K * (t - b))

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
G t \<le> G b * exp (- K * (t - b))

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
G t \<le> G b * exp (- K * (t - b))

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
have "G b = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G b = C
[PROOF STEP]
by (simp add: G_def)
[PROOF STATE]
proof (state)
this:
G b = C

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g t \<le> C * exp (- K * (t - b))

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - b))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g t \<le> C * exp (- K * (t - b))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gronwall_general_segment:
  fixes a b::real
  assumes "\<And>t. t \<in> closed_segment a b \<Longrightarrow> g t \<le> C + K * integral (closed_segment a t) g"
    and "continuous_on (closed_segment a b) g"
    and "\<And>t. t \<in> closed_segment a b \<Longrightarrow> 0 \<le> g t"
    and "0 < C"
    and "0 < K"
    and "t \<in> closed_segment a b"
  shows "g t \<le> C * exp (K * abs (t - a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
 2. \<not> ?P \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
assume "a \<le> b"
[PROOF STATE]
proof (state)
this:
a \<le> b

goal (2 subgoals):
 1. ?P \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
 2. \<not> ?P \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
[PROOF STEP]
have *: "abs (t - a) = t -a"
[PROOF STATE]
proof (prove)
using this:
a \<le> b

goal (1 subgoal):
 1. \<bar>t - a\<bar> = t - a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<le> b
?t \<in> closed_segment a b \<Longrightarrow> g ?t \<le> C + K * integral (closed_segment a ?t) g
continuous_on (closed_segment a b) g
?t \<in> closed_segment a b \<Longrightarrow> 0 \<le> g ?t
0 < C
0 < K
t \<in> closed_segment a b

goal (1 subgoal):
 1. \<bar>t - a\<bar> = t - a
[PROOF STEP]
by (auto simp: closed_segment_eq_real_ivl)
[PROOF STATE]
proof (state)
this:
\<bar>t - a\<bar> = t - a

goal (2 subgoals):
 1. ?P \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
 2. \<not> ?P \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?t \<in> closed_segment a b \<Longrightarrow> g ?t \<le> C + K * integral (closed_segment a ?t) g
continuous_on (closed_segment a b) g
?t \<in> closed_segment a b \<Longrightarrow> 0 \<le> g ?t
0 < C
0 < K
t \<in> closed_segment a b

goal (1 subgoal):
 1. g t \<le> C * exp (K * (t - a))
[PROOF STEP]
by (intro gronwall_general[where b=b]) (auto intro!: simp: closed_segment_eq_real_ivl \<open>a \<le> b\<close>)
[PROOF STATE]
proof (state)
this:
g t \<le> C * exp (K * \<bar>t - a\<bar>)

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
assume "\<not>a \<le> b"
[PROOF STATE]
proof (state)
this:
\<not> a \<le> b

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> a \<le> b
[PROOF STEP]
have *: "K * abs (t - a) = - K * (t - a)"
[PROOF STATE]
proof (prove)
using this:
\<not> a \<le> b

goal (1 subgoal):
 1. K * \<bar>t - a\<bar> = - K * (t - a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> a \<le> b
?t \<in> closed_segment a b \<Longrightarrow> g ?t \<le> C + K * integral (closed_segment a ?t) g
continuous_on (closed_segment a b) g
?t \<in> closed_segment a b \<Longrightarrow> 0 \<le> g ?t
0 < C
0 < K
t \<in> closed_segment a b

goal (1 subgoal):
 1. K * \<bar>t - a\<bar> = - K * (t - a)
[PROOF STEP]
by (auto simp: closed_segment_eq_real_ivl algebra_simps)
[PROOF STATE]
proof (state)
this:
K * \<bar>t - a\<bar> = - K * (t - a)

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
K * \<bar>t - a\<bar> = - K * (t - a)

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
fix s :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
assume a1: "b \<le> s"
[PROOF STATE]
proof (state)
this:
b \<le> s

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
assume a2: "s \<le> a"
[PROOF STATE]
proof (state)
this:
s \<le> a

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
assume a3: "\<And>t. b \<le> t \<and> t \<le> a \<Longrightarrow> g t \<le> C + K * integral (if a \<le> t then {a..t} else {t..a}) g"
[PROOF STATE]
proof (state)
this:
b \<le> ?t \<and> ?t \<le> a \<Longrightarrow> g ?t \<le> C + K * integral (if a \<le> ?t then {a..?t} else {?t..a}) g

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
have "s = a \<or> s < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = a \<or> s < a
[PROOF STEP]
using a2
[PROOF STATE]
proof (prove)
using this:
s \<le> a

goal (1 subgoal):
 1. s = a \<or> s < a
[PROOF STEP]
by (meson less_eq_real_def)
[PROOF STATE]
proof (state)
this:
s = a \<or> s < a

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s = a \<or> s < a
[PROOF STEP]
have "g s \<le> C + K * integral {s..a} g"
[PROOF STATE]
proof (prove)
using this:
s = a \<or> s < a

goal (1 subgoal):
 1. g s \<le> C + K * integral {s..a} g
[PROOF STEP]
using a3 a1
[PROOF STATE]
proof (prove)
using this:
s = a \<or> s < a
b \<le> ?t \<and> ?t \<le> a \<Longrightarrow> g ?t \<le> C + K * integral (if a \<le> ?t then {a..?t} else {?t..a}) g
b \<le> s

goal (1 subgoal):
 1. g s \<le> C + K * integral {s..a} g
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
g s \<le> C + K * integral {s..a} g

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>b \<le> ?s2; ?s2 \<le> a; \<And>t. b \<le> t \<and> t \<le> a \<Longrightarrow> g t \<le> C + K * integral (if a \<le> t then {a..t} else {t..a}) g\<rbrakk> \<Longrightarrow> g ?s2 \<le> C + K * integral {?s2..a} g

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>b \<le> ?s2; ?s2 \<le> a; \<And>t. b \<le> t \<and> t \<le> a \<Longrightarrow> g t \<le> C + K * integral (if a \<le> t then {a..t} else {t..a}) g\<rbrakk> \<Longrightarrow> g ?s2 \<le> C + K * integral {?s2..a} g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b \<le> ?s2; ?s2 \<le> a; \<And>t. b \<le> t \<and> t \<le> a \<Longrightarrow> g t \<le> C + K * integral (if a \<le> t then {a..t} else {t..a}) g\<rbrakk> \<Longrightarrow> g ?s2 \<le> C + K * integral {?s2..a} g

goal (1 subgoal):
 1. g t \<le> C * exp (K * \<bar>t - a\<bar>)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b \<le> ?s2; ?s2 \<le> a; \<And>t. b \<le> t \<and> t \<le> a \<Longrightarrow> g t \<le> C + K * integral (if a \<le> t then {a..t} else {t..a}) g\<rbrakk> \<Longrightarrow> g ?s2 \<le> C + K * integral {?s2..a} g

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - a))
[PROOF STEP]
using assms  \<open>\<not>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b \<le> ?s2; ?s2 \<le> a; \<And>t. b \<le> t \<and> t \<le> a \<Longrightarrow> g t \<le> C + K * integral (if a \<le> t then {a..t} else {t..a}) g\<rbrakk> \<Longrightarrow> g ?s2 \<le> C + K * integral {?s2..a} g
?t \<in> closed_segment a b \<Longrightarrow> g ?t \<le> C + K * integral (closed_segment a ?t) g
continuous_on (closed_segment a b) g
?t \<in> closed_segment a b \<Longrightarrow> 0 \<le> g ?t
0 < C
0 < K
t \<in> closed_segment a b
\<not> a \<le> b

goal (1 subgoal):
 1. g t \<le> C * exp (- K * (t - a))
[PROOF STEP]
by (intro gronwall_general_left)
      (auto intro!: simp: closed_segment_eq_real_ivl)
[PROOF STATE]
proof (state)
this:
g t \<le> C * exp (K * \<bar>t - a\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gronwall_more_general_segment:
  fixes a b c::real
  assumes "\<And>t. t \<in> closed_segment a b \<Longrightarrow> g t \<le> C + K * integral (closed_segment c t) g"
    and cont: "continuous_on (closed_segment a b) g"
    and "\<And>t. t \<in> closed_segment a b \<Longrightarrow> 0 \<le> g t"
    and "0 < C"
    and "0 < K"
    and t: "t \<in> closed_segment a b"
    and c: "c \<in> closed_segment a b"
  shows "g t \<le> C * exp (K * abs (t - c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
from t c
[PROOF STATE]
proof (chain)
picking this:
t \<in> closed_segment a b
c \<in> closed_segment a b
[PROOF STEP]
have "t \<in> closed_segment c a \<or> t \<in> closed_segment c b"
[PROOF STATE]
proof (prove)
using this:
t \<in> closed_segment a b
c \<in> closed_segment a b

goal (1 subgoal):
 1. t \<in> closed_segment c a \<or> t \<in> closed_segment c b
[PROOF STEP]
by (auto simp: closed_segment_eq_real_ivl split_ifs)
[PROOF STATE]
proof (state)
this:
t \<in> closed_segment c a \<or> t \<in> closed_segment c b

goal (1 subgoal):
 1. g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> closed_segment c a \<or> t \<in> closed_segment c b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t \<in> closed_segment c a \<or> t \<in> closed_segment c b

goal (1 subgoal):
 1. g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<in> closed_segment c a \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
 2. t \<in> closed_segment c b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
assume "t \<in> closed_segment c a"
[PROOF STATE]
proof (state)
this:
t \<in> closed_segment c a

goal (2 subgoals):
 1. t \<in> closed_segment c a \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
 2. t \<in> closed_segment c b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t \<in> closed_segment c a

goal (2 subgoals):
 1. t \<in> closed_segment c a \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
 2. t \<in> closed_segment c b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
have subs: "closed_segment c a \<subseteq> closed_segment a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_segment c a \<subseteq> closed_segment a b
[PROOF STEP]
using t c
[PROOF STATE]
proof (prove)
using this:
t \<in> closed_segment a b
c \<in> closed_segment a b

goal (1 subgoal):
 1. closed_segment c a \<subseteq> closed_segment a b
[PROOF STEP]
by (auto simp: closed_segment_eq_real_ivl split_ifs)
[PROOF STATE]
proof (state)
this:
closed_segment c a \<subseteq> closed_segment a b

goal (2 subgoals):
 1. t \<in> closed_segment c a \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
 2. t \<in> closed_segment c b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t \<in> closed_segment c a
closed_segment c a \<subseteq> closed_segment a b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t \<in> closed_segment c a
closed_segment c a \<subseteq> closed_segment a b

goal (1 subgoal):
 1. g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
by (intro gronwall_general_segment[where b=a])
        (auto intro!: assms intro: continuous_on_subset)
[PROOF STATE]
proof (state)
this:
g t \<le> C * exp (K * \<bar>t - c\<bar>)

goal (1 subgoal):
 1. t \<in> closed_segment c b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> closed_segment c b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
assume "t \<in> closed_segment c b"
[PROOF STATE]
proof (state)
this:
t \<in> closed_segment c b

goal (1 subgoal):
 1. t \<in> closed_segment c b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
t \<in> closed_segment c b

goal (1 subgoal):
 1. t \<in> closed_segment c b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
have subs: "closed_segment c b \<subseteq> closed_segment a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_segment c b \<subseteq> closed_segment a b
[PROOF STEP]
using t c
[PROOF STATE]
proof (prove)
using this:
t \<in> closed_segment a b
c \<in> closed_segment a b

goal (1 subgoal):
 1. closed_segment c b \<subseteq> closed_segment a b
[PROOF STEP]
by (auto simp: closed_segment_eq_real_ivl)
[PROOF STATE]
proof (state)
this:
closed_segment c b \<subseteq> closed_segment a b

goal (1 subgoal):
 1. t \<in> closed_segment c b \<Longrightarrow> g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
t \<in> closed_segment c b
closed_segment c b \<subseteq> closed_segment a b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
t \<in> closed_segment c b
closed_segment c b \<subseteq> closed_segment a b

goal (1 subgoal):
 1. g t \<le> C * exp (K * \<bar>t - c\<bar>)
[PROOF STEP]
by (intro gronwall_general_segment[where b=b])
        (auto intro!: assms intro: continuous_on_subset)
[PROOF STATE]
proof (state)
this:
g t \<le> C * exp (K * \<bar>t - c\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g t \<le> C * exp (K * \<bar>t - c\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gronwall:
  fixes g K C and t::real
  defines "G \<equiv> \<lambda>t. C + K * integral {0..t} (\<lambda>s. g s)"
  assumes g_le_G: "\<And>t. 0 \<le> t \<Longrightarrow> t \<le> a \<Longrightarrow> g t \<le> G t"
  assumes g_cont: "continuous_on {0..a} g"
  assumes g_nonneg: "\<And>t. 0 \<le> t \<Longrightarrow> t \<le> a \<Longrightarrow> 0 \<le> g t"
  assumes pos: "0 < C" "0 < K"
  assumes "0 \<le> t" "t \<le> a"
  shows "g t \<le> C * exp (K * t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> C * exp (K * t)
[PROOF STEP]
apply(rule gronwall_general[where a=0, simplified, OF assms(2-6)[unfolded G_def]])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. 0 \<le> t \<and> t \<le> a \<Longrightarrow> 0 \<le> t
 2. \<And>t. 0 \<le> t \<and> t \<le> a \<Longrightarrow> t \<le> a
 3. \<And>t. 0 \<le> t \<and> t \<le> a \<Longrightarrow> 0 \<le> t
 4. \<And>t. 0 \<le> t \<and> t \<le> a \<Longrightarrow> t \<le> a
 5. 0 \<le> t \<and> t \<le> a
[PROOF STEP]
using assms(7,8)
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> a

goal (5 subgoals):
 1. \<And>t. 0 \<le> t \<and> t \<le> a \<Longrightarrow> 0 \<le> t
 2. \<And>t. 0 \<le> t \<and> t \<le> a \<Longrightarrow> t \<le> a
 3. \<And>t. 0 \<le> t \<and> t \<le> a \<Longrightarrow> 0 \<le> t
 4. \<And>t. 0 \<le> t \<and> t \<le> a \<Longrightarrow> t \<le> a
 5. 0 \<le> t \<and> t \<le> a
[PROOF STEP]
by simp_all


[STATEMENT]
lemma gronwall_left:
  fixes g K C and t::real
  defines "G \<equiv> \<lambda>t. C + K * integral {t..0} (\<lambda>s. g s)"
  assumes g_le_G: "\<And>t. a \<le> t \<Longrightarrow> t \<le> 0 \<Longrightarrow> g t \<le> G t"
  assumes g_cont: "continuous_on {a..0} g"
  assumes g_nonneg: "\<And>t. a \<le> t \<Longrightarrow> t \<le> 0 \<Longrightarrow> 0 \<le> g t"
  assumes pos: "0 < C" "0 < K"
  assumes "a \<le> t" "t \<le> 0"
  shows "g t \<le> C * exp (-K * t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<le> C * exp (- K * t)
[PROOF STEP]
apply(simp, rule gronwall_general_left[where b=0, simplified, OF assms(2-6)[unfolded G_def]])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>t. a \<le> t \<and> t \<le> 0 \<Longrightarrow> a \<le> t
 2. \<And>t. a \<le> t \<and> t \<le> 0 \<Longrightarrow> t \<le> 0
 3. \<And>t. a \<le> t \<and> t \<le> 0 \<Longrightarrow> a \<le> t
 4. \<And>t. a \<le> t \<and> t \<le> 0 \<Longrightarrow> t \<le> 0
 5. a \<le> t \<and> t \<le> 0
[PROOF STEP]
using assms(7,8)
[PROOF STATE]
proof (prove)
using this:
a \<le> t
t \<le> 0

goal (5 subgoals):
 1. \<And>t. a \<le> t \<and> t \<le> 0 \<Longrightarrow> a \<le> t
 2. \<And>t. a \<le> t \<and> t \<le> 0 \<Longrightarrow> t \<le> 0
 3. \<And>t. a \<le> t \<and> t \<le> 0 \<Longrightarrow> a \<le> t
 4. \<And>t. a \<le> t \<and> t \<le> 0 \<Longrightarrow> t \<le> 0
 5. a \<le> t \<and> t \<le> 0
[PROOF STEP]
by simp_all


[STATEMENT]
lemma difind_difelem:
       "i < length xs \<Longrightarrow> distinct xs \<Longrightarrow> xs ! j = a \<Longrightarrow> j < length xs \<Longrightarrow> i \<noteq> j
          \<Longrightarrow> ~ a = xs ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; distinct xs; xs ! j = a; j < length xs; i \<noteq> j\<rbrakk> \<Longrightarrow> a \<noteq> xs ! i
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; distinct xs; xs ! j = a; j < length xs; i \<noteq> j; \<not> a \<noteq> xs ! i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(metis index_nth_id)


[STATEMENT]
lemma fullchar: assumes  "index xs q < length xs"
  shows
    "(i < length xs) =
  (index xs q < i \<and> i < length xs
    \<or> index xs q = i
    \<or> index xs q - n \<le> i \<and> i < index xs q
    \<or> i < index xs q - n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < length xs) = (index xs q < i \<and> i < length xs \<or> index xs q = i \<or> index xs q - n \<le> i \<and> i < index xs q \<or> i < index xs q - n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
index xs q < length xs

goal (1 subgoal):
 1. (i < length xs) = (index xs q < i \<and> i < length xs \<or> index xs q = i \<or> index xs q - n \<le> i \<and> i < index xs q \<or> i < index xs q - n)
[PROOF STEP]
by auto