MeasureTheory.integral_fn_integral_add
theorem MeasureTheory.integral_fn_integral_add :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
{E' : Type u_7} [inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ℝ E'] ⦃f g : α × β → E⦄ (F : E → E'),
MeasureTheory.Integrable f (μ.prod ν) →
MeasureTheory.Integrable g (μ.prod ν) →
∫ (x : α), F (∫ (y : β), f (x, y) + g (x, y) ∂ν) ∂μ =
∫ (x : α), F (∫ (y : β), f (x, y) ∂ν + ∫ (y : β), g (x, y) ∂ν) ∂μ
This theorem, `MeasureTheory.integral_fn_integral_add`, states that for any given function `F`, and any given functions `f` and `g` that are integrable with respect to the product measure of `μ` and `ν`, the integral over `α` of the function `F` applied to the integral over `β` of the sum of `f` and `g` is equal to the integral over `α` of `F` applied to the sum of the integral over `β` of `f` and the integral over `β` of `g`. In other words, the order of performing the integration and the addition does not matter: you can first add and then integrate, or first integrate and then add, and the result will be the same.
In mathematical notation, this translates to:
∫F(∫(f(x,y) + g(x,y))dν) dμ = ∫F((∫f(x,y)dν) + (∫g(x,y)dν))dμ
The assumptions are that `f` and `g` are integrable and `F` can be any function. The spaces `α`, `β`, `E` and `E'` are measurable with `α` and `β` endowed with measures `μ` and `ν` respectively, and `E` and `E'` are normed additive commutative groups with a real normed vector space structure. The measures `μ` and `ν` are assumed to be sigma-finite.
More concisely: For integrable functions `f` and `g` and any function `F`, the integral of `F` over the product measure of the sum of the integrals of `f` and `g` is equal to the integral of `F` over the sum of the integrals of `f` and `g`.
|
MeasureTheory.integral_integral_sub
theorem MeasureTheory.integral_integral_sub :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
⦃f g : α × β → E⦄,
MeasureTheory.Integrable f (μ.prod ν) →
MeasureTheory.Integrable g (μ.prod ν) →
∫ (x : α), ∫ (y : β), f (x, y) - g (x, y) ∂ν ∂μ =
∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ - ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
The theorem `MeasureTheory.integral_integral_sub` asserts that for double integrals, subtraction is commutative. More specifically, this theorem states that for any two integrable functions `f` and `g` over a product measure space `(μ.prod ν)`, the double integral of the difference of `f` and `g` is equal to the difference of the double integrals of `f` and `g`. This is mathematically expressed as ∫∫ (f(x, y) - g(x, y)) dν dμ = ∫∫ f(x, y) dν dμ - ∫∫ g(x, y) dν dμ for all `x` in `α` and `y` in `β`. The integrability of `f` and `g` ensures that all these integrals are well-defined.
More concisely: The theorem asserts that for integrable functions $f$ and $g$ over a product measure space, $\int\int(f(x,y)-g(x,y))d\mu d\nu = \int\int f(x,y)d\mu d\nu - \int\int g(x,y)d\mu d\nu$.
|
MeasureTheory.integral_integral
theorem MeasureTheory.integral_integral :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
{f : α → β → E},
MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν) →
∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (z : α × β), f z.1 z.2 ∂μ.prod ν
This is a reversed version of Fubini's Theorem. The theorem states that, for all types `α`, `β`, and `E`, along with `α` and `β` being measurable spaces and `μ` and `ν` being measures on `α` and `β` respectively, and `E` being a normed addition commutative group, if a function `f : α → β → E` is integrable with respect to the product measure of `μ` and `ν`, then the double integral of `f` with respect to `ν` and `μ` is equal to the integral over the function `f` with respect to the product measure of `μ` and `ν`. This theorem essentially allows us to interchange the order of integration in a double integral under certain conditions.
More concisely: If `α`, `β` are measurable spaces, `E` a normed addition commutative group, `μ` and `ν` measures on `α` and `β` respectively, and `f : α → β → E` integrable with respect to the product measure of `μ` and `ν`, then ∫∫(`f`(x, y) d(`μ`(x) d(`ν`(y))) = ∫(`f`(x, y) d(`ν`(y)) d(`μ`(x)).
|
MeasureTheory.integral_integral_swap
theorem MeasureTheory.integral_integral_swap :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
⦃f : α → β → E⦄,
MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν) →
∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (y : β), ∫ (x : α), f x y ∂μ ∂ν
The theorem `MeasureTheory.integral_integral_swap` states that for any two types `α` and `β`, and a normed additive commutative group `E`, given measurable spaces on `α` and `β`, measures `μ` and `ν` on `α` and `β` respectively, and a condition where `ν` and `μ` are sigma finite. If we have a function `f` from `α` to `β` to `E` that is integrable when uncurried over the product of the measures `μ` and `ν`, then the double integral of `f` with respect to `ν` and then `μ` is equal to the double integral of `f` with respect to `μ` and then `ν`. In other words, it allows us to switch the order of integration.
More concisely: For measurable spaces `(α, Σα, μ)` and `(β, Σβ, ν)`, if `f: α → β → E` is integrable with respect to the product measure `μ ⨯ ν` on `α × β`, then `∫(∫f(x, y) d(μ ⨯ ν)(x, y)) dy dμ = ∫(∫f(x, y) dμ(x) dy) dν`.
|
MeasureTheory.StronglyMeasurable.integral_prod_left
theorem MeasureTheory.StronglyMeasurable.integral_prod_left :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E]
[inst_4 : MeasureTheory.SigmaFinite μ] ⦃f : α → β → E⦄,
MeasureTheory.StronglyMeasurable (Function.uncurry f) →
MeasureTheory.StronglyMeasurable fun y => ∫ (x : α), f x y ∂μ
The theorem `MeasureTheory.StronglyMeasurable.integral_prod_left` states that for any measure space `α` with a `σ`-finite measure `μ`, and any types `β` and `E` (where `E` is a normed addition commutative group and a normed space over the real numbers), if we consider a function `f` from `α × β` to `E` that is strongly measurable (i.e., it is the limit of simple functions), then the function that maps each member of `β` to the Bochner integral over `α` of `f` with respect to `μ` is also strongly measurable. In other words, the Bochner integral is measurable. This result is used to show that the integrand of the right-hand side of the symmetric version of Fubini's theorem is measurable.
More concisely: Given a measure space `(α, Σ, μ)` with `σ-finite` measure `μ`, a normed addition commutative group and normed space `(E, ||.||)` over the real numbers, and a strongly measurable function `f : α × β → E`, the function that maps each `β` element to the Bochner integral of `f` over `α` is also strongly measurable.
|
MeasureTheory.continuous_integral_integral
theorem MeasureTheory.continuous_integral_integral :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ],
Continuous fun f => ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ
This theorem states that for any types `α`, `β`, and `E`, given measurable spaces over `α` and `β` and measures `μ` and `ν` over these spaces, and assuming `E` forms a normed additive commutative group and a normed space over the real numbers, and both measures `μ` and `ν` are sigma-finite, then the map which takes a L¹-function `f` from `α × β` to `E` and sends it to the double integral of `f` is a continuous function. In mathematical notation, this can be written as the continuity of the mapping `f ⟼ ∫∫f dν dμ`.
More concisely: Given measurable spaces `α`, `β`, types `E` (a normed additive commutative group and normed space over the real numbers), and sigma-finite measures `μ` and `ν` on `α × β` and `E`, respectively, the map `f ⟼ ∫∫f dν dμ` is a continuous function from the space of L¹-functions from `α × β` to `E`.
|
MeasureTheory.integrable_prod_iff'
theorem MeasureTheory.integrable_prod_iff' :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ] ⦃f : α × β → E⦄,
MeasureTheory.AEStronglyMeasurable f (μ.prod ν) →
(MeasureTheory.Integrable f (μ.prod ν) ↔
(∀ᵐ (y : β) ∂ν, MeasureTheory.Integrable (fun x => f (x, y)) μ) ∧
MeasureTheory.Integrable (fun y => ∫ (x : α), ‖f (x, y)‖ ∂μ) ν)
The theorem `MeasureTheory.integrable_prod_iff'` states that for a binary function `f`, the function is integrable with respect to the product measure of `μ` and `ν` if and only if two conditions are met. First, the function `x ↦ f (x, y)` must be integrable for almost every `y` with respect to the measure `μ`. Second, the function `y ↦ ∫ ‖f (x, y)‖ dx` must be integrable with respect to the measure `ν`. Here, `f` is assumed to be almost everywhere strongly measurable with respect to the product measure of `μ` and `ν`. The function `f` takes a pair of inputs, one from the set `α` and one from the set `β`, and produces a value in the normed additively commutative group `E`. The measure spaces of `α` and `β` are both assumed to be sigma-finite.
More concisely: A function `f : α × β → E` is integrable with respect to the product measure of `μ` and `ν` if and only if for almost every `y` in `β`, `x ↦ f (x, y)` is integrable with respect to `μ` and `y ↦ ∫‖f(x,y)‖ dx` is integrable with respect to `ν`.
|
MeasureTheory.StronglyMeasurable.integral_prod_right
theorem MeasureTheory.StronglyMeasurable.integral_prod_right :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E]
[inst_4 : MeasureTheory.SigmaFinite ν] ⦃f : α → β → E⦄,
MeasureTheory.StronglyMeasurable (Function.uncurry f) →
MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν
This theorem, named `MeasureTheory.StronglyMeasurable.integral_prod_right`, states that the Bochner integral is measurable. More specifically, given a function `f` from `α` to `β` to `E`, where `α`, `β`, and `E` are types, `α` and `β` have associated measurable spaces, `E` is a normed add commutative group and a normed space over the real numbers, and `ν` is a sigma-finite measure on `β`, if the function `f` in uncurried form is strongly measurable (i.e., it is the limit point of simple functions), then the function which takes `x` in `α` to the Bochner integral of `f x` with respect to `ν` is also strongly measurable. This theorem provides an important result used in the proof of Fubini's theorem, specifically for the measurability of the integrand on the right-hand-side of the theorem.
More concisely: If a strongly measurable function from a measurable space to another measurable space, whose values are integrable with respect to a sigma-finite measure, then the function defined as the Bochner integral of the function with respect to the measure is also strongly measurable.
|
MeasureTheory.StronglyMeasurable.integral_prod_right'
theorem MeasureTheory.StronglyMeasurable.integral_prod_right' :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E]
[inst_4 : MeasureTheory.SigmaFinite ν] ⦃f : α × β → E⦄,
MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν
This theorem states that the Bochner integral is measurable. Specifically, for any strongly measurable function `f` from a product of two types `α` and `β` into a normed add commutative group `E`, the function that maps each `x` to the Bochner integral of `f` over `β` with respect to `y`, holding `x` constant, is also strongly measurable. This is a key property used in proving Fubini's theorem, as it guarantees that the integrand of the right-hand-side of Fubini's theorem is measurable. In terms of LaTeX mathematics, this theorem can be written as: If `f : α × β → E` is strongly measurable, then the function `x ↦ ∫ f(x, y) dy` is also strongly measurable.
More concisely: If `f : α × β → E` is strongly measurable, then the function `x ↦ ∫ₔ f(x, y) dy` is also strongly measurable, where the integration is taken over `β` with respect to some suitable measure.
|
MeasureTheory.integral_integral_swap_of_hasCompactSupport
theorem MeasureTheory.integral_integral_swap_of_hasCompactSupport :
∀ {E : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {X : Type u_8} {Y : Type u_9}
[inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [inst_4 : MeasurableSpace X]
[inst_5 : MeasurableSpace Y] [inst_6 : OpensMeasurableSpace X] [inst_7 : OpensMeasurableSpace Y] {f : X → Y → E},
Continuous (Function.uncurry f) →
HasCompactSupport (Function.uncurry f) →
∀ {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y}
[inst_8 : MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_9 : MeasureTheory.IsFiniteMeasureOnCompacts ν],
∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
This theorem is a version of the Fubini theorem for continuous functions with compact support. It states that the order of integration with respect to locally finite measures can be swapped. Notably, this theorem does not assume that the measures are σ-finite, which is typically a requirement in the usual statement of the Fubini theorem. Here, the theorem is applied to a function `f` from types `X` and `Y` to `E` that is continuous when interpreted as a function on `X × Y` and has compact support. Given locally finite measures `μ` on `X` and `ν` on `Y`, the theorem asserts that the double integral of `f` with respect to `μ` and `ν` is the same regardless of the order of integration.
More concisely: Given a continuous function `f` from types `X` and `Y` to `E` with compact support and locally finite measures `μ` on `X` and `ν` on `Y`, the double integral of `f` with respect to `μ` and then `ν` is equal to the double integral with respect to `ν` and then `μ`.
|
MeasureTheory.integral_integral_symm
theorem MeasureTheory.integral_integral_symm :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
{f : α → β → E},
MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν) →
∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (z : β × α), f z.2 z.1 ∂ν.prod μ
This is a reversed version of Fubini's Theorem. The theorem states that for any two measure spaces, `α` and `β`, with measures `μ` and `ν` respectively, and a function `f` that maps from `α` to `β` resulting in a normed addition commutative group `E`, if the uncurry version of `f` is integrable with respect to the product measure `μ.prod ν`, then the double integral of `f` with respect to measures `ν` and `μ` (in that order) is equal to the integral of `f` applied in reverse order of arguments with respect to the product measure `ν.prod μ`. In simpler terms, it allows swapping the order of integration in a double integral under certain conditions.
More concisely: If `f: α × β → E` is a measurable function between two measure spaces `α` and `β` with measures `μ` and `ν`, and the uncurried function `(x, y) ↦ f x y` is integrable with respect to the product measure `μ.prod ν`, then the double integral of `f` with respect to `ν` and `μ` equals the double integral of the function `g(x, y) := f(y, x)` with respect to `μ.prod ν`.
|
MeasureTheory.AEStronglyMeasurable.integral_prod_right'
theorem MeasureTheory.AEStronglyMeasurable.integral_prod_right' :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] ⦃f : α × β → E⦄,
MeasureTheory.AEStronglyMeasurable f (μ.prod ν) →
MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : β), f (x, y) ∂ν) μ
This theorem states that the Bochner integral is almost everywhere measurable. More concretely, given a function `f` defined on the product space of two sets `α` and `β`, if `f` is almost everywhere strongly measurable with respect to the product measure of `μ` and `ν`, then the function obtained by integrating `f` over `β` for each fixed value in `α` is also almost everywhere strongly measurable with respect to the measure `μ`. This result is crucial in proving the right-hand side of Fubini's theorem, which involves the integrability of such functions.
More concisely: If a function `f` on the product space of `α × β` is almost everywhere strongly measurable with respect to the product measure of `μ` and `ν`, then the function obtained by integrating `f` over `β` for each fixed value in `α` is almost everywhere strongly measurable with respect to `μ`.
|
MeasureTheory.StronglyMeasurable.integral_prod_left'
theorem MeasureTheory.StronglyMeasurable.integral_prod_left' :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E]
[inst_4 : MeasureTheory.SigmaFinite μ] ⦃f : α × β → E⦄,
MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun y => ∫ (x : α), f (x, y) ∂μ
The theorem `MeasureTheory.StronglyMeasurable.integral_prod_left'` asserts that the Bochner integral is measurable. This is crucial in demonstrating that the integrand of the symmetric version of Fubini's theorem is measurable. In more detail, given a measurable space `α`, another measurable space `β`, and a type `E` that forms a normed additive commutative group and a normed space over the real numbers, along with a sigma-finite measure `μ` on `α`, if a function `f` from the product of `α` and `β` to `E` is strongly measurable (i.e., it is the limit of simple functions), then the function that maps each element `y` of `β` to the Bochner integral of `f` over `α` with respect to `μ`, is also strongly measurable.
More concisely: If `f` is a strongly measurable function from the product of two measurable spaces to a normed additive commutative group with respect to a sigma-finite measure, then the function that maps each element to the Bochner integral of `f` over one of the spaces is also strongly measurable.
|
MeasureTheory.integral_integral_add'
theorem MeasureTheory.integral_integral_add' :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
⦃f g : α × β → E⦄,
MeasureTheory.Integrable f (μ.prod ν) →
MeasureTheory.Integrable g (μ.prod ν) →
∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ =
∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ + ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
The theorem states that the double integral of the sum of two functions is equal to the sum of the double integrals of the functions. More precisely, for any two functions `f` and `g` that map from a product of types `α` and `β` into a normed additive commutative group `E`, and are integrable with respect to the product measure of measures `μ` and `ν`, the double integral of `(f + g) (x, y)` with respect to `ν` and `μ` is equal to the sum of the double integral of `f (x, y)` and the double integral of `g (x, y)`, both also with respect to `ν` and `μ`. This is a version where the sum of the functions is taken pointwise before integration, i.e., `(f + g) (x, y)` instead of `f (x, y) + g (x, y)`.
More concisely: For integrable functions `f` and `g` from the product of types `α` and `β` into a normed additive commutative group `E`, their pointwise sum is integrable, and their double integrals with respect to measures `μ` and `ν` are equal to the sum of their individual double integrals.
|
MeasureTheory.integral_integral_sub'
theorem MeasureTheory.integral_integral_sub' :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
⦃f g : α × β → E⦄,
MeasureTheory.Integrable f (μ.prod ν) →
MeasureTheory.Integrable g (μ.prod ν) →
∫ (x : α), ∫ (y : β), (f - g) (x, y) ∂ν ∂μ =
∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ - ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
The theorem `MeasureTheory.integral_integral_sub'` states that the double integral of the difference of two functions is equal to the difference of the double integrals of the two functions individually. More specifically, for any two integrable functions `f` and `g` on a product space of `α` and `β` with measures `μ` and `ν` respectively, the double integral of `(f - g) (x, y)` with respect to `ν` and `μ` is equal to the difference of the double integral of `f (x, y)` and the double integral of `g (x, y)`, both also taken with respect to `ν` and `μ`. This is a property of double integrals reflecting the commutativity with subtraction operation.
More concisely: The theorem asserts that for integrable functions $f$ and $g$ on the product space $\alpha \times \beta$ with measures $\mu$ and $\nu$, respectively, their double integrals with respect to $\nu$ and $\mu$ satisfy $\int\int(f(x, y) - g(x, y))\ d\mu\ d\nu = \int\int f(x, y)\ d\mu\ d\nu - \int\int g(x, y)\ d\mu\ d\nu$.
|
MeasureTheory.set_integral_prod
theorem MeasureTheory.set_integral_prod :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
(f : α × β → E) {s : Set α} {t : Set β},
MeasureTheory.IntegrableOn f (s ×ˢ t) (μ.prod ν) →
∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
This theorem is an alias of `MeasureTheory.setIntegral_prod` and it is a statement of Fubini's Theorem for set integrals in Measure Theory. According to the theorem, for a measurable space of types `α` and `β`, measures `μ` and `ν`, a normed additive commutative group `E`, and sets `s` of `α` and `t` of `β`, if a function `f` from the Cartesian product of `α` and `β` to `E` is integrable over the Cartesian product of sets `s` and `t`, then the double integral of `f` over the product of sets `s` and `t` with respect to the product of measures `μ` and `ν` is equal to the iterated integral of `f` over `s` and `t` with respect to `ν` and `μ` respectively.
More concisely: For measurable sets S in α and T in β, measures μ and ν, and integrable function f from S×T to a normed additive commutative group E, the double integral of f over S×T with respect to μ⊗ν equals the iterated integral of f first with respect to ν over T and then with respect to μ over S.
|
MeasureTheory.Integrable.swap
theorem MeasureTheory.Integrable.swap :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : MeasureTheory.SigmaFinite μ] ⦃f : α × β → E⦄,
MeasureTheory.Integrable f (μ.prod ν) → MeasureTheory.Integrable (f ∘ Prod.swap) (ν.prod μ)
The theorem `MeasureTheory.Integrable.swap` states that for any two types `α` and `β` representing the spaces of integration, and a type `E` representing a normed, additive commutative group, given a measure `μ` on `α`, a measure `ν` on `β`, and a function `f` from the product of `α` and `β` to `E`, if `f` is integrable with respect to the product measure of `μ` and `ν`, then the composition of `f` with the swap function (which switches the order of the pair `(α, β)` to `(β, α)`) is also integrable with respect to the product measure of `ν` and `μ`. This theorem assumes that both `μ` and `ν` are sigma-finite measures, meaning they can be decomposed into a countable union of sets with finite measure.
More concisely: If `μ` is a sigma-finite measure on `α`, `ν` is a sigma-finite measure on `β`, and `f : α × β → E` is integrable with respect to the product measure of `μ` and `ν`, then `f` composed with the swap function is integrable with respect to the product measure of `ν` and `μ`.
|
MeasureTheory.integral_prod_symm
theorem MeasureTheory.integral_prod_symm :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
(f : α × β → E),
MeasureTheory.Integrable f (μ.prod ν) → ∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
This is a symmetric version of Fubini's Theorem for integrable functions on a product space `α × β`. The theorem states that, for any function `f` from `α × β` to `E` which is integrable with respect to the product measure `μ.prod ν`, the Bochner integral of `f` with respect to `μ.prod ν` is equal to the iterated Bochner integral of `f` with respect to `μ` and `ν`, in the opposite order. That is, the integral of `f` over `α × β` is equal to the integral over `β` of the integrals over `α`.
More concisely: For integrable functions `f` on the product space `α × β` with respect to the product measure `μ.prod ν`, the Bochner integral of `f` equals the iterated integral of `f(x, y)` with respect to `μ` and then `ν`, or the integral over `β` of the integrals over `α` of `f`.
|
MeasureTheory.integral_prod
theorem MeasureTheory.integral_prod :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
(f : α × β → E),
MeasureTheory.Integrable f (μ.prod ν) → ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
**Fubini's Theorem**: This theorem states that for a function `f` on a product space `α × β` that is integrable with respect to the product of measures `μ` and `ν`, the Bochner integral of `f` with respect to the product measure equals the iterated Bochner integral of `f` with respect to the measures `ν` and `μ`. In other words, the integral of `f` over the product space can be computed as an iteration of integrals over each individual space. The theorem assumes that both `μ` and `ν` are sigma-finite measures, and the integrable space `E` is a normed add commutative group over the reals. The functions `integrable_prod_iff` and `MeasureTheory.Integrable.integral_prod_right` can be useful to show that the function is integrable and that the inner integral of the right-hand side is integrable, respectively.
More concisely: Fubini's Theorem states that for a measurable and integrable function on a product measure space, its integral with respect to the product measure equals the iterated integral with respect to the measures on the individual factor spaces.
|
MeasureTheory.integral_integral_add
theorem MeasureTheory.integral_integral_add :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
⦃f g : α × β → E⦄,
MeasureTheory.Integrable f (μ.prod ν) →
MeasureTheory.Integrable g (μ.prod ν) →
∫ (x : α), ∫ (y : β), f (x, y) + g (x, y) ∂ν ∂μ =
∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ + ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
The theorem `MeasureTheory.integral_integral_add` states that double integrals commute with addition. In more detail, for two measurable spaces `α` and `β`, a measure `μ` on `α` and a measure `ν` on `β`, and two functions `f` and `g` from the product space `α × β` to a normed addative commutative group `E`, if `f` and `g` are both integrable with respect to the product measure `μ.prod ν`, then the double integral of the sum of `f` and `g` equals the sum of the double integrals of `f` and `g`, i.e., $\int_{α} \int_{β} [f(x,y) + g(x,y)] dν dμ = \int_{α} \int_{β} f(x,y) dν dμ + \int_{α} \int_{β} g(x,y) dν dμ$.
More concisely: For measurable spaces `α` and `β`, measures `μ` on `α` and `ν` on `β`, and integrable functions `f` and `g` from `α × β` to a normed additive commutative group `E`, their double integrals commute, i.e., $\int\int_{\alpha\times\beta} (f + g) d(\mu\cdot\nu) = \int\int_{\alpha\times\beta} f d(\mu\cdot\nu) + \int\int_{\alpha\times\beta} g d(\mu\cdot\nu)$.
|
MeasureTheory.Integrable.integral_prod_left
theorem MeasureTheory.Integrable.integral_prod_left :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] ⦃f : α × β → E⦄,
MeasureTheory.Integrable f (μ.prod ν) → MeasureTheory.Integrable (fun x => ∫ (y : β), f (x, y) ∂ν) μ
The theorem `MeasureTheory.Integrable.integral_prod_left` states that for any two types `α` and `β` with respective measures `μ` and `ν`, and a function `f` from the Cartesian product of `α` and `β` to another type `E` (where 'E' is a Normed Additive Commutative Group and a Normed Space over the Reals), if `f` is integrable with respect to the product measure of `μ` and `ν`, then the function that maps each element of `α` to the integral of `f` over `β` (with the element of `α` fixed) is also integrable with respect to measure `μ`. In other words, it allows us to integrate the function `f` with respect to one variable first, ensuring the result is still an integrable function of the remaining variable.
More concisely: Given measurable spaces `(α, μ)` and `(β, ν)`, a function `f : α × β → E` (where `E` is a real Normed Additive Commutative Group) that is μν-integrable, the function `g : α → E` defined by `g(a) = ∫β f(a, b) dν` is μ-integrable.
|
MeasureTheory.integrable_prod_iff
theorem MeasureTheory.integrable_prod_iff :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] ⦃f : α × β → E⦄,
MeasureTheory.AEStronglyMeasurable f (μ.prod ν) →
(MeasureTheory.Integrable f (μ.prod ν) ↔
(∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun y => f (x, y)) ν) ∧
MeasureTheory.Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ)
The theorem states that a binary function is integrable with respect to the product measure of two measures, if and only if the function, when it is fixed to an almost every value of the first variable, is integrable with respect to the second measure, and the function, mapping each value of the first variable to the integral of the absolute value of the function (when the first variable is fixed to that value) with respect to the second variable, is integrable with respect to the first measure. This condition holds if the binary function is almost everywhere equal to the limit of a sequence of simple functions with respect to the product measure.
More concisely: A binary function is integrable with respect to the product measure if and only if, for almost every value of the first variable, the function restricted to that value is integrable with respect to the second measure, and the function mapping each value of the first variable to the integral of its absolute value with respect to the second variable is integrable with respect to the first measure. Alternatively, if the binary function is almost everywhere equal to the limit of a sequence of simple functions with respect to the product measure.
|
MeasureTheory.integral_fn_integral_sub
theorem MeasureTheory.integral_fn_integral_sub :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
{E' : Type u_7} [inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace ℝ E'] ⦃f g : α × β → E⦄ (F : E → E'),
MeasureTheory.Integrable f (μ.prod ν) →
MeasureTheory.Integrable g (μ.prod ν) →
∫ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ =
∫ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ
This theorem states that the integral of a composite function, where the inner function is the difference of two integrable functions, is equal to the difference of the integrals of the composite functions with each individual integrable function. Specifically, if `f` and `g` are integrable functions over a product measure space, with the measures `μ` and `ν`, then the integral with respect to `μ` of the function `F` composed with the integral with respect to `ν` of the difference `f - g`, is equal to the integral with respect to `μ` of the function `F` composed with the difference of the integrals with respect to `ν` of `f` and `g`. This expresses a form of the commutativity of subtraction with respect to integration in measure theory.
More concisely: If `f` and `g` are integrable functions over a product measure space with measures `μ` and `ν`, then ∫(F ∘ (f - g) dμ dν) = ∫(F ∘ f dμ) - ∫(F ∘ g dμ), where F is a composite function.
|
MeasureTheory.lintegral_fn_integral_sub
theorem MeasureTheory.lintegral_fn_integral_sub :
∀ {α : Type u_1} {β : Type u_3} {E : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E]
[inst_3 : MeasureTheory.SigmaFinite ν] [inst_4 : NormedSpace ℝ E] [inst_5 : MeasureTheory.SigmaFinite μ]
⦃f g : α × β → E⦄ (F : E → ENNReal),
MeasureTheory.Integrable f (μ.prod ν) →
MeasureTheory.Integrable g (μ.prod ν) →
∫⁻ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ =
∫⁻ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ
This theorem states that integrals commute with subtraction within a lower Lebesgue integral. Specifically, given measurable spaces `α` and `β`, measures `μ` and `ν` on these spaces, two functions `f` and `g` mapping from the product space `α × β` to a normed add commutative group `E`, and a function `F` mapping from `E` to the extended nonnegative real numbers, if both `f` and `g` are integrable with respect to the product measure `μ.prod ν`, then the lower Lebesgue integral over `α` of `F` applied to the integral over `β` of the difference `f(x, y) - g(x, y)` with respect to `ν`, equals the lower Lebesgue integral over `α` of `F` applied to the difference of the integrals over `β` of `f(x, y)` and `g(x, y)` with respect to `ν`. In mathematical notation, this is:
∫ (over `α`) F(∫ (over `β`) [f(x, y) - g(x, y)] dν) dμ = ∫ (over `α`) F([∫ (over `β`) f(x, y) dν - ∫ (over `β`) g(x, y) dν]) dμ.
More concisely: The lower Lebesgue integral of the difference of two integrable functions with respect to a product measure commutes, i.e., the integral of the difference over one measure is equal to the difference of the integrals over both measures.
|