ProbabilityTheory.set_lintegral_condCDF
theorem ProbabilityTheory.set_lintegral_condCDF :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ))
[inst : MeasureTheory.IsFiniteMeasure ρ] (x : ℝ) {s : Set α},
MeasurableSet s →
∫⁻ (a : α) in s, ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) x) ∂ρ.fst = ↑↑ρ (s ×ˢ Set.Iic x)
This theorem, named `ProbabilityTheory.set_lintegral_condCDF`, states that for any given measure `ρ` on the product space of some type `α` and the real numbers (`α × ℝ`), and for any real number `x` and a measurable set `s` of type `α`, the integral over `s` with respect to the marginal measure on `α` obtained from `ρ`, of the function that assigns to each element `a` in `s` the extended non-negative real number obtained from the conditional cumulative distribution function (CDF) at `a` and `x`, is equal to the measure `ρ` of the Cartesian product of `s` and the left-closed right-infinite interval of all real numbers less than or equal to `x`. This theorem connects the Lebesgue integral of the conditional CDF and the measure of a set in the product space.
More concisely: For measure `ρ` on `α × ℝ`, and measurable set `s` in `α`, the integral of the conditional CDF with respect to the marginal measure on `α` over `s` equals the measure of `s` times the length of the interval `[-\infty, x]` for any real number `x`.
|
MeasureTheory.Measure.IicSnd_le_fst
theorem MeasureTheory.Measure.IicSnd_le_fst :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ), ρ.IicSnd r ≤ ρ.fst := by
sorry
This theorem states that for any type `α` equipped with a measurable space structure `mα`, for any measure `ρ` on the product of `α` and the real numbers `ℝ`, and for any real number `r`, the measure obtained by restricting `ρ` to the set of all pairs whose second component is less than or equal to `r` (denoted by `MeasureTheory.Measure.IicSnd ρ r`), when projected onto `α`, is less than or equal to the marginal measure of `ρ` projected onto `α` (denoted by `MeasureTheory.Measure.fst ρ`). In mathematical language, it can be stated as: $\forall α, ρ, r: MeasureTheory.Measure.IicSnd(ρ, r) \leq MeasureTheory.Measure.fst(ρ)$.
More concisely: For any measure `ρ` on the product of a measurable space `α` and the real numbers `ℝ`, and for any real number `r`, the measure of the subset of `α` obtained by projecting the set where the second component is less than or equal to `r` from the product space has lesser or equal measure compared to the marginal measure on `α` from `ρ`.
|
ProbabilityTheory.condCDF_nonneg
theorem ProbabilityTheory.condCDF_nonneg :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (r : ℝ),
0 ≤ ↑(ProbabilityTheory.condCDF ρ a) r
The theorem `ProbabilityTheory.condCDF_nonneg` states that for any type `α` equipped with a measurable space structure `mα` and for any measure `ρ` on the product space `α × ℝ`, the conditional cumulative distribution function (condCDF), which is a function of `α` and `ℝ`, is non-negative for all `a : α` and `r : ℝ`. In other words, the conditional cumulative distribution function of a measure `ρ`, for any `a` in the space `α` and any real number `r`, is always greater than or equal to zero.
More concisely: For any measurable space (α, mα) and measure ρ on α × ℝ, the conditional cumulative distribution function of ρ is non-negative, i.e., ∀a:α, ∀r:ℝ, ρ.condCDF a r ≥ 0.
|
ProbabilityTheory.condCDF_le_one
theorem ProbabilityTheory.condCDF_le_one :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (x : ℝ),
↑(ProbabilityTheory.condCDF ρ a) x ≤ 1
The theorem `ProbabilityTheory.condCDF_le_one` states that for any type `α`, its associated measurable space `mα`, a measure `ρ` on the product space of `α` and the real numbers `ℝ`, and any `a` in `α` and `x` in `ℝ`, the conditional cumulative distribution function (CDF) of the measure given the value `a` on `α` is always less than or equal to 1. This aligns with the property that the cumulative distribution function of a probability measure cannot exceed 1.
More concisely: For any measurable space `(α, mα)`, measure `ρ` on `α × ℝ`, and `a ∈ α` and `x ∈ ℝ`, the conditional CDF of `ρ` given `a` satisfies `ρ(a, ∞) ≤ 1`.
|
ProbabilityTheory.measurable_condCDF
theorem ProbabilityTheory.measurable_condCDF :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (x : ℝ),
Measurable fun a => ↑(ProbabilityTheory.condCDF ρ a) x
The theorem `ProbabilityTheory.measurable_condCDF` states that for any measure `ρ` on the product space of a measurable space `α` and the real numbers, and for any real number `x`, the function which maps each element of `α` to the value at `x` of the conditional cumulative distribution function (CDF) of the measure given the element is measurable. In other words, the conditional CDF, evaluated at a fixed real number `x`, is a measurable function of `a : α`.
More concisely: For any measure $\rho$ on the product space of a measurable space $\alpha$ and the real numbers, the function mapping each $a \in \alpha$ to the value at $x$ of the conditional cumulative distribution function of $\rho$ given $a$ is measurable.
|
MeasureTheory.Measure.IicSnd_apply
theorem MeasureTheory.Measure.IicSnd_apply :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ) {s : Set α},
MeasurableSet s → ↑↑(ρ.IicSnd r) s = ↑↑ρ (s ×ˢ Set.Iic r)
The theorem `MeasureTheory.Measure.IicSnd_apply` states that for any measurable space `α`, any measure `ρ` on the product space `α × ℝ`, any real number `r`, and any set `s` in `α` that is measurable, the measure of `s` under `IicSnd ρ r` is equal to the measure of the cartesian product of `s` and the interval from negative infinity up to `r` under `ρ`. Here, `Set.Iic r` represents the interval of all real numbers less than or equal to `r`, and `s ×ˢ Set.Iic r` is the cartesian product of `s` and this interval. This theorem connects the measure of a set in the original measurable space with the measure of a related set in the product space.
More concisely: For any measurable space `α`, measure `ρ` on `α × ℝ`, measurable set `s` in `α`, and real number `r`, the measure of `s` under `IicSnd ρ r` equals the measure of `s ×ˢ Set.Iic r` under `ρ`.
|
ProbabilityTheory.tendsto_condCDF_atTop
theorem ProbabilityTheory.tendsto_condCDF_atTop :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α),
Filter.Tendsto (↑(ProbabilityTheory.condCDF ρ a)) Filter.atTop (nhds 1)
The theorem `ProbabilityTheory.tendsto_condCDF_atTop` states that for any measurable space `α` and any measure `ρ` on the product of `α` and the real numbers `ℝ`, for every element `a` in `α`, the conditional cumulative distribution function (CDF) of the measure given the value on `α` tends to 1 as it approaches positive infinity. In other words, as we go further and further along the real number line, the probability (as measured by the CDF) that a given element `a` of `α` is associated with a real number in that part of the line approaches 1. This is a standard result in probability theory, reflecting the fact that the total probability over all possible outcomes must be 1.
More concisely: For any measurable space α and measure ρ on α x ℝ, the conditional CDF of ρ given the α-coordinate tends to 1 as the real number argument approaches positive infinity for each fixed α-element.
|
ProbabilityTheory.stronglyMeasurable_condCDF
theorem ProbabilityTheory.stronglyMeasurable_condCDF :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (x : ℝ),
MeasureTheory.StronglyMeasurable fun a => ↑(ProbabilityTheory.condCDF ρ a) x
The theorem `ProbabilityTheory.stronglyMeasurable_condCDF` states that for any type `α` with a measurable space structure `mα`, any measure `ρ` on the product space of `α` and the real numbers, and any real number `x`, the conditional cumulative distribution function (condCDF), when applied to a member of `α` and then evaluated at `x`, is a strongly measurable function. Here, a function is considered "strongly measurable" if it can be approximated by a sequence of simple functions.
More concisely: For any measurable space `(α, mα)`, measure `ρ` on `α × ℝ`, and real number `x`, the function `α => ρ.condCDF ∘ fst ∣α => x` is strongly measurable.
|
ProbabilityTheory.tendsto_condCDF_atBot
theorem ProbabilityTheory.tendsto_condCDF_atBot :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α),
Filter.Tendsto (↑(ProbabilityTheory.condCDF ρ a)) Filter.atBot (nhds 0)
The theorem `ProbabilityTheory.tendto_condCDF_atBot` states that for every datum `a` of any type `α`, within a `MeasurableSpace α`, and for a given measure `ρ` on the product space of `α` and `ℝ` (the real numbers), the conditional cumulative distribution function (CDF) of `ρ` with respect to `a` tends to 0 as it approaches negative infinity. In more mathematical terms, this theorem asserts that $\lim_{x\to -\infty} \text{condCDF } \rho a = 0$ for all `a : α`.
More concisely: For every measurable space `(α, Σ)` and measure `ρ` on its product with `ℝ`, the conditional cumulative distribution function of `ρ` with respect to any datum `a : α` tends to 0 as `x` approaches negative infinity. In symbols: $\lim\_{x \to -\infty} \text{condCDF}\_\rho(a)(x) = 0$.
|
ProbabilityTheory.measurable_preCDF
theorem ProbabilityTheory.measurable_preCDF :
∀ {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} {r : ℚ},
Measurable (ProbabilityTheory.preCDF ρ r)
The theorem `ProbabilityTheory.measurable_preCDF` states that for any given type `α`, a measurable space `mα` over this type, a measure `ρ` on the product of this type and the real numbers, and a rational number `r`, the pre-cumulative distribution function (`preCDF`) for the given measure `ρ` and rational `r` is measurable. Here, a function is deemed measurable if the preimage of any measurable set under this function is also measurable. This theorem is a fundamental concept in probability theory, ensuring the measurability of the pre-cumulative distribution function, a prerequisite for any further probabilistic analysis.
More concisely: The pre-cumulative distribution function of a measure over a type and a rational number is measurable.
|
ProbabilityTheory.measurable_measure_condCDF
theorem ProbabilityTheory.measurable_measure_condCDF :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)),
Measurable fun a => (ProbabilityTheory.condCDF ρ a).measure
The theorem `ProbabilityTheory.measurable_measure_condCDF` states that for any type `α` equipped with a measurable space `mα`, and for any measure `ρ` on the product space of `α` and real numbers `ℝ`, the function which maps `a` from `α` to the measure of the conditional cumulative distribution function (CDF) of `ρ` given `a` is measurable. In other words, it asserts that the mapping from points in `α` to measures of the corresponding conditional CDFs respects the structure of the measurable spaces, i.e., the preimage of any measurable set under this mapping is also a measurable set.
More concisely: The function mapping an element `a` in a measurable space `α` to the measure of the conditional cumulative distribution function of a measure `ρ` on the product space of `α` and real numbers `ℝ`, given `a`, is measurable.
|
ProbabilityTheory.set_lintegral_preCDF_fst
theorem ProbabilityTheory.set_lintegral_preCDF_fst :
∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℚ) {s : Set α},
MeasurableSet s →
∀ [inst : MeasureTheory.IsFiniteMeasure ρ],
∫⁻ (x : α) in s, ProbabilityTheory.preCDF ρ r x ∂ρ.fst = ↑↑(ρ.IicSnd ↑r) s
The theorem `ProbabilityTheory.set_lintegral_preCDF_fst` states that for any type `α` equipped with a measurable space structure `mα`, a measure `ρ` on the product space `α × ℝ`, a rational number `r`, and a measurable set `s` in `α` under the assumption that `ρ` admits a finite measure, the \(\mathbb{N}\)-integral over the set `s` of the function `ProbabilityTheory.preCDF ρ r x`, with respect to the marginal measure `MeasureTheory.Measure.fst ρ` on `α`, is equal to the measure of the set `s` under the measure `MeasureTheory.Measure.IicSnd ρ r`, which is the marginal measure on `α` obtained by restricting `ρ` to the set `Set.univ ×ˢ Set.Iic r`. In other words, this theorem is a property about the connection between a measure and its associated pre-cumulative distribution function.
More concisely: For any measurable space `(α, mα)`, measure `ρ` on `α × ℝ`, rational number `r`, and measurable set `s` in `α`, under the assumption that `ρ` admits a finite measure, the \(\mathbb{N}\)-integral of `ProbabilityTheory.preCDF ρ r x` over `s` with respect to `MeasureTheory.Measure.fst ρ` equals the measure of `s` under `MeasureTheory.Measure.IicSnd ρ r`.
|