absolutelyContinuous_tilted — Mathlib

English

If hf expresses Integrable exp(f), then μ ≪ μ.tilted f, i.e., tilting preserves absolute continuity in the other direction as well.

Русский

Если exp(f) интегрируема, то μ \u226a μ.tilted f, т.е. тильтование сохраняет отношение абсолютной непрерывности в обратную сторону.

LaTeX

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

Lean4

theorem absolutelyContinuous_tilted (hf : Integrable (fun x ↦ exp (f x)) μ) : μ ≪ μ.tilted f := by
  cases eq_zero_or_neZero μ with
  | inl h => simp only [h, tilted_zero_measure]; exact fun _ _ ↦ by simp
  | inr h0 =>
    refine withDensity_absolutelyContinuous' ?_ ?_
    · exact (hf.1.aemeasurable.div_const _).ennreal_ofReal
    · filter_upwards
      simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
      exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

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