[Merged by Bors] - feat(measure_theory/measurable_space): defining a measurable function on countably many pieces

[sgouezel]

Also, remove open_locale classical in this file and add decidability assumptions where needed. And add a few isolated useful lemmas.

---

[RemyDegenne]

Looks good!
bors d+

[RemyDegenne]

Could this be a measurability lemma? There are many hypothesis so the tactic is likely to be stuck after that, but at least it should suggest refine measurable.find _ _ _

[RemyDegenne]

This works:

/-- A piecewise function on countably many pieces is measurable if all the data is measurable. -/
@[measurability]
lemma measurable.find {m : measurable_space α}
  {f : ℕ → α → β} {p : ℕ → α → Prop} [∀ n, decidable_pred (p n)]
  (hf : ∀ n, measurable (f n)) (hp : ∀ n, measurable_set {x | p n x}) (h : ∀ x, ∃ n, p n x) :
  measurable (λ x, f (nat.find (h x)) x) :=
begin
  have : measurable (λ (p : α × ℕ), f p.2 p.1) := measurable_from_prod_encodable (λ n, hf n),
  exact this.comp (measurable.prod_mk measurable_id (measurable_find h hp)),
end

example {m : measurable_space α}
  {f : ℕ → α → β} {p : ℕ → α → Prop} [∀ n, decidable_pred (p n)]
  (hf : ∀ n, measurable (f n)) (hp : ∀ n, measurable_set {x | p n x}) (h : ∀ x, ∃ n, p n x) :
  measurable (λ x, f (nat.find (h x)) x) :=
by measurability

And if I omit hp in the example, it suggests Try this: refine measurable.find hf (λ (n : ℕ), _[n]) (λ (x : α), h x), which is not too bad.

[bors]

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests