Measurability lemmas

theorem MeasureTheory.ae_eq_set_iff {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} {s t : Set α} : s =ᶠ[ae μ] t ↔ ∀ᵐ (a : α) ∂μ, a ∈ s ↔ a ∈ t

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.MeasurableSet.imp {α : Type u_1} {mα : MeasurableSpace α} {p q : α → Prop} (hs : MeasurableSet {x : α | p x}) (ht : MeasurableSet {x : α | q x}) : MeasurableSet {x : α | p x → q x}

theorem MeasureTheory.MeasurableSet.iff {α : Type u_1} {mα : MeasurableSpace α} {p q : α → Prop} (hs : MeasurableSet {x : α | p x}) (ht : MeasurableSet {x : α | q x}) : MeasurableSet {x : α | p x ↔ q x}

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.Measure.trim_comap_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {X : α → β} (hX : Measurable X) {s : Set β} (hs : MeasurableSet s) : (μ.trim ⋯) (X ⁻¹' s) = (map X μ) s

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