MeasureTheory.Measure.measurable_lintegral
theorem MeasureTheory.Measure.measurable_lintegral :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ENNReal},
Measurable f → Measurable fun μ => ∫⁻ (x : α), f x ∂μ
The theorem `MeasureTheory.Measure.measurable_lintegral` states that for every type `α` that is a measurable space and a function `f` from `α` to the extended nonnegative real numbers (denoted as `[0, ∞]`), if the function `f` is measurable, then the function that maps a measure `μ` to the integral (specifically, Lebesgue integral) of `f` with respect to `μ` over the space `α` is also measurable. In simpler words, this theorem ensures that the operation of taking the Lebesgue integral of a measurable function is itself a measurable process.
More concisely: If `α` is a measurable space and `f` is a measurable function from `α` to `[0, ∞]`, then the function that maps a measure `μ` to the Lebesgue integral of `f` with respect to `μ` is measurable.
|
MeasureTheory.Measure.measurable_join
theorem MeasureTheory.Measure.measurable_join :
∀ {α : Type u_1} [inst : MeasurableSpace α], Measurable MeasureTheory.Measure.join
This theorem states that for any type `α` that has a `MeasurableSpace` instance, the monadic join operation on `Measure` in the category of measurable spaces and measurable functions, `MeasureTheory.Measure.join`, is a measurable function. In mathematical terms, the preimage of every measurable set under `MeasureTheory.Measure.join` is also a measurable set.
More concisely: For any measurable spaces `(X, Σ\_X)` and `(Y, Σ\_Y)` and measurable functions `f : X → Y` and `g : X' → X`, the compositions `g ^-1 ∘ MeasureTheory.Measure.join (f, g) ∘ Measure.universe` and `MeasureTheory.Measure.join (f, g) ∘ Measure.universe ∘ g ^-1` are measurable functions between measurable sets. (Here, `Measure.universe` is the lift of a set to a measurable set in the given measurable space.)
|
MeasureTheory.Measure.join_apply
theorem MeasureTheory.Measure.join_apply :
∀ {α : Type u_1} [inst : MeasurableSpace α] {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {s : Set α},
MeasurableSet s → ↑↑m.join s = ∫⁻ (μ : MeasureTheory.Measure α), ↑↑μ s ∂m
The theorem `MeasureTheory.Measure.join_apply` states that for any measurable space `α`, any measure `m` on the space of measures on `α`, and any set `s` of `α`, if `s` is a measurable set, then the measure of `s` under the joined measure `m` is equal to the integral over all measures `μ` in `α` of the measure of `s` under `μ`, with respect to `m`. This essentially provides the rule for computing the measure of a set under a joined measure in terms of the measures it joins.
More concisely: For any measurable space `α`, measurable set `s` in `α`, measure `m` on the space of measures over `α`, and measurable measure `μ` on `α`, the integral of the measure of `s` under `μ with respect to `m` equals the measure of `s` under the joined measure `m ⊕ μ`.
|
MeasureTheory.Measure.measurable_coe
theorem MeasureTheory.Measure.measurable_coe :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, MeasurableSet s → Measurable fun μ => ↑↑μ s
This theorem, `MeasureTheory.Measure.measurable_coe`, states that for any given measurable space `α`, and any given set `s` in this space such that `s` is a measurable set, the function which maps each measure `μ` to the measure of the set `s` is a measurable function. In other words, the preimage of every measurable set under this function is also a measurable set. This is a characteristic property of measurable functions in the field of measure theory.
More concisely: The function that maps a measure to the measure of a measurable set is a measurable function.
|
MeasureTheory.Measure.measurable_dirac
theorem MeasureTheory.Measure.measurable_dirac :
∀ {α : Type u_1} [inst : MeasurableSpace α], Measurable MeasureTheory.Measure.dirac
The theorem `MeasureTheory.Measure.measurable_dirac` states that for any type `α` equipped with a measurable space structure, the Dirac measure function is measurable. In mathematical terms, this means that for any set `α` where we can define what it means for a subset to be measurable, the function that assigns to each point in `α` the Dirac measure at that point, is itself a measurable function. This means that the preimage of any measurable set under the Dirac measure function is also a measurable set.
More concisely: The Dirac measure function, which maps each point in a measurable space to the Dirac measure at that point, is a measurable function.
|
MeasureTheory.Measure.measurable_map
theorem MeasureTheory.Measure.measurable_map :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (f : α → β),
Measurable f → Measurable fun μ => MeasureTheory.Measure.map f μ
The theorem `MeasureTheory.Measure.measurable_map` states that for any two types `α` and `β` that each have a measurable space structure, and for any function `f` from `α` to `β`, if `f` is a measurable function then the function which maps each measure on `α` to its pushforward measure on `β` via `f` is also measurable. This means that for every measurable set in the target space of measures, the preimage of this set under the measure pushforward function is also measurable.
More concisely: If `f: α → β` is a measurable function between measurable spaces `(α, Σα)` and `(β, Σβ)`, then the function that maps each measure `μ ∈ Σα` to its pushforward `f_#(μ) ∈ Σβ` is also a measurable function from `(Σα, ℬ(Σα))` to `(Σβ, ℬ(Σβ))`.
|
MeasureTheory.Measure.measurable_measure
theorem MeasureTheory.Measure.measurable_measure :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{μ : α → MeasureTheory.Measure β},
Measurable μ ↔ ∀ (s : Set β), MeasurableSet s → Measurable fun b => ↑↑(μ b) s
This theorem, `MeasureTheory.Measure.measurable_measure`, states that for any two types `α` and `β` equipped with measurable spaces, and a function `μ` from `α` to `MeasureTheory.Measure` of `β`, `μ` is measurable if and only if for every set `s` of type `β` that is a measurable set, the function that maps each element `b` to the measure of `s` under `μ b` is also measurable. Here, "measurable" means that the preimage of any measurable set under the function is also a measurable set.
More concisely: A function `μ:` `α` `→` `MeasureTheory.Measure` `β` is measurable if and only if for every measurable set `s` in `β`, the function that maps each `b` in `α` to the measure of `s` under `μ b` is also measurable.
|
MeasureTheory.Measure.bind_apply
theorem MeasureTheory.Measure.bind_apply :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
{m : MeasureTheory.Measure α} {f : α → MeasureTheory.Measure β} {s : Set β},
MeasurableSet s → Measurable f → ↑↑(m.bind f) s = ∫⁻ (a : α), ↑↑(f a) s ∂m
The theorem `MeasureTheory.Measure.bind_apply` states that for any types `α` and `β` that are equipped with measurable spaces, given a measure `m` on `α`, a function `f` from `α` to the set of measures on `β`, and a set `s` in `β`, if `s` is a measurable set and `f` is a measurable function, then the measure of `s` under the measure obtained by binding `m` and `f` is equal to the integral over `α` of the function that sends `a` in `α` to the measure of `s` under the measure `f(a)`, with respect to the measure `m`. In other words, it shows how the `bind` operation on measures interacts with the application of a measure to a set, in terms of an integral of measures.
More concisely: For measurable spaces (α, m) and (β, ν), measurable function f : α → ν, and measurable set s ∈ β, the integral of the function mapping a ∈ α to ν(s under f(a)) with respect to m equals the measure of s under the measure obtained by binding m and f.
|
MeasureTheory.Measure.measurable_of_measurable_coe
theorem MeasureTheory.Measure.measurable_of_measurable_coe :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
(f : β → MeasureTheory.Measure α),
(∀ (s : Set α), MeasurableSet s → Measurable fun b => ↑↑(f b) s) → Measurable f
The theorem `MeasureTheory.Measure.measurable_of_measurable_coe` states that for any two types `α` and `β` each equipped with a measurable space structure, if we have a function `f` from `β` to the space of measures on `α`, then `f` is a measurable function if the function that maps each element `b` of `β` to the measure of a set `s` under the measure `f b` is measurable for every measurable set `s`. In other words, `f` is measurable if for every measurable set `s`, the function that maps `b` to the measure of `s` in the measure space defined by `f(b)` is a measurable function.
More concisely: A function `f` from a measurable space `(β, Σβ)` to the space of measures on another measurable space `(α, Σα)` is measurable if the function that maps each `b ∈ β` to the measure of a given measurable set `s ∈ Σα` under the measure `f(b)` is itself measurable.
|