Measurable.add_const
theorem Measurable.add_const :
∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f : α → M}
[inst_2 : MeasurableAdd M], Measurable f → ∀ (c : M), Measurable fun x => f x + c
This theorem states that if `f` is a measurable function from a measurable space `α` to another measurable space `M` that has a defined addition operation, then for any constant `c` from `M`, the function which maps each element `x` in `α` to the sum of `f(x)` and `c` is also measurable. In other words, adding a constant to the values of a measurable function from a space with a defined addition operation does not prevent the resultant function from being measurable.
More concisely: If `f` is a measurable function from a measurable space `α` to an Abelian group `M`, then the function `x ↦ f(x) + c` is measurable for any constant `c` in `M`.
|
Finset.measurable_sum
theorem Finset.measurable_sum :
∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M]
[inst_2 : MeasurableAdd₂ M] {m : MeasurableSpace α} {f : ι → α → M} (s : Finset ι),
(∀ i ∈ s, Measurable (f i)) → Measurable fun a => s.sum fun i => f i a
The theorem `Finset.measurable_sum` establishes that if we have a measurable space `M` with an additive commutative monoid structure and a binary function that is measurable, alongside another measurable space α, then for any finite set `s` of some type `ι` and a function `f` that maps each element of `s` to a measurable function from `α` to `M`, if each of these measurable functions `f i` for `i` in `s` is measurable, then the function that maps each element `a` in `α` to the sum of `f i a` as `i` ranges over `s` is also measurable. In simple terms, the sum of measurable functions over a finite set is measurable.
More concisely: If `M` is a measurable space with an additive commutative monoid structure, and `f : ι → α → M` is a function where `ι` is finite and each `f i` is measurable, then the function `g : α → M` defined by `g a := ∑ i in ι, f i a` is measurable.
|
AEMeasurable.div_const
theorem AEMeasurable.div_const :
∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f : α → G}
{μ : MeasureTheory.Measure α} [inst_2 : MeasurableDiv G],
AEMeasurable f μ → ∀ (c : G), AEMeasurable (fun x => f x / c) μ
The theorem `AEMeasurable.div_const` states that for any type `G` with a `MeasurableSpace` and a `Div` instance, any measurable space `α`, any function `f` from `α` to `G`, and any measure `μ` on `α`, if `f` is almost everywhere measurable with respect to `μ`, then for any constant `c` in `G`, the function `fun x => f x / c` (which maps each `x` in `α` to `f(x)/c` in `G`) is almost everywhere measurable with respect to `μ` as well. This theorem essentially says that dividing an almost everywhere measurable function by a constant results in another function that is still almost everywhere measurable.
More concisely: If `f` is almost everywhere measurable with respect to measure `μ` on measurable space `α` and `G` is a type with a `Div` instance, then the function `x ↦ f x / c` is almost everywhere measurable for any constant `c` in `G`.
|
AEMeasurable.pow_const
theorem AEMeasurable.pow_const :
∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
[inst_2 : Pow β γ] [inst_3 : MeasurablePow β γ] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β},
AEMeasurable f μ → ∀ (c : γ), AEMeasurable (fun x => f x ^ c) μ
The theorem `AEMeasurable.pow_const` states that for all types `β`, `γ`, and `α`, such that `β` and `γ` are measurable spaces, `β` has a power operation to `γ`, and this power function is measurable, for any measurable space `m` on `α`, any measure `μ` on `α`, and any function `f` from `α` to `β` which is almost everywhere measurable, for every constant `c` of type `γ`, the function that maps each `x` in `α` to the `c`-th power of `f(x)` is also almost everywhere measurable. In other words, if a function is almost everywhere measurable, then so is its power function for any constant exponent.
More concisely: For measurable spaces `β`, `γ`, and type `α`, if `β` has a measurable power operation to `γ`, `f: α → β` is almost everywhere measurable, and `c` is a constant of type `γ`, then the function `x => c ^ (f x)` is almost everywhere measurable.
|
Measurable.inv
theorem Measurable.inv :
∀ {G : Type u_2} {α : Type u_3} [inst : Inv G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableInv G]
{m : MeasurableSpace α} {f : α → G}, Measurable f → Measurable fun x => (f x)⁻¹
The theorem `Measurable.inv` states that for any type `G` with an `Inv` (inverse) operation and a `MeasurableSpace` structure and any type `α` with a `MeasurableSpace` structure, if `G` also has a `MeasurableInv` structure (where the preimage of every measurable set under inversion is measurable) and if we have a measurable function `f` from `α` to `G`, then the function which takes `x` in `α` and maps it to the inverse of `f(x)` in `G`, is also measurable. In mathematical terms, if `f : α → G` is a measurable function, then the function `x ↦ (f(x))⁻¹` is also measurable.
More concisely: If `f : α → G` is a measurable function between measurable spaces `α` and `G`, where `G` is endowed with an inverse operation and a measurable inverse structure, then the function `x ↦ (f(x))⁻¹` is measurable.
|
Measurable.const_smul
theorem Measurable.const_smul :
∀ {M : Type u_2} {β : Type u_3} {α : Type u_4} [inst : MeasurableSpace M] [inst_1 : MeasurableSpace β]
[inst_2 : SMul M β] {m : MeasurableSpace α} {g : α → β} [inst : MeasurableSMul M β],
Measurable g → ∀ (c : M), Measurable (c • g)
The theorem `Measurable.const_smul` states that given three types `M`, `β`, and `α`, under the assumption that `M` and `β` are measurable spaces and `M` and `β` have a scalar multiplication operation (`SMul`), if we have a measurable function `g` from `α` to `β` and any scalar `c` of type `M`, then the function obtained by scalar multiplication of `g` by `c` is also measurable. Here, a function is said to be measurable if the preimage of every measurable set is also measurable.
More concisely: If `M` and `β` are measurable spaces with a scalar multiplication operation, and `g` is a measurable function from `α` to `β` and `c` is any scalar in `M`, then the function `x ↔ c * g(x)` is measurable from `α` to `β`.
|
Measurable.mul
theorem Measurable.mul :
∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f g : α → M}
[inst_2 : MeasurableMul₂ M], Measurable f → Measurable g → Measurable fun a => f a * g a
The theorem `Measurable.mul` states that given any two functions `f` and `g` from a measurable space `α` to a space `M` equipped with a multiplication operation and a measure, if both `f` and `g` are measurable functions, then the function that maps an element of `α` to the product of `f` and `g` at that element (i.e., `(a => f a * g a)`) is also a measurable function. This is under the condition that `M` also supports the `MeasurableMul₂` operation, which is a typeclass indicating that the multiplication operation is measurable.
More concisely: If `α` is a measurable space, `M` is a measurable space equipped with a measurable multiplication operation, and `f` and `g` are measurable functions from `α` to `M`, then the function mapping `α` to the product of `f` and `g` is measurable.
|
Measurable.smul
theorem Measurable.smul :
∀ {M : Type u_2} {β : Type u_3} {α : Type u_4} [inst : MeasurableSpace M] [inst_1 : MeasurableSpace β]
[inst_2 : SMul M β] {m : MeasurableSpace α} {f : α → M} {g : α → β} [inst_3 : MeasurableSMul₂ M β],
Measurable f → Measurable g → Measurable fun x => f x • g x
The theorem `Measurable.smul` states that for any three types 'M', 'β', and 'α', where 'M' and 'β' are equipped with measurable spaces and 'M' and 'β' form a scalar multiplication structure, if we have a measurable space 'm' on 'α' and two functions 'f' and 'g' mapping 'α' to 'M' and 'β' respectively, then under the condition that 'M' and 'β' also form a measurable scalar multiplication structure, if both 'f' and 'g' are measurable functions, then the function that maps 'x' from 'α' to the scalar product of 'f(x)' and 'g(x)' is also measurable. In other words, the scalar product of two measurable functions is itself a measurable function.
More concisely: If M and β are measurable spaces with a measurable scalar multiplication structure, and f and g are measurable functions from a measurable space α to M and β, respectively, then the function x ∈ α => (f x) * (g x) is measurable.
|
Measurable.add
theorem Measurable.add :
∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f g : α → M}
[inst_2 : MeasurableAdd₂ M], Measurable f → Measurable g → Measurable fun a => f a + g a
The theorem `Measurable.add` states that for all types `M` and `α`, where `M` is a measurable space and has an addition operation, and `α` is a measurable space, if `f` and `g` are measurable functions from `α` to `M` and `M` supports measurable addition, then the function that maps each element `a` in `α` to the sum `f(a) + g(a)` in `M` is also a measurable function. This theorem establishes the measurability of the sum of two measurable functions.
More concisely: If `M` is a measurable space with an addition operation and `f` and `g` are measurable functions from a measurable space `α` to `M`, then the function that maps each `α` element `a` to the sum `f(a) + g(a)` is measurable.
|
measurable_div_const'
theorem measurable_div_const' :
∀ {G : Type u_2} [inst : DivInvMonoid G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g : G),
Measurable fun h => h / g
This theorem, `measurable_div_const'`, states that for any type `G` which has a division and inversion monoid structure, a measurable space structure, and a measurable multiplication structure, and any element `g` of type `G`, the function that takes an element `h` of the same type and divides it by `g` is a measurable function. In other words, the preimage of any measurable set under this function is also a measurable set. This is an alternative version of `measurable_div_const` which requires `MeasurableMul` instead of `MeasurableDiv` to avoid unnecessary type-class assumptions.
More concisely: For any type `G` with division and inversion monoid, measurable space, and measurable multiplication structures, the function that divides any element by a fixed element of `G` is measurable.
|
measurable_mul_unop
theorem measurable_mul_unop : ∀ {α : Type u_2} [inst : MeasurableSpace α], Measurable MulOpposite.unop
The theorem `measurable_mul_unop` asserts that for every type `α` equipped with a `MeasurableSpace` structure, the function `MulOpposite.unop` (which takes an element of the multiplicative opposite of `α` and returns an element of `α`) is measurable. In other words, the preimage of every measurable set under `MulOpposite.unop` is also measurable. This is a statement about the interplay between measure theory and the operation of taking the multiplicative opposite of a type.
More concisely: For any measurable space `α`, the function `MulOpposite.unop` mapping elements of the multiplicative opposite of `α` to `α` is a measurable function.
|
Measurable.neg
theorem Measurable.neg :
∀ {G : Type u_2} {α : Type u_3} [inst : Neg G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableNeg G]
{m : MeasurableSpace α} {f : α → G}, Measurable f → Measurable fun x => -f x
The theorem `Measurable.neg` states that, for any type `G` equipped with a negation operation and a measurable structure, and any type `α` with a measurable space structure, if we have a measurable function `f` from `α` to `G`, then the function obtained by applying the negation operation to the output of `f` (i.e., the function `x => -f x`) is also measurable. This means that if we take any measurable set in `G`, the preimage of this set under the negation of `f` is also measurable in `α`.
More concisely: If `f: α → G` is a measurable function between measurable spaces `(α, Σα)` and `(G, ΣG)`, where `G` is a negated type equipped with a negation operation, then the function `x ↦ -(f x)` is measurable.
|
Measurable.const_add
theorem Measurable.const_add :
∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f : α → M}
[inst_2 : MeasurableAdd M], Measurable f → ∀ (c : M), Measurable fun x => c + f x
The theorem `Measurable.const_add` states that for any type `M` with a `MeasurableSpace` structure and an `Add` operation, and any type `α` with a `MeasurableSpace` structure, if we have a function `f` from `α` to `M` that is measurable, and `M` has a `MeasurableAdd` structure, then for every constant `c` from `M`, the function that adds `c` to `f(x)` for every `x` in `α` is also measurable. In terms of measure theory, this means that the function obtained by adding a fixed constant to a measurable function is itself measurable.
More concisely: If `f` is a measurable function from a measurable space `(α, Σα)` to a measurable space `(M, ΣM)` with additive structure and `c` is a constant in `M`, then the function `x ↦ f(x) + c` is measurable.
|
AEMeasurable.const_smul
theorem AEMeasurable.const_smul :
∀ {M : Type u_2} {β : Type u_3} {α : Type u_4} [inst : MeasurableSpace M] [inst_1 : MeasurableSpace β]
[inst_2 : SMul M β] {m : MeasurableSpace α} {g : α → β} [inst : MeasurableSMul M β] {μ : MeasureTheory.Measure α},
AEMeasurable g μ → ∀ (c : M), AEMeasurable (c • g) μ
The theorem `AEMeasurable.const_smul` states that for any given types `M`, `β`, and `α`, with `M` and `β` being measurable spaces and `M` and `β` having a scalar multiplication (`SMul`), and given a measurable space `m` on `α`, a function `g: α → β`, a scalar multiplication measurability instance `inst` for `M` and `β`, and a measure `μ` on `α`, if `g` is almost everywhere measurable with respect to measure `μ`, then for any constant `c` from `M`, the function obtained by scalar multiplication of `c` and `g` (i.e., `c • g`) is also almost everywhere measurable with respect to the same measure `μ`.
More concisely: If `M` and `β` are measurable spaces with scalar multiplication, `m` is a measurable space on `α`, `g: α → β` is almost everywhere measurable with respect to measure `μ` on `α`, and `c` is a constant from `M`, then `c • g` is almost everywhere measurable with respect to `μ`.
|
Measurable.pow_const
theorem Measurable.pow_const :
∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
[inst_2 : Pow β γ] [inst_3 : MeasurablePow β γ] {m : MeasurableSpace α} {f : α → β},
Measurable f → ∀ (c : γ), Measurable fun x => f x ^ c
The theorem `Measurable.pow_const` states that for any measurable spaces `β`, `γ`, and `α`, if `β` and `γ` have a power operation (`Pow β γ`) and a measurable power operation (`MeasurablePow β γ`) is defined between these spaces, and if `f` is a measurable function from `α` to `β`, then for any constant `c` of type `γ`, the function that maps `x` in `α` to the `c`-th power of `f(x)` is measurable. In other words, if we can measure `f`, and we can measure the operation of raising to the `c`-th power, then we can also measure the function that first applies `f` and then raises the result to the `c`-th power.
More concisely: If `β` and `γ` are measurable spaces with a measurable power operation, and `f` is a measurable function from `α` to `β`, then the function `x ↦ c ^ (f x)` is measurable for any constant `c` of type `γ`.
|
AEMeasurable.inv
theorem AEMeasurable.inv :
∀ {G : Type u_2} {α : Type u_3} [inst : Inv G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableInv G]
{m : MeasurableSpace α} {f : α → G} {μ : MeasureTheory.Measure α},
AEMeasurable f μ → AEMeasurable (fun x => (f x)⁻¹) μ
The theorem `AEMeasurable.inv` states that for any types `G` and `α` where `G` has an `Inv` instance and a `MeasurableSpace` instance and also a `MeasurableInv` instance, and given a measurable space `m` on `α`, a function `f` from `α` to `G`, and a measure `μ` on `α`, if `f` is almost everywhere measurable (i.e., it is equal almost everywhere to a measurable function), then the function that takes `x` to the inverse of `f(x)` is also almost everywhere measurable.
More concisely: If `f` is almost everywhere measurable from a measurable space `(α, Σ, μ)` to a measurable space `(G, ℬ, ν)` where `G` has an `Inv` and `MeasurableSpace` instance, then the function `x ↦ Inv(f(x))` is almost everywhere measurable.
|
Measurable.pow
theorem Measurable.pow :
∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
[inst_2 : Pow β γ] [inst_3 : MeasurablePow β γ] {m : MeasurableSpace α} {f : α → β} {g : α → γ},
Measurable f → Measurable g → Measurable fun x => f x ^ g x
The theorem `Measurable.pow` states that for any types `β`, `γ`, and `α`, where `β` and `γ` have `MeasurableSpace` instances and a `Pow` operation, and `β` and `γ` also have a `MeasurablePow` instance, if we have a measurable space `m` of type `α`, and two functions `f : α → β` and `g : α → γ` such that `f` and `g` are measurable, then the function that takes an input `x` of type `α` and maps it to the power of `f x` by `g x` is also measurable. In simpler terms, this theorem asserts that the power of two measurable functions is also measurable.
More concisely: If `β` and `γ` are measurable spaces with measurable powers, and `f : α → β` and `g : α → γ` are measurable functions, then the function `x ↦ f x^g x` is measurable.
|
Measurable.const_mul
theorem Measurable.const_mul :
∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f : α → M}
[inst_2 : MeasurableMul M], Measurable f → ∀ (c : M), Measurable fun x => c * f x
The theorem `Measurable.const_mul` states that for any types `M` and `α`, given a measurable space over `M`, a multiplication operation on `M`, a measurable space `m` over `α`, a function `f` from `α` to `M`, and a measurability condition on the multiplication in `M`, if `f` is measurable, then the function that multiplies each output of `f` by a constant `c` is also measurable. In other words, if `f` is a measurable function from `α` to `M` and `c` is a constant in `M`, then the function defined by `x ↦ c * f(x)` is also measurable.
More concisely: If `f` is a measurable function from a measurable space `(α, Σ)` to a measurable space `(M, ℬ)` with a measurable multiplication operation, then the function `x ↦ c * f(x)` is measurable for any constant `c` in `M`.
|
Measurable.sub
theorem Measurable.sub :
∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f g : α → G}
[inst_2 : MeasurableSub₂ G], Measurable f → Measurable g → Measurable fun a => f a - g a
The theorem `Measurable.sub` states that for any type 'G' equipped with a measurable space structure and a subtraction operation, and any measurable space 'α', if 'f' and 'g' are two measurable functions from 'α' to 'G' and if 'G' has a defined measurable subtraction operation, then the function that maps each value in 'α' to the difference of the corresponding values in 'f' and 'g' is also a measurable function. This essentially means that the subtraction of two measurable functions is again a measurable function.
More concisely: If 'f' and 'g' are measurable functions from a measurable space 'α' to a measurable group 'G' with a defined measurable subtraction operation, then their pointwise difference is also a measurable function from 'α' to 'G'.
|
Measurable.mul_const
theorem Measurable.mul_const :
∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f : α → M}
[inst_2 : MeasurableMul M], Measurable f → ∀ (c : M), Measurable fun x => f x * c
The theorem `Measurable.mul_const` states that for any type `M` with a multiplication operation, any measurable space `M` and `α`, any measure preserving function `f` from `α` to `M`, and any constant `c` of type `M`, the function that sends `x` to the product of `f(x)` and `c` is also a measure preserving function. In other words, the multiplication of a measurable function by a constant maintains the measurability of the function.
More concisely: If `f` is a measure-preserving function from a measurable space `(α, Σ, μ)` to a type `M` with multiplication, and `c` is a constant of type `M`, then the function `x ↦ f(x) * c` is also measure-preserving.
|
measurable_add_unop
theorem measurable_add_unop : ∀ {α : Type u_2} [inst : MeasurableSpace α], Measurable AddOpposite.unop
The theorem `measurable_add_unop` states that for any type `α` which has a `MeasurableSpace` structure (think of it as a space where we can talk about "measurable" sets), the function `AddOpposite.unop` is a measurable function. In other words, given any measurable set in `α`, the preimage of this set under the function `AddOpposite.unop` is also a measurable set. The function `AddOpposite.unop` itself is used to convert an element of the additive opposite type `αᵃᵒᵖ` to the original type `α`.
More concisely: For any measurable space `α`, the function `AddOpposite.unop` from `α` to `α` is a measurable function.
|
measurableSet_eq_fun
theorem measurableSet_eq_fun :
∀ {α : Type u_3} {m : MeasurableSpace α} {E : Type u_4} [inst : MeasurableSpace E] [inst_1 : AddGroup E]
[inst_2 : MeasurableSingletonClass E] [inst_3 : MeasurableSub₂ E] {f g : α → E},
Measurable f → Measurable g → MeasurableSet {x | f x = g x}
The theorem `measurableSet_eq_fun` states that for any measurable spaces `α` and `E`, wherein `E` is an additive group and has measurable singleton and subtraction operations, if `f` and `g` are two measurable functions from `α` to `E`, then the set of all points `x` in `α` where `f x` equals `g x` is also a measurable set. In other words, the preimage of any measurable set under the equality function of `f` and `g` is measurable.
More concisely: If `α` is a measurable space, `E` is a measurable additive group, and `f, g : α → E` are measurable functions, then the set `{x : α | f x = g x}` is measurable.
|
Measurable.div
theorem Measurable.div :
∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f g : α → G}
[inst_2 : MeasurableDiv₂ G], Measurable f → Measurable g → Measurable fun a => f a / g a
The theorem `Measurable.div` states that for any type `G` with a `MeasurableSpace` and `Div` structures, and any type `α` with a `MeasurableSpace` structure, if `f` and `g` are two functions from `α` to `G` and `G` has a `MeasurableDiv₂` structure, then the function that takes an element `a` from `α` and maps it to the result of `f(a)` divided by `g(a)` (denoted as `f a / g a`), is also a measurable function. In other words, the division of two measurable functions is also measurable.
More concisely: If `f` and `g` are measurable functions from a measurable space `α` to a MeasurableSpace `G` with a MeasurableDiv₂ structure, then the function `x ↦ f x / g x` is measurable.
|
Measurable.sub_const
theorem Measurable.sub_const :
∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Sub G] {m : MeasurableSpace α} {f : α → G}
[inst_2 : MeasurableSub G], Measurable f → ∀ (c : G), Measurable fun x => f x - c
The theorem `Measurable.sub_const` states that for any type `G` with a `MeasurableSpace` and `Sub` structure, any type `α` with a `MeasurableSpace` structure, any function `f` from `α` to `G`, and any element `c` of `G`, if `f` is a measurable function and `G` supports measurable subtraction, then the function that maps each element `x` in `α` to the difference between `f(x)` and `c` is also measurable. This essentially means that subtracting a constant from a measurable function yields another measurable function, provided the codomain of the function supports both measurable spaces and subtraction.
More concisely: If `f` is a measurable function from a measurable space `α` to a measurable space `G` with subtraction, then the function `x ↦ f(x) - c` is measurable for any constant `c` in `G`.
|
AEMeasurable.add
theorem AEMeasurable.add :
∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f g : α → M}
{μ : MeasureTheory.Measure α} [inst_2 : MeasurableAdd₂ M],
AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun a => f a + g a) μ
This theorem states that, given two functions `f` and `g` from a type `α` to a type `M` where `M` is a measurable space with a defined addition operation, if both `f` and `g` are almost everywhere measurable with respect to a measure `μ`, then the function that maps `a` to the sum of `f(a)` and `g(a)` is also almost everywhere measurable with respect to the same measure. Here, almost everywhere measurable means that the functions coincide almost everywhere with a measurable function.
More concisely: If `f` and `g` are almost everywhere measurable functions from a measurable space `(α, μ)` to a measurable additive group `M`, then their pointwise sum is also almost everywhere measurable.
|
measurable_sub_const'
theorem measurable_sub_const' :
∀ {G : Type u_2} [inst : SubNegMonoid G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g : G),
Measurable fun h => h - g
This theorem, `measurable_sub_const'`, states that for any type `G` that has a subtraction and negation operation (i.e., is a `SubNegMonoid`) and is a measurable space with a measurable addition operation (i.e., has `MeasurableAdd`), and for any element `g` of `G`, the function that subtracts `g` from its input is a measurable function. In other words, if you have a set `G` where you can measure, subtract, and add elements, and you have a specific element `g` from that set, then the function that subtracts `g` from another element is always a measurable function. A function is measurable if the preimage of every measurable set is also a measurable set.
More concisely: If `G` is a SubNegMonoid with MeasurableAdd, then for any `g` in `G`, the function `x => x - g` is measurable.
|
AEMeasurable.mul
theorem AEMeasurable.mul :
∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f g : α → M}
{μ : MeasureTheory.Measure α} [inst_2 : MeasurableMul₂ M],
AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun a => f a * g a) μ
This theorem, `AEMeasurable.mul`, states that in a measurable space `M` equipped with a binary multiplication operation, given two functions `f` and `g` from some measurable space `α` to `M` which are "almost everywhere measurable" with respect to a given measure `μ`, their pointwise product is also "almost everywhere measurable".
In other words, if `f` and `g` coincide almost everywhere with measurable functions in the measure space defined by `μ`, then the function that maps each element `a` in `α` to the product of `f(a)` and `g(a)` also coincides almost everywhere with a measurable function. This is under the assumption that the multiplication operation on `M` is measurable as a binary function.
More concisely: Given measurable spaces `(M, Σ)` with a measurable binary multiplication operation, if `f` and `g` are almost everywhere defined measurable functions from a measurable space `(α, Σ′)` to `(M, Σ)` with respect to measures `μ` and `ν`, respectively, then their pointwise product is an almost everywhere defined measurable function from `α` to `M`.
|