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 along some subset of the variables, use MeasureTheory.measurePreserving_piEquivPiSubtypeProd to reduce to the situation of a product of two measures: this lemma states that the bijection MeasurableEquiv.piEquivPiSubtypeProd α p between (∀ i : ι, α i) and ((i : {i // p i}) → α i) × ((i : {i // ¬ p i}) → α i) maps a product measure to a direct product of product measures, to which one can apply the usual Fubini for direct product of measures.

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 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

We start with some measurability properties

theorem IsPiSystem.pi {ι : Type u_1} {α : ι → Type u_3} {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), IsPiSystem (C i)) : IsPiSystem (Set.pi Set.univ '' Set.pi Set.univ C)

Boxes formed by π-systems form a π-system.

theorem isPiSystem_pi {ι : Type u_1} {α : ι → Type u_3} [(i : ι) → MeasurableSpace (α i)] : IsPiSystem (Set.pi Set.univ '' Set.pi Set.univ fun i => {s | MeasurableSet s})

Boxes form a π-system.

theorem IsCountablySpanning.pi {ι : Type u_1} {α : ι → Type u_3} [Finite ι] {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), IsCountablySpanning (C i)) : IsCountablySpanning (Set.pi Set.univ '' Set.pi Set.univ C)

Boxes of countably spanning sets are countably spanning.

theorem generateFrom_pi_eq {ι : Type u_1} {α : ι → Type u_3} [Finite ι] {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), IsCountablySpanning (C i)) : MeasurableSpace.pi = MeasurableSpace.generateFrom (Set.pi Set.univ '' Set.pi Set.univ C)

The product of generated σ-algebras is the one generated by boxes, if both generating sets are countably spanning.

theorem generateFrom_eq_pi {ι : Type u_1} {α : ι → Type u_3} [Finite ι] [h : (i : ι) → MeasurableSpace (α i)] {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), MeasurableSpace.generateFrom (C i) = h i) (h2C : ∀ (i : ι), IsCountablySpanning (C i)) : MeasurableSpace.generateFrom (Set.pi Set.univ '' Set.pi Set.univ C) = MeasurableSpace.pi

If C and D generate the σ-algebras on α resp. β, then rectangles formed by C and D generate the σ-algebra on α × β.

theorem generateFrom_pi {ι : Type u_1} {α : ι → Type u_3} [Finite ι] [(i : ι) → MeasurableSpace (α i)] : MeasurableSpace.generateFrom (Set.pi Set.univ '' Set.pi Set.univ fun i => {s | MeasurableSet s}) = MeasurableSpace.pi

The product σ-algebra is generated from boxes, i.e. s ×ˢ t for sets s : set α and t : set β.

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

An upper bound for the measure in a finite product space. It is defined to 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 = Finset.prod Finset.univ fun i => ↑(m i) (Function.eval i '' s)

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

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

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

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

def MeasureTheory.OuterMeasure.pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] (m : (i : ι) → MeasureTheory.OuterMeasure (α i)) : MeasureTheory.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 : ι) → MeasureTheory.OuterMeasure (α i)) (s : (i : ι) → Set (α i)) : ↑(MeasureTheory.OuterMeasure.pi m) (Set.pi Set.univ s) ≤ Finset.prod Finset.univ fun i => ↑(m i) (s i)

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

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

A product of measures in tprod α l.

Equations

• MeasureTheory.Measure.tprod l μ = List.rec (MeasureTheory.Measure.dirac PUnit.unit) (fun i l ih => let_fun this := MeasureTheory.Measure.prod (μ i) ih; this) l

@[simp]

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

@[simp]

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

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

Equations

• @MeasureTheory.Measure.sigmaFinite_tprod = @MeasureTheory.Measure.sigmaFinite_tprod.proof_1

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

def MeasureTheory.Measure.pi' {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [Encodable ι] : MeasureTheory.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' (_ : ∀ (x : ι), x ∈ Encodable.sortedUniv ι)) (MeasureTheory.Measure.tprod (Encodable.sortedUniv ι) μ)

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

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

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

@[irreducible]

def MeasureTheory.Measure.pi {ι : Type u_4} {α : ι → Type u_5} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) : MeasureTheory.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.Measure.wrapped✝.1

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

