tilted_absolutelyContinuous — Mathlib

English

Tilting by f yields a measure absolutely continuous with respect to μ, i.e., μ.tilted f ≪ μ, provided exp(f) is μ-integrable.

Русский

Тильтовая мера по f абсолютно непрерывна по отношению к μ, если exp(f) интегрируема по μ.

LaTeX

$$$$ \\mu^{\\mathrm{tilted}} f \\ll \\mu. $$$$

Lean4

theorem tilted_absolutelyContinuous (μ : Measure α) (f : α → ℝ) : μ.tilted f ≪ μ :=
  withDensity_absolutelyContinuous _ _

Похожие утверждения