Measures on a product at atoms

The product measure at a pair on reals, the atoms of a product with a point mass, and the product measure at a set given by its fibers over a finite second coordinate; the marginals Measure.fst and Measure.snd at a singleton, as sums over the other coordinate when it ranges over a finite type, in ℝ≥0∞ and on reals; and absolute continuity of a joint with respect to the product of its marginals. [UPSTREAM] candidate for Mathlib/MeasureTheory/Measure/Prod.lean.

theorem MeasureTheory.Measure.prod_real_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure α) (ν : Measure β) [SFinite ν] (a : α) (b : β) : (μ.prod ν).real {(a, b)} = μ.real {a} * ν.real {b}

theorem MeasureTheory.Measure.prod_dirac_apply_singleton_ne_zero_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : Measure α) (b : β) (p : α × β) : (μ.prod (dirac b)) {p} ≠ 0 ↔ μ {p.1} ≠ 0 ∧ p.2 = b

The atoms of μ.prod (dirac b) are the atoms of μ paired with b.

Sets given by their fibers over a finite coordinate

theorem MeasureTheory.Measure.prod_apply_fibers {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype β] (μ : Measure α) (ν : Measure β) {f : β → Set α} [SFinite ν] (hf : ∀ (b : β), MeasurableSet (f b)) : (μ.prod ν) {p : α × β | p.1 ∈ f p.2} = ∑ b : β, μ (f b) * ν {b}

theorem MeasureTheory.Measure.prod_real_fibers {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype β] (μ : Measure α) (ν : Measure β) {f : β → Set α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hf : ∀ (b : β), MeasurableSet (f b)) : (μ.prod ν).real {p : α × β | p.1 ∈ f p.2} = ∑ b : β, μ.real (f b) * ν.real {b}

Marginals at a singleton

theorem MeasureTheory.Measure.fst_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Fintype β] (ρ : Measure (α × β)) (a : α) : ρ.fst {a} = ∑ b : β, ρ {(a, b)}

theorem MeasureTheory.Measure.snd_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Fintype α] (ρ : Measure (α × β)) (b : β) : ρ.snd {b} = ∑ a : α, ρ {(a, b)}

theorem MeasureTheory.Measure.fst_real_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Fintype β] (ρ : Measure (α × β)) (a : α) : ρ.fst.real {a} = ρ.real ↑({a} ×ˢ Finset.univ)

theorem MeasureTheory.Measure.snd_real_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Fintype α] (ρ : Measure (α × β)) (b : β) : ρ.snd.real {b} = ρ.real ↑(Finset.univ ×ˢ {b})

theorem MeasureTheory.Measure.fst_real_singleton_eq_sum {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Fintype β] (ρ : Measure (α × β)) [IsFiniteMeasure ρ] (a : α) : ρ.fst.real {a} = ∑ b : β, ρ.real {(a, b)}

theorem MeasureTheory.Measure.snd_real_singleton_eq_sum {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Fintype α] (ρ : Measure (α × β)) [IsFiniteMeasure ρ] (b : β) : ρ.snd.real {b} = ∑ a : α, ρ.real {(a, b)}

theorem MeasureTheory.Measure.absolutelyContinuous_fst_prod_snd {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Countable α] [Countable β] (ρ : Measure (α × β)) [SFinite ρ] : ρ.AbsolutelyContinuous (ρ.fst.prod ρ.snd)