English
If hs and ht are fundamental domains for the same action, then for any f, the integrals over s and t agree after invariant translations.
Русский
Если s и t — фундаментальные области одной группы, то для любой f интегралы по s и по t совпадают после инвариантных преобразований.
LaTeX
$$$$\\int_{s} f(x) d\\mu(x) = \\int_{t} f(x) d\\mu(x).$$$$
Lean4
/-- If the action of a countable group `G` admits an invariant measure `μ` with a fundamental domain
`s`, then every null-measurable set `t` of measure strictly greater than `μ s` contains two
points `x y` such that `g • x = y` for some `g ≠ 1`. -/
@[to_additive /-- If the additive action of a countable group `G` admits an invariant measure `μ`
with a fundamental domain `s`, then every null-measurable set `t` of measure strictly greater than
`μ s` contains two points `x y` such that `g +ᵥ x = y` for some `g ≠ 0`. -/
]
theorem exists_ne_one_smul_eq (hs : IsFundamentalDomain G s μ) (htm : NullMeasurableSet t μ) (ht : μ s < μ t) :
∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ (1 : G) ∧ g • x = y :=
by
contrapose! ht
refine hs.measure_le_of_pairwise_disjoint htm (Pairwise.aedisjoint fun g₁ g₂ hne => ?_)
dsimp [Function.onFun]
refine (Disjoint.inf_left _ ?_).inf_right _
rw [Set.disjoint_left]
rintro _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy : g₂ • y = g₁ • x⟩
refine ht x hx y hy (g₂⁻¹ * g₁) (mt inv_mul_eq_one.1 hne.symm) ?_
rw [mul_smul, ← hxy, inv_smul_smul]
