Indexed product measures

In this file we define and prove properties about finite products of measures (and at some point, countable products of measures).

Main definition

• MeasureTheory.Measure.pi: The product of finitely many σ-finite measures. Given μ : (i : ι) → Measure (α i) for [Fintype ι] it has type Measure ((i : ι) → α i).

To apply Fubini's theorem or Tonelli's theorem along some subset, we recommend using the marginal construction MeasureTheory.lmarginal and (todo) MeasureTheory.marginal. This allows you to apply these theorems without any bookkeeping with measurable equivalences.

Implementation Notes

We define MeasureTheory.OuterMeasure.pi, the product of finitely many outer measures, as the maximal outer measure n with the property that n (pi univ s) ≤ ∏ i, m i (s i), where pi univ s is the product of the sets {s i | i : ι}.

We then show that this induces a product of measures, called MeasureTheory.Measure.pi. For a collection of σ-finite measures μ and a collection of measurable sets s we show that Measure.pi μ (pi univ s) = ∏ i, m i (s i). To do this, we follow the following steps:

• We know that there is some ordering on ι, given by an element of [Countable ι].
• Using this, we have an equivalence MeasurableEquiv.piMeasurableEquivTProd between ∀ i, α i and an iterated product of α i, called List.tprod α l for some list l.
• On this iterated product we can easily define a product measure MeasureTheory.Measure.tprod by iterating MeasureTheory.Measure.prod
• Using the previous two steps we construct MeasureTheory.Measure.pi' on (i : ι) → α i for countable ι.
• We know that MeasureTheory.Measure.pi' sends products of sets to products of measures, and since MeasureTheory.Measure.pi is the maximal such measure (or at least, it comes from an outer measure which is the maximal such outer measure), we get the same rule for MeasureTheory.Measure.pi.

Tags

finitary product measure

noncomputable def MeasureTheory.piPremeasure {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] (m : (i : ι) → OuterMeasure (α i)) (s : Set ((i : ι) → α i)) : ENNReal

An upper bound for the measure in a finite product space. It is defined by taking the image of the set under all projections, and taking the product of the measures of these images. For measurable boxes it is equal to the correct measure.

Equations

• MeasureTheory.piPremeasure m s = ∏ i : ι, (m i) (Function.eval i '' s)

theorem MeasureTheory.piPremeasure_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] {m : (i : ι) → OuterMeasure (α i)} {s : (i : ι) → Set (α i)} (hs : (Set.univ.pi s).Nonempty) : piPremeasure m (Set.univ.pi s) = ∏ i : ι, (m i) (s i)

theorem MeasureTheory.piPremeasure_pi' {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] {m : (i : ι) → OuterMeasure (α i)} {s : (i : ι) → Set (α i)} : piPremeasure m (Set.univ.pi s) = ∏ i : ι, (m i) (s i)

theorem MeasureTheory.piPremeasure_pi_mono {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] {m : (i : ι) → OuterMeasure (α i)} {s t : Set ((i : ι) → α i)} (h : s ⊆ t) : piPremeasure m s ≤ piPremeasure m t

theorem MeasureTheory.piPremeasure_pi_eval {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] {m : (i : ι) → OuterMeasure (α i)} {s : Set ((i : ι) → α i)} : piPremeasure m (Set.univ.pi fun (i : ι) => Function.eval i '' s) = piPremeasure m s

noncomputable def MeasureTheory.OuterMeasure.pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] (m : (i : ι) → OuterMeasure (α i)) : OuterMeasure ((i : ι) → α i)

OuterMeasure.pi m is the finite product of the outer measures {m i | i : ι}. It is defined to be the maximal outer measure n with the property that n (pi univ s) ≤ ∏ i, m i (s i), where pi univ s is the product of the sets {s i | i : ι}.

Equations

• MeasureTheory.OuterMeasure.pi m = MeasureTheory.OuterMeasure.boundedBy (MeasureTheory.piPremeasure m)

theorem MeasureTheory.OuterMeasure.pi_pi_le {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] (m : (i : ι) → OuterMeasure (α i)) (s : (i : ι) → Set (α i)) : (OuterMeasure.pi m) (Set.univ.pi s) ≤ ∏ i : ι, (m i) (s i)

theorem MeasureTheory.OuterMeasure.le_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] {m : (i : ι) → OuterMeasure (α i)} {n : OuterMeasure ((i : ι) → α i)} : n ≤ OuterMeasure.pi m ↔ ∀ (s : (i : ι) → Set (α i)), (Set.univ.pi s).Nonempty → n (Set.univ.pi s) ≤ ∏ i : ι, (m i) (s i)

noncomputable def MeasureTheory.Measure.tprod {δ : Type u_4} {X : δ → Type u_5} [(i : δ) → MeasurableSpace (X i)] (l : List δ) (μ : (i : δ) → Measure (X i)) : Measure (List.TProd X l)

A product of measures in tprod α l.

Equations

• MeasureTheory.Measure.tprod l μ = List.rec (MeasureTheory.Measure.dirac PUnit.unit) (fun (i : δ) (l : List δ) (ih : MeasureTheory.Measure (List.TProd X l)) => (μ i).prod ih) l

@[simp]

theorem MeasureTheory.Measure.tprod_nil {δ : Type u_4} {X : δ → Type u_5} [(i : δ) → MeasurableSpace (X i)] (μ : (i : δ) → Measure (X i)) : Measure.tprod [] μ = dirac PUnit.unit

@[simp]

theorem MeasureTheory.Measure.tprod_cons {δ : Type u_4} {X : δ → Type u_5} [(i : δ) → MeasurableSpace (X i)] (i : δ) (l : List δ) (μ : (i : δ) → Measure (X i)) : Measure.tprod (i :: l) μ = (μ i).prod (Measure.tprod l μ)

instance MeasureTheory.Measure.sigmaFinite_tprod {δ : Type u_4} {X : δ → Type u_5} [(i : δ) → MeasurableSpace (X i)] (l : List δ) (μ : (i : δ) → Measure (X i)) [∀ (i : δ), SigmaFinite (μ i)] : SigmaFinite (Measure.tprod l μ)

theorem MeasureTheory.Measure.tprod_tprod {δ : Type u_4} {X : δ → Type u_5} [(i : δ) → MeasurableSpace (X i)] (l : List δ) (μ : (i : δ) → Measure (X i)) [∀ (i : δ), SigmaFinite (μ i)] (s : (i : δ) → Set (X i)) : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun (i : δ) => (μ i) (s i)) l).prod

noncomputable def MeasureTheory.Measure.pi' {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [Encodable ι] : Measure ((i : ι) → α i)

The product measure on an encodable finite type, defined by mapping Measure.tprod along the equivalence MeasurableEquiv.piMeasurableEquivTProd. The definition MeasureTheory.Measure.pi should be used instead of this one.

Equations

• MeasureTheory.Measure.pi' μ = MeasureTheory.Measure.map (List.TProd.elim' ⋯) (MeasureTheory.Measure.tprod (Encodable.sortedUniv ι) μ)

theorem MeasureTheory.Measure.pi'_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [Encodable ι] [∀ (i : ι), SigmaFinite (μ i)] (s : (i : ι) → Set (α i)) : (pi' μ) (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)

theorem MeasureTheory.Measure.pi_caratheodory {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) : MeasurableSpace.pi ≤ (OuterMeasure.pi fun (i : ι) => (μ i).toOuterMeasure).caratheodory

@[irreducible]

noncomputable def MeasureTheory.Measure.pi {ι : Type u_4} {α : ι → Type u_5} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) : Measure ((i : ι) → α i)

Measure.pi μ is the finite product of the measures {μ i | i : ι}. It is defined to be measure corresponding to MeasureTheory.OuterMeasure.pi.

Equations

• MeasureTheory.Measure.pi μ = (MeasureTheory.OuterMeasure.pi fun (i : ι) => (μ i).toOuterMeasure).toMeasure ⋯

theorem MeasureTheory.Measure.pi_def {ι : Type u_4} {α : ι → Type u_5} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) : Measure.pi μ = (OuterMeasure.pi fun (i : ι) => (μ i).toOuterMeasure).toMeasure ⋯

@[implicit_reducible]

noncomputable instance MeasureTheory.MeasureSpace.pi {ι : Type u_1} [Fintype ι] {α : ι → Type u_4} [(i : ι) → MeasureSpace (α i)] : MeasureSpace ((i : ι) → α i)

Equations

• MeasureTheory.MeasureSpace.pi = { toMeasurableSpace := MeasurableSpace.pi, volume := MeasureTheory.Measure.pi fun (x : ι) => MeasureTheory.volume }

theorem MeasureTheory.Measure.pi_pi_aux {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] (s : (i : ι) → Set (α i)) (hs : ∀ (i : ι), MeasurableSet (s i)) : (Measure.pi μ) (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)

def MeasureTheory.Measure.FiniteSpanningSetsIn.pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} {C : (i : ι) → Set (Set (α i))} (hμ : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)) : (Measure.pi μ).FiniteSpanningSetsIn (Set.univ.pi '' Set.univ.pi C)

Measure.pi μ has finite spanning sets in rectangles of finite spanning sets.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.Measure.pi_eq_generateFrom {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), MeasurableSpace.generateFrom (C i) = inst✝ i) (h2C : ∀ (i : ι), IsPiSystem (C i)) (h3C : (i : ι) → (μ i).FiniteSpanningSetsIn (C i)) {μν : Measure ((i : ι) → α i)} (h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → μν (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)) : Measure.pi μ = μν

A measure on a finite product space equals the product measure if they are equal on rectangles with as sides sets that generate the corresponding σ-algebras.

theorem MeasureTheory.Measure.pi_eq {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] {μ' : Measure ((i : ι) → α i)} (h : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (s i)) → μ' (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)) : Measure.pi μ = μ'

A measure on a finite product space equals the product measure if they are equal on rectangles.

theorem MeasureTheory.Measure.pi'_eq_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [Encodable ι] [∀ (i : ι), SigmaFinite (μ i)] : pi' μ = Measure.pi μ

@[simp]

theorem MeasureTheory.Measure.pi_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] (s : (i : ι) → Set (α i)) : (Measure.pi μ) (Set.univ.pi s) = ∏ i : ι, (μ i) (s i)

theorem MeasureTheory.Measure.pi_univ {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] : (Measure.pi μ) Set.univ = ∏ i : ι, (μ i) Set.univ

@[simp]

theorem MeasureTheory.Measure.pi_singleton {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] (f : (i : ι) → α i) : (Measure.pi μ) {f} = ∏ i : ι, (μ i) {f i}

instance MeasureTheory.Measure.pi.instIsFiniteMeasure {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), IsFiniteMeasure (μ i)] : IsFiniteMeasure (Measure.pi μ)

instance MeasureTheory.Measure.instIsFiniteMeasureForallVolume {ι : Type u_1} [Fintype ι] {α : ι → Type u_4} [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), IsFiniteMeasure volume] : IsFiniteMeasure volume

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

