English
Let E be a finite-dimensional real normed vector space with Haar measure μ. If s ⊆ E is bounded and nonempty and u: N → E is a bounded sequence such that the translates {u(n)} + s are pairwise disjoint for all n, then μ(s) = 0.
Русский
Пусть E — конечномерное вещественное нормированное пространство с гааровской мерой μ. Пусть s ⊆ E ограничено и непусто, а u: ℕ → E — ограниченная последовательность так, что множества {u(n)} + s попарно попарно непересекаются. Тогда μ(s) = 0.
LaTeX
$$$\\mu(s) = 0$$$
Lean4
/-- If a set is disjoint of its translates by infinitely many bounded vectors, then it has measure
zero. This auxiliary lemma proves this assuming additionally that the set is bounded. -/
theorem addHaar_eq_zero_of_disjoint_translates_aux {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ] {s : Set E}
(u : ℕ → E) (sb : IsBounded s) (hu : IsBounded (range u)) (hs : Pairwise (Disjoint on fun n => {u n} + s))
(h's : MeasurableSet s) : μ s = 0 := by
by_contra h
apply lt_irrefl ∞
calc
∞ = ∑' _ : ℕ, μ s := (ENNReal.tsum_const_eq_top_of_ne_zero h).symm
_ = ∑' n : ℕ, μ ({u n} + s) := by congr 1; ext1 n; simp only [image_add_left, measure_preimage_add, singleton_add]
_ = μ (⋃ n, {u n} + s) :=
(Eq.symm <|
measure_iUnion hs fun n => by simpa only [image_add_left, singleton_add] using measurable_id.const_add _ h's)
_ = μ (range u + s) := by rw [← iUnion_add, iUnion_singleton_eq_range]
_ < ∞ := (hu.add sb).measure_lt_top
