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 #
MeasureTheory.Measure.prod: The product of two measures.
Main results #
MeasureTheory.Measure.prod_applystatesμ.prod ν s = ∫⁻ x, ν {y | (x, y) ∈ s} ∂μfor measurables.MeasureTheory.Measure.prod_apply_symmis the reversed version.MeasureTheory.Measure.prod_prodstatesμ.prod ν (s ×ˢ t) = μ s * ν tfor measurable setssandt.MeasureTheory.lintegral_prod: Tonelli's theorem. It states that for a measurable functionα × β → ℝ≥0∞we have∫⁻ z, f z ∂(μ.prod ν) = ∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ. The version for functionsα → β → ℝ≥0∞is reversed, and calledlintegral_lintegral. Both versions have a variant with_symmappended, where the order of integration is reversed. The lemmaMeasurable.lintegral_prod_right'states that the inner integral of the right-hand side is measurable.
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
measurable_measure_prod_mk_left_finite
{α : Type u_1}
{β : Type u_2}
[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_2}
[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_2}
[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_left
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
:
Measurable fun (x : α) => MeasureTheory.Measure.map (Prod.mk x) ν
theorem
Measurable.map_prod_mk_right
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
:
Measurable fun (y : β) => MeasureTheory.Measure.map (fun (x : α) => (x, y)) μ
theorem
Measurable.lintegral_prod_right'
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{f : α × β → ENNReal}
:
Measurable 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.
theorem
Measurable.lintegral_prod_right
{α : Type u_1}
{β : Type u_2}
[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_2}
[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_2}
[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_4}
{β : Type u_5}
[MeasurableSpace α]
[MeasurableSpace β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure β)
:
μ.prod ν = μ.bind fun (x : α) => MeasureTheory.Measure.map (Prod.mk x) ν
@[irreducible]
def
MeasureTheory.Measure.prod
{α : Type u_4}
{β : Type u_5}
[MeasurableSpace α]
[MeasurableSpace β]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure β)
:
MeasureTheory.Measure (α × β)
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.
Instances For
instance
MeasureTheory.Measure.prod.measureSpace
{α : Type u_4}
{β : Type u_5}
[MeasureTheory.MeasureSpace α]
[MeasureTheory.MeasureSpace β]
:
MeasureTheory.MeasureSpace (α × β)
Equations
- MeasureTheory.Measure.prod.measureSpace = MeasureTheory.MeasureSpace.mk (MeasureTheory.volume.prod MeasureTheory.volume)
theorem
MeasureTheory.Measure.volume_eq_prod
(α : Type u_4)
(β : Type u_5)
[MeasureTheory.MeasureSpace α]
[MeasureTheory.MeasureSpace β]
:
MeasureTheory.volume = MeasureTheory.volume.prod MeasureTheory.volume
theorem
MeasureTheory.Measure.prod_apply
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{s : Set (α × β)}
(hs : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.Measure.prod_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
(s : Set α)
(t : Set β)
:
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_2}
[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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
:
MeasureTheory.Measure.map Prod.snd (μ.prod ν) = μ Set.univ • ν
instance
MeasureTheory.Measure.prod.instIsOpenPosMeasure
{X : Type u_4}
{Y : Type u_5}
[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_4}
{Y : Type u_5}
[TopologicalSpace X]
[MeasureTheory.MeasureSpace X]
[MeasureTheory.volume.IsOpenPosMeasure]
[TopologicalSpace Y]
[MeasureTheory.MeasureSpace Y]
[MeasureTheory.volume.IsOpenPosMeasure]
[MeasureTheory.SFinite MeasureTheory.volume]
:
MeasureTheory.volume.IsOpenPosMeasure
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.prod.instIsFiniteMeasure
{α : Type u_4}
{β : Type u_5}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure β)
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
MeasureTheory.IsFiniteMeasure (μ.prod ν)
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.instIsFiniteMeasureProdVolume
{α : Type u_4}
{β : Type u_5}
[MeasureTheory.MeasureSpace α]
[MeasureTheory.MeasureSpace β]
[MeasureTheory.IsFiniteMeasure MeasureTheory.volume]
[MeasureTheory.IsFiniteMeasure MeasureTheory.volume]
:
MeasureTheory.IsFiniteMeasure MeasureTheory.volume
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.prod.instIsProbabilityMeasure
{α : Type u_4}
{β : Type u_5}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure β)
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
:
MeasureTheory.IsProbabilityMeasure (μ.prod ν)
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.instIsProbabilityMeasureProdVolume
{α : Type u_4}
{β : Type u_5}
[MeasureTheory.MeasureSpace α]
[MeasureTheory.MeasureSpace β]
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
[MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
:
MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.prod.instIsFiniteMeasureOnCompacts
{α : Type u_4}
{β : Type u_5}
[TopologicalSpace α]
[TopologicalSpace β]
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure β)
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
[MeasureTheory.IsFiniteMeasureOnCompacts ν]
[MeasureTheory.SFinite ν]
:
MeasureTheory.IsFiniteMeasureOnCompacts (μ.prod ν)
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.instIsFiniteMeasureOnCompactsProdVolumeOfSFinite
{X : Type u_4}
{Y : Type u_5}
[TopologicalSpace X]
[MeasureTheory.MeasureSpace X]
[MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume]
[TopologicalSpace Y]
[MeasureTheory.MeasureSpace Y]
[MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume]
[MeasureTheory.SFinite MeasureTheory.volume]
:
MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.prod.instNoAtoms_fst
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.NoAtoms μ]
:
MeasureTheory.NoAtoms (μ.prod ν)
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.prod.instNoAtoms_snd
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.NoAtoms ν]
:
MeasureTheory.NoAtoms (μ.prod ν)
Equations
- ⋯ = ⋯
theorem
MeasureTheory.Measure.ae_measure_lt_top
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{s : Set (α × β)}
(hs : MeasurableSet s)
(h2s : (μ.prod ν) s ≠ ⊤)
:
theorem
MeasureTheory.Measure.measure_prod_null
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{s : Set (α × β)}
(hs : MeasurableSet s)
:
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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{s : Set (α × β)}
(h : (μ.prod ν) 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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ μ' : 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_2}
[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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{γ : Type u_4}
{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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{γ : Type u_4}
{f g : α → β → γ}
(h : Function.uncurry f =ᵐ[μ.prod ν] Function.uncurry g)
:
theorem
MeasureTheory.Measure.ae_prod_iff_ae_ae
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{p : α × β → Prop}
(hp : MeasurableSet {x : α × β | p x})
:
theorem
MeasureTheory.Measure.ae_prod_mem_iff_ae_ae_mem
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{s : Set (α × β)}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.quasiMeasurePreserving_fst
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
:
MeasureTheory.Measure.QuasiMeasurePreserving Prod.fst (μ.prod ν) μ
theorem
MeasureTheory.Measure.quasiMeasurePreserving_snd
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
:
MeasureTheory.Measure.QuasiMeasurePreserving Prod.snd (μ.prod ν) ν
theorem
MeasureTheory.Measure.set_prod_ae_eq
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{s s' : Set α}
{t t' : Set β}
(hs : s =ᵐ[μ] s')
(ht : t =ᵐ[ν] t')
:
theorem
MeasureTheory.Measure.measure_prod_compl_eq_zero
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{s : Set α}
{t : Set β}
(s_ae_univ : μ sᶜ = 0)
(t_ae_univ : ν tᶜ = 0)
:
theorem
MeasureTheory.NullMeasurableSet.prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{s : Set α}
{t : Set β}
(s_mble : MeasureTheory.NullMeasurableSet s μ)
(t_mble : MeasureTheory.NullMeasurableSet t ν)
:
MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν)
theorem
MeasureTheory.NullMeasurableSet.right_of_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{s : Set α}
{t : Set β}
(h : MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν))
(hs : μ s ≠ 0)
:
If s ×ˢ t is a null measurable set and μ s ≠ 0, then t is a null measurable set.
theorem
MeasureTheory.NullMeasurableSet.of_preimage_snd
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[NeZero μ]
{t : Set β}
(h : MeasureTheory.NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν))
:
If Prod.snd ⁻¹' t is a null measurable set and μ ≠ 0, then t is a null measurable set.
theorem
MeasureTheory.Measure.nullMeasurableSet_preimage_snd
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[NeZero μ]
{t : Set β}
:
MeasureTheory.NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet t ν
Prod.snd ⁻¹' t is null measurable w.r.t. μ.prod ν iff t is null measurable w.r.t. ν
provided that μ ≠ 0.
theorem
MeasureTheory.Measure.nullMeasurable_comp_snd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[NeZero μ]
{f : β → γ}
:
MeasureTheory.NullMeasurable (f ∘ Prod.snd) (μ.prod ν) ↔ MeasureTheory.NullMeasurable f ν
noncomputable def
MeasureTheory.Measure.FiniteSpanningSetsIn.prod
{α : Type u_1}
{β : Type u_2}
[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
- hμ.prod hν = { set := fun (n : ℕ) => hμ.set (Nat.unpair n).1 ×ˢ hν.set (Nat.unpair n).2, set_mem := ⋯, finite := ⋯, spanning := ⋯ }
Instances For
theorem
MeasureTheory.Measure.prod_sum_left
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ι : Type u_4}
(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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ι' : Type u_4}
[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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ι : Type u_4}
{ι' : Type u_5}
[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)
instance
MeasureTheory.Measure.prod.instSigmaFinite
{α : Type u_4}
{β : Type u_5}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
{x✝¹ : MeasurableSpace β}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SigmaFinite ν]
:
MeasureTheory.SigmaFinite (μ.prod ν)
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.prod.instSFinite
{α : Type u_4}
{β : Type u_5}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
{x✝¹ : MeasurableSpace β}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
:
MeasureTheory.SFinite (μ.prod ν)
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.instSigmaFiniteProdVolume
{α : Type u_4}
{β : Type u_5}
[MeasureTheory.MeasureSpace α]
[MeasureTheory.SigmaFinite MeasureTheory.volume]
[MeasureTheory.MeasureSpace β]
[MeasureTheory.SigmaFinite MeasureTheory.volume]
:
MeasureTheory.SigmaFinite MeasureTheory.volume
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.instSFiniteProdVolume
{α : Type u_4}
{β : Type u_5}
[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_2}
[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₁ : ∀ s ∈ C, ∀ t ∈ D, μν (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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
{ν : MeasureTheory.Measure β}
[MeasureTheory.SigmaFinite ν]
{μν : MeasureTheory.Measure (α × β)}
(h : ∀ (s : Set α) (t : Set β), MeasurableSet s → MeasurableSet 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_swap
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
:
MeasureTheory.Measure.map Prod.swap (μ.prod ν) = ν.prod μ
theorem
MeasureTheory.Measure.measurePreserving_swap
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
:
MeasureTheory.MeasurePreserving Prod.swap (μ.prod ν) (ν.prod μ)
theorem
MeasureTheory.Measure.prod_apply_symm
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
{s : Set (α × β)}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.ae_ae_comm
{α : Type u_1}
{β : Type u_2}
[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
theorem
MeasureTheory.NullMeasurableSet.left_of_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
{s : Set α}
{t : Set β}
(h : MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν))
(ht : ν t ≠ 0)
:
If s ×ˢ t is a null measurable set and ν t ≠ 0, then s is a null measurable set.
theorem
MeasureTheory.NullMeasurableSet.of_preimage_fst
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
[NeZero ν]
{s : Set α}
(h : MeasureTheory.NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν))
:
If Prod.fst ⁻¹' s is a null measurable set and ν ≠ 0, then s is a null measurable set.
theorem
MeasureTheory.Measure.nullMeasurableSet_preimage_fst
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
[NeZero ν]
{s : Set α}
:
MeasureTheory.NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet s μ
Prod.fst ⁻¹' s is null measurable w.r.t. μ.prod ν iff s is null measurable w.r.t. μ
provided that ν ≠ 0.
theorem
MeasureTheory.Measure.nullMeasurable_comp_fst
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
[NeZero ν]
{f : α → γ}
:
MeasureTheory.NullMeasurable (f ∘ Prod.fst) (μ.prod ν) ↔ MeasureTheory.NullMeasurable f μ
theorem
MeasureTheory.Measure.nullMeasurableSet_prod_of_ne_zero
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
{s : Set α}
{t : Set β}
(hs : μ s ≠ 0)
(ht : ν t ≠ 0)
:
MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet s μ ∧ MeasureTheory.NullMeasurableSet t ν
The product of two non-null sets is null measurable if and only if both of them are null measurable.
theorem
MeasureTheory.Measure.nullMeasurableSet_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
{s : Set α}
{t : Set β}
:
MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet s μ ∧ MeasureTheory.NullMeasurableSet t ν ∨ μ s = 0 ∨ ν t = 0
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_2}
{γ : Type u_3}
[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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
(s : Set α)
(t : Set β)
:
theorem
MeasureTheory.Measure.restrict_prod_eq_prod_univ
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
(s : Set α)
:
theorem
MeasureTheory.Measure.prod_dirac
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
(y : β)
:
μ.prod (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.map (fun (x : α) => (x, y)) μ
theorem
MeasureTheory.Measure.dirac_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
(x : α)
:
(MeasureTheory.Measure.dirac x).prod ν = MeasureTheory.Measure.map (Prod.mk x) ν
theorem
MeasureTheory.Measure.dirac_prod_dirac
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{x : α}
{y : β}
:
(MeasureTheory.Measure.dirac x).prod (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.dirac (x, y)
theorem
MeasureTheory.Measure.prod_add
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
(ν' : MeasureTheory.Measure β)
[MeasureTheory.SFinite ν']
:
theorem
MeasureTheory.Measure.add_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
(μ' : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ']
:
@[simp]
theorem
MeasureTheory.Measure.zero_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(ν : MeasureTheory.Measure β)
:
MeasureTheory.Measure.prod 0 ν = 0
@[simp]
theorem
MeasureTheory.Measure.prod_zero
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(μ : MeasureTheory.Measure α)
:
μ.prod 0 = 0
theorem
MeasureTheory.Measure.map_prod_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{δ : Type u_4}
[MeasurableSpace δ]
{f : α → β}
{g : γ → δ}
(μa : MeasureTheory.Measure α)
(μc : MeasureTheory.Measure γ)
[MeasureTheory.SFinite μa]
[MeasureTheory.SFinite μc]
(hf : Measurable f)
(hg : Measurable g)
:
(MeasureTheory.Measure.map f μa).prod (MeasureTheory.Measure.map g μc) = MeasureTheory.Measure.map (Prod.map f g) (μa.prod μc)
theorem
MeasureTheory.MeasurePreserving.skew_product
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{δ : Type u_4}
[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_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{δ : Type u_4}
[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_2}
{γ : Type u_3}
[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)) ν τ)
:
MeasureTheory.Measure.QuasiMeasurePreserving f (μ.prod ν) τ
theorem
MeasureTheory.QuasiMeasurePreserving.prod_of_left
{α : Type u_4}
{β : Type u_5}
{γ : Type u_6}
[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)) μ τ)
:
MeasureTheory.Measure.QuasiMeasurePreserving f (μ.prod ν) τ
theorem
AEMeasurable.prod_swap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[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_2}
{γ : Type u_3}
[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_2}
{γ : Type u_3}
[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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
(f : α × β → ENNReal)
:
theorem
MeasureTheory.lintegral_prod_of_measurable
{α : Type u_1}
{β : Type u_2}
[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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
(f : α × β → ENNReal)
(hf : AEMeasurable f (μ.prod ν))
:
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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
(f : α × β → ENNReal)
(hf : AEMeasurable f (μ.prod ν))
:
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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
(f : α × β → ENNReal)
(hf : Measurable f)
:
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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
⦃f : α → β → ENNReal⦄
(hf : AEMeasurable (Function.uncurry f) (μ.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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.SFinite μ]
⦃f : α → β → ENNReal⦄
(hf : AEMeasurable (Function.uncurry f) (μ.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_2}
[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_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
{f : α → ENNReal}
{g : β → ENNReal}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g ν)
:
Marginals of a measure defined on a product #
noncomputable def
MeasureTheory.Measure.fst
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(ρ : MeasureTheory.Measure (α × β))
:
Marginal measure on α obtained from a measure ρ on α × β, defined by ρ.map Prod.fst.
Equations
- ρ.fst = MeasureTheory.Measure.map Prod.fst ρ
Instances For
theorem
MeasureTheory.Measure.fst_apply
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
{s : Set α}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.fst_univ
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
:
ρ.fst Set.univ = ρ Set.univ
@[simp]
theorem
MeasureTheory.Measure.fst_zero
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
instance
MeasureTheory.Measure.instSFiniteFstOfProd
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
[MeasureTheory.SFinite ρ]
:
MeasureTheory.SFinite ρ.fst
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.fst.instIsFiniteMeasure
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
[MeasureTheory.IsFiniteMeasure ρ]
:
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.fst.instIsProbabilityMeasure
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
[MeasureTheory.IsProbabilityMeasure ρ]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
MeasureTheory.Measure.fst_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.IsProbabilityMeasure ν]
:
(μ.prod ν).fst = μ
theorem
MeasureTheory.Measure.fst_map_prod_mk₀
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[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_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{X : α → β}
{Y : α → γ}
{μ : MeasureTheory.Measure α}
(hY : Measurable Y)
:
(MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ).fst = MeasureTheory.Measure.map X μ
@[simp]
theorem
MeasureTheory.Measure.fst_add
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ ν : MeasureTheory.Measure (α × β)}
:
theorem
MeasureTheory.Measure.fst_sum
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ι : Type u_4}
(μ : ι → MeasureTheory.Measure (α × β))
:
(MeasureTheory.Measure.sum μ).fst = MeasureTheory.Measure.sum fun (n : ι) => (μ n).fst
theorem
MeasureTheory.Measure.fst_mono
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ μ : MeasureTheory.Measure (α × β)}
(h : ρ ≤ μ)
:
ρ.fst ≤ μ.fst
noncomputable def
MeasureTheory.Measure.snd
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(ρ : MeasureTheory.Measure (α × β))
:
Marginal measure on β obtained from a measure on ρ α × β, defined by ρ.map Prod.snd.
Equations
- ρ.snd = MeasureTheory.Measure.map Prod.snd ρ
Instances For
theorem
MeasureTheory.Measure.snd_apply
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
{s : Set β}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.snd_univ
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
:
ρ.snd Set.univ = ρ Set.univ
@[simp]
theorem
MeasureTheory.Measure.snd_zero
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
:
instance
MeasureTheory.Measure.instSFiniteSndOfProd
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
[MeasureTheory.SFinite ρ]
:
MeasureTheory.SFinite ρ.snd
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.snd.instIsFiniteMeasure
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
[MeasureTheory.IsFiniteMeasure ρ]
:
Equations
- ⋯ = ⋯
instance
MeasureTheory.Measure.snd.instIsProbabilityMeasure
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
[MeasureTheory.IsProbabilityMeasure ρ]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
MeasureTheory.Measure.snd_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SFinite ν]
[MeasureTheory.IsProbabilityMeasure μ]
:
(μ.prod ν).snd = ν
theorem
MeasureTheory.Measure.snd_map_prod_mk₀
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[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_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{X : α → β}
{Y : α → γ}
{μ : MeasureTheory.Measure α}
(hX : Measurable X)
:
(MeasureTheory.Measure.map (fun (a : α) => (X a, Y a)) μ).snd = MeasureTheory.Measure.map Y μ
@[simp]
theorem
MeasureTheory.Measure.snd_add
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ ν : MeasureTheory.Measure (α × β)}
:
theorem
MeasureTheory.Measure.snd_sum
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ι : Type u_4}
(μ : ι → MeasureTheory.Measure (α × β))
:
(MeasureTheory.Measure.sum μ).snd = MeasureTheory.Measure.sum fun (n : ι) => (μ n).snd
theorem
MeasureTheory.Measure.snd_mono
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ μ : MeasureTheory.Measure (α × β)}
(h : ρ ≤ μ)
:
ρ.snd ≤ μ.snd
@[simp]
theorem
MeasureTheory.Measure.fst_map_swap
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
:
(MeasureTheory.Measure.map Prod.swap ρ).fst = ρ.snd
@[simp]
theorem
MeasureTheory.Measure.snd_map_swap
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)}
:
(MeasureTheory.Measure.map Prod.swap ρ).snd = ρ.fst
theorem
MeasureTheory.measurePreserving_prodAssoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(μa : MeasureTheory.Measure α)
(μb : MeasureTheory.Measure β)
(μc : MeasureTheory.Measure γ)
[MeasureTheory.SFinite μb]
[MeasureTheory.SFinite μc]
:
MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.prodAssoc) ((μa.prod μb).prod μc) (μa.prod (μb.prod μc))
The measurable equiv induced by the equiv (α × β) × γ ≃ α × (β × γ) is measure preserving.
theorem
MeasureTheory.volume_preserving_prodAssoc
{α₁ : Type u_4}
{β₁ : Type u_5}
{γ₁ : Type u_6}
[MeasureTheory.MeasureSpace α₁]
[MeasureTheory.MeasureSpace β₁]
[MeasureTheory.MeasureSpace γ₁]
[MeasureTheory.SFinite MeasureTheory.volume]
[MeasureTheory.SFinite MeasureTheory.volume]
:
MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.prodAssoc) MeasureTheory.volume MeasureTheory.volume