measure_isMulInvariant_eq_smul_of_isCompact_closure

English

Uniqueness of Haar measures on compact groups: two Haar measures coincide up to a multiplicative factor.

Русский

Уникальность мер Хаара на компактной группе: две меры Хаара совпадают до множителя.

LaTeX

$$$$ μ' = haarScalarFactor μ' μ \\cdot μ $$$$

Lean4

/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite on compacts, they coincide in the following
sense: they give the same value to sets with compact closure, up to the multiplicative
constant `haarScalarFactor μ' μ`. -/
@[to_additive measure_isAddInvariant_eq_smul_of_isCompact_closure /-- **Uniqueness of left-invariant measures**:
    Given two left-invariant measures which are finite on compacts, they coincide in the following
    sense: they give the same value to sets with compact closure, up to the multiplicative
    constant `addHaarScalarFactor μ' μ`. -/
    ]
theorem measure_isMulInvariant_eq_smul_of_isCompact_closure [LocallyCompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
    [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] {s : Set G} (h's : IsCompact (closure s)) :
    μ' s = haarScalarFactor μ' μ • μ s := by
  let ν := haarScalarFactor μ' μ • μ
  apply le_antisymm
  ·
    calc
      μ' s ≤ μ' ((toMeasurable ν s) ∩ (closure s)) :=
        measure_mono <| subset_inter (subset_toMeasurable ν s) subset_closure
      _ = ν ((toMeasurable ν s) ∩ (closure s)) :=
        by
        apply measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet _ _ _ _
        · exact (measurableSet_toMeasurable ν s).inter isClosed_closure.measurableSet
        · exact h's.closure_of_subset inter_subset_right
      _ ≤ ν (toMeasurable ν s) := (measure_mono inter_subset_left)
      _ = ν s := measure_toMeasurable s
  ·
    calc
      ν s ≤ ν ((toMeasurable μ' s) ∩ (closure s)) :=
        measure_mono <| subset_inter (subset_toMeasurable μ' s) subset_closure
      _ = μ' ((toMeasurable μ' s) ∩ (closure s)) :=
        by
        apply (measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet _ _ _ _).symm
        · exact (measurableSet_toMeasurable μ' s).inter isClosed_closure.measurableSet
        · exact h's.closure_of_subset inter_subset_right
      _ ≤ μ' (toMeasurable μ' s) := (measure_mono inter_subset_left)
      _ = μ' s := measure_toMeasurable s

Похожие утверждения