English
Scaling commutes with comap: comap f (c • μ) = c • comap f μ for c ∈ ℝ≥0∞, with case distinctions on c and appropriate measurability hypotheses.
Русский
Умножение меры на скаляр и операция comap коммутируют: comap f (c • μ) = c • comap f μ при надлежащих предположениях о меры и скаляре.
LaTeX
$$$\\mathrm{comap}\\ f (c \\cdot \\mu) = c \\cdot \\mathrm{comap}\\ f\\, \\mu$$$
Lean4
theorem comap_smul {μ : Measure β} (c : ℝ≥0∞) : comap f (c • μ) = c • comap f μ :=
by
obtain rfl | hc := eq_or_ne c 0
· simp
by_cases h : Function.Injective f ∧ ∀ s : Set α, MeasurableSet s → NullMeasurableSet (f '' s) μ
· ext s hs
rw [comap_apply₀ f _ h.1 _ hs.nullMeasurableSet, smul_apply, smul_apply,
comap_apply₀ f μ h.1 h.2 hs.nullMeasurableSet]
simpa [nullMeasurableSet_smul_measure_iff hc] using h.2
· have h' : ¬(Function.Injective f ∧ ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)) := by
simpa [nullMeasurableSet_smul_measure_iff hc] using h
simp [comap_undef, h, h']
