Measurability of functions on a sigma type

A function on Σ a, β a is measurable as soon as each of its restrictions f ∘ Sigma.mk a is. We also record measurability facts about the first projection of Σ n : ℕ, β n.

theorem measurable_sigma_mk {α : Type u_1} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] (a : α) : Measurable (Sigma.mk a)

theorem measurable_sigma_of_measurable_comp_mk {α : Type u_1} {γ : Type u_2} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] [MeasurableSpace γ] {f : (a : α) × β a → γ} (h : ∀ (a : α), Measurable (f ∘ Sigma.mk a)) : Measurable f

A function on a sigma type is measurable if all its restrictions to the fibers are.

theorem measurableSet_sigma_iff {α : Type u_1} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] {s : Set ((a : α) × β a)} : MeasurableSet s ↔ ∀ (a : α), MeasurableSet (Sigma.mk a ⁻¹' s)

A set in a sigma type is measurable iff its trace on every fiber is.

theorem measurable_sigma_iff {α : Type u_1} {γ : Type u_2} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] [MeasurableSpace γ] {f : (a : α) × β a → γ} : Measurable f ↔ ∀ (a : α), Measurable (f ∘ Sigma.mk a)

theorem measurable_sigma_fst {α : Type u_1} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] [MeasurableSpace α] : Measurable Sigma.fst

The first projection of a sigma type is measurable (it is constant on every fiber).

theorem Measurable.sigmaMk {α : Type u_1} {γ : Type u_2} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] [MeasurableSpace γ] [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] {n : γ → α} (hn : Measurable n) {f : (a : α) → γ → β a} (hf : ∀ (a : α), Measurable (f a)) : Measurable fun (x : γ) => ⟨n x, f (n x) x⟩

x ↦ ⟨n x, f (n x) x⟩ is measurable when the index n x ranges over a countable type with measurable singletons and each f i is measurable.

theorem measurableEmbedding_sigma_mk {α : Type u_1} {β : α → Type u_3} [(a : α) → MeasurableSpace (β a)] (a : α) : MeasurableEmbedding (Sigma.mk a)

Sigma.mk a is a measurable embedding.

theorem measurableSet_sigma_fst_le {X : ℕ → Type u_4} [(n : ℕ) → MeasurableSpace (X n)] (M : ℕ) : MeasurableSet {x : (n : ℕ) × X n | x.fst ≤ M}

The set of elements of Σ n : ℕ, X n with first component at most M is measurable.

theorem measurableSet_sigma_fst_lt {X : ℕ → Type u_4} [(n : ℕ) → MeasurableSpace (X n)] (M : ℕ) : MeasurableSet {x : (n : ℕ) × X n | x.fst < M}

The set of elements of Σ n : ℕ, X n with first component less than M is measurable.

theorem MeasureTheory.Measure.map_sigmaMk_succ_apply_fst_le {X : ℕ → Type u_4} [(n : ℕ) → MeasurableSpace (X n)] {M : ℕ} (μ : Measure (X (M + 1))) : (map (Sigma.mk (M + 1)) μ) {x : (n : ℕ) × X n | x.fst ≤ M} = 0

The image of a measure on X (M + 1) by Sigma.mk (M + 1) gives measure zero to the elements of Σ n : ℕ, X n with first component at most M.