LeanPool.RlTheoryInLean.MeasureTheory.Measure.Prod

theorem MeasureTheory.Measure.prod_preimage_snd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure α) (ν : Measure β) (hν : SFinite ν) (A : Set β) : (μ.prod ν) (Prod.snd ⁻¹' A) = μ Set.univ * ν A

theorem MeasureTheory.Measure.prod_preimage_fst {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure α) (ν : Measure β) (hν : SFinite ν) (A : Set α) : (μ.prod ν) (Prod.fst ⁻¹' A) = μ A * ν Set.univ

theorem MeasureTheory.Measure.map_prodMk_dirac {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {X : α → β} {Y : α → γ} {μ : Measure α} {C : β} (hC : ∀ᵐ (a : α) ∂μ, X a = C) (hY : Measurable Y) [SFinite (map Y μ)] : map (fun (a : α) => (X a, Y a)) μ = (dirac C).prod (map Y μ)