smulInvariantMeasure_tfae — Mathlib

English

Equivalence of several formulations of SMul invariance: μ is SMulInvariant, preimage invariance, image invariance, and measure-preserving properties for all actions and maps.

Русский

Эквивалентность нескольких формулировок инвариантности по отношению к группе: μ инвариантна, предобразная и образная инвариантности, свойства сохранения меры для всех отображений.

LaTeX

$$$\\text{List.TFAE}([\\text{SMulInvariantMeasure } G α μ, \\forall c,s(MeasurableSet s\\to μ((c•·)^{-1}s)=μ s), \\forall c,s(MeasurableSet s\\to μ(c·s)=μ s), \\forall c,s μ((c•·)^{-1}s)=μ s, \\forall c μ((c•·)^{-1}·)=μ, ∀ c: G, \\operatorname{map}(c•·) μ = μ, ∀ c: G, \\text{MeasurePreserving} (c•·) μ μ])$$$

Lean4

/-- Equivalent definitions of a measure invariant under a multiplicative action of a group.

- 0: `SMulInvariantMeasure G α μ`;

- 1: for every `c : G` and a measurable set `s`, the measure of the preimage of `s` under scalar
     multiplication by `c` is equal to the measure of `s`;

- 2: for every `c : G` and a measurable set `s`, the measure of the image `c • s` of `s` under
     scalar multiplication by `c` is equal to the measure of `s`;

- 3, 4: properties 2, 3 for any set, including non-measurable ones;

- 5: for any `c : G`, scalar multiplication by `c` maps `μ` to `μ`;

- 6: for any `c : G`, scalar multiplication by `c` is a measure-preserving map. -/
@[to_additive]
theorem smulInvariantMeasure_tfae :
    List.TFAE
      [SMulInvariantMeasure G α μ, ∀ (c : G) (s), MeasurableSet s → μ ((c • ·) ⁻¹' s) = μ s,
        ∀ (c : G) (s), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s), μ ((c • ·) ⁻¹' s) = μ s,
        ∀ (c : G) (s), μ (c • s) = μ s, ∀ c : G, Measure.map (c • ·) μ = μ, ∀ c : G, MeasurePreserving (c • ·) μ μ] :=
  by
  tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
  tfae_have 1 → 6 := fun h c => (measurePreserving_smul c μ).map_eq
  tfae_have 6 → 7 := fun H c => ⟨measurable_const_smul c, H c⟩
  tfae_have 7 → 4 := fun H c => (H c).measure_preimage_emb (measurableEmbedding_const_smul c)
  tfae_have 4 → 5
    | H, c, s => by
      rw [← preimage_smul_inv]
      apply H
  tfae_have 5 → 3 := fun H c s _ => H c s
  tfae_have 3 → 2
    | H, c, s, hs => by
      rw [preimage_smul]
      exact H c⁻¹ s hs
  tfae_finish

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