AEMeasurable.prod_mk
theorem AEMeasurable.prod_mk :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
[inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {f : α → β} {g : α → γ},
AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun x => (f x, g x)) μ
The theorem `AEMeasurable.prod_mk` states that for any types `α`, `β`, and `γ`; given a measurable space over `α`, a measurable space over `β`, a measurable space over `γ`, a measure `μ` over the type `α`, and functions `f` and `g` that map from `α` to `β` and `γ` respectively; if `f` and `g` are both almost everywhere measurable (AEMeasurable), then the function that maps `x` in `α` to the pair `(f x, g x)` is also almost everywhere measurable. In other words, we can create an almost everywhere measurable function over pairs of the range values, if the original functions are almost everywhere measurable.
More concisely: If `f` and `g` are almost everywhere measurable functions from a measurable space `(α, Σα, μ)` to measurable spaces `(β, Σβ)` and `(γ, Σγ)` respectively, then the function `x ↦ (f x, g x)` is almost everywhere measurable from `(α, Σα)` to the product measurable space `(β × γ, Σβ × Σγ)`.
|
MeasureTheory.Measure.map_sum
theorem MeasureTheory.Measure.map_sum :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {ι : Type u_7}
{m : ι → MeasureTheory.Measure α} {f : α → β},
AEMeasurable f (MeasureTheory.Measure.sum m) →
MeasureTheory.Measure.map f (MeasureTheory.Measure.sum m) =
MeasureTheory.Measure.sum fun i => MeasureTheory.Measure.map f (m i)
The theorem `MeasureTheory.Measure.map_sum` states that for any types `α`, `β`, and `ι`, along with a measurable space `m0` on `α`, a measurable space instance on `β`, a function `m` from `ι` to measures on `α`, and a function `f` from `α` to `β`: If the function `f` is almost everywhere measurable with respect to the sum of the measures given by `m`, then the pushforward of the sum of the measures by the function `f` is equal to the sum of the pushforwards of the individual measures by `f`. In other words, when a function is almost everywhere measurable, mapping the function across the sum of measures is the same as summing the measures obtained by mapping the function across each individual measure.
More concisely: If `m:` ι → MeasurableSpace α, `f:` α → β is almost everywhere measurable, then `∫(∑ i: ι, m i)(f) = ∑ i: ι, ∫m i(f)`.
|
AEMeasurable.restrict
theorem AEMeasurable.restrict :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
{μ : MeasureTheory.Measure α}, AEMeasurable f μ → ∀ {s : Set α}, AEMeasurable f (μ.restrict s)
This theorem states that, for any given types `α` and `β`, with `α` being a measurable space, and any function `f : α → β`, if `f` is almost everywhere measurable with respect to a measure `μ` on `α`, then `f` is also almost everywhere measurable with respect to the restriction of `μ` to any subset `s` of `α`. In other words, if a function almost everywhere equals a measurable function with respect to a certain measure, it will still almost everywhere equal a measurable function when that measure is restricted to a subset.
More concisely: If `f : α → β` is almost everywhere measurable with respect to measure `μ` on `α`, then `f` is almost everywhere measurable with respect to the restriction of `μ` to any subset `s` of `α`.
|
AEMeasurable.comp_quasiMeasurePreserving
theorem AEMeasurable.comp_quasiMeasurePreserving :
∀ {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
[inst_1 : MeasurableSpace δ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure δ} {f : α → δ} {g : δ → β},
AEMeasurable g ν → MeasureTheory.Measure.QuasiMeasurePreserving f μ ν → AEMeasurable (g ∘ f) μ
This theorem states that if a function `g` is "almost everywhere measurable" with respect to a measure `ν`, and if a function `f` is "quasi measure preserving" from measure `μ` to measure `ν`, then the composition function `g ∘ f` is "almost everywhere measurable" with respect to measure `μ`.
In mathematical terms, a function is "almost everywhere measurable" if it is almost everywhere equal to a measurable function. A function is "quasi measure preserving" if the preimage of every measurable set under this function is measurable and the measure of the preimage set is equal to the measure of the original set.
More concisely: If `g` is almost everywhere equal to a measurable function and `f` is a quasi measure preserving function between measures `μ` and `ν`, then the composition `g ∘ f` is almost everywhere measurable with respect to measure `μ`.
|
MeasureTheory.NullMeasurable.aemeasurable_of_aerange
theorem MeasureTheory.NullMeasurable.aemeasurable_of_aerange :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
{f : α → β} {t : Set β} [inst_1 : MeasurableSpace.CountablyGenerated ↑t],
MeasureTheory.NullMeasurable f μ → (∀ᵐ (x : α) ∂μ, f x ∈ t) → AEMeasurable f μ
This theorem states that for any null measurable function `f` from a measurable space `α` to another measurable space `β`, if almost every value of `f` belongs to a set `t` in `β` such that the restriction of the `σ`-algebra in the codomain to `t` is countably generated, then `f` is almost everywhere measurable. In other words, if `f` maps almost all of its inputs into a specific countable subset of the codomain, and `f` is null measurable, then `f` is almost everywhere measurable. This theorem bridges the concepts of null measurability and almost everywhere measurability under certain conditions.
More concisely: If a null measurable function from a measurable space to a codomain with a countably generated sub-σ-algebra mapping almost all of its inputs to this sub-σ-algebra's elements is almost everywhere defined, then it is almost everywhere measurable.
|
AEMeasurable.map_map_of_aemeasurable
theorem AEMeasurable.map_map_of_aemeasurable :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
[inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {g : β → γ} {f : α → β},
AEMeasurable g (MeasureTheory.Measure.map f μ) →
AEMeasurable f μ →
MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ
This theorem, `AEMeasurable.map_map_of_aemeasurable`, states that for all types `α`, `β`, and `γ`, with `α`, `β`, and `γ` representing sets, and given measurable spaces on these sets (`m0` on `α`, `inst` on `β`, and `inst_1` on `γ`), a measure `μ` on `α`, and functions `g : β → γ` and `f : α → β`, if `g` is almost everywhere measurable with respect to the measure obtained by mapping `f` to the measure `μ`, and `f` is almost everywhere measurable with respect to the measure `μ`, then the measure obtained by first mapping `f` to the measure `μ` and then mapping `g` to the result, is equal to the measure obtained by mapping the composition of `g` and `f` to the measure `μ`. In other words, it asserts that for almost everywhere measurable functions, the operation of measure pushforward commutes with function composition.
More concisely: Given measurable spaces `(α, m0)`, `(β, inst)`, `(γ, inst_1)` and measures `μ` on `α`, if `f : α → β` and `g : β → γ` are almost everywhere measurable with respect to `μ` and the measures induced by `f` and `g`, then `(μ ∘ f) ∘ g = μ ∘ (g ∘ f)` almost everywhere.
|
AEMeasurable.mono_measure
theorem AEMeasurable.mono_measure :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
{μ ν : MeasureTheory.Measure α}, AEMeasurable f μ → ν ≤ μ → AEMeasurable f ν
The theorem `AEMeasurable.mono_measure` states that for any types `α` and `β`, where `α` has a measurable space structure `m0` and `β` has a measurable space structure `inst`, any function `f` from `α` to `β`, and any two measures `μ` and `ν` on the measurable space `α`, if the function `f` is almost everywhere measurable with respect to the measure `μ` and the measure `ν` is less than or equal to the measure `μ` (i.e., `ν` is a sub-measure of `μ`), then the function `f` is also almost everywhere measurable with respect to the measure `ν`. In other words, almost everywhere measurability of a function is preserved under taking sub-measures.
More concisely: If a function between measurable spaces is almost everywhere measurable with respect to a measure and is sub-measurable (i.e., the smaller measure is less than or equal to the larger one), then the function is almost everywhere measurable with respect to the smaller measure.
|
Mathlib.MeasureTheory.Measure.AEMeasurable._auxLemma.1
theorem Mathlib.MeasureTheory.Measure.AEMeasurable._auxLemma.1 :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
{μ : MeasureTheory.Measure α} [inst_1 : Subsingleton α], AEMeasurable f μ = True
This theorem states that for any types `α` and `β`, with `α` being a subsingleton (i.e., it has at most one element), any measurable spaces `m0` and `inst` over `α` and `β` respectively, any function `f` from `α` to `β`, and any measure `μ` on the measurable space `α`, the function `f` is almost everywhere measurable with respect to measure `μ`. In other words, the function `f` coincides almost everywhere with a measurable function, which is trivially true when the domain `α` has at most one element.
More concisely: For any subsingleton type `α`, any measurable spaces `m0` over `α` and `inst` over `β`, any function `f` from `α` to `β`, and any measure `μ` on `α`, the function `f` is almost everywhere equal to a measurable function.
|
AEMeasurable.comp_measurable
theorem AEMeasurable.comp_measurable :
∀ {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
[inst_1 : MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : α → δ} {g : δ → β},
AEMeasurable g (MeasureTheory.Measure.map f μ) → Measurable f → AEMeasurable (g ∘ f) μ
The theorem `AEMeasurable.comp_measurable` states that, given three types `α`, `β`, and `δ` with associated measurable spaces, a measure `μ` on `α`, a function `f` from `α` to `δ`, and a function `g` from `δ` to `β`, if `g` is almost everywhere measurable with respect to the measure `μ` transformed by `f`, and if `f` itself is measurable, then the composition of `g` and `f` (denoted as `g ∘ f`) is also almost everywhere measurable with respect to the measure `μ`.
In other words, the measurability of the composition of two functions is preserved when one of the functions is measurable and the other is almost everywhere measurable.
More concisely: If a function `g` is almost everywhere measurable with respect to the measure `μ` transformed by a measurable function `f`, then the composition `g ∘ f` is almost everywhere measurable with respect to `μ`.
|
MeasurableEmbedding.aemeasurable_map_iff
theorem MeasurableEmbedding.aemeasurable_map_iff :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
[inst_1 : MeasurableSpace γ] {f : α → β} {μ : MeasureTheory.Measure α} {g : β → γ},
MeasurableEmbedding f → (AEMeasurable g (MeasureTheory.Measure.map f μ) ↔ AEMeasurable (g ∘ f) μ)
This theorem states that for any three types `α`, `β` and `γ` that have corresponding measurable spaces `m0`, `inst` and `inst_1`, and functions `f : α → β` and `g : β → γ`, and a measure `μ` on `α`, then if `f` is a measurable embedding, it follows that `g` is almost everywhere measurable with respect to the push-forward measure `f` applied to `μ` if and only if the composition `g ∘ f` is almost everywhere measurable with respect to `μ`. Here, a function is defined to be almost everywhere measurable if it is equal almost everywhere to a measurable function, while a measurable embedding is a function that is both injective and measurable, and the push-forward of a measure via a function `f` is a new measure on the target space of `f`.
More concisely: A measurable embedding `f : α → β` makes `g : β → γ` almost everywhere measurable with respect to the pushforward measure if and only if the composition `g ∘ f` is almost everywhere measurable with respect to the original measure.
|
aemeasurable_id''
theorem aemeasurable_id'' :
∀ {α : Type u_2} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {m : MeasurableSpace α},
m ≤ m0 → AEMeasurable id μ
The theorem `aemeasurable_id''` states that for any type α and for any two measurable spaces `m` and `m0` on α, if `m` is a subspace of `m0`, then the identity function is almost everywhere measurable with respect to a measure `μ`. In other words, the identity function coincides almost everywhere with a measurable function under the given measure.
More concisely: If α is a type, `m` is a measurable space on α, and `m0` is a larger measurable space on α, such that `m` is a subspace of `m0`, then the identity function on α is almost everywhere measurable with respect to any measure μ on `m0`.
|
AEMeasurable.indicator
theorem AEMeasurable.indicator :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
{μ : MeasureTheory.Measure α} [inst_1 : Zero β],
AEMeasurable f μ → ∀ {s : Set α}, MeasurableSet s → AEMeasurable (s.indicator f) μ
The `AEMeasurable.indicator` theorem states that for any types `α` and `β`, given a measure space `m0` on `α` and a `MeasurableSpace β`, a function `f` from `α` to `β`, a measure `μ` on `α`, and an instance of `Zero β`, if the function `f` is almost everywhere measurable with respect to the measure `μ`, then for any set `s` of `α` that is a measurable set, the function resulting from the application of the set indicator function to `s` and `f` is also almost everywhere measurable with respect to the measure `μ`. In other words, if a function is almost everywhere measurable, then the indicator function on any measurable set of the function's domain is also almost everywhere measurable.
More concisely: Given a measure space, a measurable function, and a measurable set, the indicator function of the set applied to the function is almost everywhere measurable if the function is.
|
AEMeasurable.comp_aemeasurable
theorem AEMeasurable.comp_aemeasurable :
∀ {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
[inst_1 : MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : α → δ} {g : δ → β},
AEMeasurable g (MeasureTheory.Measure.map f μ) → AEMeasurable f μ → AEMeasurable (g ∘ f) μ
The theorem `AEMeasurable.comp_aemeasurable` states that for any three types `α`, `β`, and `δ` and any two functions `f : α → δ` and `g : δ → β`, if `g` is almost everywhere measurable with respect to the measure induced on `δ` by `f` and the measure `μ` on `α`, and if `f` is also almost everywhere measurable with respect to `μ`, then the composition of `g` and `f` (i.e., `g ∘ f`) is also almost everywhere measurable with respect to `μ`. This theorem formalizes in Lean 4 one of the properties of almost everywhere measurable functions in measure theory.
More concisely: If `f : α → δ` and `g : δ → β` are almost everywhere measurable functions with respect to the same measure `μ`, then their composition `g ∘ f` is also almost everywhere measurable.
|
aemeasurable_indicator_const_iff
theorem aemeasurable_indicator_const_iff :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
[inst_1 : Zero β] {s : Set α} [inst_2 : MeasurableSingletonClass β] (b : β) [inst_3 : NeZero b],
AEMeasurable (s.indicator fun x => b) μ ↔ MeasureTheory.NullMeasurableSet s μ
The theorem `aemeasurable_indicator_const_iff` provides a characterization of the almost-everywhere measurability of an indicator function that takes a constant value `b` on a set `A` and `0` elsewhere. Specifically, it states that for any types `α` and `β`, any `MeasurableSpace` structures on `α` and `β`, any measure `μ` on `α`, any zero element of type `β`, any set `s` of type `α`, any singleton measurable class for `β`, and any non-zero element `b` of type `β`, this indicator function is almost everywhere measurable with respect to measure `μ` if and only if the set `s` is a null-measurable set with respect to measure `μ`. In simpler terms, the function is almost everywhere measurable if the set can be approximated by a measurable set up to a set of null measure.
More concisely: The indicator function of a null-measurable set with respect to a measure is almost everywhere measurable if and only if it takes a constant value.
|
AEMeasurable.sum_measure
theorem AEMeasurable.sum_measure :
∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
[inst_1 : Countable ι] {μ : ι → MeasureTheory.Measure α},
(∀ (i : ι), AEMeasurable f (μ i)) → AEMeasurable f (MeasureTheory.Measure.sum μ)
This theorem, `AEMeasurable.sum_measure`, states that for any types `ι`, `α`, and `β`, given a measurable space on `α`, a measurable space on `β`, a function `f` from `α` to `β`, a countable index set `ι`, and a family of measures `μ` indexed by `ι`, if the function `f` is "almost everywhere measurable" with respect to each measure `μ i` for every index `i`, then `f` is also "almost everywhere measurable" with respect to the sum of the measures `μ`.
In other terms, "almost everywhere measurable" means that the function `f` coincides almost everywhere with a measurable function. The term "almost everywhere" is defined with respect to a measure, and means "everywhere except on a set of measure zero". The theorem therefore asserts that the property of being "almost everywhere measurable" is preserved under taking the sum of measures.
More concisely: Given measurable spaces on types `α` and `β`, a measurable function `f` from `α` to `β`, a countable index set `ι`, and a family of measures `μ i` on `α` indexed by `ι`, if `f` is almost everywhere measurable with respect to each `μ i`, then `f` is almost everywhere measurable with respect to the sum of the `μ i`.
|
AEMeasurable.mono'
theorem AEMeasurable.mono' :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
{μ ν : MeasureTheory.Measure α}, AEMeasurable f μ → ν.AbsolutelyContinuous μ → AEMeasurable f ν
The theorem `AEMeasurable.mono'` states that for all types `α` and `β`, given a measurable space `α` and a measure space `β`, for a function `f` from `α` to `β`, and for any two measures `μ` and `ν` on `α`, if `f` is almost everywhere measurable with respect to `μ`, and `ν` is absolutely continuous with respect to `μ`, then `f` is also almost everywhere measurable with respect to `ν`. Here, a function is almost everywhere measurable if it agrees almost everywhere with a measurable function, and a measure `ν` is absolutely continuous with respect to another measure `μ` if whenever a set has `μ` measure zero, it also has `ν` measure zero.
More concisely: If a function between measurable spaces is almost everywhere measurable with respect to one measure and absolutely continuous with respect to another measure, then it is almost everywhere measurable with respect to the second measure.
|
MeasureTheory.NullMeasurable.aemeasurable
theorem MeasureTheory.NullMeasurable.aemeasurable :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
{f : α → β} [hc : MeasurableSpace.CountablyGenerated β], MeasureTheory.NullMeasurable f μ → AEMeasurable f μ
The theorem states that if we have a null measurable function whose codomain's sigma-algebra is countably generated, then this function is also almost everywhere measurable. In other words, for a function `f` mapping from type `α` to `β`, if the function `f` is null measurable and if the measurable space of `β` is countably generated, then `f` coincides almost everywhere with a measurable function. This essentially asserts a relationship between the null measurability and almost everywhere measurability of a function under certain conditions.
More concisely: If a null measurable function from a measurable space `(α, Σα)` to a countably generated measurable space `(β, Σβ)` has a measurable equivalence class, then the function is almost everywhere measurable.
|