aestronglyMeasurable_of_aestronglyMeasurable_trim

English

Characterizes AEStronglyMeasurable with density by relating to a scaled function under the density measure.

Русский

Характеризует AEStronglyMeasurable с плотностью через масштабированную функцию относительно меры плотности.

LaTeX

$$$$\\text{AEStronglyMeasurable}(g, \\mu.withDensity(f)) \\iff \\text{AEStronglyMeasurable}( (f)^{\\_} \\cdot g, \\mu ).$$$$

Lean4

theorem _root_.aestronglyMeasurable_of_aestronglyMeasurable_trim {α} {m m0 : MeasurableSpace α} {μ : Measure α}
    (hm : m ≤ m0) {f : α → β} (hf : AEStronglyMeasurable[m] f (μ.trim hm)) : AEStronglyMeasurable f μ :=
  ⟨hf.mk f, StronglyMeasurable.mono hf.stronglyMeasurable_mk hm, ae_eq_of_ae_eq_trim hf.ae_eq_mk⟩

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