ProdDecomp

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Two-factor variance decomposition

The "law of total variance" for a product of two probability measures, proved by direct Fubini computation for bounded observables (no condExp).

• Homogenization.variance_prod_eq: for a bounded measurable F : α × β → ℝ and probability measures P, Q, Var[F; P ⊗ Q] = ∫ b, Var[F(·,b); P] dQ + Var[b ↦ ∫ F(·,b) dP; Q].

theorem HCPolySupport.variance_prod_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (P : MeasureTheory.Measure α) (Q : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure P] [MeasureTheory.IsProbabilityMeasure Q] {F : α × β → ℝ} (hF : Measurable F) {M : ℝ} (hM : ∀ (p : α × β), |F p| ≤ M) : ProbabilityTheory.variance F (P.prod Q) = ∫ (b : β), ProbabilityTheory.variance (fun (a : α) => F (a, b)) P ∂Q + ProbabilityTheory.variance (fun (b : β) => ∫ (a : α), F (a, b) ∂P) Q

Two-factor variance decomposition (law of total variance for a product of two probability measures), bounded-observable form. Here the first coordinate is "integrated out": g b := ∫ a, F (a, b) ∂P is the conditional mean.