English
Let μ, μ′ be left-invariant measures on a locally compact group G. If μ(s) ≠ ∞ and μ′(s) ≠ ∞ for some s, then μ′(s) = haarScalarFactor μ′ μ · μ(s).
Русский
Пусть μ и μ′ — лево-инвариантные меры на локально компактной группе G. Если существует множество s с μ(s) ≠ ∞ и μ′(s) ≠ ∞, то μ′(s) = haarScalarFactor μ′ μ · μ(s).
LaTeX
$$$\\forall G \\, [\\text{LocallyCompactSpace } G] \\, (μ' : \\mathrm{Measure}(G)) \\, (μ : \\mathrm{Measure}(G)) \\, [\\text{IsHaarMeasure } μ] \\, [\\text{IsFiniteMeasureOnCompacts } μ'] \\, [\\text{IsMulLeftInvariant } μ'] \\, \\forall s : Set G, μ s \\neq \\infty \\, \\land \\, μ' s \\neq \\infty \\Rightarrow μ' s = haarScalarFactor μ' μ · μ s$$
Lean4
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite on
compacts and inner regular for finite measure sets with respect to compact sets,
they coincide in the following sense: they give the same value to finite measure sets,
up to a multiplicative constant. -/
@[to_additive]
theorem measure_isMulLeftInvariant_eq_smul_of_ne_top [LocallyCompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
[IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] [InnerRegularCompactLTTop μ] [InnerRegularCompactLTTop μ']
{s : Set G} (hs : μ s ≠ ∞) (h's : μ' s ≠ ∞) : μ' s = haarScalarFactor μ' μ • μ s := by
/- We know that the measures integrate in the same way continuous compactly supported functions,
up to the factor `c = haarScalarFactor μ' μ`. -/
let c := haarScalarFactor μ' μ
have B : ∀ s, MeasurableSet s → μ s < ∞ → μ' s < ∞ → μ' s = (c • μ) s :=
by
intro s s_meas hs h's
have : (c • μ) s ≠ ∞ := by simp [ENNReal.mul_eq_top, hs.ne]
rw [s_meas.measure_eq_iSup_isCompact_of_ne_top h's.ne, s_meas.measure_eq_iSup_isCompact_of_ne_top this]
congr! 4 with K _Ks K_comp
exact measure_isMulInvariant_eq_smul_of_isCompact_closure μ' μ K_comp.closure
let t := toMeasurable μ' s ∩ toMeasurable μ s
have st : s ⊆ t := subset_inter (subset_toMeasurable μ' s) (subset_toMeasurable μ s)
have mu'_t : μ' t = μ' s := by
apply le_antisymm
· exact (measure_mono inter_subset_left).trans (measure_toMeasurable s).le
· exact measure_mono st
have mu_t : μ t = μ s := by
apply le_antisymm
· exact (measure_mono inter_subset_right).trans (measure_toMeasurable s).le
· exact measure_mono st
simp only [← mu'_t, ← mu_t, nnreal_smul_coe_apply]
apply B
· exact (measurableSet_toMeasurable _ _).inter (measurableSet_toMeasurable _ _)
· exact mu_t.le.trans_lt hs.lt_top
· exact mu'_t.le.trans_lt h's.lt_top
