Documentation

Mathlib.MeasureTheory.Constructions.Prod.Basic

The product measure #

In this file we define and prove properties about the binary product measure. If α and β have s-finite measures μ resp. ν then α × β can be equipped with a s-finite measure μ.prod ν that satisfies (μ.prod ν) s = ∫⁻ x, ν {y | (x, y) ∈ s} ∂μ. We also have (μ.prod ν) (s ×ˢ t) = μ s * ν t, i.e. the measure of a rectangle is the product of the measures of the sides.

We also prove Tonelli's theorem.

Main definition #

Main results #

Implementation Notes #

Many results are proven twice, once for functions in curried form (α → β → γ) and one for functions in uncurried form (α × β → γ). The former often has an assumption Measurable (uncurry f), which could be inconvenient to discharge, but for the latter it is more common that the function has to be given explicitly, since Lean cannot synthesize the function by itself. We name the lemmas about the uncurried form with a prime. Tonelli's theorem has a different naming scheme, since the version for the uncurried version is reversed.

Tags #

product measure, Tonelli's theorem, Fubini-Tonelli theorem

theorem IsPiSystem.prod {α : Type u_1} {β : Type u_3} {C : Set (Set α)} {D : Set (Set β)} (hC : IsPiSystem C) (hD : IsPiSystem D) :
IsPiSystem (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) C D)

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

theorem IsCountablySpanning.prod {α : Type u_1} {β : Type u_3} {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C) (hD : IsCountablySpanning D) :
IsCountablySpanning (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) C D)

Rectangles of countably spanning sets are countably spanning.

Measurability #

Before we define the product measure, we can talk about the measurability of operations on binary functions. We show that if f is a binary measurable function, then the function that integrates along one of the variables (using either the Lebesgue or Bochner integral) is measurable.

theorem generateFrom_prod_eq {α : Type u_7} {β : Type u_8} {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C) (hD : IsCountablySpanning D) :
Prod.instMeasurableSpace = MeasurableSpace.generateFrom (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) C D)

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

theorem generateFrom_eq_prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {C : Set (Set α)} {D : Set (Set β)} (hC : MeasurableSpace.generateFrom C = inst✝¹) (hD : MeasurableSpace.generateFrom D = inst✝) (h2C : IsCountablySpanning C) (h2D : IsCountablySpanning D) :
MeasurableSpace.generateFrom (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) C D) = Prod.instMeasurableSpace

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

theorem generateFrom_prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] :
MeasurableSpace.generateFrom (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t}) = Prod.instMeasurableSpace

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

theorem isPiSystem_prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] :
IsPiSystem (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})

Rectangles form a π-system.