@[simp]

theorem MeasureTheory.Measure.pi_pi_finset {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), IsProbabilityMeasure (μ i)] (f : (i : ι) → Set (α i)) (s : Finset ι) : (Measure.pi μ) ((↑s).pi f) = ∏ i ∈ s, (μ i) (f i)

instance MeasureTheory.Measure.instIsProbabilityMeasureForallVolume {ι : Type u_1} [Fintype ι] {α : ι → Type u_4} [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), IsProbabilityMeasure volume] : IsProbabilityMeasure volume

theorem MeasureTheory.Measure.pi_ball {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → MetricSpace (α i)] (x : (i : ι) → α i) {r : ℝ} (hr : 0 < r) : (Measure.pi μ) (Metric.ball x r) = ∏ i : ι, (μ i) (Metric.ball (x i) r)

theorem MeasureTheory.Measure.pi_closedBall {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → MetricSpace (α i)] (x : (i : ι) → α i) {r : ℝ} (hr : 0 ≤ r) : (Measure.pi μ) (Metric.closedBall x r) = ∏ i : ι, (μ i) (Metric.closedBall (x i) r)

instance MeasureTheory.Measure.pi.sigmaFinite {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] : SigmaFinite (Measure.pi μ)

instance MeasureTheory.Measure.instSigmaFiniteForallVolume {ι : Type u_1} [Fintype ι] {α : ι → Type u_4} [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), SigmaFinite volume] : SigmaFinite volume

theorem MeasureTheory.Measure.pi_of_empty {α : Type u_4} [Fintype α] [IsEmpty α] {β : α → Type u_5} {m : (a : α) → MeasurableSpace (β a)} (μ : (a : α) → Measure (β a)) (x : (a : α) → β a := fun (a : α) => isEmptyElim a) : Measure.pi μ = dirac x

theorem MeasureTheory.Measure.volume_pi_eq_dirac {ι : Type u_4} [Fintype ι] [IsEmpty ι] {α : ι → Type u_5} [(i : ι) → MeasureSpace (α i)] (x : (a : ι) → α a := fun (a : ι) => isEmptyElim a) : volume = dirac x

@[simp]

theorem MeasureTheory.Measure.pi_empty_univ {α : Type u_4} [Fintype α] [IsEmpty α] {β : α → Type u_5} {m : (α : α) → MeasurableSpace (β α)} (μ : (a : α) → Measure (β a)) : (Measure.pi μ) Set.univ = 1

theorem MeasureTheory.Measure.pi_eval_preimage_null {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] {i : ι} {s : Set (α i)} (hs : (μ i) s = 0) : (Measure.pi μ) (Function.eval i ⁻¹' s) = 0

theorem MeasureTheory.Measure.quasiMeasurePreserving_eval {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] (i : ι) : QuasiMeasurePreserving (Function.eval i) (Measure.pi μ) (μ i)

theorem MeasureTheory.Measure.pi_map_eval {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [DecidableEq ι] (i : ι) : map (Function.eval i) (Measure.pi μ) = (∏ j ∈ Finset.univ.erase i, (μ j) Set.univ) • μ i

theorem MeasureTheory.Measure.pi_map_pi {ι : Type u_1} [Fintype ι] {X : ι → Type u_4} {Y : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)} {μ : (i : ι) → Measure (X i)} [(i : ι) → MeasurableSpace (Y i)] {f : (i : ι) → X i → Y i} [hμ : ∀ (i : ι), SigmaFinite (map (f i) (μ i))] (hf : ∀ (i : ι), AEMeasurable (f i) (μ i)) : map (fun (x : (i : ι) → X i) (i : ι) => f i (x i)) (Measure.pi μ) = Measure.pi fun (i : ι) => map (f i) (μ i)

theorem MeasureTheory.measurePreserving_eval {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), IsProbabilityMeasure (μ i)] (i : ι) : MeasurePreserving (Function.eval i) (Measure.pi μ) (μ i)

theorem MeasureTheory.Measure.pi_hyperplane {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] (i : ι) [NoAtoms (μ i)] (x : α i) : (Measure.pi μ) {f : (i : ι) → α i | f i = x} = 0

theorem MeasureTheory.Measure.ae_eval_ne {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] (i : ι) [NoAtoms (μ i)] (x : α i) : ∀ᵐ (y : (i : ι) → α i) ∂Measure.pi μ, y i ≠ x

theorem MeasureTheory.Measure.restrict_pi_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] (s : (i : ι) → Set (α i)) : (Measure.pi μ).restrict (Set.univ.pi fun (i : ι) => s i) = Measure.pi fun (i : ι) => (μ i).restrict (s i)

theorem MeasureTheory.Measure.tendsto_eval_ae_ae {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] {i : ι} : Filter.Tendsto (Function.eval i) (ae (Measure.pi μ)) (ae (μ i))

theorem MeasureTheory.Measure.ae_pi_le_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] : ae (Measure.pi μ) ≤ Filter.pi fun (i : ι) => ae (μ i)

theorem MeasureTheory.Measure.ae_eq_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] {β : ι → Type u_4} {f f' : (i : ι) → α i → β i} (h : ∀ (i : ι), f i =ᶠ[ae (μ i)] f' i) : (fun (x : (i : ι) → α i) (i : ι) => f i (x i)) =ᶠ[ae (Measure.pi μ)] fun (x : (i : ι) → α i) (i : ι) => f' i (x i)

