MeasureTheory.SimpleFunc.ext
theorem MeasureTheory.SimpleFunc.ext :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {f g : MeasureTheory.SimpleFunc α β},
(∀ (a : α), ↑f a = ↑g a) → f = g
This theorem, `MeasureTheory.SimpleFunc.ext`, in the Lean 4 language is stating that for any two simple functions `f` and `g` of the same types `α` and `β`, where `α` is a measurable space, if the function values of `f` and `g` are equal for all elements of `α` (i.e., `f(a) = g(a)` for all `a` in `α`), then `f` and `g` are essentially the same function. In simpler terms, if two simple functions produce the same outputs for the same inputs, they are the same function.
More concisely: If two simple functions `f` and `g` of the same types have equal values for all measurable elements, then `f` and `g` are equal almost everywhere.
|
MeasureTheory.SimpleFunc.coe_injective
theorem MeasureTheory.SimpleFunc.coe_injective :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] ⦃f g : MeasureTheory.SimpleFunc α β⦄, ↑f = ↑g → f = g
This theorem, `MeasureTheory.SimpleFunc.coe_injective`, states that for any two simple functions `f` and `g` over a measurable space `α`, if the co-domain (expressed as `↑f` and `↑g`) of these two functions is equal, then the functions `f` and `g` themselves are equal. This shows that the function from `MeasureTheory.SimpleFunc α β` to its co-domain is injective, i.e., different simple functions have different co-domains.
More concisely: If two simple functions `f` and `g` over a measurable space `α` have equal co-domains, then `f` equals `g`.
|
MeasureTheory.SimpleFunc.coe_pow
theorem MeasureTheory.SimpleFunc.coe_pow :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Monoid β] (f : MeasureTheory.SimpleFunc α β)
(n : ℕ), ↑(f ^ n) = ↑f ^ n
This theorem states that for any measurable space `α` and any monoid `β`, for a given simple function `f` from `α` to `β` and a natural number `n`, the coercion of the nth power of `f` (`f ^ n`) is equal to the nth power of the coercion of `f` (`↑f ^ n`). Here, a simple function refers to a Measure Theory concept, where the function only takes on a finite number of values.
More concisely: For any measurable space `α`, monoid `β`, simple function `f` from `α` to `β`, and natural number `n`, `(↑f ^ n) = ↑(f ^ n)`.
|
MeasureTheory.SimpleFunc.restrict_of_not_measurable
theorem MeasureTheory.SimpleFunc.restrict_of_not_measurable :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] {f : MeasureTheory.SimpleFunc α β}
{s : Set α}, ¬MeasurableSet s → f.restrict s = 0
The theorem `MeasureTheory.SimpleFunc.restrict_of_not_measurable` states that for any given types `α` and `β`, with `α` having a `MeasurableSpace` instance and `β` having a `Zero` instance, given a simple function `f` from `α` to `β` and a set `s` of type `α`, if the set `s` is not measurable, then the restriction of the simple function `f` to the set `s` is equivalent to the zero function. In other words, if you restrict a simple function to a non-measurable set, you will get a function that is identically zero.
More concisely: If `α` is a measurable space, `β` has a zero, `f` is a simple function from `α` to `β`, and `s` is a non-measurable subset of `α`, then `f[s]` (the restriction of `f` to `s`) is equal to the zero function.
|
MeasureTheory.SimpleFunc.coe_sub
theorem MeasureTheory.SimpleFunc.coe_sub :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Sub β] (f g : MeasureTheory.SimpleFunc α β),
↑(f - g) = ↑f - ↑g
This theorem states that for any two simple functions `f` and `g` of type `MeasureTheory.SimpleFunc` that map from a measurable space `α` to an arbitrary type `β` that supports subtraction operation, the coercion of the difference between `f` and `g` (i.e., `f - g`) is equal to the difference between the coercion of `f` and the coercion of `g` (i.e., `↑f - ↑g`). This means that taking the difference of two simple functions and then coercing the result is the same as coercing the functions first and then taking their difference.
More concisely: For any measurable spaces α and simple functions f, g : α → β with β having subtraction, the coercion of (f - g) is equal to ↑f - ↑g.
|
MeasureTheory.SimpleFunc.measurable
theorem MeasureTheory.SimpleFunc.measurable :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
(f : MeasureTheory.SimpleFunc α β), Measurable ↑f
This theorem states that any simple function is measurable. Here, a simple function `f` is a function from a measurable space `α` to another measurable space `β`. A function is considered measurable if the preimage of any measurable set is also a measurable set. In this context, a measurable set is a set for which a measure can be assigned in a meaningful way. Consequently, the theorem confirms that for every simple function `f`, the function `f` is measurable.
More concisely: Every simple function between two measurable spaces is measurable.
|
MeasureTheory.SimpleFunc.coe_smul
theorem MeasureTheory.SimpleFunc.coe_smul :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : SMul K β] (c : K)
(f : MeasureTheory.SimpleFunc α β), ↑(c • f) = c • ↑f
This theorem states that for any measurable space `α`, any types `β` and `K`, and given that `K` is a scalar multiplication type over `β`, if we have a scalar `c` of type `K` and a simple function `f` from `α` to `β` under the measure theory context, then the coercion of the scalar multiplication of `c` and `f` (i.e., `c • f`) is equal to the scalar multiplication of `c` and the coercion of `f` (i.e., `c • ↑f`). This theorem ensures the compatibility of scalar multiplication with the coercion operation in the context of simple functions in measure theory.
More concisely: For any measurable space, scalar multiplication type `K` over type `β`, scalar `c` in `K`, and simple function `f` from `α` to `β`, `c • f` equals `c • ↑f` in the context of measure theory.
|
MeasureTheory.SimpleFunc.lintegral_eq_of_measure_preimage
theorem MeasureTheory.SimpleFunc.lintegral_eq_of_measure_preimage :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasurableSpace β]
{f : MeasureTheory.SimpleFunc α ENNReal} {g : MeasureTheory.SimpleFunc β ENNReal} {ν : MeasureTheory.Measure β},
(∀ (y : ENNReal), ↑↑μ (↑f ⁻¹' {y}) = ↑↑ν (↑g ⁻¹' {y})) → f.lintegral μ = g.lintegral ν
The theorem `MeasureTheory.SimpleFunc.lintegral_eq_of_measure_preimage` states that for any two simple functions `f` and `g` mapping into the extended nonnegative real numbers, from measurable spaces `α` and `β` respectively, with associated measures `μ` and `ν`, the Lebesgue integral of `f` with respect to `μ` equals the Lebesgue integral of `g` with respect to `ν`, if and only if for every extended nonnegative real number `y`, the measure of the preimage of `f` under `y` equals the measure of the preimage of `g` under `y`. In simpler terms, the integrals of two simple functions are equal if the measures of the sets of all elements that are mapped to the same value by each function are equal.
More concisely: The Lebesgue integrals of simple functions `f` and `g` from measurable spaces `α` and `β` with measures `μ` and `ν` respectively, are equal if and only if for each extended nonnegative real number `y`, the preimages `f⁻¹{y}` and `g⁻¹{y}` have equal measures under `μ` and `ν`.
|
Measurable.simpleFunc_add
theorem Measurable.simpleFunc_add :
∀ {α : Type u_1} {E : Type u_5} {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : AddGroup E]
[inst_2 : MeasurableAdd E] {g : α → E},
Measurable g → ∀ (f : MeasureTheory.SimpleFunc α E), Measurable (↑f + g)
This theorem establishes that in a topological vector space, if you have a measurable function and a simple function, the function that maps each input to the sum of the values of the simple function and the measurable function at that input is itself measurable. More technically, for any given measurable space `α`, a type `E` that has a structure of measurable space, addition operation, and a property that the addition operation is measurable, if `g` is a measurable function from `α` to `E`, and `f` is a simple function from `α` to `E`, then the function which adds the respective outputs of `f` and `g` for each input in `α` is also a measurable function.
More concisely: In a topological vector space, if `g` is a measurable function and `f` is a simple function, then the function that maps each input to the sum of `f` and `g` is measurable.
|
Measurable.ennreal_induction
theorem Measurable.ennreal_induction :
∀ {α : Type u_1} [inst : MeasurableSpace α] {P : (α → ENNReal) → Prop},
(∀ (c : ENNReal) ⦃s : Set α⦄, MeasurableSet s → P (s.indicator fun x => c)) →
(∀ ⦃f g : α → ENNReal⦄,
Disjoint (Function.support f) (Function.support g) → Measurable f → Measurable g → P f → P g → P (f + g)) →
(∀ ⦃f : ℕ → α → ENNReal⦄,
(∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ n, f n x) →
∀ ⦃f : α → ENNReal⦄, Measurable f → P f
This theorem, `Measurable.ennreal_induction`, is a form of structural induction for measurable functions into the extended nonnegative real numbers (ℝ≥0∞).
The theorem states that to prove a property, `P`, holds for an arbitrary measurable function, `f`, it is sufficient to show three things:
1. `P` holds for characteristic functions (functions that take the value 1 on a given set and 0 otherwise) multiplied by a constant `c`.
2. `P` is preserved under the addition of two measurable functions `f` and `g` whose supports (the sets where the functions are non-zero) are disjoint, given that `P` holds for `f` and `g`.
3. `P` is preserved under the supremum (least upper bound) of a monotone increasing sequence of measurable functions, given that `P` holds for every function in the sequence.
If these conditions are met, then `P` holds for any measurable function `f` into ℝ≥0∞.
More concisely: Given a property `P` and a measurable function `f` from a measurable space to the extended nonnegative real numbers, if `P` holds for characteristic functions scaled by constants, is preserved under the addition of measurable functions with disjoint supports, and is preserved under the supremum of monotone increasing sequences of measurable functions, then `P` holds for `f`.
|
MeasureTheory.SimpleFunc.measurableSet_cut
theorem MeasureTheory.SimpleFunc.measurableSet_cut :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (r : α → β → Prop) (f : MeasureTheory.SimpleFunc α β),
(∀ (b : β), MeasurableSet {a | r a b}) → MeasurableSet {a | r a (↑f a)}
The theorem `MeasureTheory.SimpleFunc.measurableSet_cut` states that for any given types `α` and `β`, along with a measurable space `α`, a relation `r` between types `α` and `β`, and a simple function `f` mapping `α` to `β`, if for every `β`, the set of `α` that relate to `β` (denoted by `{a | r a b}`) is measurable, then the set of `α` that relate to the function value of `α` (denoted by `{a | r a (↑f a)}`) is also measurable. Here, 'measurable' refers to the set being measurable in the ambient measure space on `α`. This theorem establishes a condition under which the measurability of a certain type of set ensures the measurability of another related set.
More concisely: If for every `β`, the set `{a | r a b}` is measurable and `r` is a relation between types `α` and `β`, then the set `{a | r a (↑f a)}` is measurable for any measurable space on `α` and simple function `f` mapping `α` to `β`.
|
MeasureTheory.SimpleFunc.coe_range
theorem MeasureTheory.SimpleFunc.coe_range :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β),
↑f.range = Set.range ↑f
The theorem `MeasureTheory.SimpleFunc.coe_range` states that for any type `α` equipped with a measurable space structure (`inst : MeasurableSpace α`) and any type `β`, the range, as a `Finset`, of a simple function `f : MeasureTheory.SimpleFunc α β` when coerced to a `Set` is equal to the set range of `f` itself. In other words, the set of all outputs of the function `f` (when viewed as a simple function or a regular function) are the same.
More concisely: For any measurable space `(α, Σ, mu)` and simple function `f : α → β` between measurable sets, the range of `f` as a `Finset` is equal to the set of images of `f`.
|
MeasureTheory.SimpleFunc.monotone_eapprox
theorem MeasureTheory.SimpleFunc.monotone_eapprox :
∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ENNReal), Monotone (MeasureTheory.SimpleFunc.eapprox f) := by
sorry
This theorem states that for any type `α` equipped with a measurable space instance and for any function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), the sequence of simple functions that approximate `f` (obtained using `MeasureTheory.SimpleFunc.eapprox`) is monotone. In other words, if `n ≤ m` then `MeasureTheory.SimpleFunc.eapprox f n` is less than or equal to `MeasureTheory.SimpleFunc.eapprox f m` for all elements of `α`. Here, the term "less than or equal to" is understood in the sense of pointwise comparison of functions, i.e., for each point in the domain the value of the first function is less than or equal to the value of the second function.
More concisely: For any measurable space `(α, Σ, μ)` and measurable function `f : α → ENNReal`, the sequence of simple function approximations `MeasureTheory.SimpleFunc.eapprox f n` is monotone increasing, i.e., `n ≤ m` implies `MeasureTheory.SimpleFunc.eapprox f n ≤ MeasureTheory.SimpleFunc.eapprox f m` pointwise.
|
MeasureTheory.SimpleFunc.measurableSet_preimage
theorem MeasureTheory.SimpleFunc.measurableSet_preimage :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (s : Set β),
MeasurableSet (↑f ⁻¹' s)
The theorem `MeasureTheory.SimpleFunc.measurableSet_preimage` states that for any types `α` and `β`, given a measurable space structure on `α`, a simple function `f` from `α` to `β`, and a set `s` of type `β`, the preimage of the set `s` under the function `f` is a measurable set.
In other words, if we apply the function `f` to some elements of `α` and consider the set of all such elements that map into `s`, that set of elements from `α` is measurable. This is a fundamental property in measure theory, which ensures that we can measure the "size" of the set of all elements that get mapped into a particular subset of the range of a simple function.
More concisely: If `α` is a measurable space, `f` is a simple function from `α` to `β`, and `s` is a set in `β`, then the preimage `f⁻¹(s)` is a measurable set in `α`.
|
MeasureTheory.SimpleFunc.extend_apply
theorem MeasureTheory.SimpleFunc.extend_apply :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
(f₁ : MeasureTheory.SimpleFunc α γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : MeasureTheory.SimpleFunc β γ)
(x : α), ↑(f₁.extend g hg f₂) (g x) = ↑f₁ x
This theorem states that, given two simple functions `f₁` and `f₂` with domains `α` and `β` respectively and the same codomain `γ`, alongside a measurable embedding function `g` from `α` to `β`, when we extend `f₁` along `g` to obtain a new simple function, then for any point `x` in `α`, the value of the extended function at the image of `x` under `g` is the same as the value of `f₁` at `x`. This is true under the assumption that `α` and `β` are equipped with measurable spaces.
More concisely: Given measurable spaces `(α, Σα)` and `(β, Σβ)`, measurable embeddings `g : α → β`, simple functions `f₁ : α → γ`, and `f₂ : β → γ` with `f₁ = f₂ ∘ g`, we have `(f₁ ! g x) = f₂ x` for all `x : α`.
|
MeasureTheory.SimpleFunc.coe_add
theorem MeasureTheory.SimpleFunc.coe_add :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Add β] (f g : MeasureTheory.SimpleFunc α β),
↑(f + g) = ↑f + ↑g
This theorem states that for any two simple functions `f` and `g`, which are defined over a measurable space `α` and take values in an additive space `β`, the measure of the sum `f + g` equals to the sum of their respective measures. In other words, the measure of the sum of two simple functions is the sum of their measures. This property is fundamental in measure theory and integral calculus.
More concisely: For simple functions `f` and `g` on measurable space `α` with values in an additive space `β`, their sum `f + g` has the same measure as the sum of their individual measures.
|
MeasureTheory.SimpleFunc.add_lintegral
theorem MeasureTheory.SimpleFunc.add_lintegral :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : MeasureTheory.SimpleFunc α ENNReal),
(f + g).lintegral μ = f.lintegral μ + g.lintegral μ
The theorem `MeasureTheory.SimpleFunc.add_lintegral` states that for any measure space `α` with a measure `μ`, and for any two simple functions `f` and `g` mapping from `α` to the extended nonnegative real numbers, the integral of the sum of the two simple functions (i.e., `f + g`) with respect to the measure `μ` equals the sum of the integrals of the individual simple functions `f` and `g` with respect to the measure `μ`. In mathematical terms, this theorem asserts linearity of the integral on simple functions, namely ∫(f + g) dμ = ∫f dμ + ∫g dμ.
More concisely: The integral of the sum of two simple functions with respect to a measure is equal to the sum of their individual integrals with respect to the same measure.
|
MeasureTheory.SimpleFunc.coe_zero
theorem MeasureTheory.SimpleFunc.coe_zero :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β], ↑0 = 0
The theorem `MeasureTheory.SimpleFunc.coe_zero` states that for any types `α` and `β`, where `α` has a measurable space structure and `β` has a zero element, the coercion of zero (denoted as `↑0`) equals to zero. Essentially, it establishes that in the context of measure theory, the simple function's representation of zero is the same as the typical notion of zero.
More concisely: For any measurable space `α` and type `β` with a zero element, the coercion of zero from the simple function space to `β` equals zero.
|
Measurable.add_simpleFunc
theorem Measurable.add_simpleFunc :
∀ {α : Type u_1} {E : Type u_5} {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : AddGroup E]
[inst_2 : MeasurableAdd E] {g : α → E},
Measurable g → ∀ (f : MeasureTheory.SimpleFunc α E), Measurable (g + ↑f)
In the context of a topological vector space, the theorem `Measurable.add_simpleFunc` asserts that for any measurable space `α` and type `E`, given `x` which is a measurable space of type `α`, `E` as a measurable space, an addition group on `E`, a measurable addition for `E`, and a function `g` mapping from `α` to `E` that is measurable, if `f` is a simple function from `α` to `E`, then the sum of `g` and `f` (denoted as `g + ↑f`) is also measurable. Here, measurability means that the preimage of any measurable set under the function is also measurable.
More concisely: If `α` is a measurable space, `E` is an additive Abelian group with a measurable addition, `g` is a measurable function from `α` to `E`, and `f` is a simple measurable function from `α` to `E`, then the function `g + f` is measurable.
|
MeasureTheory.SimpleFunc.lintegral_congr
theorem MeasureTheory.SimpleFunc.lintegral_congr :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : MeasureTheory.SimpleFunc α ENNReal},
μ.ae.EventuallyEq ↑f ↑g → f.lintegral μ = g.lintegral μ
This theorem states that if two simple functions, where a simple function is a measurable function that takes on a finite number of values, are almost everywhere equal with respect to a given measure, then the Lebesgue integrals of these two functions with respect to the same measure are equal. The function values are of type ENNReal, which refer to the extended nonnegative real numbers, often denoted as [0, ∞], which is relevant as it is the codomain of a measure. So, in simple terms, if two simple functions are essentially the same when measured, then their areas under the curve (Lebesgue integrals) are the same.
More concisely: If two simple functions are almost everywhere equal with respect to a measure, then their Lebesgue integrals are equal.
|
MeasureTheory.SimpleFunc.coe_mul
theorem MeasureTheory.SimpleFunc.coe_mul :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Mul β] (f g : MeasureTheory.SimpleFunc α β),
↑(f * g) = ↑f * ↑g
This theorem states that for any two simple functions `f` and `g` from a measurable space `α` to a type `β` equipped with a multiplication operation, the result of multiplying the two simple functions (`f * g`) and then converting to a non-simple function (using the coercion function `↑`) is the same as first converting each of the simple functions to non-simple functions and then multiplying these non-simple functions (`↑f * ↑g`).
More concisely: For any measurable spaces `α` and type `β` with multiplication, the conversion of the product of two simple functions `f` and `g` from `α` to `β` to a non-simple function is equal to the product of the non-simple functions obtained from the conversion of `f` and `g`. In Lean 4 symbolism: `(↑(f * g) = ↑f * ↑g)`.
|
MeasureTheory.SimpleFunc.coe_restrict
theorem MeasureTheory.SimpleFunc.coe_restrict :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] (f : MeasureTheory.SimpleFunc α β)
{s : Set α}, MeasurableSet s → ↑(f.restrict s) = s.indicator ↑f
This theorem states that for any measure space 'α' and any type 'β' with a zero element, given a measure theory simple function 'f' from 'α' to 'β' and a set 's' in 'α' that is measurable, the function obtained by restricting 'f' to 's' is identical to the indicator function of 's' applied to the original function 'f'. In other words, each value 'a' in the set 's' maps to 'f a' and values not in 's' map to zero.
More concisely: For any measurable set $s$ in a measure space $\alpha$ and measurable simple function $f:\alpha\to\beta$ with zero element, the restricted function $f|_s = \chi_s\circ f$, where $\chi_s$ is the indicator function of $s$.
|
MeasureTheory.SimpleFunc.finMeasSupp_iff
theorem MeasureTheory.SimpleFunc.finMeasSupp_iff :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : Zero β] {μ : MeasureTheory.Measure α}
{f : MeasureTheory.SimpleFunc α β}, f.FinMeasSupp μ ↔ ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
This theorem states that a `MeasureTheory.SimpleFunc` `f` has finite measure support with respect to measure `μ` if and only if for any value `y` in the codomain, if `y` is not zero then the measure of the preimage of `y` under `f` is less than infinity. In other words, the function `f` is equal to zero except on a set of finite measure.
More concisely: A function `f` in the category of `MeasureTheory.SimpleFunc` has finite measure support with respect to measure `μ` if and only if for all codomain values `y` different from zero, the preimage of `y` under `f` has finite measure.
|
MeasureTheory.SimpleFunc.iSup_eapprox_apply
theorem MeasureTheory.SimpleFunc.iSup_eapprox_apply :
∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ENNReal),
Measurable f → ∀ (a : α), ⨆ n, ↑(MeasureTheory.SimpleFunc.eapprox f n) a = f a
This theorem states that for any measurable space `α` and a measurable function `f` from `α` to the extended nonnegative real numbers (`ENNReal`), for any element `a` in `α`, the supremum (or least upper bound) over all natural numbers `n` of the value of `a` under the `n`th approximation of `f` by simple functions is equal to the actual value of `f` at `a`. In other words, the sequence of simple function approximations converges pointwise to the original function `f` for every element in the domain.
More concisely: For any measurable space `α`, measurable function `f` from `α` to the extended nonnegative real numbers, and any `α` element `a`, the pointwise limit of the sequence of simple function approximations of `f` equals the value of `f` at `a`.
|
Mathlib.MeasureTheory.Function.SimpleFunc._auxLemma.1
theorem Mathlib.MeasureTheory.Function.SimpleFunc._auxLemma.1 :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {b : β},
(b ∈ f.range) = (b ∈ Set.range ↑f)
The theorem `Mathlib.MeasureTheory.Function.SimpleFunc._auxLemma.1` establishes an equivalence between the range of a simple function `f` in measure theory and the set range of `f`. More specifically, for any types `α` and `β`, given a measurable space instance on `α` and a simple function `f` from `α` to `β`, and any element `b` of `β`, it states that `b` is in the range of `f` (as defined in measure theory) if and only if `b` is in the set range of `f`.
More concisely: For any measurable simple function $f$ from type $\alpha$ to type $\beta$ in measure theory, the range of $f$ equals the set range of $f$.
|
MeasureTheory.SimpleFunc.finite_range
theorem MeasureTheory.SimpleFunc.finite_range :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β),
(Set.range ↑f).Finite
The theorem `MeasureTheory.SimpleFunc.finite_range` states that for any measurable space `α` and type `β`, the range of any simple function (a function from `α` to `β` that only takes a finite number of distinct values) is a finite set. In other words, there exists a natural number `n` such that there is an equivalence between the range of the simple function and the set of natural numbers less than `n`.
More concisely: A simple function from a measurable space to a type with a finite range is equal in size to some finite set.
|
MeasureTheory.SimpleFunc.lintegral_mono
theorem MeasureTheory.SimpleFunc.lintegral_mono :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f g : MeasureTheory.SimpleFunc α ENNReal},
f ≤ g → μ ≤ ν → f.lintegral μ ≤ g.lintegral ν
The theorem `MeasureTheory.SimpleFunc.lintegral_mono` states that the integral of a simple function, whose codomain is the set of extended nonnegative real numbers, is monotone with respect to both the function and the measure. Specifically, for any measurable space `α` and any two measures `μ` and `ν` on `α`, if one simple function `f` is less than or equal to another simple function `g` and if the measure `μ` is less than or equal to measure `ν`, then the integral of the function `f` with respect to measure `μ` is less than or equal to the integral of the function `g` with respect to measure `ν`.
More concisely: If simple functions `f` and `g` are measurable, `α` is a measurable space, and measures `μ` and `ν` satisfy `μ ≤ ν`, then for all `x ∈ ℝ↑`, `∫(f dμ) ≤ ∫(g dν)`.
|
MeasureTheory.SimpleFunc.map_lintegral
theorem MeasureTheory.SimpleFunc.map_lintegral :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (g : β → ENNReal)
(f : MeasureTheory.SimpleFunc α β),
(MeasureTheory.SimpleFunc.map g f).lintegral μ = f.range.sum fun x => g x * ↑↑μ (↑f ⁻¹' {x})
The theorem `MeasureTheory.SimpleFunc.map_lintegral` states that for any measurable space `α`, function `g` from `β` to the extended nonnegative real numbers `ENNReal`, and a simple function `f` from `α` to `β`, the integral of the function `g` composed with `f` with respect to a measure `μ` is equal to the sum, over the range of `f`, of the product of `g(x)` and the measure of the preimage of `x` under `f`. In other words, it's calculating the integral of `(g ∘ f)` in terms of the values of `f` and `g` and the measure `μ`.
More concisely: For any measurable spaces α, β, measurable function f: α → β, simple function g: β → [0, +∞], and measure μ on α, the integral of g ∘ f with respect to μ is equal to the sum, over the range of f, of the products g(x) * μ(f^-1(x)).
|
MeasureTheory.SimpleFunc.mem_range
theorem MeasureTheory.SimpleFunc.mem_range :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {b : β},
b ∈ f.range ↔ b ∈ Set.range ↑f
The theorem `MeasureTheory.SimpleFunc.mem_range` states that for any types `α` and `β`, with `α` being a measurable space, and any simple function `f` from `α` to `β`, and any element `b` of type `β`, `b` is in the range of the simple function `f` (expressed as a finite set) if and only if `b` is in the image of the function `f` over its entire domain (expressed as a set). In other words, it's asserting that the range of a simple function `f` and the set of images of `f` over its entire domain are the same.
More concisely: For any measurable space (α, Σ), simple function f : α → β, and b ∈ β, b is in the range of f if and only if b is in the image of f.
|
MeasureTheory.SimpleFunc.coe_one
theorem MeasureTheory.SimpleFunc.coe_one :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : One β], ↑1 = 1
This theorem states that for any types `α` and `β`, where `α` is a measurable space and `β` has a defined "one" operation, the coercion of the numeric value one (1) is still one (1). Essentially, this means that the number one (1) maintains its identity under coercion in this context.
More concisely: For any measurable spaces `α` and type `β` with a defined "one" operation, the coercion of the numeric value 1 from the real numbers to `β` is equal to the "one" element of `β`.
|
MeasureTheory.SimpleFunc.support_eq
theorem MeasureTheory.SimpleFunc.support_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] (f : MeasureTheory.SimpleFunc α β),
Function.support ↑f = ⋃ y ∈ Finset.filter (fun y => y ≠ 0) f.range, ↑f ⁻¹' {y}
The theorem `MeasureTheory.SimpleFunc.support_eq` states that for any measurable space `α` and any type `β` with a zero, given a simple function `f` mapping `α` to `β`, the support of `f` (i.e., the set of points `x` in `α` for which `f(x)` is not zero) is equal to the union of the preimage of `f` for each element `y` in the filtered set, where the filter excludes zero and operates on the range of `f`. In other words, the support of `f` is the collection of all points mapped to nonzero values by `f`.
More concisely: The support of a simple function from a measurable space to a type with a zero is equal to the union of the preimages of non-zero elements under that function.
|
MeasureTheory.SimpleFunc.induction
theorem MeasureTheory.SimpleFunc.induction :
∀ {α : Type u_5} {γ : Type u_6} [inst : MeasurableSpace α] [inst_1 : AddMonoid γ]
{P : MeasureTheory.SimpleFunc α γ → Prop},
(∀ (c : γ) {s : Set α} (hs : MeasurableSet s),
P
(MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c)
(MeasureTheory.SimpleFunc.const α 0))) →
(∀ ⦃f g : MeasureTheory.SimpleFunc α γ⦄,
Disjoint (Function.support ↑f) (Function.support ↑g) → P f → P g → P (f + g)) →
∀ (f : MeasureTheory.SimpleFunc α γ), P f
The theorem `MeasureTheory.SimpleFunc.induction` states that to prove a property for an arbitrary simple function, it is sufficient to show two things:
1. The property holds for simple functions that are multiples of characteristic functions. A characteristic function takes a measurable set and its measureability, along with some constant, and gives a simple function. This function is zero elsewhere but equals to the given constant on the provided set.
2. The property is closed under addition, that is, if the property holds for two simple functions whose supports (sets where the function is non-zero) are disjoint, then it also holds for the function obtained by adding these two functions.
To put it more formally, let `α` be a type with a measurable space structure, and let `γ` be a type with an addition monoid structure. If `P` is a property on simple functions from `α` to `γ`, then to prove that `P` holds for all simple functions, it is enough to show that `P` holds for simple functions that are multiples of characteristic functions, and that whenever `f` and `g` are simple functions with disjoint supports and `P` holds for `f` and `g`, then `P` also holds for `f + g`.
More concisely: To prove a property holds for all simple functions from a measurable space to an additive monoid, it suffices if it holds for simple functions that are multiples of characteristic functions and for the sum of two such functions with disjoint supports.
|
MeasureTheory.SimpleFunc.measurableSet_fiber
theorem MeasureTheory.SimpleFunc.measurableSet_fiber :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (x : β),
MeasurableSet (↑f ⁻¹' {x})
The theorem `MeasureTheory.SimpleFunc.measurableSet_fiber` states that for any types `α` and `β`, given a measurable space `α` and a simple function `f` from `α` to `β`, the preimage of any singleton set `{x}` under the function `f` is a measurable set. Here, `x` is a value of type `β`. In other words, this theorem states that for any value `x` in the codomain, the set of elements in the domain that map to `x` under `f` is a measurable set.
More concisely: For any measurable space (α, Σ), simple function f : α → β, and x ∈ β, the preimage {α ∣ f(α) = x} is a measurable set in Σ.
|
MeasureTheory.SimpleFunc.lintegral_eq_of_subset
theorem MeasureTheory.SimpleFunc.lintegral_eq_of_subset :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α ENNReal)
{s : Finset ENNReal},
(∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s) →
f.lintegral μ = s.sum fun x => x * ↑↑μ (↑f ⁻¹' {x})
This theorem states that, for any measurable space `α`, measure `μ` on `α`, and simple function `f` from `α` to the extended nonnegative reals, if every non-zero value of `f` that is assigned a non-zero measure by `μ` is included in a finite set `s`, then the integral of `f` with respect to `μ` is equal to the sum, over all elements `x` in `s`, of `x` times the measure of the preimage of `x` under `f`. This effectively means that the integral of a simple function can be computed by summing up the products of each unique function value and its corresponding measure over a suitable finite set.
More concisely: If a simple function `f` from a measurable space `(α, μ)` to the extended nonnegative reals assigns a finite, non-zero measure to every non-zero value that lies in a finite set `s`, then the integral of `f` with respect to `μ` equals the sum of `x` times the measure of `f^{-1}({x})` for all `x` in `s`.
|