tilted_of_not_aemeasurable — Mathlib

English

If f is not AEMeasurable, then μ.tilted f = 0.

Русский

Если f не AE-измерима, то μ.tilted f = 0.

LaTeX

$$tilted_of_not_aemeasurable (hf : ¬AEMeasurable f μ) : μ.tilted f = 0$$

Lean4

@[simp]
theorem tilted_of_not_aemeasurable (hf : ¬AEMeasurable f μ) : μ.tilted f = 0 :=
  by
  refine tilted_of_not_integrable ?_
  suffices ¬AEMeasurable (fun x ↦ exp (f x)) μ by exact fun h ↦ this h.1.aemeasurable
  exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h)

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