Commit 2024-12-05 07:37 06422de9

feat(Analysis/BoxIntegral/UnitPartition): Prove results linking integral point counting and integrals (#12405) We prove the following result:

Let s be a bounded, measurable set of ι → ℝ whose frontier has zero volume and let F be a continuous function. Then the limit as n → ∞ of ∑ F x / n ^ card ι, where the sum is over the points in s ∩ n⁻¹ • (ι → ℤ), tends to the integral of F over s. using Riemann integration. As a special case, we deduce that The limit as n → ∞ of card (s ∩ n⁻¹ • (ι → ℤ)) / n ^ card ι tends to the volume of s. Both of these statements are for a variable n : ℕ. However, with the additional hypothesis: x • s ⊆ y • s whenever 0 < x ≤ y, we generalize the previous statement to a real variable. This PR is part of the proof of the Analytic Class Number Formula.