theorem MeasureTheory.Measure.ae_le_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] {β : ι → Type u_4} [(i : ι) → Preorder (β i)] {f f' : (i : ι) → α i → β i} (h : ∀ (i : ι), f i ≤ᶠ[ae (μ i)] f' i) : (fun (x : (i : ι) → α i) (i : ι) => f i (x i)) ≤ᶠ[ae (Measure.pi μ)] fun (x : (i : ι) → α i) (i : ι) => f' i (x i)

theorem MeasureTheory.Measure.ae_le_set_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] {I : Set ι} {s t : (i : ι) → Set (α i)} (h : ∀ i ∈ I, s i ≤ᶠ[ae (μ i)] t i) : I.pi s ≤ᶠ[ae (Measure.pi μ)] I.pi t

theorem MeasureTheory.Measure.ae_eq_set_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] {I : Set ι} {s t : (i : ι) → Set (α i)} (h : ∀ i ∈ I, s i =ᶠ[ae (μ i)] t i) : I.pi s =ᶠ[ae (Measure.pi μ)] I.pi t

theorem MeasureTheory.Measure.pi_map_piCongrLeft {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [hι' : Fintype ι'] (e : ι ≃ ι') {β : ι' → Type u_4} [(i : ι') → MeasurableSpace (β i)] (μ : (i : ι') → Measure (β i)) [∀ (i : ι'), SigmaFinite (μ i)] : map (⇑(MeasurableEquiv.piCongrLeft (fun (i : ι') => β i) e)) (Measure.pi fun (i : ι) => μ (e i)) = Measure.pi μ

theorem MeasureTheory.Measure.pi_map_piOptionEquivProd {ι : Type u_1} [Fintype ι] {β : Option ι → Type u_4} [(i : Option ι) → MeasurableSpace (β i)] (μ : (i : Option ι) → Measure (β i)) [∀ (i : Option ι), SigmaFinite (μ i)] : map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun (i : ι) => μ (some i)).prod (μ none)) = Measure.pi μ

