Documentation

Mathlib.MeasureTheory.Integral.Marginal

Marginals of multivariate functions #

In this file, we define a convenient way to compute integrals of multivariate functions, especially if you want to write expressions where you integrate only over some of the variables that the function depends on. This is common in induction arguments involving integrals of multivariate functions. This constructions allows working with iterated integrals and applying Tonelli's theorem and Fubini's theorem, without using measurable equivalences by changing the representation of your space (e.g. ((ι ⊕ ι') → ℝ) ≃ (ι → ℝ) × (ι' → ℝ)).

Main Definitions #

Main Results #

Implementation notes #

The function f can have an arbitrary product as its domain (even infinite products), but the set s of integration variables is a Finset. We are assuming that the function f is measurable for most of this file. Note that asking whether it is AEMeasurable is not even well-posed, since there is no well-behaved measure on the domain of f.

Todo #

def MeasureTheory.lmarginal {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] [DecidableEq δ] (μ : (i : δ) → MeasureTheory.Measure (π i)) (s : Finset δ) (f : ((i : δ) → π i)ENNReal) (x : (i : δ) → π i) :

Integrate f(x₁,…,xₙ) over all variables xᵢ where i ∈ s. Return a function in the remaining variables (it will be constant in the xᵢ for i ∈ s). This is the marginal distribution of all variables not in s when the considered measure is the product measure.

Equations
Instances For

    Integrate f(x₁,…,xₙ) over all variables xᵢ where i ∈ s. Return a function in the remaining variables (it will be constant in the xᵢ for i ∈ s). This is the marginal distribution of all variables not in s when the considered measure is the product measure.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Integrate f(x₁,…,xₙ) over all variables xᵢ where i ∈ s. Return a function in the remaining variables (it will be constant in the xᵢ for i ∈ s). This is the marginal distribution of all variables not in s when the considered measure is the product measure.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Measurable.lmarginal {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] (μ : (i : δ) → MeasureTheory.Measure (π i)) [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] {s : Finset δ} {f : ((i : δ) → π i)ENNReal} (hf : Measurable f) :
        @[simp]
        theorem MeasureTheory.lmarginal_empty {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] (μ : (i : δ) → MeasureTheory.Measure (π i)) [DecidableEq δ] (f : ((i : δ) → π i)ENNReal) :
        theorem MeasureTheory.lmarginal_congr {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] (μ : (i : δ) → MeasureTheory.Measure (π i)) [DecidableEq δ] {s : Finset δ} {x : (i : δ) → π i} {y : (i : δ) → π i} (f : ((i : δ) → π i)ENNReal) (h : is, x i = y i) :

        The marginal distribution is independent of the variables in s.

        theorem MeasureTheory.lmarginal_update_of_mem {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] (μ : (i : δ) → MeasureTheory.Measure (π i)) [DecidableEq δ] {s : Finset δ} {i : δ} (hi : i s) (f : ((i : δ) → π i)ENNReal) (x : (i : δ) → π i) (y : π i) :
        theorem MeasureTheory.lmarginal_union {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] (μ : (i : δ) → MeasureTheory.Measure (π i)) [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] {s : Finset δ} {t : Finset δ} (f : ((i : δ) → π i)ENNReal) (hf : Measurable f) (hst : Disjoint s t) :
        theorem MeasureTheory.lmarginal_union' {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] (μ : (i : δ) → MeasureTheory.Measure (π i)) [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] (f : ((i : δ) → π i)ENNReal) (hf : Measurable f) {s : Finset δ} {t : Finset δ} (hst : Disjoint s t) :
        theorem MeasureTheory.lmarginal_singleton {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [DecidableEq δ] (f : ((i : δ) → π i)ENNReal) (i : δ) :
        ∫⋯∫⁻_{i}, f μ = fun (x : (a : δ) → π a) => ∫⁻ (xᵢ : π i), f (Function.update x i xᵢ)μ i
        theorem MeasureTheory.lmarginal_insert {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] {s : Finset δ} (f : ((i : δ) → π i)ENNReal) (hf : Measurable f) {i : δ} (hi : is) (x : (i : δ) → π i) :
        (∫⋯∫⁻_insert i s, f μ) x = ∫⁻ (xᵢ : π i), (∫⋯∫⁻_s, f μ) (Function.update x i xᵢ)μ i

        Peel off a single integral from a lmarginal integral at the beginning (compare with lmarginal_insert', which peels off an integral at the end).

        theorem MeasureTheory.lmarginal_erase {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] {s : Finset δ} (f : ((i : δ) → π i)ENNReal) (hf : Measurable f) {i : δ} (hi : i s) (x : (i : δ) → π i) :
        (∫⋯∫⁻_s, f μ) x = ∫⁻ (xᵢ : π i), (∫⋯∫⁻_Finset.erase s i, f μ) (Function.update x i xᵢ)μ i

        Peel off a single integral from a lmarginal integral at the beginning (compare with lmarginal_erase', which peels off an integral at the end).

        theorem MeasureTheory.lmarginal_insert' {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] {s : Finset δ} (f : ((i : δ) → π i)ENNReal) (hf : Measurable f) {i : δ} (hi : is) :
        ∫⋯∫⁻_insert i s, f μ = ∫⋯∫⁻_s, fun (x : (i : δ) → π i) => ∫⁻ (xᵢ : π i), f (Function.update x i xᵢ)μ i μ

        Peel off a single integral from a lmarginal integral at the end (compare with lmarginal_insert, which peels off an integral at the beginning).

        theorem MeasureTheory.lmarginal_erase' {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] {s : Finset δ} (f : ((i : δ) → π i)ENNReal) (hf : Measurable f) {i : δ} (hi : i s) :
        ∫⋯∫⁻_s, f μ = ∫⋯∫⁻_Finset.erase s i, fun (x : (i : δ) → π i) => ∫⁻ (xᵢ : π i), f (Function.update x i xᵢ)μ i μ

        Peel off a single integral from a lmarginal integral at the end (compare with lmarginal_erase, which peels off an integral at the beginning).

        theorem MeasureTheory.lmarginal_mono {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [DecidableEq δ] {s : Finset δ} {f : ((i : δ) → π i)ENNReal} {g : ((i : δ) → π i)ENNReal} (hfg : f g) :
        @[simp]
        theorem MeasureTheory.lmarginal_univ {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] [Fintype δ] {f : ((i : δ) → π i)ENNReal} :
        ∫⋯∫⁻_Finset.univ, f μ = fun (x : (i : δ) → π i) => ∫⁻ (x : (i : δ) → π i), f xMeasureTheory.Measure.pi μ
        theorem MeasureTheory.lintegral_eq_lmarginal_univ {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] [Fintype δ] {f : ((i : δ) → π i)ENNReal} (x : (i : δ) → π i) :
        ∫⁻ (x : (i : δ) → π i), f xMeasureTheory.Measure.pi μ = (∫⋯∫⁻_Finset.univ, f μ) x
        theorem MeasureTheory.lmarginal_image {δ : Type u_1} {δ' : Type u_2} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] [DecidableEq δ'] {e : δ'δ} (he : Function.Injective e) (s : Finset δ') {f : ((i : δ') → π (e i))ENNReal} (hf : Measurable f) (x : (i : δ) → π i) :
        (∫⋯∫⁻_Finset.image e s, f fun (x : (i : δ) → π i) => (fun {x_1 : δ'} => x) ∘' e μ) x = (∫⋯∫⁻_s, f (fun {x : δ'} => μ) ∘' e) ((fun {x_1 : δ'} => x) ∘' e)
        theorem MeasureTheory.lmarginal_update_of_not_mem {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] {s : Finset δ} {i : δ} {f : ((i : δ) → π i)ENNReal} (hf : Measurable f) (hi : is) (x : (i : δ) → π i) (y : π i) :
        (∫⋯∫⁻_s, f μ) (Function.update x i y) = (∫⋯∫⁻_s, f fun (x : (i : δ) → π i) => Function.update x i y μ) x
        theorem MeasureTheory.lmarginal_eq_of_subset {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] {s : Finset δ} {t : Finset δ} {f : ((i : δ) → π i)ENNReal} {g : ((i : δ) → π i)ENNReal} (hst : s t) (hf : Measurable f) (hg : Measurable g) (hfg : ∫⋯∫⁻_s, f μ = ∫⋯∫⁻_s, g μ) :
        theorem MeasureTheory.lmarginal_le_of_subset {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] {s : Finset δ} {t : Finset δ} {f : ((i : δ) → π i)ENNReal} {g : ((i : δ) → π i)ENNReal} (hst : s t) (hf : Measurable f) (hg : Measurable g) (hfg : ∫⋯∫⁻_s, f μ ∫⋯∫⁻_s, g μ) :
        theorem MeasureTheory.lintegral_eq_of_lmarginal_eq {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] [Fintype δ] (s : Finset δ) {f : ((i : δ) → π i)ENNReal} {g : ((i : δ) → π i)ENNReal} (hf : Measurable f) (hg : Measurable g) (hfg : ∫⋯∫⁻_s, f μ = ∫⋯∫⁻_s, g μ) :
        ∫⁻ (x : (i : δ) → π i), f xMeasureTheory.Measure.pi μ = ∫⁻ (x : (i : δ) → π i), g xMeasureTheory.Measure.pi μ
        theorem MeasureTheory.lintegral_le_of_lmarginal_le {δ : Type u_1} {π : δType u_3} [(x : δ) → MeasurableSpace (π x)] {μ : (i : δ) → MeasureTheory.Measure (π i)} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [DecidableEq δ] [Fintype δ] (s : Finset δ) {f : ((i : δ) → π i)ENNReal} {g : ((i : δ) → π i)ENNReal} (hf : Measurable f) (hg : Measurable g) (hfg : ∫⋯∫⁻_s, f μ ∫⋯∫⁻_s, g μ) :
        ∫⁻ (x : (i : δ) → π i), f xMeasureTheory.Measure.pi μ ∫⁻ (x : (i : δ) → π i), g xMeasureTheory.Measure.pi μ