: "\a b z. \\x. x \ T \ x \ S \ g x = f x; + ((\x. if x \ T then f x else 0) has_integral z) (cbox a b)\ + \ ((\x. if x \ T then g x else 0) has_integral z) (cbox a b)" + by (auto dest!: *[where f="\x. if x\T then f x else 0" and g="\x. if x \ T then g x else 0"]) show ?thesis using fint gf apply (subst has_integral_alt) apply (subst (asm) has_integral_alt) - apply (simp split: if_split_asm) + apply (auto split: if_split_asm) apply (blast dest: *) - apply (erule_tac V = "\a b. T \ cbox a b" in thin_rl) - apply (elim all_forward imp_forward ex_forward all_forward conj_forward asm_rl) - apply (auto dest!: *[where f="\x. if x\T then f x else 0" and g="\x. if x \ T then g x else 0"]) - done + using \

by meson qed lemma has_integral_spike_eq: @@ -2383,10 +2351,7 @@ using negligible_standard_hyperplane[OF SOME_Basis, of "a \ (SOME i. i \ Basis)"] negligible_subset by blast lemma negligible_insert[simp]: "negligible (insert a s) \ negligible s" - apply (subst insert_is_Un) - unfolding negligible_Un_eq - apply auto - done + by (metis insert_is_Un negligible_Un_eq negligible_sing) lemma negligible_empty[iff]: "negligible {}" using negligible_insert by blast @@ -2478,9 +2443,8 @@ lemma has_integral_spike_interior: assumes f: "(f has_integral y) (cbox a b)" and gf: "\x. x \ box a b \ g x = f x" shows "(g has_integral y) (cbox a b)" - apply (rule has_integral_spike[OF negligible_frontier_interval _ f]) - using gf by auto - + by (meson Diff_iff gf has_integral_spike[OF negligible_frontier_interval _ f]) + lemma has_integral_spike_interior_eq: assumes "\x. x \ box a b \ g x = f x" shows "(f has_integral y) (cbox a b) \ (g has_integral y) (cbox a b)" @@ -2507,16 +2471,15 @@ fix a b :: 'b show "\g. (\x\cbox a b. norm (f x - g x) \ e) \ g integrable_on cbox a b" if "box a b = {}" for a b - apply (rule_tac x=f in exI) - using assms that by (auto simp: content_eq_0_interior) + using assms that + by (metis content_eq_0_interior integrable_on_null interior_cbox norm_zero right_minus_eq) { fix c g and k :: 'b assume fg: "\x\cbox a b. norm (f x - g x) \ e" and g: "g integrable_on cbox a b" assume k: "k \ Basis" show "\g. (\x\cbox a b \ {x. x \ k \ c}. norm (f x - g x) \ e) \ g integrable_on cbox a b \ {x. x \ k \ c}" "\g. (\x\cbox a b \ {x. c \ x \ k}. norm (f x - g x) \ e) \ g integrable_on cbox a b \ {x. c \ x \ k}" - apply (rule_tac[!] x=g in exI) - using fg integrable_split[OF g k] by auto + using fg g k by auto } show "\g. (\x\cbox a b. norm (f x - g x) \ e) \ g integrable_on cbox a b" if fg1: "\x\cbox a b \ {x. x \ k \ c}. norm (f x - g1 x) \ e" @@ -2583,8 +2546,7 @@ then have x: "x \ cbox a b" using as ptag by auto show "\g. (\x\l. norm (f x - g x) \ e) \ g integrable_on l" - apply (rule_tac x="\y. f x" in exI) - proof safe + proof (intro exI conjI strip) show "(\y. f x) integrable_on l" unfolding integrable_on_def l by blast next @@ -2650,22 +2612,15 @@ let ?P = "\e opp. \d. gauge d \ (\p. p tagged_division_of (cbox a b) \ d fine p \ opp (norm (($x, k)\p. content k *\<^sub>R f x) - i)) e)" show ?thesis - apply (subst has_integral) - proof safe + proof (subst has_integral, safe) fix e :: real assume e: "e > 0" - { assume "\e>0. ?P e (<)" - then show "?P (e * content (cbox a b)) ($" - apply (rule allE [where x="e * content (cbox a b)"]) - apply (elim impE ex_forward conj_forward) - using F e apply (auto simp add: algebra_simps) - done } - { assume "\e>0. ?P (e * content (cbox a b)) (\)" - then show "?P e (<)" - apply (rule allE [where x="e/2 / content (cbox a b)"]) - apply (elim impE ex_forward conj_forward) - using F e apply (auto simp add: algebra_simps) - done } + show "?P (e * content (cbox a b)) (\)" if \

