instance MeasureTheory.Measure.instIsProbabilityMeasureForallPi_pFR {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] : MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.pi μ)

Equations

• ⋯ = ⋯

@[simp]

theorem MeasureTheory.Measure.pi_pi_set {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (t : Set ι) [DecidablePred fun (x : ι) => x ∈ t] (s : (i : ι) → Set (α i)) : (MeasureTheory.Measure.pi μ) (t.pi s) = (Finset.filter (fun (x : ι) => x ∈ t) Finset.univ).prod fun (i : ι) => (μ i) (s i)

@[simp]

theorem MeasureTheory.Measure.pi_pi_finset {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (t : Finset ι) (s : (i : ι) → Set (α i)) : (MeasureTheory.Measure.pi μ) ((↑t).pi s) = t.prod fun (i : ι) => (μ i) (s i)

@[simp]

theorem MeasureTheory.Measure.pi_eval_preimage {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (i : ι) (s : Set (α i)) : (MeasureTheory.Measure.pi μ) (Function.eval i ⁻¹' s) = (μ i) s

theorem MeasureTheory.Measure.map_eval_pi {ι : Type u_1} {α : ι → Type u_2} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (i : ι) : MeasureTheory.Measure.map (Function.eval i) (MeasureTheory.Measure.pi μ) = μ i