Mathlib.MeasureTheory.Measure.Stieltjes._auxLemma.9
theorem Mathlib.MeasureTheory.Measure.Stieltjes._auxLemma.9 :
∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (¬a < b) = (b ≤ a)
This theorem is from the Measure Theory library in Mathlib. Specifically, it's a lemma about Stieltjes measures. It states that for any type `α` with a linear order, and any two elements `a` and `b` of type `α`, the statement "`a` is not less than `b`" is equivalent to the statement "`b` is less than or equal to `a`". In mathematical terms, it says that ∀ `a`, `b` in `α`, ¬(`a` < `b`) ⇔ `b` ≤ `a`.
More concisely: For any linearly ordered type `α`, the negation of `a` being less than `b` is equivalent to `b` being less than or equal to `a`.
|
StieltjesFunction.measure_Ioo
theorem StieltjesFunction.measure_Ioo :
∀ (f : StieltjesFunction) {a b : ℝ}, ↑↑f.measure (Set.Ioo a b) = ENNReal.ofReal (Function.leftLim (↑f) b - ↑f a)
The theorem `StieltjesFunction.measure_Ioo` states that for any Stieltjes Function `f` and for any real numbers `a` and `b`, the measure of the open interval `(a, b)` with respect to `f` is equal to the extended non-negative real value of the difference of the left limit of `f` at `b` and the value of `f` at `a`. The Stieltjes Function is a type of measure which gives the mass `f b - f a` to the interval `(a, b]`. The interval `(a, b)` is defined as the set of all real numbers `x` such that `a < x < b`. The function `ENNReal.ofReal` returns the non-negative real part of a real number.
More concisely: For any Stieltjes Function `f` and real numbers `a < b`, the measure of the open interval `(a, b)` with respect to `f` equals the non-negative real value of `(f a) - (f b)`.
|
StieltjesFunction.measure_singleton
theorem StieltjesFunction.measure_singleton :
∀ (f : StieltjesFunction) (a : ℝ), ↑↑f.measure {a} = ENNReal.ofReal (↑f a - Function.leftLim (↑f) a)
This theorem states that for any StieltjesFunction `f` and any real number `a`, the measure of the set containing only `a` according to the measure associated with `f` is equal to the extended non-negative real value of the difference between the value of `f` at `a` and the left limit of `f` at `a`. In other words, the Stieltjes measure of a singleton set `{a}` is the non-negative difference between the function value at a point `a` and its left limit at this point.
More concisely: For any Stieltjes function `f` and real number `a`, the measure of the singleton set `{a}` according to `f` equals the non-negative difference between `f`'s value at `a` and its left limit at `a`.
|
StieltjesFunction.measure_Ioc
theorem StieltjesFunction.measure_Ioc :
∀ (f : StieltjesFunction) (a b : ℝ), ↑↑f.measure (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)
This theorem states that for any Stieltjes function `f` and any two real numbers `a` and `b`, the measure of the interval `(a, b]` under this function is equal to the nonnegative real part of the difference `f(b) - f(a)`. In other words, it is associating a measure to the interval `(a, b]` that corresponds to the difference in the values of `f` at `b` and `a`, with the measure being `0` if this difference is negative. The function `f` essentially maps an interval of real numbers to a measure, and this theorem gives the rule for how it does this.
More concisely: For any Stieltjes function `f` and real numbers `a` and `b` with `b > a`, the measure of the interval `(a, b]` under `f` equals the nonnegative real part of `(f(b) - f(a))`.
|
StieltjesFunction.length_subadditive_Icc_Ioo
theorem StieltjesFunction.length_subadditive_Icc_Ioo :
∀ (f : StieltjesFunction) {a b : ℝ} {c d : ℕ → ℝ},
Set.Icc a b ⊆ ⋃ i, Set.Ioo (c i) (d i) →
ENNReal.ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ENNReal.ofReal (↑f (d i) - ↑f (c i))
This theorem states that if a compact interval `[a, b]` is covered by a union of open intervals `(c i, d i)`, then the difference `f b - f a` is less than or equal to the sum of the differences `f (d i) - f (c i)`, where `f` is a StieltjesFunction. Here, the intervals and the differences are considered in the extended non-negative real numbers (`ENNReal`) and the real numbers are converted to `ENNReal` using the `ofReal` function, which returns `x` if it is nonnegative and `0` otherwise. This theorem is a technical tool used in proving the same statement for half-open intervals, with the key point of this theorem being that one can take advantage of compactness to reduce it to a finite sum and subsequently argue by induction on the size of the covering set.
More concisely: If a compact interval [a, b] is covered by a union of open intervals (ci, di), where ci and di are real numbers, then the difference between the Stieltjes integrals of a Stieltjes function f over [a, b] and [a, b] with respect to an increasing function g is less than or equal to the sum of the differences between the Stieltjes integrals of f over (ci, di) and (ci, di) with respect to g.
|
StieltjesFunction.mono
theorem StieltjesFunction.mono : ∀ (f : StieltjesFunction), Monotone ↑f
The theorem `StieltjesFunction.mono` states that for every Stieltjes function `f`, the function `f` is monotone. In other words, if `a ≤ b` for any real numbers `a` and `b`, then `f(a) ≤ f(b)`. This property is essential in many mathematical contexts, for instance in probability theory where Stieltjes functions often represent distribution functions of random variables, which must be non-decreasing.
More concisely: For every Stieltjes function `f`, if `a ≤ b` are real numbers then `f(a) ≤ f(b)`.
|
Mathlib.MeasureTheory.Measure.Stieltjes._auxLemma.15
theorem Mathlib.MeasureTheory.Measure.Stieltjes._auxLemma.15 :
∀ {p q : ℝ}, 0 ≤ p → 0 ≤ q → ENNReal.ofReal p + ENNReal.ofReal q = ENNReal.ofReal (p + q)
This theorem, from the Measure Theory module in Mathlib, states that for any two real numbers `p` and `q` that are both nonnegative, the function `ENNReal.ofReal` (which returns the input if it is nonnegative, otherwise returns `0`) preserves addition. In mathematical terms, applying the `ENNReal.ofReal` function to the sum of `p` and `q` (`p + q`) gives the same result as individually applying `ENNReal.ofReal` to `p` and `q` and then adding those results.
More concisely: For all nonnegative real numbers `p` and `q`, `ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q`.
|
StieltjesFunction.iInf_rat_gt_eq
theorem StieltjesFunction.iInf_rat_gt_eq : ∀ (f : StieltjesFunction) (x : ℝ), ⨅ r, ↑f ↑↑r = ↑f x
This theorem states that for any Stieltjes function 'f' and any real number 'x', the infimum (greatest lower bound) of the values of 'f' on the set of rational numbers 'r' is equal to the value of 'f' at 'x'. In other words, for all Stieltjes functions and real numbers, the function value at that real number is the lowest possible value that the function can take on the rationals.
More concisely: For any Stieltjes function `f` and real number `x`, the infimum of `f` over rational numbers equals `f`(x).
|
StieltjesFunction.id_leftLim
theorem StieltjesFunction.id_leftLim : ∀ (x : ℝ), Function.leftLim (↑StieltjesFunction.id) x = x
The theorem `StieltjesFunction.id_leftLim` states that for all real numbers `x`, the left limit of the Stieltjes function constructed from the identity function (denoted as `StieltjesFunction.id`) at `x` is equal to `x`. In other words, if we approach any real number `x` from the left via this Stieltjes function, the limit value we obtain is exactly `x`.
More concisely: For all real numbers x, the left limit of StieltjesFunction.id at x equals x.
|
StieltjesFunction.measure_Iic
theorem StieltjesFunction.measure_Iic :
∀ (f : StieltjesFunction) {l : ℝ},
Filter.Tendsto (↑f) Filter.atBot (nhds l) → ∀ (x : ℝ), ↑↑f.measure (Set.Iic x) = ENNReal.ofReal (↑f x - l)
The theorem `StieltjesFunction.measure_Iic` states that for any Stieltjes function `f` and any real number `l`, if `f` tends to `l` as we go to negative infinity (meaning that for any neighborhood of `l`, there is a sufficiently large negative number such that the function values in the interval extending from this negative number to infinity are all in this neighborhood), then for any real number `x`, the measure associated to `f` of the interval from negative infinity to `x` (inclusive) is equal to the non-negative part of `f(x) - l`. This theorem basically describes how the measure of an interval under a Stieltjes function behaves as the function tends to a limit at negative infinity.
More concisely: For any Stieltjes function `f` and real number `l`, if `f(x)` approaches `l` as `x` approaches negative infinity, then the measure of the interval from negative infinity to `x` under `f` equals `max(0, f(x) - l)`.
|
StieltjesFunction.measure_univ
theorem StieltjesFunction.measure_univ :
∀ (f : StieltjesFunction) {l u : ℝ},
Filter.Tendsto (↑f) Filter.atBot (nhds l) →
Filter.Tendsto (↑f) Filter.atTop (nhds u) → ↑↑f.measure Set.univ = ENNReal.ofReal (u - l)
This theorem states that for any Stieltjes function `f` and real numbers `l` and `u`, if `f` tends to `l` as the input approaches negative infinity (represented by `Filter.atBot`) and `f` tends to `u` as the input approaches positive infinity (represented by `Filter.atTop`), then the measure of the universal set (which includes all real numbers) according to the measure defined by `f` is equal to the extended non-negative real value of `(u - l)`. In other words, provided the limit conditions for `f`, the total "mass" or measure over all real numbers as per the Stieltjes function is just the difference between the limits at positive and negative infinity.
More concisely: For any Stieltjes function `f`, if `f` has finite limits `l` as the input approaches negative infinity and `u` as the input approaches positive infinity, then the integral of `f` over the real numbers is equal to `u - l`.
|