English
For h and f invariant with respect to G, the restricted integral over g•t ∩ s of f equals the transferred integral.
Русский
Если f инвариантна по G, то ограниченный интеграл по g•t ∩ s равен перенесённому интегралу.
LaTeX
$$$$\\int_{t\\cap (g\\cdot s)} f = \\int_{g\\cdot t\\cap s} f(g^{-1}\\cdot x) \\, d\\mu(x).$$$$
Lean4
@[to_additive]
theorem measure_set_eq (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {A : Set α}
(hA₀ : MeasurableSet A) (hA : ∀ g : G, (fun x => g • x) ⁻¹' A = A) : μ (A ∩ s) = μ (A ∩ t) :=
by
have : ∫⁻ x in s, A.indicator 1 x ∂μ = ∫⁻ x in t, A.indicator 1 x ∂μ :=
by
refine hs.setLIntegral_eq ht (Set.indicator A fun _ => 1) fun g x ↦ ?_
convert (Set.indicator_comp_right (g • · : α → α) (g := fun _ ↦ (1 : ℝ≥0∞))).symm
rw [hA g]
simpa [Measure.restrict_apply hA₀, lintegral_indicator hA₀] using this
