[STATEMENT]
lemma  length_1_calculate_data_satisfies_properties_R:
  fixes p:: "real poly"
  fixes qs :: "real poly list"
  fixes subsets :: "(nat list*nat list) list"
  fixes signs :: "rat list list"
  assumes nonzero: "p \<noteq> 0"
  assumes len1: "length qs = 1"
  shows "satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
have h1: "all_list_constr_R  [([], []),([0], []),([], [0])] (length qs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_list_constr_R [([], []), ([0], []), ([], [0])] (length qs)
[PROOF STEP]
using len1
[PROOF STATE]
proof (prove)
using this:
length qs = 1

goal (1 subgoal):
 1. all_list_constr_R [([], []), ([0], []), ([], [0])] (length qs)
[PROOF STEP]
unfolding all_list_constr_R_def list_constr_def
[PROOF STATE]
proof (prove)
using this:
length qs = 1

goal (1 subgoal):
 1. \<forall>x. List.member [([], []), ([0], []), ([], [0])] x \<longrightarrow> list_all (\<lambda>x. x < length qs) (fst x) \<and> list_all (\<lambda>x. x < length qs) (snd x)
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>length qs = Suc 0; List.member [([], []), ([0], []), ([], [0])] (a, b)\<rbrakk> \<Longrightarrow> list_all (\<lambda>x. x = 0) a
 2. \<And>a b. \<lbrakk>length qs = Suc 0; List.member [([], []), ([0], []), ([], [0])] (a, b)\<rbrakk> \<Longrightarrow> list_all (\<lambda>x. x = 0) b
[PROOF STEP]
apply (smt (verit, best) Ball_set in_set_member member_rec(1) member_rec(2) prod.inject)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>length qs = Suc 0; List.member [([], []), ([0], []), ([], [0])] (a, b)\<rbrakk> \<Longrightarrow> list_all (\<lambda>x. x = 0) b
[PROOF STEP]
by (smt (verit, ccfv_threshold) Ball_set in_set_member member_rec(1) member_rec(2) prod.inject)
[PROOF STATE]
proof (state)
this:
all_list_constr_R [([], []), ([0], []), ([], [0])] (length qs)

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
have h2: "well_def_signs (length qs) [[1],[-1]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. well_def_signs (length qs) [[1], [- 1]]
[PROOF STEP]
unfolding well_def_signs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>signs\<in>set [[1], [- 1]]. length signs = length qs
[PROOF STEP]
using len1 in_set_member
[PROOF STATE]
proof (prove)
using this:
length qs = 1
(?x \<in> set ?xs) = List.member ?xs ?x

goal (1 subgoal):
 1. \<forall>signs\<in>set [[1], [- 1]]. length signs = length qs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_def_signs (length qs) [[1], [- 1]]

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
have h3: "distinct ([[1],[0],[-1]]::rat list list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct [[1], [0], [- 1]]
[PROOF STEP]
unfolding distinct_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_list True (\<lambda>x xs. (\<and>) (x \<notin> set xs)) [[1], [0], [- 1]]
[PROOF STEP]
using in_set_member
[PROOF STATE]
proof (prove)
using this:
(?x \<in> set ?xs) = List.member ?xs ?x

goal (1 subgoal):
 1. rec_list True (\<lambda>x xs. (\<and>) (x \<notin> set xs)) [[1], [0], [- 1]]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct [[1], [0], [- 1]]

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
have h4: "satisfy_equation_R p qs [([], []),([0], []),([], [0])] [[1],[0],[-1]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. satisfy_equation_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]]
[PROOF STEP]
using assms base_case_satisfy_equation_alt_R[of qs p]
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0
length qs = 1
\<lbrakk>length qs = 1; p \<noteq> 0\<rbrakk> \<Longrightarrow> satisfy_equation_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]]

goal (1 subgoal):
 1. satisfy_equation_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
satisfy_equation_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]]

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
have h6: "(mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]::rat mat) = (matrix_A_R ([[1],[0],[-1]]) ([([], []),([0], []),([], [0])]) :: rat mat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]] = M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]
[PROOF STEP]
using mat_base_case_R
[PROOF STATE]
proof (prove)
using this:
M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])] = mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]]

goal (1 subgoal):
 1. mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]] = M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]] = M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]] = M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]
[PROOF STEP]
have h5: "invertible_mat (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]::rat mat)"
[PROOF STATE]
proof (prove)
using this:
mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]] = M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]

goal (1 subgoal):
 1. invertible_mat (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])
[PROOF STEP]
using base_case_invertible_mat_R
[PROOF STATE]
proof (prove)
using this:
mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]] = M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]
invertible_mat (M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])])

goal (1 subgoal):
 1. invertible_mat (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invertible_mat (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
have h7:  "set (characterize_consistent_signs_at_roots p qs) \<subseteq> set ([[1],[0],[-1]])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (characterize_consistent_signs_at_roots p qs) \<subseteq> set [[1], [0], [- 1]]
[PROOF STEP]
using assms base_case_sgas_alt_R[of qs p]
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0
length qs = 1
\<lbrakk>length qs = 1; p \<noteq> 0\<rbrakk> \<Longrightarrow> set (characterize_consistent_signs_at_roots p qs) \<subseteq> {[1], [0], [- 1]}

goal (1 subgoal):
 1. set (characterize_consistent_signs_at_roots p qs) \<subseteq> set [[1], [0], [- 1]]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (characterize_consistent_signs_at_roots p qs) \<subseteq> set [[1], [0], [- 1]]

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
have base_case_hyp: "satisfies_properties_R p qs [([], []),([0], []),([], [0])] [[1],[0],[-1]] (mat_of_rows_list 3 [[1,1,1], [0,1,0], [1,0,-1]]::rat mat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. satisfies_properties_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]] (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])
[PROOF STEP]
using h1 h2 h3 h4 h5 h6 h7
[PROOF STATE]
proof (prove)
using this:
all_list_constr_R [([], []), ([0], []), ([], [0])] (length qs)
well_def_signs (length qs) [[1], [- 1]]
distinct [[1], [0], [- 1]]
satisfy_equation_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]]
invertible_mat (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])
mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]] = M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]
set (characterize_consistent_signs_at_roots p qs) \<subseteq> set [[1], [0], [- 1]]

goal (1 subgoal):
 1. satisfies_properties_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]] (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])
[PROOF STEP]
using satisfies_properties_R_def
[PROOF STATE]
proof (prove)
using this:
all_list_constr_R [([], []), ([0], []), ([], [0])] (length qs)
well_def_signs (length qs) [[1], [- 1]]
distinct [[1], [0], [- 1]]
satisfy_equation_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]]
invertible_mat (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])
mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]] = M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]
set (characterize_consistent_signs_at_roots p qs) \<subseteq> set [[1], [0], [- 1]]
satisfies_properties_R ?p ?qs ?subsets ?signs ?matrix = (all_list_constr_R ?subsets (length ?qs) \<and> well_def_signs (length ?qs) ?signs \<and> distinct ?signs \<and> satisfy_equation_R ?p ?qs ?subsets ?signs \<and> invertible_mat ?matrix \<and> ?matrix = M_mat_R ?signs ?subsets \<and> set (characterize_consistent_signs_at_roots ?p ?qs) \<subseteq> set ?signs)

goal (1 subgoal):
 1. satisfies_properties_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]] (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>all_list_constr_R [([], []), ([0], []), ([], [0])] (length qs); well_def_signs (length qs) [[1], [- 1]]; satisfy_equation_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]]; invertible_mat (M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]); mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]] = M_mat_R [[1], [0], [- 1]] [([], []), ([0], []), ([], [0])]; set (characterize_consistent_signs_at_roots p qs) \<subseteq> {[1], [0], [- 1]}; \<And>p qs subsets signs matrix. satisfies_properties_R p qs subsets signs matrix = (all_list_constr_R subsets (length qs) \<and> well_def_signs (length qs) signs \<and> distinct signs \<and> satisfy_equation_R p qs subsets signs \<and> invertible_mat matrix \<and> matrix = M_mat_R signs subsets \<and> set (characterize_consistent_signs_at_roots p qs) \<subseteq> set signs)\<rbrakk> \<Longrightarrow> well_def_signs (length qs) [[1], [0], [- 1]]
