English
Left-invariant measures μ', ν' satisfy that μ' equals the smoothed scalar multiple of ν' by the ratio μ'(s)/ν'(s).
Русский
Левые инвариантные меры μ', ν' равны друг другу до скалярного множителя, равного отношению μ'(s) к ν'(s).
LaTeX
$$$\mu' = \left( \dfrac{\mu'(s)}{\nu'(s)} \right) \cdot \nu'$$$
Lean4
@[to_additive]
theorem measure_mul_measure_eq (s t : Set G) (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ∞) : μ' s * ν' t = ν' s * μ' t :=
by
wlog hs : MeasurableSet s generalizing s
· rcases exists_measurable_superset₂ μ' ν' s with ⟨s', -, hm, hμ, hν⟩
rw [← hμ, ← hν, this s' _ _ hm] <;> rwa [hν]
wlog ht : MeasurableSet t generalizing t
· rcases exists_measurable_superset₂ μ' ν' t with ⟨t', -, hm, hμ, hν⟩
rw [← hμ, ← hν, this _ hm]
have h1 := measure_lintegral_div_measure ν' ν' hs h2s h3s (t.indicator fun _ => 1) (measurable_const.indicator ht)
have h2 := measure_lintegral_div_measure μ' ν' hs h2s h3s (t.indicator fun _ => 1) (measurable_const.indicator ht)
rw [lintegral_indicator ht, setLIntegral_one] at h1 h2
rw [← h1, mul_left_comm, h2]