[rule_format]: "\\>0. ?P \ (<)" + using \

[of "e * content (cbox a b)"] + by (meson F e less_imp_le mult_pos_pos) + show "?P e (<)" if \

[rule_format]: "\\>0. ?P (\ * content (cbox a b)) (\)" + using \

[of "e/2 / content (cbox a b)"] + using F e by (force simp add: algebra_simps) qed qed @@ -2737,11 +2692,15 @@ also have "\ \ e * norm (u - x) + e * norm (v - x)" proof (rule add_mono) show "norm (f u - f x - (u - x) *\<^sub>R f' x) \ e * norm (u - x)" - apply (rule d(2)[of x u]) - using \x \ K\ kab \u \ K\ ball dist_real_def by (auto simp add:dist_real_def) + proof (rule d) + show "norm (u - x) < d x" + using \u \ K\ ball by (auto simp add: dist_real_def) + qed (use \x \ K\ \u \ K\ kab in auto) show "norm (f v - f x - (v - x) *\<^sub>R f' x) \ e * norm (v - x)" - apply (rule d(2)[of x v]) - using \x \ K\ kab \v \ K\ ball dist_real_def by (auto simp add:dist_real_def) + proof (rule d) + show "norm (v - x) < d x" + using \v \ K\ ball by (auto simp add: dist_real_def) + qed (use \x \ K\ \v \ K\ kab in auto) qed also have "\ \ e * (Sup K - Inf K)" using \x \ K\ by (auto simp: k interval_bounds_real[OF \u \ v\] field_simps) @@ -2759,9 +2718,8 @@ shows "((\x. x) has_integral (b\<^sup>2 - a\<^sup>2)/2) {a..b}" proof - have "((\x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}" - apply (rule fundamental_theorem_of_calculus [OF assms]) unfolding power2_eq_square - by (rule derivative_eq_intros | simp)+ + by (rule fundamental_theorem_of_calculus [OF assms] derivative_eq_intros | simp)+ then show ?thesis by (simp add: field_simps) qed @@ -2813,9 +2771,8 @@ show "((\x. - cos (n * x) / n) has_vector_derivative sin (n * a)) (at a within {-pi..pi})" if "a \ {-pi..pi}" for a :: real using that False - apply (simp only: has_vector_derivative_def) - apply (rule derivative_eq_intros | force)+ - done + unfolding has_vector_derivative_def + by (intro derivative_eq_intros | force)+ qed auto then show ?thesis by simp @@ -2839,9 +2796,8 @@ if "x \ {-pi..pi}" for x :: real using that False - apply (simp only: has_vector_derivative_def) - apply (rule derivative_eq_intros | force)+ - done + unfolding has_vector_derivative_def + by (intro derivative_eq_intros | force)+ qed auto with False show ?thesis by (simp add: mult.commute) @@ -3087,18 +3043,17 @@ shows "operative conj True (\i. f integrable_on i)" proof - interpret comm_monoid conj True - by standard auto - have 1: "\a b. box a b = {} \ f integrable_on cbox a b" - by (simp add: content_eq_0_interior integrable_on_null) - have 2: "\a b c k. - \k \ Basis; - f integrable_on cbox a b \ {x. x \ k \ c}; - f integrable_on cbox a b \ {x. c \ x \ k}\ - \ f integrable_on cbox a b" - unfolding integrable_on_def by (auto intro!: has_integral_split) + proof qed show ?thesis - apply standard - using 1 2 by blast+ + proof + show "\a b. box a b = {} \ (f integrable_on cbox a b) = True" + by (simp add: content_eq_0_interior integrable_on_null) + show "\a b c k. + k \ Basis \ + (f integrable_on cbox a b) \ + (f integrable_on cbox a b \ {x. x \ k \ c} \ f integrable_on cbox a b \ {x. c \ x \ k})" + unfolding integrable_on_def by (auto intro!: has_integral_split) + qed qed lemma integrable_subinterval: @@ -3246,7 +3201,7 @@ assume "e > 0" obtain d where "d>0" and d: "\x'. \x' \ {a..b} - S; \x' - x\ < d\ \ norm(f x' - f x) \ e" using \e>0\ fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le) - have "norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \ e * \y - x\" + have "norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \ e * \y - x\" (is "?lhs \ ?rhs") if y: "y \ {a..b} - S" and yx: "\y - x\ < d" for y proof (cases "y < x") case False @@ -3255,18 +3210,18 @@ then have Idiff: "?I a y - ?I a x = ?I x y" using False x by (simp add: algebra_simps integral_combine) have fux_int: "((\u. f u - f x) has_integral integral {x..y} f - (y-x) *\<^sub>R f x) {x..y}" - apply (rule has_integral_diff) - using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]]) - using has_integral_const_real [of "f x" x y] False - apply simp - done - have "\xa. y - x < d \ (\x'. a \ x' \ x' \ b \ x' \ S \ \x' - x\ < d \ norm (f x' - f x) \ e) \ 0 < e \ xa \ S \ a \ x \ x \ S \ y \ b \ y \ S \ x \ xa \ xa \ y \ norm (f xa - f x) \ e" - using assms by auto - show ?thesis - using False - apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc) - apply (rule has_integral_bound_real[where f="(\u. f u - f x)"]) - using yx False d x y \e>0\ assms by (auto simp: Idiff fux_int) + proof (rule has_integral_diff) + show "(f has_integral integral {x..y} f) {x..y}" + using x y by (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]]) + show "((\u. f x) has_integral (y - x) *\<^sub>R f x) {x..y}" + using has_integral_const_real [of "f x" x y] False by simp + qed + have "?lhs \ e * content {x..y}" + using yx False d x y \e>0\ assms + by (intro has_integral_bound_real[where f="(\u. f u - f x)"]) (auto simp: Idiff fux_int) + also have "... \ ?rhs" + using False by auto + finally show ?thesis . next case True have "f integrable_on {a..x}" @@ -3274,16 +3229,18 @@ then have Idiff: "?I a x - ?I a y = ?I y x" using True x y by (simp add: algebra_simps integral_combine) have fux_int: "((\u. f u - f x) has_integral integral {y..x} f - (x - y) *\<^sub>R f x) {y..x}" - apply (rule has_integral_diff) - using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]]) - using has_integral_const_real [of "f x" y x] True - apply simp - done - have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \ e * \y - x\" - using True - apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc) - apply (rule has_integral_bound_real[where f="(\u. f u - f x)"]) - using yx True d x y \e>0\ assms by (auto simp: Idiff fux_int) + proof (rule has_integral_diff) + show "(f has_integral integral {y..x} f) {y..x}" + using x y by (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]]) + show "((\u. f x) has_integral (x - y) *\<^sub>R f x) {y..x}" + using has_integral_const_real [of "f x" y x] True by simp + qed + have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \ e * content {y..x}" + using yx True d x y \e>0\ assms + by (intro has_integral_bound_real[where f="(\u. f u - f x)"]) (auto simp: Idiff fux_int) + also have "... \ e * \y - x\" + using True by auto + finally have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \ e * \y - x\" . then show ?thesis by (simp add: algebra_simps norm_minus_commute) qed @@ -3423,22 +3380,22 @@ using p(6) by auto then obtain X y where "h x \ X" "(y, X) \ p" by blast then show "x \ \{k. \x. (x, k) \ (\(x, k). (g x, g ` k)) ` p}" - apply clarsimp - by (metis (no_types, lifting) assms(3) image_eqI pair_imageI) + by clarsimp (metis (no_types, lifting) gh image_eqI pair_imageI) qed (use gab in auto) have *: "inj_on (\(x, k). (g x, g ` k)) p" using inj(1) unfolding inj_on_def by fastforce - have "(\(x, k)\(\(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\(x, k)\p. content k *\<^sub>R f (g x)) - i" (is "?l = _") - using r - apply (simp only: algebra_simps add_left_cancel scaleR_right.sum) - apply (subst sum.reindex_bij_betw[symmetric, where h="\(x, k). (g x, g ` k)" and S=p]) - apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4)) - done - also have "\ = r *\<^sub>R ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r") + have "(\(x,K)\(\(y,L). (g y, g ` L)) ` p. content K *\<^sub>R f x) + = (\u\p. case case u of (x,K) \ (g x, g ` K) of (y,L) \ content L *\<^sub>R f y)" + by (metis (mono_tags, lifting) "*" sum.reindex_cong) + also have "... = (\(x,K)\p. r *\<^sub>R content K *\<^sub>R f (g x))" + using r by (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4)) + finally + have "(\(x, K)\(\(x,K). (g x, g ` K)) ` p. content K *\<^sub>R f x) - i = r *\<^sub>R (\(x,K)\p. content K *\<^sub>R f (g x)) - i" + by (simp add: scaleR_right.sum split_def) + also have "\ = r *\<^sub>R ((\(x,K)\p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" using \0 < r\ by (auto simp: scaleR_diff_right) - finally have eq: "?l = ?r" . - show "norm ((\(x,K)\p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" - using d[OF gimp] \0 < r\ by (auto simp add: eq) + finally show "norm ((\(x,K)\p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e" + using d[OF gimp] \0 < r\ by auto qed qed then show ?thesis @@ -3454,8 +3411,8 @@ proof - interpret finite_product_sigma_finite "\_. lborel" Basis proof qed simp - - have "emeasure lborel {x\space lborel. x \ k = c} = emeasure (\\<^sub>M j::'a\Basis. lborel) (\\<^sub>E j\Basis. if j = k then {c} else UNIV)" + have "emeasure lborel {x\space lborel. x \ k = c} + = emeasure (\\<^sub>M j::'a\Basis. lborel) (\\<^sub>E j\Basis. if j = k then {c} else UNIV)" using k by (auto simp add: lborel_eq[where 'a='a] emeasure_distr intro!: arg_cong2[where f=emeasure]) (auto simp: space_PiM PiE_iff extensional_def split: if_split_asm) @@ -3520,11 +3477,7 @@ proof (cases "m \ 0") case True with \cbox a b \ {}\ have "cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c) \ {}" - unfolding box_ne_empty - apply (intro ballI) - apply (erule_tac x=i in ballE) - apply (auto simp: inner_simps mult_left_mono) - done + by (simp add: box_ne_empty inner_left_distrib mult_left_mono) moreover from True have *: "\i. (m *\<^sub>R b + c) \ i - (m *\<^sub>R a + c) \ i = m *\<^sub>R (b-a) \ i" by (simp add: inner_simps field_simps) ultimately show ?thesis @@ -3533,11 +3486,7 @@ next case False with \cbox a b \ {}\ have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \ {}" - unfolding box_ne_empty - apply (intro ballI) - apply (erule_tac x=i in ballE) - apply (auto simp: inner_simps mult_left_mono) - done + by (simp add: box_ne_empty inner_left_distrib mult_left_mono) moreover from False have *: "\i. (m *\<^sub>R a + c) \ i - (m *\<^sub>R b + c) \ i = (-m) *\<^sub>R (b-a) \ i" by (simp add: inner_simps field_simps) ultimately show ?thesis using False @@ -3550,25 +3499,21 @@ fixes a :: "'a::euclidean_space" assumes "(f has_integral i) (cbox a b)" and "m \ 0" - shows "((\x. f(m *\<^sub>R x + c)) has_integral ((1 / (\m\ ^ DIM('a))) *\<^sub>R i)) ((\x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` cbox a b)" - apply (rule has_integral_twiddle) - using assms - apply (safe intro!: interval_image_affinity_interval content_image_affinity_cbox) - apply (rule zero_less_power) - unfolding scaleR_right_distrib - apply auto - done + shows "((\x. f(m *\<^sub>R x + c)) has_integral (1 / (\m\ ^ DIM('a))) *\<^sub>R i) ((\x. (1 / m) *\<^sub>R x + -((1 / m) *\<^sub>R c)) ` cbox a b)" +proof (rule has_integral_twiddle) + show "\w z. (\x. (1 / m) *\<^sub>R x + - ((1 / m) *\<^sub>R c)) ` cbox u v = cbox w z" + "\w z. (\x. m *\<^sub>R x + c) ` cbox u v = cbox w z" for u v + using interval_image_affinity_interval by blast+ + show "content ((\x. m *\<^sub>R x + c) ` cbox u v) = \m\ ^ DIM('a) * content (cbox u v)" for u v + using content_image_affinity_cbox by blast +qed (use assms zero_less_power in \auto simp: field_simps\) lemma integrable_affinity: assumes "f integrable_on cbox a b" and "m \ 0" shows "(\x. f(m *\<^sub>R x + c)) integrable_on ((\x. (1 / m) *\<^sub>R x + -((1/m) *\<^sub>R c)) ` cbox a b)" - using assms - unfolding integrable_on_def - apply safe - apply (drule has_integral_affinity) - apply auto - done + using has_integral_affinity assms + unfolding integrable_on_def by blast lemmas has_integral_affinity01 = has_integral_affinity [of _ _ 0 "1::real", simplified] @@ -3660,10 +3605,16 @@ by (force dest: has_integral_stretch) lemma vec_lambda_eq_sum: - shows "(\ k. f k (x $ k)) = (\k\Basis. (f (axis_index k) (x \ k)) *\<^sub>R k)" - apply (simp add: Basis_vec_def cart_eq_inner_axis UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def) - apply (simp add: vec_eq_iff axis_def if_distrib cong: if_cong) - done + "(\ k. f k (x $ k)) = (\k\Basis. (f (axis_index k) (x \ k)) *\<^sub>R k)" (is "?lhs = ?rhs") +proof - + have "?lhs = (\ k. f k (x \ axis k 1))" + by (simp add: cart_eq_inner_axis) + also have "... = (\u\UNIV. f u (x \ axis u 1) *\<^sub>R axis u 1)" + by (simp add: vec_eq_iff axis_def if_distrib cong: if_cong) + also have "... = ?rhs" + by (simp add: Basis_vec_def UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def) + finally show ?thesis . +qed lemma has_integral_stretch_cart: fixes m :: "'n::finite \ real" @@ -3703,11 +3654,17 @@ lemma uminus_interval_vector[simp]: fixes a b :: "'a::euclidean_space" shows "uminus ` cbox a b = cbox (-b) (-a)" - apply safe - apply (simp add: mem_box(2)) - apply (rule_tac x="-x" in image_eqI) - apply (auto simp add: mem_box) - done +proof - + have "x \ uminus ` cbox a b" if "x \ cbox (- b) (- a)" for x + proof - + have "-x \ cbox a b" + using that by (auto simp: mem_box) + then show ?thesis + by force + qed + then show ?thesis + by (auto simp: mem_box) +qed lemma has_integral_reflect_lemma[intro]: assumes "(f has_integral i) (cbox a b)" @@ -3771,22 +3728,20 @@ assume e: "e > 0" then have eba8: "(e * (b-a)) / 8 > 0" using ab by (auto simp add: field_simps) - note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt] + note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt, THEN conjunct2, rule_format] + thm derf_exp have bounded: "\x. x \ {a<.. bounded_linear (\u. u *\<^sub>R f' x)" - using derf_exp by simp + by (simp add: bounded_linear_scaleR_left) have "\x \ box a b. \d>0. \y. norm (y-x) < d \ norm (f y - f x - (y-x) *\<^sub>R f' x) \ e/2 * norm (y-x)" - (is "\x \ box a b. ?Q x") + (is "\x \ box a b. ?Q x") \\The explicit quantifier is required by the following step\ proof - fix x assume x: "x \ box a b" - show "?Q x" - apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]]) - using x e by auto + fix x assume "x \ box a b" + with e show "?Q x" + using derf_exp [of x "e/2"] by auto qed - from this [unfolded bgauge_existence_lemma] - obtain d where d: "\x. 0 < d x" - "\x y. \x \ box a b; norm (y-x) < d x\ - \ norm (f y - f x - (y-x) *\<^sub>R f' x) \ e/2 * norm (y-x)" - by metis + then obtain d where d: "\x. 0 < d x" + "\x y. \