English
If e is a measurable embedding, then integrability at filter is preserved by composition and by comap: IntegrableAtFilter f (l.map e) μ ↔ IntegrableAtFilter (f ∘ e) l (μ.comap e).
Русский
Для меримого вложения e сохраняется интегрируемость при композиции и комапе: IntegrableAtFilter f (l.map e) μ ⇔ IntegrableAtFilter (f ∘ e) l (μ.comap e).
LaTeX
$$$\\operatorname{IntegrableAtFilter}(f, (l\\mapsto e), \\mu) \\iff \\operatorname{IntegrableAtFilter}(f\\circ e, l, \\mu\\circ e^{-1}).$$$
Lean4
theorem _root_.MeasurableEmbedding.integrableAtFilter_iff_comap [MeasurableSpace β] {e : α → β}
(he : MeasurableEmbedding e) {f : β → ε} {μ : Measure β} :
IntegrableAtFilter f (l.map e) μ ↔ IntegrableAtFilter (f ∘ e) l (μ.comap e) :=
by
simp_rw [← he.integrableAtFilter_map_iff, IntegrableAtFilter, he.map_comap]
constructor <;> rintro ⟨s, hs, int⟩
· exact ⟨s, hs, int.mono_measure <| μ.restrict_le_self⟩
· exact ⟨_, inter_mem hs range_mem_map, int.inter_of_restrict⟩
