Measures invariant under addition #
This file records measure formulas for finite families of disjoint additive translates. In lattice-point counting, the formula turns disjoint translates of a fundamental-domain cell into measure bounds that can be compared with the number of cells.
Main results #
Measure.measure_biUnion_sub_mem: a finite disjoint union of translates has measure equal to the number of translates times the measure of the original set.
theorem
MeasureTheory.Measure.measure_biUnion_sub_mem
{E : Type u_1}
[AddGroup E]
[MeasurableSpace E]
[MeasurableAdd E]
(mu : Measure E)
[mu.IsAddRightInvariant]
{G F : Set E}
(hFm : MeasurableSet F)
(hdisj : ∀ w₁ ∈ G, ∀ w₂ ∈ G, w₁ ≠ w₂ → Disjoint {y : E | y - w₁ ∈ F} {y : E | y - w₂ ∈ F})
{T : Finset E}
(hT : ↑T ⊆ G)
:
The union of finitely many pairwise disjoint translates of a measurable set has measure equal to the number of translates times the measure of the set.