Theorems · Theorem · measure theory

MeasureTheory.Measure.addHaar_eq_zero_of_disjoint_translates_aux

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {s : Set E} (u : ℕ → E),
  Bornology.IsBounded s →
    Bornology.IsBounded (Set.range u) →
      Pairwise (Function.onFun Disjoint fun n => {u n} + s) → MeasurableSet s → μ s = 0

If a set is disjoint from its translates by infinitely many bounded vectors, then it has measure zero. This auxiliary lemma proves this assuming additionally that the set is bounded.

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Cited by

1 results in Mathlib

Foundations

Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceFiniteDimensionalMeasureTheory.Measure.IsAddHaarMeasure