theorem
MeasureTheory.Sigma.measurable_mk
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → MeasurableSpace (P i)]
(i : I)
:
Measurable fun (x : P i) => ⟨i, x⟩
theorem
MeasureTheory.Sigma.measurable_mk'
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → MeasurableSpace (P i)]
{A : Type u_3}
[MeasurableSpace A]
(i : I)
{f : A → P i}
(hf : Measurable f)
:
Measurable fun (x : A) => ⟨i, f x⟩
theorem
MeasureTheory.Sigma.measurable_elim
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → MeasurableSpace (P i)]
{A : Type u_3}
[MeasurableSpace A]
{f : Sigma P → A}
(hf : ∀ (i : I), Measurable fun (x : P i) => f ⟨i, x⟩)
:
theorem
MeasureTheory.Sigma.measurable_elim'
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → MeasurableSpace (P i)]
{A : Type u_3}
[MeasurableSpace A]
{f : (i : I) → P i → A}
(hf : ∀ (i : I), Measurable (f i))
{g : A → (i : I) × P i}
(hg : Measurable g)
:
Measurable fun (x : A) => f (g x).fst (g x).snd
@[simp]
theorem
MeasureTheory.Sigma.measurable_fst
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → MeasurableSpace (P i)]
[MeasurableSpace I]
:
theorem
MeasureTheory.Sigma.measurable_cast
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → MeasurableSpace (P i)]
{A : Type u_3}
[MeasurableSpace A]
(ix : A → I)
(i : I)
(p : ∀ (x : A), ix x = i)
(f : (x : A) → P (ix x))
(hf : Measurable fun (x : A) => ⟨ix x, f x⟩)
:
Measurable fun (x : A) => cast ⋯ (f x)
theorem
MeasureTheory.Sigma.measurable_eq_rec
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → MeasurableSpace (P i)]
{A : Type u_3}
[MeasurableSpace A]
(ix : A → I)
(i : I)
(p : ∀ (x : A), ix x = i)
(f : (x : A) → P (ix x))
(hf : Measurable fun (x : A) => ⟨ix x, f x⟩)
:
Measurable fun (x : A) => ⋯ ▸ f x
theorem
MeasureTheory.Sigma.measurable_distrib
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → MeasurableSpace (P i)]
{A : Type u_3}
[MeasurableSpace A]
[Countable I]
:
theorem
MeasureTheory.Sigma.measurable_distrib'
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → MeasurableSpace (P i)]
{A : Type u_3}
[MeasurableSpace A]
{B : Type u}
[MeasurableSpace B]
[Countable I]
{f : A × Sigma P → B}
(hf : Measurable fun (x : (i : I) × A × P i) => f (x.snd.1, ⟨x.fst, x.snd.2⟩))
:
instance
MeasureTheory.Sigma.instDiscreteMeasurableSpaceSigma_quasiBorelSpaces
{I : Type u_1}
{P : I → Type u_2}
[(i : I) → MeasurableSpace (P i)]
[∀ (i : I), DiscreteMeasurableSpace (P i)]
: