English
In the same setting as above, if the translates {u(n)} + s are pairwise disjoint for infinitely many bounded vectors u(n) and s is measurable, then μ(s) = 0.
Русский
В тех же условиях, если для бесконечного множества ограниченных векторов u(n) множества {u(n)} + s попарно непересекаются и 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. -/
theorem addHaar_eq_zero_of_disjoint_translates {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]
[BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ] {s : Set E} (u : ℕ → E)
(hu : IsBounded (range u)) (hs : Pairwise (Disjoint on fun n => {u n} + s)) (h's : MeasurableSet s) : μ s = 0 :=
by
suffices H : ∀ R, μ (s ∩ closedBall 0 R) = 0
by
apply le_antisymm _ (zero_le _)
calc
μ s ≤ ∑' n : ℕ, μ (s ∩ closedBall 0 n) :=
by
conv_lhs => rw [← iUnion_inter_closedBall_nat s 0]
exact measure_iUnion_le _
_ = 0 := by simp only [H, tsum_zero]
intro R
apply
addHaar_eq_zero_of_disjoint_translates_aux μ u (isBounded_closedBall.subset inter_subset_right) hu _
(h's.inter measurableSet_closedBall)
refine pairwise_disjoint_mono hs fun n => ?_
exact add_subset_add Subset.rfl inter_subset_left
