English
If a compact closed set k is everywhere positive with respect to a left-invariant measure on a topological group, then k is a Gδ set.
Русский
Если компактно-замкнутое множество k имеет повсюду положительную меру относительно лево-инвариантной меры на топологической группе, то k является Gδ.
LaTeX
$$IsEverywherePos μ k → IsCompact k → IsClosed k → IsGδ k$$
Lean4
/-- If a compact closed set is everywhere positive with respect to a left-invariant measure on a
topological group, then it is a Gδ set. This is nontrivial, as there is no second-countability or
metrizability assumption in the statement, so a general compact closed set has no reason to be
a countable intersection of open sets. -/
@[to_additive]
theorem IsGdelta_of_isMulLeftInvariant {k : Set G} (h : μ.IsEverywherePos k) (hk : IsCompact k) (h'k : IsClosed k) :
IsGδ k := by
/- Consider a decreasing sequence of open neighborhoods `Vₙ` of the identity, such that `g k \ k`
has small measure for all `g ∈ Vₙ`. We claim that `k = ⋂ Vₙ k`, which proves
the lemma as the sets on the right are open. The inclusion `⊆` is trivial.
Let us show the converse. Take `x` in the intersection. For each `n`, write `x = vₙ yₙ` with
`vₙ ∈ Vₙ` and `yₙ ∈ k`. Let `z ∈ k` be a cluster value of `yₙ`, by compactness. As multiplication
by `vₙ = x yₙ⁻¹ ∈ Vₙ` changes the measure of `k` by very little, passing to the limit we get
`μ (x z⁻¹ k \ k) = 0`. By invariance of the measure under `z x ⁻¹`, we get `μ (k \ z x⁻¹ k) = 0`.
Assume `x ∉ k`. Then `z ∈ k \ z x⁻¹ k`. Even more, this set is a neighborhood of `z` within `k`
(as `z x⁻¹ k` is closed), and it has zero measure. This contradicts the fact that `k` has
positive measure around the point `z`. -/
obtain ⟨u, -, u_mem, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo 0 1) ∧ Tendsto u atTop (𝓝 0) :=
exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ≥0∞) < 1)
have : ∀ n, ∃ (W : Set G), IsOpen W ∧ 1 ∈ W ∧ ∀ g ∈ W * W, μ ((g • k) \ k) < u n := fun n ↦
exists_open_nhds_one_mul_subset (eventually_nhds_one_measure_smul_diff_lt hk h'k (u_mem n).1.ne')
choose W W_open mem_W hW using this
let V n := ⋂ i ∈ Finset.range n, W i
suffices ⋂ n, V n * k ⊆ k
by
replace : k = ⋂ n, V n * k :=
by
apply Subset.antisymm (subset_iInter_iff.2 (fun n ↦ ?_)) this
exact subset_mul_right k (by simp [V, mem_W])
rw [this]
refine .iInter_of_isOpen fun n ↦ ?_
exact .mul_right (isOpen_biInter_finset (fun i _hi ↦ W_open i))
intro x hx
choose v hv y hy hvy using mem_iInter.1 hx
obtain ⟨z, zk, hz⟩ : ∃ z ∈ k, MapClusterPt z atTop y := hk.exists_mapClusterPt (by simp [hy])
have A n : μ (((x * z⁻¹) • k) \ k) ≤ u n := by
apply le_of_lt (hW _ _ ?_)
have : W n * { z } ∈ 𝓝 z := (IsOpen.mul_right (W_open n)).mem_nhds (by simp [mem_W])
obtain ⟨i, hi, ni⟩ : ∃ i, y i ∈ W n * { z } ∧ n < i :=
((hz.frequently this).and_eventually (eventually_gt_atTop n)).exists
refine ⟨x * (y i)⁻¹, ?_, y i * z⁻¹, by simpa using hi, by group⟩
have I : V i ⊆ W n := iInter₂_subset n (by simp [ni])
have J : x * (y i)⁻¹ ∈ V i := by simpa [← hvy i] using hv i
exact I J
have B : μ (((x * z⁻¹) • k) \ k) = 0 := le_antisymm (ge_of_tendsto u_lim (Eventually.of_forall A)) bot_le
have C : μ (k \ (z * x⁻¹) • k) = 0 :=
by
have : μ ((z * x⁻¹) • (((x * z⁻¹) • k) \ k)) = 0 := by rwa [measure_smul]
rw [← this, smul_set_sdiff, smul_smul]
group
simp
by_contra H
have : k ∩ ((z * x⁻¹) • k)ᶜ ∈ 𝓝[k] z := by
apply inter_mem_nhdsWithin k
apply IsOpen.mem_nhds (by simpa using h'k.smul _)
simp only [mem_compl_iff]
contrapose! H
simpa [mem_smul_set_iff_inv_smul_mem] using H
have : 0 < μ (k \ ((z * x⁻¹) • k)) := h z zk _ this
exact lt_irrefl _ (C.le.trans_lt this)