theorem MeasureTheory.Measure.pi_Iio_ae_eq_pi_Iic {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {s : Set ι} {f : (i : ι) → α i} : (s.pi fun (i : ι) => Set.Iio (f i)) =ᶠ[ae (Measure.pi μ)] s.pi fun (i : ι) => Set.Iic (f i)

theorem MeasureTheory.Measure.pi_Ioi_ae_eq_pi_Ici {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {s : Set ι} {f : (i : ι) → α i} : (s.pi fun (i : ι) => Set.Ioi (f i)) =ᶠ[ae (Measure.pi μ)] s.pi fun (i : ι) => Set.Ici (f i)

theorem MeasureTheory.Measure.univ_pi_Iio_ae_eq_Iic {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {f : (i : ι) → α i} : (Set.univ.pi fun (i : ι) => Set.Iio (f i)) =ᶠ[ae (Measure.pi μ)] Set.Iic f

theorem MeasureTheory.Measure.univ_pi_Ioi_ae_eq_Ici {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {f : (i : ι) → α i} : (Set.univ.pi fun (i : ι) => Set.Ioi (f i)) =ᶠ[ae (Measure.pi μ)] Set.Ici f

theorem MeasureTheory.Measure.pi_Ioo_ae_eq_pi_Icc {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {s : Set ι} {f g : (i : ι) → α i} : (s.pi fun (i : ι) => Set.Ioo (f i) (g i)) =ᶠ[ae (Measure.pi μ)] s.pi fun (i : ι) => Set.Icc (f i) (g i)

theorem MeasureTheory.Measure.pi_Ioo_ae_eq_pi_Ioc {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {s : Set ι} {f g : (i : ι) → α i} : (s.pi fun (i : ι) => Set.Ioo (f i) (g i)) =ᶠ[ae (Measure.pi μ)] s.pi fun (i : ι) => Set.Ioc (f i) (g i)

theorem MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {f g : (i : ι) → α i} : (Set.univ.pi fun (i : ι) => Set.Ioo (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Set.Icc f g

theorem MeasureTheory.Measure.pi_Ioc_ae_eq_pi_Icc {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {s : Set ι} {f g : (i : ι) → α i} : (s.pi fun (i : ι) => Set.Ioc (f i) (g i)) =ᶠ[ae (Measure.pi μ)] s.pi fun (i : ι) => Set.Icc (f i) (g i)

theorem MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {f g : (i : ι) → α i} : (Set.univ.pi fun (i : ι) => Set.Ioc (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Set.Icc f g

theorem MeasureTheory.Measure.pi_Ico_ae_eq_pi_Icc {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {s : Set ι} {f g : (i : ι) → α i} : (s.pi fun (i : ι) => Set.Ico (f i) (g i)) =ᶠ[ae (Measure.pi μ)] s.pi fun (i : ι) => Set.Icc (f i) (g i)

theorem MeasureTheory.Measure.univ_pi_Ico_ae_eq_Icc {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), NoAtoms (μ i)] {f g : (i : ι) → α i} : (Set.univ.pi fun (i : ι) => Set.Ico (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Set.Icc f g

theorem MeasureTheory.Measure.pi_noAtoms {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] (i : ι) [NoAtoms (μ i)] : NoAtoms (Measure.pi μ)

If one of the measures μ i has no atoms, them Measure.pi µ has no atoms. The instance below assumes that all μ i have no atoms.

instance MeasureTheory.Measure.pi_noAtoms' {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [h : Nonempty ι] [∀ (i : ι), NoAtoms (μ i)] : NoAtoms (Measure.pi μ)

instance MeasureTheory.Measure.instNoAtomsForallVolumeOfNonemptyOfSigmaFinite {ι : Type u_1} [Fintype ι] {α : ι → Type u_4} [Nonempty ι] [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), NoAtoms volume] : NoAtoms volume

instance MeasureTheory.Measure.pi.isLocallyFiniteMeasure {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → Measure (α i)} [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), IsLocallyFiniteMeasure (μ i)] : IsLocallyFiniteMeasure (Measure.pi μ)

instance MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite {ι : Type u_1} [Fintype ι] {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasureSpace (X i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), IsLocallyFiniteMeasure volume] : IsLocallyFiniteMeasure volume

instance IsUnifLocDoublingMeasure.pi {ι : Type u_4} [Fintype ι] {X : ι → Type u_5} [(i : ι) → PseudoMetricSpace (X i)] [(i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.Measure (X i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [∀ (i : ι), IsUnifLocDoublingMeasure (μ i)] : IsUnifLocDoublingMeasure (MeasureTheory.Measure.pi μ)

instance MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_pi {ι : Type u_4} [Fintype ι] {X : ι → Type u_5} [(i : ι) → PseudoMetricSpace (X i)] [(i : ι) → MeasureSpace (X i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), IsUnifLocDoublingMeasure volume] : IsUnifLocDoublingMeasure volume

instance MeasureTheory.Measure.pi.isMulLeftInvariant {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → Group (α i)] [∀ (i : ι), MeasurableMul (α i)] [∀ (i : ι), (μ i).IsMulLeftInvariant] : (Measure.pi μ).IsMulLeftInvariant

instance MeasureTheory.Measure.pi.isAddLeftInvariant {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → AddGroup (α i)] [∀ (i : ι), MeasurableAdd (α i)] [∀ (i : ι), (μ i).IsAddLeftInvariant] : (Measure.pi μ).IsAddLeftInvariant

instance MeasureTheory.Measure.instIsMulLeftInvariantForallVolumeOfMeasurableMulOfSigmaFinite {ι : Type u_1} [Fintype ι] {G : ι → Type u_4} [(i : ι) → Group (G i)] [(i : ι) → MeasureSpace (G i)] [∀ (i : ι), MeasurableMul (G i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), volume.IsMulLeftInvariant] : volume.IsMulLeftInvariant

instance MeasureTheory.Measure.instIsAddLeftInvariantForallVolumeOfMeasurableAddOfSigmaFinite {ι : Type u_1} [Fintype ι] {G : ι → Type u_4} [(i : ι) → AddGroup (G i)] [(i : ι) → MeasureSpace (G i)] [∀ (i : ι), MeasurableAdd (G i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), volume.IsAddLeftInvariant] : volume.IsAddLeftInvariant

instance MeasureTheory.Measure.pi.isMulRightInvariant {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → Group (α i)] [∀ (i : ι), MeasurableMul (α i)] [∀ (i : ι), (μ i).IsMulRightInvariant] : (Measure.pi μ).IsMulRightInvariant

instance MeasureTheory.Measure.pi.isAddRightInvariant {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → AddGroup (α i)] [∀ (i : ι), MeasurableAdd (α i)] [∀ (i : ι), (μ i).IsAddRightInvariant] : (Measure.pi μ).IsAddRightInvariant

instance MeasureTheory.Measure.instIsMulRightInvariantForallVolumeOfMeasurableMulOfSigmaFinite {ι : Type u_1} [Fintype ι] {G : ι → Type u_4} [(i : ι) → Group (G i)] [(i : ι) → MeasureSpace (G i)] [∀ (i : ι), MeasurableMul (G i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), volume.IsMulRightInvariant] : volume.IsMulRightInvariant

instance MeasureTheory.Measure.instIsAddRightInvariantForallVolumeOfMeasurableAddOfSigmaFinite {ι : Type u_1} [Fintype ι] {G : ι → Type u_4} [(i : ι) → AddGroup (G i)] [(i : ι) → MeasureSpace (G i)] [∀ (i : ι), MeasurableAdd (G i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), volume.IsAddRightInvariant] : volume.IsAddRightInvariant

instance MeasureTheory.Measure.pi.isInvInvariant {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → Group (α i)] [∀ (i : ι), MeasurableInv (α i)] [∀ (i : ι), (μ i).IsInvInvariant] : (Measure.pi μ).IsInvInvariant

instance MeasureTheory.Measure.pi.isNegInvariant {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → AddGroup (α i)] [∀ (i : ι), MeasurableNeg (α i)] [∀ (i : ι), (μ i).IsNegInvariant] : (Measure.pi μ).IsNegInvariant

instance MeasureTheory.Measure.instIsInvInvariantForallVolumeOfMeasurableInvOfSigmaFinite {ι : Type u_1} [Fintype ι] {G : ι → Type u_4} [(i : ι) → Group (G i)] [(i : ι) → MeasureSpace (G i)] [∀ (i : ι), MeasurableInv (G i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), volume.IsInvInvariant] : volume.IsInvInvariant

instance MeasureTheory.Measure.instIsNegInvariantForallVolumeOfMeasurableNegOfSigmaFinite {ι : Type u_1} [Fintype ι] {G : ι → Type u_4} [(i : ι) → AddGroup (G i)] [(i : ι) → MeasureSpace (G i)] [∀ (i : ι), MeasurableNeg (G i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), volume.IsNegInvariant] : volume.IsNegInvariant

instance MeasureTheory.Measure.pi.isOpenPosMeasure {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), (μ i).IsOpenPosMeasure] : (Measure.pi μ).IsOpenPosMeasure

instance MeasureTheory.Measure.instIsOpenPosMeasureForallVolumeOfSigmaFinite {ι : Type u_1} [Fintype ι] {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasureSpace (X i)] [∀ (i : ι), volume.IsOpenPosMeasure] [∀ (i : ι), SigmaFinite volume] : volume.IsOpenPosMeasure

instance MeasureTheory.Measure.pi.isFiniteMeasureOnCompacts {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), IsFiniteMeasureOnCompacts (μ i)] : IsFiniteMeasureOnCompacts (Measure.pi μ)

instance MeasureTheory.Measure.instIsFiniteMeasureOnCompactsForallVolumeOfSigmaFinite {ι : Type u_1} [Fintype ι] {X : ι → Type u_4} [(i : ι) → MeasureSpace (X i)] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), IsFiniteMeasureOnCompacts volume] : IsFiniteMeasureOnCompacts volume

instance MeasureTheory.Measure.pi.isHaarMeasure {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → Group (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), (μ i).IsHaarMeasure] [∀ (i : ι), MeasurableMul (α i)] : (Measure.pi μ).IsHaarMeasure

instance MeasureTheory.Measure.pi.isAddHaarMeasure {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [(i : ι) → AddGroup (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), (μ i).IsAddHaarMeasure] [∀ (i : ι), MeasurableAdd (α i)] : (Measure.pi μ).IsAddHaarMeasure

instance MeasureTheory.Measure.instIsHaarMeasureForallVolumeOfMeasurableMulOfSigmaFinite {ι : Type u_1} [Fintype ι] {G : ι → Type u_4} [(i : ι) → Group (G i)] [(i : ι) → MeasureSpace (G i)] [∀ (i : ι), MeasurableMul (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), volume.IsHaarMeasure] : volume.IsHaarMeasure

instance MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite {ι : Type u_1} [Fintype ι] {G : ι → Type u_4} [(i : ι) → AddGroup (G i)] [(i : ι) → MeasureSpace (G i)] [∀ (i : ι), MeasurableAdd (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), SigmaFinite volume] [∀ (i : ι), volume.IsAddHaarMeasure] : volume.IsAddHaarMeasure

theorem MeasureTheory.volume_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasureSpace (α i)] : volume = Measure.pi fun (x : ι) => volume

theorem MeasureTheory.volume_pi_pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), SigmaFinite volume] (s : (i : ι) → Set (α i)) : volume (Set.univ.pi s) = ∏ i : ι, volume (s i)

theorem MeasureTheory.volume_pi_ball {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), SigmaFinite volume] [(i : ι) → MetricSpace (α i)] (x : (i : ι) → α i) {r : ℝ} (hr : 0 < r) : volume (Metric.ball x r) = ∏ i : ι, volume (Metric.ball (x i) r)

theorem MeasureTheory.volume_pi_closedBall {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), SigmaFinite volume] [(i : ι) → MetricSpace (α i)] (x : (i : ι) → α i) {r : ℝ} (hr : 0 ≤ r) : volume (Metric.closedBall x r) = ∏ i : ι, volume (Metric.closedBall (x i) r)

instance MeasureTheory.Pi.isMulLeftInvariant_volume {ι : Type u_1} [Fintype ι] {α : Type u_4} [Group α] [MeasureSpace α] [SigmaFinite volume] [MeasurableMul α] [volume.IsMulLeftInvariant] : volume.IsMulLeftInvariant

We intentionally restrict this only to the nondependent function space, since type-class inference cannot find an instance for ι → ℝ when this is stated for dependent function spaces.

instance MeasureTheory.Pi.isAddLeftInvariant_volume {ι : Type u_1} [Fintype ι] {α : Type u_4} [AddGroup α] [MeasureSpace α] [SigmaFinite volume] [MeasurableAdd α] [volume.IsAddLeftInvariant] : volume.IsAddLeftInvariant

We intentionally restrict this only to the nondependent function space, since type-class inference cannot find an instance for ι → ℝ when this is stated for dependent function spaces.

instance MeasureTheory.Pi.isInvInvariant_volume {ι : Type u_1} [Fintype ι] {α : Type u_4} [Group α] [MeasureSpace α] [SigmaFinite volume] [MeasurableInv α] [volume.IsInvInvariant] : volume.IsInvInvariant

We intentionally restrict this only to the nondependent function space, since type-class inference cannot find an instance for ι → ℝ when this is stated for dependent function spaces.

instance MeasureTheory.Pi.isNegInvariant_volume {ι : Type u_1} [Fintype ι] {α : Type u_4} [AddGroup α] [MeasureSpace α] [SigmaFinite volume] [MeasurableNeg α] [volume.IsNegInvariant] : volume.IsNegInvariant

We intentionally restrict this only to the nondependent function space, since type-class inference cannot find an instance for ι → ℝ when this is stated for dependent function spaces.

Measure-preserving equivalences

In this section we prove that some measurable equivalences (e.g., between Fin 1 → α and α or between Fin 2 → α and α × α) preserve measure or volume. These lemmas can be used to prove that measures of corresponding sets (images or preimages) have equal measures and functions f ∘ e and f have equal integrals, see lemmas in the MeasureTheory.measurePreserving prefix.

theorem MeasureTheory.measurePreserving_piEquivPiSubtypeProd {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] {m : (i : ι) → MeasurableSpace (α i)} (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] (p : ι → Prop) [DecidablePred p] : MeasurePreserving (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p)) (Measure.pi μ) ((Measure.pi fun (i : Subtype p) => μ ↑i).prod (Measure.pi fun (i : { i : ι // ¬p i }) => μ ↑i))

theorem MeasureTheory.volume_preserving_piEquivPiSubtypeProd {ι : Type u_1} [Fintype ι] (α : ι → Type u_4) [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), SigmaFinite volume] (p : ι → Prop) [DecidablePred p] : MeasurePreserving (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p)) volume volume

theorem MeasureTheory.measurePreserving_piCongrLeft {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} [Fintype ι] {m : (i : ι) → MeasurableSpace (α i)} (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] [Fintype ι'] (f : ι' ≃ ι) : MeasurePreserving (⇑(MeasurableEquiv.piCongrLeft α f)) (Measure.pi fun (i' : ι') => μ (f i')) (Measure.pi μ)

theorem MeasureTheory.volume_measurePreserving_piCongrLeft {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] (α : ι → Type u_4) (f : ι' ≃ ι) [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), SigmaFinite volume] : MeasurePreserving (⇑(MeasurableEquiv.piCongrLeft α f)) volume volume

theorem MeasureTheory.measurePreserving_arrowProdEquivProdArrow (α : Type u_4) (β : Type u_5) (γ : Type u_6) [MeasurableSpace α] [MeasurableSpace β] [Fintype γ] (μ : γ → Measure α) (ν : γ → Measure β) [∀ (i : γ), SigmaFinite (μ i)] [∀ (i : γ), SigmaFinite (ν i)] : MeasurePreserving (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) (Measure.pi fun (i : γ) => (μ i).prod (ν i)) ((Measure.pi fun (i : γ) => μ i).prod (Measure.pi fun (i : γ) => ν i))

theorem MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow (α : Type u_4) (β : Type u_5) (γ : Type u_6) [MeasureSpace α] [MeasureSpace β] [Fintype γ] [SigmaFinite volume] [SigmaFinite volume] : MeasurePreserving (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) volume volume

theorem MeasureTheory.measurePreserving_sumPiEquivProdPi_symm {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {X : ι ⊕ ι' → Type u_4} {m : (i : ι ⊕ ι') → MeasurableSpace (X i)} (μ : (i : ι ⊕ ι') → Measure (X i)) [∀ (i : ι ⊕ ι'), SigmaFinite (μ i)] : MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm) ((Measure.pi fun (i : ι) => μ (Sum.inl i)).prod (Measure.pi fun (i : ι') => μ (Sum.inr i))) (Measure.pi μ)

theorem MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] (X : ι ⊕ ι' → Type u_4) [(i : ι ⊕ ι') → MeasureSpace (X i)] [∀ (i : ι ⊕ ι'), SigmaFinite volume] : MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm) volume volume

theorem MeasureTheory.measurePreserving_sumPiEquivProdPi {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {X : ι ⊕ ι' → Type u_4} {_m : (i : ι ⊕ ι') → MeasurableSpace (X i)} (μ : (i : ι ⊕ ι') → Measure (X i)) [∀ (i : ι ⊕ ι'), SigmaFinite (μ i)] : MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi X)) (Measure.pi μ) ((Measure.pi fun (i : ι) => μ (Sum.inl i)).prod (Measure.pi fun (i : ι') => μ (Sum.inr i)))

theorem MeasureTheory.volume_measurePreserving_sumPiEquivProdPi {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] (X : ι ⊕ ι' → Type u_4) [(i : ι ⊕ ι') → MeasureSpace (X i)] [∀ (i : ι ⊕ ι'), SigmaFinite volume] : MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi X)) volume volume

theorem MeasureTheory.measurePreserving_piFinSuccAbove {n : ℕ} {α : Fin (n + 1) → Type u} {m : (i : Fin (n + 1)) → MeasurableSpace (α i)} (μ : (i : Fin (n + 1)) → Measure (α i)) [∀ (i : Fin (n + 1)), SigmaFinite (μ i)] (i : Fin (n + 1)) : MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove α i)) (Measure.pi μ) ((μ i).prod (Measure.pi fun (j : Fin n) => μ (i.succAbove j)))

theorem MeasureTheory.volume_preserving_piFinSuccAbove {n : ℕ} (α : Fin (n + 1) → Type u) [(i : Fin (n + 1)) → MeasureSpace (α i)] [∀ (i : Fin (n + 1)), SigmaFinite volume] (i : Fin (n + 1)) : MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove α i)) volume volume

theorem MeasureTheory.measurePreserving_piUnique {ι : Type u_1} [Fintype ι] {X : ι → Type u_4} [Unique ι] {m : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i)) : MeasurePreserving (⇑(MeasurableEquiv.piUnique X)) (Measure.pi μ) (μ default)

theorem MeasureTheory.volume_preserving_piUnique {ι : Type u_1} [Fintype ι] (X : ι → Type u_4) [Unique ι] [(i : ι) → MeasureSpace (X i)] : MeasurePreserving (⇑(MeasurableEquiv.piUnique X)) volume volume

theorem MeasureTheory.measurePreserving_funUnique {β : Type u} {_m : MeasurableSpace β} (μ : Measure β) (α : Type v) [Unique α] : MeasurePreserving (⇑(MeasurableEquiv.funUnique α β)) (Measure.pi fun (x : α) => μ) μ

theorem MeasureTheory.volume_preserving_funUnique (α : Type u) (β : Type v) [Unique α] [MeasureSpace β] : MeasurePreserving (⇑(MeasurableEquiv.funUnique α β)) volume volume

theorem MeasureTheory.measurePreserving_piFinTwo {α : Fin 2 → Type u} {m : (i : Fin 2) → MeasurableSpace (α i)} (μ : (i : Fin 2) → Measure (α i)) [∀ (i : Fin 2), SigmaFinite (μ i)] : MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ) ((μ 0).prod (μ 1))

theorem MeasureTheory.volume_preserving_piFinTwo (α : Fin 2 → Type u) [(i : Fin 2) → MeasureSpace (α i)] [∀ (i : Fin 2), SigmaFinite volume] : MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) volume volume

theorem MeasureTheory.measurePreserving_finTwoArrow_vec {α : Type u} {x✝ : MeasurableSpace α} (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] : MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (Measure.pi ![μ, ν]) (μ.prod ν)

theorem MeasureTheory.measurePreserving_finTwoArrow {α : Type u} {m : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] : MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (Measure.pi fun (x : Fin 2) => μ) (μ.prod μ)

theorem MeasureTheory.volume_preserving_finTwoArrow (α : Type u) [MeasureSpace α] [SigmaFinite volume] : MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) volume volume

theorem MeasureTheory.measurePreserving_pi_empty {ι : Type u} {α : ι → Type v} [Fintype ι] [IsEmpty ι] {m : (i : ι) → MeasurableSpace (α i)} (μ : (i : ι) → Measure (α i)) : MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) (Measure.pi μ) (Measure.dirac ())

theorem MeasureTheory.volume_preserving_pi_empty {ι : Type u} (α : ι → Type v) [Fintype ι] [IsEmpty ι] [(i : ι) → MeasureSpace (α i)] : MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) volume volume

theorem MeasureTheory.measurePreserving_piFinsetUnion {ι : Type u_4} {α : ι → Type u_5} {x✝ : (i : ι) → MeasurableSpace (α i)} [DecidableEq ι] {s t : Finset ι} (h : Disjoint s t) (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] : MeasurePreserving (⇑(MeasurableEquiv.piFinsetUnion α h)) ((Measure.pi fun (i : ↥s) => μ ↑i).prod (Measure.pi fun (i : ↥t) => μ ↑i)) (Measure.pi fun (i : ↥(s ∪ t)) => μ ↑i)

theorem MeasureTheory.volume_preserving_piFinsetUnion {ι : Type u_4} [DecidableEq ι] (α : ι → Type u_5) {s t : Finset ι} (h : Disjoint s t) [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), SigmaFinite volume] : MeasurePreserving (⇑(MeasurableEquiv.piFinsetUnion α h)) volume volume

theorem MeasureTheory.measurePreserving_pi {ι : Type u_4} [Fintype ι] {α : ι → Type v} {β : ι → Type u_5} [(i : ι) → MeasurableSpace (α i)] [(i : ι) → MeasurableSpace (β i)] (μ : (i : ι) → Measure (α i)) (ν : (i : ι) → Measure (β i)) {f : (i : ι) → α i → β i} [hν : ∀ (i : ι), SigmaFinite (ν i)] (hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)) : MeasurePreserving (fun (a : (i : ι) → α i) (i : ι) => f i (a i)) (Measure.pi μ) (Measure.pi ν)

theorem MeasureTheory.volume_preserving_pi {ι : Type u_1} [Fintype ι] {α' : ι → Type u_4} {β' : ι → Type u_5} [(i : ι) → MeasureSpace (α' i)] [(i : ι) → MeasureSpace (β' i)] [∀ (i : ι), SigmaFinite volume] {f : (i : ι) → α' i → β' i} (hf : ∀ (i : ι), MeasurePreserving (f i) volume volume) : MeasurePreserving (fun (a : (i : ι) → α' i) (i : ι) => f i (a i)) volume volume

theorem MeasureTheory.measurePreserving_arrowCongr' {α₁ : Type u_4} {β₁ : Type u_5} {α₂ : Type u_6} {β₂ : Type u_7} [Fintype α₁] [Fintype α₂] [MeasurableSpace β₁] [MeasurableSpace β₂] (μ : α₁ → Measure β₁) (ν : α₂ → Measure β₂) [∀ (i : α₂), SigmaFinite (ν i)] (eα : α₁ ≃ α₂) (eβ : β₁ ≃ᵐ β₂) (hm : ∀ (i : α₁), MeasurePreserving (⇑eβ) (μ i) (ν (eα i))) : MeasurePreserving (⇑(MeasurableEquiv.arrowCongr' eα eβ)) (Measure.pi fun (i : α₁) => μ i) (Measure.pi fun (i : α₂) => ν i)

The measurable equiv (α₁ → β₁) ≃ᵐ (α₂ → β₂) induced by α₁ ≃ α₂ and β₁ ≃ᵐ β₂ is measure preserving.

theorem MeasureTheory.volume_preserving_arrowCongr' {α₁ : Type u_4} {β₁ : Type u_5} {α₂ : Type u_6} {β₂ : Type u_7} [Fintype α₁] [Fintype α₂] [MeasureSpace β₁] [MeasureSpace β₂] [SigmaFinite volume] (hα : α₁ ≃ α₂) (hβ : β₁ ≃ᵐ β₂) (hm : MeasurePreserving (⇑hβ) volume volume) : MeasurePreserving (⇑(MeasurableEquiv.arrowCongr' hα hβ)) volume volume

The measurable equiv (α₁ → β₁) ≃ᵐ (α₂ → β₂) induced by α₁ ≃ α₂ and β₁ ≃ᵐ β₂ is volume preserving.