theorem
MeasureTheory.Measure.map_prod_comap_swap
{Ω : Type u_1}
{α : Type u_2}
{γ : Type u_4}
[MeasurableSpace Ω]
[MeasurableSpace α]
[MeasurableSpace γ]
{X : Ω → α}
{Z : Ω → γ}
(hX : Measurable X)
(hZ : Measurable Z)
(μ : MeasureTheory.Measure Ω)
:
MeasureTheory.Measure.comap Prod.swap (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Z ω)) μ) = MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, X ω)) μ
The law of $(X, Z)$ is the image of the law of $(Z,X)$.
theorem
MeasureTheory.Measure.prod_apply_singleton
{α : Type u_5}
{β : Type u_6}
:
∀ {x : MeasurableSpace α} {x_1 : MeasurableSpace β} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β)
[inst : MeasureTheory.SigmaFinite ν] (x_2 : α × β), (μ.prod ν) {x_2} = μ {x_2.1} * ν {x_2.2}
theorem
MeasureTheory.Measure.prod_of_full_measure_finset
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
[MeasureTheory.SigmaFinite ν]
{A : Finset α}
{B : Finset β}
(hA : μ (↑A)ᶜ = 0)
(hB : ν (↑B)ᶜ = 0)
: