English
In a noncompact locally compact group, a left-invariant measure that is positive on open sets has infinite mass: μ(univ) = ∞.
Русский
В некомпактной локально компактной группе левая инвариантная мера, положительная на открытых множествах, имеет бесконечную массу: μ(G) = ∞.
LaTeX
$$$\text{NoncompactSpace}(G) \land \text{WeaklyLocallyCompactSpace}(G) \Rightarrow (\IsOpenPosMeasure(μ) \land μ.IsMulLeftInvariant) \Rightarrow μ(\text{univ}) = ∞$$$
Lean4
/-- In a noncompact locally compact group, a left-invariant measure which is positive
on open sets has infinite mass. -/
@[to_additive (attr := simp) /--
In a noncompact locally compact additive group, a left-invariant measure which is positive on
open sets has infinite mass. -/
]
theorem measure_univ_of_isMulLeftInvariant [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : Measure G)
[IsOpenPosMeasure μ] [μ.IsMulLeftInvariant] : μ univ = ∞ := by
/- Consider a closed compact set `K` with nonempty interior. For any compact set `L`, one may
find `g = g (L)` such that `L` is disjoint from `g • K`. Iterating this, one finds
infinitely many translates of `K` which are disjoint from each other. As they all have the
same positive mass, it follows that the space has infinite measure. -/
obtain ⟨K, K1, hK, Kclosed⟩ : ∃ K ∈ 𝓝 (1 : G), IsCompact K ∧ IsClosed K := exists_mem_nhds_isCompact_isClosed 1
have K_pos : 0 < μ K := measure_pos_of_mem_nhds μ K1
have A : ∀ L : Set G, IsCompact L → ∃ g : G, Disjoint L (g • K) := fun L hL => exists_disjoint_smul_of_isCompact hL hK
choose! g hg using A
set L : ℕ → Set G := fun n => (fun T => T ∪ g T • K)^[n] K
have Lcompact : ∀ n, IsCompact (L n) := fun n ↦ by
induction n with
| zero => exact hK
| succ n IH =>
simp_rw [L, iterate_succ']
apply IsCompact.union IH (hK.smul (g (L n)))
have Lclosed : ∀ n, IsClosed (L n) := fun n ↦ by
induction n with
| zero => exact Kclosed
| succ n IH =>
simp_rw [L, iterate_succ']
apply IsClosed.union IH (Kclosed.smul (g (L n)))
have M : ∀ n, μ (L n) = (n + 1 : ℕ) * μ K := fun n ↦ by
induction n with
| zero => simp only [L, one_mul, Nat.cast_one, iterate_zero, id, Nat.zero_add]
| succ n IH =>
calc
μ (L (n + 1)) = μ (L n) + μ (g (L n) • K) :=
by
simp_rw [L, iterate_succ']
exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet
_ = (n + 1 + 1 : ℕ) * μ K := by simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]
have N : Tendsto (fun n => μ (L n)) atTop (𝓝 (∞ * μ K)) :=
by
simp_rw [M]
apply ENNReal.Tendsto.mul_const _ (Or.inl ENNReal.top_ne_zero)
exact ENNReal.tendsto_nat_nhds_top.comp (tendsto_add_atTop_nat _)
simp only [ENNReal.top_mul', K_pos.ne', if_false] at N
apply top_le_iff.1
exact le_of_tendsto' N fun n => measure_mono (subset_univ _)
