src/HOL/Analysis/Ball_Volume.thy
changeset 69566 c41954ee87cf
parent 69517 dc20f278e8f3
child 70136 f03a01a18c6e
     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Tue Jan 01 20:57:54 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Tue Jan 01 21:47:27 2019 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4     Author:   Manuel Eberl, TU M√ľnchen
     1.5  *)
     1.6  
     1.7 -section \<open>The Volume of an $n$-Dimensional Ball\<close>
     1.8 +section \<open>The Volume of an \<open>n\<close>-Dimensional Ball\<close>
     1.9  
    1.10  theory Ball_Volume
    1.11    imports Gamma_Function Lebesgue_Integral_Substitution
    1.12 @@ -25,8 +25,8 @@
    1.13  
    1.14  text \<open>
    1.15    We first need the value of the following integral, which is at the core of
    1.16 -  computing the measure of an $n+1$-dimensional ball in terms of the measure of an 
    1.17 -  $n$-dimensional one.
    1.18 +  computing the measure of an \<open>n + 1\<close>-dimensional ball in terms of the measure of an 
    1.19 +  \<open>n\<close>-dimensional one.
    1.20  \<close>
    1.21  lemma emeasure_cball_aux_integral:
    1.22    "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) =