equal
deleted
inserted
replaced
67 |
67 |
68 have A: "continuous_on {min u' v'..max u' v'} g'" |
68 have A: "continuous_on {min u' v'..max u' v'} g'" |
69 by (simp only: u'v' max_absorb2 min_absorb1) |
69 by (simp only: u'v' max_absorb2 min_absorb1) |
70 (intro continuous_on_subset[OF contg'], insert u'v', auto) |
70 (intro continuous_on_subset[OF contg'], insert u'v', auto) |
71 have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})" |
71 have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})" |
72 using asm by (intro has_field_derivative_subset[OF derivg] set_mp[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto |
72 using asm by (intro has_field_derivative_subset[OF derivg] subsetD[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto |
73 hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow> |
73 hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow> |
74 (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})" |
74 (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})" |
75 by (simp only: u'v' max_absorb2 min_absorb1) |
75 by (simp only: u'v' max_absorb2 min_absorb1) |
76 (auto simp: has_field_derivative_iff_has_vector_derivative) |
76 (auto simp: has_field_derivative_iff_has_vector_derivative) |
77 have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)" |
77 have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)" |