ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot
theorem ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ} (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α),
Filter.Tendsto (↑(hf.stieltjesFunction a)) Filter.atBot (nhds 0)
This theorem states that, for any measurable space α and a function `f : α → ℚ → ℝ` that has the `IsMeasurableRatCDF` property, if we extend `f` from rational numbers to real numbers to obtain a Stieltjes function, then this Stieltjes function tends towards negative infinity and converges to zero. In other words, as we consider smaller and smaller values in the domain of the Stieltjes function, the function values get arbitrarily close to zero. This is expressed formally as the function `f` being continuous from the bottom (`Filter.atBot`) towards a neighborhood of zero (`nhds 0`).
More concisely: Given a measurable space α and a measurable function `f : α → ℚ → ℝ` with the `IsMeasurableRatCDF` property, its extended Stieltjes function is continuous from below towards zero.
|
ProbabilityTheory.IsMeasurableRatCDF.nonneg
theorem ProbabilityTheory.IsMeasurableRatCDF.nonneg :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ},
ProbabilityTheory.IsMeasurableRatCDF f → ∀ (a : α) (q : ℚ), 0 ≤ f a q
This theorem states that for any measurable space `α` and any function `f` from `α` to the set of rational numbers `ℚ` and then to real numbers `ℝ`, if `f` is a measurable rational cumulative distribution function (`IsMeasurableRatCDF`), then the output of `f` for any `α` and `ℚ` is always non-negative. In other words, the value of the rational cumulative distribution function at any point is always greater than or equal to zero.
More concisely: For any measurable space `α` and measurable rational cumulative distribution function `f` from `α` to the rational numbers `ℚ` and then to real numbers `ℝ`, `f(x) ≥ 0` for all `x ∈ α`.
|
ProbabilityTheory.isMeasurableRatCDF_toRatCDF
theorem ProbabilityTheory.isMeasurableRatCDF_toRatCDF :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ},
Measurable f → ProbabilityTheory.IsMeasurableRatCDF (ProbabilityTheory.toRatCDF f)
The theorem `ProbabilityTheory.isMeasurableRatCDF_toRatCDF` states that for any measurable space `α` and any function `f` from `α` to the set of real-valued functions on rational numbers, if `f` is measurable, then the function obtained by transforming `f` using the `ProbabilityTheory.toRatCDF` function, which replaces `f(a)` by a default function if `f(a)` does not satisfy the property `IsRatStieltjesPoint`, is also measurable in the sense of the `ProbabilityTheory.IsMeasurableRatCDF` definition.
More concisely: If `f` is a measurable real-valued function on a measurable space, then the function obtained by applying `ProbabilityTheory.toRatCDF` to `f` is also measurable as a real-valued function on rational numbers according to the `ProbabilityTheory.IsMeasurableRatCDF` definition.
|
ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_univ
theorem ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_univ :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ} (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α),
↑↑(hf.stieltjesFunction a).measure Set.univ = 1
This theorem states that for any measurable space 'α' and a function 'f' from 'α' to the real numbers that has the 'IsMeasurableRatCDF' property, when we extend 'f' to a Stieltjes function and subsequently associate a measure to it, the measure of the universal set (i.e., the set of all elements of 'α') is always equal to 1. In simple terms, this theorem asserts that the total probability of all events in our measurable space under this specific construction of a measure is 1, reflecting a fundamental property of probability measures.
More concisely: For any measurable space 'α' and a measurable function 'f' from 'α' to the real numbers with 'IsMeasurableRatCDF' property, the measure of the universal set induced by the associated Stieltjes measure of 'f' is equal to 1.
|
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq
theorem ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ} (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α)
(r : ℚ), ↑(hf.stieltjesFunction a) ↑r = f a r
This theorem states that for any given measurable space `α`, and a function `f` from `α` to the set of real numbers parameterized by rational numbers, if `f` satisfies the property `IsMeasurableRatCDF`, then the Stieltjes function obtained by extending `f` from rational numbers to real numbers produces the same output as `f` for every `α` and rational number input. More formally, for every `α` in `α`, and rational number `r`, the value of the Stieltjes function at `r` is equal to `f(α, r)`.
More concisely: For any measurable space `α` and measurable function `f` from `α` to the real numbers parameterized by rational numbers, satisfying `IsMeasurableRatCDF`, the extended Stieltjes function of `f` equals `f` itself for every `α` in `α` and rational number `r`.
|
ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction
theorem ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction :
∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ} (hf : ProbabilityTheory.IsMeasurableRatCDF f) (x : ℝ),
Measurable fun a => ↑(hf.stieltjesFunction a) x
The theorem `ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction` states that for any measurable space `α`, and any rational function `f : α → ℚ → ℝ` that satisfies the `IsMeasurableRatCDF` property, for any real number `x`, the function that maps each `α` to the `x`-th value of the Stieltjes function associated with `f` (obtained through `ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction`) is measurable. This means the preimage of every measurable set under this function is a measurable set. The `IsMeasurableRatCDF` property ensures that `f` is a measurable function from the rational numbers to the real numbers.
More concisely: For any measurable space `α` and measurable function `f : α → ℚ → ℝ` satisfying the `IsMeasurableRatCDF` property, the function that maps each `x ∈ ℝ` to the `x`-th value of the Stieltjes function associated with `f` is measurable.
|
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def
theorem ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def :
∀ {α : Type u_4} (f : α → ℚ → ℝ) (a : α) (x : ℝ),
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux f a x = ⨅ q, f a ↑q
This theorem states that for any type `α`, for any function `f` from `α` to rational numbers to real numbers, and for any elements `a` of `α` and `x` of real numbers, the operation of `IsMeasurableRatCDF.stieltjesFunctionAux` applied to `f`, `a`, and `x` is equal to the infimum of applying `f` to `a` and the real number representation of a rational number `q`. In more informal terms, it asserts that the stieltjesFunctionAux operation extracts the smallest value of `f` over all rational numbers greater than `x` for a fixed `a`.
More concisely: For any type `α`, any function `f` from `α` to rational numbers to real numbers, and any `a` of type `α` and `x` of type real, the value of `IsMeasurableRatCDF.stieltjesFunctionAux` on `f`, `a`, and `x` equals the infimum of `f a` and the real number representation of the greatest rational number `q` less than or equal to `x`.
|