Documentation

Mathlib.MeasureTheory.Constructions.Pi

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 #

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

Tags #

finitary product measure

We start with some measurability properties

theorem MeasurableSpace.pi_eq_generateFrom_projections {ι : Type u_1} {α : ιType u_3} {mα : (i : ι) → MeasurableSpace (α i)} :
MeasurableSpace.pi = MeasurableSpace.generateFrom {B : Set ((x : ι) → α x) | ∃ (i : ι) (A : Set (α i)), MeasurableSet A Function.eval i ⁻¹' A = B}
theorem IsPiSystem.pi {ι : Type u_1} {α : ιType u_3} {C : (i : ι) → Set (Set (α i))} (hC : ∀ (i : ι), IsPiSystem (C i)) :
IsPiSystem (Set.univ.pi '' Set.univ.pi C)

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

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

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
Instances For
    theorem MeasureTheory.piPremeasure_pi {ι : Type u_1} {α : ιType u_3} [Fintype ι] {m : (i : ι) → MeasureTheory.OuterMeasure (α i)} {s : (i : ι) → Set (α i)} (hs : (Set.univ.pi s).Nonempty) :
    MeasureTheory.piPremeasure m (Set.univ.pi s) = 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.univ.pi s) = 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) :
    theorem MeasureTheory.piPremeasure_pi_eval {ι : Type u_1} {α : ιType u_3} [Fintype ι] {m : (i : ι) → MeasureTheory.OuterMeasure (α i)} {s : Set ((i : ι) → α i)} :
    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
    Instances For
      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.univ.pi s) 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.univ.pi s).Nonemptyn (Set.univ.pi s) i : ι, (m i) (s i)
      def MeasureTheory.Measure.tprod {δ : Type u_4} {π : δType u_5} [(x : δ) → MeasurableSpace (π x)] (l : List δ) (μ : (i : δ) → MeasureTheory.Measure (π i)) :

      A product of measures in tprod α l.

      Equations
      Instances For
        @[simp]
        theorem MeasureTheory.Measure.tprod_nil {δ : Type u_4} {π : δType u_5} [(x : δ) → MeasurableSpace (π x)] (μ : (i : δ) → MeasureTheory.Measure (π i)) :
        @[simp]
        theorem MeasureTheory.Measure.tprod_cons {δ : Type u_4} {π : δType u_5} [(x : δ) → MeasurableSpace (π x)] (i : δ) (l : List δ) (μ : (i : δ) → MeasureTheory.Measure (π i)) :
        instance MeasureTheory.Measure.sigmaFinite_tprod {δ : Type u_4} {π : δType u_5} [(x : δ) → MeasurableSpace (π x)] (l : List δ) (μ : (i : δ) → MeasureTheory.Measure (π i)) [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] :
        Equations
        • =
        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.map (fun (i : δ) => (μ i) (s i)) l).prod
        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
        Instances For
          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.univ.pi s) = 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.pi fun (i : ι) => (μ i).toOuterMeasure).caratheodory
          @[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
          Instances For
            theorem MeasureTheory.Measure.pi_def {ι : Type u_4} {α : ιType u_5} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) :
            MeasureTheory.Measure.pi μ = (MeasureTheory.OuterMeasure.pi fun (i : ι) => (μ i).toOuterMeasure).toMeasure
            instance MeasureTheory.MeasureSpace.pi {ι : Type u_1} [Fintype ι] {α : ιType u_4} [(i : ι) → MeasureTheory.MeasureSpace (α i)] :
            MeasureTheory.MeasureSpace ((i : ι) → α i)
            Equations
            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.univ.pi s) = 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 : ι) → (μ i).FiniteSpanningSetsIn (C i)) :
            (MeasureTheory.Measure.pi μ).FiniteSpanningSetsIn (Set.univ.pi '' Set.univ.pi C)

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

            Equations
            Instances For
              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 : ι) → (μ i).FiniteSpanningSetsIn (C i)) {μν : MeasureTheory.Measure ((i : ι) → α i)} (h₁ : ∀ (s : (i : ι) → Set (α i)), (∀ (i : ι), s i C i)μν (Set.univ.pi s) = i : ι, (μ i) (s i)) :

              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.univ.pi s) = i : ι, (μ i) (s i)) :

              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 ι] :
              @[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.univ.pi s) = 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 = 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) = 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) = 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)] :
              Equations
              • =
              instance MeasureTheory.Measure.instSigmaFiniteForallVolume {ι : Type u_1} [Fintype ι] {α : ιType u_4} [(i : ι) → MeasureTheory.MeasureSpace (α i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] :
              MeasureTheory.SigmaFinite MeasureTheory.volume
              Equations
              • =
              instance MeasureTheory.Measure.pi.instIsFiniteMeasure {ι : Type u_1} {α : ιType u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] :
              Equations
              • =
              instance MeasureTheory.Measure.instIsFiniteMeasureForallVolume {ι : Type u_1} [Fintype ι] {α : ιType u_4} [(i : ι) → MeasureTheory.MeasureSpace (α i)] [∀ (i : ι), MeasureTheory.IsFiniteMeasure MeasureTheory.volume] :
              MeasureTheory.IsFiniteMeasure MeasureTheory.volume
              Equations
              • =
              instance MeasureTheory.Measure.pi.instIsProbabilityMeasure {ι : Type u_1} {α : ιType u_3} [Fintype ι] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] :
              Equations
              • =
              instance MeasureTheory.Measure.instIsProbabilityMeasureForallVolume {ι : Type u_1} [Fintype ι] {α : ιType u_4} [(i : ι) → MeasureTheory.MeasureSpace (α i)] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] :
              Equations
              • =
              theorem MeasureTheory.Measure.pi_of_empty {α : Type u_4} [Fintype α] [IsEmpty α] {β : αType u_5} {m : (a : α) → MeasurableSpace (β a)} (μ : (a : α) → MeasureTheory.Measure (β a)) (x : optParam ((a : α) → β a) fun (a : α) => isEmptyElim a) :
              theorem MeasureTheory.Measure.volume_pi_eq_dirac {ι : Type u_4} [Fintype ι] [IsEmpty ι] {α : ιType u_5} [(i : ι) → MeasureTheory.MeasureSpace (α i)] (x : optParam ((a : ι) → α a) fun (a : ι) => isEmptyElim a) :
              MeasureTheory.volume = MeasureTheory.Measure.dirac x
              @[simp]
              theorem MeasureTheory.Measure.pi_empty_univ {α : Type u_4} [Fintype α] [IsEmpty α] {β : αType u_5} {m : (α : α) → MeasurableSpace (β α)} (μ : (a : α) → MeasureTheory.Measure (β a)) :
              (MeasureTheory.Measure.pi μ) Set.univ = 1
              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) :
              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 : (i : ι) → α i | 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 : ι} :
              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)] :
              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 =ᵐ[μ i] f' i) :
              (fun (x : (i : ι) → α i) (i : ι) => f i (x i)) =ᵐ[MeasureTheory.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 : ι) → 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 ≤ᵐ[μ i] f' i) :
              (fun (x : (i : ι) → α i) (i : ι) => f i (x i)) ≤ᵐ[MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {I : Set ι} {s : (i : ι) → Set (α i)} {t : (i : ι) → Set (α i)} (h : iI, s i ≤ᵐ[μ i] t i) :
              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 : iI, s i =ᵐ[μ i] t i) :
              theorem MeasureTheory.Measure.pi_map_piCongrLeft {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [hι' : Fintype ι'] (e : ι ι') {β : ι'Type u_4} [(i : ι') → MeasurableSpace (β i)] (μ : (i : ι') → MeasureTheory.Measure (β i)) [∀ (i : ι'), MeasureTheory.SigmaFinite (μ i)] :
              theorem MeasureTheory.Measure.pi_map_piOptionEquivProd {ι : Type u_1} [Fintype ι] {β : Option ιType u_4} [(i : Option ι) → MeasurableSpace (β i)] (μ : (i : Option ι) → MeasureTheory.Measure (β i)) [∀ (i : Option ι), MeasureTheory.SigmaFinite (μ i)] :
              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} :
              (s.pi fun (i : ι) => Set.Iio (f i)) =ᵐ[MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {s : Set ι} {f : (i : ι) → α i} :
              (s.pi fun (i : ι) => Set.Ioi (f i)) =ᵐ[MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {f : (i : ι) → α i} :
              (Set.univ.pi fun (i : ι) => Set.Iio (f i)) =ᵐ[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.univ.pi fun (i : ι) => Set.Ioi (f i)) =ᵐ[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} :
              (s.pi fun (i : ι) => Set.Ioo (f i) (g i)) =ᵐ[MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {s : Set ι} {f : (i : ι) → α i} {g : (i : ι) → α i} :
              (s.pi fun (i : ι) => Set.Ioo (f i) (g i)) =ᵐ[MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {f : (i : ι) → α i} {g : (i : ι) → α i} :
              (Set.univ.pi fun (i : ι) => Set.Ioo (f i) (g i)) =ᵐ[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} :
              (s.pi fun (i : ι) => Set.Ioc (f i) (g i)) =ᵐ[MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {f : (i : ι) → α i} {g : (i : ι) → α i} :
              (Set.univ.pi fun (i : ι) => Set.Ioc (f i) (g i)) =ᵐ[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} :
              (s.pi fun (i : ι) => Set.Ico (f i) (g i)) =ᵐ[MeasureTheory.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 : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NoAtoms (μ i)] {f : (i : ι) → α i} {g : (i : ι) → α i} :
              (Set.univ.pi fun (i : ι) => Set.Ico (f i) (g i)) =ᵐ[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)] :

              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)] :
              Equations
              • =
              instance MeasureTheory.Measure.instNoAtomsForallVolumeOfNonemptyOfSigmaFinite {ι : 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
              • =
              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)] :
              Equations
              • =
              instance MeasureTheory.Measure.instIsLocallyFiniteMeasureForallVolumeOfSigmaFinite {ι : 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] :
              Equations
              • =
              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 : ι), (μ i).IsAddLeftInvariant] :
              (MeasureTheory.Measure.pi μ).IsAddLeftInvariant
              Equations
              • =
              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 : ι), (μ i).IsMulLeftInvariant] :
              (MeasureTheory.Measure.pi μ).IsMulLeftInvariant
              Equations
              • =
              instance MeasureTheory.Measure.instIsAddLeftInvariantForallVolumeOfMeasurableAddOfSigmaFinite {ι : 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.volume.IsAddLeftInvariant] :
              MeasureTheory.volume.IsAddLeftInvariant
              Equations
              • =
              instance MeasureTheory.Measure.instIsMulLeftInvariantForallVolumeOfMeasurableMulOfSigmaFinite {ι : 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.volume.IsMulLeftInvariant] :
              MeasureTheory.volume.IsMulLeftInvariant
              Equations
              • =
              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 : ι), (μ i).IsAddRightInvariant] :
              (MeasureTheory.Measure.pi μ).IsAddRightInvariant
              Equations
              • =
              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 : ι), (μ i).IsMulRightInvariant] :
              (MeasureTheory.Measure.pi μ).IsMulRightInvariant
              Equations
              • =
              instance MeasureTheory.Measure.instIsAddRightInvariantForallVolumeOfMeasurableAddOfSigmaFinite {ι : 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.volume.IsAddRightInvariant] :
              MeasureTheory.volume.IsAddRightInvariant
              Equations
              • =
              instance MeasureTheory.Measure.instIsMulRightInvariantForallVolumeOfMeasurableMulOfSigmaFinite {ι : 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.volume.IsMulRightInvariant] :
              MeasureTheory.volume.IsMulRightInvariant
              Equations
              • =
              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 : ι), (μ i).IsNegInvariant] :
              (MeasureTheory.Measure.pi μ).IsNegInvariant
              Equations
              • =
              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 : ι), (μ i).IsInvInvariant] :
              (MeasureTheory.Measure.pi μ).IsInvInvariant
              Equations
              • =
              instance MeasureTheory.Measure.instIsNegInvariantForallVolumeOfMeasurableNegOfSigmaFinite {ι : 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.volume.IsNegInvariant] :
              MeasureTheory.volume.IsNegInvariant
              Equations
              • =
              instance MeasureTheory.Measure.instIsInvInvariantForallVolumeOfMeasurableInvOfSigmaFinite {ι : 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.volume.IsInvInvariant] :
              MeasureTheory.volume.IsInvInvariant
              Equations
              • =
              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 : ι), (μ i).IsOpenPosMeasure] :
              (MeasureTheory.Measure.pi μ).IsOpenPosMeasure
              Equations
              • =
              instance MeasureTheory.Measure.instIsOpenPosMeasureForallVolumeOfSigmaFinite {ι : Type u_1} [Fintype ι] {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasureTheory.MeasureSpace (X i)] [∀ (i : ι), MeasureTheory.volume.IsOpenPosMeasure] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] :
              MeasureTheory.volume.IsOpenPosMeasure
              Equations
              • =
              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)] :
              Equations
              • =
              instance MeasureTheory.Measure.instIsFiniteMeasureOnCompactsForallVolumeOfSigmaFinite {ι : 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] :
              Equations
              • =
              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 : ι), (μ i).IsAddHaarMeasure] [∀ (i : ι), MeasurableAdd (α i)] :
              (MeasureTheory.Measure.pi μ).IsAddHaarMeasure
              Equations
              • =
              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 : ι), (μ i).IsHaarMeasure] [∀ (i : ι), MeasurableMul (α i)] :
              (MeasureTheory.Measure.pi μ).IsHaarMeasure
              Equations
              • =
              instance MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite {ι : 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.volume.IsAddHaarMeasure] :
              MeasureTheory.volume.IsAddHaarMeasure
              Equations
              • =
              instance MeasureTheory.Measure.instIsHaarMeasureForallVolumeOfMeasurableMulOfSigmaFinite {ι : 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.volume.IsHaarMeasure] :
              MeasureTheory.volume.IsHaarMeasure
              Equations
              • =
              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.univ.pi s) = 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) = 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) = 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.volume.IsAddLeftInvariant] :
              MeasureTheory.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.

              Equations
              • =
              instance MeasureTheory.Pi.isMulLeftInvariant_volume {ι : Type u_1} [Fintype ι] {α : Type u_4} [Group α] [MeasureTheory.MeasureSpace α] [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasurableMul α] [MeasureTheory.volume.IsMulLeftInvariant] :
              MeasureTheory.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.

              Equations
              • =
              instance MeasureTheory.Pi.isNegInvariant_volume {ι : Type u_1} [Fintype ι] {α : Type u_4} [AddGroup α] [MeasureTheory.MeasureSpace α] [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasurableNeg α] [MeasureTheory.volume.IsNegInvariant] :
              MeasureTheory.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.

              Equations
              • =
              instance MeasureTheory.Pi.isInvInvariant_volume {ι : Type u_1} [Fintype ι] {α : Type u_4} [Group α] [MeasureTheory.MeasureSpace α] [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasurableInv α] [MeasureTheory.volume.IsInvInvariant] :
              MeasureTheory.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.

              Equations
              • =

              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 : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (p : ιProp) [DecidablePred p] :
              theorem MeasureTheory.volume_preserving_piEquivPiSubtypeProd {ι : Type u_1} [Fintype ι] (α : ιType u_4) [(i : ι) → MeasureTheory.MeasureSpace (α i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] (p : ιProp) [DecidablePred p] :
              MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p)) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.measurePreserving_piCongrLeft {ι : Type u_1} {ι' : Type u_2} {α : ιType u_3} [Fintype ι] {m : (i : ι) → MeasurableSpace (α i)} (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [Fintype ι'] (f : ι' ι) :
              theorem MeasureTheory.volume_measurePreserving_piCongrLeft {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] (α : ιType u_4) (f : ι' ι) [(i : ι) → MeasureTheory.MeasureSpace (α i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] :
              MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piCongrLeft α f)) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.measurePreserving_sumPiEquivProdPi_symm {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {π : ι ι'Type u_4} {m : (i : ι ι') → MeasurableSpace (π i)} (μ : (i : ι ι') → MeasureTheory.Measure (π i)) [∀ (i : ι ι'), MeasureTheory.SigmaFinite (μ i)] :
              theorem MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] (π : ι ι'Type u_4) [(i : ι ι') → MeasureTheory.MeasureSpace (π i)] [∀ (i : ι ι'), MeasureTheory.SigmaFinite MeasureTheory.volume] :
              MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi π).symm) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.measurePreserving_sumPiEquivProdPi {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {π : ι ι'Type u_4} {_m : (i : ι ι') → MeasurableSpace (π i)} (μ : (i : ι ι') → MeasureTheory.Measure (π i)) [∀ (i : ι ι'), MeasureTheory.SigmaFinite (μ i)] :
              theorem MeasureTheory.volume_measurePreserving_sumPiEquivProdPi {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] (π : ι ι'Type u_4) [(i : ι ι') → MeasureTheory.MeasureSpace (π i)] [∀ (i : ι ι'), MeasureTheory.SigmaFinite MeasureTheory.volume] :
              MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi π)) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.measurePreserving_piFinSuccAbove {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)) :
              theorem MeasureTheory.volume_preserving_piFinSuccAbove {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.piFinSuccAbove α i)) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.measurePreserving_piUnique {ι : Type u_1} [Fintype ι] {π : ιType u_4} [Unique ι] {m : (i : ι) → MeasurableSpace (π i)} (μ : (i : ι) → MeasureTheory.Measure (π i)) :
              theorem MeasureTheory.volume_preserving_piUnique {ι : Type u_1} [Fintype ι] (π : ιType u_4) [Unique ι] [(i : ι) → MeasureTheory.MeasureSpace (π i)] :
              MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piUnique π)) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.volume_preserving_funUnique (α : Type u) (β : Type v) [Unique α] [MeasureTheory.MeasureSpace β] :
              MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.funUnique α β)) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.measurePreserving_piFinTwo {α : Fin 2Type u} {m : (i : Fin 2) → MeasurableSpace (α i)} (μ : (i : Fin 2) → MeasureTheory.Measure (α i)) [∀ (i : Fin 2), MeasureTheory.SigmaFinite (μ i)] :
              theorem MeasureTheory.volume_preserving_piFinTwo (α : Fin 2Type u) [(i : Fin 2) → MeasureTheory.MeasureSpace (α i)] [∀ (i : Fin 2), MeasureTheory.SigmaFinite MeasureTheory.volume] :
              MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.measurePreserving_finTwoArrow_vec {α : Type u} :
              ∀ {x : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] [inst : MeasureTheory.SigmaFinite ν], MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (MeasureTheory.Measure.pi ![μ, ν]) (μ.prod ν)
              theorem MeasureTheory.measurePreserving_finTwoArrow {α : Type u} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] :
              MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (MeasureTheory.Measure.pi fun (x : Fin 2) => μ) (μ.prod μ)
              theorem MeasureTheory.volume_preserving_finTwoArrow (α : Type u) [MeasureTheory.MeasureSpace α] [MeasureTheory.SigmaFinite MeasureTheory.volume] :
              MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.volume_preserving_pi_empty {ι : Type u} (α : ιType v) [Fintype ι] [IsEmpty ι] [(i : ι) → MeasureTheory.MeasureSpace (α i)] :
              MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.measurePreserving_piFinsetUnion {ι : Type u_4} {α : ιType u_5} :
              ∀ {x : (i : ι) → MeasurableSpace (α i)} [inst : DecidableEq ι] {s t : Finset ι} (h : Disjoint s t) (μ : (i : ι) → MeasureTheory.Measure (α i)) [inst_1 : ∀ (i : ι), MeasureTheory.SigmaFinite (μ i)], MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinsetUnion α h)) ((MeasureTheory.Measure.pi fun (i : { x : ι // x s }) => μ i).prod (MeasureTheory.Measure.pi fun (i : { x : ι // x t }) => μ i)) (MeasureTheory.Measure.pi fun (i : { x : ι // x s t }) => μ i)
              theorem MeasureTheory.volume_preserving_piFinsetUnion {ι : Type u_4} [DecidableEq ι] (α : ιType u_5) {s : Finset ι} {t : Finset ι} (h : Disjoint s t) [(i : ι) → MeasureTheory.MeasureSpace (α i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] :
              MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinsetUnion α h)) MeasureTheory.volume MeasureTheory.volume
              theorem MeasureTheory.measurePreserving_pi {ι : Type u_4} [Fintype ι] {α : ιType v} {β : ιType u_5} [(i : ι) → MeasureTheory.MeasureSpace (α i)] [(i : ι) → MeasurableSpace (β i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) (ν : (i : ι) → MeasureTheory.Measure (β i)) {f : (i : ι) → α iβ i} [∀ (i : ι), MeasureTheory.SigmaFinite (ν i)] (hf : ∀ (i : ι), MeasureTheory.MeasurePreserving (f i) (μ i) (ν i)) :
              MeasureTheory.MeasurePreserving (fun (a : (i : ι) → α i) (i : ι) => f i (a i)) (MeasureTheory.Measure.pi μ) (MeasureTheory.Measure.pi ν)
              theorem MeasureTheory.volume_preserving_pi {ι : Type u_1} [Fintype ι] {α' : ιType u_4} {β' : ιType u_5} [(i : ι) → MeasureTheory.MeasureSpace (α' i)] [(i : ι) → MeasureTheory.MeasureSpace (β' i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] {f : (i : ι) → α' iβ' i} (hf : ∀ (i : ι), MeasureTheory.MeasurePreserving (f i) MeasureTheory.volume MeasureTheory.volume) :
              MeasureTheory.MeasurePreserving (fun (a : (i : ι) → α' i) (i : ι) => f i (a i)) MeasureTheory.volume MeasureTheory.volume