absolutelyContinuous_map_div_left

English

The measure μ is absolutely continuous with respect to the pushforward by left-division by g.

Русский

Мера μ абсолютно непрерывна по отношению к отображению, отправляющему h ↦ g/h.

LaTeX

$$$\mu \ll \operatorname{map}(h \mapsto g/h)\mu$$$

Lean4

@[to_additive]
theorem absolutelyContinuous_map_div_left (g : G) : μ ≪ map (fun h => g / h) μ :=
  by
  simp_rw [div_eq_mul_inv]
  have := map_map (μ := μ) (measurable_const_mul g) measurable_inv
  simp only [Function.comp_def] at this
  rw [← this]
  conv_lhs => rw [← map_mul_left_eq_self μ g]
  exact (absolutelyContinuous_inv μ).map (measurable_const_mul g)

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