ProbabilityTheory.measure_cdf
theorem ProbabilityTheory.measure_cdf :
∀ (μ : MeasureTheory.Measure ℝ) [inst : MeasureTheory.IsProbabilityMeasure μ],
(ProbabilityTheory.cdf μ).measure = μ
This theorem states that for every probability measure `μ` on the real numbers, the measure associated with the cumulative distribution function (CDF) of `μ` is the same as `μ` itself. In more detail, the `ProbabilityTheory.cdf μ` constructs the cumulative distribution function for the probability measure `μ`, and `(ProbabilityTheory.cdf μ).measure` retrieves the measure associated with that cumulative distribution function. According to this theorem, this retrieved measure is identical to the original measure `μ`. This property underlines the consistency between the concept of a probability measure and its cumulative distribution function in the measure theory.
More concisely: For every probability measure `μ` on the real numbers, `ProbabilityTheory.cdf μ`.measure equals `μ`.
|
ProbabilityTheory.monotone_cdf
theorem ProbabilityTheory.monotone_cdf : ∀ (μ : MeasureTheory.Measure ℝ), Monotone ↑(ProbabilityTheory.cdf μ) := by
sorry
The theorem `ProbabilityTheory.monotone_cdf` asserts that, for any measure `μ` on the real numbers, the cumulative distribution function (CDF), as defined by `ProbabilityTheory.cdf μ`, is a monotone function. In other words, for any two real numbers `a` and `b`, if `a` is less than or equal to `b`, then the value of the CDF at `a` is also less than or equal to the value of the CDF at `b`. This property is a fundamental characteristic of cumulative distribution functions in probability theory.
More concisely: For any measure μ on the real numbers, the cumulative distribution function (CDF) defined by `ProbabilityTheory.cdf μ` is a monotone function, i.e., for all real numbers `a ≤ b`, `ProbabilityTheory.cdf μ a ≤ ProbabilityTheory.cdf μ b`.
|
ProbabilityTheory.cdf_le_one
theorem ProbabilityTheory.cdf_le_one : ∀ (μ : MeasureTheory.Measure ℝ) (x : ℝ), ↑(ProbabilityTheory.cdf μ) x ≤ 1 := by
sorry
This theorem states that the cumulative distribution function (CDF), as defined in the context of probability theory for a given probability measure `μ` and real number `x`, is always less than or equal to 1. In other words, it formally guarantees that the probability of events occurring up to a certain point, as represented by the CDF, does not exceed the total probability of 1. This is a fundamental property of any probability measure, reflecting the intuitive concept that the total probability of all possible outcomes of a random experiment must be 1.
More concisely: For any probability measure `μ` and real number `x`, the cumulative distribution function `F` satisfying `μ` satisfies `F x ≤ 1`.
|
MeasureTheory.Measure.eq_of_cdf
theorem MeasureTheory.Measure.eq_of_cdf :
∀ (μ ν : MeasureTheory.Measure ℝ) [inst : MeasureTheory.IsProbabilityMeasure μ]
[inst : MeasureTheory.IsProbabilityMeasure ν], ProbabilityTheory.cdf μ = ProbabilityTheory.cdf ν → μ = ν
This theorem states that if two real-valued probability distributions have the same cumulative distribution function (CDF), then they are equal. In other words, for any two probability measures `μ` and `ν`, if their CDFs as defined by `ProbabilityTheory.cdf μ` and `ProbabilityTheory.cdf ν` are identical, then `μ` and `ν` must be the same measure. The theorem applies specifically to probability measures, which are measures with total measure one.
More concisely: If two real-valued probability measures have identical cumulative distribution functions, they are equal.
|
ProbabilityTheory.tendsto_cdf_atBot
theorem ProbabilityTheory.tendsto_cdf_atBot :
∀ (μ : MeasureTheory.Measure ℝ), Filter.Tendsto (↑(ProbabilityTheory.cdf μ)) Filter.atBot (nhds 0)
This theorem states that the cumulative distribution function (CDF) of any real measure tends to 0 as its argument tends to negative infinity. In other words, for any probability measure `μ`, as we consider increasingly negative values, the CDF of `μ` approaches 0. This is a common property of CDFs in probability theory, reflecting that the probability of the random variable being less than any given value approaches 0 as that value goes to negative infinity.
More concisely: For any real measure `μ`, the limit as `x` approaches negative infinity of its cumulative distribution function is 0.
|
ProbabilityTheory.cdf_nonneg
theorem ProbabilityTheory.cdf_nonneg : ∀ (μ : MeasureTheory.Measure ℝ) (x : ℝ), 0 ≤ ↑(ProbabilityTheory.cdf μ) x := by
sorry
The theorem `ProbabilityTheory.cdf_nonneg` states that the cumulative distribution function (cdf), as defined in the context of real measure theory, is always non-negative. Specifically, for any given measure `μ` over the real numbers and any real number `x`, the value of the cdf at `x` (denoted as `(ProbabilityTheory.cdf μ) x`) is guaranteed to be greater than or equal to zero.
More concisely: For any real measure μ, the cumulative distribution function (cdf) satisfies (ProbabilityTheory.cdf μ) (x) ≥ 0 for all real numbers x.
|
ProbabilityTheory.tendsto_cdf_atTop
theorem ProbabilityTheory.tendsto_cdf_atTop :
∀ (μ : MeasureTheory.Measure ℝ), Filter.Tendsto (↑(ProbabilityTheory.cdf μ)) Filter.atTop (nhds 1)
This theorem states that for any real measure `μ`, the cumulative distribution function (CDF) of `μ` tends to 1 as the input goes to positive infinity. In other words, as you consider larger and larger values in the domain of the CDF of `μ`, the function's output gets closer and closer to 1. This aligns with the standard understanding in probability theory that the CDF of a probability measure will always approach 1 as the input grows without bound.
More concisely: For any real measure `μ`, the limit as `x` approaches infinity of the cumulative distribution function (CDF) of `μ` is 1.
|