Real.volume_Icc
theorem Real.volume_Icc : ∀ {a b : ℝ}, ↑↑MeasureTheory.volume (Set.Icc a b) = ENNReal.ofReal (b - a)
The theorem `Real.volume_Icc` states that for any two real numbers `a` and `b`, the Lebesgue measure (volume) of the interval between `a` and `b` (inclusive of `a` and `b`) is equal to the nonnegative part of the difference between `b` and `a`. In mathematical terms, for any $a, b \in \mathbb{R}$, ${\mu([a, b])} = \max\{b - a, 0\}$ where $\mu$ denotes the Lebesgue measure. This theorem essentially asserts that the measure of an interval in the real numbers is just the difference of its endpoints when the left endpoint is less than or equal to the right endpoint, and zero otherwise.
More concisely: The Lebesgue measure of the interval $[a, b]$ is equal to the maximum of the difference between $b$ and $a$, and 0.
|
nullMeasurableSet_regionBetween
theorem nullMeasurableSet_regionBetween :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ},
AEMeasurable f μ →
AEMeasurable g μ →
∀ {s : Set α},
MeasureTheory.NullMeasurableSet s μ →
MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioo (f p.1) (g p.1)}
(μ.prod MeasureTheory.volume)
This theorem states that for any measurable space `α` and any measure `μ` on `α`, if `f` and `g` are two almost everywhere (a.e.)-measurable functions from `α` to real numbers, and if `s` is a null-measurable set in `α`, then the set of ordered pairs whose first element is in `s` and whose second element is strictly between the values of `f` and `g` at the first element, is also a null-measurable set under the product measure of `μ` and the Lebesgue measure. In other words, the region between two a.e.-measurable functions on a null-measurable set is itself null-measurable.
More concisely: Given measurable spaces `α` and a measure `μ` on `α`, if `f` and `g` are almost everywhere (a.e.)-measurable functions from `α` to the real numbers and `s` is a null-measurable set, then the set of pairs `(x, y)` with `x` in `s` and `f(x) < y < g(x)` is null-measurable under the product measure of `μ` and the Lebesgue measure.
|
measurableSet_region_between_oc
theorem measurableSet_region_between_oc :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f g : α → ℝ} {s : Set α},
Measurable f → Measurable g → MeasurableSet s → MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)}
This theorem states that for any measurable space `α`, any two measurable functions `f` and `g` from `α` to the real numbers, and any measurable set `s` within `α`, the set of points `p` such that the first component of `p` is in `s` and the second component of `p` is in the left-open right-closed interval between `f(p.1)` and `g(p.1)` is also a measurable set. In other words, the region between the graphs of two measurable functions over a measurable set is itself measurable, including the graph of the upper function.
More concisely: The set of points in a measurable space with measurable functions to the real numbers, where the first component is in a measurable set and the second component is between the function values, is itself measurable.
|
Real.map_linearMap_volume_pi_eq_smul_volume_pi
theorem Real.map_linearMap_volume_pi_eq_smul_volume_pi :
∀ {ι : Type u_1} [inst : Fintype ι] {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ},
LinearMap.det f ≠ 0 →
MeasureTheory.Measure.map (⇑f) MeasureTheory.volume =
ENNReal.ofReal |(LinearMap.det f)⁻¹| • MeasureTheory.volume
This theorem states that for any invertible linear map `f` from a vector space (over real numbers) indexed by some finite type `ι` to itself, the pushforward of the Lebesgue measure (also known as `MeasureTheory.volume`) under this map is equal to the Lebesgue measure rescaled by the absolute value of the inverse of the determinant of `f`. In other words, given a linear transformation, it will scale the volume of any measurable set by the absolute value of its determinant's reciprocal. If the determinant of the linear map is non-zero (which makes the map invertible), the measure transform (or pushforward) of the Lebesgue measure via this map is equivalent to the Lebesgue measure scaled by this factor. Note that the measure is expressed in terms of non-negative extended real numbers (`ENNReal`), and the absolute value of the inverse determinant is treated as such.
More concisely: For any invertible linear map `f` from a real vector space to itself, the pushforward of the Lebesgue measure is equal to the rescaled Lebesgue measure with factor abs(det(f)^(-1)).
|
measurableSet_region_between_cc
theorem measurableSet_region_between_cc :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f g : α → ℝ} {s : Set α},
Measurable f → Measurable g → MeasurableSet s → MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)}
This theorem states that for any measurable space `α`, any two measurable functions `f` and `g` from `α` to real numbers, and any measurable set `s` in `α`, the region between the graphs of `f` and `g` over the set `s` is also measurable. Here, the region between the graphs of `f` and `g` is defined as the set of points `(x, y)` such that `x` is in `s` and `y` lies in the closed interval from `f(x)` to `g(x)`, inclusive.
More concisely: For any measurable spaces `α`, measurable functions `f` and `g` from `α` to real numbers, and measurable set `s` in `α`, the set of points `(x, y)` with `x` in `s` and `y` between `f(x)` and `g(x)` forms a measurable subset of the product measurable space `α × ℝ`.
|
measurableSet_region_between_co
theorem measurableSet_region_between_co :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f g : α → ℝ} {s : Set α},
Measurable f → Measurable g → MeasurableSet s → MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ico (f p.1) (g p.1)}
This theorem states that the region between two measurable functions on a measurable set is also measurable. More specifically, if we have two measurable functions `f` and `g` mapping from a type `α` to real numbers, and a measurable set `s` of type `α`, then the set of pairs `p` where the first element of `p` is in `s` and the second element of `p` is in the left-closed right-open interval between `f(p.1)` and `g(p.1)`, is also a measurable set. This can be seen as a version of the theorem which includes the graph of the lower function `f`. The measurability of the functions and the set ensures that we can perform meaningful measure-theoretic operations on them.
More concisely: If `f` and `g` are measurable functions from a measurable set `s` in `α` to real numbers, then the set of pairs `{(x, y) | x ∈ s ∧ f x ≤ y < g x}` is measurable.
|
nullMeasurableSet_region_between_oc
theorem nullMeasurableSet_region_between_oc :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ},
AEMeasurable f μ →
AEMeasurable g μ →
∀ {s : Set α},
MeasureTheory.NullMeasurableSet s μ →
MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)}
(μ.prod MeasureTheory.volume)
The theorem `nullMeasurableSet_region_between_oc` states that, given a measurable space `α` and a measure `μ` on that space, if we have two almost everywhere measurable functions `f` and `g` from `α` to the real numbers, along with a set `s` that is null measurable with respect to `μ`, then the set of pairs `p` such that the first element of `p` is in `s` and the second element of `p` is in the open-closed interval between `f(p.1)` and `g(p.1)` (i.e., greater than `f(p.1)` and less than or equal to `g(p.1)`) is also null measurable with respect to the product of `μ` and Lebesgue measure. This theorem is a version of the statement about null measurability of the region between two almost everywhere measurable functions, extended to include the graph of the upper function.
More concisely: Given a measurable space `(α, Σ, μ)` and almost everywhere measurable functions `f, g: α → ℝ`, if `s ⊆ α` is null measurable, then the set `{ (x, y) ∈ s × ℝ : f(x) ≤ y ≤ g(x) }` is null measurable with respect to the product measure μ × Lebesgue measure.
|
Real.volume_eq_stieltjes_id
theorem Real.volume_eq_stieltjes_id : MeasureTheory.volume = StieltjesFunction.id.measure
The theorem `Real.volume_eq_stieltjes_id` states that the volume on the real number line, which is a specific case of the volume on a finite-dimensional inner product space, is identical to the Stieltjes measure that is derived from the identity function.
More concisely: The volume of integration with respect to the Lebesgue measure on the real line is equal to the Stieltjes measure induced by the identity function.
|
Real.volume_Ico
theorem Real.volume_Ico : ∀ {a b : ℝ}, ↑↑MeasureTheory.volume (Set.Ico a b) = ENNReal.ofReal (b - a)
The `Real.volume_Ico` theorem states that for any pair of real numbers `a` and `b`, the measure (or "volume") of the left-closed right-open interval from `a` to `b` is equal to the extended non-negative real number representation of the difference `(b - a)`. In simpler terms, the length of the interval from `a` to `b` (where `a` is included and `b` is excluded) is equal to the absolute difference between `b` and `a`. This is subject to the condition that if the difference `(b - a)` is negative, it's considered as `0`.
More concisely: The volume of the left-closed right-open real interval [a, b) is equal to the absolute difference b - a.
|
nullMeasurableSet_region_between_cc
theorem nullMeasurableSet_region_between_cc :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ},
AEMeasurable f μ →
AEMeasurable g μ →
∀ {s : Set α},
MeasureTheory.NullMeasurableSet s μ →
MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)}
(μ.prod MeasureTheory.volume)
This theorem states that for any two almost everywhere (a.e.) measurable functions `f` and `g` on a space `α` equipped with a measurable space structure and a measure `μ`, if a set `s` in `α` is null-measurable with respect to `μ`, then the set of all points `p` such that the first component of `p` belongs to `s` and the second component belongs to the closed interval between `f` and `g` evaluated at the first component of `p`, is also null-measurable with respect to the product measure of `μ` and the Lebesgue measure. In simpler terms, it asserts that the region between two a.e. measurable functions on a null-measurable set is also null-measurable, including the graphs of both functions.
More concisely: If `f` and `g` are almost everywhere measurable functions on the measurable space `(α, μ)`, and `s ⊆ α` is null-measurable, then the set of points `(x, y)` with `x ∈ s` and `y ∈ [f x, g x]` is null-measurable with respect to the product measure of `μ` and the Lebesgue measure.
|
Mathlib.MeasureTheory.Measure.Lebesgue.Basic._auxLemma.10
theorem Mathlib.MeasureTheory.Measure.Lebesgue.Basic._auxLemma.10 : ∀ {b a : Prop}, (∃ (_ : a), b) = (a ∧ b)
This theorem from Measure Theory in Mathlib (a library for the Lean Theorem Prover) states that for any two propositions `a` and `b`, the statement "there exists an instance where `a` is true such that `b` is also true" is equivalent to the statement "`a` is true and `b` is true". This establishes an equivalence between two different ways of expressing a joint assertion in logic.
More concisely: The theorem asserts that for all propositions `a` and `b`, the existence of an instance where `a` and `b` both hold is equivalent to `a` and `b` both holding.
|
Real.volume_Icc_pi
theorem Real.volume_Icc_pi :
∀ {ι : Type u_1} [inst : Fintype ι] {a b : ι → ℝ},
↑↑MeasureTheory.volume (Set.Icc a b) = Finset.univ.prod fun i => ENNReal.ofReal (b i - a i)
This theorem, `Real.volume_Icc_pi`, states that for every finite type ι, and for any two functions `a` and `b` that map from this type to the set of real numbers, the measure (or "volume") of the closed interval from `a` to `b` in the real line (as given by `Set.Icc a b`) is equal to the product, over all elements of the universe of the type ι, of the nonnegative part of the difference between the value of `b` and `a` at each element (as given by `ENNReal.ofReal (b i - a i)`). In simpler terms, it calculates the "volume" of a multidimensional box, where the box's dimensions are specified by the differences between the values of `b` and `a` at each point in ι.
More concisely: The volume of a closed real interval with endpoints given by functions mapping from a type ι to the real numbers is equal to the product of the nonnegative differences between the function values at each index in ι.
|
Real.volume_Ioi
theorem Real.volume_Ioi : ∀ {a : ℝ}, ↑↑MeasureTheory.volume (Set.Ioi a) = ⊤
The theorem `Real.volume_Ioi` states that for any real number `a`, the Lebesgue measure (or "volume") of the set of all real numbers greater than `a` (denoted by `Set.Ioi a`), is infinite. This is symbolized in Lean 4 by `⊤`. In other words, the size of any interval that begins at a real number and extends infinitely to the right is always considered to be infinite.
More concisely: The Lebesgue measure of the set of real numbers strictly greater than a real number `a` is infinite.
|
Real.volume_val
theorem Real.volume_val : ∀ (s : Set ℝ), ↑↑MeasureTheory.volume s = ↑↑StieltjesFunction.id.measure s
This theorem states that for any set `s` of real numbers, the measure of `s` under the Lebesgue measure (denoted by `MeasureTheory.volume s`) is equal to the measure of `s` under the measure associated with the identity Stieltjes function. In mathematical terms, this could be written as: for all subsets `s` of ℝ, the Lebesgue measure of `s` equals the measure of `s` given by the Stieltjes function associated with the identity function on ℝ.
More concisely: For any set `s` of real numbers, the Lebesgue measure of `s` equals the measure of `s` with respect to the Stieltjes integral using the identity function.
|
measurableSet_regionBetween
theorem measurableSet_regionBetween :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f g : α → ℝ} {s : Set α},
Measurable f → Measurable g → MeasurableSet s → MeasurableSet (regionBetween f g s)
This theorem states that the region between two measurable functions on a measurable set is also measurable. Here, a function is defined as measurable if the preimage of every measurable set under that function is also measurable. The region between two real-valued functions, `f` and `g`, on a set `s` is defined as the set of pairs `(x, y)` where `x` is in `s` and `y` lies strictly between `f(x)` and `g(x)`. In other words, if `f` and `g` are measurable functions and `s` is a measurable set, then the set of all points `(x, y)` such that `x` is in `s` and `f(x) < y < g(x)` is a measurable set.
More concisely: If `f` and `g` are measurable functions on a measurable set `s` with `f(x) ≤ g(x)` for all `x` in `s`, then the set of pairs `(x, y)` in `s × ℝ` with `f(x) < y < g(x)` is a measurable subset of `s × ℝ`.
|
volume_regionBetween_eq_lintegral
theorem volume_regionBetween_eq_lintegral :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} {s : Set α}
[inst_1 : MeasureTheory.SigmaFinite μ],
AEMeasurable f (μ.restrict s) →
AEMeasurable g (μ.restrict s) →
MeasurableSet s →
↑↑(μ.prod MeasureTheory.volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ENNReal.ofReal ((g - f) y) ∂μ
The theorem `volume_regionBetween_eq_lintegral` states that for a measurable space `α`, a measure `μ` on `α`, two real-valued functions `f` and `g` that are almost everywhere measurable with respect to the measure `μ` restricted to a set `s`, and a set `s` that is measurable, if `μ` is sigma-finite, then the measure of the region between `f` and `g` over the set `s` (in the product measure space of `μ` and Lebesgue measure) is equal to the Lebesgue integral over `s` of the non-negative part of the difference between `g` and `f`. In mathematical terms, it's saying that the volume of the region between two functions can be calculated as an integral of the difference between the two functions.
More concisely: For a sigma-finite measure `μ` on a measurable space `α`, the volume of the region between almost everywhere measurable functions `f` and `g` over a measurable set `s` equals the Lebesgue integral over `s` of the positive part of `g - f`.
|
Real.volume_Ioo
theorem Real.volume_Ioo : ∀ {a b : ℝ}, ↑↑MeasureTheory.volume (Set.Ioo a b) = ENNReal.ofReal (b - a)
This theorem, named `Real.volume_Ioo`, states that for any two real numbers `a` and `b`, the measure (think of this as the "volume" in a one-dimensional sense) of the open interval (excluding `a` and `b`) between `a` and `b` is equal to the nonnegative real part of the difference between `b` and `a`. In mathematical terms, this means that the Lebesgue measure of the interval $(a, b)$, denoted by $\mu((a, b))$, is equal to max$(b - a, 0)$. If `b` is greater than `a`, it is just `b - a`; otherwise, it is `0`.
More concisely: The Lebesgue measure of the open real interval $(a, b)$ is equal to the non-negative difference between $b$ and $a$.
|
measurableSet_graph
theorem measurableSet_graph :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℝ}, Measurable f → MeasurableSet {p | p.2 = f p.1}
The theorem `measurableSet_graph` states that for any type `α` with a measurable space structure and any measurable function `f` from `α` to the real numbers ℝ, the graph of `f` is a measurable set. In other words, the set of all pairs `(x, y)` such that `y = f(x)` is a measurable set. Here, the term "measurable" refers to the function `f` satisfying the property that the preimage of any measurable set is also a measurable set.
More concisely: If `α` is a type with a measurable space structure and `f` is a measurable function from `α` to ℝ, then the graph of `f` is a measurable set.
|
nullMeasurableSet_region_between_co
theorem nullMeasurableSet_region_between_co :
∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ},
AEMeasurable f μ →
AEMeasurable g μ →
∀ {s : Set α},
MeasureTheory.NullMeasurableSet s μ →
MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ico (f p.1) (g p.1)}
(μ.prod MeasureTheory.volume)
The theorem `nullMeasurableSet_region_between_co` states that for any measurable space `α` and a measure `μ` on that space, if we have two almost everywhere measurable functions `f` and `g` from `α` to real numbers `ℝ`, and a set `s` in `α` that is null measurable with respect to the measure `μ`, then the set of all ordered pairs `(p.1, p.2)` such that `p.1` is in `s` and `p.2` is in the left-closed right-open interval between `f(p.1)` and `g(p.1)` is also null measurable with respect to the product measure of `μ` and Lebesgue measure. In other words, the region between the graphs of two almost everywhere measurable functions on a null measurable set is null measurable, where the region includes the graph of the lower function.
More concisely: If `μ` is a measure on the measurable space `α`, `f` and `g` are almost everywhere measurable functions from `α` to `ℝ`, and `s` is a null measurable set in `α` with respect to `μ`, then the set of ordered pairs `(x, y)` where `x` is in `s` and `y` is in the left-closed right-open interval between `f(x)` and `g(x)` is null measurable with respect to the product measure of `μ` and Lebesgue measure.
|
Real.smul_map_diagonal_volume_pi
theorem Real.smul_map_diagonal_volume_pi :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {D : ι → ℝ},
(Matrix.diagonal D).det ≠ 0 →
ENNReal.ofReal |(Matrix.diagonal D).det| •
MeasureTheory.Measure.map (⇑(Matrix.toLin' (Matrix.diagonal D))) MeasureTheory.volume =
MeasureTheory.volume
The theorem `Real.smul_map_diagonal_volume_pi` states that for a given non-zero diagonal matrix defined over real numbers, the measure obtained by rescaling the Lebesgue measure according to the absolute value of the determinant of the diagonal matrix and then mapping it via the linear equivalence represented by the diagonal matrix is equal to the original Lebesgue measure. This result is a special case of the theorem `Real.map_matrix_volume_pi_eq_smul_volume_pi`, which should be used in general. The proof of the general case makes use of this particular case.
More concisely: For a non-zero real diagonal matrix, the Lebesgue measure of a set is equal to the rescaled Lebesgue measure obtained by multiplying the original measure by the absolute value of the determinant and applying the linear transformation represented by the diagonal matrix.
|
Real.map_matrix_volume_pi_eq_smul_volume_pi
theorem Real.map_matrix_volume_pi_eq_smul_volume_pi :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {M : Matrix ι ι ℝ},
M.det ≠ 0 →
MeasureTheory.Measure.map (⇑(Matrix.toLin' M)) MeasureTheory.volume =
ENNReal.ofReal |M.det⁻¹| • MeasureTheory.volume
This theorem states that for any invertible matrix `M` which is a square matrix (same number of rows and columns) with real number entries and whose indices are drawn from an arbitrary type `ι` (with a finite number of elements and a decidable equality relation), the Lebesgue measure (denoted by `MeasureTheory.volume`) gets rescaled when pushed forward through the linear transformation associated with the matrix (given by the function `Matrix.toLin' M`). The rescaling factor is given by the absolute value of the reciprocal of the determinant of the matrix (`|M.det⁻¹|`). In other words, the measure of any subset of the real numbers is multiplied by `|M.det⁻¹|` under the map `Matrix.toLin' M`. The condition `M.det ≠ 0` ensures that the matrix `M` is invertible, or equivalently, that the associated linear transformation is a bijection, which is crucial for the result to hold.
More concisely: For any invertible square matrix M with real number entries and finite index type ι, the Lebesgue measure is multiplied by the absolute value of the reciprocal of the determinant when pushed forward through the linear transformation associated with M.
|
Mathlib.MeasureTheory.Measure.Lebesgue.Basic._auxLemma.9
theorem Mathlib.MeasureTheory.Measure.Lebesgue.Basic._auxLemma.9 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋃ i, s i) = ∃ i, x ∈ s i
This theorem is about the membership of elements in a union of sets. It states that: for any type `α`, any indexing type `ι`, any element `x` of type `α`, and any indexed family of sets `s` of type `ι → Set α`, an element `x` belongs to the union over `i` of the sets `s i` if and only if there exists an index `i` such that `x` belongs to `s i`. In mathematical notation, this theorem states that
\[ x \in \bigcup_{i} s_{i} \iff \exists i, x \in s_{i}. \]
This is a fundamental result in set theory, expressing that an element belongs to a union of sets exactly when it belongs to at least one of the sets.
More concisely: An element belongs to the union of a family of sets if and only if it is an element of at least one set in the family.
|
ae_restrict_of_ae_restrict_inter_Ioo
theorem ae_restrict_of_ae_restrict_inter_Ioo :
∀ {μ : MeasureTheory.Measure ℝ} [inst : MeasureTheory.NoAtoms μ] {s : Set ℝ} {p : ℝ → Prop},
(∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Set.Ioo a b), p x) →
∀ᵐ (x : ℝ) ∂μ.restrict s, p x
The theorem, `ae_restrict_of_ae_restrict_inter_Ioo`, states that for any measure `μ` on the set of real numbers (with no atoms), a set `s` of real numbers, and a property `p` defined on the real numbers. If, for all `a` and `b` in `s` with `a` less than `b`, the property `p` holds almost everywhere (i.e., except on a set of measure zero) in the intersection of `s` and the open interval from `a` to `b` (denoted as `(a, b)`), then `p` also holds almost everywhere in `s`. This theorem is formulated with the restriction of the measure `μ` to the mentioned sets. This theorem is a variation of another theorem `ae_of_mem_of_ae_of_mem_inter_Ioo`.
More concisely: If `μ` is a measure on the real numbers with no atoms, `s` is a set of real numbers, and for all `a` and `b` in `s` with `a < b`, property `p` holds almost everywhere in `s ∩ (a, b)`, then `p` holds almost everywhere in `s`.
|
Real.volume_Ioc
theorem Real.volume_Ioc : ∀ {a b : ℝ}, ↑↑MeasureTheory.volume (Set.Ioc a b) = ENNReal.ofReal (b - a)
This theorem, named `Real.volume_Ioc`, states that for any two real numbers `a` and `b`, the measure (in terms of Lebesgue measure, sometimes referred to as "volume") of the interval that is open on the left and closed on the right, denoted as `(a, b]` (or `Set.Ioc a b` in Lean), is equivalent to the non-negative part of the difference `b - a`. This non-negative part is computed by the function `ENNReal.ofReal`, which returns `b - a` if it is a non-negative number, and `0` otherwise. In mathematical terms, it is saying that the measure of the interval (a, b] is max{b - a, 0}.
More concisely: The Lebesgue measure of the interval (a, b] equals the non-negative value of b - a.
|
Real.volume_preserving_transvectionStruct
theorem Real.volume_preserving_transvectionStruct :
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (t : Matrix.TransvectionStruct ι ℝ),
MeasureTheory.MeasurePreserving (⇑(Matrix.toLin' t.toMatrix)) MeasureTheory.volume MeasureTheory.volume
This theorem, `Real.volume_preserving_transvectionStruct`, asserts that a transvection preserves Lebesgue measure. In more detail, for any finite type `ι` with decidable equality and any transvection structure `t` over `ι` with real coefficients, the linear transformation represented by the matrix of `t` (when acting on real-valued functions on `ι`) preserves the Lebesgue measure. This is expressed by stating that the measure of the preimage of any set under this transformation, as per the Lebesgue measure, is the same as the measure of the set itself.
More concisely: A transvection with real coefficients, represented by a matrix over a finite type with decidable equality, preserves Lebesgue measure, i.e., the measure of the preimage of a set under this transformation equals the measure of the set.
|
ae_of_mem_of_ae_of_mem_inter_Ioo
theorem ae_of_mem_of_ae_of_mem_inter_Ioo :
∀ {μ : MeasureTheory.Measure ℝ} [inst : MeasureTheory.NoAtoms μ] {s : Set ℝ} {p : ℝ → Prop},
(∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Set.Ioo a b → p x) → ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
The theorem `ae_of_mem_of_ae_of_mem_inter_Ioo` states that for any measure `μ` on the real numbers which has no atoms, any set `s` of real numbers, and any property `p` defined for real numbers, if the property `p` holds almost everywhere in the intersection of the set `s` and the open interval `(a, b)` for all `a` and `b` in `s` with `a < b`, then the property `p` also holds almost everywhere in the set `s`. The term "almost everywhere" is understood in the sense of measure theory: a property holds almost everywhere if the set of points where it fails to hold has measure zero.
More concisely: If a property holds almost everywhere in the intersection of a set and every open subinterval, then it holds almost everywhere in the set (in the sense of measure theory).
|