English
If μ is left-invariant and assigns positive mass to a compact set K, then μ has positive mass on every nonempty open set.
Русский
Если μ лево-инвариантна и μ(K) > 0 для некоторого компактного K, то μ имеет положительную массу на всяком ненулевом открытом множестве.
LaTeX
$$$\forall K\, (\text{IsCompact}(K) \land \mu(K) \neq 0) \Rightarrow \text{IsOpenPosMeasure}(\mu)$$$
Lean4
/-- If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to
any open set. -/
@[to_additive /-- If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to
any open set. -/
]
theorem isOpenPosMeasure_of_mulLeftInvariant_of_compact (K : Set G) (hK : IsCompact K) (h : μ K ≠ 0) :
IsOpenPosMeasure μ := by
refine ⟨fun U hU hne => ?_⟩
contrapose! h
rw [← nonpos_iff_eq_zero]
rw [← hU.interior_eq] at hne
obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U :=
compact_covered_by_mul_left_translates hK hne
calc
μ K ≤ μ (⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U) := measure_mono hKt
_ ≤ ∑ g ∈ t, μ ((fun h : G => g * h) ⁻¹' U) := (measure_biUnion_finset_le _ _)
_ = 0 := by simp [measure_preimage_mul, h]
