measure_preimage_smul_of_nullMeasurableSet

English

As above, equality holds for preimage under the action when s is null-measurable.

Русский

Как выше, равенство меры сохраняется при предобразе через действие, если s нуль-мезируемо.

LaTeX

$$$\text{NullMeasurableSet}(s,μ) \Rightarrow ∀ c, μ((c\cdot)^{-1} s) = μ(s)$$$

Lean4

@[to_additive]
theorem measure_preimage_smul_of_nullMeasurableSet (hs : NullMeasurableSet s μ) (c : G) : μ ((c • ·) ⁻¹' s) = μ s :=
  by
  rw [← measure_toMeasurable s, ← SMulInvariantMeasure.measure_preimage_smul c (measurableSet_toMeasurable μ s)]
  exact measure_congr (tendsto_smul_ae μ c hs.toMeasurable_ae_eq) |>.symm

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