Commit 2024-12-14 15:50 197eebfa

View on Github →

feat: volume of Euclidean balls in even and odd dimensions (#19949) The formula in terms of the Gamma function is nice, as it is not necessary to split on whether the dimension is even or odd, but for specific calculations (e.g., the volume of a ball in three dimensions), it's nice to have these more specific versions. Written as a consequence of Zulip.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

added theorem Real.Gamma_nat_add_half

added theorem Real.Gamma_nat_add_one_add_half

Modified Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

modified theorem EuclideanSpace.volume_ball

added theorem EuclideanSpace.volume_ball_fin_three

added theorem EuclideanSpace.volume_ball_fin_two

modified theorem EuclideanSpace.volume_closedBall

added theorem EuclideanSpace.volume_closedBall_fin_three

added theorem EuclideanSpace.volume_closedBall_fin_two

modified theorem InnerProductSpace.volume_ball

added theorem InnerProductSpace.volume_ball_of_dim_even

added theorem InnerProductSpace.volume_ball_of_dim_odd

modified theorem InnerProductSpace.volume_closedBall

added theorem InnerProductSpace.volume_closedBall_of_dim_even

added theorem InnerProductSpace.volume_closedBall_of_dim_odd

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean