aemeasurable_of_aemeasurable_exp_mul

English

If aemeasurable exp(t f) with t ≠ 0, then f is aemeasurable.

Русский

Если a.e. измеримо exp(t f) при t ≠ 0, то f измеримо почти везде.

LaTeX

$$$$\\forall t\\neq 0:\\; \\text{AEMeasurable}(e^{t f}) \\Rightarrow \\text{AEMeasurable}(f).$$$$

Lean4

theorem aemeasurable_of_aemeasurable_exp_mul {t : ℝ} (ht : t ≠ 0) (hf : AEMeasurable (fun x ↦ exp (t * f x)) μ) :
    AEMeasurable f μ := by
  simpa only [mul_div_cancel_left₀ _ ht] using (aemeasurable_of_aemeasurable_exp hf).div (aemeasurable_const (b := t))

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