theorem MeasureTheory.Measure.ae_eq_mul_lintegral_iff_ae_mul_comm {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f g : α → ENNReal} [SFinite μ] (hf : Measurable f) (hg : Measurable g) (hf1 : ∫⁻ (x : α), f x ∂μ = 1) : (g =ᵐ[μ] fun (x : α) => f x * ∫⁻ (y : α), g y ∂μ) ↔ ∀ᵐ (z : α × α) ∂μ.prod μ, g z.1 * f z.2 = g z.2 * f z.1

If ∫⁻ f ∂μ = 1, then g is a.e. equal to f times its integral iff g x * f y = g y * f x for μ.prod μ-a.e. (x, y).

theorem MeasureTheory.Measure.eq_prod_of_dirac_right (X : Type u_1) (Y : Type u_2) [MeasurableSpace X] [MeasurableSpace Y] (ν : Measure X) (y : Y) (μ : Measure (X × Y)) (marg_X : map Prod.fst μ = ν) (marg_Y : map Prod.snd μ = dirac y) : μ = ν.prod (dirac y)

theorem MeasureTheory.Measure.eq_prod_of_dirac_left (X : Type u_1) (Y : Type u_2) [MeasurableSpace X] [MeasurableSpace Y] (x : X) (ν : Measure Y) (μ : Measure (X × Y)) (marg_X : map Prod.fst μ = dirac x) (marg_Y : map Prod.snd μ = ν) : μ = (dirac x).prod ν