English
If e: α → β is a measurable embedding and f: β → ε, then integrability along a filter is preserved by pullback/pushforward: IntegrableAtFilter f (l.map e) μ ⇔ IntegrableAtFilter (f ∘ e) l μ.
Русский
Пусть e: α → β — меримо вложение, f: β → ε. Тогда интегрируемость на фильтре сохраняется при композиции: IntegrableAtFilter f (l.map e) μ ⇔ IntegrableAtFilter (f ∘ e) l μ.
LaTeX
$$$\\text{If } e: \\alpha \\to \\beta \\text{ is a MeasurableEmbedding and } f: \\beta \\to \\varepsilon, \\\\ \\operatorname{IntegrableAtFilter}(f, l\\!\\map e, \\mu) \\;\\Longleftrightarrow\\; \\operatorname{IntegrableAtFilter}(f\\circ e, l, \\mu).$$$
Lean4
theorem _root_.MeasurableEmbedding.integrableAtFilter_map_iff [MeasurableSpace β] {e : α → β}
(he : MeasurableEmbedding e) {f : β → ε} :
IntegrableAtFilter f (l.map e) (μ.map e) ↔ IntegrableAtFilter (f ∘ e) l μ :=
by
simp_rw [IntegrableAtFilter, he.integrableOn_map_iff]
constructor <;> rintro ⟨s, hs⟩
· exact ⟨_, hs⟩
· exact ⟨e '' s, by rwa [mem_map, he.injective.preimage_image]⟩
