125 by (simp add: algebra_simps content_cbox_if box_eq_empty) |
125 by (simp add: algebra_simps content_cbox_if box_eq_empty) |
126 |
126 |
127 lemma content_0_subset: "content(cbox a b) = 0 \<Longrightarrow> s \<subseteq> cbox a b \<Longrightarrow> content s = 0" |
127 lemma content_0_subset: "content(cbox a b) = 0 \<Longrightarrow> s \<subseteq> cbox a b \<Longrightarrow> content s = 0" |
128 using emeasure_mono[of s "cbox a b" lborel] |
128 using emeasure_mono[of s "cbox a b" lborel] |
129 by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq) |
129 by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq) |
|
130 |
|
131 lemma content_ball_pos: |
|
132 assumes "r > 0" |
|
133 shows "content (ball c r) > 0" |
|
134 proof - |
|
135 from rational_boxes[OF assms, of c] obtain a b where ab: "c \<in> box a b" "box a b \<subseteq> ball c r" |
|
136 by auto |
|
137 from ab have "0 < content (box a b)" |
|
138 by (subst measure_lborel_box_eq) (auto intro!: prod_pos simp: algebra_simps box_def) |
|
139 have "emeasure lborel (box a b) \<le> emeasure lborel (ball c r)" |
|
140 using ab by (intro emeasure_mono) auto |
|
141 also have "emeasure lborel (box a b) = ennreal (content (box a b))" |
|
142 using emeasure_lborel_box_finite[of a b] by (intro emeasure_eq_ennreal_measure) auto |
|
143 also have "emeasure lborel (ball c r) = ennreal (content (ball c r))" |
|
144 using emeasure_lborel_ball_finite[of c r] by (intro emeasure_eq_ennreal_measure) auto |
|
145 finally show ?thesis |
|
146 using \<open>content (box a b) > 0\<close> by simp |
|
147 qed |
|
148 |
|
149 lemma content_cball_pos: |
|
150 assumes "r > 0" |
|
151 shows "content (cball c r) > 0" |
|
152 proof - |
|
153 from rational_boxes[OF assms, of c] obtain a b where ab: "c \<in> box a b" "box a b \<subseteq> ball c r" |
|
154 by auto |
|
155 from ab have "0 < content (box a b)" |
|
156 by (subst measure_lborel_box_eq) (auto intro!: prod_pos simp: algebra_simps box_def) |
|
157 have "emeasure lborel (box a b) \<le> emeasure lborel (ball c r)" |
|
158 using ab by (intro emeasure_mono) auto |
|
159 also have "\<dots> \<le> emeasure lborel (cball c r)" |
|
160 by (intro emeasure_mono) auto |
|
161 also have "emeasure lborel (box a b) = ennreal (content (box a b))" |
|
162 using emeasure_lborel_box_finite[of a b] by (intro emeasure_eq_ennreal_measure) auto |
|
163 also have "emeasure lborel (cball c r) = ennreal (content (cball c r))" |
|
164 using emeasure_lborel_cball_finite[of c r] by (intro emeasure_eq_ennreal_measure) auto |
|
165 finally show ?thesis |
|
166 using \<open>content (box a b) > 0\<close> by simp |
|
167 qed |
130 |
168 |
131 lemma content_split: |
169 lemma content_split: |
132 fixes a :: "'a::euclidean_space" |
170 fixes a :: "'a::euclidean_space" |
133 assumes "k \<in> Basis" |
171 assumes "k \<in> Basis" |
134 shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})" |
172 shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})" |