measurable_measure_prod_mk_left_finite
theorem measurable_measure_prod_mk_left_finite :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.IsFiniteMeasure ν] {s : Set (α × β)},
MeasurableSet s → Measurable fun x => ↑↑ν (Prod.mk x ⁻¹' s)
The theorem `measurable_measure_prod_mk_left_finite` states the following:
For any given types `α` and `β`, measurable spaces on `α` and `β`, a measure `ν` on `β` that is finite, and a set `s` in the product space `α × β` that is measurable, the function that maps each element `x` in `α` to the measure of the set of all `y` in `β` for which `(x, y)` is in `s`, is a measurable function.
In mathematical terms, this is saying that if `ν` is a finite measure, and `s` is a subset of the Cartesian product `α × β` that is measurable, then the function `x ↦ ν { y | (x, y) ∈ s }` is a measurable function. This theorem is a specific case of a more general result, `measurable_measure_prod_mk_left`.
More concisely: For any finite measurable space `(α, Σα)`, measurable space `(β, Σβ)`, measurable set `s ∈ Σα × Σβ`, and measure `ν` on `β`, the function `x ↦ ν(s₁⁻¹(x))`, where `s₁ = {(x, y) | (x, y) ∈ s}`, is a measurable function from `α` to the measurable space of real numbers.
|
MeasureTheory.Measure.prod_apply
theorem MeasureTheory.Measure.prod_apply :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] {s : Set (α × β)},
MeasurableSet s → ↑↑(μ.prod ν) s = ∫⁻ (x : α), ↑↑ν (Prod.mk x ⁻¹' s) ∂μ
This theorem, called `MeasureTheory.Measure.prod_apply`, states that for any types `α` and `β`, given the measurable spaces on `α` and `β`, a measure `μ` on `α`, a sigma-finite measure `ν` on `β`, and a measurable set `s` of pairs `(α, β)`, the measure of `s` with respect to the product measure of `μ` and `ν` is equal to the integral over `α` of the measure of the pre-image of `s` under the function that pairs `x` with elements of `β`, with respect to the measure `μ`. This is a formalization of the property of product measures in measure theory.
More concisely: For measurable spaces (α, μ) and (β, ν), and measurable set S of pairs (α, β), the product measure μ × ν of μ and ν satisfies (μ × ν)(S) = ∫x:α. μ( {α : α | (α, ∃β. (α, β) ∈ S) } ) dμ.
|
MeasureTheory.Measure.prod_swap
theorem MeasureTheory.Measure.prod_swap :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ], MeasureTheory.Measure.map Prod.swap (μ.prod ν) = ν.prod μ
The `MeasureTheory.Measure.prod_swap` theorem states that for any two types `α` and `β`, which are measurable spaces, and two measures `μ` and `ν` on these spaces that are sigma-finite, the measure of the swapped product pair `(b, a)` is the same as the measure of the original product pair `(a, b)`. In other words, the measure of the product space when `μ` is applied to `α` and `ν` is applied to `β` remains the same even if `α` and `β` are swapped, assuming the measure `map` is applied to the swap of the product pair.
More concisely: For measurable spaces `(α, Σα, μ)` and `(β, Σβ, ν)` with sigma-finite measures, `μ ⊗ ν` on `(α × β, Σα × Σβ)` equals `ν ⊗ μ` on `(β × α, Σβ × Σα)`.
|
MeasureTheory.Measure.prod_dirac
theorem MeasureTheory.Measure.prod_dirac :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SFinite μ] (y : β),
μ.prod (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.map (fun x => (x, y)) μ
The theorem `MeasureTheory.Measure.prod_dirac` states that for any measurable space `α` and `β`, any measure `μ` on `α` that is sigma-finite, and any element `y` of `β`, the product measure of `μ` and the dirac measure at `y` is equal to the pushforward of `μ` via the map that sends each element `x` of `α` to the pair `(x, y)`. In other words, it specifies how the dirac measure interacts with the operation of forming product measures.
More concisely: For any sigma-finite measure `μ` on measurable space `(α, Σα)`, and any `y` in measurable space `(β, Σβ)`, the product measure of `μ` and the Dirac measure at `y` is equal to the pushforward of `μ` under the map sending `x` to `(x, y)`.
|
Measurable.lintegral_prod_right
theorem Measurable.lintegral_prod_right :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] {f : α → β → ENNReal},
Measurable (Function.uncurry f) → Measurable fun x => ∫⁻ (y : β), f x y ∂ν
This theorem, named "Measurable.lintegral_prod_right", states that the Lebesgue integral is measurable. More specifically, given a measurable space `α`, another measurable space `β`, a measure `ν` on `β` that is `SFinite`, and a function `f` from `α` to `β` that yields extended nonnegative real numbers (`ENNReal`), if the uncurried form of `f` is measurable, then the Lebesgue integral of `f` with respect to `ν` is also measurable. In mathematical terms, for all `x` in `α`, the function that maps `x` to the integral from `β` to `ENNReal` of `f(x,y)` with respect to `ν` is measurable. This theorem is utilized to show that the integrand of Tonelli's theorem is measurable.
More concisely: Given measurable spaces `α` and `β`, a `SFinite` measure `ν` on `β`, and a measurable function `f` from `α` to `β` that maps to extended nonnegative real numbers, the function that maps each `x` in `α` to the Lebesgue integral of `f(x,y)` with respect to `ν` is measurable.
|
MeasureTheory.lintegral_prod_of_measurable
theorem MeasureTheory.lintegral_prod_of_measurable :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
(f : α × β → ENNReal), Measurable f → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
**Tonelli's Theorem**: Given two measurable spaces `α` and `β` with measures `μ` and `ν`, respectively, and a function `f` from the product space `α × β` to the set of extended nonnegative real numbers `[0, ∞]`, if `f` is a measurable function, then the integral of `f` with respect to the product measure `μ.prod ν` is equal to the iterated integral of `f` with respect to the measures `ν` and `μ`. In other words, we can swap the order of integration without changing the result, assuming finiteness of the measure `ν`. This is expressed in Lean as `∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ`.
More concisely: Given measurable spaces `α`, `β` with measures `μ` and `ν`, and a measurable function `f` from `α × β` to `[0, ∞]`, the iterated integrals of `f` with respect to `μ` then `ν` and `ν` then `μ` are equal: `∫⁻ (x, y : α × β), f x y ∂μ.prod ν = ∫⁻ (x : α) ∫⁻ (y : β), f x y ∂ν ∂μ`.
|
MeasureTheory.Measure.prod_def
theorem MeasureTheory.Measure.prod_def :
∀ {α : Type u_7} {β : Type u_8} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
(μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β),
μ.prod ν = μ.bind fun x => MeasureTheory.Measure.map (Prod.mk x) ν
This theorem states that for any two measurable spaces `α` and `β`, and for any two measures `μ` on `α` and `ν` on `β`, the binary product of the two measures `μ` and `ν` is equal to the measure resulting from binding the measure `μ` to a function that maps each element `x` of `α` to the measure of `β` obtained by pushing forward `ν` via the function `Prod.mk x` (which pairs `x` with each point in `β`). This relationship holds for arbitrary measures, but properties are mostly proven assuming that at least one of the measures is sigma-finite.
More concisely: For any measurable spaces `α` and `β` and measures `μ` on `α` and `ν` on `β`, `μ ⊤ (x ↓ᵢ β) = ∫ᵢxβ ν`, where `x ↓ᵢ β` is the fiber measure of `β` over `x` and `μ ⊤` is the outer measure induced by `μ`.
|
MeasureTheory.lintegral_lintegral
theorem MeasureTheory.lintegral_lintegral :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
⦃f : α → β → ENNReal⦄,
AEMeasurable (Function.uncurry f) (μ.prod ν) →
∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (z : α × β), f z.1 z.2 ∂μ.prod ν
This theorem is a reversed version of Tonelli's Theorem. It states that given two measurable spaces `α` and `β`, measures `μ` on `α` and `ν` on `β` (with `ν` being sigma-finite), and a function `f` from `α` and `β` to the extended nonnegative real numbers that is almost everywhere measurable when considered as a function on the product of `α` and `β`, the double integral of `f` with respect to `ν` and then `μ` is equal to the integral of `f` with respect to the product measure on `α × β`. In this version of the theorem, `f` is presented in its curried form (`f : α → β → ENNReal`), which makes it easier for Lean's elaborator to automatically figure out `f`.
More concisely: Given measurable spaces `α`, `β`, measures `μ` on `α` and `σ-finite ν` on `β`, and a curried almost everywhere measurable function `f : α → β → ENNReal`, the double integral of `f` with respect to `ν` then `μ` equals the integral of `f` with respect to the product measure on `α × β`.
|
MeasureTheory.MeasurePreserving.prod
theorem MeasureTheory.MeasurePreserving.prod :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {δ : Type u_7} [inst_3 : MeasurableSpace δ] {μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {μd : MeasureTheory.Measure δ}
[inst_4 : MeasureTheory.SFinite μa] [inst_5 : MeasureTheory.SFinite μc] {f : α → β} {g : γ → δ},
MeasureTheory.MeasurePreserving f μa μb →
MeasureTheory.MeasurePreserving g μc μd →
MeasureTheory.MeasurePreserving (Prod.map f g) (μa.prod μc) (μb.prod μd)
The theorem `MeasureTheory.MeasurePreserving.prod` states that for types `α, β, γ, δ` which have associated measurable spaces and for measures `μa` on `α`, `μb` on `β`, `μc` on `γ`, and `μd` on `δ` (where `μa` and `μc` are sigma-finite), if a function `f : α → β` preserves the measure from `μa` to `μb` and a function `g : γ → δ` preserves the measure from `μc` to `μd`, then the `Prod.map` of `f` and `g` preserves the product measure from `μa.prod μc` to `μb.prod μd`.
More concisely: Given measurable spaces `(α, σα)`, `(β, σβ)`, `(γ, σγ)`, and `(δ, σδ)`, and sigma-finite measures `μa` on `α`, `μb` on `β`, `μc` on `γ`, and `μd` on `δ`, if functions `f : α → β` and `g : γ → δ` preserve the measures `μa` and `μc` respectively, then the composite function `Prod.map f g` preserves the product measure `μa.prod μc` of `μa` and `μc` on the product space `α × γ`.
|
MeasureTheory.Measure.quasiMeasurePreserving_snd
theorem MeasureTheory.Measure.quasiMeasurePreserving_snd :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν],
MeasureTheory.Measure.QuasiMeasurePreserving Prod.snd (μ.prod ν) ν
The theorem `MeasureTheory.Measure.quasiMeasurePreserving_snd` states that for any types `α` and `β` with their respective measurable spaces, and given measures `μ` on `α` and `ν` on `β`, where `ν` is s-finite (meaning it can be approximated by a finite measure), the second projection function `Prod.snd` is a quasi measure preserving function. In other words, if we take the product measure of `μ` and `ν`, and then apply the function `Prod.snd` to this product measure, we get the measure `ν` back. This theorem is a part of measure theory, which is a branch of mathematics that studies measurable spaces and measures on them.
More concisely: Given measurable spaces (α, μ) and (β, ν), where ν is s-finite, the second projection function Prod.snd is a quasi-measure preserving function between the product measure μ × ν and ν.
|
MeasureTheory.NullMeasurableSet.of_preimage_fst
theorem MeasureTheory.NullMeasurableSet.of_preimage_fst :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ] [inst_4 : NeZero ν] {s : Set α},
MeasureTheory.NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν) → MeasureTheory.NullMeasurableSet s μ
The theorem `MeasureTheory.NullMeasurableSet.of_preimage_fst` states that for any given set `s` of a certain type `α`, if the preimage of `s` under the first projection function `Prod.fst` is a null measurable set in the product measure space of `μ` and `ν`, and if `ν` is not zero, then `s` is also a null measurable set in the measure space defined by `μ`. Here, a null measurable set is a set that can be approximated by a measurable set up to a set of null measure. The first projection function `Prod.fst` takes a pair and returns the first component of the pair. The term `Prod.fst ⁻¹' s` refers to the preimage of `s` under the function `Prod.fst`, which is the set of all pairs whose first component belongs to `s`.
More concisely: If the preimage of a set `s` under the first projection function `Prod.fst` is a null measurable set in the product measure space with respect to measures `μ` and `ν` (where `ν` is not zero), then `s` is a null measurable set in the measure space defined by `μ`.
|
MeasureTheory.Measure.nullMeasurableSet_preimage_fst
theorem MeasureTheory.Measure.nullMeasurableSet_preimage_fst :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ] [inst_4 : NeZero ν] {s : Set α},
MeasureTheory.NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet s μ
The theorem `MeasureTheory.Measure.nullMeasurableSet_preimage_fst` states that for any given types `α` and `β`, measurable spaces `α` and `β`, measures `μ` on `α` and `ν` on `β`, provided that `ν` is not zero, for any set `s` of `α`, the preimage of `s` under the first projection function (i.e., `Prod.fst ⁻¹' s`) is null measurable with respect to the product measure `μ.prod ν` if and only if `s` is null measurable with respect to `μ`. Here, a set is called null measurable if it can be approximated by a measurable set up to a set of null measure.
More concisely: For measurable spaces (α, μ) and (β, ν) with ν being non-zero, the preimage of a null measurable set in α under the first projection function is null measurable with respect to the product measure μ.prod ν.
|
MeasureTheory.NullMeasurableSet.left_of_prod
theorem MeasureTheory.NullMeasurableSet.left_of_prod :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ] {s : Set α} {t : Set β},
MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) → ↑↑ν t ≠ 0 → MeasureTheory.NullMeasurableSet s μ
The theorem `MeasureTheory.NullMeasurableSet.left_of_prod` states that, given two types `α` and `β` with their respective measurable spaces and measures `μ` and `ν`, if the Cartesian product `s ×ˢ t` of two sets `s` and `t` forms a null measurable set, and the measure of set `t` under `ν` is not zero, then set `s` is a null measurable set under measure `μ`. This essentially means that if a set product is approximately measurable excluding a negligible part and one factor set has non-zero measure, then the other factor set is also approximately measurable excluding a negligible part.
More concisely: If the Cartesian product of two sets is null measurable and the measure of one factor is not zero, then the other factor is null measurable.
|
MeasureTheory.Measure.prod_restrict
theorem MeasureTheory.Measure.prod_restrict :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ] (s : Set α) (t : Set β),
(μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
This theorem, from the field of measure theory, states that for any two types `α` and `β` which are measurable spaces and for any two sigma-finite measures `μ` and `ν` defined on these spaces, along with any sets `s` of type `α` and `t` of type `β`, the product measure of the restrictions of `μ` and `ν` to the sets `s` and `t` respectively, is equal to the restriction of the product measure of `μ` and `ν` to the cartesian product of the sets `s` and `t`. This is essentially a statement about how measures behave under restrictions and products.
More concisely: For any measurable spaces `(α, Σα, μ)` and `(β, Σβ, ν)` with sigma-finite measures `μ` and `ν`, the product measure of `μ` restricted to a set `s ∈ Σα` and `ν` restricted to a set `t ∈ Σβ` equals the restriction of the product measure of `μ` and `ν` to the cartesian product `s × t`.
|
MeasureTheory.NullMeasurableSet.right_of_prod
theorem MeasureTheory.NullMeasurableSet.right_of_prod :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] {s : Set α}
{t : Set β},
MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) → ↑↑μ s ≠ 0 → MeasureTheory.NullMeasurableSet t ν
This theorem states that for any two sets `s` and `t` of any two types `α` and `β`, respectively, equipped with measurable spaces and measures `μ` and `ν` respectively, if the product set `s ×ˢ t` is a null measurable set with respect to the product measure of `μ` and `ν`, and the measure of the set `s` is not zero, then the set `t` itself is a null measurable set with respect to the measure `ν`. This theorem holds under the assumption that the measure `ν` is sigma-finite. In other words, if a set in the product space is approximately measurable and the first factor has non-zero measure, then the second factor is also approximately measurable.
More concisely: If `s` and `t` are measurable sets of types `α` and `β` respectively, equipped with sigma-finite measures `μ` and `ν`, and the product `s ×ˢ t` is null with respect to the product measure of `μ` and `ν`, then `t` is null with respect to `ν`, given that `μ(s) ≠ 0`.
|
AEMeasurable.fst
theorem AEMeasurable.fst :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
[inst_3 : MeasureTheory.SFinite ν] {f : α → γ}, AEMeasurable f μ → AEMeasurable (fun z => f z.1) (μ.prod ν)
This theorem states that for any function `f`, from a type `α` to a type `γ`, which is almost everywhere measurable with respect to a measure `μ` on `α`, the function that takes a pair `(z1, z2)` to `f(z1)` is also almost everywhere measurable with respect to the product measure of `μ` and another measure `ν` on a type `β`. This holds under the condition that the measure `ν` is s-finite, meaning it can be decomposed into a countably finite union of sets with finite measure.
More concisely: If `μ` is a measure on `α` and `ν` is an s-finite measure on `β`, then the function `(z1, z2) mapsto f(z1)` is almost everywhere measurable with respect to the product measure of `μ` and `ν`, for any almost everywhere measurable function `f` from `α` to `γ`.
|
MeasureTheory.Measure.fst_apply
theorem MeasureTheory.Measure.fst_apply :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)} {s : Set α}, MeasurableSet s → ↑↑ρ.fst s = ↑↑ρ (Prod.fst ⁻¹' s)
The theorem `MeasureTheory.Measure.fst_apply` states that for any types `α` and `β` with measurable spaces `inst` and `inst_1` respectively, any measure `ρ` on the product space `α × β`, and any set `s` of `α` that is a measurable set, the measure of `s` under the map `MeasureTheory.Measure.fst ρ` (i.e., the measure obtained by projecting `ρ` onto its first component) is equal to the measure `ρ` of the preimage of `s` under the projection function `Prod.fst` (i.e., the set of all pairs `(a, b)` in `α × β` such that `a` is in `s`). In mathematical terms, if `s ⊆ α` is measurable, then `(MeasureTheory.Measure.fst ρ) s = ρ ({(a, b) ∈ α × β : a ∈ s})`.
More concisely: For any measurable sets `s ⊆ α` in measurable spaces `α × β`, the measure of `s` under the projection function `MeasureTheory.Measure.fst` on a product measure `ρ` equals the measure of the preimage of `s` under the `Prod.fst` function.
|
Measurable.lintegral_prod_right'
theorem Measurable.lintegral_prod_right' :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] {f : α × β → ENNReal},
Measurable f → Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
The theorem states that the Lebesgue integral is a measurable function. Specifically, if we have two measurable spaces `α` and `β`, a measure `ν` on `β` that is sigma-finite, and a measurable function `f` from the product space `α × β` to the extended nonnegative real numbers (ENNReal), then the function that assigns to each `x` in `α` the Lebesgue integral over `β` of `f(x, y)` with respect to `ν` is also measurable. This result is particularly important as it ensures the integrand on the right-hand side of Tonelli's theorem is measurable.
More concisely: Given measurable spaces `α` and `β`, a sigma-finite measure `ν` on `β`, and a measurable function `f` from the product space `α × β` to the extended nonnegative real numbers, the function assigning to each `x` in `α` the Lebesgue integral of `f(x, y)` over `β` with respect to `ν` is measurable.
|
MeasureTheory.Measure.measurePreserving_swap
theorem MeasureTheory.Measure.measurePreserving_swap :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ], MeasureTheory.MeasurePreserving Prod.swap (μ.prod ν) (ν.prod μ)
The theorem `MeasureTheory.Measure.measurePreserving_swap` states that for any pair of types `α` and `β` equipped with structures of measurable spaces and measures `μ` and `ν` respectively, where both measures are sigma-finite, the function `Prod.swap` is measure-preserving with respect to the product measures on `α × β` and `β × α`. In other words, swapping the factors in the product of two measures does not change the product measure. This corresponds to the mathematical statement that the product of two measures is invariant under the swap of the factors, assuming both measures are sigma-finite.
More concisely: For any sigma-finite measurable spaces `(α, Σα, μ)` and `(β, Σβ, ν)`, the product measures `μ ⨝ ν` and `ν ⨝ μ` on `α × β` are equal.
|
generateFrom_prod
theorem generateFrom_prod :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
MeasurableSpace.generateFrom (Set.image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t}) =
Prod.instMeasurableSpace
This theorem states that the product σ-algebra (which is a type of measure space) is generated from Cartesian products of sets. More specifically, for any two types `α` and `β` each equipped with a measurable space structure, the smallest σ-algebra containing all Cartesian products (`s ×ˢ t`) of measurable sets `s` of `α` and measurable sets `t` of `β` is precisely the σ-algebra given by the product of the measurable spaces of `α` and `β`.
In mathematical terms, it can be expressed as follows: Let `α` and `β` be sets equipped with measurable spaces. Then the product σ-algebra on the Cartesian product `α × β` is generated by the sets of the form `s × t`, where `s` is a measurable set in `α` and `t` is a measurable set in `β`.
More concisely: The product σ-algebra on the Cartesian product of two measurable spaces is generated by the measurable Cartesian products of sets from each space.
|
isPiSystem_prod
theorem isPiSystem_prod :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β],
IsPiSystem (Set.image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t})
The theorem `isPiSystem_prod` states that rectangles form a π-system. Specifically, for any types `α` and `β` which each have a measurable space structure, the set of all Cartesian products `{x ×ˢ x_1 | x ∈ subset of measurable sets in α, x_1 ∈ subset of measurable sets in β}` forms a π-system. In mathematical terms, this means that if you take two such Cartesian product sets (which we can think of as rectangles) that are not disjoint, then their intersection is also a member of this set. Thus, this set is closed under binary intersection of non-disjoint sets, satisfying the definition of a π-system.
More concisely: The set of all Cartesian products of measurable subsets from two measurable spaces forms a π-system.
|
MeasureTheory.Measure.measure_prod_null
theorem MeasureTheory.Measure.measure_prod_null :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] {s : Set (α × β)},
MeasurableSet s → (↑↑(μ.prod ν) s = 0 ↔ μ.ae.EventuallyEq (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) 0)
The theorem `MeasureTheory.Measure.measure_prod_null` states that for any given types `α` and `β` equipped with measure spaces, any measures `μ` and `ν` on `α` and `β` respectively (with `ν` being sigma-finite), and any measurable set `s` of pairs from `α` and `β`, the measure of `s` under the product measure of `μ` and `ν` is zero if and only if the measure of the preimage of `s` under the function that pairs each element of `α` with `β` is almost everywhere zero with respect to the measure `μ`. Here, "almost everywhere" is in reference to the filter of co-null sets in the measure space. The theorem also notes that the measurability assumption on `s` cannot be omitted, referencing an example in Walter Rudin's book *Real and Complex Analysis*.
More concisely: The product measure of two sigma-finite measures is zero on a set in the product space if and only if the preimage of that set under the diagonal function is almost everywhere null with respect to the first measure.
|
MeasureTheory.Measure.prod_eq
theorem MeasureTheory.Measure.prod_eq :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SigmaFinite μ] {ν : MeasureTheory.Measure β}
[inst_3 : MeasureTheory.SigmaFinite ν] {μν : MeasureTheory.Measure (α × β)},
(∀ (s : Set α) (t : Set β), MeasurableSet s → MeasurableSet t → ↑↑μν (s ×ˢ t) = ↑↑μ s * ↑↑ν t) → μ.prod ν = μν
This theorem states that for any types `α` and `β` with given measurable spaces, if we have sigma-finite measures `μ` on `α` and `ν` on `β`, and another measure `μν` on the product space `α × β`, then if `μν` equals the product of `μ` and `ν` on all measurable rectangles (that is, for all measurable sets `s` of `α` and `t` of `β`, the measure of their Cartesian product under `μν` equals the product of their individual measures under `μ` and `ν` respectively), then the product measure of `μ` and `ν` is equal to `μν`. This theorem essentially provides a uniqueness condition for the product measure in the setting of sigma-finite measures.
More concisely: If two sigma-finite measures on measurable spaces `α` and `β` have equal product measures on all measurable rectangles, then they are equal as measures on the product space `α × β`.
|
MeasureTheory.Measure.map_prod_map
theorem MeasureTheory.Measure.map_prod_map :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {δ : Type u_7} [inst_3 : MeasurableSpace δ] {f : α → β} {g : γ → δ}
(μa : MeasureTheory.Measure α) (μc : MeasureTheory.Measure γ) [inst_4 : MeasureTheory.SFinite μa]
[inst_5 : MeasureTheory.SFinite μc],
Measurable f →
Measurable g →
(MeasureTheory.Measure.map f μa).prod (MeasureTheory.Measure.map g μc) =
MeasureTheory.Measure.map (Prod.map f g) (μa.prod μc)
The theorem `MeasureTheory.Measure.map_prod_map` states that for any measurable spaces α, β, γ, δ, any measurable functions `f` from α to β and `g` from γ to δ, and any σ-finite measures `μa` on α and `μc` on γ, the measure of the product of the spaces resulting from mapping `f` and `g` under `μa` and `μc` respectively, is equal to the measure resulting from mapping the product function `Prod.map f g` under the product measure of `μa` and `μc`. Essentially, it states that the pushing forward measures with a pair of functions then taking the product measure is the same as taking the product measure then pushing forward with the product function.
More concisely: For measurable spaces α, β, γ, δ, measurable functions f : α → β and g : γ → δ, and σ-finite measures μa on α and μc on γ, the measure of the product of the spaces α × γ under the measures μa ⊤μc and μa ⊤ (Prod.map f g) μc is equal.
|
Measurable.lintegral_prod_left'
theorem Measurable.lintegral_prod_left' :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SFinite μ] {f : α × β → ENNReal},
Measurable f → Measurable fun y => ∫⁻ (x : α), f (x, y) ∂μ
The theorem `Measurable.lintegral_prod_left'` states that the Lebesgue integral is a measurable function. More specifically, given a measurable space `α`, another measurable space `β`, a measure `μ` on `α` that is sigma finite, and a measurable function `f` from the product of `α` and `β` to the extended nonnegative real numbers (`ENNReal`), the function that maps each element `y` of `β` to the Lebesgue integral over `α` of the function `x ↦ f(x, y)` with respect to `μ` is measurable. This establishes the measurability of the integrand of the symmetric version of Tonelli's theorem.
More concisely: Given a sigma-finite measure `μ` on a measurable space `α` and a measurable function `f` from the product of `α` and another measurable space `β` to the extended nonnegative real numbers, the function that maps each `y` in `β` to the Lebesgue integral of `x ↦ f(x, y)` over `α` is measurable.
|
MeasureTheory.NullMeasurableSet.of_preimage_snd
theorem MeasureTheory.NullMeasurableSet.of_preimage_snd :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] [inst_3 : NeZero μ]
{t : Set β}, MeasureTheory.NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν) → MeasureTheory.NullMeasurableSet t ν
The theorem `MeasureTheory.NullMeasurableSet.of_preimage_snd` states that for any given types `α` and `β` with their respective measurable spaces, and measures `μ` on `α` and `ν` on `β`, if `μ` is non-zero, `ν` is sigma-finite, and the preimage of a set `t` under the second projection function `Prod.snd` is a null measurable set with respect to the product measure of `μ` and `ν`, then `t` itself is a null measurable set with respect to `ν`. In other words, if a set obtained by projecting onto the second component of a pair is approximately a measurable set, then the original set is also approximately a measurable set.
More concisely: If `μ` is a non-zero measure on `α`, `ν` is sigma-finite on `β`, and the preimage of a null measurable set `t` under the second projection function `Prod.snd` is null measurable with respect to the product measure of `μ` and `ν`, then `t` itself is null measurable with respect to `ν`.
|
MeasureTheory.Measure.prod_sum
theorem MeasureTheory.Measure.prod_sum :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ι : Type u_7}
{ι' : Type u_8} [inst_2 : Countable ι'] (m : ι → MeasureTheory.Measure α) (m' : ι' → MeasureTheory.Measure β)
[inst_3 : ∀ (n : ι'), MeasureTheory.SFinite (m' n)],
(MeasureTheory.Measure.sum m).prod (MeasureTheory.Measure.sum m') =
MeasureTheory.Measure.sum fun p => (m p.1).prod (m' p.2)
This theorem states that for any index sets `ι` and `ι'` (where `ι'` is countable), and corresponding families of measures `m` on a measurable space `α` and `m'` on a measurable space `β` (such that every measure `m'(n)` for `n` in `ι'` is s-finite), the measure of the product of the sum of the `m` measures and the sum of the `m'` measures is equal to the sum of the measures of the products of the `m` and `m'` measures, indexed by pairs of elements from `ι` and `ι'`. In mathematical terms, it asserts that `(∑m)⨂(∑m') = ∑(m⨂m')` over the product space `α × β`.
More concisely: For countable index sets `ι` and `ι'`, and families of s-finite measures `m` on a measurable space `α` and `m'` on a measurable space `β`, the measure of the product of the sum of `m` and the sum of `m'` is equal to the sum of the measures of the products of `m` and `m'`. That is, `(∑m)⨂(∑m') = ∑(m⨂m')` over the product space `α × β`.
|
MeasureTheory.MeasurePreserving.skew_product
theorem MeasureTheory.MeasurePreserving.skew_product :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
[inst_2 : MeasurableSpace γ] {δ : Type u_7} [inst_3 : MeasurableSpace δ] {μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {μd : MeasureTheory.Measure δ}
[inst_4 : MeasureTheory.SFinite μa] [inst_5 : MeasureTheory.SFinite μc] {f : α → β},
MeasureTheory.MeasurePreserving f μa μb →
∀ {g : α → γ → δ},
Measurable (Function.uncurry g) →
(∀ᵐ (x : α) ∂μa, MeasureTheory.Measure.map (g x) μc = μd) →
MeasureTheory.MeasurePreserving (fun p => (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)
This theorem, named `MeasureTheory.MeasurePreserving.skew_product`, states the following: for every measurable spaces `α`, `β`, `γ`, `δ` and measures `μa` on `α`, `μb` on `β`, `μc` on `γ`, `μd` on `δ`, where `μa` and `μc` are sigma-finite, and every function `f` from `α` to `β`, if `f` preserves the measure `μa` to `μb`, then for every function `g` from `α → γ` to `δ` that is measurable when uncurried, if almost every `x` in `α` with respect to measure `μa` maps to a measure `μd` under the function `g x`, then the function that maps a pair `p` to `(f p.1, g p.1 p.2)` preserves the product measure `μa × μc` to the product measure `μb × μd`. In essence, under these conditions, the "skew product" of `f` and `g` preserves the product measure from `α × γ` to `β × δ`.
More concisely: If `α`, `β`, `γ`, `δ` are measurable spaces, `μa` and `μc` are sigma-finite measures on `α` and `γ` respectively, `f: α → β` is measure-preserving for `μa` and `μb`, and `g: α → δ` is a measurable function such that almost every `x` in `α` maps to a non-zero measure under `μd` when applying `g` with respect to `μa`, then the function `(f, g): α × γ → β × δ`, defined by `(f, g)(p) = (f p.1, g p.1 p.2)`, preserves the product measures `μa × μc` and `μb × μd`.
|
MeasureTheory.Measure.quasiMeasurePreserving_fst
theorem MeasureTheory.Measure.quasiMeasurePreserving_fst :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν],
MeasureTheory.Measure.QuasiMeasurePreserving Prod.fst (μ.prod ν) μ
The theorem `MeasureTheory.Measure.quasiMeasurePreserving_fst` states that for any two types `α` and `β` with associated measurable spaces, and for any given measures `μ` and `ν` on `α` and `β` respectively, where `ν` is s-finite (i.e., it can be approximated by a finite measure), the function `Prod.fst` which gives the first projection of a pair, is quasi-measure-preserving. In other words, when we consider the product measure of `μ` and `ν` on the product space `α × β`, projecting this measure onto the `α` part via `Prod.fst` preserves the original measure `μ` on `α`.
More concisely: Given measurable spaces `(α, Σα, μ)` and `(β, Σβ, ν)` where `ν` is s-finite, the function `Prod.fst : α × β → α` is quasi-measure-preserving with respect to the product measure `μ ⊗ ν` on `(α × β, Σα × Σβ)`.
|
MeasureTheory.Measure.measure_ae_null_of_prod_null
theorem MeasureTheory.Measure.measure_ae_null_of_prod_null :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] {s : Set (α × β)},
↑↑(μ.prod ν) s = 0 → μ.ae.EventuallyEq (fun x => ↑↑ν (Prod.mk x ⁻¹' s)) 0
This theorem is from the field of measure theory, specifically regarding product measures. It states that for any types `α` and `β`, along with measurable spaces over these types, and given measures `μ` and `ν` over these spaces, respectively (with `ν` being sigma-finite), if a set `s` of the product space `(α × β)` has measure zero under the product measure `μ.prod ν`, then almost everywhere with respect to measure `μ`, the preimage of `s` under the function that maps `x` to `(x, y)`, for `y` in `β`, has measure zero under measure `ν`.
In other words, if a set in the product space has a product measure of zero, then for almost all `x` in `α`, the set of `y` in `β` such that `(x, y)` is in the original set, has a `ν`-measure of zero. Note that this doesn't hold the other way around without the assumption that `s` is measurable.
More concisely: For measurable spaces `(α, Σα)` and `(β, Σβ)` with sigma-finite measure `ν` on `(β, Σβ)`, if a measurable set `s` in the product space `(α × β, Σα × Σβ)` has product measure `μ.prod ν(s) = 0`, then almost everywhere in `α` with respect to `μ`, the set `{y ∈ β | (x, y) ∈ s}` has `ν` measure zero for all `x ∈ α`.
|
MeasureTheory.Measure.nullMeasurableSet_prod
theorem MeasureTheory.Measure.nullMeasurableSet_prod :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ] {s : Set α} {t : Set β},
MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
MeasureTheory.NullMeasurableSet s μ ∧ MeasureTheory.NullMeasurableSet t ν ∨ ↑↑μ s = 0 ∨ ↑↑ν t = 0
The theorem `MeasureTheory.Measure.nullMeasurableSet_prod` states that for any two sets `s` and `t` from respective measure spaces `α` and `β`, the product of `s` and `t` is a null measurable set with respect to the product measure `(μ.prod ν)` if and only if either both `s` and `t` are null measurable sets with respect to their respective measures `μ` and `ν`, or one of them (`s` or `t`) has measure zero. Here, a set is null measurable if it can be approximated by a measurable set up to a set of null measure.
More concisely: A set in the product of two measure spaces is null measurable with respect to the product measure if and only if both sets are null measurable with respect to their respective measures or one of them has measure zero.
|
measurable_measure_prod_mk_left
theorem measurable_measure_prod_mk_left :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] {s : Set (α × β)},
MeasurableSet s → Measurable fun x => ↑↑ν (Prod.mk x ⁻¹' s)
The theorem `measurable_measure_prod_mk_left` states that if we have a measure `ν` on a measurable space `β` which is s-finite (i.e., can be decomposed into a countable union of sets with finite measure), and a measurable set `s` in the product space `α × β`, then the function that maps each element `x` of `α` to the measure of the set of `y` in `β` such that `(x, y)` is in `s`, is a measurable function. In other words, for every `x` in `α`, the measure of the set `{ y | (x, y) ∈ s }` is a measurable function of `x`. This theorem is fundamental in the study of product measures and their properties.
More concisely: If `ν` is an s-finite measure on a measurable space `β`, and `s` is a measurable set in the product space `α × β`, then the function that maps each `x` in `α` to the measure of `{ y | (x, y) ∈ s }` is measurable.
|
measurable_measure_prod_mk_right
theorem measurable_measure_prod_mk_right :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SFinite μ] {s : Set (α × β)},
MeasurableSet s → Measurable fun y => ↑↑μ ((fun x => (x, y)) ⁻¹' s)
The theorem `measurable_measure_prod_mk_right` states that if `μ` is a σ-finite measure and `s` is a subset of the Cartesian product of `α` and `β` that is measurable, then the function `y ↦ μ { x | (x, y) ∈ s }` is also measurable. In other words, for a σ-finite measure `μ` and a measurable set `s` in the product space of `α` and `β`, the function that maps each `y` to the measure of the set of `x` such that `(x, y)` is in `s` is a measurable function.
More concisely: If `μ` is a σ-finite measure and `s` is a measurable subset of the product space `α × β`, then the function `y ↦ μ { x | (x, y) ∈ s }` is a measurable function.
|
generateFrom_prod_eq
theorem generateFrom_prod_eq :
∀ {α : Type u_7} {β : Type u_8} {C : Set (Set α)} {D : Set (Set β)},
IsCountablySpanning C →
IsCountablySpanning D →
Prod.instMeasurableSpace = MeasurableSpace.generateFrom (Set.image2 (fun x x_1 => x ×ˢ x_1) C D)
The theorem `generateFrom_prod_eq` states that for any two sets of sets `C` and `D` over types `α` and `β` respectively, if both `C` and `D` are countably spanning (that is, a countable subset of each can span the whole type), then the measurable space formed by the product of the individual measurable spaces generated by `C` and `D` is identical to the measurable space generated by the set of all ordered pairs (rectangles) formed by an element from `C` and an element from `D`. The function `(fun x x_1 => x ×ˢ x_1)` is used to create these ordered pairs. This theorem is used in measure theory to relate the product of generated σ-algebras to the σ-algebra generated by rectangles.
More concisely: If sets `C` over type `α` and `D` over type `β` are countably spanning, then the measurable space generated by their product is equal to the measurable space generated by all rectangles formed by an element from `C` and an element from `D`.
|
MeasureTheory.Measure.snd_apply
theorem MeasureTheory.Measure.snd_apply :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{ρ : MeasureTheory.Measure (α × β)} {s : Set β}, MeasurableSet s → ↑↑ρ.snd s = ↑↑ρ (Prod.snd ⁻¹' s)
The theorem `MeasureTheory.Measure.snd_apply` states that for any types `α` and `β`, which have associated measurable spaces, any measure `ρ` on the product space `α × β`, and any set `s` of `β` that is measurable, the measure of `s` under the marginal measure on `β` obtained from `ρ` (noted as `MeasureTheory.Measure.snd ρ s`) is equal to the measure under `ρ` of the preimage of `s` under the second projection function (`Prod.snd`). In other words, the measure of a set in the marginal distribution is the same as the measure of the set of pairs that map to that set in the original distribution.
More concisely: For any measurable spaces (α, Σα) and (β, Σβ), measurable set s ∈ Σβ, and measure ρ on the product space (α × β) with Σα × Σβ-measurable second projection function p, the measure of s under the marginal measure on β (MeasureTheory.Measure.snd ρ s) equals the measure of p⁁⁻¹(s) under ρ.
|
MeasureTheory.lintegral_lintegral_symm
theorem MeasureTheory.lintegral_lintegral_symm :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ] ⦃f : α → β → ENNReal⦄,
AEMeasurable (Function.uncurry f) (μ.prod ν) →
∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (z : β × α), f z.2 z.1 ∂ν.prod μ
This theorem is a reversed version of Tonelli's Theorem, which states that for a measure space `α` and `β` with measures `μ` and `ν` respectively and a function `f` from `α × β` to the extended nonnegative real numbers, if the uncurried function `f` is almost everywhere measurable with respect to the product measure `μ.prod ν`, then the nested integral of `f` with respect to `ν` then `μ` is equal to the integral of `f` with its arguments flipped with respect to the product measure `ν.prod μ`. This version of the theorem is particularly useful in scenarios where automated tools struggle to infer the function `f`.
More concisely: If `μ` and `ν` are measures on measurable spaces `α` and `β` respectively, and `f : α × β → ℝ∞`, is almost everywhere measurable with respect to the product measure `μ.prod ν`, then:
∫∫ₙₙⁱⁱ `f`(x, y) d(`μ.prod ν`) (x, y) = ∫∫ₙₙⁱⁱ `f`(y, x) d(`ν.prod μ`) (y, x)
|
MeasureTheory.Measure.nullMeasurableSet_prod_of_ne_zero
theorem MeasureTheory.Measure.nullMeasurableSet_prod_of_ne_zero :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ] {s : Set α} {t : Set β},
↑↑μ s ≠ 0 →
↑↑ν t ≠ 0 →
(MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
MeasureTheory.NullMeasurableSet s μ ∧ MeasureTheory.NullMeasurableSet t ν)
The theorem `MeasureTheory.Measure.nullMeasurableSet_prod_of_ne_zero` states that for any two sets `s` and `t` of types `α` and `β` respectively, given that they are equipped with measurable spaces and sigma-finite measures `μ` and `ν`, the product of `s` and `t` is a null measurable set with respect to the product measure `μ.prod ν` if and only if both `s` and `t` are null measurable sets with respect to `μ` and `ν` respectively. This is provided that neither `s` or `t` are null sets, i.e., neither `μ s` nor `ν t` is zero.
More concisely: For two sigma-finite measurable sets `s` of type `α` and `t` of type `β`, equipped with measures `μ` and `ν` respectively, their product is a null measurable set with respect to the product measure `μ.prod ν` if and only if both `s` and `t` are null measurable sets with respect to `μ` and `ν` respectively, and neither is a null set.
|
MeasureTheory.Measure.nullMeasurableSet_preimage_snd
theorem MeasureTheory.Measure.nullMeasurableSet_preimage_snd :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] [inst_3 : NeZero μ]
{t : Set β}, MeasureTheory.NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν) ↔ MeasureTheory.NullMeasurableSet t ν
The theorem `MeasureTheory.Measure.nullMeasurableSet_preimage_snd` states that for all measurable spaces `α` and `β`, with measures `μ` and `ν` respectively, and for a set `t` of `β`, the preimage of `t` under the second projection of a product (i.e., `Prod.snd ⁻¹' t`) is null measurable with respect to the product measure `μ.prod ν` if and only if `t` itself is null measurable with respect to the measure `ν`, provided that the measure `μ` is not zero. Here, a set is said to be null measurable if it can be approximated by a measurable set up to a set of null measure. The condition `μ ≠ 0` ensures that the measure `μ` is not a zero measure.
More concisely: For measurable spaces `α`, `β` with measures `μ` and `ν`, and a null measurable set `t` in `β`, the preimage of `t` under the second projection of their product, `Prod.snd ⁻¹' t`, is null measurable with respect to the product measure `μ.prod ν` if and only if `μ ≠ 0`.
|
MeasureTheory.Measure.prod_eq_generateFrom
theorem MeasureTheory.Measure.prod_eq_generateFrom :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {C : Set (Set α)} {D : Set (Set β)},
MeasurableSpace.generateFrom C = inst →
MeasurableSpace.generateFrom D = inst_1 →
IsPiSystem C →
IsPiSystem D →
μ.FiniteSpanningSetsIn C →
ν.FiniteSpanningSetsIn D →
∀ {μν : MeasureTheory.Measure (α × β)},
(∀ s ∈ C, ∀ t ∈ D, ↑↑μν (s ×ˢ t) = ↑↑μ s * ↑↑ν t) → μ.prod ν = μν
This theorem states that for any two types `α` and `β` with their respective measurable spaces and measures (`μ` for `α` and `ν` for `β`), if we have two sets `C` and `D` such that the measurable spaces generated from `C` and `D` are the same as the original measurable spaces and both `C` and `D` are π-systems, and `μ` and `ν` have finite spanning sets in `C` and `D` respectively, then for any measure `μν` on the product space of `α` and `β`, if `μν` of the product set `s ×ˢ t` equals the product of `μ` of `s` and `ν` of `t` for all `s` in `C` and `t` in `D`, then the product measure of `μ` and `ν` is equal to `μν`. In essence, it's saying that the measure on a product space equals the product measure if they give the same values on rectangles generated by the σ-algebras.
More concisely: If two measurable spaces `(α, σ(`α`), μ)` and `(β, σ(`β`), ν)` have identical measurable structures, `C` and `D` are π-systems generating these structures, and have finite measure spanning sets, then equal product measures on rectangles `s ×ˢ t` in `C` and `D` imply equal product measures `μ ⊛ ν` on the product measurable space.
|
IsPiSystem.prod
theorem IsPiSystem.prod :
∀ {α : Type u_1} {β : Type u_3} {C : Set (Set α)} {D : Set (Set β)},
IsPiSystem C → IsPiSystem D → IsPiSystem (Set.image2 (fun x x_1 => x ×ˢ x_1) C D)
The theorem `IsPiSystem.prod` states that for any types `α` and `β`, and for any sets `C` and `D` which are π-systems (collections of subsets that are closed under binary intersection of non-disjoint sets), the set formed by the Cartesian product of elements from `C` and `D` is also a π-system. More specifically, it uses the `Set.image2` function to construct the Cartesian product of the sets in `C` and `D`, and asserts that this is a π-system. In other words, if we take any two rectangles (which are Cartesian products of sets), and if their intersection is nonempty, then this intersection also belongs to the collection of all such rectangles, thus making this collection a π-system.
More concisely: Given π-systems C and D of subsets of types α and β respectively, the set of all Cartesian products of elements from C and D is also a π-system.
|
MeasureTheory.Measure.ae_ae_of_ae_prod
theorem MeasureTheory.Measure.ae_ae_of_ae_prod :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] {p : α × β → Prop},
(∀ᵐ (z : α × β) ∂μ.prod ν, p z) → ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p (x, y)
The theorem `MeasureTheory.Measure.ae_ae_of_ae_prod` asserts that for any two measurable spaces `α` and `β`, and two measures `μ` and `ν` where `ν` is s-finite, if a property `p` holds almost everywhere on the product space `α × β` with respect to the product measure, then it follows that for almost every `x` in `α` with respect to `μ` and for almost every `y` in `β` with respect to `ν`, the property `p` holds on the pair `(x, y)`. Note that the converse of this statement is not generally true.
More concisely: Given measurable spaces `α` and `β`, measures `μ` on `α` and `ν` on `β` (WITH `ν` s-finite), if a property `p` holds almost everywhere on `α × β` with respect to the product measure, then `p` holds almost everywhere on `α × β` with respect to `μ` and almost everywhere on `β` with respect to `ν`.
|
MeasureTheory.lintegral_prod
theorem MeasureTheory.lintegral_prod :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
(f : α × β → ENNReal),
AEMeasurable f (μ.prod ν) → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
**Tonelli's Theorem**: For all non-negative extended real-valued functions `f` that are almost everywhere measurable on the product space `α × β`, the theorem asserts that the integral of `f` with respect to the product measure of measures `μ` and `ν` equals the iterated integral of `f` with respect to `ν` and `μ`. This holds under the assumption that the measure `ν` is sigma-finite. In other words, if `f` is an almost everywhere measurable function from `α × β` to non-negative extended reals (`[0, ∞]`), then the integral of `f` over the product space is equal to the iterated integral of `f` over the individual spaces.
More concisely: For a non-negative, almost everywhere measurable function `f` on the product space `α × β` with sigma-finite measure `ν`, the integral of `f` with respect to the product measure of `μ` and `ν` equals the iterated integral with respect to `ν` and `μ`.
|
MeasureTheory.lintegral_prod_symm'
theorem MeasureTheory.lintegral_prod_symm' :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ] (f : α × β → ENNReal),
Measurable f → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
The theorem `MeasureTheory.lintegral_prod_symm'` is a symmetric version of Tonelli's Theorem for measurable spaces. It states that given a measurable space `α` and `β`, measures `μ` and `ν` on these spaces respectively, and a measurable function `f` from the product of `α` and `β` to the extended nonnegative real numbers, the integral of `f` with respect to the product measure is equal to the iterated integral, computed in reverse order. In other words, the integral of `f` over `α × β` is the same as first integrating over `α` and then over `β`. This theorem is under the assumption that both the measures `μ` and `ν` are sigma-finite.
More concisely: Given measurable spaces `α` and `β`, measures `μ` on `α` and `ν` on `β`, and a measurable function `f` from `α × β` to the extended nonnegative real numbers, the symmetric Tonelli's Theorem states that the integral of `f` with respect to the product measure is equal to the iterated integral, where the integration over `β` is performed first and then over `α`. Under the assumption that both `μ` and `ν` are sigma-finite.
|
Measurable.lintegral_prod_left
theorem Measurable.lintegral_prod_left :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SFinite μ] {f : α → β → ENNReal},
Measurable (Function.uncurry f) → Measurable fun y => ∫⁻ (x : α), f x y ∂μ
This theorem, `Measurable.lintegral_prod_left`, states that the Lebesgue integral is a measurable function. Specifically, given any two measurable spaces `α` and `β`, a measure `μ` on `α` that is sigma-finite, and a function `f` from `α` to `β` to the extended nonnegative real numbers (which includes positive infinity), if the uncurried version of `f` (a function from pairs of type `α` and `β` to the extended nonnegative real numbers) is measurable, then the function mapping each element `y` of `β` to the Lebesgue integral of the function `x ↦ f x y` with respect to `μ` is also measurable. This is an important result in measure theory and it forms part of the symmetric version of Tonelli's theorem.
More concisely: Given measurable spaces `α` and `β`, a sigma-finite measure `μ` on `α`, and a measurable function `f : α → β → ℝ∞`, the function mapping each `y` in `β` to the Lebesgue integral of `x ↦ f x y` with respect to `μ` is measurable.
|
MeasureTheory.Measure.prod_prod
theorem MeasureTheory.Measure.prod_prod :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν] (s : Set α)
(t : Set β), ↑↑(μ.prod ν) (s ×ˢ t) = ↑↑μ s * ↑↑ν t
This theorem states that, for any two given types `α` and `β` with associated measurable spaces, and given measures `μ` and `ν` where ν is s-finite, the product measure of the product of two sets, `s` from type `α` and `t` from type `β`, is equal to the product of their individual measures. This holds even if the sets `s` and `t` are not measurable. In mathematical terms, for any sets `s` and `t`, we have: `(MeasureTheory.Measure.prod μ ν) (s × t) = μ s * ν t`.
More concisely: For any s-finite measures μ and ν on measurable spaces (α, Σα) and (β, Σβ), respectively, the product measure of μ and ν on the product measurable space (α × β, Σα × Σβ) equals the product of their individual measures: (μ × ν).(s × t) = μ(s) * ν(t), for any sets s ∈ Σα and t ∈ Σβ.
|
MeasureTheory.lintegral_lintegral_swap
theorem MeasureTheory.lintegral_lintegral_swap :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ] ⦃f : α → β → ENNReal⦄,
AEMeasurable (Function.uncurry f) (μ.prod ν) →
∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (y : β), ∫⁻ (x : α), f x y ∂μ ∂ν
This theorem, `MeasureTheory.lintegral_lintegral_swap`, verifies the property that the order of integration can be interchanged in the context of Lebesgue integration. More specifically, if you have a function `f` mapping from a pair of variables `(α, β)` to the extended nonnegative real numbers, and this function is almost everywhere measurable with respect to the product of two measures `μ` and `ν`, then the double Lebesgue integral of `f` with respect to `ν` and then `μ` is equal to the double Lebesgue integral of `f` with respect to `μ` and then `ν`. This order swapping is valid under the conditions that both `μ` and `ν` are sigma-finite measures.
More concisely: If `f` is an almost everywhere measurable function from the product of two measurable spaces with respect to sigma-finite measures `μ` and `ν`, then the order of integrating `f` with respect to `μ` and `ν` can be interchanged: ∫∫\_Δ\_(α, β) f(α, β) dμ dν = ∫∫\_Δ\_(α, β) f(α, β) dν dμ.
|
MeasureTheory.lintegral_prod_symm
theorem MeasureTheory.lintegral_prod_symm :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : MeasureTheory.SFinite ν]
[inst_3 : MeasureTheory.SFinite μ] (f : α × β → ENNReal),
AEMeasurable f (μ.prod ν) → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
The theorem `MeasureTheory.lintegral_prod_symm` is a symmetric version of Tonelli's Theorem. It states that for functions `f` mapping from a product of two types `α` and `β` to the extended nonnegative real numbers (`ℝ≥0∞`), which are almost everywhere measurable with respect to the product of measures `μ` and `ν`, the integral of `f` with respect to the product measure is equal to the iterated integral, but with the order of integration reversed. In other words, integrating first over `α` and then over `β` is the same as integrating over the product space `α × β`. This statement requires both the measures `μ` and `ν` to be sigma-finite.
More concisely: For measurable functions `f` from the product space `α × β` to the extended nonnegative real numbers with respect to the sigma-finite product measures `μ` and `ν`, the integral of `f` with respect to `μ` over `α` and then `ν` over `β` equals the integral of `f` with respect to the reversed order of measures.
|
IsCountablySpanning.prod
theorem IsCountablySpanning.prod :
∀ {α : Type u_1} {β : Type u_3} {C : Set (Set α)} {D : Set (Set β)},
IsCountablySpanning C → IsCountablySpanning D → IsCountablySpanning (Set.image2 (fun x x_1 => x ×ˢ x_1) C D)
The theorem `IsCountablySpanning.prod` states that if you have two collections of sets, `C` and `D`, each spanning their respective types `α` and `β` countably, then the image of the Cartesian product (x ×ˢ x_1) of these sets also spans countably. In other words, if `C` and `D` are countably spanning sets, then the set of all pairs `(x, x_1)`, where `x` is in some set of `C` and `x_1` is in some set of `D`, is also a countably spanning set.
More concisely: If sets `C` and `D` countably span types `α` and `β` respectively, then their Cartesian product `C × D` countably spans the type `α × β`.
|
generateFrom_eq_prod
theorem generateFrom_eq_prod :
∀ {α : Type u_1} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {C : Set (Set α)}
{D : Set (Set β)},
MeasurableSpace.generateFrom C = inst →
MeasurableSpace.generateFrom D = inst_1 →
IsCountablySpanning C →
IsCountablySpanning D →
MeasurableSpace.generateFrom (Set.image2 (fun x x_1 => x ×ˢ x_1) C D) = Prod.instMeasurableSpace
The theorem `generateFrom_eq_prod` states that if sets `C` and `D` generate the σ-algebras on types `α` and `β` respectively, and if they are countably spanning (i.e., their countable subsets span the whole respective types), then the smallest σ-algebra on the product type `α × β`, generated by the set of all Cartesian products formed by `C` and `D`, is equal to the product σ-algebra on `α × β`. In simpler words, given any two measurable spaces, the σ-algebra generated by the Cartesian product of any countably spanning sets that generates the two spaces, is equal to the σ-algebra on the product space.
More concisely: If sets C and D generate the sigma-algebras on types α and β respectively and are countably spanning, then the sigma-algebra generated by the Cartesian products of C and D equals the product sigma-algebra on α × β.
|