English
If a null-measurable subset of the circle is almost invariant under all rational rotations with denominators growing, then it is almost empty or almost full.
Русский
Если нуль-измеримое множество на окружности почти инвариантно относительно все рациональные вращения с знаменателями растущими, тогда множество почти пусто или почти всё.
LaTeX
$$$\text{ae\_empty\_or\_univ\_of\_forall\_vadd\_ae\_eq\_self}$$$
Lean4
/-- If a null-measurable subset of the circle is almost invariant under rotation by a family of
rational angles with denominators tending to infinity, then it must be almost empty or almost full.
-/
theorem ae_empty_or_univ_of_forall_vadd_ae_eq_self {s : Set <| AddCircle T} (hs : NullMeasurableSet s volume)
{ι : Type*} {l : Filter ι} [l.NeBot] {u : ι → AddCircle T} (hu₁ : ∀ i, (u i +ᵥ s : Set _) =ᵐ[volume] s)
(hu₂ : Tendsto (addOrderOf ∘ u) l atTop) : s =ᵐ[volume] (∅ : Set <| AddCircle T) ∨ s =ᵐ[volume] univ := by
/- Sketch of proof:
Assume `T = 1` for simplicity and let `μ` be the Haar measure. We may assume `s` has positive
measure since otherwise there is nothing to prove. In this case, by Lebesgue's density theorem,
there exists a point `d` of positive density. Let `Iⱼ` be the sequence of closed balls about `d`
of diameter `1 / nⱼ` where `nⱼ` is the additive order of `uⱼ`. Since `d` has positive density we
must have `μ (s ∩ Iⱼ) / μ Iⱼ → 1` along `l`. However since `s` is invariant under the action of
`uⱼ` and since `Iⱼ` is a fundamental domain for this action, we must have
`μ (s ∩ Iⱼ) = nⱼ * μ s = (μ Iⱼ) * μ s`. We thus have `μ s → 1` and thus `μ s = 1`. -/
set μ := (volume : Measure <| AddCircle T)
set n : ι → ℕ := addOrderOf ∘ u
have hT₀ : 0 < T := hT.out
have hT₁ : ENNReal.ofReal T ≠ 0 := by simpa
rw [ae_eq_empty, ae_eq_univ_iff_measure_eq hs, AddCircle.measure_univ]
rcases eq_or_ne (μ s) 0 with h | h; · exact Or.inl h
right
obtain ⟨d, -, hd⟩ :
∃ d,
d ∈ s ∧
∀ {ι'} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
Tendsto δ l (𝓝[>] 0) →
(∀ᶠ j in l, d ∈ closedBall (w j) (1 * δ j)) →
Tendsto (fun j => μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1) :=
exists_mem_of_measure_ne_zero_of_ae h (IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div μ s 1)
let I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
replace hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1) :=
by
let δ : ι → ℝ := fun j => T / (2 * ↑(n j))
have hδ₀ : ∀ᶠ j in l, 0 < δ j := (hu₂.eventually_gt_atTop 0).mono fun j hj => div_pos hT₀ <| by positivity
have hδ₁ : Tendsto δ l (𝓝[>] 0) := by
refine tendsto_nhdsWithin_iff.mpr ⟨?_, hδ₀⟩
replace hu₂ : Tendsto (fun j => T⁻¹ * 2 * n j) l atTop :=
(tendsto_natCast_atTop_iff.mpr hu₂).const_mul_atTop (by positivity : 0 < T⁻¹ * 2)
convert hu₂.inv_tendsto_atTop
ext j
simp only [δ, Pi.inv_apply, mul_inv_rev, inv_inv, div_eq_inv_mul, ← mul_assoc]
have hw : ∀ᶠ j in l, d ∈ closedBall d (1 * δ j) :=
hδ₀.mono fun j hj => by
simp only [one_mul, mem_closedBall, dist_self]
apply hj.le
exact hd _ δ hδ₁ hw
suffices ∀ᶠ j in l, μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
by
replace hd := hd.congr' this
rwa [tendsto_const_nhds_iff, ENNReal.div_eq_one_iff hT₁ ENNReal.ofReal_ne_top] at hd
refine (hu₂.eventually_gt_atTop 0).mono fun j hj => ?_
have : addOrderOf (u j) = n j := rfl
have huj : IsOfFinAddOrder (u j) := addOrderOf_pos_iff.mp hj
have huj' : 1 ≤ (↑(n j) : ℝ) := by norm_cast
have hI₀ : μ (I j) ≠ 0 := (measure_closedBall_pos _ d <| by positivity).ne.symm
have hI₁ : μ (I j) ≠ ⊤ := measure_ne_top _ _
have hI₂ : μ (I j) * ↑(n j) = ENNReal.ofReal T :=
by
rw [volume_closedBall, mul_div, mul_div_mul_left T _ two_ne_zero, min_eq_right (div_le_self hT₀.le huj'), mul_comm,
← nsmul_eq_mul, ← ENNReal.ofReal_nsmul, nsmul_eq_mul, mul_div_cancel₀]
exact Nat.cast_ne_zero.mpr hj.ne'
rw [ENNReal.div_eq_div_iff hT₁ ENNReal.ofReal_ne_top hI₀ hI₁,
volume_of_add_preimage_eq s _ (u j) d huj (hu₁ j) closedBall_ae_eq_ball, nsmul_eq_mul, ← mul_assoc, this, hI₂]
