English
Under sigma-finite μ and ν, for a measurable f, one has an equality of llr between μ.tilted f and ν, expressed in terms of llr μ ν and f.
Русский
При сигма-ограниченных μ и ν и измеримой функции f существует равенство llr(μ.tilted f, ν) в терминах llr(μ, ν) и f.
LaTeX
$$$\\mathrm{llr}(\\mu\\tilted f, \\nu) =_{\\mu\\text{-a.e.}} f - \\log\\left(\\int e^{f} d\\mu\\right) + \\mathrm{llr}(\\mu, \\nu)$$$
Lean4
/-- The pushforward of a measure as a linear map. It is defined to be `0` if `f` is not
a measurable function. -/
noncomputable def mapₗ [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : Measure α →ₗ[ℝ≥0∞] Measure β :=
if hf : Measurable f then
liftLinear (OuterMeasure.map f) fun μ _s hs t => le_toOuterMeasure_caratheodory μ _ (hf hs) (f ⁻¹' t)
else 0
