measurable embedding

Stream: maths

[Yury G. Kudryashov]

I'm going to introduce

structure measurable_embedding {α β : Type*} [measurable_space α] [measurable_space β] (f : α → β) :
  Prop :=
(injective : injective f)
(measurable : measurable f)
(measurable_set_image' : ∀ ⦃s⦄, measurable_set s → measurable_set (f '' s))

[Yury G. Kudryashov]

Currently we have separate lemmas about closed_embeddings and measurable_equivs.

[Yury G. Kudryashov]

With this definition we can generalize all these lemmas to measurable_embeddings.

[Yury G. Kudryashov]

(an embedding is a measurable_embedding if it has a measurable range, so any closed embedding is a measurable embedding)

[Yury G. Kudryashov]

Any objections/comments?

[Yakov Pechersky]

Would it make sense to extend "embedding"?

[Johan Commelin]

That bundles the function, right?

[Yakov Pechersky]

Yes

[Yakov Pechersky]

I don't know the measure part of the library, how often one needs solely props or works with families of measurable functions.

[Yury G. Kudryashov]

An embedding says something about topology, so I don't want to extend it.

[Yury G. Kudryashov]

I don't want to bundle the function because I'm not going to make statements about the space of all measurable embeddings (see also docs#embedding, docs#closed_embedding, docs#open_embedding).

[Yury G. Kudryashov]

With a predicate we can do rw [hf.some_lemma] without moving to bundled functions first.

[Yury G. Kudryashov]

Right now I have theory about measurable_embeddings up to

/-- If `g : α → β` is a measurable embedding and `f : β → ℝ≥0∞` is any function (not necessarily
measurable), then `∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ`. Compare with `lintegral_map` wich
applies to any measurable `g : α → β` but requires that `f` is measurable as well. -/
lemma lintegral_map_embedding [measurable_space β] (f : β → ℝ≥0∞) {g : α → β}
  (hg : measurable_embedding g) :
  ∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ :=

[Yakov Pechersky]

Sorry I wasn't clear, I meant docs#function.embedding

[Yaël Dillies]

Also, should stuff in topology be disambiguated? There's docs#embedding, docs#locally_finite... I assume those names are historical artifacts because not much was here to concurrence them back when they got defined, right?

[Yury G. Kudryashov]

function.embedding has bundled to_fun, and I want to have a predicate like docs#embedding.