equal
deleted
inserted
replaced
43 lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)" |
43 lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)" |
44 unfolding content_cbox_cases by simp |
44 unfolding content_cbox_cases by simp |
45 |
45 |
46 lemma content_cbox': "cbox a b \<noteq> {} \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)" |
46 lemma content_cbox': "cbox a b \<noteq> {} \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)" |
47 by (simp add: box_ne_empty inner_diff) |
47 by (simp add: box_ne_empty inner_diff) |
|
48 |
|
49 lemma content_cbox_if: "content (cbox a b) = (if cbox a b = {} then 0 else \<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)" |
|
50 by (simp add: content_cbox') |
|
51 |
|
52 lemma content_division_of: |
|
53 assumes "K \<in> \<D>" "\<D> division_of S" |
|
54 shows "content K = (\<Prod>i \<in> Basis. interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)" |
|
55 proof - |
|
56 obtain a b where "K = cbox a b" |
|
57 using cbox_division_memE assms by metis |
|
58 then show ?thesis |
|
59 using assms by (force simp: division_of_def content_cbox') |
|
60 qed |
48 |
61 |
49 lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a" |
62 lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a" |
50 by simp |
63 by simp |
51 |
64 |
52 lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})" |
65 lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})" |