Products of measures with densities

TheoremIterated integrals of a product of one-variable functions#✓fully proved

Let \(\mu_i\) be σ-finite measures on measurable spaces \(X_i\), indexed by a finite type \(\iota\), and let \(g_i : X_i \to [0, \infty]\) be measurable functions. For a finite set \(s \subseteq \iota\) and a point \(x \in \prod_i X_i\), integrating \(y \mapsto \prod_{i \in \iota} g_i(y_i)\) over the coordinates \(y_i\) with \(i \in s\), each against \(\mu_i\), while the other coordinates are fixed to those of \(x\), gives \(\left(\prod_{i \in s} \int g_i \, d\mu_i\right) \cdot \prod_{i \notin s} g_i(x_i)\).

theorem lmarginal_prod [DecidableEq ι] [Fintype ι] {g : ∀ i, X i → ℝ≥0∞}
    (hg : ∀ i, Measurable (g i)) (s : Finset ι) (x : ∀ i, X i) :
    (∫⋯∫⁻_s, (fun y ↦ ∏ i, g i (y i)) ∂μ) x =
      (∏ i ∈ s, ∫⁻ t, g i t ∂μ i) * ∏ i ∈ univ \ s, g i (x i)

Used by 1

Used byTonelli for products

TheoremTonelli for products#✓fully proved

Let \(\mu_i\) be σ-finite measures on measurable spaces \(X_i\), indexed by a finite type \(\iota\), and let \(g_i : X_i \to [0, \infty]\) be measurable functions. Then the integral of \(y \mapsto \prod_{i \in \iota} g_i(y_i)\) with respect to the product measure \(\prod_i \mu_i\) equals \(\prod_{i \in \iota} \int g_i \, d\mu_i\).

theorem lintegral_fintype_prod_eq_prod [Fintype ι] {g : ∀ i, X i → ℝ≥0∞}
    (hg : ∀ i, Measurable (g i)) :
    ∫⁻ y, ∏ i, g i (y i) ∂Measure.pi μ = ∏ i, ∫⁻ t, g i t ∂μ i

Uses 1 · Used by 1

Proof usesIterated integrals of a product of one-variable functions

Used byA product of measures with densities

TheoremA product of measures with densities#✓fully proved

Let \(\mu_i\) be σ-finite measures on measurable spaces \(X_i\), indexed by a finite type \(\iota\), and let \(f_i : X_i \to [0, \infty]\) be measurable functions such that, for each \(i\), the measure \(f_i \mu_i\) with density \(f_i\) with respect to \(\mu_i\) is σ-finite. Then the product measure \(\prod_i f_i \mu_i\) equals the measure with density \(y \mapsto \prod_{i \in \iota} f_i(y_i)\) with respect to the product measure \(\prod_i \mu_i\).

The σ-finiteness of the weighted measures guarantees that their product measure is characterized on boxes.

theorem Measure.pi_withDensity [Fintype ι] {f : ∀ i, X i → ℝ≥0∞} (hf : ∀ i, Measurable (f i))
    [∀ i, SigmaFinite ((μ i).withDensity (f i))] :
    Measure.pi (fun i ↦ (μ i).withDensity (f i)) =
      (Measure.pi μ).withDensity fun y ↦ ∏ i, f i (y i)

Uses 1 · Used by 1

Proof usesTonelli for products

Used byThe linear regression likelihood is a product of Gaussians

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.