--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Aug 23 20:41:15 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Aug 23 22:05:53 2017 +0200
@@ -188,15 +188,23 @@
finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
qed
-lemma operative_content[intro]: "add.operative content"
- by (force simp add: add.operative_def content_split[symmetric] content_eq_0_interior)
+global_interpretation sum_content: operative plus 0 content
+ rewrites "comm_monoid_set.F plus 0 = sum"
+proof -
+ interpret operative plus 0 content
+ by standard (auto simp add: content_split [symmetric] content_eq_0_interior)
+ show "operative plus 0 content"
+ by standard
+ show "comm_monoid_set.F plus 0 = sum"
+ by (simp add: sum_def)
+qed
lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> sum content d = content (cbox a b)"
- by (metis operative_content sum.operative_division)
+ by (fact sum_content.division)
lemma additive_content_tagged_division:
"d tagged_division_of (cbox a b) \<Longrightarrow> sum (\<lambda>(x,l). content l) d = content (cbox a b)"
- unfolding sum.operative_tagged_division[OF operative_content, symmetric] by blast
+ by (fact sum_content.tagged_division)
lemma subadditive_content_division:
assumes "\<D> division_of S" "S \<subseteq> cbox a b"
@@ -1405,16 +1413,16 @@
by (simp add: interval_split[OF k] integrable_Cauchy)
qed
-lemma operative_integral:
+lemma operative_integralI:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
- shows "comm_monoid.operative (lift_option op +) (Some 0)
+ shows "operative (lift_option op +) (Some 0)
(\<lambda>i. if f integrable_on i then Some (integral i f) else None)"
proof -
interpret comm_monoid "lift_option plus" "Some (0::'b)"
by (rule comm_monoid_lift_option)
(rule add.comm_monoid_axioms)
show ?thesis
- proof (unfold operative_def, safe)
+ proof
fix a b c
fix k :: 'a
assume k: "k \<in> Basis"
@@ -2458,45 +2466,49 @@
subsection \<open>Integrability of continuous functions.\<close>
-lemma operative_approximable:
+lemma operative_approximableI:
fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
assumes "0 \<le> e"
- shows "comm_monoid.operative op \<and> True (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)"
- unfolding comm_monoid.operative_def[OF comm_monoid_and]
-proof safe
- fix a b :: 'b
- show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
- if "box a b = {}" for a b
- apply (rule_tac x=f in exI)
- using assms that by (auto simp: content_eq_0_interior)
- {
- fix c g and k :: 'b
- assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b"
- assume k: "k \<in> Basis"
- show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
- "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
- apply (rule_tac[!] x=g in exI)
- using fg integrable_split[OF g k] by auto
- }
- show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
- if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e"
- and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
- and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e"
- and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
- and k: "k \<in> Basis"
- for c k g1 g2
- proof -
- let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
+ shows "operative conj True (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)"
+proof -
+ interpret comm_monoid conj True
+ by standard auto
+ show ?thesis
+ proof (standard, safe)
+ fix a b :: 'b
show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
- proof (intro exI conjI ballI)
- show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x
- by (auto simp: that assms fg1 fg2)
- show "?g integrable_on cbox a b"
- proof -
- have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
- by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
- with has_integral_split[OF _ _ k] show ?thesis
- unfolding integrable_on_def by blast
+ if "box a b = {}" for a b
+ apply (rule_tac x=f in exI)
+ using assms that by (auto simp: content_eq_0_interior)
+ {
+ fix c g and k :: 'b
+ assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b"
+ assume k: "k \<in> Basis"
+ show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
+ "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
+ apply (rule_tac[!] x=g in exI)
+ using fg integrable_split[OF g k] by auto
+ }
+ show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+ if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e"
+ and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
+ and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e"
+ and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
+ and k: "k \<in> Basis"
+ for c k g1 g2
+ proof -
+ let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
+ show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+ proof (intro exI conjI ballI)
+ show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x
+ by (auto simp: that assms fg1 fg2)
+ show "?g integrable_on cbox a b"
+ proof -
+ have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
+ by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
+ with has_integral_split[OF _ _ k] show ?thesis
+ unfolding integrable_on_def by blast
+ qed
qed
qed
qed
@@ -2517,11 +2529,9 @@
and f: "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
obtains g where "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" "g integrable_on cbox a b"
proof -
- note * = comm_monoid_set.operative_division
- [OF comm_monoid_set_and operative_approximable[OF \<open>0 \<le> e\<close>] d]
- have "finite d"
- by (rule division_of_finite[OF d])
- with f *[unfolded comm_monoid_set_F_and, of f] that show thesis
+ interpret operative conj True "\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i"
+ using \<open>0 \<le> e\<close> by (rule operative_approximableI)
+ from f local.division [OF d] that show thesis
by auto
qed
@@ -3000,31 +3010,43 @@
subsection \<open>Integrability on subintervals.\<close>
-lemma operative_integrable:
+lemma operative_integrableI:
fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
- shows "comm_monoid.operative op \<and> True (\<lambda>i. f integrable_on i)"
- unfolding comm_monoid.operative_def[OF comm_monoid_and]
- apply safe
- apply (subst integrable_on_def)
- apply rule
- apply (rule has_integral_null_eq[where i=0, THEN iffD2])
- apply (simp add: content_eq_0_interior)
- apply rule
- apply (rule, assumption, assumption)+
- unfolding integrable_on_def
- by (auto intro!: has_integral_split)
+ assumes "0 \<le> e"
+ shows "operative conj True (\<lambda>i. f integrable_on i)"
+proof -
+ interpret comm_monoid conj True
+ by standard auto
+ show ?thesis
+ apply standard
+ apply safe
+ apply (subst integrable_on_def)
+ apply rule
+ apply (rule has_integral_null_eq[where i=0, THEN iffD2])
+ apply (simp add: content_eq_0_interior)
+ apply rule
+ apply (rule, assumption, assumption)+
+ unfolding integrable_on_def
+ apply (auto intro!: has_integral_split)
+ done
+qed
lemma integrable_subinterval:
fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
assumes "f integrable_on cbox a b"
and "cbox c d \<subseteq> cbox a b"
shows "f integrable_on cbox c d"
- apply (cases "cbox c d = {}")
- defer
- apply (rule partial_division_extend_1[OF assms(2)],assumption)
- using comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable,symmetric,of _ _ _ f] assms(1)
- apply (auto simp: comm_monoid_set_F_and)
- done
+proof -
+ interpret operative conj True "\<lambda>i. f integrable_on i"
+ using order_refl by (rule operative_integrableI)
+ show ?thesis
+ apply (cases "cbox c d = {}")
+ defer
+ apply (rule partial_division_extend_1[OF assms(2)],assumption)
+ using division [symmetric] assms(1)
+ apply (auto simp: comm_monoid_set_F_and)
+ done
+qed
lemma integrable_subinterval_real:
fixes f :: "real \<Rightarrow> 'a::banach"
@@ -3044,10 +3066,10 @@
and cb: "(f has_integral j) {c..b}"
shows "(f has_integral (i + j)) {a..b}"
proof -
- interpret comm_monoid "lift_option plus" "Some (0::'a)"
- by (rule comm_monoid_lift_option)
- (rule add.comm_monoid_axioms)
- from operative_integral [of f, unfolded operative_1_le] \<open>a \<le> c\<close> \<open>c \<le> b\<close>
+ interpret operative_real "lift_option plus" "Some 0"
+ "\<lambda>i. if f integrable_on i then Some (integral i f) else None"
+ using operative_integralI by (rule operative_realI)
+ from \<open>a \<le> c\<close> \<open>c \<le> b\<close> ac cb coalesce_less_eq
have *: "lift_option op +
(if f integrable_on {a..c} then Some (integral {a..c} f) else None)
(if f integrable_on {c..b} then Some (integral {c..b} f) else None) =
@@ -3098,6 +3120,8 @@
f integrable_on cbox u v"
shows "f integrable_on cbox a b"
proof -
+ interpret operative conj True "\<lambda>i. f integrable_on i"
+ using order_refl by (rule operative_integrableI)
have "\<forall>x. \<exists>d>0. x\<in>cbox a b \<longrightarrow> (\<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow>
f integrable_on cbox u v)"
using assms by (metis zero_less_one)
@@ -3112,8 +3136,7 @@
have "f integrable_on k" if "(x, k) \<in> p" for x k
using tagged_division_ofD(2-4)[OF p(1) that] fineD[OF p(2) that] d[of x] by auto
then show ?thesis
- unfolding comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable sndp, symmetric]
- comm_monoid_set_F_and
+ unfolding division [symmetric, OF sndp] comm_monoid_set_F_and
by auto
qed
@@ -4486,13 +4509,11 @@
}
assume "cbox c d \<noteq> {}"
from partial_division_extend_1 [OF assms(2) this] guess p . note p=this
- interpret comm_monoid_set "lift_option plus" "Some (0 :: 'b)"
- apply (rule comm_monoid_set.intro)
- apply (rule comm_monoid_lift_option)
- apply (rule add.comm_monoid_axioms)
- done
- note operat = operative_division
- [OF operative_integral p(1), symmetric]
+ interpret operative "lift_option plus" "Some (0 :: 'b)"
+ "\<lambda>i. if g integrable_on i then Some (integral i g) else None"
+ by (fact operative_integralI)
+ note operat = division
+ [OF p(1), symmetric]
let ?P = "(if g integrable_on cbox a b then Some (integral (cbox a b) g) else None) = Some i"
{
presume "?P"
@@ -7012,16 +7033,16 @@
apply (auto simp: has_integral_integral [symmetric])
done
-lemma integral_swap_operative:
+lemma integral_swap_operativeI:
fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
assumes f: "continuous_on s f" and e: "0 < e"
- shows "comm_monoid.operative (op \<and>) True
+ shows "operative conj True
(\<lambda>k. \<forall>a b c d.
cbox (a,c) (b,d) \<subseteq> k \<and> cbox (a,c) (b,d) \<subseteq> s
\<longrightarrow> norm(integral (cbox (a,c) (b,d)) f -
integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f((x,y)))))
\<le> e * content (cbox (a,c) (b,d)))"
-proof (auto simp: comm_monoid.operative_def[OF comm_monoid_and])
+proof (standard, auto)
fix a::'a and c::'b and b::'a and d::'b and u::'a and v::'a and w::'b and z::'b
assume *: "box (a, c) (b, d) = {}"
and cb1: "cbox (u, w) (v, z) \<subseteq> cbox (a, c) (b, d)"
@@ -7115,8 +7136,8 @@
lemma integral_prod_continuous:
fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
- assumes "continuous_on (cbox (a,c) (b,d)) f" (is "continuous_on ?CBOX f")
- shows "integral (cbox (a,c) (b,d)) f = integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f(x,y)))"
+ assumes "continuous_on (cbox (a, c) (b, d)) f" (is "continuous_on ?CBOX f")
+ shows "integral (cbox (a, c) (b, d)) f = integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y)))"
proof (cases "content ?CBOX = 0")
case True
then show ?thesis
@@ -7127,22 +7148,41 @@
using content_lt_nz by blast
have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) = 0"
proof (rule dense_eq0_I, simp)
- fix e::real assume "0 < e"
- with cbp have e': "0 < e/content ?CBOX"
+ fix e :: real
+ assume "0 < e"
+ with \<open>content ?CBOX > 0\<close> have "0 < e / content ?CBOX"
by simp
- have f_int_acbd: "f integrable_on cbox (a,c) (b,d)"
+ have f_int_acbd: "f integrable_on ?CBOX"
by (rule integrable_continuous [OF assms])
{ fix p
- assume p: "p division_of cbox (a,c) (b,d)"
- note opd1 = comm_monoid_set.operative_division [OF comm_monoid_set_and integral_swap_operative [OF assms e'], THEN iffD1,
- THEN spec, THEN spec, THEN spec, THEN spec, of p "(a,c)" "(b,d)" a c b d]
- have "(\<And>t u v w z.
- \<lbrakk>t \<in> p; cbox (u,w) (v,z) \<subseteq> t; cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)\<rbrakk> \<Longrightarrow>
- norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))))
- \<le> e * content (cbox (u,w) (v,z)) / content?CBOX)
- \<Longrightarrow>
- norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
- using opd1 [OF p] False by (simp add: comm_monoid_set_F_and)
+ assume p: "p division_of ?CBOX"
+ then have "finite p"
+ by blast
+ define e' where "e' = e / content ?CBOX"
+ with \<open>0 < e\<close> \<open>0 < e / content ?CBOX\<close>
+ have "0 < e'"
+ by simp
+ interpret operative conj True
+ "\<lambda>k. \<forall>a' b' c' d'.
+ cbox (a', c') (b', d') \<subseteq> k \<and> cbox (a', c') (b', d') \<subseteq> ?CBOX
+ \<longrightarrow> norm (integral (cbox (a', c') (b', d')) f -
+ integral (cbox a' b') (\<lambda>x. integral (cbox c' d') (\<lambda>y. f ((x, y)))))
+ \<le> e' * content (cbox (a', c') (b', d'))"
+ using assms \<open>0 < e'\<close> by (rule integral_swap_operativeI)
+ have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y))))
+ \<le> e' * content ?CBOX"
+ if "\<And>t u v w z. t \<in> p \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> t \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> ?CBOX
+ \<Longrightarrow> norm (integral (cbox (u, w) (v, z)) f -
+ integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))))
+ \<le> e' * content (cbox (u, w) (v, z))"
+ using that division [of p "(a, c)" "(b, d)"] p \<open>finite p\<close> by (auto simp add: comm_monoid_set_F_and)
+ with False have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y))))
+ \<le> e"
+ if "\<And>t u v w z. t \<in> p \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> t \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> ?CBOX
+ \<Longrightarrow> norm (integral (cbox (u, w) (v, z)) f -
+ integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))))
+ \<le> e * content (cbox (u, w) (v, z)) / content ?CBOX"
+ using that by (simp add: e'_def)
} note op_acbd = this
{ fix k::real and p and u::'a and v w and z::'b and t1 t2 l
assume k: "0 < k"
@@ -7177,7 +7217,7 @@
\<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
- using cbp e' nf'
+ using cbp \<open>0 < e / content ?CBOX\<close> nf'
apply (auto simp: integrable_diff f_int_uwvz integrable_const)
done
have int_integrable: "(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) integrable_on cbox u v"
@@ -7188,14 +7228,14 @@
\<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2"
apply (simp only: integral_diff [symmetric] f_int_uv integrable_const)
apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
- using cbp e' nf'
+ using cbp \<open>0 < e / content ?CBOX\<close> nf'
apply (auto simp: integrable_diff f_int_uv integrable_const)
done
have "norm (integral (cbox u v)
(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
\<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)"
apply (rule integrable_bound [OF _ _ normint_wz])
- using cbp e'
+ using cbp \<open>0 < e / content ?CBOX\<close>
apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const)
done
also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
--- a/src/HOL/Analysis/Tagged_Division.thy Wed Aug 23 20:41:15 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy Wed Aug 23 22:05:53 2017 +0200
@@ -10,6 +10,8 @@
Topology_Euclidean_Space
begin
+term comm_monoid
+
lemma sum_Sigma_product:
assumes "finite S"
and "\<And>i. i \<in> S \<Longrightarrow> finite (T i)"
@@ -571,7 +573,7 @@
"g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
using f g by (auto simp: PiE_iff)
with * ord[of i] show "interior l \<inter> interior k = {}"
- by (auto simp add: l k interior_cbox disjoint_interval intro!: bexI[of _ i])
+ by (auto simp add: l k disjoint_interval intro!: bexI[of _ i])
}
note \<open>k \<subseteq> cbox a b\<close>
}
@@ -1198,6 +1200,91 @@
apply auto
done
+lemma tagged_division_union_interval:
+ fixes a :: "'a::euclidean_space"
+ assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
+ and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+ and k: "k \<in> Basis"
+ shows "(p1 \<union> p2) tagged_division_of (cbox a b)"
+proof -
+ have *: "cbox a b = (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<union> (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+ by auto
+ show ?thesis
+ apply (subst *)
+ apply (rule tagged_division_union[OF assms(1-2)])
+ unfolding interval_split[OF k] interior_cbox
+ using k
+ apply (auto simp add: box_def elim!: ballE[where x=k])
+ done
+qed
+
+lemma tagged_division_union_interval_real:
+ fixes a :: real
+ assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
+ and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
+ and k: "k \<in> Basis"
+ shows "(p1 \<union> p2) tagged_division_of {a .. b}"
+ using assms
+ unfolding box_real[symmetric]
+ by (rule tagged_division_union_interval)
+
+lemma tagged_division_split_left_inj:
+ assumes d: "d tagged_division_of i"
+ and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
+ and "K1 \<noteq> K2"
+ and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
+ shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
+proof -
+ have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
+ using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
+ then show ?thesis
+ using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+qed
+
+lemma tagged_division_split_right_inj:
+ assumes d: "d tagged_division_of i"
+ and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
+ and "K1 \<noteq> K2"
+ and eq: "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
+ shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
+proof -
+ have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
+ using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
+ then show ?thesis
+ using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+qed
+
+lemma (in comm_monoid_set) over_tagged_division_lemma:
+ assumes "p tagged_division_of i"
+ and "\<And>u v. box u v = {} \<Longrightarrow> d (cbox u v) = \<^bold>1"
+ shows "F (\<lambda>(_, k). d k) p = F d (snd ` p)"
+proof -
+ have *: "(\<lambda>(_ ,k). d k) = d \<circ> snd"
+ by (simp add: fun_eq_iff)
+ note assm = tagged_division_ofD[OF assms(1)]
+ show ?thesis
+ unfolding *
+ proof (rule reindex_nontrivial[symmetric])
+ show "finite p"
+ using assm by auto
+ fix x y
+ assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
+ obtain a b where ab: "snd x = cbox a b"
+ using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
+ have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
+ using \<open>x \<in> p\<close> \<open>x \<noteq> y\<close> \<open>snd x = snd y\<close> [symmetric] by auto
+ with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
+ by (intro assm(5)[of "fst x" _ "fst y"]) auto
+ then have "box a b = {}"
+ unfolding \<open>snd x = snd y\<close>[symmetric] ab by auto
+ then have "d (cbox a b) = \<^bold>1"
+ using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
+ then show "d (snd x) = \<^bold>1"
+ unfolding ab by auto
+ qed
+qed
+
+
subsection \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
@@ -1231,29 +1318,21 @@
lemma comm_monoid_set_and: "comm_monoid_set HOL.conj True"
by (rule comm_monoid_set.intro) (fact comm_monoid_and)
-paragraph \<open>Operative\<close>
-definition (in comm_monoid) operative :: "('b::euclidean_space set \<Rightarrow> 'a) \<Rightarrow> bool"
- where "operative g \<longleftrightarrow>
- (\<forall>a b. box a b = {} \<longrightarrow> g (cbox a b) = \<^bold>1) \<and>
- (\<forall>a b c. \<forall>k\<in>Basis. g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c}))"
+paragraph \<open>Misc\<close>
-lemma (in comm_monoid) operativeD[dest]:
- assumes "operative g"
- shows "\<And>a b. box a b = {} \<Longrightarrow> g (cbox a b) = \<^bold>1"
- and "\<And>a b c k. k \<in> Basis \<Longrightarrow> g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
- using assms unfolding operative_def by auto
+lemma interval_real_split:
+ "{a .. b::real} \<inter> {x. x \<le> c} = {a .. min b c}"
+ "{a .. b} \<inter> {x. c \<le> x} = {max a c .. b}"
+ apply (metis Int_atLeastAtMostL1 atMost_def)
+ apply (metis Int_atLeastAtMostL2 atLeast_def)
+ done
-lemma (in comm_monoid) operative_empty:
- assumes g: "operative g" shows "g {} = \<^bold>1"
-proof -
- have *: "cbox One (-One) = ({}::'b set)"
- by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
- moreover have "box One (-One) = ({}::'b set)"
- using box_subset_cbox[of One "-One"] by (auto simp: *)
- ultimately show ?thesis
- using operativeD(1)[OF g, of One "-One"] by simp
-qed
+lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
+ by (meson zero_less_one)
+
+
+paragraph \<open>Division points\<close>
definition "division_points (k::('a::euclidean_space) set) d =
{(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
@@ -1460,30 +1539,47 @@
done
by (simp add: interval_split k interval_doublesplit)
qed
-
-lemma (in comm_monoid_set) operative_division:
+
+paragraph \<open>Operative\<close>
+
+locale operative = comm_monoid_set +
fixes g :: "'b::euclidean_space set \<Rightarrow> 'a"
- assumes g: "operative g" and d: "d division_of (cbox a b)" shows "F g d = g (cbox a b)"
+ assumes box_empty_imp: "\<And>a b. box a b = {} \<Longrightarrow> g (cbox a b) = \<^bold>1"
+ and Basis_imp: "\<And>a b c k. k \<in> Basis \<Longrightarrow> g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+begin
+
+lemma empty [simp]:
+ "g {} = \<^bold>1"
+proof -
+ have *: "cbox One (-One) = ({}::'b set)"
+ by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
+ moreover have "box One (-One) = ({}::'b set)"
+ using box_subset_cbox[of One "-One"] by (auto simp: *)
+ ultimately show ?thesis
+ using box_empty_imp [of One "-One"] by simp
+qed
+
+lemma division:
+ "F g d = g (cbox a b)" if "d division_of (cbox a b)"
proof -
define C where [abs_def]: "C = card (division_points (cbox a b) d)"
then show ?thesis
- using d
- proof (induction C arbitrary: a b d rule: less_induct)
+ using that proof (induction C arbitrary: a b d rule: less_induct)
case (less a b d)
show ?case
proof cases
assume "box a b = {}"
{ fix k assume "k\<in>d"
then obtain a' b' where k: "k = cbox a' b'"
- using division_ofD(4)[OF less.prems] by blast
+ using division_ofD(4) [OF less.prems] by blast
with \<open>k\<in>d\<close> division_ofD(2)[OF less.prems] have "cbox a' b' \<subseteq> cbox a b"
by auto
then have "box a' b' \<subseteq> box a b"
unfolding subset_box by auto
then have "g k = \<^bold>1"
- using operativeD(1)[OF g, of a' b'] k by (simp add: \<open>box a b = {}\<close>) }
+ using box_empty_imp [of a' b'] k by (simp add: \<open>box a b = {}\<close>) }
then show "box a b = {} \<Longrightarrow> F g d = g (cbox a b)"
- by (auto intro!: neutral simp: operativeD(1)[OF g])
+ by (auto intro!: neutral simp: box_empty_imp)
next
assume "box a b \<noteq> {}"
then have ab: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" and ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
@@ -1558,7 +1654,7 @@
then have "box u v = {}"
using j unfolding box_eq_empty by (auto intro!: bexI[of _ j])
then show "g x = \<^bold>1"
- unfolding uv(1) by (rule operativeD(1)[OF g])
+ unfolding uv(1) by (rule box_empty_imp)
qed
then show "F g d = g (cbox a b)"
using division_ofD[OF less.prems]
@@ -1611,7 +1707,8 @@
have "interior (cbox u v \<inter> ?lec) = {}"
using that division_split_left_inj leq less.prems by blast
then show ?thesis
- unfolding leq interval_split[OF \<open>k \<in> Basis\<close>] using g by auto
+ unfolding leq interval_split [OF \<open>k \<in> Basis\<close>]
+ by (auto intro: box_empty_imp)
qed
have fxk_ge: "g (l \<inter> {x. x \<bullet> k \<ge> c}) = \<^bold>1"
if "l \<in> d" "y \<in> d" "l \<inter> ?gec = y \<inter> ?gec" "l \<noteq> y" for l y
@@ -1621,23 +1718,26 @@
have "interior (cbox u v \<inter> ?gec) = {}"
using that division_split_right_inj leq less.prems by blast
then show ?thesis
- unfolding leq interval_split[OF \<open>k \<in> Basis\<close>] using g by auto
+ unfolding leq interval_split[OF \<open>k \<in> Basis\<close>]
+ by (auto intro: box_empty_imp)
qed
have d1_alt: "d1 = (\<lambda>l. l \<inter> ?lec) ` {l \<in> d. l \<inter> ?lec \<noteq> {}}"
using d1_def by auto
have d2_alt: "d2 = (\<lambda>l. l \<inter> ?gec) ` {l \<in> d. l \<inter> ?gec \<noteq> {}}"
using d2_def by auto
have "g (cbox a b) = F g d1 \<^bold>* F g d2" (is "_ = ?prev")
- unfolding * using g \<open>k \<in> Basis\<close> by blast
+ unfolding * using \<open>k \<in> Basis\<close>
+ by (auto dest: Basis_imp)
also have "F g d1 = F (\<lambda>l. g (l \<inter> ?lec)) d"
unfolding d1_alt using division_of_finite[OF less.prems] fxk_le
- by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
+ by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
also have "F g d2 = F (\<lambda>l. g (l \<inter> ?gec)) d"
unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge
- by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
+ by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
also have *: "\<forall>x\<in>d. g x = g (x \<inter> ?lec) \<^bold>* g (x \<inter> ?gec)"
unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
- using g \<open>k \<in> Basis\<close> by blast
+ using \<open>k \<in> Basis\<close>
+ by (auto dest: Basis_imp)
have "F (\<lambda>l. g (l \<inter> ?lec)) d \<^bold>* F (\<lambda>l. g (l \<inter> ?gec)) d = F g d"
using * by (simp add: distrib)
finally show ?thesis by auto
@@ -1646,166 +1746,86 @@
qed
qed
-lemma (in comm_monoid_set) over_tagged_division_lemma:
- assumes "p tagged_division_of i"
- and "\<And>u v. cbox u v \<noteq> {} \<Longrightarrow> box u v = {} \<Longrightarrow> d (cbox u v) = \<^bold>1"
- shows "F (\<lambda>(x,k). d k) p = F d (snd ` p)"
+lemma tagged_division:
+ assumes "d tagged_division_of (cbox a b)"
+ shows "F (\<lambda>(_, l). g l) d = g (cbox a b)"
+proof -
+ have "F (\<lambda>(_, k). g k) d = F g (snd ` d)"
+ using assms box_empty_imp by (rule over_tagged_division_lemma)
+ then show ?thesis
+ unfolding assms [THEN division_of_tagged_division, THEN division] .
+qed
+
+end
+
+locale operative_real = comm_monoid_set +
+ fixes g :: "real set \<Rightarrow> 'a"
+ assumes neutral: "b \<le> a \<Longrightarrow> g {a..b} = \<^bold>1"
+ assumes coalesce_less: "a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+begin
+
+sublocale operative where g = g
+ rewrites "box = (greaterThanLessThan :: real \<Rightarrow> _)"
+ and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
+ and "\<And>x::real. x \<in> Basis \<longleftrightarrow> x = 1"
proof -
- have *: "(\<lambda>(x,k). d k) = d \<circ> snd"
- unfolding o_def by (rule ext) auto
- note assm = tagged_division_ofD[OF assms(1)]
+ show "operative f z g"
+ proof
+ show "g (cbox a b) = \<^bold>1" if "box a b = {}" for a b
+ using that by (simp add: neutral)
+ show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
+ if "k \<in> Basis" for a b c k
+ proof -
+ from that have [simp]: "k = 1"
+ by simp
+ from neutral [of 0 1] neutral [of a a for a] coalesce_less
+ have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
+ "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+ by auto
+ have "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
+ by (auto simp: min_def max_def le_less)
+ then show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
+ by (simp add: atMost_def [symmetric] atLeast_def [symmetric])
+ qed
+ qed
+ show "box = (greaterThanLessThan :: real \<Rightarrow> _)"
+ and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
+ and "\<And>x::real. x \<in> Basis \<longleftrightarrow> x = 1"
+ by (simp_all add: fun_eq_iff)
+qed
+
+lemma coalesce_less_eq:
+ "g {a..c} \<^bold>* g {c..b} = g {a..b}" if "a \<le> c" "c \<le> b"
+proof (cases "c = a \<or> c = b")
+ case False
+ with that have "a < c" "c < b"
+ by auto
+ then show ?thesis
+ by (rule coalesce_less)
+next
+ case True
+ with that box_empty_imp [of a a] box_empty_imp [of b b] show ?thesis
+ by safe simp_all
+qed
+
+end
+
+lemma operative_realI:
+ "operative_real f z g" if "operative f z g"
+proof -
+ interpret operative f z g
+ using that .
show ?thesis
- unfolding *
- proof (rule reindex_nontrivial[symmetric])
- show "finite p"
- using assm by auto
- fix x y
- assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
- obtain a b where ab: "snd x = cbox a b"
- using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
- have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
- by (metis prod.collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
- with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
- by (intro assm(5)[of "fst x" _ "fst y"]) auto
- then have "box a b = {}"
- unfolding \<open>snd x = snd y\<close>[symmetric] ab by auto
- then have "d (cbox a b) = \<^bold>1"
- using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
- then show "d (snd x) = \<^bold>1"
- unfolding ab by auto
+ proof
+ show "g {a..b} = z" if "b \<le> a" for a b
+ using that box_empty_imp by simp
+ show "f (g {a..c}) (g {c..b}) = g {a..b}" if "a < c" "c < b" for a b c
+ using that
+ using Basis_imp [of 1 a b c]
+ by (simp_all add: atMost_def [symmetric] atLeast_def [symmetric] max_def min_def)
qed
qed
-lemma (in comm_monoid_set) operative_tagged_division:
- assumes f: "operative g" and d: "d tagged_division_of (cbox a b)"
- shows "F (\<lambda>(x, l). g l) d = g (cbox a b)"
- unfolding d[THEN division_of_tagged_division, THEN operative_division[OF f], symmetric]
- by (simp add: f[THEN operativeD(1)] over_tagged_division_lemma[OF d])
-
-lemma interval_real_split:
- "{a .. b::real} \<inter> {x. x \<le> c} = {a .. min b c}"
- "{a .. b} \<inter> {x. c \<le> x} = {max a c .. b}"
- apply (metis Int_atLeastAtMostL1 atMost_def)
- apply (metis Int_atLeastAtMostL2 atLeast_def)
- done
-
-lemma (in comm_monoid) operative_1_lt:
- "operative (g :: real set \<Rightarrow> 'a) \<longleftrightarrow>
- ((\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1) \<and> (\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))"
- apply (simp add: operative_def atMost_def[symmetric] atLeast_def[symmetric])
-proof safe
- fix a b c :: real
- assume *: "\<forall>a b c. g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
- assume "a < c" "c < b"
- with *[rule_format, of a b c] show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
- by (simp add: less_imp_le min.absorb2 max.absorb2)
-next
- fix a b c :: real
- assume as: "\<forall>a b. b \<le> a \<longrightarrow> g {a..b} = \<^bold>1"
- "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
- from as(1)[rule_format, of 0 1] as(1)[rule_format, of a a for a] as(2)
- have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
- "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
- by auto
- show "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
- by (auto simp: min_def max_def le_less)
-qed
-
-lemma (in comm_monoid) operative_1_le:
- "operative (g :: real set \<Rightarrow> 'a) \<longleftrightarrow>
- ((\<forall>a b. b \<le> a \<longrightarrow> g {a..b} = \<^bold>1) \<and> (\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))"
- unfolding operative_1_lt
-proof safe
- fix a b c :: real
- assume as: "\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}" "a < c" "c < b"
- show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
- apply (rule as(1)[rule_format])
- using as(2-)
- apply auto
- done
-next
- fix a b c :: real
- assume eq1: "\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1"
- and eqg: "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
- and "a \<le> c"
- and "c \<le> b"
- show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
- proof (cases "c = a \<or> c = b")
- case False
- then show ?thesis
- using eqg \<open>a \<le> c\<close> \<open>c \<le> b\<close> by auto
- next
- case True
- then show ?thesis
- proof
- assume *: "c = a"
- then have "g {a .. c} = \<^bold>1"
- using eq1 by blast
- then show ?thesis
- unfolding * by auto
- next
- assume *: "c = b"
- then have "g {c .. b} = \<^bold>1"
- using eq1 by blast
- then show ?thesis
- unfolding * by auto
- qed
- qed
-qed
-
-lemma tagged_division_union_interval:
- fixes a :: "'a::euclidean_space"
- assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
- and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
- and k: "k \<in> Basis"
- shows "(p1 \<union> p2) tagged_division_of (cbox a b)"
-proof -
- have *: "cbox a b = (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<union> (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
- by auto
- show ?thesis
- apply (subst *)
- apply (rule tagged_division_union[OF assms(1-2)])
- unfolding interval_split[OF k] interior_cbox
- using k
- apply (auto simp add: box_def elim!: ballE[where x=k])
- done
-qed
-
-lemma tagged_division_union_interval_real:
- fixes a :: real
- assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
- and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
- and k: "k \<in> Basis"
- shows "(p1 \<union> p2) tagged_division_of {a .. b}"
- using assms
- unfolding box_real[symmetric]
- by (rule tagged_division_union_interval)
-
-lemma tagged_division_split_left_inj:
- assumes d: "d tagged_division_of i"
- and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
- and "K1 \<noteq> K2"
- and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
- shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
-proof -
- have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
- using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
- then show ?thesis
- using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
-qed
-
-lemma tagged_division_split_right_inj:
- assumes d: "d tagged_division_of i"
- and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
- and "K1 \<noteq> K2"
- and eq: "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
- shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
-proof -
- have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
- using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
- then show ?thesis
- using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
-qed
subsection \<open>Special case of additivity we need for the FTC.\<close>
@@ -1816,10 +1836,11 @@
shows "sum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
proof -
let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
+ interpret operative_real plus 0 ?f
+ rewrites "comm_monoid_set.F op + 0 = sum"
+ by standard[1] (auto simp add: sum_def)
have p_td: "p tagged_division_of cbox a b"
using assms(2) box_real(2) by presburger
- have *: "add.operative ?f"
- unfolding add.operative_1_lt box_eq_empty by auto
have **: "cbox a b \<noteq> {}"
using assms(1) by auto
then have "f b - f a = (\<Sum>(x, l)\<in>p. if l = {} then 0 else f (interval_upperbound l) - f (interval_lowerbound l))"
@@ -1827,14 +1848,12 @@
have "(if cbox a b = {} then 0 else f (interval_upperbound (cbox a b)) - f (interval_lowerbound (cbox a b))) = f b - f a"
using assms by auto
then show ?thesis
- using p_td assms by (simp add: "*" sum.operative_tagged_division)
+ using p_td assms by (simp add: tagged_division)
qed
then show ?thesis
using assms by (auto intro!: sum.cong)
qed
-lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
- by (meson zero_less_one)
subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>