MeasureTheory.lmarginal_erase
theorem MeasureTheory.lmarginal_erase :
∀ {δ : Type u_1} {π : δ → Type u_3} [inst : (x : δ) → MeasurableSpace (π x)]
{μ : (i : δ) → MeasureTheory.Measure (π i)} [inst_1 : ∀ (i : δ), MeasureTheory.SigmaFinite (μ i)]
[inst_2 : DecidableEq δ] {s : Finset δ} (f : ((i : δ) → π i) → ENNReal),
Measurable f →
∀ {i : δ},
i ∈ s →
∀ (x : (i : δ) → π i),
(∫⋯∫⁻_s, f ∂μ) x = ∫⁻ (xᵢ : π i), (∫⋯∫⁻_s.erase i, f ∂μ) (Function.update x i xᵢ) ∂μ i
The theorem `MeasureTheory.lmarginal_erase` states that, given a measure space setup where `δ` is a type, `π` is a function from `δ` to some other type, and each `π i` is a measurable space. We also have `μ`, a measure on each `π i`, and each measure `μ i` is sigma-finite. We also assume that we have the ability to decide equality on `δ`. We then consider a finite subset `s` of `δ` and a measurable function `f` mapping from `δ` to the extended non-negative real numbers (ENNReal). The theorem then states that for any `i` in `s` and any function `x` from `δ` to `π i`, the Lebesgue integral of `f` with respect to the measure `μ` over the set `s` evaluated at `x`, is equal to the Lebesgue integral over `π i` of the function obtained by updating `x` at `i` with `xᵢ`, and then taking the Lebesgue integral over the set `s` removed of `i`.
This theorem allows us to decompose a multiple integral into a sequence of single integrals, essentially it describes a method to "peel off" a single integral from a sequence of multiple iterated integrals.
More concisely: Given a measure space setup, a finite subset of the domain, and a measurable function, the Lebesgue integral of the function over the subset equals the sum of the integrals of the updated function over the subset's elements and over the subset without that element.
|
MeasureTheory.lmarginal_union
theorem MeasureTheory.lmarginal_union :
∀ {δ : Type u_1} {π : δ → Type u_3} [inst : (x : δ) → MeasurableSpace (π x)]
(μ : (i : δ) → MeasureTheory.Measure (π i)) [inst_1 : ∀ (i : δ), MeasureTheory.SigmaFinite (μ i)]
[inst_2 : DecidableEq δ] {s t : Finset δ} (f : ((i : δ) → π i) → ENNReal),
Measurable f → Disjoint s t → ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ
This theorem, `MeasureTheory.lmarginal_union`, states that for any type `δ`, function `π` from `δ` to another type, where each element of `δ` has an associated measurable space, a family `μ` of measures (each `μ i` is a measure on the measurable space `π i`), a function `f` from a `δ`-indexed product space to the Extended Nonnegative Real numbers (ENNReal), and disjoint finite subsets `s` and `t` of `δ`: If the function `f` is measurable and `s` and `t` are disjoint, then the integral over `s` union `t` of `f` with respect to `μ` is equal to the double integral over `s` and then `t` of `f` with respect to `μ`. This means that, under these conditions, the measure of `f` over the union of `s` and `t` can be computed by separately measuring over `s` and `t` and then combining these measurements.
More concisely: For measurable functions `f` and disjoint sets `s` and `t` in a product measurable space, the integral of `f` over `s` union `t` equals the sum of the integrals over `s` and `t`.
|
MeasureTheory.lmarginal_erase'
theorem MeasureTheory.lmarginal_erase' :
∀ {δ : Type u_1} {π : δ → Type u_3} [inst : (x : δ) → MeasurableSpace (π x)]
{μ : (i : δ) → MeasureTheory.Measure (π i)} [inst_1 : ∀ (i : δ), MeasureTheory.SigmaFinite (μ i)]
[inst_2 : DecidableEq δ] {s : Finset δ} (f : ((i : δ) → π i) → ENNReal),
Measurable f →
∀ {i : δ}, i ∈ s → ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s.erase i, fun x => ∫⁻ (xᵢ : π i), f (Function.update x i xᵢ) ∂μ i ∂μ
The theorem `MeasureTheory.lmarginal_erase'` in Measure Theory states that for any type `δ`, a function `π` from `δ` to some other type, a measurable space over `π x` for each `x` in `δ`, a measure `μ` over `π i` for each `i` in `δ`, a finite set `s` of elements of type `δ`, and a function `f` from a function over `δ` to extended nonnegative real numbers (or `ENNReal`), if `f` is measurable and `i` is an element of `s`, then the multiple integral over `s` of `f` with respect to the measure `μ` is equal to the multiple integral over the set `s` excluding `i`, of the function that at each point `x` integrates over `xᵢ` in `π i`, the function `f` applied to the update of `x` at `i` by `xᵢ`, with respect to `μ i` and `μ`. This theorem is a tool used for manipulating and simplifying the expressions involving multiple integrals in the context of measure theory.
More concisely: For any measurable function `f` from a measurable space `(δ, Σ)` to extended nonnegative real numbers, measure spaces `(π(x), Σ'x)_x` over `π(x)` for each `x` in `δ`, measures `μ_i` over `(π(i), Σ'i)` for each `i` in a finite set `s` in `δ`, and measurable function `π: δ → π(δ)`, the multiple integral of `f` over `s` equals the sum of the multiple integrals of `f(π(_) . update i with x)` over `s \ {i}` with respect to `μ_i` and `μ`.
|
MeasureTheory.lmarginal_congr
theorem MeasureTheory.lmarginal_congr :
∀ {δ : Type u_1} {π : δ → Type u_3} [inst : (x : δ) → MeasurableSpace (π x)]
(μ : (i : δ) → MeasureTheory.Measure (π i)) [inst_1 : DecidableEq δ] {s : Finset δ} {x y : (i : δ) → π i}
(f : ((i : δ) → π i) → ENNReal), (∀ i ∉ s, x i = y i) → (∫⋯∫⁻_s, f ∂μ) x = (∫⋯∫⁻_s, f ∂μ) y
This theorem, `MeasureTheory.lmarginal_congr`, states that the marginal distribution is independent of the variables in a set `s`. More specifically, for any type `δ`, any function `π` mapping elements of `δ` to a measurable space, a measure `μ` over the space defined by `π`, and any two functions `x` and `y` from `δ` to `π`, if for all `i` not in `s`, `x i` equals `y i`, then the integral over `s` of a function `f` with respect to `μ` evaluated at `x` is equal to the same integral evaluated at `y`. In other words, changing the variables outside of `s` does not affect the value of the integral of `f` over `s`.
More concisely: If two functions agree outside of a set `s` in their domains, then integrals of a function `f` with respect to a measure `μ` defined by a mapping `π` are equal over `s` for those functions.
|
MeasureTheory.lmarginal_insert'
theorem MeasureTheory.lmarginal_insert' :
∀ {δ : Type u_1} {π : δ → Type u_3} [inst : (x : δ) → MeasurableSpace (π x)]
{μ : (i : δ) → MeasureTheory.Measure (π i)} [inst_1 : ∀ (i : δ), MeasureTheory.SigmaFinite (μ i)]
[inst_2 : DecidableEq δ] {s : Finset δ} (f : ((i : δ) → π i) → ENNReal),
Measurable f →
∀ {i : δ}, i ∉ s → ∫⋯∫⁻_insert i s, f ∂μ = ∫⋯∫⁻_s, fun x => ∫⁻ (xᵢ : π i), f (Function.update x i xᵢ) ∂μ i ∂μ
The theorem `MeasureTheory.lmarginal_insert'` states that for a given type `δ`, a measurable space `π i` for each `δ`, a measure `μ i` for each `δ`, a decidable equality on `δ`, and a finset `s` of `δ`, if we have a measurable function `f` that maps from a function over `δ` to extended nonnegative real numbers (typically used in the context of measures), we can "peel off" or remove an integral from the end of a `lmarginal` integral. In other words, for any `i` not in the set `s`, the measure-theoretic integral over the finset obtained by inserting `i` into `s` of `f` with respect to the measure `μ` is equal to the integral over `s` of the function that for each `x` gives the integral over `π i` of `f` updated with `i` mapped to `x_i` with respect to the measure `μ i`, all with respect to the measure `μ`. This theorem is useful for breaking down complex integrals into simpler components.
More concisely: For any measurable spaces `π i`, measures `μ i`, a decidable equality on `δ`, a finset `s` of `δ`, and a measurable function `f` mapping from functions over `δ` to extended nonnegative real numbers, the measure-theoretic integral over `s` of the function `x ↦ ∫πi f(x̄) dμi(x̄)` is equal to the integral over `s⋃{i} δ` of `f` with respect to the measure `μ`.
|
MeasureTheory.lmarginal_insert
theorem MeasureTheory.lmarginal_insert :
∀ {δ : Type u_1} {π : δ → Type u_3} [inst : (x : δ) → MeasurableSpace (π x)]
{μ : (i : δ) → MeasureTheory.Measure (π i)} [inst_1 : ∀ (i : δ), MeasureTheory.SigmaFinite (μ i)]
[inst_2 : DecidableEq δ] {s : Finset δ} (f : ((i : δ) → π i) → ENNReal),
Measurable f →
∀ {i : δ},
i ∉ s →
∀ (x : (i : δ) → π i),
(∫⋯∫⁻_insert i s, f ∂μ) x = ∫⁻ (xᵢ : π i), (∫⋯∫⁻_s, f ∂μ) (Function.update x i xᵢ) ∂μ i
The theorem `MeasureTheory.lmarginal_insert` states that for a measurable function `f` from a family of measurable spaces `{π i : i ∈ δ}` to the extended nonnegative real numbers (`ENNReal`), under certain conditions, it's possible to "peel off" one integral from an iterated integral over a finite set `s` of indices. Specifically, if `i` is an index not in `s`, the integral of `f` with respect to a family of measures `{μ i : i ∈ δ}` over the set obtained by adding `i` to `s`, when evaluated at a given point `x`, is equal to the integral of a function that modifies `f` at `i` by replacing its value with a new variable, with respect to the measure `μ i`. This is done by applying the function `Function.update` to the function `f`, the index `i`, and the new variable, the integral is then performed over `s` and `i`. The conditions for this theorem to hold include that the measures are sigma-finite and the equality on the index set is decidable.
More concisely: Given a measurable function `f` from a finite index set `δ` to the extended nonnegative real numbers and a finite subset `s` of `δ`, if the measures `{μ i : i ∈ δ}` are sigma-finite and the equality on the index set is decidable, then for any index `i notin s` and point `x`, the integral of `f` with respect to `{μ i}` over the set `s ∪ {i}` equals the integral of `Function.update f i new_var` with respect to `{μ i}` over `s`.
|