Measurability lemmas #
theorem
MeasureTheory.measurable_comp_comap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
(f : α → β)
{g : β → γ}
(hg : Measurable g)
:
Measurable (g ∘ f)
theorem
MeasureTheory.Measurable.coe_nat_enat
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℕ}
(hf : Measurable f)
:
Measurable fun (a : α) => ↑(f a)
theorem
MeasureTheory.Measurable.toNat
{α : Type u_1}
{mα : MeasurableSpace α}
{f : α → ℕ∞}
(hf : Measurable f)
:
Measurable fun (a : α) => (f a).toNat
theorem
MeasureTheory.measurable_sum_range_of_le
{α : Type u_1}
{mα : MeasurableSpace α}
{f : ℕ → α → ℝ}
{g : α → ℕ}
{n : ℕ}
(hg_le : ∀ (a : α), g a ≤ n)
(hf : ∀ (i : ℕ), Measurable (f i))
(hg : Measurable g)
:
Measurable fun (a : α) => ∑ i ∈ Finset.range (g a), f i a
theorem
MeasureTheory.measurable_sum_Icc_of_le
{α : Type u_1}
{mα : MeasurableSpace α}
{f : ℕ → α → ℝ}
{g : α → ℕ}
{n : ℕ}
(hg_le : ∀ (a : α), g a ≤ n)
(hf : ∀ (i : ℕ), Measurable (f i))
(hg : Measurable g)
:
Measurable fun (a : α) => ∑ i ∈ Finset.Icc 1 (g a), f i a