--- a/src/HOL/Analysis/Ball_Volume.thy Mon Oct 04 12:32:50 2021 +0100
+++ b/src/HOL/Analysis/Ball_Volume.thy Mon Oct 04 16:10:55 2021 +0100
@@ -1,4 +1,4 @@
-(*
+(*
File: HOL/Analysis/Ball_Volume.thy
Author: Manuel Eberl, TU München
*)
@@ -25,11 +25,11 @@
text \<open>
We first need the value of the following integral, which is at the core of
- computing the measure of an \<open>n + 1\<close>-dimensional ball in terms of the measure of an
+ computing the measure of an \<open>n + 1\<close>-dimensional ball in terms of the measure of an
\<open>n\<close>-dimensional one.
\<close>
lemma emeasure_cball_aux_integral:
- "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) =
+ "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) =
ennreal (Beta (1 / 2) (real n / 2 + 1))"
proof -
have "((\<lambda>t. t powr (-1 / 2) * (1 - t) powr (real n / 2)) has_integral
@@ -37,7 +37,7 @@
using has_integral_Beta_real[of "1/2" "n / 2 + 1"] by simp
from nn_integral_has_integral_lebesgue[OF _ this] have
"ennreal (Beta (1 / 2) (real n / 2 + 1)) =
- nn_integral lborel (\<lambda>t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) *
+ nn_integral lborel (\<lambda>t. ennreal (t powr (-1 / 2) * (1 - t) powr (real n / 2) *
indicator {0^2..1^2} t))"
by (simp add: mult_ac ennreal_mult' ennreal_indicator)
also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (x\<^sup>2 powr - (1 / 2) * (1 - x\<^sup>2) powr (real n / 2) * (2 * x) *
@@ -45,7 +45,7 @@
by (subst nn_integral_substitution[where g = "\<lambda>x. x ^ 2" and g' = "\<lambda>x. 2 * x"])
(auto intro!: derivative_eq_intros continuous_intros simp: set_borel_measurable_def)
also have "\<dots> = (\<integral>\<^sup>+ x. 2 * ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
- by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"])
+ by (intro nn_integral_cong_AE AE_I[of _ _ "{0}"])
(auto simp: indicator_def powr_minus powr_half_sqrt field_split_simps ennreal_mult')
also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel) +
(\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {0..1} x) \<partial>lborel)"
@@ -54,7 +54,7 @@
by (subst nn_integral_real_affine[of _ "-1" 0])
(auto simp: indicator_def intro!: nn_integral_cong)
hence "?I + ?I = \<dots> + ?I" by simp
- also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) *
+ also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) *
(indicator {-1..0} x + indicator{0..1} x)) \<partial>lborel)"
by (subst nn_integral_add [symmetric]) (auto simp: algebra_simps)
also have "\<dots> = (\<integral>\<^sup>+ x. ennreal ((1 - x\<^sup>2) powr (real n / 2) * indicator {-1..1} x) \<partial>lborel)"
@@ -69,13 +69,10 @@
lemma real_sqrt_le_iff': "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> sqrt x \<le> y \<longleftrightarrow> x \<le> y ^ 2"
using real_le_lsqrt sqrt_le_D by blast
-lemma power2_le_iff_abs_le: "y \<ge> 0 \<Longrightarrow> (x::real) ^ 2 \<le> y ^ 2 \<longleftrightarrow> abs x \<le> y"
- by (subst real_sqrt_le_iff' [symmetric]) auto
-
text \<open>
- Isabelle's type system makes it very difficult to do an induction over the dimension
- of a Euclidean space type, because the type would change in the inductive step. To avoid
- this problem, we instead formulate the problem in a more concrete way by unfolding the
+ Isabelle's type system makes it very difficult to do an induction over the dimension
+ of a Euclidean space type, because the type would change in the inductive step. To avoid
+ this problem, we instead formulate the problem in a more concrete way by unfolding the
definition of the Euclidean norm.
\<close>
lemma emeasure_cball_aux:
@@ -92,17 +89,17 @@
case (insert i A r)
interpret product_sigma_finite "\<lambda>_. lborel"
by standard
- have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
+ have "emeasure (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter> space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) =
nn_integral (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))
(indicator ({f. sqrt (\<Sum>i\<in>insert i A. (f i)\<^sup>2) \<le> r} \<inter>
space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))))"
by (subst nn_integral_indicator) auto
- also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator ({f. sqrt ((f i)\<^sup>2 + (\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> r} \<inter>
- space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y))
+ also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator ({f. sqrt ((f i)\<^sup>2 + (\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> r} \<inter>
+ space (Pi\<^sub>M (insert i A) (\<lambda>_. lborel))) (x(i := y))
\<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
using insert.prems insert.hyps by (subst product_nn_integral_insert_rev) auto
- also have "\<dots> = (\<integral>\<^sup>+ (y::real). \<integral>\<^sup>+ x. indicator {-r..r} y * indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le>
+ also have "\<dots> = (\<integral>\<^sup>+ (y::real). \<integral>\<^sup>+ x. indicator {-r..r} y * indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le>
sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x \<partial>Pi\<^sub>M A (\<lambda>_. lborel) \<partial>lborel)"
proof (intro nn_integral_cong, goal_cases)
case (1 y f)
@@ -118,13 +115,13 @@
thus ?case using 1 \<open>r > 0\<close>
by (auto simp: sum_nonneg real_sqrt_le_iff' indicator_def PiE_def space_PiM dest!: *)
qed
- also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (\<integral>\<^sup>+ x. indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2))
+ also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (\<integral>\<^sup>+ x. indicator ({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2))
\<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) x
\<partial>Pi\<^sub>M A (\<lambda>_. lborel)) \<partial>lborel)" by (subst nn_integral_cmult) auto
- also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel))
+ also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * emeasure (PiM A (\<lambda>_. lborel))
({f. sqrt ((\<Sum>i\<in>A. (f i)\<^sup>2)) \<le> sqrt (r ^ 2 - y ^ 2)} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) \<partial>lborel)"
using \<open>finite A\<close> by (intro nn_integral_cong, subst nn_integral_indicator) auto
- also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) *
+ also have "\<dots> = (\<integral>\<^sup>+ (y::real). indicator {-r..r} y * ennreal (unit_ball_vol (real (card A)) *
(sqrt (r ^ 2 - y ^ 2)) ^ card A) \<partial>lborel)"
proof (intro nn_integral_cong_AE, goal_cases)
case 1
@@ -141,28 +138,28 @@
qed (insert elim, auto)
qed
qed
- also have "\<dots> = ennreal (unit_ball_vol (real (card A))) *
+ also have "\<dots> = ennreal (unit_ball_vol (real (card A))) *
(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel)"
by (subst nn_integral_cmult [symmetric])
(auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
- (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A
+ (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A
\<partial>(distr lborel borel ((*) (1/r))))" using \<open>r > 0\<close>
by (subst nn_integral_distr)
(auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
- also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *
+ also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *
(indicator {- 1..1} x * sqrt (1 - x\<^sup>2) ^ card A) \<partial>lborel)" using \<open>r > 0\<close>
by (subst lborel_distr_mult) (auto simp: nn_integral_density ennreal_mult' [symmetric] mult_ac)
- also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x *
+ also have "\<dots> = ennreal (r ^ Suc (card A)) * (\<integral>\<^sup>+ x. indicator {- 1..1} x *
sqrt (1 - x\<^sup>2) ^ card A \<partial>lborel)"
by (subst nn_integral_cmult) auto
also note emeasure_cball_aux_integral
also have "ennreal (unit_ball_vol (real (card A))) * (ennreal (r ^ Suc (card A)) *
- ennreal (Beta (1/2) (card A / 2 + 1))) =
+ ennreal (Beta (1/2) (card A / 2 + 1))) =
ennreal (unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) * r ^ Suc (card A))"
using \<open>r > 0\<close> by (simp add: ennreal_mult' [symmetric] mult_ac)
also have "unit_ball_vol (card A) * Beta (1/2) (card A / 2 + 1) = unit_ball_vol (Suc (card A))"
- by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps
+ by (auto simp: unit_ball_vol_def Beta_def Gamma_eq_zero_iff field_simps
Gamma_one_half_real powr_half_sqrt [symmetric] powr_add [symmetric])
also have "Suc (card A) = card (insert i A)" using insert.hyps by simp
finally show ?case .
@@ -182,11 +179,11 @@
proof (cases "r = 0")
case False
with r have r: "r > 0" by simp
- have "(lborel :: 'a measure) =
+ have "(lborel :: 'a measure) =
distr (Pi\<^sub>M Basis (\<lambda>_. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
by (rule lborel_eq)
- also have "emeasure \<dots> (cball 0 r) =
- emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel))
+ also have "emeasure \<dots> (cball 0 r) =
+ emeasure (Pi\<^sub>M Basis (\<lambda>_. lborel))
({y. dist 0 (\<Sum>b\<in>Basis. y b *\<^sub>R b :: 'a) \<le> r} \<inter> space (Pi\<^sub>M Basis (\<lambda>_. lborel)))"
by (subst emeasure_distr) (auto simp: cball_def)
also have "{f. dist 0 (\<Sum>b\<in>Basis. f b *\<^sub>R b :: 'a) \<le> r} = {f. sqrt (\<Sum>i\<in>Basis. (f i)\<^sup>2) \<le> r}"
@@ -227,7 +224,7 @@
text \<open>
- Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in
+ Lastly, we now prove some nicer explicit formulas for the volume of the unit balls in
the cases of even and odd integer dimensions.
\<close>
lemma unit_ball_vol_even:
@@ -240,7 +237,7 @@
"unit_ball_vol (real (2 * n + 1)) =
(2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
proof -
- have "unit_ball_vol (real (2 * n + 1)) =
+ have "unit_ball_vol (real (2 * n + 1)) =
pi powr (real n + 1 / 2) / Gamma (1 / 2 + real (Suc n))"
by (simp add: unit_ball_vol_def field_simps)
also have "pochhammer (1 / 2) (Suc n) = Gamma (1 / 2 + real (Suc n)) / Gamma (1 / 2)"
@@ -250,7 +247,7 @@
also have "pi powr (real n + 1 / 2) / \<dots> = pi ^ n / pochhammer (1 / 2) (Suc n)"
by (simp add: powr_add powr_half_sqrt powr_realpow)
finally show "unit_ball_vol (real (2 * n + 1)) = \<dots>" .
- also have "pochhammer (1 / 2 :: real) (Suc n) =
+ also have "pochhammer (1 / 2 :: real) (Suc n) =
fact (2 * Suc n) / (2 ^ (2 * Suc n) * fact (Suc n))"
using fact_double[of "Suc n", where ?'a = real] by (simp add: divide_simps mult_ac)
also have "pi ^n / \<dots> = (2 ^ (2 * Suc n) * fact (Suc n)) / fact (2 * Suc n) * pi ^ n"
@@ -263,7 +260,7 @@
"unit_ball_vol (numeral (Num.Bit1 n)) = 2 ^ (2 * Suc (numeral n)) * fact (Suc (numeral n)) /
fact (2 * Suc (numeral n)) * pi ^ numeral n" (is ?th2)
proof -
- have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)"
+ have "numeral (Num.Bit0 n) = (2 * numeral n :: nat)"
by (simp only: numeral_Bit0 mult_2 ring_distribs)
also have "unit_ball_vol \<dots> = pi ^ numeral n / fact (numeral n)"
by (rule unit_ball_vol_even)