integrableAtFilter_atBot_iff — Mathlib

English

MeasurableEmbedding.integrableAtFilter_iff_comap: For a measurable embedding e, IntegrableAtFilter f (l.map e) μ ↔ IntegrableAtFilter (f ∘ e) l (μ.comap e).

Русский

MeasurableEmbedding.integrableAtFilter_iff_comap: для меримого вложения e, IntegrableAtFilter(f, l.map e, μ) эквивалентно IntegrableAtFilter(f∘e, l, μ comap e).

LaTeX

$$$\\operatorname{IntegrableAtFilter}(f, \\operatorname{Filter.map}(e, l), \\mu) \\iff \\operatorname{IntegrableAtFilter}(f \\circ e, l, \\mu \\circ e^{-1}).$$$

Lean4

theorem integrableAtFilter_atBot_iff [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2] [Nonempty α] :
    IntegrableAtFilter f atBot μ ↔ ∃ a, IntegrableOn f (Iic a) μ :=
  by
  refine ⟨fun ⟨s, hs, hi⟩ ↦ ?_, fun ⟨a, ha⟩ ↦ ⟨Iic a, Iic_mem_atBot a, ha⟩⟩
  obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs
  exact ⟨t, hi.mono_set fun _ hx ↦ ht _ hx⟩

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