Measures on a product at atoms

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; the product measure at a rectangle on reals; absolute continuity of a joint with respect to the product of its marginals; and a product measure, conditioned on an event of the first coordinate, at a set given by its fibers over a finite second coordinate. [UPSTREAM] candidate for Mathlib/MeasureTheory/Measure/Prod.lean.

theorem MeasureTheory.Measure.measureReal_prod_prod {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure α) (ν : Measure β) [SFinite ν] (s : Set α) (t : Set β) : (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t

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.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)

The first marginal at a singleton is the mass of the corresponding product event.

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})

The second marginal at a singleton is the mass of the corresponding product event.

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)

A joint on a countable product is absolutely continuous with respect to the product of its marginals.

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 α) [SFinite μ] (ν : Measure β) [SFinite ν] {f : β → Set α} (hf : ∀ (b : β), MeasurableSet (f b)) : (μ.prod ν) {p : α × β | p.1 ∈ f p.2} = ∑ b : β, μ (f b) * ν {b}

The product measure at a set given by its fibers over a finite second coordinate.

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

Conditioning a product on an event of the first coordinate, at a set given by its fibers over a finite second coordinate: the fibers' conditional masses, mixed by the second factor.

theorem MeasureTheory.Measure.cond_prod_fst_real_fibers {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype β] (μ : Measure α) [SFinite μ] (ν : Measure β) [SFinite ν] {f : β → Set α} [IsProbabilityMeasure ν] {s : Set α} (hs : MeasurableSet s) (hf : ∀ (b : β), MeasurableSet (f b)) : (μ.prod ν)[|Prod.fst ⁻¹' s].real {p : α × β | p.1 ∈ f p.2} = ∑ b : β, μ[|s].real (f b) * ν.real {b}

cond_prod_fst_apply_fibers on reals.