821 |
821 |
822 lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0" |
822 lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0" |
823 using emeasure_lborel_cbox[of x x] nonempty_Basis |
823 using emeasure_lborel_cbox[of x x] nonempty_Basis |
824 by (auto simp del: emeasure_lborel_cbox nonempty_Basis) |
824 by (auto simp del: emeasure_lborel_cbox nonempty_Basis) |
825 |
825 |
|
826 lemma emeasure_lborel_cbox_finite: "emeasure lborel (cbox a b) < \<infinity>" |
|
827 by (auto simp: emeasure_lborel_cbox_eq) |
|
828 |
|
829 lemma emeasure_lborel_box_finite: "emeasure lborel (box a b) < \<infinity>" |
|
830 by (auto simp: emeasure_lborel_box_eq) |
|
831 |
|
832 lemma emeasure_lborel_ball_finite: "emeasure lborel (ball c r) < \<infinity>" |
|
833 proof - |
|
834 have "bounded (ball c r)" by simp |
|
835 from bounded_subset_cbox_symmetric[OF this] obtain a where a: "ball c r \<subseteq> cbox (-a) a" |
|
836 by auto |
|
837 hence "emeasure lborel (ball c r) \<le> emeasure lborel (cbox (-a) a)" |
|
838 by (intro emeasure_mono) auto |
|
839 also have "\<dots> < \<infinity>" by (simp add: emeasure_lborel_cbox_eq) |
|
840 finally show ?thesis . |
|
841 qed |
|
842 |
|
843 lemma emeasure_lborel_cball_finite: "emeasure lborel (cball c r) < \<infinity>" |
|
844 proof - |
|
845 have "bounded (cball c r)" by simp |
|
846 from bounded_subset_cbox_symmetric[OF this] obtain a where a: "cball c r \<subseteq> cbox (-a) a" |
|
847 by auto |
|
848 hence "emeasure lborel (cball c r) \<le> emeasure lborel (cbox (-a) a)" |
|
849 by (intro emeasure_mono) auto |
|
850 also have "\<dots> < \<infinity>" by (simp add: emeasure_lborel_cbox_eq) |
|
851 finally show ?thesis . |
|
852 qed |
|
853 |
826 lemma fmeasurable_cbox [iff]: "cbox a b \<in> fmeasurable lborel" |
854 lemma fmeasurable_cbox [iff]: "cbox a b \<in> fmeasurable lborel" |
827 and fmeasurable_box [iff]: "box a b \<in> fmeasurable lborel" |
855 and fmeasurable_box [iff]: "box a b \<in> fmeasurable lborel" |
828 by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq) |
856 by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq) |
829 |
857 |
830 lemma |
858 lemma |