theorem measurable_measure_prod_mk_left_finite {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} [MeasureTheory.IsFiniteMeasure ν] {s : Set (α × β)} (hs : MeasurableSet s) :
Measurable fun (x : α) => ν (Prod.mk x ⁻¹' s)

If ν is a finite measure, and s ⊆ α × β is measurable, then x ↦ ν { y | (x, y) ∈ s } is a measurable function. measurable_measure_prod_mk_left is strictly more general.

theorem measurable_measure_prod_mk_left {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) :
Measurable fun (x : α) => ν (Prod.mk x ⁻¹' s)

If ν is an s-finite measure, and s ⊆ α × β is measurable, then x ↦ ν { y | (x, y) ∈ s } is a measurable function.

theorem measurable_measure_prod_mk_right {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {s : Set (α × β)} (hs : MeasurableSet s) :
Measurable fun (y : β) => μ ((fun (x : α) => (x, y)) ⁻¹' s)

If μ is a σ-finite measure, and s ⊆ α × β is measurable, then y ↦ μ { x | (x, y) ∈ s } is a measurable function.

theorem Measurable.map_prod_mk_right {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] :
Measurable fun (y : β) => MeasureTheory.Measure.map (fun (x : α) => (x, y)) μ
theorem MeasurableEmbedding.prod_mk {α : Type u_7} {β : Type u_8} {γ : Type u_9} {δ : Type u_10} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : αβ} {g : γδ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
MeasurableEmbedding fun (x : γ × α) => (g x.1, f x.2)
theorem MeasurableEmbedding.prod_mk_left {α : Type u_1} [MeasurableSpace α] {β : Type u_7} {γ : Type u_8} [MeasurableSingletonClass α] {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (x : α) {f : γβ} (hf : MeasurableEmbedding f) :
MeasurableEmbedding fun (y : γ) => (x, f y)
theorem MeasurableEmbedding.prod_mk_right {α : Type u_1} [MeasurableSpace α] {β : Type u_7} {γ : Type u_8} [MeasurableSingletonClass α] {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : γβ} (hf : MeasurableEmbedding f) (x : α) :
MeasurableEmbedding fun (y : γ) => (f y, x)
theorem measurableEmbedding_prod_mk_right {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] (x : α) :
MeasurableEmbedding fun (y : β) => (y, x)
theorem Measurable.lintegral_prod_right' {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : α × βENNReal} :
Measurable fMeasurable fun (x : α) => ∫⁻ (y : β), f (x, y)ν

The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of) Tonelli's theorem is measurable.

theorem Measurable.lintegral_prod_right {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : αβENNReal} (hf : Measurable (Function.uncurry f)) :
Measurable fun (x : α) => ∫⁻ (y : β), f x yν

The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of) Tonelli's theorem is measurable. This version has the argument f in curried form.

theorem Measurable.lintegral_prod_left' {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {f : α × βENNReal} (hf : Measurable f) :
Measurable fun (y : β) => ∫⁻ (x : α), f (x, y)μ

The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of) the symmetric version of Tonelli's theorem is measurable.

theorem Measurable.lintegral_prod_left {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {f : αβENNReal} (hf : Measurable (Function.uncurry f)) :
Measurable fun (y : β) => ∫⁻ (x : α), f x yμ

The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of) the symmetric version of Tonelli's theorem is measurable. This version has the argument f in curried form.

The product measure #

theorem MeasureTheory.Measure.prod_def {α : Type u_7} {β : Type u_8} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β) :
μ.prod ν = μ.bind fun (x : α) => MeasureTheory.Measure.map (Prod.mk x) ν
@[irreducible]

The binary product of measures. They are defined for arbitrary measures, but we basically prove all properties under the assumption that at least one of them is s-finite.

Equations
Instances For
    Equations
    theorem MeasureTheory.Measure.volume_eq_prod (α : Type u_7) (β : Type u_8) [MeasureTheory.MeasureSpace α] [MeasureTheory.MeasureSpace β] :
    MeasureTheory.volume = MeasureTheory.volume.prod MeasureTheory.volume
    theorem MeasureTheory.Measure.prod_apply {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) :
    (μ.prod ν) s = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s)μ
    @[simp]
    theorem MeasureTheory.Measure.prod_prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (s : Set α) (t : Set β) :
    (μ.prod ν) (s ×ˢ t) = μ s * ν t

    The product measure of the product of two sets is the product of their measures. Note that we do not need the sets to be measurable.

    @[simp]
    theorem MeasureTheory.Measure.map_fst_prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] :
    MeasureTheory.Measure.map Prod.fst (μ.prod ν) = ν Set.univ μ
    @[simp]
    theorem MeasureTheory.Measure.map_snd_prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] :
    MeasureTheory.Measure.map Prod.snd (μ.prod ν) = μ Set.univ ν
    instance MeasureTheory.Measure.prod.instIsOpenPosMeasure {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [TopologicalSpace Y] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {m' : MeasurableSpace Y} {ν : MeasureTheory.Measure Y} [ν.IsOpenPosMeasure] [MeasureTheory.SFinite ν] :
    (μ.prod ν).IsOpenPosMeasure
    Equations
    • =
    instance MeasureTheory.Measure.instIsOpenPosMeasureProdVolumeOfSFinite {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [MeasureTheory.MeasureSpace X] [MeasureTheory.volume.IsOpenPosMeasure] [TopologicalSpace Y] [MeasureTheory.MeasureSpace Y] [MeasureTheory.volume.IsOpenPosMeasure] [MeasureTheory.SFinite MeasureTheory.volume] :
    MeasureTheory.volume.IsOpenPosMeasure
    Equations
    • =
    theorem MeasureTheory.Measure.ae_measure_lt_top {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) (h2s : (μ.prod ν) s ) :
    ∀ᵐ (x : α) ∂μ, ν (Prod.mk x ⁻¹' s) <
    theorem MeasureTheory.Measure.measure_prod_null {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) :
    (μ.prod ν) s = 0 (fun (x : α) => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0

    Note: the assumption hs cannot be dropped. For a counterexample, see Walter Rudin Real and Complex Analysis, example (c) in section 8.9.

    theorem MeasureTheory.Measure.measure_ae_null_of_prod_null {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)} (h : (μ.prod ν) s = 0) :
    (fun (x : α) => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0

    Note: the converse is not true without assuming that s is measurable. For a counterexample, see Walter Rudin Real and Complex Analysis, example (c) in section 8.9.

    theorem MeasureTheory.Measure.AbsolutelyContinuous.prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {μ' : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {ν' : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite ν'] (h1 : μ.AbsolutelyContinuous μ') (h2 : ν.AbsolutelyContinuous ν') :
    (μ.prod ν).AbsolutelyContinuous (μ'.prod ν')
    theorem MeasureTheory.Measure.ae_ae_of_ae_prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {p : α × βProp} (h : ∀ᵐ (z : α × β) ∂μ.prod ν, p z) :
    ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p (x, y)

    Note: the converse is not true. For a counterexample, see Walter Rudin Real and Complex Analysis, example (c) in section 8.9. It is true if the set is measurable, see ae_prod_mem_iff_ae_ae_mem.

    theorem MeasureTheory.Measure.ae_ae_eq_curry_of_prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {γ : Type u_7} {f : α × βγ} {g : α × βγ} (h : f =ᵐ[μ.prod ν] g) :
    ∀ᵐ (x : α) ∂μ, Function.curry f x =ᵐ[ν] Function.curry g x
    theorem MeasureTheory.Measure.ae_ae_eq_of_ae_eq_uncurry {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {γ : Type u_7} {f : αβγ} {g : αβγ} (h : Function.uncurry f =ᵐ[μ.prod ν] Function.uncurry g) :
    ∀ᵐ (x : α) ∂μ, f x =ᵐ[ν] g x
    theorem MeasureTheory.Measure.ae_prod_iff_ae_ae {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {p : α × βProp} (hp : MeasurableSet {x : α × β | p x}) :
    (∀ᵐ (z : α × β) ∂μ.prod ν, p z) ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p (x, y)
    theorem MeasureTheory.Measure.ae_prod_mem_iff_ae_ae_mem {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)} (hs : MeasurableSet s) :
    (∀ᵐ (z : α × β) ∂μ.prod ν, z s) ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, (x, y) s
    theorem MeasureTheory.Measure.set_prod_ae_eq {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set α} {s' : Set α} {t : Set β} {t' : Set β} (hs : s =ᵐ[μ] s') (ht : t =ᵐ[ν] t') :
    s ×ˢ t =ᵐ[μ.prod ν] s' ×ˢ t'
    theorem MeasureTheory.Measure.measure_prod_compl_eq_zero {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set α} {t : Set β} (s_ae_univ : μ s = 0) (t_ae_univ : ν t = 0) :
    (μ.prod ν) (s ×ˢ t) = 0

    If s ×ˢ t is a null measurable set and μ s ≠ 0, then t is a null measurable set.

    If Prod.snd ⁻¹' t is a null measurable set and μ ≠ 0, then t is a null measurable set.

    Prod.snd ⁻¹' t is null measurable w.r.t. μ.prod ν iff t is null measurable w.r.t. ν provided that μ ≠ 0.

    noncomputable def MeasureTheory.Measure.FiniteSpanningSetsIn.prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {C : Set (Set α)} {D : Set (Set β)} (hμ : μ.FiniteSpanningSetsIn C) (hν : ν.FiniteSpanningSetsIn D) :
    (μ.prod ν).FiniteSpanningSetsIn (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) C D)

    μ.prod ν has finite spanning sets in rectangles of finite spanning sets.

    Equations
    • .prod = { set := fun (n : ) => .set (Nat.unpair n).1 ×ˢ .set (Nat.unpair n).2, set_mem := , finite := , spanning := }
    Instances For
      theorem MeasureTheory.Measure.prod_sum_left {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ι : Type u_7} (m : ιMeasureTheory.Measure α) (μ : MeasureTheory.Measure β) [MeasureTheory.SFinite μ] :
      (MeasureTheory.Measure.sum m).prod μ = MeasureTheory.Measure.sum fun (i : ι) => (m i).prod μ
      theorem MeasureTheory.Measure.prod_sum_right {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ι' : Type u_7} [Countable ι'] (m : MeasureTheory.Measure α) (m' : ι'MeasureTheory.Measure β) [∀ (n : ι'), MeasureTheory.SFinite (m' n)] :
      m.prod (MeasureTheory.Measure.sum m') = MeasureTheory.Measure.sum fun (p : ι') => m.prod (m' p)
      theorem MeasureTheory.Measure.prod_sum {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ι : Type u_7} {ι' : Type u_8} [Countable ι'] (m : ιMeasureTheory.Measure α) (m' : ι'MeasureTheory.Measure β) [∀ (n : ι'), MeasureTheory.SFinite (m' n)] :
      (MeasureTheory.Measure.sum m).prod (MeasureTheory.Measure.sum m') = MeasureTheory.Measure.sum fun (p : ι × ι') => (m p.1).prod (m' p.2)
      Equations
      • =
      instance MeasureTheory.Measure.prod.instSFinite {α : Type u_7} {β : Type u_8} :
      Equations
      • =
      Equations
      • =
      instance MeasureTheory.Measure.instSFiniteProdVolume {α : Type u_7} {β : Type u_8} [MeasureTheory.MeasureSpace α] [MeasureTheory.SFinite MeasureTheory.volume] [MeasureTheory.MeasureSpace β] [MeasureTheory.SFinite MeasureTheory.volume] :
      MeasureTheory.SFinite MeasureTheory.volume
      Equations
      • =
      theorem MeasureTheory.Measure.prod_eq_generateFrom {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {C : Set (Set α)} {D : Set (Set β)} (hC : MeasurableSpace.generateFrom C = inst✝¹) (hD : MeasurableSpace.generateFrom D = inst✝) (h2C : IsPiSystem C) (h2D : IsPiSystem D) (h3C : μ.FiniteSpanningSetsIn C) (h3D : ν.FiniteSpanningSetsIn D) {μν : MeasureTheory.Measure (α × β)} (h₁ : sC, tD, μν (s ×ˢ t) = μ s * ν t) :
      μ.prod ν = μν

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

      theorem MeasureTheory.Measure.prod_eq {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite ν] {μν : MeasureTheory.Measure (α × β)} (h : ∀ (s : Set α) (t : Set β), MeasurableSet sMeasurableSet tμν (s ×ˢ t) = μ s * ν t) :
      μ.prod ν = μν

      A measure on a product space equals the product measure of sigma-finite measures if they are equal on rectangles.

      theorem MeasureTheory.Measure.prod_apply_symm {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set (α × β)} (hs : MeasurableSet s) :
      (μ.prod ν) s = ∫⁻ (y : β), μ ((fun (x : α) => (x, y)) ⁻¹' s)ν
      theorem MeasureTheory.Measure.ae_ae_comm {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {p : αβProp} (h : MeasurableSet {x : α × β | p x.1 x.2}) :
      (∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p x y) ∀ᵐ (y : β) ∂ν, ∀ᵐ (x : α) ∂μ, p x y

      If s ×ˢ t is a null measurable set and ν t ≠ 0, then s is a null measurable set.

      If Prod.fst ⁻¹' s is a null measurable set and ν ≠ 0, then s is a null measurable set.

      Prod.fst ⁻¹' s is null measurable w.r.t. μ.prod ν iff s is null measurable w.r.t. μ provided that ν ≠ 0.

      The product of two non-null sets is null measurable if and only if both of them are null measurable.

      The product of two sets is null measurable if and only if both of them are null measurable or one of them has measure zero.

      theorem MeasureTheory.Measure.prodAssoc_prod {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {τ : MeasureTheory.Measure γ} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite τ] :
      MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)

      The product of specific measures #

      theorem MeasureTheory.Measure.prod_restrict {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (s : Set α) (t : Set β) :
      (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
      theorem MeasureTheory.Measure.restrict_prod_eq_prod_univ {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (s : Set α) :
      (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ Set.univ)
      theorem MeasureTheory.Measure.prod_dirac {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (y : β) :
      μ.prod (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.map (fun (x : α) => (x, y)) μ
      theorem MeasureTheory.Measure.prod_add {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (ν' : MeasureTheory.Measure β) [MeasureTheory.SFinite ν'] :
      μ.prod (ν + ν') = μ.prod ν + μ.prod ν'
      theorem MeasureTheory.Measure.add_prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (μ' : MeasureTheory.Measure α) [MeasureTheory.SFinite μ'] :
      (μ + μ').prod ν = μ.prod ν + μ'.prod ν
      @[simp]
      theorem MeasureTheory.Measure.prod_zero {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) :
      μ.prod 0 = 0
      theorem MeasureTheory.Measure.map_prod_map {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {δ : Type u_7} [MeasurableSpace δ] {f : αβ} {g : γδ} (μa : MeasureTheory.Measure α) (μc : MeasureTheory.Measure γ) [MeasureTheory.SFinite μa] [MeasureTheory.SFinite μc] (hf : Measurable f) (hg : Measurable g) :
      theorem MeasureTheory.MeasurePreserving.skew_product {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {δ : Type u_7} [MeasurableSpace δ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {μd : MeasureTheory.Measure δ} [MeasureTheory.SFinite μa] [MeasureTheory.SFinite μc] {f : αβ} (hf : MeasureTheory.MeasurePreserving f μa μb) {g : αγδ} (hgm : Measurable (Function.uncurry g)) (hg : ∀ᵐ (a : α) ∂μa, MeasureTheory.Measure.map (g a) μc = μd) :
      MeasureTheory.MeasurePreserving (fun (p : α × γ) => (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)

      Let f : α → β be a measure preserving map. For a.e. all a, let g a : γ → δ be a measure preserving map. Also suppose that g is measurable as a function of two arguments. Then the map fun (a, c) ↦ (f a, g a c) is a measure preserving map for the product measures on α × γ and β × δ.

      Some authors call a map of the form fun (a, c) ↦ (f a, g a c) a skew product over f, thus the choice of a name.

      theorem MeasureTheory.MeasurePreserving.prod {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {δ : Type u_7} [MeasurableSpace δ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {μd : MeasureTheory.Measure δ} [MeasureTheory.SFinite μa] [MeasureTheory.SFinite μc] {f : αβ} {g : γδ} (hf : MeasureTheory.MeasurePreserving f μa μb) (hg : MeasureTheory.MeasurePreserving g μc μd) :
      MeasureTheory.MeasurePreserving (Prod.map f g) (μa.prod μc) (μb.prod μd)

      If f : α → β sends the measure μa to μb and g : γ → δ sends the measure μc to μd, then Prod.map f g sends μa.prod μc to μb.prod μd.

      theorem MeasureTheory.QuasiMeasurePreserving.prod_of_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : α × βγ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {τ : MeasureTheory.Measure γ} (hf : Measurable f) [MeasureTheory.SFinite ν] (h2f : ∀ᵐ (x : α) ∂μ, MeasureTheory.Measure.QuasiMeasurePreserving (fun (y : β) => f (x, y)) ν τ) :
      theorem MeasureTheory.QuasiMeasurePreserving.prod_of_left {α : Type u_7} {β : Type u_8} {γ : Type u_9} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : α × βγ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {τ : MeasureTheory.Measure γ} (hf : Measurable f) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (h2f : ∀ᵐ (y : β) ∂ν, MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => f (x, y)) μ τ) :
      theorem AEMeasurable.prod_swap {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {f : β × αγ} (hf : AEMeasurable f (ν.prod μ)) :
      AEMeasurable (fun (z : α × β) => f z.swap) (μ.prod ν)
      theorem AEMeasurable.fst {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : αγ} (hf : AEMeasurable f μ) :
      AEMeasurable (fun (z : α × β) => f z.1) (μ.prod ν)
      theorem AEMeasurable.snd {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : βγ} (hf : AEMeasurable f ν) :
      AEMeasurable (fun (z : α × β) => f z.2) (μ.prod ν)

      The Lebesgue integral on a product #

      theorem MeasureTheory.lintegral_prod_swap {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (f : α × βENNReal) :
      ∫⁻ (z : β × α), f z.swapν.prod μ = ∫⁻ (z : α × β), f zμ.prod ν
      theorem MeasureTheory.lintegral_prod_of_measurable {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (f : α × βENNReal) :
      Measurable f∫⁻ (z : α × β), f zμ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y)νμ

      Tonelli's Theorem: For ℝ≥0∞-valued measurable functions on α × β, the integral of f is equal to the iterated integral.

      theorem MeasureTheory.lintegral_prod {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (f : α × βENNReal) (hf : AEMeasurable f (μ.prod ν)) :
      ∫⁻ (z : α × β), f zμ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y)νμ

      Tonelli's Theorem: For ℝ≥0∞-valued almost everywhere measurable functions on α × β, the integral of f is equal to the iterated integral.

      theorem MeasureTheory.lintegral_prod_symm {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (f : α × βENNReal) (hf : AEMeasurable f (μ.prod ν)) :
      ∫⁻ (z : α × β), f zμ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y)μν

      The symmetric version of Tonelli's Theorem: For ℝ≥0∞-valued almost everywhere measurable functions on α × β, the integral of f is equal to the iterated integral, in reverse order.

      theorem MeasureTheory.lintegral_prod_symm' {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (f : α × βENNReal) (hf : Measurable f) :
      ∫⁻ (z : α × β), f zμ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y)μν

      The symmetric version of Tonelli's Theorem: For ℝ≥0∞-valued measurable functions on α × β, the integral of f is equal to the iterated integral, in reverse order.

      theorem MeasureTheory.lintegral_lintegral {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] ⦃f : αβENNReal (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) :
      ∫⁻ (x : α), ∫⁻ (y : β), f x yνμ = ∫⁻ (z : α × β), f z.1 z.2μ.prod ν

      The reversed version of Tonelli's Theorem. In this version f is in curried form, which makes it easier for the elaborator to figure out f automatically.

      theorem MeasureTheory.lintegral_lintegral_symm {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] ⦃f : αβENNReal (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) :
      ∫⁻ (x : α), ∫⁻ (y : β), f x yνμ = ∫⁻ (z : β × α), f z.2 z.1ν.prod μ

      The reversed version of Tonelli's Theorem (symmetric version). In this version f is in curried form, which makes it easier for the elaborator to figure out f automatically.

      theorem MeasureTheory.lintegral_lintegral_swap {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] ⦃f : αβENNReal (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) :
      ∫⁻ (x : α), ∫⁻ (y : β), f x yνμ = ∫⁻ (y : β), ∫⁻ (x : α), f x yμν

      Change the order of Lebesgue integration.

      theorem MeasureTheory.lintegral_prod_mul {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : αENNReal} {g : βENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) :
      ∫⁻ (z : α × β), f z.1 * g z.2μ.prod ν = (∫⁻ (x : α), f xμ) * ∫⁻ (y : β), g yν

      Marginals of a measure defined on a product #

      noncomputable def MeasureTheory.Measure.fst {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (ρ : MeasureTheory.Measure (α × β)) :

      Marginal measure on α obtained from a measure ρ on α × β, defined by ρ.map Prod.fst.

      Equations
      Instances For
        theorem MeasureTheory.Measure.fst_apply {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} {s : Set α} (hs : MeasurableSet s) :
        ρ.fst s = ρ (Prod.fst ⁻¹' s)
        theorem MeasureTheory.Measure.fst_univ {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} :
        ρ.fst Set.univ = ρ Set.univ
        theorem MeasureTheory.Measure.fst_map_prod_mk₀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {X : αβ} {Y : αγ} {μ : MeasureTheory.Measure α} (hY : AEMeasurable Y μ) :
        (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ).fst = MeasureTheory.Measure.map X μ
        theorem MeasureTheory.Measure.fst_map_prod_mk {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {X : αβ} {Y : αγ} {μ : MeasureTheory.Measure α} (hY : Measurable Y) :
        (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ).fst = MeasureTheory.Measure.map X μ
        theorem MeasureTheory.Measure.fst_mono {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} {μ : MeasureTheory.Measure (α × β)} (h : ρ μ) :
        ρ.fst μ.fst
        noncomputable def MeasureTheory.Measure.snd {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (ρ : MeasureTheory.Measure (α × β)) :

        Marginal measure on β obtained from a measure on ρ α × β, defined by ρ.map Prod.snd.

        Equations
        Instances For
          theorem MeasureTheory.Measure.snd_apply {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} {s : Set β} (hs : MeasurableSet s) :
          ρ.snd s = ρ (Prod.snd ⁻¹' s)
          theorem MeasureTheory.Measure.snd_univ {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} :
          ρ.snd Set.univ = ρ Set.univ
          theorem MeasureTheory.Measure.snd_map_prod_mk₀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {X : αβ} {Y : αγ} {μ : MeasureTheory.Measure α} (hX : AEMeasurable X μ) :
          (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ).snd = MeasureTheory.Measure.map Y μ
          theorem MeasureTheory.Measure.snd_map_prod_mk {α : Type u_1} {β : Type u_3} {γ : Type u_5} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {X : αβ} {Y : αγ} {μ : MeasureTheory.Measure α} (hX : Measurable X) :
          (MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ).snd = MeasureTheory.Measure.map Y μ
          theorem MeasureTheory.Measure.snd_mono {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} {μ : MeasureTheory.Measure (α × β)} (h : ρ μ) :
          ρ.snd μ.snd
          @[simp]
          theorem MeasureTheory.Measure.fst_map_swap {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} :
          (MeasureTheory.Measure.map Prod.swap ρ).fst = ρ.snd
          @[simp]
          theorem MeasureTheory.Measure.snd_map_swap {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {ρ : MeasureTheory.Measure (α × β)} :
          (MeasureTheory.Measure.map Prod.swap ρ).snd = ρ.fst