instance
MeasureTheory.Measure.instIsProbabilityMeasureForallPi_pFR
{ι : Type u_1}
{α : ι → Type u_2}
[Fintype ι]
[(i : ι) → MeasurableSpace (α i)]
(μ : (i : ι) → MeasureTheory.Measure (α i))
[∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
:
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) = ∏ i ∈ Finset.filter (fun (x : ι) => x ∈ t) Finset.univ, (μ 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) = ∏ i ∈ t, (μ 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 : ι)
: