src/HOL/Analysis/Ball_Volume.thy
 changeset 67982 7643b005b29a parent 67976 75b94eb58c3d child 68624 205d352ed727
```     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Sat Apr 14 20:19:52 2018 +0100
1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Sun Apr 15 13:57:00 2018 +0100
1.3 @@ -1,10 +1,10 @@
1.4  (*
1.5     File:     HOL/Analysis/Gamma_Function.thy
1.6     Author:   Manuel Eberl, TU München
1.7 +*)
1.8
1.9 -   The volume (Lebesgue measure) of an n-dimensional ball.
1.10 -*)
1.11 -section \<open>The volume of an \$n\$-ball\<close>
1.12 +section \<open>The volume (Lebesgue measure) of an \$n\$-dimensional ball\<close>
1.13 +
1.14  theory Ball_Volume
1.15    imports Gamma_Function Lebesgue_Integral_Substitution
1.16  begin
1.17 @@ -301,4 +301,30 @@
1.18  corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
1.19    by (simp add: content_ball unit_ball_vol_3)
1.20
1.21 +text \<open>
1.22 +  Useful equivalent forms
1.23 +\<close>
1.24 +corollary content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.25 +proof -
1.26 +  have "r > 0 \<Longrightarrow> content (ball c r) > 0"
1.27 +    by (simp add: content_ball unit_ball_vol_def)
1.28 +  then show ?thesis
1.29 +    by (fastforce simp: ball_empty)
1.30 +qed
1.31 +
1.32 +corollary content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
1.33 +  by (auto simp: zero_less_measure_iff)
1.34 +
1.35 +corollary content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.36 +proof (cases "r = 0")
1.37 +  case False
1.38 +  moreover have "r > 0 \<Longrightarrow> content (cball c r) > 0"
1.39 +    by (simp add: content_cball unit_ball_vol_def)
1.40 +  ultimately show ?thesis
1.41 +    by fastforce
1.42 +qed auto
1.43 +
1.44 +corollary content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
1.45 +  by (auto simp: zero_less_measure_iff)
1.46 +
1.47  end
```