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