Equations

• MeasureTheory.MeasureSpace.pi = MeasureTheory.MeasureSpace.mk (MeasureTheory.Measure.pi fun x => MeasureTheory.volume)

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

def MeasureTheory.Measure.FiniteSpanningSetsIn.pi {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → MeasureTheory.Measure (α i)} {C : (i : ι) → Set (Set (α i))} (hμ : (i : ι) → MeasureTheory.Measure.FiniteSpanningSetsIn (μ i) (C i)) : MeasureTheory.Measure.FiniteSpanningSetsIn (MeasureTheory.Measure.pi μ) (Set.pi Set.univ '' Set.pi Set.univ 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 : ι) → MeasureTheory.Measure (α i)} {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), MeasurableSpace.generateFrom (C i) = inst✝ i) (h2C : ∀ (i : ι), IsPiSystem (C i)) (h3C : (i : ι) → MeasureTheory.Measure.FiniteSpanningSetsIn (μ i) (C i)) {μν : MeasureTheory.Measure ((i : ι) → α i)} (h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i ∈ C i) → ↑↑μν (Set.pi Set.univ s) = Finset.prod Finset.univ fun i => ↑↑(μ i) (s i)) : MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {μ' : MeasureTheory.Measure ((i : ι) → α i)} (h : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (s i)) → ↑↑μ' (Set.pi Set.univ s) = Finset.prod Finset.univ fun i => ↑↑(μ i) (s i)) : MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [Encodable ι] : MeasureTheory.Measure.pi' μ = MeasureTheory.Measure.pi μ

@[simp]

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

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

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

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

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

Equations

• @MeasureTheory.Measure.pi.sigmaFinite = @MeasureTheory.Measure.pi.sigmaFinite.proof_1

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

Equations

• @MeasureTheory.Measure.instSigmaFiniteForAllToMeasurableSpacePiVolume = @MeasureTheory.Measure.instSigmaFiniteForAllToMeasurableSpacePiVolume.proof_1

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

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

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

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

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

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

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

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

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

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

