Resampling one coordinate of a product distribution

Holding one coordinate of an independent product fixed is overwriting it after sampling (pi_update_pure). Consequently an average over the product may first draw the whole tuple and then redraw one coordinate independently (sum_pi_mul_update). This is the step that fixes all coordinates but one in coordinate-wise averaging arguments.

Main results

• Cslib.Probability.PMF.pi_update_pure: fixing a coordinate is overwriting it.
• Cslib.Probability.PMF.sum_pi_mul_update: an average over a product equals the average with one coordinate redrawn independently.

theorem Cslib.Probability.PMF.pi_update_pure {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] (p : (i : ι) → PMF (α i)) (i : ι) (v : α i) : pi (Function.update p i (PMF.pure v)) = PMF.map (fun (y : (a : ι) → α a) => Function.update y i v) (pi p)

Fixing a coordinate of an independent product to v is the same as overwriting it with v after sampling.

theorem Cslib.Probability.PMF.sum_pi_mul_update {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u_2} [(i : ι) → Fintype (α i)] (p : (i : ι) → PMF (α i)) (i : ι) (F : ((j : ι) → α j) → ℝ) : ∑ y : (i : ι) → α i, ((pi p) y).toReal * F y = ∑ y : (i : ι) → α i, ((pi p) y).toReal * ∑ v : α i, ((p i) v).toReal * F (Function.update y i v)

Resampling a coordinate. Averaging F over an independent product is the same as drawing a tuple and then redrawing coordinate i independently from its own law.