--- a/src/HOL/Analysis/Arcwise_Connected.thy Sat Oct 31 21:06:29 2020 +0100
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Sat Oct 31 21:24:40 2020 +0000
@@ -16,9 +16,8 @@
lemma segment_to_closest_point:
fixes S :: "'a :: euclidean_space set"
shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}"
- apply (subst disjoint_iff_not_equal)
- apply (clarify dest!: dist_in_open_segment)
- by (metis closest_point_le dist_commute le_less_trans less_irrefl)
+ unfolding disjoint_iff
+ by (metis closest_point_le dist_commute dist_in_open_segment not_le)
lemma segment_to_point_exists:
fixes S :: "'a :: euclidean_space set"
@@ -110,10 +109,7 @@
show "\<Inter>(F ` UNIV) \<noteq> {} \<and> \<Inter>(F ` UNIV) \<subseteq> S \<and> \<phi> (\<Inter>(F ` UNIV))"
proof (intro conjI)
show "\<Inter>(F ` UNIV) \<noteq> {}"
- apply (rule compact_nest)
- apply (meson F cloF \<open>compact S\<close> seq_compact_closed_subset seq_compact_eq_compact)
- apply (simp add: F)
- by (meson Fsub lift_Suc_antimono_le)
+ by (metis F Fsub \<open>compact S\<close> cloF closed_Int_compact compact_nest inf.orderE lift_Suc_antimono_le)
show " \<Inter>(F ` UNIV) \<subseteq> S"
using F by blast
show "\<phi> (\<Inter>(F ` UNIV))"
@@ -160,12 +156,9 @@
also have "... = e"
by simp
finally have "dist (\<Sum>i\<in>Basis. (\<lfloor>2^k*(x \<bullet> i)\<rfloor> / 2^k) *\<^sub>R i) x < e" .
- then
+ with Ints_of_int
show "\<exists>k. \<exists>f \<in> Basis \<rightarrow> \<int>. dist (\<Sum>b\<in>Basis. (f b / 2^k) *\<^sub>R b) x < e"
- apply (rule_tac x=k in exI)
- apply (rule_tac x="\<lambda>i. of_int (floor (2^k*(x \<bullet> i)))" in bexI)
- apply auto
- done
+ by fastforce
qed
then show ?thesis by auto
qed
@@ -223,8 +216,7 @@
definition\<^marker>\<open>tag unimportant\<close> dyadics :: "'a::field_char_0 set" where "dyadics \<equiv> \<Union>k m. {of_nat m / 2^k}"
lemma real_in_dyadics [simp]: "real m \<in> dyadics"
- apply (simp add: dyadics_def)
- by (metis divide_numeral_1 numeral_One power_0)
+ by (simp add: dyadics_def) (metis divide_numeral_1 numeral_One power_0)
lemma nat_neq_4k1: "of_nat m \<noteq> (4 * of_nat k + 1) / (2 * 2^n :: 'a::field_char_0)"
proof
@@ -264,8 +256,8 @@
then have "(4 * m + k) * (2 ^ n') = (4 * m' + k) * (2^n)"
by linarith
then obtain "4*m + k = 4*m' + k" "n=n'"
- apply (rule prime_power_cancel2 [OF two_is_prime_nat])
- using assms by auto
+ using prime_power_cancel2 [OF two_is_prime_nat] assms
+ by (metis even_mult_iff even_numeral odd_add)
then have "m=m'" "n=n'"
by auto
}
@@ -353,13 +345,14 @@
apply (rule dyadic_413_cases, force+)
done
next
- show "?rhs \<subseteq> dyadics"
- apply (clarsimp simp: dyadics_def Nats_def simp del: power_Suc)
- apply (intro conjI subsetI)
- apply (auto simp del: power_Suc)
- apply (metis divide_numeral_1 numeral_One power_0)
- apply (metis of_nat_Suc of_nat_mult of_nat_numeral)
+ have "range of_nat \<subseteq> (\<Union>k m. {(of_nat m::'a) / 2 ^ k})"
+ by clarsimp (metis divide_numeral_1 numeral_One power_0)
+ moreover have "\<And>k m. \<exists>k' m'. ((1::'a) + 4 * of_nat m) / 2 ^ Suc k = of_nat m' / 2 ^ k'"
+ by (metis (no_types) of_nat_Suc of_nat_mult of_nat_numeral)
+ moreover have "\<And>k m. \<exists>k' m'. (4 * of_nat m + (3::'a)) / 2 ^ Suc k = of_nat m' / 2 ^ k'"
by (metis of_nat_add of_nat_mult of_nat_numeral)
+ ultimately show "?rhs \<subseteq> dyadics"
+ by (auto simp: dyadics_def Nats_def)
qed
@@ -369,9 +362,8 @@
| "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
| "x \<notin> dyadics \<Longrightarrow> dyad_rec b l r x = undefined"
using iff_4k [of _ 1] iff_4k [of _ 3]
- apply (simp_all add: nat_neq_4k1 nat_neq_4k3 neq_4k1_k43, atomize_elim)
- apply (fastforce simp add: dyadics_iff Nats_def field_simps)+
- done
+ apply (simp_all add: nat_neq_4k1 nat_neq_4k3 neq_4k1_k43 dyadics_iff Nats_def)
+ by (fastforce simp: field_simps)+
lemma dyadics_levels: "dyadics = (\<Union>K. \<Union>k<K. \<Union> m. {of_nat m / 2^k})"
unfolding dyadics_def by auto
@@ -452,13 +444,16 @@
by (simp add: dyad_rec.psimps dyad_rec_termination)
lemma dyad_rec_41 [simp]: "dyad_rec b l r ((4 * real m + 1) / 2 ^ (Suc n)) = l (dyad_rec b l r ((2*m + 1) / 2^n))"
- apply (rule dyad_rec.psimps)
- by (metis dyad_rec_level_termination lessI add.commute of_nat_Suc of_nat_mult of_nat_numeral)
-
+proof (rule dyad_rec.psimps)
+ show "dyad_rec_dom (b, l, r, (4 * real m + 1) / 2 ^ Suc n)"
+ by (metis add.commute dyad_rec_level_termination lessI of_nat_Suc of_nat_mult of_nat_numeral)
+qed
lemma dyad_rec_43 [simp]: "dyad_rec b l r ((4 * real m + 3) / 2 ^ (Suc n)) = r (dyad_rec b l r ((2*m + 1) / 2^n))"
- apply (rule dyad_rec.psimps)
- by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral)
+proof (rule dyad_rec.psimps)
+ show "dyad_rec_dom (b, l, r, (4 * real m + 3) / 2 ^ Suc n)"
+ by (metis dyad_rec_level_termination lessI of_nat_add of_nat_mult of_nat_numeral)
+qed
lemma dyad_rec_41_times2:
assumes "n > 0"
@@ -509,17 +504,15 @@
by (simp add: dyad_rec2_def)
lemma leftrec_41: "n > 0 \<Longrightarrow> leftrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) = leftrec u v lc rc ((2 * real m + 1) / 2^n)"
- apply (simp only: dyad_rec2_def dyad_rec_41_times2)
- apply (simp add: case_prod_beta)
- done
+ unfolding dyad_rec2_def dyad_rec_41_times2
+ by (simp add: case_prod_beta)
lemma leftrec_43: "n > 0 \<Longrightarrow>
leftrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) =
rc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
(midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
- apply (simp only: dyad_rec2_def dyad_rec_43_times2)
- apply (simp add: case_prod_beta)
- done
+ unfolding dyad_rec2_def dyad_rec_43_times2
+ by (simp add: case_prod_beta)
lemma rightrec_base: "rightrec u v lc rc (real m / 2) = v"
by (simp add: dyad_rec2_def)
@@ -528,14 +521,12 @@
rightrec u v lc rc ((4 * real m + 1) / 2 ^ (Suc n)) =
lc (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n))
(midpoint (leftrec u v lc rc ((2 * real m + 1) / 2^n)) (rightrec u v lc rc ((2 * real m + 1) / 2^n)))"
- apply (simp only: dyad_rec2_def dyad_rec_41_times2)
- apply (simp add: case_prod_beta)
- done
+ unfolding dyad_rec2_def dyad_rec_41_times2
+ by (simp add: case_prod_beta)
lemma rightrec_43: "n > 0 \<Longrightarrow> rightrec u v lc rc ((4 * real m + 3) / 2 ^ (Suc n)) = rightrec u v lc rc ((2 * real m + 1) / 2^n)"
- apply (simp only: dyad_rec2_def dyad_rec_43_times2)
- apply (simp add: case_prod_beta)
- done
+ unfolding dyad_rec2_def dyad_rec_43_times2
+ by (simp add: case_prod_beta)
lemma dyadics_in_open_unit_interval:
"{0<..<1} \<inter> (\<Union>k m. {real m / 2^k}) = (\<Union>k. \<Union>m \<in> {0<..<2^k}. {real m / 2^k})"
@@ -565,8 +556,8 @@
with that have "m \<in> cbox c0 d0"
by auto
obtain c d where cd: "{a..b} \<inter> f -` {f m} = {c..d}"
- apply (rule_tac c="max a c0" and d="min b d0" in that)
- using ab01 cd0 by auto
+ using ab01 cd0
+ by (rule_tac c="max a c0" and d="min b d0" in that) auto
then have cdab: "{c..d} \<subseteq> {a..b}"
by blast
show ?thesis
@@ -614,7 +605,7 @@
apply (rule that, blast)
done
then have left_right: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> a \<le> leftcut a b m \<and> rightcut a b m \<le> b"
- and left_right_m: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> leftcut a b m \<le> m \<and> m \<le> rightcut a b m"
+ and left_right_m: "\<And>a b m. \<lbrakk>m \<in> {a..b}; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> leftcut a b m \<le> m \<and> m \<le> rightcut a b m"
by auto
have left_neq: "\<lbrakk>a \<le> x; x < leftcut a b m; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m"
and right_neq: "\<lbrakk>rightcut a b m < x; x \<le> b; a \<le> m; m \<le> b; {a..b} \<subseteq> {0..1}\<rbrakk> \<Longrightarrow> f x \<noteq> f m"
@@ -709,24 +700,17 @@
case True
then obtain r where r: "m = 2*r" by (metis evenE)
show ?thesis
- using a_le_c [of "m+1"] c_le_b [of "m+1"] a_ge_0 [of "m+1"] b_le_1 [of "m+1"]
- Suc.IH [of "m+1"]
- apply (simp add: r m add.commute [of 1] \<open>n > 0\<close> a41 b41 del: power_Suc)
- apply (auto simp: left_right [THEN conjunct1])
- using order_trans [OF left_le c_le_v]
- by (metis (no_types, hide_lams) add.commute mult_2 of_nat_Suc of_nat_add)
+ using order_trans [OF left_le c_le_v, of "1+2*r"] Suc.IH [of "m+1"]
+ using a_le_c [of "m+1"] c_le_b [of "m+1"] a_ge_0 [of "m+1"] b_le_1 [of "m+1"] left_right \<open>n > 0\<close>
+ by (simp_all add: r m add.commute [of 1] a41 b41 del: power_Suc)
next
case False
then obtain r where r: "m = 2*r + 1" by (metis oddE)
show ?thesis
- using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"]
- Suc.IH [of "m+1"]
- apply (simp add: r m add.commute [of 3] \<open>n > 0\<close> a43 b43 del: power_Suc)
- apply (auto simp: add.commute left_right [THEN conjunct2])
- using order_trans [OF c_ge_u right_ge]
- apply (metis (no_types, hide_lams) mult_2 numeral_One of_nat_add of_nat_numeral)
- apply (metis Suc.IH mult_2 of_nat_1 of_nat_add)
- done
+ using order_trans [OF c_ge_u right_ge, of "1+2*r"] Suc.IH [of "m"]
+ using a_le_c [of "m"] c_le_b [of "m"] a_ge_0 [of "m"] b_le_1 [of "m"] left_right \<open>n > 0\<close>
+ apply (simp_all add: r m add.commute [of 3] a43 b43 del: power_Suc)
+ by (simp add: add.commute)
qed
qed
qed
@@ -738,8 +722,7 @@
have alec [simp]: "a(m / 2^n) \<le> c(m / 2^n)" and cleb [simp]: "c(m / 2^n) \<le> b(m / 2^n)" for m::nat and n
by (auto simp: c_def ge_midpoint_1 le_midpoint_1 uabv)
have c_ge_0 [simp]: "0 \<le> c(m / 2^n)" and c_le_1 [simp]: "c(m / 2^n) \<le> 1" for m::nat and n
- using a_ge_0 alec order_trans apply blast
- by (meson b_le_1 cleb order_trans)
+ using a_ge_0 alec b_le_1 cleb order_trans by blast+
have "\<lbrakk>d = m-n; odd j; \<bar>real i / 2^m - real j / 2^n\<bar> < 1/2 ^ n\<rbrakk>
\<Longrightarrow> (a(j / 2^n)) \<le> (c(i / 2^m)) \<and> (c(i / 2^m)) \<le> (b(j / 2^n))" for d i j m n
proof (induction d arbitrary: j n rule: less_induct)
@@ -786,25 +769,27 @@
by (auto simp: ac)
next
case True show ?thesis
- proof (cases "real i / 2^m" "real j / 2^n" rule: linorder_cases)
+ proof (cases "i / 2^m" "j / 2^n" rule: linorder_cases)
case less
moreover have "real (4 * k + 1) / 2 ^ Suc n + 1 / (2 ^ Suc n) = real j / 2 ^ n"
using k by (force simp: field_split_simps)
- moreover have "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 2 / (2 ^ Suc n)"
+ moreover have "\<bar>real i / 2 ^ m - j / 2 ^ n\<bar> < 2 / (2 ^ Suc n)"
using less.prems by simp
ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)"
using less.prems by linarith
- have *: "a (real (4 * k + 1) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
+ have "a (real (4 * k + 1) / 2 ^ Suc n) \<le> c (i / 2 ^ m) \<and>
c (real i / 2 ^ m) \<le> b (real (4 * k + 1) / 2 ^ Suc n)"
- apply (rule less.IH [OF _ refl])
- using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2)
- done
- show ?thesis
+ proof (rule less.IH [OF _ refl])
+ show "m - Suc n < d"
+ using \<open>n < m\<close> diff_less_mono2 less.prems(1) lessI by presburger
+ show "\<bar>real i / 2 ^ m - real (4 * k + 1) / 2 ^ Suc n\<bar> < 1 / 2 ^ Suc n"
+ using closer \<open>n < m\<close> \<open>d = m - n\<close> by (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2)
+ qed auto
+ then show ?thesis
using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"]
- using k a41 b41 * \<open>0 < n\<close>
- apply (simp add: add.commute)
- done
+ using k a41 b41 \<open>0 < n\<close>
+ by (simp add: add.commute)
next
case equal then show ?thesis by simp
next
@@ -815,17 +800,19 @@
using less.prems by simp
ultimately have closer: "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / (2 ^ Suc n)"
using less.prems by linarith
- have *: "a (real (4 * k + 3) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
+ have "a (real (4 * k + 3) / 2 ^ Suc n) \<le> c (real i / 2 ^ m) \<and>
c (real i / 2 ^ m) \<le> b (real (4 * k + 3) / 2 ^ Suc n)"
- apply (rule less.IH [OF _ refl])
- using closer \<open>n < m\<close> \<open>d = m - n\<close> apply (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2)
- done
- show ?thesis
+ proof (rule less.IH [OF _ refl])
+ show "m - Suc n < d"
+ using \<open>n < m\<close> diff_less_mono2 less.prems(1) by blast
+ show "\<bar>real i / 2 ^ m - real (4 * k + 3) / 2 ^ Suc n\<bar> < 1 / 2 ^ Suc n"
+ using closer \<open>n < m\<close> \<open>d = m - n\<close> by (auto simp: field_split_simps \<open>n < m\<close> diff_less_mono2)
+ qed auto
+ then show ?thesis
using LR [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
using alec [of "2*k+1"] cleb [of "2*k+1"] a_ge_0 [of "2*k+1"] b_le_1 [of "2*k+1"]
- using k a43 b43 * \<open>0 < n\<close>
- apply (simp add: add.commute)
- done
+ using k a43 b43 \<open>0 < n\<close>
+ by (simp add: add.commute)
qed
qed
qed
@@ -912,9 +899,7 @@
with \<open>0 < j\<close> have "k > 0" "2 * k < 2 ^ n"
using Suc.prems(2) k by auto
with k \<open>0 < n\<close> Suc.IH [of k] show ?thesis
- apply (simp add: m1_to_3 a41 b43 del: power_Suc)
- apply (subst of_nat_diff, auto)
- done
+ by (simp add: m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff)
next
case False
then obtain k where k: "j = 2*k + 1" by (metis oddE)
@@ -924,8 +909,7 @@
= f (rightcut (a ((2 * k + 1) / 2^n)) (b ((2 * k + 1) / 2^n)) (c ((2 * k + 1) / 2^n)))"
using alec [of "2*k+1" n] cleb [of "2*k+1" n] a_ge_0 [of "2*k+1" n] b_le_1 [of "2*k+1" n] k
using left_right_m [of "c((2*k + 1) / 2^n)" "a((2*k + 1) / 2^n)" "b((2*k + 1) / 2^n)"]
- apply (auto simp: add.commute feqm [OF order_refl] feqm [OF _ order_refl, symmetric])
- done
+ by (auto simp: add.commute feqm [OF order_refl] feqm [OF _ order_refl, symmetric])
then
show ?thesis
by (simp add: k add.commute [of 1] add.commute [of 3] a43 b41\<open>0 < n\<close> del: power_Suc)
@@ -951,9 +935,7 @@
by auto
then show ?thesis
using Suc.IH [of k] k \<open>0 < k\<close>
- apply (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc)
- apply (auto simp: of_nat_diff)
- done
+ by (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff)
next
case False
then obtain k where k: "j = 2*k + 1" by (metis oddE)
@@ -1057,8 +1039,7 @@
show thesis
proof
show "(1::nat) < 2 ^ n"
- apply (subst one_less_power)
- using \<open>n > 0\<close> by auto
+ by (metis Suc_1 \<open>0 < n\<close> lessI one_less_power)
show "\<bar>real i / 2 ^ m - real 1/2 ^ n\<bar> < 1/2 ^ n"
using i less_j1 by (simp add: dist_norm field_simps True)
show "\<bar>real k / 2 ^ p - real 1/2 ^ n\<bar> < 1/2 ^ n"
@@ -1109,35 +1090,34 @@
qed
show ?thesis
proof
- have "real j < 2 ^ n"
- using j_le i k
- apply (auto simp: le_max_iff_disj simp del: of_nat_less_numeral_power_cancel_iff
- elim!: le_less_trans)
- apply (auto simp: field_simps)
- done
+ have "2 ^ n * real i / 2 ^ m < 2 ^ n" "2 ^ n * real k / 2 ^ p < 2 ^ n"
+ using i k by (auto simp: field_simps)
+ then have "max (2^n * i / 2^m) (2^n * k / 2^p) < 2^n"
+ by simp
+ with j_le have "real j < 2 ^ n" by linarith
then show "j < 2 ^ n"
by auto
- show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n"
+ have "\<bar>real i * 2 ^ n - real j * 2 ^ m\<bar> < 2 ^ m"
using clo less_j1 j_le
- apply (auto simp: le_max_iff_disj field_split_simps dist_norm)
- apply (auto simp: algebra_simps abs_if split: if_split_asm dest: 1 2)
- done
- show "\<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2 ^ n"
- using clo less_j1 j_le
- apply (auto simp: le_max_iff_disj field_split_simps dist_norm)
- apply (auto simp: algebra_simps not_less abs_if split: if_split_asm dest: 3 2)
- done
+ by (auto simp: le_max_iff_disj field_split_simps dist_norm abs_if split: if_split_asm dest: 1 2)
+ then show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n"
+ by (auto simp: field_split_simps)
+ have "\<bar>real k * 2 ^ n - real j * 2 ^ p\<bar> < 2 ^ p"
+ using clo less_j1 j_le
+ by (auto simp: le_max_iff_disj field_split_simps dist_norm abs_if split: if_split_asm dest: 3 2)
+ then show "\<bar>real k / 2 ^ p - real j / 2 ^ n\<bar> < 1/2 ^ n"
+ by (auto simp: le_max_iff_disj field_split_simps dist_norm)
qed (use False in simp)
qed
qed
show "dist (f (c (real k / 2 ^ p))) (f (c (real i / 2 ^ m))) < e"
proof (rule dist_triangle_half_l)
show "dist (f (c (real k / 2 ^ p))) (f(c(j / 2^n))) < e/2"
- apply (rule dist_fc_close)
- using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> k clo_kj by auto
+ using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> k clo_kj
+ by (intro dist_fc_close) auto
show "dist (f (c (real i / 2 ^ m))) (f (c (real j / 2 ^ n))) < e/2"
- apply (rule dist_fc_close)
- using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> i clo_ij by auto
+ using \<open>0 < j\<close> \<open>j < 2 ^ n\<close> i clo_ij
+ by (intro dist_fc_close) auto
qed
qed
qed
@@ -1191,8 +1171,7 @@
proof cases
case 1
then show ?thesis
- apply (rule_tac x=u in exI)
- using uabv [of 1 1] f0u [of u] f0u [of x] by auto
+ using uabv [of 1 1] f0u [of u] f0u [of x] by force
next
case 2
then show ?thesis
@@ -1200,8 +1179,7 @@
next
case 3
then show ?thesis
- apply (rule_tac x=v in exI)
- using uabv [of 1 1] fv1 [of v] fv1 [of x] by auto
+ using uabv [of 1 1] fv1 [of v] fv1 [of x] by force
qed
with \<open>n=0\<close> show ?thesis
by (rule_tac x=1 in exI) auto
@@ -1212,6 +1190,9 @@
and y: "y \<in> {a (real m / 2 ^ n)..b (real m / 2 ^ n)}" and feq: "f y = f x"
by metis
then obtain j where j: "m = 2*j + 1" by (metis oddE)
+ have j4: "4 * j + 1 < 2 ^ Suc n"
+ using mless j by (simp add: algebra_simps)
+
consider "y \<in> {a((2*j + 1) / 2^n) .. b((4*j + 1) / 2 ^ (Suc n))}"
| "y \<in> {b((4*j + 1) / 2 ^ (Suc n)) .. a((4*j + 3) / 2 ^ (Suc n))}"
| "y \<in> {a((4*j + 3) / 2 ^ (Suc n)) .. b((2*j + 1) / 2^n)}"
@@ -1219,33 +1200,35 @@
then show ?thesis
proof cases
case 1
- then show ?thesis
- apply (rule_tac x="4*j + 1" in exI)
- apply (rule_tac x=y in exI)
- using mless j \<open>n \<noteq> 0\<close>
- apply (simp add: feq a41 b41 add.commute [of 1] del: power_Suc)
- apply (simp add: algebra_simps)
- done
+ show ?thesis
+ proof (intro exI conjI)
+ show "y \<in> {a (real (4 * j + 1) / 2 ^ Suc n)..b (real (4 * j + 1) / 2 ^ Suc n)}"
+ using mless j \<open>n \<noteq> 0\<close> 1 by (simp add: a41 b41 add.commute [of 1] del: power_Suc)
+ qed (use feq j4 in auto)
next
case 2
show ?thesis
- apply (rule_tac x="4*j + 1" in exI)
- apply (rule_tac x="b((4*j + 1) / 2 ^ (Suc n))" in exI)
- using mless \<open>n \<noteq> 0\<close> 2 j
- using alec [of "2*j+1" n] cleb [of "2*j+1" n] a_ge_0 [of "2*j+1" n] b_le_1 [of "2*j+1" n]
- using left_right [of "c((2*j + 1) / 2^n)" "a((2*j + 1) / 2^n)" "b((2*j + 1) / 2^n)"]
- apply (simp add: a41 b41 a43 b43 add.commute [of 1] add.commute [of 3] del: power_Suc)
- apply (auto simp: feq [symmetric] intro: f_eqI)
- done
+ proof (intro exI conjI)
+ show "b (real (4 * j + 1) / 2 ^ Suc n) \<in> {a (real (4 * j + 1) / 2 ^ Suc n)..b (real (4 * j + 1) / 2 ^ Suc n)}"
+ using \<open>n \<noteq> 0\<close> alec [of "2*j+1" n] cleb [of "2*j+1" n] a_ge_0 [of "2*j+1" n] b_le_1 [of "2*j+1" n]
+ using left_right [of "c((2*j + 1) / 2^n)" "a((2*j + 1) / 2^n)" "b((2*j + 1) / 2^n)"]
+ by (simp add: a41 b41 add.commute [of 1] del: power_Suc)
+ show "f (b (real (4 * j + 1) / 2 ^ Suc n)) = f x"
+ using \<open>n \<noteq> 0\<close> 2
+ using alec [of "2*j+1" n] cleb [of "2*j+1" n] a_ge_0 [of "2*j+1" n] b_le_1 [of "2*j+1" n]
+ by (force simp add: b41 a43 add.commute [of 1] feq [symmetric] simp del: power_Suc intro: f_eqI)
+ qed (use j4 in auto)
next
case 3
- then show ?thesis
- apply (rule_tac x="4*j + 3" in exI)
- apply (rule_tac x=y in exI)
- using mless j \<open>n \<noteq> 0\<close>
- apply (simp add: feq a43 b43 del: power_Suc)
- apply (simp add: algebra_simps)
- done
+ show ?thesis
+ proof (intro exI conjI)
+ show "4 * j + 3 < 2 ^ Suc n"
+ using mless j by simp
+ show "f y = f x"
+ by fact
+ show "y \<in> {a (real (4 * j + 3) / 2 ^ Suc n) .. b (real (4 * j + 3) / 2 ^ Suc n)}"
+ using 3 False b43 [of n j] by (simp add: add.commute)
+ qed (use 3 in auto)
qed
qed
qed
@@ -1255,24 +1238,26 @@
by fastforce
with * obtain m::nat and y
where "odd m" "0 < m" and mless: "m < 2 ^ n"
- and y: "y \<in> {a(m / 2^n) .. b(m / 2^n)}" and feq: "f x = f y"
- by metis
+ and y: "a(m / 2^n) \<le> y \<and> y \<le> b(m / 2^n)" and feq: "f x = f y"
+ by (metis atLeastAtMost_iff)
then have "0 \<le> y" "y \<le> 1"
- by (metis atLeastAtMost_iff a_ge_0 b_le_1 order.trans)+
+ by (meson a_ge_0 b_le_1 order.trans)+
moreover have "y < \<delta> + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < \<delta> + y"
- using y apply simp_all
- using alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
+ using y alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
by linarith+
moreover note \<open>0 < m\<close> mless \<open>0 \<le> x\<close> \<open>x \<le> 1\<close>
- ultimately show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
- apply (rule_tac x=n in exI)
- apply (rule_tac x=m in bexI)
- apply (auto simp: dist_norm h_eq feq \<delta>)
- done
+ ultimately have "dist (h (real m / 2 ^ n)) (f x) < e"
+ by (auto simp: dist_norm h_eq feq \<delta>)
+ then show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
+ using \<open>0 < m\<close> greaterThanLessThan_iff mless by blast
qed
also have "... \<subseteq> h ` {0..1}"
- apply (rule closure_minimal)
- using compact_continuous_image [OF cont_h] compact_imp_closed by (auto simp: D01_def)
+ proof (rule closure_minimal)
+ show "h ` D01 \<subseteq> h ` {0..1}"
+ using cloD01 closure_subset by blast
+ show "closed (h ` {0..1})"
+ using compact_continuous_image [OF cont_h] compact_imp_closed by auto
+ qed
finally show "f ` {0..1} \<subseteq> h ` {0..1}" .
qed
moreover have "inj_on h {0..1}"
@@ -1394,8 +1379,7 @@
qed
have c_gt_0 [simp]: "0 < c(m / 2^n)" and c_less_1 [simp]: "c(m / 2^n) < 1" for m::nat and n
using a_less_b [of m n] apply (simp_all add: c_def midpoint_def)
- using a_ge_0 [of m n] b_le_1 [of m n] apply linarith+
- done
+ using a_ge_0 [of m n] b_le_1 [of m n] by linarith+
have approx: "\<exists>j n. odd j \<and> n \<noteq> 0 \<and>
real i / 2^m \<le> real j / 2^n \<and>
real j / 2^n \<le> real k / 2^p \<and>
@@ -1423,7 +1407,7 @@
case 0 with less.prems show ?thesis by auto
next
case (Suc p')
- have False if "real i * 2 ^ p' < real k * 2 ^ m'" "k < 2 ^ p'" "2 ^ m' \<le> i"
+ have \<section>: False if "real i * 2 ^ p' < real k * 2 ^ m'" "k < 2 ^ p'" "2 ^ m' \<le> i"
proof -
have "real k * 2 ^ m' < 2 ^ p' * 2 ^ m'"
using that by simp
@@ -1431,11 +1415,13 @@
using that by linarith
with that show ?thesis by simp
qed
- then show ?thesis
+ moreover have *: "real i / 2 ^ m' < real k / 2^p'" "k < 2 ^ p'"
+ using less.prems \<open>m = Suc m'\<close> 2 Suc by (force simp: field_split_simps)+
+ moreover have "i < 2 ^ m' "
+ using \<section> * by (clarsimp simp: divide_simps linorder_not_le) (meson linorder_not_le)
+ ultimately show ?thesis
using less.IH [of "m'+p'" i m' k p'] less.prems \<open>m = Suc m'\<close> 2 Suc
- apply atomize
- apply (force simp: field_split_simps)
- done
+ by (force simp: field_split_simps)
qed
qed
next
@@ -1449,10 +1435,18 @@
case 0 with less.prems show ?thesis by auto
next
case (Suc p')
- then show ?thesis
+ have "real (i - 2 ^ m') / 2 ^ m' < real (k - 2 ^ p') / 2 ^ p'"
+ using less.prems \<open>m = Suc m'\<close> Suc 3 by (auto simp: field_simps of_nat_diff)
+ moreover have "k - 2 ^ p' < 2 ^ p'" "i - 2 ^ m' < 2 ^ m'"
+ using less.prems Suc \<open>m = Suc m'\<close> by auto
+ moreover
+ have "2 ^ p' \<le> k" "2 ^ p' \<noteq> k"
+ using less.prems \<open>m = Suc m'\<close> Suc 3 by auto
+ then have "2 ^ p' < k"
+ by linarith
+ ultimately show ?thesis
using less.IH [of "m'+p'" "i - 2^m'" m' "k - 2 ^ p'" p'] less.prems \<open>m = Suc m'\<close> Suc 3
- apply atomize
- apply (auto simp: field_simps of_nat_diff)
+ apply (clarsimp simp: field_simps of_nat_diff)
apply (rule_tac x="2 ^ n + j" in exI, simp)
apply (rule_tac x="Suc n" in exI)
apply (auto simp: field_simps)
@@ -1476,15 +1470,10 @@
case True then show ?thesis by simp
next
case False
- with i_le_j q have less: "i / 2^m < (2*q + 1) / 2^n'"
- by auto
- have *: "\<lbrakk>i < q; abs(i - q) < s*2; q = r + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real
- by auto
- have "c(i / 2^m) \<le> b(real(4 * q + 1) / 2 ^ (Suc n'))"
- apply (rule ci_le_bj, force)
- apply (rule * [OF less])
- using i_le_j clo_ij q apply (auto simp: field_split_simps)
- done
+ with i_le_j clo_ij q have "\<bar>real i / 2 ^ m - real (4 * q + 1) / 2 ^ Suc n'\<bar> < 1 / 2 ^ Suc n'"
+ by (auto simp: field_split_simps)
+ then have "c(i / 2^m) \<le> b(real(4 * q + 1) / 2 ^ (Suc n'))"
+ by (meson ci_le_bj even_mult_iff even_numeral even_plus_one_iff)
then show ?thesis
using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] b41 [of n' q] \<open>n' \<noteq> 0\<close>
using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
@@ -1500,11 +1489,10 @@
by auto
have *: "\<lbrakk>q < i; abs(i - q) < s*2; r = q + s\<rbrakk> \<Longrightarrow> abs(i - r) < s" for i q s r::real
by auto
- have "a(real(4*q + 3) / 2 ^ (Suc n')) \<le> c(j / 2^n)"
- apply (rule aj_le_ci, force)
- apply (rule * [OF less])
- using j_le_j clo_jj q apply (auto simp: field_split_simps)
- done
+ have "\<bar>real j / 2 ^ n - real (4 * q + 3) / 2 ^ Suc n'\<bar> < 1 / 2 ^ Suc n'"
+ by (rule * [OF less]) (use j_le_j clo_jj q in \<open>auto simp: field_split_simps\<close>)
+ then have "a(real(4*q + 3) / 2 ^ (Suc n')) \<le> c(j / 2^n)"
+ by (metis Suc3_eq_add_3 add.commute aj_le_ci even_Suc even_mult_iff even_numeral)
then show ?thesis
using alec [of "2*q+1" n'] cleb [of "2*q+1" n'] a_ge_0 [of "2*q+1" n'] b_le_1 [of "2*q+1" n'] a43 [of n' q] \<open>n' \<noteq> 0\<close>
using left_right_m [of "c((2*q + 1) / 2^n')" "a((2*q + 1) / 2^n')" "b((2*q + 1) / 2^n')"]
@@ -1611,15 +1599,13 @@
using m by (auto simp: field_split_simps)
have closure0m: "{0..m / 2^n} = closure ({0<..< m / 2^n} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
by (subst closure_dyadic_rationals_in_convex_set_pos_1, simp_all add: not_le m)
- have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
- apply (subst closure_dyadic_rationals_in_convex_set_pos_1; simp add: not_le m)
- using \<open>0 < real m / 2 ^ n\<close> by linarith
+ have "2^n > m"
+ by (simp add: m(2) not_le)
+ then have closurem1: "{m / 2^n .. 1} = closure ({m / 2^n <..< 1} \<inter> (\<Union>k m. {real m / 2 ^ k}))"
+ using closure_dyadic_rationals_in_convex_set_pos_1 m_div(1) by fastforce
have cont_h': "continuous_on (closure ({u<..<v} \<inter> (\<Union>k m. {real m / 2 ^ k}))) h"
if "0 \<le> u" "v \<le> 1" for u v
- apply (rule continuous_on_subset [OF cont_h])
- apply (rule closure_minimal [OF subsetI])
- using that apply auto
- done
+ using that by (intro continuous_on_subset [OF cont_h] closure_minimal [OF subsetI]) auto
have closed_f': "closed (f ` {u..v})" if "0 \<le> u" "v \<le> 1" for u v
by (metis compact_continuous_image cont_f compact_interval atLeastatMost_subset_iff
compact_imp_closed continuous_on_subset that)
@@ -1629,20 +1615,18 @@
proof clarsimp
fix p q
assume p: "0 < real p / 2 ^ q" "real p / 2 ^ q < real m / 2 ^ n"
- then have [simp]: "0 < p" "p < 2 ^ q"
- apply (simp add: field_split_simps)
- apply (blast intro: p less_2I m_div less_trans)
- done
+ then have [simp]: "0 < p"
+ by (simp add: field_split_simps)
+ have [simp]: "p < 2 ^ q"
+ by (blast intro: p less_2I m_div less_trans)
have "f (c (real p / 2 ^ q)) \<in> f ` {0..c (real m / 2 ^ n)}"
by (auto simp: clec p m)
then show "h (real p / 2 ^ q) \<in> f ` {0..c (real m / 2 ^ n)}"
by (simp add: h_eq)
qed
- then have "h ` {0 .. m / 2^n} \<subseteq> f ` {0 .. c(m / 2^n)}"
+ with m_div have "h ` {0 .. m / 2^n} \<subseteq> f ` {0 .. c(m / 2^n)}"
apply (subst closure0m)
- apply (rule image_closure_subset [OF cont_h' closed_f'])
- using m_div apply auto
- done
+ by (rule image_closure_subset [OF cont_h' closed_f']) auto
then have hx1: "h x1 \<in> f ` {0 .. c(m / 2^n)}"
using x12 less.prems(1) by auto
then obtain t1 where t1: "h x1 = f t1" "0 \<le> t1" "t1 \<le> c (m / 2 ^ n)"
@@ -1658,11 +1642,9 @@
then show "h (real p / 2 ^ q) \<in> f ` {c (real m / 2 ^ n)..1}"
by (simp add: h_eq)
qed
- then have "h ` {m / 2^n .. 1} \<subseteq> f ` {c(m / 2^n) .. 1}"
+ with m have "h ` {m / 2^n .. 1} \<subseteq> f ` {c(m / 2^n) .. 1}"
apply (subst closurem1)
- apply (rule image_closure_subset [OF cont_h' closed_f'])
- using m apply auto
- done
+ by (rule image_closure_subset [OF cont_h' closed_f']) auto
then have hx2: "h x2 \<in> f ` {c(m / 2^n)..1}"
using x12 less.prems by auto
then obtain t2 where t2: "h x2 = f t2" "c (m / 2 ^ n) \<le> t2" "t2 \<le> 1"
@@ -1718,15 +1700,15 @@
by (metis uniformly_continuous_onE [OF ucont_p])
have minxy: "min e (y - x) < (y - x) * (3 / 2)"
by (subst min_less_iff_disj) (simp add: less)
- obtain w z where "w < z" and w: "w \<in> {x<..<y}" and z: "z \<in> {x<..<y}"
+ define w where "w \<equiv> x + (min e (y - x) / 3)"
+ define z where "z \<equiv>y - (min e (y - x) / 3)"
+ have "w < z" and w: "w \<in> {x<..<y}" and z: "z \<in> {x<..<y}"
and wxe: "norm(w - x) < e" and zye: "norm(z - y) < e"
- apply (rule_tac w = "x + (min e (y - x) / 3)" and z = "y - (min e (y - x) / 3)" in that)
- using minxy \<open>0 < e\<close> less by simp_all
+ using minxy \<open>0 < e\<close> less unfolding w_def z_def by auto
have Fclo: "\<And>T. T \<in> range F \<Longrightarrow> closed T"
by (metis \<open>\<And>n. closed (F n)\<close> image_iff)
have eq: "{w..z} \<inter> \<Inter>(F ` UNIV) = {}"
- using less w z apply (auto simp: open_segment_eq_real_ivl)
- by (metis (no_types, hide_lams) INT_I IntI empty_iff greaterThanLessThan_iff not_le order.trans)
+ using less w z by (simp add: open_segment_eq_real_ivl disjoint_iff)
then obtain K where "finite K" and K: "{w..z} \<inter> (\<Inter> (F ` K)) = {}"
by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo])
then have "K \<noteq> {}"
@@ -1752,8 +1734,7 @@
by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(1) less_eq_real_def w)
qed (auto simp: open_segment_eq_real_ivl intro!: that)
with False show thesis
- apply (auto simp: disjoint_iff_not_equal intro!: that)
- by (metis greaterThanLessThan_iff less_eq_real_def)
+ by (auto simp add: disjoint_iff less_eq_real_def intro!: that)
qed
obtain v where v: "v \<in> F n" "v \<in> {z..y}" "({z..v} - {v}) \<inter> F n = {}"
proof (cases "z \<in> F n")
@@ -1771,9 +1752,10 @@
show "F n \<inter> {z..y} \<noteq> {}"
by (metis atLeastAtMost_iff disjoint_iff_not_equal greaterThanLessThan_iff less.prems(2) less_eq_real_def z)
show "\<And>b. \<lbrakk>b \<in> F n \<inter> {z..y}; open_segment z b \<inter> (F n \<inter> {z..y}) = {}\<rbrakk> \<Longrightarrow> thesis"
- apply (rule that)
- apply (auto simp: open_segment_eq_real_ivl)
- by (metis DiffI Int_iff atLeastAtMost_diff_ends atLeastAtMost_iff atLeastatMost_empty_iff empty_iff insert_iff False)
+ proof
+ show "\<And>b. \<lbrakk>b \<in> F n \<inter> {z..y}; open_segment z b \<inter> (F n \<inter> {z..y}) = {}\<rbrakk> \<Longrightarrow> ({z..b} - {b}) \<inter> F n = {}"
+ using False by (auto simp: open_segment_eq_real_ivl less_eq_real_def)
+ qed auto
qed
qed
obtain u v where "u \<in> {0..1}" "v \<in> {0..1}" "norm(u - x) < e" "norm(v - y) < e" "p u = p v"
@@ -1807,8 +1789,7 @@
qed
then show ?case
using e [of x u] e [of y v] xy
- apply (simp add: open_segment_eq_real_ivl dist_norm del: divide_const_simps)
- by (metis dist_norm dist_triangle_half_r less_irrefl)
+ by (metis dist_norm dist_triangle_half_r order_less_irrefl)
qed (auto simp: open_segment_commute)
show ?thesis
unfolding \<phi>_def by (metis (no_types, hide_lams) INT_I Inf_lower2 rangeI that(3) F01 subsetCE pqF)
@@ -1830,8 +1811,7 @@
have "insert x (open_segment x y \<union> open_segment x z) \<inter> T = {}"
by (metis False Int_Un_distrib2 Int_insert_left Un_empty_right xyT xzT)
moreover have "open_segment y z \<inter> T \<subseteq> insert x (open_segment x y \<union> open_segment x z) \<inter> T"
- apply auto
- by (metis greaterThanLessThan_iff less_eq_real_def less_le_trans linorder_neqE_linordered_idom open_segment_eq_real_ivl)
+ by (auto simp: open_segment_eq_real_ivl)
ultimately have "open_segment y z \<inter> T = {}"
by blast
with that peq show ?thesis by metis
@@ -1877,13 +1857,21 @@
have uvT: "closed (closed_segment u v \<inter> T)" "closed_segment u v \<inter> T \<noteq> {}"
using False open_closed_segment by (auto simp: \<open>closed T\<close> closed_Int)
obtain w where "w \<in> T" and w: "w \<in> closed_segment u v" "open_segment u w \<inter> T = {}"
- apply (rule segment_to_point_exists [OF uvT, of u])
- by (metis IntD1 Int_commute Int_left_commute ends_in_segment(1) inf.orderE subset_oc_segment)
+ proof (rule segment_to_point_exists [OF uvT])
+ fix b
+ assume "b \<in> closed_segment u v \<inter> T" "open_segment u b \<inter> (closed_segment u v \<inter> T) = {}"
+ then show thesis
+ by (metis IntD1 IntD2 ends_in_segment(1) inf.orderE inf_assoc subset_oc_segment that)
+ qed
then have puw: "dist (p u) (p w) < \<epsilon> / 2"
by (metis (no_types) \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE)
obtain z where "z \<in> T" and z: "z \<in> closed_segment u v" "open_segment v z \<inter> T = {}"
- apply (rule segment_to_point_exists [OF uvT, of v])
- by (metis IntD2 Int_commute Int_left_commute ends_in_segment(2) inf.orderE subset_oc_segment)
+ proof (rule segment_to_point_exists [OF uvT])
+ fix b
+ assume "b \<in> closed_segment u v \<inter> T" "open_segment v b \<inter> (closed_segment u v \<inter> T) = {}"
+ then show thesis
+ by (metis IntD1 IntD2 ends_in_segment(2) inf.orderE inf_assoc subset_oc_segment that)
+ qed
then have "dist (p u) (p z) < \<epsilon> / 2"
by (metis \<open>T \<subseteq> {0..1}\<close> \<open>dist v u < \<delta>\<close> \<delta> dist_commute dist_in_closed_segment le_less_trans subsetCE)
then show ?thesis
@@ -2048,11 +2036,10 @@
with y \<open>r > 0\<close> obtain g where "arc g" and pig: "path_image g \<subseteq> ball z r"
and g: "pathstart g = y" "pathfinish g = z"
using \<open>y \<noteq> z\<close> by (force simp: path_connected_arcwise)
- have "compact (g -` frontier S \<inter> {0..1})"
- apply (simp add: compact_eq_bounded_closed bounded_Int)
- apply (rule closed_vimage_Int)
- using \<open>arc g\<close> apply (auto simp: arc_def path_def)
- done
+ have "continuous_on {0..1} g"
+ using \<open>arc g\<close> arc_imp_path path_def by blast
+ then have "compact (g -` frontier S \<inter> {0..1})"
+ by (simp add: bounded_Int closed_Diff closed_vimage_Int compact_eq_bounded_closed)
moreover have "g -` frontier S \<inter> {0..1} \<noteq> {}"
proof -
have "\<exists>r. r \<in> g -` frontier S \<and> r \<in> {0..1}"
@@ -2082,11 +2069,7 @@
then show "pathfinish (subpath 0 t g) \<in> V"
by auto
then have "inj_on (subpath 0 t g) {0..1}"
- using t01
- apply (clarsimp simp: inj_on_def subpath_def)
- apply (drule inj_onD [OF arc_imp_inj_on [OF \<open>arc g\<close>]])
- using mult_le_one apply auto
- done
+ using t01 \<open>arc (subpath 0 t g)\<close> arc_imp_inj_on by blast
then have "subpath 0 t g ` {0..<1} \<subseteq> subpath 0 t g ` {0..1} - {subpath 0 t g 1}"
by (force simp: dest: inj_onD)
moreover have False if "subpath 0 t g ` ({0..<1}) - S \<noteq> {}"
@@ -2096,11 +2079,10 @@
have "subpath 0 t g ` {0..<1} \<inter> frontier S \<noteq> {}"
proof (rule connected_Int_frontier [OF _ _ that])
show "connected (subpath 0 t g ` {0..<1})"
- apply (rule connected_continuous_image)
- apply (simp add: subpath_def)
- apply (intro continuous_intros continuous_on_compose2 [OF contg])
- apply (auto simp: \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> mult_le_one)
- done
+ proof (rule connected_continuous_image)
+ show "continuous_on {0..<1} (subpath 0 t g)"
+ by (meson \<open>arc (subpath 0 t g)\<close> arc_def atLeastLessThan_subseteq_atLeastAtMost_iff continuous_on_subset order_refl path_def)
+ qed auto
show "subpath 0 t g ` {0..<1} \<inter> S \<noteq> {}"
using \<open>y \<in> S\<close> g(1) by (force simp: subpath_def image_def pathstart_def)
qed
@@ -2139,17 +2121,18 @@
by (simp add: \<open>arc g\<close> arc_imp_path)
then obtain h where "arc h"
and h: "path_image h \<subseteq> path_image (f +++ g)" "pathstart h = x" "pathfinish h = pathfinish g"
- apply (rule path_contains_arc [of "f +++ g" x "pathfinish g"])
- using f \<open>x \<notin> V\<close> \<open>pathfinish g \<in> V\<close> by auto
- have "h ` {0..1} - {h 1} \<subseteq> S"
- using f g h apply (clarsimp simp: path_image_join)
+ using path_contains_arc [of "f +++ g" x "pathfinish g"] \<open>x \<notin> V\<close> \<open>pathfinish g \<in> V\<close> f
+ by (metis pathfinish_join pathstart_join)
+ have "path_image h \<subseteq> path_image f \<union> path_image g"
+ using h(1) path_image_join_subset by auto
+ then have "h ` {0..1} - {h 1} \<subseteq> S"
+ using f g h
apply (simp add: path_image_def pathfinish_def subset_iff image_def Bex_def)
by (metis le_less)
then have "h ` {0..<1} \<subseteq> S"
using \<open>arc h\<close> by (force simp: arc_def dest: inj_onD)
then show thesis
- apply (rule that [OF \<open>arc h\<close>])
- using h \<open>pathfinish g \<in> V\<close> by auto
+ using \<open>arc h\<close> g(3) h that by presburger
qed
lemma dense_access_fp_aux:
@@ -2188,9 +2171,10 @@
proof
show "arc \<gamma>" "pathstart \<gamma> \<in> U" "pathfinish \<gamma> \<in> V"
using \<gamma> \<open>arc \<gamma>\<close> \<open>pathfinish h \<in> U - {pathfinish g}\<close> \<open>pathfinish g \<in> V\<close> by auto
- have "\<gamma> ` {0..1} - {\<gamma> 0, \<gamma> 1} \<subseteq> S"
- using \<gamma> g h
- apply (simp add: path_image_join)
+ have "path_image \<gamma> \<subseteq> path_image h \<union> path_image g"
+ by (metis \<gamma>(1) g(2) h(2) path_image_join path_image_reversepath pathfinish_reversepath)
+ then have "\<gamma> ` {0..1} - {\<gamma> 0, \<gamma> 1} \<subseteq> S"
+ using \<gamma> g h
apply (simp add: path_image_def pathstart_def pathfinish_def subset_iff image_def Bex_def)
by (metis linorder_neqE_linordered_idom not_less)
then show "\<gamma> ` {0<..<1} \<subseteq> S"
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Oct 31 21:06:29 2020 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Oct 31 21:24:40 2020 +0000
@@ -14,6 +14,10 @@
Cartesian_Euclidean_Space
begin
+lemma LIMSEQ_if_less: "(\<lambda>k. if i < k then a else b) \<longlonglongrightarrow> a"
+ by (rule_tac k="Suc i" in LIMSEQ_offset) auto
+
+text \<open>Note that the rhs is an implication. This lemma plays a specific role in one proof.\<close>
lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
by (auto intro: order_trans)
@@ -227,8 +231,8 @@
also have "\<dots> = ?\<mu> E - ?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}})"
using \<open>E \<in> sets ?L\<close> fin[of X] sets[of X] by (auto intro!: emeasure_Diff)
finally have "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}}) \<le> e"
- using \<open>0 < e\<close> e_less_M apply (cases "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}})")
- by (auto simp add: \<open>?\<mu> E = M\<close> ennreal_minus ennreal_le_iff2)
+ using \<open>0 < e\<close> e_less_M
+ by (cases "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}})") (auto simp add: \<open>?\<mu> E = M\<close> ennreal_minus ennreal_le_iff2)
note this }
note upper_bound = this
@@ -345,12 +349,8 @@
proof cases
assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b"
then show ?thesis
- apply simp
- apply (subst has_integral_restrict[symmetric, OF box_subset_cbox])
- apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"])
using has_integral_const[of "1::real" l u]
- apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases)
- done
+ by (simp flip: has_integral_restrict[OF box_subset_cbox] add: has_integral_spike_interior)
next
assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)"
then have "box l u = {}"
@@ -405,11 +405,8 @@
by (intro sum_mono2) auto
from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
by (auto simp add: disjoint_family_on_def)
- show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> \<Union>(F ` UNIV) \<inter> box a b then 1 else 0)"
- apply (auto simp: * sum.If_cases Iio_Int_singleton)
- apply (rule_tac k="Suc xa" in LIMSEQ_offset)
- apply simp
- done
+ show "(\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> \<Union>(F ` UNIV) \<inter> box a b then 1 else 0)" for x
+ by (auto simp: * sum.If_cases Iio_Int_singleton if_distrib LIMSEQ_if_less cong: if_cong)
have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
by (intro emeasure_mono) auto
@@ -486,14 +483,8 @@
case (seq U)
note seq(1)[measurable] and f[measurable]
- { fix i x
- have "U i x \<le> f x"
- using seq(5)
- apply (rule LIMSEQ_le_const)
- using seq(4)
- apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def)
- done }
- note U_le_f = this
+ have U_le_f: "U i x \<le> f x" for i x
+ by (metis (no_types) LIMSEQ_le_const UNIV_I incseq_def le_fun_def seq.hyps(4) seq.hyps(5) space_borel)
{ fix i
have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)"
@@ -910,9 +901,7 @@
using assms has_integral_integral_lborel
unfolding set_integrable_def set_lebesgue_integral_def by blast
hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
- apply (subst has_integral_restrict_UNIV [symmetric])
- apply (rule has_integral_eq)
- by auto
+ by (simp add: indicator_scaleR_eq_if)
thus "f integrable_on S"
by (auto simp add: integrable_on_def)
with 1 have "(f has_integral (integral S f)) S"
@@ -1088,8 +1077,8 @@
lemma absolutely_integrable_reflect[simp]:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "(\<lambda>x. f(-x)) absolutely_integrable_on cbox (-b) (-a) \<longleftrightarrow> f absolutely_integrable_on cbox a b"
- apply (auto simp: absolutely_integrable_on_def dest: integrable_reflect [THEN iffD1])
- unfolding integrable_on_def by auto
+ unfolding absolutely_integrable_on_def
+ by (metis (mono_tags, lifting) integrable_eq integrable_reflect)
lemma absolutely_integrable_reflect_real[simp]:
fixes f :: "real \<Rightarrow> 'b::euclidean_space"
@@ -1168,15 +1157,16 @@
proof -
have "integral UNIV (indicator (S \<inter> T)) = integral UNIV (\<lambda>a. if a \<in> S \<inter> T then 1::real else 0)"
by (meson indicator_def)
- moreover
- have "(indicator (S \<inter> T) has_integral measure lebesgue (S \<inter> T)) UNIV"
+ moreover have "(indicator (S \<inter> T) has_integral measure lebesgue (S \<inter> T)) UNIV"
using assms by (simp add: lmeasurable_iff_has_integral)
ultimately have "integral UNIV (\<lambda>x. if x \<in> S \<inter> T then 1 else 0) = measure lebesgue (S \<inter> T)"
by (metis (no_types) integral_unique)
- then show ?thesis
- using integral_restrict_Int [of UNIV "S \<inter> T" "\<lambda>x. 1::real"]
- apply (simp add: integral_restrict_Int [symmetric])
+ moreover have "integral T (\<lambda>a. if a \<in> S then 1::real else 0) = integral (S \<inter> T \<inter> UNIV) (\<lambda>a. 1)"
+ by (simp add: Henstock_Kurzweil_Integration.integral_restrict_Int)
+ moreover have "integral T (indicat_real S) = integral T (\<lambda>a. if a \<in> S then 1 else 0)"
by (meson indicator_def)
+ ultimately show ?thesis
+ by (simp add: assms lmeasure_integral)
qed
lemma measurable_integrable:
@@ -1234,9 +1224,8 @@
by (meson has_measure_limit fmeasurable.Int lmeasurable_cbox)
next
assume RHS [rule_format]: ?rhs
- show ?lhs
+ then show ?lhs
apply (simp add: lmeasurable_iff_indicator_has_integral has_integral' [where i=m])
- using RHS
by (metis (full_types) integral_indicator integrable_integral integrable_on_indicator)
qed
@@ -1305,14 +1294,13 @@
assumes "a \<noteq> 0 \<or> b \<noteq> 0" shows "negligible {x. a \<bullet> x = b}"
proof -
obtain x where x: "a \<bullet> x \<noteq> b"
- using assms
- apply auto
- apply (metis inner_eq_zero_iff inner_zero_right)
- using inner_zero_right by fastforce
+ using assms by (metis euclidean_all_zero_iff inner_zero_right)
+ moreover have "c = 1" if "a \<bullet> (x + c *\<^sub>R w) = b" "a \<bullet> (x + w) = b" for c w
+ using that
+ by (metis (no_types, hide_lams) add_diff_eq diff_0 diff_minus_eq_add inner_diff_right inner_scaleR_right mult_cancel_right2 right_minus_eq x)
+ ultimately
show ?thesis
- apply (rule starlike_negligible [OF closed_hyperplane, of x])
- using x apply (auto simp: algebra_simps)
- done
+ using starlike_negligible [OF closed_hyperplane, of x] by simp
qed
lemma negligible_lowdim:
@@ -1348,12 +1336,15 @@
(simp_all add: frontier_def negligible_lowdim 1)
next
case 2
- obtain a where a: "a \<in> interior S"
- apply (rule interior_simplex_nonempty [OF indB])
- apply (simp add: indB independent_finite)
- apply (simp add: cardB 2)
- apply (metis \<open>B \<subseteq> S\<close> \<open>0 \<in> S\<close> \<open>convex S\<close> insert_absorb insert_subset interior_mono subset_hull)
- done
+ obtain a where "a \<in> interior (convex hull insert 0 B)"
+ proof (rule interior_simplex_nonempty [OF indB])
+ show "finite B"
+ by (simp add: indB independent_finite)
+ show "card B = DIM('N)"
+ by (simp add: cardB 2)
+ qed
+ then have a: "a \<in> interior S"
+ by (metis \<open>B \<subseteq> S\<close> \<open>0 \<in> S\<close> \<open>convex S\<close> insert_absorb insert_subset interior_mono subset_hull)
show ?thesis
proof (rule starlike_negligible_strong [where a=a])
fix c::real and x
@@ -1361,10 +1352,9 @@
by (simp add: algebra_simps)
assume "0 \<le> c" "c < 1" "a + x \<in> frontier S"
then show "a + c *\<^sub>R x \<notin> frontier S"
- apply (clarsimp simp: frontier_def)
- apply (subst eq)
- apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a, of _ "1-c"], auto)
- done
+ using eq mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a, of _ "1-c"]
+ unfolding frontier_def
+ by (metis Diff_iff add_diff_cancel_left' add_diff_eq diff_gt_0_iff_gt group_cancel.rule0 not_le)
qed auto
qed
qed
@@ -1426,10 +1416,7 @@
lemma negligible_convex_interior:
"convex S \<Longrightarrow> (negligible S \<longleftrightarrow> interior S = {})"
- apply safe
- apply (metis interior_subset negligible_subset open_interior open_not_negligible)
- apply (metis Diff_empty closure_subset frontier_def negligible_convex_frontier negligible_subset)
- done
+ by (metis Diff_empty closure_subset frontier_def interior_subset negligible_convex_frontier negligible_subset open_interior open_not_negligible)
lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
by (auto simp: measure_def null_sets_def)
@@ -1441,8 +1428,7 @@
by (auto simp: measure_eq_0_null_sets negligible_iff_null_sets)
lemma negligible_iff_measure0: "S \<in> lmeasurable \<Longrightarrow> (negligible S \<longleftrightarrow> measure lebesgue S = 0)"
- apply (auto simp: measure_eq_0_null_sets negligible_iff_null_sets)
- by (metis completion.null_sets_outer subsetI)
+ by (metis (full_types) completion.null_sets_outer negligible_iff_null_sets negligible_imp_measure0 order_refl)
lemma negligible_imp_sets: "negligible S \<Longrightarrow> S \<in> sets lebesgue"
by (simp add: negligible_iff_null_sets null_setsD2)
@@ -1474,12 +1460,7 @@
qed
lemma negligible_UNIV: "negligible S \<longleftrightarrow> (indicat_real S has_integral 0) UNIV" (is "_=?rhs")
-proof
- assume ?rhs
- then show "negligible S"
- apply (auto simp: negligible_def has_integral_iff integrable_on_indicator)
- by (metis negligible integral_unique lmeasure_integral_UNIV negligible_iff_measure0)
-qed (simp add: negligible)
+ by (metis lmeasurable_iff_indicator_has_integral negligible_iff_measure)
lemma sets_negligible_symdiff:
"\<lbrakk>S \<in> sets lebesgue; negligible((S - T) \<union> (T - S))\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
@@ -1688,11 +1669,7 @@
then obtain \<epsilon> where "0 < \<epsilon>" "ball x \<epsilon> \<subseteq> T \<inter> U"
by (metis \<open>open T\<close> \<open>open U\<close> openE open_Int)
then show ?thesis
- apply (rule_tac x="min (1/2) \<epsilon>" in exI)
- apply (simp del: divide_const_simps)
- apply (intro allI impI conjI)
- apply (metis dist_commute dist_norm mem_ball subsetCE)
- by (metis Int_iff subsetCE U dist_norm mem_ball norm_minus_commute)
+ by (rule_tac x="min (1/2) \<epsilon>" in exI) (simp add: U dist_norm norm_minus_commute subset_iff)
next
case False
then show ?thesis
@@ -1709,10 +1686,13 @@
obtain B where B: "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
using \<open>bounded S\<close> bounded_iff by blast
show ?thesis
- apply (rule_tac c = "abs B + 1" in that)
- using norm_bound_Basis_le Basis_le_norm
- apply (fastforce simp: box_eq_empty mem_box dest!: B intro: order_trans)+
- done
+ proof (rule_tac c = "abs B + 1" in that)
+ show "S \<subseteq> cbox (- (\<bar>B\<bar> + 1) *\<^sub>R One) ((\<bar>B\<bar> + 1) *\<^sub>R One)"
+ using norm_bound_Basis_le Basis_le_norm
+ by (fastforce simp: mem_box dest!: B intro: order_trans)
+ show "box (- (\<bar>B\<bar> + 1) *\<^sub>R One) ((\<bar>B\<bar> + 1) *\<^sub>R One) \<noteq> {}"
+ by (simp add: box_eq_empty(1))
+ qed
qed
obtain \<D> where "countable \<D>"
and Dsub: "\<Union>\<D> \<subseteq> cbox (-c *\<^sub>R One) (c *\<^sub>R One)"
@@ -1728,10 +1708,7 @@
obtain u v where "K = cbox u v"
using \<open>K \<in> \<D>\<close> cbox by blast
with that show ?thesis
- apply (rule_tac x=u in exI)
- apply (rule_tac x=v in exI)
- apply (metis Int_iff interior_cbox cbox Ksub)
- done
+ by (metis Int_iff interior_cbox cbox Ksub)
qed
then obtain uf vf zf
where uvz: "\<And>K. K \<in> \<D> \<Longrightarrow>
@@ -1771,8 +1748,7 @@
have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
by (rule prod_constant [symmetric])
also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
- apply (rule prod.cong [OF refl])
- by (simp add: \<open>X \<in> \<D>\<close> inner_diff_left prj1_idem)
+ by (simp add: \<open>X \<in> \<D>\<close> inner_diff_left prj1_idem cong: prod.cong)
finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
@@ -1788,11 +1764,9 @@
have 0: "0 \<le> prj1 (vf X - uf X)"
using \<open>X \<in> \<D>\<close> prj1_def vu_pos by fastforce
have "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
- apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close>)
- apply (simp add: power_mult_distrib \<open>0 < B\<close> prj1_eq [symmetric])
+ apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> \<open>0 < B\<close> flip: prj1_eq)
using MleN 0 1 uvz \<open>X \<in> \<D>\<close>
- apply (fastforce simp add: box_ne_empty power_decreasing)
- done
+ by (fastforce simp add: box_ne_empty power_decreasing)
also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X"
by (subst (3) ufvf[symmetric]) simp
finally show "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * measure lebesgue X" .
@@ -1801,11 +1775,11 @@
by (simp add: sum_distrib_left)
also have "\<dots> \<le> e/2"
proof -
- have div: "\<D>' division_of \<Union>\<D>'"
- apply (auto simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
- using cbox that apply blast
- using pairwise_subset [OF pw \<open>\<D>' \<subseteq> \<D>\<close>] unfolding pairwise_def apply force+
- done
+ have "\<And>K. K \<in> \<D>' \<Longrightarrow> \<exists>a b. K = cbox a b"
+ using cbox that by blast
+ then have div: "\<D>' division_of \<Union>\<D>'"
+ using pairwise_subset [OF pw \<open>\<D>' \<subseteq> \<D>\<close>] unfolding pairwise_def
+ by (force simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
have le_meaT: "measure lebesgue (\<Union>\<D>') \<le> measure lebesgue T"
proof (rule measure_mono_fmeasurable)
show "(\<Union>\<D>') \<in> sets lebesgue"
@@ -1830,10 +1804,8 @@
(2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue (\<Union>\<D>')"
using content_division [OF div] by auto
also have "\<dots> \<le> (2 * B * real DIM('M)) ^ DIM('N) * measure lebesgue T"
- apply (rule mult_left_mono [OF le_meaT])
- using \<open>0 < B\<close>
- apply (simp add: algebra_simps)
- done
+ using \<open>0 < B\<close>
+ by (intro mult_left_mono [OF le_meaT]) (force simp add: algebra_simps)
also have "\<dots> \<le> e/2"
using T \<open>0 < B\<close> by (simp add: field_simps)
finally show ?thesis .
@@ -1924,12 +1896,10 @@
then show ?thesis
using B order_trans that by blast
qed
- have "x \<in> ?S (nat (ceiling (max B (norm x))))"
- apply (simp add: \<open>x \<in> S \<close>, rule)
- using real_nat_ceiling_ge max.bounded_iff apply blast
- using T no
- apply (force simp: algebra_simps)
- done
+ have "norm x \<le> real (nat \<lceil>max B (norm x)\<rceil>)"
+ by linarith
+ then have "x \<in> ?S (nat (ceiling (max B (norm x))))"
+ using T no by (force simp: \<open>x \<in> S\<close> algebra_simps)
then show "x \<in> (\<Union>n. ?S n)" by force
qed auto
then show ?thesis
@@ -1946,9 +1916,9 @@
if "x \<in> S" for x
proof -
obtain f' where "linear f'"
- and f': "\<And>e. e>0 \<Longrightarrow>
- \<exists>d>0. \<forall>y\<in>S. norm (y - x) < d \<longrightarrow>
- norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)"
+ and f': "\<And>e. e>0 \<Longrightarrow>
+ \<exists>d>0. \<forall>y\<in>S. norm (y - x) < d \<longrightarrow>
+ norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)"
using diff_f \<open>x \<in> S\<close>
by (auto simp: linear_linear differentiable_on_def differentiable_def has_derivative_within_alt)
obtain B where "B > 0" and B: "\<forall>x. norm (f' x) \<le> B * norm x"
@@ -1957,24 +1927,21 @@
and d: "\<And>y. \<lbrakk>y \<in> S; norm (y - x) < d\<rbrakk> \<Longrightarrow>
norm (f y - f x - f' (y - x)) \<le> norm (y - x)"
using f' [of 1] by (force simp:)
- have *: "norm (f y - f x) \<le> (B + 1) * norm (y - x)"
- if "y \<in> S" "norm (y - x) < d" for y
- proof -
- have "norm (f y - f x) -B * norm (y - x) \<le> norm (f y - f x) - norm (f' (y - x))"
- by (simp add: B)
- also have "\<dots> \<le> norm (f y - f x - f' (y - x))"
- by (rule norm_triangle_ineq2)
- also have "... \<le> norm (y - x)"
- by (rule d [OF that])
- finally show ?thesis
- by (simp add: algebra_simps)
- qed
show ?thesis
- apply (rule_tac x="ball x d" in exI)
- apply (rule_tac x="B+1" in exI)
- using \<open>d>0\<close>
- apply (auto simp: dist_norm norm_minus_commute intro!: *)
- done
+ proof (intro exI conjI ballI)
+ show "norm (f y - f x) \<le> (B + 1) * norm (y - x)"
+ if "y \<in> S \<inter> ball x d" for y
+ proof -
+ have "norm (f y - f x) - B * norm (y - x) \<le> norm (f y - f x) - norm (f' (y - x))"
+ by (simp add: B)
+ also have "\<dots> \<le> norm (f y - f x - f' (y - x))"
+ by (rule norm_triangle_ineq2)
+ also have "... \<le> norm (y - x)"
+ by (metis IntE d dist_norm mem_ball norm_minus_commute that)
+ finally show ?thesis
+ by (simp add: algebra_simps)
+ qed
+ qed (use \<open>d>0\<close> in auto)
qed
with negligible_locally_Lipschitz_image assms show ?thesis by metis
qed
@@ -1990,25 +1957,28 @@
where "linear lift" "linear drop" and dropl [simp]: "\<And>z. drop (lift z) = z"
and "j \<in> Basis" and j: "\<And>x. lift(x,0) \<bullet> j = 0"
using lowerdim_embeddings [OF MlessN] by metis
- have "negligible {x. x\<bullet>j = 0}"
- by (metis \<open>j \<in> Basis\<close> negligible_standard_hyperplane)
- then have neg0S: "negligible ((\<lambda>x. lift (x, 0)) ` S)"
- apply (rule negligible_subset)
- by (simp add: image_subsetI j)
- have diff_f': "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S"
+ have "negligible ((\<lambda>x. lift (x, 0)) ` S)"
+ proof -
+ have "negligible {x. x\<bullet>j = 0}"
+ by (metis \<open>j \<in> Basis\<close> negligible_standard_hyperplane)
+ moreover have "(\<lambda>m. lift (m, 0)) ` S \<subseteq> {n. n \<bullet> j = 0}"
+ using j by force
+ ultimately show ?thesis
+ using negligible_subset by auto
+ qed
+ moreover
+ have "f \<circ> fst \<circ> drop differentiable_on (\<lambda>x. lift (x, 0)) ` S"
using diff_f
apply (clarsimp simp add: differentiable_on_def)
apply (intro differentiable_chain_within linear_imp_differentiable [OF \<open>linear drop\<close>]
linear_imp_differentiable [OF linear_fst])
apply (force simp: image_comp o_def)
done
- have "f = (f o fst o drop o (\<lambda>x. lift (x, 0)))"
+ moreover
+ have "f = f \<circ> fst \<circ> drop \<circ> (\<lambda>x. lift (x, 0))"
by (simp add: o_def)
- then show ?thesis
- apply (rule ssubst)
- apply (subst image_comp [symmetric])
- apply (metis negligible_differentiable_image_negligible order_refl diff_f' neg0S)
- done
+ ultimately show ?thesis
+ by (metis (no_types) image_comp negligible_differentiable_image_negligible order_refl)
qed
subsection\<open>Measurability of countable unions and intersections of various kinds.\<close>
@@ -2020,21 +1990,24 @@
shows measurable_nested_Union: "(\<Union>n. S n) \<in> lmeasurable"
and measure_nested_Union: "(\<lambda>n. measure lebesgue (S n)) \<longlonglongrightarrow> measure lebesgue (\<Union>n. S n)" (is ?Lim)
proof -
- have 1: "\<And>n. (indicat_real (S n)) integrable_on UNIV"
- using S measurable_integrable by blast
- have 2: "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
- by (simp add: indicator_leI nest rev_subsetD)
- have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (\<Union>(S ` UNIV)) x)"
- apply (rule tendsto_eventually)
- apply (simp add: indicator_def)
- by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
- have 4: "bounded (range (\<lambda>n. integral UNIV (indicat_real (S n))))"
- using leB by (auto simp: lmeasure_integral_UNIV [symmetric] S bounded_iff)
- have "(\<Union>n. S n) \<in> lmeasurable \<and> ?Lim"
- apply (simp add: lmeasure_integral_UNIV S cong: conj_cong)
- apply (simp add: measurable_integrable)
- apply (rule monotone_convergence_increasing [OF 1 2 3 4])
- done
+ have "indicat_real (\<Union> (range S)) integrable_on UNIV \<and>
+ (\<lambda>n. integral UNIV (indicat_real (S n)))
+ \<longlonglongrightarrow> integral UNIV (indicat_real (\<Union> (range S)))"
+ proof (rule monotone_convergence_increasing)
+ show "\<And>n. (indicat_real (S n)) integrable_on UNIV"
+ using S measurable_integrable by blast
+ show "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
+ by (simp add: indicator_leI nest rev_subsetD)
+ have "\<And>x. (\<exists>n. x \<in> S n) \<longrightarrow> (\<forall>\<^sub>F n in sequentially. x \<in> S n)"
+ by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
+ then
+ show "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (\<Union>(S ` UNIV)) x)"
+ by (simp add: indicator_def tendsto_eventually)
+ show "bounded (range (\<lambda>n. integral UNIV (indicat_real (S n))))"
+ using leB by (auto simp: lmeasure_integral_UNIV [symmetric] S bounded_iff)
+ qed
+ then have "(\<Union>n. S n) \<in> lmeasurable \<and> ?Lim"
+ by (simp add: lmeasure_integral_UNIV S cong: conj_cong) (simp add: measurable_integrable)
then show "(\<Union>n. S n) \<in> lmeasurable" "?Lim"
by auto
qed
@@ -2094,8 +2067,9 @@
using measure_negligible_finite_Union_image [OF _ _ pairwise_subset] djointish
by (metis S finite_atMost subset_UNIV)
also have "\<dots> \<le> measure lebesgue (cbox a b)"
- apply (rule measure_mono_fmeasurable)
- using ab S by force+
+ proof (rule measure_mono_fmeasurable)
+ show "\<Union> (S ` {..n}) \<in> sets lebesgue" using S by blast
+ qed (use ab in auto)
finally show ?thesis .
qed
show "(\<Union>n. S n) \<in> lmeasurable"
@@ -2167,12 +2141,9 @@
using negligible_subset by blast
qed
-lemma locally_negligible:
- "locally negligible S \<longleftrightarrow> negligible S"
+lemma locally_negligible: "locally negligible S \<longleftrightarrow> negligible S"
unfolding locally_def
- apply safe
- apply (meson negligible_subset openin_subtopology_self locally_negligible_alt)
- by (meson negligible_subset openin_imp_subset order_refl)
+ by (metis locally_negligible_alt negligible_subset openin_imp_subset openin_subtopology_self)
subsection\<open>Integral bounds\<close>
@@ -2237,15 +2208,17 @@
qed
lemma absdiff_norm_less:
- assumes "sum (\<lambda>x. norm (f x - g x)) s < e"
- and "finite s"
- shows "\<bar>sum (\<lambda>x. norm(f x)) s - sum (\<lambda>x. norm(g x)) s\<bar> < e"
- unfolding sum_subtractf[symmetric]
- apply (rule le_less_trans[OF sum_abs])
- apply (rule le_less_trans[OF _ assms(1)])
- apply (rule sum_mono)
- apply (rule norm_triangle_ineq3)
- done
+ assumes "sum (\<lambda>x. norm (f x - g x)) S < e"
+ shows "\<bar>sum (\<lambda>x. norm(f x)) S - sum (\<lambda>x. norm(g x)) S\<bar> < e" (is "?lhs < e")
+proof -
+ have "?lhs \<le> (\<Sum>i\<in>S. \<bar>norm (f i) - norm (g i)\<bar>)"
+ by (metis (no_types) sum_abs sum_subtractf)
+ also have "... \<le> (\<Sum>x\<in>S. norm (f x - g x))"
+ by (simp add: norm_triangle_ineq3 sum_mono)
+ also have "... < e"
+ using assms(1) by blast
+ finally show ?thesis .
+qed
proposition bounded_variation_absolutely_integrable_interval:
fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
@@ -2344,17 +2317,6 @@
next
have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
unfolding p'_def using d' by blast
- have "y \<in> \<Union>{K. \<exists>x. (x, K) \<in> p'}" if y: "y \<in> cbox a b" for y
- proof -
- obtain x l where xl: "(x, l) \<in> p" "y \<in> l"
- using y unfolding p'(6)[symmetric] by auto
- obtain i where i: "i \<in> d" "y \<in> i"
- using y unfolding d'(6)[symmetric] by auto
- have "x \<in> i"
- using fineD[OF p(3) xl(1)] using k(2) i xl by auto
- then show ?thesis
- unfolding p'_def by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
- qed
show "\<Union>{K. \<exists>x. (x, K) \<in> p'} = cbox a b"
proof
show "\<Union>{k. \<exists>x. (x, k) \<in> p'} \<subseteq> cbox a b"
@@ -2370,17 +2332,24 @@
using y unfolding d'(6)[symmetric] by auto
have "x \<in> I"
using fineD[OF p(3) xl(1)] using k(2) i xl by auto
- then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
- apply (rule_tac X="I \<inter> L" in UnionI)
- using i xl by (auto simp: p'_def)
+ then show "y \<in> \<Union>{K. \<exists>x. (x, K) \<in> p'}"
+ proof -
+ obtain x l where xl: "(x, l) \<in> p" "y \<in> l"
+ using y unfolding p'(6)[symmetric] by auto
+ obtain i where i: "i \<in> d" "y \<in> i"
+ using y unfolding d'(6)[symmetric] by auto
+ have "x \<in> i"
+ using fineD[OF p(3) xl(1)] using k(2) i xl by auto
+ then show ?thesis
+ unfolding p'_def by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
+ qed
qed
qed
qed
-
then have sum_less_e2: "(\<Sum>(x,K) \<in> p'. norm (content K *\<^sub>R f x - integral K f)) < e/2"
using g(2) gp' tagged_division_of_def by blast
- have "(x, I \<inter> L) \<in> p'" if x: "(x, L) \<in> p" "I \<in> d" and y: "y \<in> I" "y \<in> L"
+ have in_p': "(x, I \<inter> L) \<in> p'" if x: "(x, L) \<in> p" "I \<in> d" and y: "y \<in> I" "y \<in> L"
for x I L y
proof -
have "x \<in> I"
@@ -2391,7 +2360,8 @@
by (simp add: p'_def)
with y show ?thesis by auto
qed
- moreover have "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
+ moreover
+ have Ex_p_p': "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
if xK: "(x,K) \<in> p'" for x K
proof -
obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l"
@@ -2402,9 +2372,10 @@
ultimately have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
by auto
have sum_p': "(\<Sum>(x,K) \<in> p'. norm (integral K f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
- apply (subst sum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
- apply (auto intro: integral_null simp: content_eq_0_interior)
- done
+ proof (rule sum.over_tagged_division_lemma[OF p''])
+ show "\<And>u v. box u v = {} \<Longrightarrow> norm (integral (cbox u v) f) = 0"
+ by (auto intro: integral_null simp: content_eq_0_interior)
+ qed
have snd_p_div: "snd ` p division_of cbox a b"
by (rule division_of_tagged_division[OF p(1)])
note snd_p = division_ofD[OF snd_p_div]
@@ -2432,28 +2403,30 @@
define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and> cbox u v \<inter> l \<noteq> {}}"
have uvab: "cbox u v \<subseteq> cbox a b"
using d(1) k uv by blast
- have "d' division_of cbox u v"
+ have d'_div: "d' division_of cbox u v"
unfolding d'_def by (rule division_inter_1 [OF snd_p_div uvab])
- moreover then have "norm (\<Sum>i\<in>d'. integral i f) \<le> (\<Sum>k\<in>d'. norm (integral k f))"
+ moreover have "norm (\<Sum>i\<in>d'. integral i f) \<le> (\<Sum>k\<in>d'. norm (integral k f))"
by (simp add: sum_norm_le)
+ moreover have "f integrable_on K"
+ using f integrable_on_subcbox uv uvab by blast
+ moreover have "d' division_of K"
+ using d'_div uv by blast
ultimately have "norm (integral K f) \<le> sum (\<lambda>k. norm (integral k f)) d'"
- apply (subst integral_combine_division_topdown[of _ _ d'])
- apply (auto simp: uv intro: integrable_on_subcbox[OF assms(1) uvab])
- done
+ by (simp add: integral_combine_division_topdown)
also have "\<dots> = (\<Sum>I\<in>{K \<inter> L |L. L \<in> snd ` p}. norm (integral I f))"
- proof -
- have *: "norm (integral I f) = 0"
- if "I \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
- "I \<notin> {cbox u v \<inter> l |l. l \<in> snd ` p \<and> cbox u v \<inter> l \<noteq> {}}" for I
- using that by auto
- show ?thesis
- apply (rule sum.mono_neutral_left)
- apply (simp add: snd_p(1))
- unfolding d'_def uv using * by auto
+ proof (rule sum.mono_neutral_left)
+ show "finite {K \<inter> L |L. L \<in> snd ` p}"
+ by (simp add: snd_p(1))
+ show "\<forall>i\<in>{K \<inter> L |L. L \<in> snd ` p} - d'. norm (integral i f) = 0"
+ "d' \<subseteq> {K \<inter> L |L. L \<in> snd ` p}"
+ using d'_def image_eqI uv by auto
qed
also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))"
- proof -
- have *: "norm (integral (K \<inter> l) f) = 0"
+ unfolding Setcompr_eq_image
+ proof (rule sum.reindex_nontrivial [unfolded o_def])
+ show "finite (snd ` p)"
+ using snd_p(1) by blast
+ show "norm (integral (K \<inter> l) f) = 0"
if "l \<in> snd ` p" "y \<in> snd ` p" "l \<noteq> y" "K \<inter> l = K \<inter> y" for l y
proof -
have "interior (K \<inter> l) \<subseteq> interior (l \<inter> y)"
@@ -2468,12 +2441,6 @@
unfolding uv Int_interval content_eq_0_interior
by (metis (mono_tags, lifting) norm_eq_zero)
qed
- show ?thesis
- unfolding Setcompr_eq_image
- apply (rule sum.reindex_nontrivial [unfolded o_def])
- apply (rule finite_imageI)
- apply (rule p')
- using * by auto
qed
finally show "norm (integral K f) \<le> (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))" .
qed
@@ -2485,7 +2452,7 @@
proof -
have eq0: " (integral (l1 \<inter> k1) f) = 0"
if "l1 \<inter> k1 = l2 \<inter> k2" "(l1, k1) \<noteq> (l2, k2)"
- "l1 \<in> d" "(j1,k1) \<in> p" "l2 \<in> d" "(j2,k2) \<in> p"
+ "l1 \<in> d" "(j1,k1) \<in> p" "l2 \<in> d" "(j2,k2) \<in> p"
for l1 l2 k1 k2 j1 j2
proof -
obtain u1 v1 u2 v2 where uv: "l1 = cbox u1 u2" "k1 = cbox v1 v2"
@@ -2508,26 +2475,14 @@
by (metis eq0 fst_conv snd_conv)
qed
also have "\<dots> = (\<Sum>(x,k) \<in> p'. norm (integral k f))"
- proof -
- have 0: "integral (ia \<inter> snd (a, b)) f = 0"
- if "ia \<inter> snd (a, b) \<notin> snd ` p'" "ia \<in> d" "(a, b) \<in> p" for ia a b
- proof -
- have "ia \<inter> b = {}"
- using that unfolding p'alt image_iff Bex_def not_ex
- apply (erule_tac x="(a, ia \<inter> b)" in allE)
- apply auto
- done
- then show ?thesis by auto
- qed
- have 1: "\<exists>i l. snd (a, b) = i \<inter> l \<and> i \<in> d \<and> l \<in> snd ` p" if "(a, b) \<in> p'" for a b
- using that
- apply (clarsimp simp: p'_def image_iff)
- by (metis (no_types, hide_lams) snd_conv)
- show ?thesis
- unfolding sum_p'
- apply (rule sum.mono_neutral_right)
- apply (metis * finite_imageI[OF fin_d_sndp])
- using 0 1 by auto
+ unfolding sum_p'
+ proof (rule sum.mono_neutral_right)
+ show "finite {i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}"
+ by (metis * finite_imageI[OF fin_d_sndp])
+ show "snd ` p' \<subseteq> {i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}"
+ by (clarsimp simp: p'_def) (metis image_eqI snd_conv)
+ show "\<forall>i\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p} - snd ` p'. norm (integral i f) = 0"
+ by clarsimp (metis Henstock_Kurzweil_Integration.integral_empty disjoint_iff image_eqI in_p' snd_conv)
qed
finally show ?thesis .
qed
@@ -2540,11 +2495,10 @@
using finite_cartesian_product[OF p'(1) d'(1)] by metis
have "(\<Sum>(x,k) \<in> p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x,k) \<in> ?S. \<bar>content k\<bar> * norm (f x))"
unfolding norm_scaleR
- apply (rule sum.mono_neutral_left)
- apply (subst *)
- apply (rule finite_imageI [OF fin_pd])
- unfolding p'alt apply auto
- by fastforce
+ proof (rule sum.mono_neutral_left)
+ show "finite {(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
+ by (simp add: "*" fin_pd)
+ qed (use p'alt in \<open>force+\<close>)
also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
proof -
have "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
@@ -2557,8 +2511,7 @@
have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
using that by auto
then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
- apply (rule disjE)
- using that p'(5) d'(5) by auto
+ using that p'(5) d'(5) by (metis snd_conv)
moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
unfolding that ..
ultimately have "interior (l1 \<inter> k1) = {}"
@@ -2570,8 +2523,7 @@
unfolding *
apply (subst sum.reindex_nontrivial [OF fin_pd])
unfolding split_paired_all o_def split_def prod.inject
- apply force+
- done
+ by force+
qed
also have "\<dots> = (\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x))"
proof -
@@ -2601,20 +2553,17 @@
qed
then show ?thesis
unfolding Setcompr_eq_image
- apply (rule sum.reindex_nontrivial [OF \<open>finite d\<close>, unfolded o_def, symmetric])
- by auto
+ by (fastforce intro: sum.reindex_nontrivial [OF \<open>finite d\<close>, unfolded o_def, symmetric])
qed
also have "\<dots> = sum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
- apply (rule sum.mono_neutral_right)
- unfolding Setcompr_eq_image
- apply (rule finite_imageI [OF \<open>finite d\<close>])
- apply (fastforce simp: inf.commute)+
- done
- finally show "(\<Sum>i\<in>d. content (l \<inter> i) * norm (f x)) = content l * norm (f x)"
- unfolding sum_distrib_right[symmetric] real_scaleR_def
- apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
- using xl(2)[unfolded uv] unfolding uv apply auto
- done
+ proof (rule sum.mono_neutral_right)
+ show "finite {k \<inter> cbox u v |k. k \<in> d}"
+ by (simp add: d'(1))
+ qed (fastforce simp: inf.commute)+
+ finally have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = content (cbox u v)"
+ using additive_content_division[OF division_inter_1[OF d(1)]] uv xl(2) by auto
+ then show "(\<Sum>i\<in>d. content (l \<inter> i) * norm (f x)) = content l * norm (f x)"
+ unfolding sum_distrib_right[symmetric] using uv by auto
qed
show ?thesis
by (subst sum_Sigma_product[symmetric]) (auto intro!: sumeq sum.cong p' d')
@@ -2636,66 +2585,55 @@
and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> sum (\<lambda>k. norm (integral k f)) d \<le> B"
shows "f absolutely_integrable_on UNIV"
proof (rule absolutely_integrable_onI, fact)
- let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (\<Union>d)}"
+ let ?f = "\<lambda>D. \<Sum>k\<in>D. norm (integral k f)" and ?D = "{d. d division_of (\<Union>d)}"
+ define SDF where "SDF \<equiv> SUP d\<in>?D. ?f d"
have D_1: "?D \<noteq> {}"
by (rule elementary_interval) auto
have D_2: "bdd_above (?f`?D)"
- by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
- note D = D_1 D_2
- let ?S = "SUP d\<in>?D. ?f d"
- have "\<And>a b. f integrable_on cbox a b"
- using assms(1) integrable_on_subcbox by blast
- then have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
- apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
- using assms(2) apply blast
- done
- have "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
- apply (subst has_integral_alt')
- apply safe
- proof goal_cases
- case (1 a b)
- show ?case
- using f_int[of a b] unfolding absolutely_integrable_on_def by auto
- next
- case prems: (2 e)
- have "\<exists>y\<in>sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
+ using assms(2) by auto
+ have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
+ using assms integrable_on_subcbox
+ by (blast intro!: bounded_variation_absolutely_integrable_interval)
+ have "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
+ \<bar>integral (cbox a b) (\<lambda>x. norm (f x)) - SDF\<bar> < e"
+ if "0 < e" for e
+ proof -
+ have "\<exists>y \<in> ?f ` ?D. \<not> y \<le> SDF - e"
proof (rule ccontr)
assume "\<not> ?thesis"
- then have "?S \<le> ?S - e"
- by (intro cSUP_least[OF D(1)]) auto
+ then have "SDF \<le> SDF - e"
+ unfolding SDF_def
+ by (metis (mono_tags) D_1 cSUP_least image_eqI)
then show False
- using prems by auto
+ using that by auto
qed
- then obtain d K where ddiv: "d division_of \<Union>d" and "K = (\<Sum>k\<in>d. norm (integral k f))"
- "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e < K"
+ then obtain d K where ddiv: "d division_of \<Union>d" and "K = ?f d" "SDF - e < K"
by (auto simp add: image_iff not_le)
- then have d: "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e
- < (\<Sum>k\<in>d. norm (integral k f))"
+ then have d: "SDF - e < ?f d"
by auto
note d'=division_ofD[OF ddiv]
have "bounded (\<Union>d)"
- by (rule elementary_bounded,fact)
- from this[unfolded bounded_pos] obtain K where
- K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
- show ?case
+ using ddiv by blast
+ then obtain K where K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K"
+ using bounded_pos by blast
+ show ?thesis
proof (intro conjI impI allI exI)
fix a b :: 'n
assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
- have *: "\<And>s s1. \<lbrakk>?S - e < s1; s1 \<le> s; s < ?S + e\<rbrakk> \<Longrightarrow> \<bar>s - ?S\<bar> < e"
+ have *: "\<And>s s1. \<lbrakk>SDF - e < s1; s1 \<le> s; s < SDF + e\<rbrakk> \<Longrightarrow> \<bar>s - SDF\<bar> < e"
by arith
- show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
+ show "\<bar>integral (cbox a b) (\<lambda>x. norm (f x)) - SDF\<bar> < e"
unfolding real_norm_def
proof (rule * [OF d])
- have "(\<Sum>k\<in>d. norm (integral k f)) \<le> sum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
+ have "?f d \<le> sum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
proof (intro sum_mono)
fix k assume "k \<in> d"
with d'(4) f_int show "norm (integral k f) \<le> integral k (\<lambda>x. norm (f x))"
by (force simp: absolutely_integrable_on_def integral_norm_bound_integral)
qed
also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
- apply (rule integral_combine_division_bottomup[OF ddiv, symmetric])
- using absolutely_integrable_on_def d'(4) f_int by blast
- also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
+ by (metis (full_types) absolutely_integrable_on_def d'(4) ddiv f_int integral_combine_division_bottomup)
+ also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. norm (f x))"
proof -
have "\<Union>d \<subseteq> cbox a b"
using K(2) ab by fastforce
@@ -2703,8 +2641,7 @@
using integrable_on_subdivision[OF ddiv] f_int[of a b] unfolding absolutely_integrable_on_def
by (auto intro!: integral_subset_le)
qed
- finally show "(\<Sum>k\<in>d. norm (integral k f))
- \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)" .
+ finally show "?f d \<le> integral (cbox a b) (\<lambda>x. norm (f x))" .
next
have "e/2>0"
using \<open>e > 0\<close> by auto
@@ -2723,31 +2660,39 @@
p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
by (rule fine_division_exists [OF gauge_Int [OF \<open>gauge d1\<close> \<open>gauge d2\<close>], of a b])
(auto simp add: fine_Int)
- have *: "\<And>sf sf' si di. \<lbrakk>sf' = sf; si \<le> ?S; \<bar>sf - si\<bar> < e/2;
- \<bar>sf' - di\<bar> < e/2\<rbrakk> \<Longrightarrow> di < ?S + e"
+ have *: "\<And>sf sf' si di. \<lbrakk>sf' = sf; si \<le> SDF; \<bar>sf - si\<bar> < e/2;
+ \<bar>sf' - di\<bar> < e/2\<rbrakk> \<Longrightarrow> di < SDF + e"
by arith
- have "integral (cbox a b) (\<lambda>x. norm (f x)) < ?S + e"
+ have "integral (cbox a b) (\<lambda>x. norm (f x)) < SDF + e"
proof (rule *)
show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e/2"
unfolding split_def
- apply (rule absdiff_norm_less)
- using d2[of p] p(1,3) apply (auto simp: tagged_division_of_def split_def)
- done
+ proof (rule absdiff_norm_less)
+ show "(\<Sum>p\<in>p. norm (content (snd p) *\<^sub>R f (fst p) - integral (snd p) f)) < e/2"
+ using d2[of p] p(1,3) by (auto simp: tagged_division_of_def split_def)
+ qed
show "\<bar>(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e/2"
using d1[OF p(1,2)] by (simp only: real_norm_def)
show "(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) = (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x))"
by (auto simp: split_paired_all sum.cong [OF refl])
- show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> ?S"
+ have "(\<Sum>(x,k) \<in> p. norm (integral k f)) = (\<Sum>k\<in>snd ` p. norm (integral k f))"
+ apply (rule sum.over_tagged_division_lemma[OF p(1)])
+ by (metis Henstock_Kurzweil_Integration.integral_empty integral_open_interval norm_zero)
+ also have "... \<le> SDF"
using partial_division_of_tagged_division[of p "cbox a b"] p(1)
- apply (subst sum.over_tagged_division_lemma[OF p(1)])
- apply (auto simp: content_eq_0_interior tagged_partial_division_of_def intro!: cSUP_upper2 D)
- done
+ by (auto simp: SDF_def tagged_partial_division_of_def intro!: cSUP_upper2 D_1 D_2)
+ finally show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> SDF" .
qed
- then show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
+ then show "integral (cbox a b) (\<lambda>x. norm (f x)) < SDF + e"
by simp
qed
- qed (insert K, auto)
+ qed (use K in auto)
qed
+ moreover have "\<And>a b. (\<lambda>x. norm (f x)) integrable_on cbox a b"
+ using absolutely_integrable_on_def f_int by auto
+ ultimately
+ have "((\<lambda>x. norm (f x)) has_integral SDF) UNIV"
+ by (auto simp: has_integral_alt')
then show "(\<lambda>x. norm (f x)) integrable_on UNIV"
by blast
qed
@@ -2844,10 +2789,13 @@
have "?\<mu> (\<Union>\<F>) \<le> ?\<mu> S + e"
proof (rule *)
have "(\<Sum>K\<in>\<F>. ?\<mu> (K \<inter> S)) = ?\<mu> (\<Union>C\<in>\<F>. C \<inter> S)"
- apply (rule measure_negligible_finite_Union_image [OF \<open>finite \<F>\<close>, symmetric])
- using \<F>div \<open>S \<in> lmeasurable\<close> apply blast
- unfolding pairwise_def
- by (metis inf.commute inf_sup_aci(3) negligible_Int subsetCE negl_int \<open>\<F> \<subseteq> \<D>\<close>)
+ proof (rule measure_negligible_finite_Union_image [OF \<open>finite \<F>\<close>, symmetric])
+ show "\<And>K. K \<in> \<F> \<Longrightarrow> K \<inter> S \<in> lmeasurable"
+ using \<F>div \<open>S \<in> lmeasurable\<close> by blast
+ show "pairwise (\<lambda>K y. negligible (K \<inter> S \<inter> (y \<inter> S))) \<F>"
+ unfolding pairwise_def
+ by (metis inf.commute inf_sup_aci(3) negligible_Int subsetCE negl_int \<open>\<F> \<subseteq> \<D>\<close>)
+ qed
also have "\<dots> = ?\<mu> (\<Union>\<F> \<inter> S)"
by simp
also have "\<dots> \<le> ?\<mu> S"
@@ -3007,8 +2955,7 @@
by (metis True empty_imp_negligible image_Int image_empty interior_Int interior_injective_linear_image that(1))
qed
moreover have "g ` K \<inter> g ` L \<subseteq> frontier (g ` K \<inter> g ` L) \<union> interior (g ` K \<inter> g ` L)"
- apply (auto simp: frontier_def)
- using closure_subset contra_subsetD by fastforce+
+ by (metis Diff_partition Int_commute calculation closure_Un_frontier frontier_def inf.absorb_iff2 inf_bot_right inf_sup_absorb negligible_Un_eq open_interior open_not_negligible sup_commute)
ultimately show ?thesis
by (rule negligible_subset)
next
@@ -3090,8 +3037,6 @@
and DD: "cbox a b - S \<subseteq> \<Union>\<D>" "\<Union>\<D> \<in> lmeasurable"
and le: "?\<mu> (\<Union>\<D>) \<le> ?\<mu> (cbox a b - S) + e/(1 + \<bar>m\<bar>)"
by (rule measurable_outer_intervals_bounded [of "cbox a b - S" a b "e/(1 + \<bar>m\<bar>)"]; use 1 2 pairwise_def in force)
- have meq: "?\<mu> (cbox a b - S) = ?\<mu> (cbox a b) - ?\<mu> S"
- by (simp add: measurable_measure_Diff \<open>S \<subseteq> cbox a b\<close> fmeasurableD that(2))
show "\<exists>T \<in> lmeasurable. T \<subseteq> f ` S \<and> m * ?\<mu> S - e \<le> ?\<mu> T"
proof (intro bexI conjI)
show "f ` (cbox a b) - f ` (\<Union>\<D>) \<subseteq> f ` S"
@@ -3099,16 +3044,24 @@
have "m * ?\<mu> S - e \<le> m * (?\<mu> S - e / (1 + \<bar>m\<bar>))"
using \<open>m \<ge> 0\<close> \<open>e > 0\<close> by (simp add: field_simps)
also have "\<dots> \<le> ?\<mu> (f ` cbox a b) - ?\<mu> (f ` (\<Union>\<D>))"
- using le \<open>m \<ge> 0\<close> \<open>e > 0\<close>
- apply (simp add: im fUD [OF \<open>countable \<D>\<close> cbox intdisj] right_diff_distrib [symmetric])
- apply (rule mult_left_mono; simp add: algebra_simps meq)
- done
+ proof -
+ have "?\<mu> (cbox a b - S) = ?\<mu> (cbox a b) - ?\<mu> S"
+ by (simp add: measurable_measure_Diff \<open>S \<subseteq> cbox a b\<close> fmeasurableD that(2))
+ then have "(?\<mu> S - e / (1 + m)) \<le> (content (cbox a b) - ?\<mu> (\<Union> \<D>))"
+ using \<open>m \<ge> 0\<close> le by auto
+ then show ?thesis
+ using \<open>m \<ge> 0\<close> \<open>e > 0\<close>
+ by (simp add: mult_left_mono im fUD [OF \<open>countable \<D>\<close> cbox intdisj] flip: right_diff_distrib)
+ qed
also have "\<dots> = ?\<mu> (f ` cbox a b - f ` \<Union>\<D>)"
- apply (rule measurable_measure_Diff [symmetric])
- apply (simp add: assms(1) measurable_linear_image_interval)
- apply (simp add: \<open>countable \<D>\<close> cbox fUD fmeasurableD intdisj)
- apply (simp add: Sup_le_iff cbox image_mono)
- done
+ proof (rule measurable_measure_Diff [symmetric])
+ show "f ` cbox a b \<in> lmeasurable"
+ by (simp add: assms(1) measurable_linear_image_interval)
+ show "f ` \<Union> \<D> \<in> sets lebesgue"
+ by (simp add: \<open>countable \<D>\<close> cbox fUD fmeasurableD intdisj)
+ show "f ` \<Union> \<D> \<subseteq> f ` cbox a b"
+ by (simp add: Sup_le_iff cbox image_mono)
+ qed
finally show "m * ?\<mu> S - e \<le> ?\<mu> (f ` cbox a b - f ` \<Union>\<D>)" .
show "f ` cbox a b - f ` \<Union>\<D> \<in> lmeasurable"
by (simp add: fUD \<open>countable \<D>\<close> \<open>linear f\<close> cbox fmeasurable.Diff intdisj measurable_linear_image_interval)
@@ -3166,7 +3119,7 @@
moreover have fim: "f ` (S \<inter> h ` (cbox a b)) = (f ` S) \<inter> cbox a b"
by (auto simp: hf rev_image_eqI fh)
ultimately have 1: "(f ` S) \<inter> cbox a b \<in> lmeasurable"
- and 2: "m * ?\<mu> (S \<inter> h ` cbox a b) = ?\<mu> ((f ` S) \<inter> cbox a b)"
+ and 2: "?\<mu> ((f ` S) \<inter> cbox a b) = m * ?\<mu> (S \<inter> h ` cbox a b)"
using fBS [of "S \<inter> (h ` (cbox a b))"] by auto
have *: "\<lbrakk>\<bar>z - m\<bar> < e; z \<le> w; w \<le> m\<rbrakk> \<Longrightarrow> \<bar>w - m\<bar> \<le> e"
for w z m and e::real by auto
@@ -3192,20 +3145,12 @@
show "?\<mu> (S \<inter> h ` cbox a b) \<le> ?\<mu> S"
by (simp add: S Shab fmeasurableD measure_mono_fmeasurable)
qed
- have "\<bar>?\<mu> (f ` S \<inter> cbox a b) - m * ?\<mu> S\<bar> \<le> m * e / (1 + \<bar>m\<bar>)"
- proof -
- have mm: "\<bar>m\<bar> = m"
- by (simp add: \<open>0 \<le> m\<close>)
- then have "\<bar>?\<mu> S - ?\<mu> (S \<inter> h ` cbox a b)\<bar> * m \<le> e / (1 + m) * m"
- by (metis (no_types) \<open>0 \<le> m\<close> meas_adiff abs_minus_commute mult_right_mono)
- moreover have "\<forall>r. \<bar>r * m\<bar> = m * \<bar>r\<bar>"
- by (metis \<open>0 \<le> m\<close> abs_mult_pos mult.commute)
- ultimately show ?thesis
- apply (simp add: 2 [symmetric])
- by (metis (no_types) abs_minus_commute mult.commute right_diff_distrib' mm)
- qed
+ have "\<bar>?\<mu> (f ` S \<inter> cbox a b) - m * ?\<mu> S\<bar> \<le> \<bar>?\<mu> S - ?\<mu> (S \<inter> h ` cbox a b)\<bar> * m"
+ by (metis "2" \<open>m \<ge> 0\<close> abs_minus_commute abs_mult_pos mult.commute order_refl right_diff_distrib')
+ also have "\<dots> \<le> e / (1 + m) * m"
+ by (metis \<open>m \<ge> 0\<close> abs_minus_commute abs_of_nonneg meas_adiff mult.commute mult_left_mono)
also have "\<dots> < e"
- using \<open>e > 0\<close> by (cases "m \<ge> 0") (simp_all add: field_simps)
+ using \<open>e > 0\<close> \<open>m \<ge> 0\<close> by (simp add: field_simps)
finally have "\<bar>?\<mu> (f ` S \<inter> cbox a b) - m * ?\<mu> S\<bar> < e" .
with 1 show ?thesis by auto
qed
@@ -3293,23 +3238,21 @@
proposition absolutely_integrable_componentwise_iff:
shows "f absolutely_integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. f x \<bullet> b) absolutely_integrable_on A)"
proof -
- have *: "(\<lambda>x. norm (f x)) integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. norm (f x \<bullet> b)) integrable_on A)"
- if "f integrable_on A"
- proof -
- have 1: "\<And>i. \<lbrakk>(\<lambda>x. norm (f x)) integrable_on A; i \<in> Basis\<rbrakk>
- \<Longrightarrow> (\<lambda>x. f x \<bullet> i) absolutely_integrable_on A"
- apply (rule absolutely_integrable_integrable_bound [where g = "\<lambda>x. norm(f x)"])
- using Basis_le_norm integrable_component that apply fastforce+
- done
- have 2: "\<forall>i\<in>Basis. (\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on A \<Longrightarrow> f absolutely_integrable_on A"
- apply (rule absolutely_integrable_integrable_bound [where g = "\<lambda>x. \<Sum>i\<in>Basis. norm (f x \<bullet> i)"])
- using norm_le_l1 that apply (force intro: integrable_sum)+
- done
- show ?thesis
- apply auto
- apply (metis (full_types) absolutely_integrable_on_def set_integrable_abs 1)
- apply (metis (full_types) absolutely_integrable_on_def 2)
- done
+ have *: "(\<lambda>x. norm (f x)) integrable_on A \<longleftrightarrow> (\<forall>b\<in>Basis. (\<lambda>x. norm (f x \<bullet> b)) integrable_on A)" (is "?lhs = ?rhs")
+ if "f integrable_on A"
+ proof
+ assume ?lhs
+ then show ?rhs
+ by (metis absolutely_integrable_on_def Topology_Euclidean_Space.norm_nth_le absolutely_integrable_integrable_bound integrable_component that)
+ next
+ assume R: ?rhs
+ have "f absolutely_integrable_on A"
+ proof (rule absolutely_integrable_integrable_bound)
+ show "(\<lambda>x. \<Sum>i\<in>Basis. norm (f x \<bullet> i)) integrable_on A"
+ using R by (force intro: integrable_sum)
+ qed (use that norm_le_l1 in auto)
+ then show ?lhs
+ using absolutely_integrable_on_def by auto
qed
show ?thesis
unfolding absolutely_integrable_on_def
@@ -3331,8 +3274,7 @@
shows "(\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on S"
proof -
have "(\<lambda>x. c *\<^sub>R x) o f absolutely_integrable_on S"
- apply (rule absolutely_integrable_linear [OF assms])
- by (simp add: bounded_linear_scaleR_right)
+ by (simp add: absolutely_integrable_linear assms bounded_linear_scaleR_right)
then show ?thesis
using assms by blast
qed
@@ -3354,10 +3296,6 @@
shows "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) absolutely_integrable_on S"
(is "?g absolutely_integrable_on S")
proof -
- have eq: "?g =
- (\<lambda>x. \<Sum>i\<in>Basis. ((\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
- (\<lambda>x. norm(\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f) x)"
- by (simp)
have *: "(\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
(\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
absolutely_integrable_on S"
@@ -3367,19 +3305,20 @@
by (simp add: linear_linear algebra_simps linearI)
moreover have "(\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
absolutely_integrable_on S"
+ using assms \<open>i \<in> Basis\<close>
unfolding o_def
- apply (rule absolutely_integrable_norm [unfolded o_def])
- using assms \<open>i \<in> Basis\<close>
- apply (auto simp: algebra_simps dest: absolutely_integrable_component[where b=i])
- done
+ by (intro absolutely_integrable_norm [unfolded o_def])
+ (auto simp: algebra_simps dest: absolutely_integrable_component)
ultimately show ?thesis
by (subst comp_assoc) (blast intro: absolutely_integrable_linear)
qed
+ have eq: "?g =
+ (\<lambda>x. \<Sum>i\<in>Basis. ((\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
+ (\<lambda>x. norm(\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f) x)"
+ by (simp)
show ?thesis
- apply (rule ssubst [OF eq])
- apply (rule absolutely_integrable_sum)
- apply (force simp: intro!: *)+
- done
+ unfolding eq
+ by (rule absolutely_integrable_sum) (force simp: intro!: *)+
qed
lemma abs_absolutely_integrableI_1:
@@ -3447,10 +3386,8 @@
qed
moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
absolutely_integrable_on S"
- apply (intro set_integral_add absolutely_integrable_scaleR_left assms)
using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
- apply (simp add: algebra_simps)
- done
+ by (intro set_integral_add absolutely_integrable_scaleR_left assms) (simp add: algebra_simps)
ultimately show ?thesis by metis
qed
@@ -3482,10 +3419,9 @@
qed
moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
absolutely_integrable_on S"
- apply (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms)
using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
- apply (simp add: algebra_simps)
- done
+ by (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms)
+ (simp add: algebra_simps)
ultimately show ?thesis by metis
qed
@@ -3522,9 +3458,10 @@
shows "f absolutely_integrable_on A"
proof -
have "(\<lambda>x. g x - (g x - f x)) absolutely_integrable_on A"
- apply (rule set_integral_diff [OF g nonnegative_absolutely_integrable])
- using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
- by (simp add: comp inner_diff_left)
+ proof (rule set_integral_diff [OF g nonnegative_absolutely_integrable])
+ show "(\<lambda>x. g x - f x) integrable_on A"
+ using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g by blast
+ qed (simp add: comp inner_diff_left)
then show ?thesis
by simp
qed
@@ -3536,9 +3473,10 @@
shows "g absolutely_integrable_on A"
proof -
have "(\<lambda>x. f x + (g x - f x)) absolutely_integrable_on A"
- apply (rule set_integral_add [OF f nonnegative_absolutely_integrable])
- using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
- by (simp add: comp inner_diff_left)
+ proof (rule set_integral_add [OF f nonnegative_absolutely_integrable])
+ show "(\<lambda>x. g x - f x) integrable_on A"
+ using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g by blast
+ qed (simp add: comp inner_diff_left)
then show ?thesis
by simp
qed
@@ -3613,9 +3551,10 @@
apply (subst has_integral_alt)
apply (subst (asm) has_integral_alt)
apply (simp add: has_integral_vec1_I_cbox split: if_split_asm)
- apply (metis vector_one_nth)
- apply (erule all_forward imp_forward asm_rl ex_forward conj_forward)+
- apply (blast intro!: *)
+ subgoal by (metis vector_one_nth)
+ subgoal
+ apply (erule all_forward imp_forward ex_forward asm_rl)+
+ by (blast intro!: *)+
done
qed
@@ -3653,10 +3592,12 @@
and B: "ball 0 B \<subseteq> cbox a b" for e B and a b::"real^1"
proof -
have B': "ball 0 B \<subseteq> {a$1..b$1}"
- using B
- apply (simp add: subset_iff Basis_vec_def cart_eq_inner_axis [symmetric] mem_box)
- apply (metis (full_types) norm_real vec_component)
- done
+ proof (clarsimp)
+ fix t
+ assume "\<bar>t\<bar> < B" then show "a $ 1 \<le> t \<and> t \<le> b $ 1"
+ using subsetD [OF B]
+ by (metis (mono_tags, hide_lams) mem_ball_0 mem_box_cart(2) norm_real vec_component)
+ qed
have eq: "(\<lambda>x. if vec x \<in> S then f (vec x) else 0) = (\<lambda>x. if x \<in> S then f x else 0) \<circ> vec"
by force
have [simp]: "(\<exists>y\<in>S. x = y $ 1) \<longleftrightarrow> vec x \<in> S" for x
@@ -3670,11 +3611,10 @@
apply (subst (asm) has_integral_alt)
apply (simp add: has_integral_vec1_D_cbox eq_cbox split: if_split_asm, blast)
apply (intro conjI impI)
- apply (metis vector_one_nth)
+ subgoal by (metis vector_one_nth)
apply (erule thin_rl)
- apply (erule all_forward imp_forward asm_rl ex_forward conj_forward)+
- using * apply blast
- done
+ apply (erule all_forward ex_forward conj_forward)+
+ by (blast intro!: *)+
qed
@@ -3988,11 +3928,8 @@
by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
also have "\<dots> = T - F a"
proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
- have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
- apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
- apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
- apply (rule filterlim_real_sequentially)
- done
+ have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
+ by (auto intro: filterlim_compose[OF lim filterlim_tendsto_add_at_top] filterlim_real_sequentially)
then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)"
by (simp add: F_mono F_le_T tendsto_diff)
qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
@@ -4028,17 +3965,22 @@
shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
= F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
proof-
- have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
- by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
- (auto intro!: DERIV_isCont)
-
- have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
- (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
- apply (subst Bochner_Integration.integral_add[symmetric])
- apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
- by (auto intro!: DERIV_isCont Bochner_Integration.integral_cong split: split_indicator)
-
- thus ?thesis using 0 by auto
+ have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel)
+ = LBINT x. F x * g x * indicat_real {a..b} x + f x * G x * indicat_real {a..b} x"
+ by (meson vector_space_over_itself.scale_left_distrib)
+ also have "... = (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
+ proof (intro Bochner_Integration.integral_add borel_integrable_atLeastAtMost cont_f cont_g continuous_intros)
+ show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont F x" "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont G x"
+ using DERIV_isCont by blast+
+ qed
+ finally have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
+ (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel" .
+ moreover have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
+ proof (intro integral_FTC_Icc_real derivative_eq_intros cont_f cont_g continuous_intros)
+ show "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont F x" "\<And>x. \<lbrakk>a \<le> x; x \<le> b\<rbrakk> \<Longrightarrow> isCont G x"
+ using DERIV_isCont by blast+
+ qed auto
+ ultimately show ?thesis by auto
qed
lemma integral_by_parts':
@@ -4737,10 +4679,8 @@
fixes f :: "'a::euclidean_space \<Rightarrow> real"
assumes "S \<in> sets lebesgue"
shows "f absolutely_integrable_on S \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S) \<and> (\<lambda>x. \<bar>f x\<bar>) integrable_on S"
- using assms
- apply (auto simp: absolutely_integrable_measurable integrable_on_lebesgue_on)
- apply (simp add: integrable_on_lebesgue_on measurable_bounded_by_integrable_imp_lebesgue_integrable)
- using abs_absolutely_integrableI_1 absolutely_integrable_measurable measurable_bounded_by_integrable_imp_integrable_real by blast
+ by (metis abs_absolutely_integrableI_1 absolutely_integrable_measurable_real assms
+ measurable_bounded_by_integrable_imp_integrable order_refl real_norm_def set_integrable_abs set_lebesgue_integral_eq_integral(1))
lemma absolutely_integrable_imp_borel_measurable:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -4782,8 +4722,8 @@
have "\<exists>T' B. open T' \<and> f x \<in> T' \<and>
(\<forall>y\<in>f ` V \<inter> T \<inter> T'. norm (g y - g (f x)) \<le> B * norm (y - f x))"
if "f x \<in> T" "x \<in> V" for x
- apply (rule_tac x = "ball (f x) 1" in exI)
- using that noxy by (force simp: g)
+ using that noxy
+ by (rule_tac x = "ball (f x) 1" in exI) (force simp: g)
then have "negligible (g ` (f ` V \<inter> T))"
by (force simp: \<open>negligible T\<close> negligible_Int intro!: negligible_locally_Lipschitz_image)
moreover have "V \<subseteq> g ` (f ` V \<inter> T)"
@@ -4826,12 +4766,12 @@
using less by linarith
with \<delta> \<open>y \<in> S\<close> have le: "norm (f y - f x - f' x (y - x)) \<le> B * norm (y - x) - norm (y - x)/i"
by (auto simp: algebra_simps)
- have *: "\<lbrakk>norm(f - f' - y) \<le> b - c; b \<le> norm y; d \<le> c\<rbrakk> \<Longrightarrow> d \<le> norm(f - f')"
- for b c d and y f f'::'a
- using norm_triangle_ineq3 [of "f - f'" y] by simp
- show ?thesis
- apply (rule * [OF le B])
+ have "norm (y - x) / real (max i j) \<le> norm (y - x) / real i"
using \<open>i \<noteq> 0\<close> \<open>j \<noteq> 0\<close> by (simp add: field_split_simps max_mult_distrib_left of_nat_max less_max_iff_disj)
+ also have "... \<le> norm (f y - f x)"
+ using B [of "y-x"] le norm_triangle_ineq3 [of "f y - f x" "f' x (y - x)"]
+ by linarith
+ finally show ?thesis .
qed
with \<open>x \<in> S\<close> \<open>i \<noteq> 0\<close> \<open>j \<noteq> 0\<close> show "\<exists>n\<in>{0<..}. x \<in> U n"
by (rule_tac x="max i j" in bexI) (auto simp: field_simps U_def less_max_iff_disj)
@@ -5069,11 +5009,11 @@
qed
finally show ?thesis .
qed
- then show "\<exists>d>0. \<forall>y\<in>f ` S.
+ with \<open>k > 0\<close> \<open>B > 0\<close> \<open>d > 0\<close> \<open>a \<in> S\<close>
+ show "\<exists>d>0. \<forall>y\<in>f ` S.
norm (y - f a) < d \<longrightarrow>
norm (g y - g (f a) - g' (y - f a)) \<le> e * norm (y - f a)"
- apply (rule_tac x="min k (d / B)" in exI)
- using \<open>k > 0\<close> \<open>B > 0\<close> \<open>d > 0\<close> \<open>a \<in> S\<close> by (auto simp: gf)
+ by (rule_tac x="min k (d / B)" in exI) (auto simp: gf)
qed
qed