measure_eq_tsum_of_ac — Mathlib

English

For invariant ν ≪ μ, and any t, ν(t) equals the sum over G of ν(t ∩ g•s): ν t = ∑' g∈G ν(t ∩ g•s).

Русский

Если ν абсолютно непрерывна по отношению к μ и t зафиксировано, то ν(t) = ∑' g∈G ν(t ∩ g•s).

LaTeX

$$$$\\nu(t) = \\sum_{g\\in G} \\nu(t \\cap (g \\cdot s)).$$$$

Lean4

@[to_additive]
theorem measure_eq_tsum_of_ac (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) (t : Set α) :
    ν t = ∑' g : G, ν (t ∩ g • s) :=
  by
  have H : ν.restrict t ≪ μ := Measure.restrict_le_self.absolutelyContinuous.trans hν
  simpa only [setLIntegral_one, Pi.one_def, Measure.restrict_apply₀ ((h.nullMeasurableSet_smul _).mono_ac H),
    inter_comm] using h.lintegral_eq_tsum_of_ac H 1

Похожие утверждения