English
For left-invariant μ' and ν' with nonzero and finite ν' s, the cross-weighted integrals satisfy μ's times ν't equals ν's times μ't.
Русский
При невырожденности и конечности ν'(s) выполняется равенство μ'(s) ν'(t) = ν'(s) μ'(t) для мер μ', ν'.
LaTeX
$$$\mu'(s) \cdot \nu'(t) = \nu'(s) \cdot \mu'(t)$$$
Lean4
/-- Any two nonzero left-invariant measures are absolutely continuous w.r.t. each other. -/
@[to_additive /-- Any two nonzero left-invariant measures are absolutely continuous w.r.t. each other. -/
]
theorem absolutelyContinuous_of_isMulLeftInvariant [IsMulLeftInvariant ν] (hν : ν ≠ 0) : μ ≪ ν :=
by
refine AbsolutelyContinuous.mk fun s sm hνs => ?_
have h1 := measure_mul_lintegral_eq μ ν sm 1 measurable_one
simp_rw [Pi.one_apply, lintegral_one, mul_one, (measure_mul_right_null ν _).mpr hνs, lintegral_zero,
mul_eq_zero (M₀ := ℝ≥0∞), measure_univ_eq_zero.not.mpr hν, or_false] at h1
exact h1
