Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Count ↔ volume bridge

Abstract

Count ↔ volume bridge.

Theorem 1.1 (Count ↔ volume bridge).

Lean statement: D5/S3/Arith/Lattices/Counting/LatticePointCount.abs_card_inter_sub_volume_mul_pow_le

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/Counting/LatticePointCount.abs_card_inter_sub_volume_mul_pow_le (✓ std3). ∎

Citation. Chris Birkbeck and the Chebotarev density contributors (2026). Chebotarev density in Lean. URL: https://github.com/CBirkbeck/chebotarev-density/tree/a00054a0e6bbc394b0e81de750db0cd2efc8bd88.

Commentary.

Count ↔ volume bridge. The number of points of n⁻¹ℤ^ι in a bounded measurable s differs from vol(s)·nᵈ by at most the number of grid cells meeting ∂s. This is the effective form of the sandwich behind tendsto_card_div_pow_atTop_volume.

References

  • Truth anchor: D5/S3/Arith/Lattices/Counting/LatticePointCount.abs_card_inter_sub_volume_mul_pow_le