[PROOF STEP]
by (simp add: well_def_signs_def)
[PROOF STATE]
proof (state)
this:
satisfies_properties_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]] (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
satisfies_properties_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]] (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])
[PROOF STEP]
have key_hyp: "satisfies_properties_R p qs (get_subsets_R (reduce_system_R p (qs,base_case_info_R))) (get_signs_R (reduce_system_R p (qs,base_case_info_R))) (get_matrix_R (reduce_system_R p (qs,base_case_info_R)))"
[PROOF STATE]
proof (prove)
using this:
satisfies_properties_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]] (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (reduce_system_R p (qs, base_case_info_R))) (get_signs_R (reduce_system_R p (qs, base_case_info_R))) (get_matrix_R (reduce_system_R p (qs, base_case_info_R)))
[PROOF STEP]
using reducing_sys_satisfies_properties_R
[PROOF STATE]
proof (prove)
using this:
satisfies_properties_R p qs [([], []), ([0], []), ([], [0])] [[1], [0], [- 1]] (mat_of_rows_list 3 [[1, 1, 1], [0, 1, 0], [1, 0, - 1]])
\<lbrakk>?p \<noteq> 0; 0 < length ?qs; satisfies_properties_R ?p ?qs ?subsets ?signs ?matrix\<rbrakk> \<Longrightarrow> satisfies_properties_R ?p ?qs (get_subsets_R (reduce_system_R ?p (?qs, ?matrix, ?subsets, ?signs))) (get_signs_R (reduce_system_R ?p (?qs, ?matrix, ?subsets, ?signs))) (get_matrix_R (reduce_system_R ?p (?qs, ?matrix, ?subsets, ?signs)))

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (reduce_system_R p (qs, base_case_info_R))) (get_signs_R (reduce_system_R p (qs, base_case_info_R))) (get_matrix_R (reduce_system_R p (qs, base_case_info_R)))
[PROOF STEP]
by (metis base_case_info_R_def len1 nonzero nonzero zero_less_one_class.zero_less_one)
[PROOF STATE]
proof (state)
this:
satisfies_properties_R p qs (get_subsets_R (reduce_system_R p (qs, base_case_info_R))) (get_signs_R (reduce_system_R p (qs, base_case_info_R))) (get_matrix_R (reduce_system_R p (qs, base_case_info_R)))

goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))
[PROOF STEP]
by (simp add: key_hyp len1)
[PROOF STATE]
proof (state)
this:
satisfies_properties_R p qs (get_subsets_R (calculate_data_R p qs)) (get_signs_R (calculate_data_R p qs)) (get_matrix_R (calculate_data_R p qs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subset_eq_imp_le_multiset:
  shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<subseteq># N \<Longrightarrow> M \<le> N
[PROOF STEP]
unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<subseteq># N \<Longrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x>y. count M x < count N x)) \<or> M = N
[PROOF STEP]
by (simp add: less_le_not_le subseteq_mset_def)


[STATEMENT]
lemma absolutely_integrable_continuous:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  shows "continuous_on (cbox a b) f \<Longrightarrow> f absolutely_integrable_on cbox a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on (cbox a b) f \<Longrightarrow> f absolutely_integrable_on cbox a b
[PROOF STEP]
using absolutely_integrable_integrable_bound
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> ?S \<Longrightarrow> norm (?f x) \<le> ?g x; ?f integrable_on ?S; ?g integrable_on ?S\<rbrakk> \<Longrightarrow> ?f absolutely_integrable_on ?S

goal (1 subgoal):
 1. continuous_on (cbox a b) f \<Longrightarrow> f absolutely_integrable_on cbox a b
[PROOF STEP]
by (simp add: absolutely_integrable_on_def continuous_on_norm integrable_continuous)


[STATEMENT]
lemma not_dvd_imp_mod_neq_0:
  \<open>a mod b \<noteq> 0\<close> if \<open>\<not> b dvd a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod b \<noteq> (0::'a)
[PROOF STEP]
using that mod_0_imp_dvd [of a b]
[PROOF STATE]
proof (prove)
using this:
\<not> b dvd a
a mod b = (0::'a) \<Longrightarrow> b dvd a

goal (1 subgoal):
 1. a mod b \<noteq> (0::'a)
[PROOF STEP]
by blast


[STATEMENT]
lemma synthetic_divmod_0 [simp]: "synthetic_divmod 0 c = (0, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. synthetic_divmod 0 c = (0, 0::'a)
[PROOF STEP]
by (simp add: synthetic_divmod_def)


[STATEMENT]
lemma lemma_order_pderiv1:
  "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q +
    smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv ([:- a, 1::'a:] ^ Suc n * q) = [:- a, 1::'a:] ^ Suc n * pderiv q + smult (of_nat (Suc n)) (q * [:- a, 1::'a:] ^ n)
[PROOF STEP]
by (simp only: pderiv_mult pderiv_power_Suc) (simp del: power_Suc of_nat_Suc add: pderiv_pCons)


[STATEMENT]
lemma multp\<^sub>D\<^sub>M_imp_multp:
  "multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N
[PROOF STEP]
assume "multp\<^sub>D\<^sub>M r M N"
[PROOF STATE]
proof (state)
this:
multp\<^sub>D\<^sub>M r M N

goal (1 subgoal):
 1. multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
multp\<^sub>D\<^sub>M r M N
[PROOF STEP]
obtain X Y where
    "X \<noteq> {#}" and "X \<subseteq># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)"
[PROOF STATE]
proof (prove)
using this:
multp\<^sub>D\<^sub>M r M N

goal (1 subgoal):
 1. (\<And>X Y. \<lbrakk>X \<noteq> {#}; X \<subseteq># N; M = N - X + Y; \<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding multp\<^sub>D\<^sub>M_def
[PROOF STATE]
proof (prove)
using this:
\<exists>X Y. X \<noteq> {#} \<and> X \<subseteq># N \<and> M = N - X + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a))

goal (1 subgoal):
 1. (\<And>X Y. \<lbrakk>X \<noteq> {#}; X \<subseteq># N; M = N - X + Y; \<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X \<noteq> {#}
X \<subseteq># N
M = N - X + Y
\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)

goal (1 subgoal):
 1. multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<noteq> {#}
X \<subseteq># N
M = N - X + Y
\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)
[PROOF STEP]
have "multp r (N - X + Y) (N - X + X)"
[PROOF STATE]
proof (prove)
using this:
X \<noteq> {#}
X \<subseteq># N
M = N - X + Y
\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> r k a)

goal (1 subgoal):
 1. multp r (N - X + Y) (N - X + X)
[PROOF STEP]
by (intro one_step_implies_multp) (auto simp: Bex_def trans_def)
[PROOF STATE]
proof (state)
this:
multp r (N - X + Y) (N - X + X)

goal (1 subgoal):
 1. multp\<^sub>D\<^sub>M r M N \<Longrightarrow> multp r M N
[PROOF STEP]
with \<open>M = N - X + Y\<close> \<open>X \<subseteq># N\<close>
[PROOF STATE]
proof (chain)
picking this:
M = N - X + Y
X \<subseteq># N
multp r (N - X + Y) (N - X + X)
[PROOF STEP]
show "multp r M N"
[PROOF STATE]
proof (prove)
using this:
M = N - X + Y
X \<subseteq># N
multp r (N - X + Y) (N - X + X)

goal (1 subgoal):
 1. multp r M N
[PROOF STEP]
by (metis subset_mset.diff_add)
[PROOF STATE]
proof (state)
this:
multp r M N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_transp:
  "transp R1 \<Longrightarrow> transp R2 \<Longrightarrow> transp (rel_sum R1 R2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transp R1; transp R2\<rbrakk> \<Longrightarrow> transp (rel_sum R1 R2)
[PROOF STEP]
unfolding transp_def split_sum_all rel_sum_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y z. R1 x y \<longrightarrow> R1 y z \<longrightarrow> R1 x z; \<forall>x y z. R2 x y \<longrightarrow> R2 y z \<longrightarrow> R2 x z\<rbrakk> \<Longrightarrow> (\<forall>x. (\<forall>xa. (\<forall>xb. R1 x xa \<longrightarrow> R1 xa xb \<longrightarrow> R1 x xb) \<and> (\<forall>xb. R1 x xa \<longrightarrow> False \<longrightarrow> False)) \<and> (\<forall>xa. (\<forall>xa. False \<longrightarrow> False \<longrightarrow> R1 x xa) \<and> (\<forall>x. False \<longrightarrow> R2 xa x \<longrightarrow> False))) \<and> (\<forall>x. (\<forall>xa. (\<forall>x. False \<longrightarrow> R1 xa x \<longrightarrow> False) \<and> (\<forall>xa. False \<longrightarrow> False \<longrightarrow> R2 x xa)) \<and> (\<forall>xa. (\<forall>xb. R2 x xa \<longrightarrow> False \<longrightarrow> False) \<and> (\<forall>xb. R2 x xa \<longrightarrow> R2 xa xb \<longrightarrow> R2 x xb)))
[PROOF STEP]
by fast


[STATEMENT]
lemma drop_bit_half:
  "drop_bit n (a div 2) = drop_bit n a div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop_bit n (a div (2::'a)) = drop_bit n a div (2::'a)
[PROOF STEP]
by (induction n arbitrary: a) (simp_all add: drop_bit_Suc)


[STATEMENT]
lemma bit_push_bit_iff [bit_simps]:
  \<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> possible_bit TYPE('a) n \<and> bit a (n - m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (push_bit m a) n = (m \<le> n \<and> possible_bit TYPE('a) n \<and> bit a (n - m))
[PROOF STEP]
by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff possible_bit_def)


[STATEMENT]
lemma take_bit_int_less_exp [simp]:
  \<open>take_bit n k < 2 ^ n\<close> for k :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit n k < 2 ^ n
[PROOF STEP]
by (simp add: take_bit_eq_mod)


[STATEMENT]
lemma ceiling_less_zero [simp]: "\<lceil>x\<rceil> < 0 \<longleftrightarrow> x \<le> -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lceil>x\<rceil> < 0) = (x \<le> - (1::'a))
[PROOF STEP]
by (simp add: ceiling_less_iff)


[STATEMENT]
lemma has_integral_iff: "(f has_integral i) S \<longleftrightarrow> (f integrable_on S \<and> integral S f = i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_integral i) S = (f integrable_on S \<and> integral S f = i)
[PROOF STEP]
by blast


[STATEMENT]
lemma leibniz_rule:
  fixes f::"'a::banach \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::banach"
  assumes fx: "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow>
    ((\<lambda>x. f x t) has_derivative blinfun_apply (fx x t)) (at x within U)"
  assumes integrable_f2: "\<And>x. x \<in> U \<Longrightarrow> f x integrable_on cbox a b"
  assumes cont_fx: "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
  assumes [intro]: "x0 \<in> U"
  assumes "convex U"
  shows
    "((\<lambda>x. integral (cbox a b) (f x)) has_derivative integral (cbox a b) (fx x0)) (at x0 within U)"
    (is "(?F has_derivative ?dF) _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
 2. \<not> ?P \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
[PROOF STEP]
assume "content (cbox a b) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
content (cbox a b) \<noteq> 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
 2. \<not> ?P \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
content (cbox a b) \<noteq> 0
[PROOF STEP]
have ne: "cbox a b \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
content (cbox a b) \<noteq> 0

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
 2. \<not> ?P \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
[PROOF STEP]
note [continuous_intros] =
    continuous_on_compose2[OF cont_fx, where f="\<lambda>y. Pair x y" for x,
      unfolded split_beta fst_conv snd_conv]
[PROOF STATE]
proof (state)
this:
\<lbrakk>continuous_on ?s (Pair ?x3); Pair ?x3 ` ?s \<subseteq> U \<times> cbox a b\<rbrakk> \<Longrightarrow> continuous_on ?s (fx ?x3)

goal (2 subgoals):
 1. ?P \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
 2. \<not> ?P \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
[PROOF STEP]
proof (intro has_derivativeI bounded_linear_scaleR_left tendstoI, fold norm_conv_dist)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
have cont_f1: "\<And>t. t \<in> cbox a b \<Longrightarrow> continuous_on U (\<lambda>x. f x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> cbox a b \<Longrightarrow> continuous_on U (\<lambda>x. f x t)
[PROOF STEP]
by (auto simp: continuous_on_eq_continuous_within intro!: has_derivative_continuous fx)
[PROOF STATE]
proof (state)
this:
?t \<in> cbox a b \<Longrightarrow> continuous_on U (\<lambda>x. f x ?t)

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
note [continuous_intros] = continuous_on_compose2[OF cont_f1]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?t1 \<in> cbox a b; continuous_on ?s ?f; ?f ` ?s \<subseteq> U\<rbrakk> \<Longrightarrow> continuous_on ?s (\<lambda>x. f (?f x) ?t1)

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
fix e'::real
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
assume "e' > 0"
[PROOF STATE]
proof (state)
this:
0 < e'

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
define e where "e = e' / (content (cbox a b) + 1)"
[PROOF STATE]
proof (state)
this:
e = e' / (content (cbox a b) + 1)

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
have "e > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < e
[PROOF STEP]
using \<open>e' > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < e'

goal (1 subgoal):
 1. 0 < e
[PROOF STEP]
by (auto simp: e_def intro!: divide_pos_pos add_nonneg_pos)
[PROOF STATE]
proof (state)
this:
0 < e

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
from continuous_on_prod_compactE[OF cont_fx compact_cbox \<open>x0 \<in> U\<close> \<open>e > 0\<close>]
[PROOF STATE]
proof (chain)
picking this:
(\<And>X0. \<lbrakk>x0 \<in> X0; open X0; \<forall>x\<in>X0 \<inter> U. \<forall>t\<in>cbox a b. dist (case (x, t) of (x, t) \<Rightarrow> fx x t) (case (x0, t) of (x, t) \<Rightarrow> fx x t) \<le> e\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain X0 where X0: "x0 \<in> X0" "open X0"
      and fx_bound: "\<And>x t. x \<in> X0 \<inter> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> norm (fx x t - fx x0 t) \<le> e"
[PROOF STATE]
proof (prove)
using this:
(\<And>X0. \<lbrakk>x0 \<in> X0; open X0; \<forall>x\<in>X0 \<inter> U. \<forall>t\<in>cbox a b. dist (case (x, t) of (x, t) \<Rightarrow> fx x t) (case (x0, t) of (x, t) \<Rightarrow> fx x t) \<le> e\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>X0. \<lbrakk>x0 \<in> X0; open X0; \<And>x t. \<lbrakk>x \<in> X0 \<inter> U; t \<in> cbox a b\<rbrakk> \<Longrightarrow> norm (fx x t - fx x0 t) \<le> e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding split_beta fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
(\<And>X0. \<lbrakk>x0 \<in> X0; open X0; \<forall>x\<in>X0 \<inter> U. \<forall>t\<in>cbox a b. dist (fx x t) (fx x0 t) \<le> e\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>X0. \<lbrakk>x0 \<in> X0; open X0; \<And>x t. \<lbrakk>x \<in> X0 \<inter> U; t \<in> cbox a b\<rbrakk> \<Longrightarrow> norm (fx x t - fx x0 t) \<le> e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis dist_norm)
[PROOF STATE]
proof (state)
this:
x0 \<in> X0
open X0
\<lbrakk>?x \<in> X0 \<inter> U; ?t \<in> cbox a b\<rbrakk> \<Longrightarrow> norm (fx ?x ?t - fx x0 ?t) \<le> e

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
note eventually_closed_segment[OF \<open>open X0\<close> \<open>x0 \<in> X0\<close>, of U]
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
have "\<forall>\<^sub>F x in at x0 within U. x \<in> X0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x0 within U. x \<in> X0
[PROOF STEP]
using \<open>open X0\<close> \<open>x0 \<in> X0\<close> eventually_at_topological
[PROOF STATE]
proof (prove)
using this:
open X0
x0 \<in> X0
eventually ?P (at ?a within ?s) = (\<exists>S. open S \<and> ?a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> ?a \<longrightarrow> x \<in> ?s \<longrightarrow> ?P x))

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x0 within U. x \<in> X0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x0 within U. x \<in> X0

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x0 within U. x \<in> X0

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
have "\<forall>\<^sub>F x in at x0 within U. x \<noteq> x0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x0 within U. x \<noteq> x0
[PROOF STEP]
by (auto simp: eventually_at_filter)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x0 within U. x \<noteq> x0

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x0 within U. x \<noteq> x0

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
have "\<forall>\<^sub>F x in at x0 within U. x \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x0 within U. x \<in> U
[PROOF STEP]
by (auto simp: eventually_at_filter)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x0 within U. x \<in> U

goal (2 subgoals):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
 2. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0
\<forall>\<^sub>F x in at x0 within U. x \<in> X0
\<forall>\<^sub>F x in at x0 within U. x \<noteq> x0
\<forall>\<^sub>F x in at x0 within U. x \<in> U
[PROOF STEP]
show "\<forall>\<^sub>F x in at x0 within U. norm ((?F x - ?F x0 - ?dF (x - x0)) /\<^sub>R norm (x - x0)) < e'"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0
\<forall>\<^sub>F x in at x0 within U. x \<in> X0
\<forall>\<^sub>F x in at x0 within U. x \<noteq> x0
\<forall>\<^sub>F x in at x0 within U. x \<in> U

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
case (elim x)
[PROOF STATE]
proof (state)
this:
closed_segment x0 x \<subseteq> X0
x \<in> X0
x \<noteq> x0
x \<in> U

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
from elim
[PROOF STATE]
proof (chain)
picking this:
closed_segment x0 x \<subseteq> X0
x \<in> X0
x \<noteq> x0
x \<in> U
[PROOF STEP]
have "0 < norm (x - x0)"
[PROOF STATE]
proof (prove)
using this:
closed_segment x0 x \<subseteq> X0
x \<in> X0
x \<noteq> x0
x \<in> U

goal (1 subgoal):
 1. 0 < norm (x - x0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < norm (x - x0)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
have "closed_segment x0 x \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_segment x0 x \<subseteq> U
[PROOF STEP]
by (rule \<open>convex U\<close>[unfolded convex_contains_segment, rule_format, OF \<open>x0 \<in> U\<close> \<open>x \<in> U\<close>])
[PROOF STATE]
proof (state)
this:
closed_segment x0 x \<subseteq> U

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
from elim
[PROOF STATE]
proof (chain)
picking this:
closed_segment x0 x \<subseteq> X0
x \<in> X0
x \<noteq> x0
x \<in> U
[PROOF STEP]
have [intro]: "x \<in> U"
[PROOF STATE]
proof (prove)
using this:
closed_segment x0 x \<subseteq> X0
x \<in> X0
x \<noteq> x0
x \<in> U

goal (1 subgoal):
 1. x \<in> U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> U

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
have "?F x - ?F x0 - ?dF (x - x0) =
        integral (cbox a b) (\<lambda>y. f x y - f x0 y - fx x0 y (x - x0))"
        (is "_ = ?id")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0) = integral (cbox a b) (\<lambda>y. f x y - f x0 y - blinfun_apply (fx x0 y) (x - x0))
[PROOF STEP]
using \<open>x \<noteq> x0\<close>
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x0

goal (1 subgoal):
 1. integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0) = integral (cbox a b) (\<lambda>y. f x y - f x0 y - blinfun_apply (fx x0 y) (x - x0))
[PROOF STEP]
by (subst blinfun_apply_integral integral_diff,
            auto intro!: integrable_diff integrable_f2 continuous_intros
              intro: integrable_continuous)+
[PROOF STATE]
proof (state)
this:
integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0) = integral (cbox a b) (\<lambda>y. f x y - f x0 y - blinfun_apply (fx x0 y) (x - x0))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0) = integral (cbox a b) (\<lambda>y. f x y - f x0 y - blinfun_apply (fx x0 y) (x - x0))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0) = integral (cbox a b) (\<lambda>y. f x y - f x0 y - blinfun_apply (fx x0 y) (x - x0))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
assume t: "t \<in> (cbox a b)"
[PROOF STATE]
proof (state)
this:
t \<in> cbox a b

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
have seg: "\<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R (x - x0) \<in> X0 \<inter> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R (x - x0) \<in> X0 \<inter> U
[PROOF STEP]
using \<open>closed_segment x0 x \<subseteq> U\<close>
            \<open>closed_segment x0 x \<subseteq> X0\<close>
[PROOF STATE]
proof (prove)
using this:
closed_segment x0 x \<subseteq> U
closed_segment x0 x \<subseteq> X0

goal (1 subgoal):
 1. \<And>t. t \<in> {0..1} \<Longrightarrow> x0 + t *\<^sub>R (x - x0) \<in> X0 \<inter> U
[PROOF STEP]
by (force simp: closed_segment_def algebra_simps)
[PROOF STATE]
proof (state)
this:
?t \<in> {0..1} \<Longrightarrow> x0 + ?t *\<^sub>R (x - x0) \<in> X0 \<inter> U

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
from t
[PROOF STATE]
proof (chain)
picking this:
t \<in> cbox a b
[PROOF STEP]
have deriv:
          "((\<lambda>x. f x t) has_derivative (fx y t)) (at y within X0 \<inter> U)"
          if "y \<in> X0 \<inter> U" for y
[PROOF STATE]
proof (prove)
using this:
t \<in> cbox a b

goal (1 subgoal):
 1. ((\<lambda>x. f x t) has_derivative blinfun_apply (fx y t)) (at y within X0 \<inter> U)
[PROOF STEP]
unfolding has_vector_derivative_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
t \<in> cbox a b

goal (1 subgoal):
 1. ((\<lambda>x. f x t) has_derivative blinfun_apply (fx y t)) (at y within X0 \<inter> U)
[PROOF STEP]
using that \<open>x \<in> X0\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> cbox a b
y \<in> X0 \<inter> U
x \<in> X0

goal (1 subgoal):
 1. ((\<lambda>x. f x t) has_derivative blinfun_apply (fx y t)) (at y within X0 \<inter> U)
[PROOF STEP]
by (intro has_derivative_subset[OF fx]) auto
[PROOF STATE]
proof (state)
this:
?y \<in> X0 \<inter> U \<Longrightarrow> ((\<lambda>x. f x t) has_derivative blinfun_apply (fx ?y t)) (at ?y within X0 \<inter> U)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
have "\<And>x. x \<in> X0 \<inter> U \<Longrightarrow> onorm (blinfun_apply (fx x t) - (fx x0 t)) \<le> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> X0 \<inter> U \<Longrightarrow> onorm (blinfun_apply (fx x t) - blinfun_apply (fx x0 t)) \<le> e
[PROOF STEP]
using fx_bound t
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X0 \<inter> U; ?t \<in> cbox a b\<rbrakk> \<Longrightarrow> norm (fx ?x ?t - fx x0 ?t) \<le> e
t \<in> cbox a b

goal (1 subgoal):
 1. \<And>x. x \<in> X0 \<inter> U \<Longrightarrow> onorm (blinfun_apply (fx x t) - blinfun_apply (fx x0 t)) \<le> e
[PROOF STEP]
by (auto simp add: norm_blinfun_def fun_diff_def blinfun.bilinear_simps[symmetric])
[PROOF STATE]
proof (state)
this:
?x \<in> X0 \<inter> U \<Longrightarrow> onorm (blinfun_apply (fx ?x t) - blinfun_apply (fx x0 t)) \<le> e

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
from differentiable_bound_linearization[OF seg deriv this] X0
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>t. t \<in> {0..1} \<Longrightarrow> t \<in> {0..1}; \<And>x. x \<in> X0 \<inter> U \<Longrightarrow> x \<in> X0 \<inter> U; \<And>x. x \<in> X0 \<inter> U \<Longrightarrow> x \<in> X0 \<inter> U; x0 \<in> X0 \<inter> U\<rbrakk> \<Longrightarrow> norm (f x t - f x0 t - blinfun_apply (fx x0 t) (x - x0)) \<le> norm (x - x0) * e
x0 \<in> X0
open X0
[PROOF STEP]
have "norm (f x t - f x0 t - fx x0 t (x - x0)) \<le> e * norm (x - x0)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>t. t \<in> {0..1} \<Longrightarrow> t \<in> {0..1}; \<And>x. x \<in> X0 \<inter> U \<Longrightarrow> x \<in> X0 \<inter> U; \<And>x. x \<in> X0 \<inter> U \<Longrightarrow> x \<in> X0 \<inter> U; x0 \<in> X0 \<inter> U\<rbrakk> \<Longrightarrow> norm (f x t - f x0 t - blinfun_apply (fx x0 t) (x - x0)) \<le> norm (x - x0) * e
x0 \<in> X0
open X0

goal (1 subgoal):
 1. norm (f x t - f x0 t - blinfun_apply (fx x0 t) (x - x0)) \<le> e * norm (x - x0)
[PROOF STEP]
by (auto simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
norm (f x t - f x0 t - blinfun_apply (fx x0 t) (x - x0)) \<le> e * norm (x - x0)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?t2 \<in> cbox a b \<Longrightarrow> norm (f x ?t2 - f x0 ?t2 - blinfun_apply (fx x0 ?t2) (x - x0)) \<le> e * norm (x - x0)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?t2 \<in> cbox a b \<Longrightarrow> norm (f x ?t2 - f x0 ?t2 - blinfun_apply (fx x0 ?t2) (x - x0)) \<le> e * norm (x - x0)
[PROOF STEP]
have "norm ?id \<le> integral (cbox a b) (\<lambda>_. e * norm (x - x0))"
[PROOF STATE]
proof (prove)
using this:
?t2 \<in> cbox a b \<Longrightarrow> norm (f x ?t2 - f x0 ?t2 - blinfun_apply (fx x0 ?t2) (x - x0)) \<le> e * norm (x - x0)

goal (1 subgoal):
 1. norm (integral (cbox a b) (\<lambda>y. f x y - f x0 y - blinfun_apply (fx x0 y) (x - x0))) \<le> integral (cbox a b) (\<lambda>_. e * norm (x - x0))
[PROOF STEP]
by (intro integral_norm_bound_integral)
          (auto intro!: continuous_intros integrable_diff integrable_f2
            intro: integrable_continuous)
[PROOF STATE]
proof (state)
this:
norm (integral (cbox a b) (\<lambda>y. f x y - f x0 y - blinfun_apply (fx x0 y) (x - x0))) \<le> integral (cbox a b) (\<lambda>_. e * norm (x - x0))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (integral (cbox a b) (\<lambda>y. f x y - f x0 y - blinfun_apply (fx x0 y) (x - x0))) \<le> integral (cbox a b) (\<lambda>_. e * norm (x - x0))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
have "\<dots> = content (cbox a b) * e * norm (x - x0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral (cbox a b) (\<lambda>_. e * norm (x - x0)) = content (cbox a b) * e * norm (x - x0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
integral (cbox a b) (\<lambda>_. e * norm (x - x0)) = content (cbox a b) * e * norm (x - x0)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral (cbox a b) (\<lambda>_. e * norm (x - x0)) = content (cbox a b) * e * norm (x - x0)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
have "\<dots> < e' * norm (x - x0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. content (cbox a b) * e * norm (x - x0) < e' * norm (x - x0)
[PROOF STEP]
proof (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. content (cbox a b) * e < e'
[PROOF STEP]
show "content (cbox a b) * e < e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. content (cbox a b) * e < e'
[PROOF STEP]
using \<open>e' > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < e'

goal (1 subgoal):
 1. content (cbox a b) * e < e'
[PROOF STEP]
by (simp add: divide_simps e_def not_less)
[PROOF STATE]
proof (state)
this:
content (cbox a b) * e < e'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
content (cbox a b) * e * norm (x - x0) < e' * norm (x - x0)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm (integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) < e' * norm (x - x0)
[PROOF STEP]
have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)"
[PROOF STATE]
proof (prove)
using this:
norm (integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) < e' * norm (x - x0)

goal (1 subgoal):
 1. norm (integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) < e' * norm (x - x0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
norm (integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) < e' * norm (x - x0)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>closed_segment x0 x \<subseteq> X0; x \<in> X0; x \<noteq> x0; x \<in> U\<rbrakk> \<Longrightarrow> norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
norm (integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) < e' * norm (x - x0)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
norm (integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) < e' * norm (x - x0)

goal (1 subgoal):
 1. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'
[PROOF STEP]
by (auto simp: divide_simps)
[PROOF STATE]
proof (state)
this:
norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at x0 within U. norm ((integral (cbox a b) (f x) - integral (cbox a b) (f x0) - blinfun_apply (integral (cbox a b) (fx x0)) (x - x0)) /\<^sub>R norm (x - x0)) < e'

goal (1 subgoal):
 1. bounded_linear (blinfun_apply (integral (cbox a b) (fx x0)))
[PROOF STEP]
qed (rule blinfun.bounded_linear_right)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)

goal (1 subgoal):
 1. \<not> content (cbox a b) \<noteq> 0 \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (fx x0))) (at x0 within U)
[PROOF STEP]
qed (auto intro!: derivative_eq_intros simp: blinfun.bilinear_simps)


[STATEMENT]
lemma leibniz_rule_field_differentiable:
  fixes f::"'a::{real_normed_field, banach} \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'a"
  assumes "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>x. f x t) has_field_derivative fx x t) (at x within U)"
  assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
  assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
  assumes "x0 \<in> U" "convex U"
  shows "(\<lambda>x. integral (cbox a b) (f x)) field_differentiable at x0 within U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. integral (cbox a b) (f x)) field_differentiable at x0 within U
[PROOF STEP]
using leibniz_rule_field_derivative[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x t. \<lbrakk>x \<in> U; t \<in> cbox a b\<rbrakk> \<Longrightarrow> x \<in> U; \<And>x t. \<lbrakk>x \<in> U; t \<in> cbox a b\<rbrakk> \<Longrightarrow> t \<in> cbox a b; \<And>x. x \<in> U \<Longrightarrow> x \<in> U\<rbrakk> \<Longrightarrow> ((\<lambda>x. integral (cbox a b) (f x)) has_field_derivative integral (cbox a b) (fx x0)) (at x0 within U)

goal (1 subgoal):
 1. (\<lambda>x. integral (cbox a b) (f x)) field_differentiable at x0 within U
[PROOF STEP]
by (auto simp: field_differentiable_def)


[STATEMENT]
lemma has_integral_substitution_general:
  fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
  assumes s: "finite s" and le: "a \<le> b"
      and subset: "g ` {a..b} \<subseteq> {c..d}"
      and f [continuous_intros]: "continuous_on {c..d} f"
      and g [continuous_intros]: "continuous_on {a..b} g"
      and deriv [derivative_intros]:
              "\<And>x. x \<in> {a..b} - s \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
    shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f - integral {g b..g a} f)) {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
let ?F = "\<lambda>x. integral {c..g x} f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
have cont_int: "continuous_on {a..b} ?F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {a..b} (\<lambda>x. integral {c..g x} f)
[PROOF STEP]
by (rule continuous_on_compose2[OF _ g subset] indefinite_integral_continuous_1
          f integrable_continuous_real)+
[PROOF STATE]
proof (state)
this:
continuous_on {a..b} (\<lambda>x. integral {c..g x} f)

goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
have deriv: "(((\<lambda>x. integral {c..x} f) \<circ> g) has_vector_derivative g' x *\<^sub>R f (g x))
                 (at x within {a..b})" if "x \<in> {a..b} - s" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. integral {c..x} f) \<circ> g has_vector_derivative g' x *\<^sub>R f (g x)) (at x within {a..b})
[PROOF STEP]
proof (rule has_vector_derivative_eq_rhs [OF vector_diff_chain_within refl])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (g has_vector_derivative g' x) (at x within {a..b})
 2. ((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x)) (at (g x) within g ` {a..b})
[PROOF STEP]
show "(g has_vector_derivative g' x) (at x within {a..b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g has_vector_derivative g' x) (at x within {a..b})
[PROOF STEP]
using deriv has_real_derivative_iff_has_vector_derivative that
[PROOF STATE]
proof (prove)
using this:
?x \<in> {a..b} - s \<Longrightarrow> (g has_real_derivative g' ?x) (at ?x within {a..b})
(?f has_real_derivative ?y) ?F = (?f has_vector_derivative ?y) ?F
x \<in> {a..b} - s

goal (1 subgoal):
 1. (g has_vector_derivative g' x) (at x within {a..b})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(g has_vector_derivative g' x) (at x within {a..b})

goal (1 subgoal):
 1. ((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x)) (at (g x) within g ` {a..b})
[PROOF STEP]
show "((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x))
          (at (g x) within g ` {a..b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x)) (at (g x) within g ` {a..b})
[PROOF STEP]
using that le subset
[PROOF STATE]
proof (prove)
using this:
x \<in> {a..b} - s
a \<le> b
g ` {a..b} \<subseteq> {c..d}

goal (1 subgoal):
 1. ((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x)) (at (g x) within g ` {a..b})
[PROOF STEP]
by (blast intro: has_vector_derivative_within_subset integral_has_vector_derivative f)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x)) (at (g x) within g ` {a..b})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<in> {a..b} - s \<Longrightarrow> ((\<lambda>x. integral {c..x} f) \<circ> g has_vector_derivative g' ?x *\<^sub>R f (g ?x)) (at ?x within {a..b})

goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
have deriv: "(?F has_vector_derivative g' x *\<^sub>R f (g x))
                  (at x)" if "x \<in> {a..b} - (s \<union> {a,b})" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. integral {c..g x} f) has_vector_derivative g' x *\<^sub>R f (g x)) (at x)
[PROOF STEP]
using deriv[of x] that
[PROOF STATE]
proof (prove)
using this:
x \<in> {a..b} - s \<Longrightarrow> ((\<lambda>x. integral {c..x} f) \<circ> g has_vector_derivative g' x *\<^sub>R f (g x)) (at x within {a..b})
x \<in> {a..b} - (s \<union> {a, b})

goal (1 subgoal):
 1. ((\<lambda>x. integral {c..g x} f) has_vector_derivative g' x *\<^sub>R f (g x)) (at x)
[PROOF STEP]
by (simp add: at_within_Icc_at o_def)
[PROOF STATE]
proof (state)
this:
?x \<in> {a..b} - (s \<union> {a, b}) \<Longrightarrow> ((\<lambda>x. integral {c..g x} f) has_vector_derivative g' ?x *\<^sub>R f (g ?x)) (at ?x)

goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {c..g b} f - integral {c..g a} f) {a..b}
[PROOF STEP]
using le cont_int s deriv cont_int
[PROOF STATE]
proof (prove)
using this:
a \<le> b
continuous_on {a..b} (\<lambda>x. integral {c..g x} f)
finite s
?x \<in> {a..b} - (s \<union> {a, b}) \<Longrightarrow> ((\<lambda>x. integral {c..g x} f) has_vector_derivative g' ?x *\<^sub>R f (g ?x)) (at ?x)
continuous_on {a..b} (\<lambda>x. integral {c..g x} f)

goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {c..g b} f - integral {c..g a} f) {a..b}
[PROOF STEP]
by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all
[PROOF STATE]
proof (state)
this:
((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {c..g b} f - integral {c..g a} f) {a..b}

goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {c..g b} f - integral {c..g a} f) {a..b}

goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
from subset
[PROOF STATE]
proof (chain)
picking this:
g ` {a..b} \<subseteq> {c..d}
[PROOF STEP]
have "g x \<in> {c..d}" if "x \<in> {a..b}" for x
[PROOF STATE]
proof (prove)
using this:
g ` {a..b} \<subseteq> {c..d}

goal (1 subgoal):
 1. g x \<in> {c..d}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
g ` {a..b} \<subseteq> {c..d}
x \<in> {a..b}

goal (1 subgoal):
 1. g x \<in> {c..d}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x \<in> {a..b} \<Longrightarrow> g ?x \<in> {c..d}

goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
from this[of a] this[of b] le
[PROOF STATE]
proof (chain)
picking this:
a \<in> {a..b} \<Longrightarrow> g a \<in> {c..d}
b \<in> {a..b} \<Longrightarrow> g b \<in> {c..d}
a \<le> b
[PROOF STEP]
have cd: "c \<le> g a" "g b \<le> d" "c \<le> g b" "g a \<le> d"
[PROOF STATE]
proof (prove)
using this:
a \<in> {a..b} \<Longrightarrow> g a \<in> {c..d}
b \<in> {a..b} \<Longrightarrow> g b \<in> {c..d}
a \<le> b

goal (1 subgoal):
 1. (c \<le> g a &&& g b \<le> d) &&& c \<le> g b &&& g a \<le> d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<le> g a
g b \<le> d
c \<le> g b
g a \<le> d

goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
have "integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
 2. \<not> ?P \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
assume "g a \<le> g b"
[PROOF STATE]
proof (state)
this:
g a \<le> g b

goal (2 subgoals):
 1. ?P \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
 2. \<not> ?P \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
note le = le this
[PROOF STATE]
proof (state)
this:
a \<le> b
g a \<le> g b

goal (2 subgoals):
 1. ?P \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
 2. \<not> ?P \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
from cd
[PROOF STATE]
proof (chain)
picking this:
c \<le> g a
g b \<le> d
c \<le> g b
g a \<le> d
[PROOF STEP]
have "integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f"
[PROOF STATE]
proof (prove)
using this:
c \<le> g a
g b \<le> d
c \<le> g b
g a \<le> d

goal (1 subgoal):
 1. integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f
[PROOF STEP]
by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
[PROOF STATE]
proof (state)
this:
integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f

goal (2 subgoals):
 1. ?P \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
 2. \<not> ?P \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
with le
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
g a \<le> g b
integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<le> b
g a \<le> g b
integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f

goal (1 subgoal):
 1. integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
by (cases "g a = g b") (simp_all add: algebra_simps)
[PROOF STATE]
proof (state)
this:
integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f

goal (1 subgoal):
 1. \<not> g a \<le> g b \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> g a \<le> g b \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
assume less: "\<not>g a \<le> g b"
[PROOF STATE]
proof (state)
this:
\<not> g a \<le> g b

goal (1 subgoal):
 1. \<not> g a \<le> g b \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> g a \<le> g b
[PROOF STEP]
have "g a \<ge> g b"
[PROOF STATE]
proof (prove)
using this:
\<not> g a \<le> g b

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

goal (1 subgoal):
 1. \<not> g a \<le> g b \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
note le = le this
[PROOF STATE]
proof (state)
this:
a \<le> b
g b \<le> g a

goal (1 subgoal):
 1. \<not> g a \<le> g b \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
from cd
[PROOF STATE]
proof (chain)
picking this:
c \<le> g a
g b \<le> d
c \<le> g b
g a \<le> d
[PROOF STEP]
have "integral {c..g b} f + integral {g b..g a} f = integral {c..g a} f"
[PROOF STATE]
proof (prove)
using this:
c \<le> g a
g b \<le> d
c \<le> g b
g a \<le> d

goal (1 subgoal):
 1. integral {c..g b} f + integral {g b..g a} f = integral {c..g a} f
[PROOF STEP]
by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
[PROOF STATE]
proof (state)
this:
integral {c..g b} f + integral {g b..g a} f = integral {c..g a} f

goal (1 subgoal):
 1. \<not> g a \<le> g b \<Longrightarrow> integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
with less
[PROOF STATE]
proof (chain)
picking this:
\<not> g a \<le> g b
integral {c..g b} f + integral {g b..g a} f = integral {c..g a} f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> g a \<le> g b
integral {c..g b} f + integral {g b..g a} f = integral {c..g a} f

goal (1 subgoal):
 1. integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f
[PROOF STEP]
by (simp_all add: algebra_simps)
[PROOF STATE]
proof (state)
this:
integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f - integral {g b..g a} f

goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}

goal (1 subgoal):
 1. ((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral integral {g a..g b} f - integral {g b..g a} f) {a..b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in prob_space) sum_indep_erlang:
  assumes indep: "indep_var borel X borel Y"
  assumes [simp, arith]: "0 < l"
  assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)"
  assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)"
  shows "distributed M lborel (\<lambda>x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distributed M lborel (\<lambda>x. X x + Y x) (\<lambda>x. ennreal (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
indep_var borel X borel Y
0 < l
distributed M lborel X (\<lambda>x. ennreal (erlang_density k\<^sub>1 l x))
distributed M lborel Y (\<lambda>x. ennreal (erlang_density k\<^sub>2 l x))

goal (1 subgoal):
 1. distributed M lborel (\<lambda>x. X x + Y x) (\<lambda>x. ennreal (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l x))
[PROOF STEP]
apply (subst convolution_erlang_density[symmetric, OF \<open>0<l\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>indep_var borel X borel Y; 0 < l; distributed M lborel X (\<lambda>x. ennreal (erlang_density k\<^sub>1 l x)); distributed M lborel Y (\<lambda>x. ennreal (erlang_density k\<^sub>2 l x))\<rbrakk> \<Longrightarrow> distributed M lborel (\<lambda>x. X x + Y x) (\<lambda>x. \<integral>\<^sup>+ y. ennreal (erlang_density k\<^sub>1 l (x - y)) * ennreal (erlang_density k\<^sub>2 l y) \<partial>lborel)
[PROOF STEP]
apply (intro distributed_convolution)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>indep_var borel X borel Y; 0 < l; distributed M lborel X (\<lambda>x. ennreal (erlang_density k\<^sub>1 l x)); distributed M lborel Y (\<lambda>x. ennreal (erlang_density k\<^sub>2 l x))\<rbrakk> \<Longrightarrow> indep_var borel X borel Y
 2. \<lbrakk>indep_var borel X borel Y; 0 < l; distributed M lborel X (\<lambda>x. ennreal (erlang_density k\<^sub>1 l x)); distributed M lborel Y (\<lambda>x. ennreal (erlang_density k\<^sub>2 l x))\<rbrakk> \<Longrightarrow> distributed M lborel X (\<lambda>a. ennreal (erlang_density k\<^sub>1 l a))
 3. \<lbrakk>indep_var borel X borel Y; 0 < l; distributed M lborel X (\<lambda>x. ennreal (erlang_density k\<^sub>1 l x)); distributed M lborel Y (\<lambda>x. ennreal (erlang_density k\<^sub>2 l x))\<rbrakk> \<Longrightarrow> distributed M lborel Y (\<lambda>a. ennreal (erlang_density k\<^sub>2 l a))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma borel_measurable_normal_density[measurable]: "normal_density \<mu> \<sigma> \<in> borel_measurable borel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_density \<mu> \<sigma> \<in> borel_measurable borel
[PROOF STEP]
by (auto simp: normal_density_def[abs_def])


[STATEMENT]
lemma intY1_is_cl: "\<lparr>pset = intY1, order = induced intY1 r\<rparr> \<in> CompleteLattice"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>pset = intY1, order = induced intY1 r\<rparr> \<in> CompleteLattice
[PROOF STEP]
unfolding intY1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>pset = interval r (lub Y cl) (Top cl), order = induced (interval r (lub Y cl) (Top cl)) r\<rparr> \<in> CompleteLattice
[PROOF STEP]
by (simp add: Top_in_lattice Top_intv_not_empty interv_is_compl_latt lubY_in_A)


[STATEMENT]
lemma closedin_Euclidean_space:
  "closedin (powertop_real UNIV) (topspace(Euclidean_space n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) (topspace (Euclidean_space n))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) (topspace (Euclidean_space n))
[PROOF STEP]
have "closedin (powertop_real UNIV) {x. x i = 0}" if "n \<le> i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) {x. x i = 0}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) {x. x i = 0}
[PROOF STEP]
have "closedin (powertop_real UNIV) {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedin (powertop_real UNIV) {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}
[PROOF STEP]
proof (rule closedin_continuous_map_preimage)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. continuous_map (powertop_real UNIV) ?Y (\<lambda>x. x i)
 2. closedin ?Y {0}
[PROOF STEP]
show "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. x i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. x i)
[PROOF STEP]
by (metis UNIV_I continuous_map_product_coordinates)
[PROOF STATE]
proof (state)
this:
continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. x i)

goal (1 subgoal):
 1. closedin euclideanreal {0}
[PROOF STEP]
show "closedin euclideanreal {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closedin euclideanreal {0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closedin euclideanreal {0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
closedin (powertop_real UNIV) {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}

goal (1 subgoal):
 1. closedin (powertop_real UNIV) {x. x i = 0}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closedin (powertop_real UNIV) {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
closedin (powertop_real UNIV) {x \<in> topspace (powertop_real UNIV). x i \<in> {0}}

goal (1 subgoal):
 1. closedin (powertop_real UNIV) {x. x i = 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closedin (powertop_real UNIV) {x. x i = 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<le> ?i \<Longrightarrow> closedin (powertop_real UNIV) {x. x ?i = 0}

goal (1 subgoal):
 1. closedin (powertop_real UNIV) (topspace (Euclidean_space n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> ?i \<Longrightarrow> closedin (powertop_real UNIV) {x. x ?i = 0}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<le> ?i \<Longrightarrow> closedin (powertop_real UNIV) {x. x ?i = 0}

goal (1 subgoal):
 1. closedin (powertop_real UNIV) (topspace (Euclidean_space n))
[PROOF STEP]
unfolding topspace_Euclidean_space_alt
[PROOF STATE]
proof (prove)
using this:
n \<le> ?i \<Longrightarrow> closedin (powertop_real UNIV) {x. x ?i = 0}

goal (1 subgoal):
 1. closedin (powertop_real UNIV) (\<Inter>i\<in>{n..}. {x \<in> topspace (powertop_real UNIV). x i \<in> {0}})
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
closedin (powertop_real UNIV) (topspace (Euclidean_space n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma residue_rmul:
  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
  shows "residue (\<lambda>z. (f z) * c) z= residue f z * c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. residue (\<lambda>z. f z * c) z = residue f z * c
[PROOF STEP]
using residue_lmul[OF assms,of c]
[PROOF STATE]
proof (prove)
using this:
residue (\<lambda>z. c * f z) z = c * residue f z

goal (1 subgoal):
 1. residue (\<lambda>z. f z * c) z = residue f z * c
[PROOF STEP]
by (auto simp add:algebra_simps)


[STATEMENT]
lemma closed_atMost [continuous_intros, simp]: "closed {..a}"
  for a :: "'a::linorder_topology"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed {..a}
[PROOF STEP]
by (simp add: closed_open)


[STATEMENT]
lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a
[PROOF STEP]
by (fact continuous_fst)


[STATEMENT]
lemma add_diff_eq_iff_ennreal[simp]:
  fixes x y :: ennreal shows "x + (y - x) = y \<longleftrightarrow> x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + (y - x) = y) = (x \<le> y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x + (y - x) = y \<Longrightarrow> x \<le> y
 2. x \<le> y \<Longrightarrow> x + (y - x) = y
[PROOF STEP]
assume *: "x + (y - x) = y"
[PROOF STATE]
proof (state)
this:
x + (y - x) = y

goal (2 subgoals):
 1. x + (y - x) = y \<Longrightarrow> x \<le> y
 2. x \<le> y \<Longrightarrow> x + (y - x) = y
[PROOF STEP]
show "x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
by (subst *[symmetric]) simp
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x + (y - x) = y
[PROOF STEP]
qed (simp add: add_diff_inverse_ennreal)


[STATEMENT]
lemma wf_prog_stat_overridesD:
  assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G"
  shows
   "G\<turnstile>resTy new\<preceq>resTy old \<and>
    accmodi old \<le> accmodi new \<and>
    \<not> is_static old"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old
[PROOF STEP]
from stat_override
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> new overrides\<^sub>S old
[PROOF STEP]
obtain c where
    clsNew: "class G (declclass new) = Some c" and
    neqObj: "declclass new \<noteq> Object"
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> new overrides\<^sub>S old

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>class G (declclass new) = Some c; declclass new \<noteq> Object\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: stat_overrides_commonD declared_in_classD)
[PROOF STATE]
proof (state)
this:
class G (declclass new) = Some c
declclass new \<noteq> Object

goal (1 subgoal):
 1. G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old
[PROOF STEP]
with stat_override
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> new overrides\<^sub>S old
class G (declclass new) = Some c
declclass new \<noteq> Object
[PROOF STEP]
obtain newM oldM where
    newM: "table_of (methods c) (msig new) = Some newM" and
     new: "new = (declclass new,(msig new),newM)" and
     old: "old = (declclass old,(msig old),oldM)" and
          "msig new = msig old"
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> new overrides\<^sub>S old
class G (declclass new) = Some c
declclass new \<noteq> Object

goal (1 subgoal):
 1. (\<And>newM oldM. \<lbrakk>table_of (methods c) (msig new) = Some newM; new = (declclass new, msig new, newM); old = (declclass old, msig old, oldM); msig new = msig old\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases new,cases old)
       (auto dest: stat_overrides_commonD
         simp add: cdeclaredmethd_def declared_in_def)
[PROOF STATE]
proof (state)
this:
table_of (methods c) (msig new) = Some newM
new = (declclass new, msig new, newM)
old = (declclass old, msig old, oldM)
msig new = msig old

goal (1 subgoal):
 1. G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old
[PROOF STEP]
with stat_override
[PROOF STATE]
proof (chain)
picking this:
G \<turnstile> new overrides\<^sub>S old
table_of (methods c) (msig new) = Some newM
new = (declclass new, msig new, newM)
old = (declclass old, msig old, oldM)
msig new = msig old
[PROOF STEP]
have stat_override':
        "G,(msig new)\<turnstile>(declclass new,newM) overrides\<^sub>S (declclass old,oldM)"
[PROOF STATE]
proof (prove)
using this:
G \<turnstile> new overrides\<^sub>S old
table_of (methods c) (msig new) = Some newM
new = (declclass new, msig new, newM)
old = (declclass old, msig old, oldM)
msig new = msig old

goal (1 subgoal):
 1. G \<turnstile> qmdecl (msig new) (declclass new, newM) overrides\<^sub>S qmdecl (msig new) (declclass old, oldM)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
G \<turnstile> qmdecl (msig new) (declclass new, newM) overrides\<^sub>S qmdecl (msig new) (declclass old, oldM)

goal (1 subgoal):
 1. G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old
[PROOF STEP]
from clsNew wf
[PROOF STATE]
proof (chain)
picking this:
class G (declclass new) = Some c
wf_prog G
[PROOF STEP]
have "wf_cdecl G (declclass new,c)"
[PROOF STATE]
proof (prove)
using this:
class G (declclass new) = Some c
wf_prog G

goal (1 subgoal):
 1. wf_cdecl G (declclass new, c)
[PROOF STEP]
by (blast intro: wf_prog_cdecl)
[PROOF STATE]
proof (state)
this:
wf_cdecl G (declclass new, c)

goal (1 subgoal):
 1. G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old
[PROOF STEP]
note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override']
[PROOF STATE]
proof (state)
this:
G\<turnstile>resTy newM\<preceq>resTy (declclass old, oldM) \<and> accmodi (declclass old, oldM) \<le> accmodi newM \<and> \<not> is_static (declclass old, oldM)

goal (1 subgoal):
 1. G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old
[PROOF STEP]
with new old
[PROOF STATE]
proof (chain)
picking this:
new = (declclass new, msig new, newM)
old = (declclass old, msig old, oldM)
G\<turnstile>resTy newM\<preceq>resTy (declclass old, oldM) \<and> accmodi (declclass old, oldM) \<le> accmodi newM \<and> \<not> is_static (declclass old, oldM)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
new = (declclass new, msig new, newM)
old = (declclass old, msig old, oldM)
G\<turnstile>resTy newM\<preceq>resTy (declclass old, oldM) \<and> accmodi (declclass old, oldM) \<le> accmodi newM \<and> \<not> is_static (declclass old, oldM)

goal (1 subgoal):
 1. G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old
[PROOF STEP]
by (cases new, cases old) auto
[PROOF STATE]
proof (state)
this:
G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le> accmodi new \<and> \<not> is_static old

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma flip_bit_eq_idem_iff:
  \<open>flip_bit n w = w \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (flip_bit n w = w) = (LENGTH('a) \<le> n)
[PROOF STEP]
using linorder_le_less_linear
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<or> ?y < ?x

goal (1 subgoal):
 1. (flip_bit n w = w) = (LENGTH('a) \<le> n)
[PROOF STEP]
by (simp add: bit_eq_iff) (auto simp add: bit_simps)


[STATEMENT]
lemma split_invar: "invar t \<Longrightarrow> split t = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar t \<Longrightarrow> split t = t
[PROOF STEP]
by(cases t rule: split.cases) clarsimp+


[STATEMENT]
lemma iterate_add_eq_add_iff1:
  \<open>i \<le> j \<Longrightarrow> (iterate_add j u + m = iterate_add i u + n) = (iterate_add (j - i) u + m = n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j \<Longrightarrow> (iterate_add j u + m = iterate_add i u + n) = (iterate_add (j - i) u + m = n)
[PROOF STEP]
by (auto dest!: le_Suc_ex add_right_imp_eq simp: ab_semigroup_add_class.add_ac(1))


[STATEMENT]
lemma fresh_ty:
  fixes x::"name"
  and   T::"ty"
  shows "x\<sharp>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> T
[PROOF STEP]
by (induct T rule: ty.induct)
   (auto simp add: fresh_nat)


[STATEMENT]
lemma rGamma_of_int: "rGamma (of_int n) = (if n > 0 then inverse (fact (nat (n - 1))) else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rGamma (of_int n) = (if 0 < n then inverse (fact (nat (n - 1))) else (0::'a))
[PROOF STEP]
by (simp add: Gamma_of_int rGamma_inverse_Gamma)