Documentation

PFR.Mathlib.MeasureTheory.Measure.Prod

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✝¹ : MeasurableSpace β} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β) [MeasureTheory.SigmaFinite ν] (x : α × β) :
(μ.prod ν) {x} = μ {x.1} * ν {x.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) :
(μ.prod ν) (↑(A ×ˢ B)) = 0

To put next to quasiMeasurePreserving_fst

To put next to quasiMeasurePreserving_fst