English
If the injectivity and measurability condition fails, the comapped measure is zero.
Русский
Если не выполняется условие инъективности и измеримости, полученная мера равна нулю.
LaTeX
$$$\text{If } \neg(\text{Injective } f \land \forall s, \text{MeasurableSet}(s) \rightarrow \text{NullMeasurableSet}(f''s, μ))\Rightarrow \operatorname{comap} f μ = 0$$$
Lean4
/-- Pullback of a `Measure` as a linear map. If `f` sends each measurable set to a measurable
set, then for each measurable set `s` we have `comapₗ f μ s = μ (f '' s)`.
Note that if `f` is not injective, this definition assigns `Set.univ` measure zero.
If the linearity is not needed, please use `comap` instead, which works for a larger class of
functions. `comapₗ` is an auxiliary definition and most lemmas deal with comap. -/
def comapₗ [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : Measure β →ₗ[ℝ≥0∞] Measure α :=
if hf : Injective f ∧ ∀ s, MeasurableSet s → MeasurableSet (f '' s) then
liftLinear (OuterMeasure.comap f) fun μ s hs t =>
by
simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1]
apply le_toOuterMeasure_caratheodory
exact hf.2 s hs
else 0