theorem MeasureTheory.Measure.pi_Iio_ae_eq_pi_Iic {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {s : Set ι} {f : (i : ι) → α i} : (Set.pi s fun i => Set.Iio (f i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.pi μ)] Set.pi s 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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {s : Set ι} {f : (i : ι) → α i} : (Set.pi s fun i => Set.Ioi (f i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.pi μ)] Set.pi s 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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {f : (i : ι) → α i} : (Set.pi Set.univ fun i => Set.Iio (f i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {f : (i : ι) → α i} : (Set.pi Set.univ fun i => Set.Ioi (f i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {s : Set ι} {f : (i : ι) → α i} {g : (i : ι) → α i} : (Set.pi s fun i => Set.Ioo (f i) (g i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.pi μ)] Set.pi s 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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {s : Set ι} {f : (i : ι) → α i} {g : (i : ι) → α i} : (Set.pi s fun i => Set.Ioo (f i) (g i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.pi μ)] Set.pi s 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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {f : (i : ι) → α i} {g : (i : ι) → α i} : (Set.pi Set.univ fun i => Set.Ioo (f i) (g i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {s : Set ι} {f : (i : ι) → α i} {g : (i : ι) → α i} : (Set.pi s fun i => Set.Ioc (f i) (g i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.pi μ)] Set.pi s 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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {f : (i : ι) → α i} {g : (i : ι) → α i} : (Set.pi Set.univ fun i => Set.Ioc (f i) (g i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {s : Set ι} {f : (i : ι) → α i} {g : (i : ι) → α i} : (Set.pi s fun i => Set.Ico (f i) (g i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.pi μ)] Set.pi s 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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {f : (i : ι) → α i} {g : (i : ι) → α i} : (Set.pi Set.univ fun i => Set.Ico (f i) (g i)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.pi μ)] Set.Icc f g

theorem MeasureTheory.Measure.pi_noAtoms {ι : Type u_1} {α : ι → Type u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (i : ι) [MeasureTheory.NoAtoms (μ i)] : MeasureTheory.NoAtoms (MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [h : Nonempty ι] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] : MeasureTheory.NoAtoms (MeasureTheory.Measure.pi μ)

Equations

• @MeasureTheory.Measure.pi_noAtoms' = @MeasureTheory.Measure.pi_noAtoms'.proof_1

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

Equations

• @MeasureTheory.Measure.instNoAtomsForAllToMeasurableSpacePiVolume = @MeasureTheory.Measure.instNoAtomsForAllToMeasurableSpacePiVolume.proof_1

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

Equations

• @MeasureTheory.Measure.pi.isLocallyFiniteMeasure = @MeasureTheory.Measure.pi.isLocallyFiniteMeasure.proof_1

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

Equations

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

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

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

Equations

• @MeasureTheory.Measure.pi.isAddLeftInvariant = @MeasureTheory.Measure.pi.isAddLeftInvariant.proof_1

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

Equations

• @MeasureTheory.Measure.pi.isMulLeftInvariant = @MeasureTheory.Measure.pi.isMulLeftInvariant.proof_1

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

Equations

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

theorem MeasureTheory.Measure.instIsAddLeftInvariantForAllToMeasurableSpacePiInstAddToAddToAddZeroClassToAddMonoidToSubNegAddMonoidVolume.proof_1 {ι : Type u_1} [Fintype ι] {G : ι → Type u_2} [(i : ι) → AddGroup (G i)] [(i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableAdd (G i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [∀ (i : ι), MeasureTheory.Measure.IsAddLeftInvariant MeasureTheory.volume] : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.pi fun x => MeasureTheory.volume)

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

Equations

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

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

Equations

• @MeasureTheory.Measure.pi.isAddRightInvariant = @MeasureTheory.Measure.pi.isAddRightInvariant.proof_1

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

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

Equations

• @MeasureTheory.Measure.pi.isMulRightInvariant = @MeasureTheory.Measure.pi.isMulRightInvariant.proof_1

theorem MeasureTheory.Measure.instIsAddRightInvariantForAllToMeasurableSpacePiInstAddToAddToAddZeroClassToAddMonoidToSubNegAddMonoidVolume.proof_1 {ι : Type u_1} [Fintype ι] {G : ι → Type u_2} [(i : ι) → AddGroup (G i)] [(i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableAdd (G i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [∀ (i : ι), MeasureTheory.Measure.IsAddRightInvariant MeasureTheory.volume] : MeasureTheory.Measure.IsAddRightInvariant (MeasureTheory.Measure.pi fun x => MeasureTheory.volume)

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

Equations

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

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

Equations

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

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

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

Equations

• @MeasureTheory.Measure.pi.isNegInvariant = @MeasureTheory.Measure.pi.isNegInvariant.proof_1

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

Equations

• @MeasureTheory.Measure.pi.isInvInvariant = @MeasureTheory.Measure.pi.isInvInvariant.proof_1

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

Equations

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

theorem MeasureTheory.Measure.instIsNegInvariantForAllToMeasurableSpacePiInstNegToNegToNegZeroClassToSubNegZeroAddMonoidToDivisionAddMonoidVolume.proof_1 {ι : Type u_1} [Fintype ι] {G : ι → Type u_2} [(i : ι) → AddGroup (G i)] [(i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableNeg (G i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [∀ (i : ι), MeasureTheory.Measure.IsNegInvariant MeasureTheory.volume] : MeasureTheory.Measure.IsNegInvariant (MeasureTheory.Measure.pi fun x => MeasureTheory.volume)

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

Equations

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

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

Equations

• @MeasureTheory.Measure.pi.isOpenPosMeasure = @MeasureTheory.Measure.pi.isOpenPosMeasure.proof_1

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

Equations

• @MeasureTheory.Measure.instIsOpenPosMeasureForAllTopologicalSpaceToMeasurableSpacePiVolume = @MeasureTheory.Measure.instIsOpenPosMeasureForAllTopologicalSpaceToMeasurableSpacePiVolume.proof_1

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

Equations

• @MeasureTheory.Measure.pi.isFiniteMeasureOnCompacts = @MeasureTheory.Measure.pi.isFiniteMeasureOnCompacts.proof_1

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

Equations

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

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

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

Equations

• @MeasureTheory.Measure.pi.isAddHaarMeasure = @MeasureTheory.Measure.pi.isAddHaarMeasure.proof_1

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

Equations

• @MeasureTheory.Measure.pi.isHaarMeasure = @MeasureTheory.Measure.pi.isHaarMeasure.proof_1

theorem MeasureTheory.Measure.instIsAddHaarMeasureForAllAddGroupTopologicalSpaceToMeasurableSpacePiVolume.proof_1 {ι : Type u_1} [Fintype ι] {G : ι → Type u_2} [(i : ι) → AddGroup (G i)] [(i : ι) → MeasureTheory.MeasureSpace (G i)] [∀ (i : ι), MeasurableAdd (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] [∀ (i : ι), MeasureTheory.Measure.IsAddHaarMeasure MeasureTheory.volume] : MeasureTheory.Measure.IsAddHaarMeasure (MeasureTheory.Measure.pi fun x => MeasureTheory.volume)

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

Equations

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

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

Equations

• @MeasureTheory.Measure.instIsHaarMeasureForAllGroupTopologicalSpaceToMeasurableSpacePiVolume = @MeasureTheory.Measure.instIsHaarMeasureForAllGroupTopologicalSpaceToMeasurableSpacePiVolume.proof_1

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

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

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

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

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

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.

Equations

• @MeasureTheory.Pi.isAddLeftInvariant_volume = @MeasureTheory.Pi.isAddLeftInvariant_volume.proof_1

theorem MeasureTheory.Pi.isAddLeftInvariant_volume.proof_1 {ι : Type u_1} [Fintype ι] {α : Type u_2} [AddGroup α] [MeasureTheory.MeasureSpace α] [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasurableAdd α] [MeasureTheory.Measure.IsAddLeftInvariant MeasureTheory.volume] : MeasureTheory.Measure.IsAddLeftInvariant (MeasureTheory.Measure.pi fun x => MeasureTheory.volume)

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

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.

Equations

• @MeasureTheory.Pi.isMulLeftInvariant_volume = @MeasureTheory.Pi.isMulLeftInvariant_volume.proof_1

theorem MeasureTheory.Pi.isNegInvariant_volume.proof_1 {ι : Type u_1} [Fintype ι] {α : Type u_2} [AddGroup α] [MeasureTheory.MeasureSpace α] [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasurableNeg α] [MeasureTheory.Measure.IsNegInvariant MeasureTheory.volume] : MeasureTheory.Measure.IsNegInvariant (MeasureTheory.Measure.pi fun x => MeasureTheory.volume)

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

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.

Equations

• @MeasureTheory.Pi.isNegInvariant_volume = @MeasureTheory.Pi.isNegInvariant_volume.proof_1

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

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.

Equations

• @MeasureTheory.Pi.isInvInvariant_volume = @MeasureTheory.Pi.isInvInvariant_volume.proof_1

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} {α : ι → Type v} [Fintype ι] {m : (i : ι) → MeasurableSpace (α i)} (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (p : ι → Prop) [DecidablePred p] : MeasureTheory.MeasurePreserving ↑(MeasurableEquiv.piEquivPiSubtypeProd α p)

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

theorem MeasureTheory.measurePreserving_piFinSuccAboveEquiv {n : ℕ} {α : Fin (n + 1) → Type u} {m : (i : Fin (n + 1)) → MeasurableSpace (α i)} (μ : (i : Fin (n + 1)) → MeasureTheory.Measure (α i)) [∀ (i : Fin (n + 1)), MeasureTheory.SigmaFinite (μ i)] (i : Fin (n + 1)) : MeasureTheory.MeasurePreserving ↑(MeasurableEquiv.piFinSuccAboveEquiv α i)

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

theorem MeasureTheory.measurePreserving_funUnique {β : Type u} {m : MeasurableSpace β} (μ : MeasureTheory.Measure β) (α : Type v) [Unique α] : MeasureTheory.MeasurePreserving ↑(MeasurableEquiv.funUnique α β)

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

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

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

theorem MeasureTheory.measurePreserving_finTwoArrow_vec {α : Type u} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] : MeasureTheory.MeasurePreserving ↑MeasurableEquiv.finTwoArrow

theorem MeasureTheory.measurePreserving_finTwoArrow {α : Type u} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : MeasureTheory.MeasurePreserving ↑MeasurableEquiv.finTwoArrow

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

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

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