ProbabilityTheory.exponentialCDFReal_eq
theorem ProbabilityTheory.exponentialCDFReal_eq :
∀ {r : ℝ},
0 < r → ∀ (x : ℝ), ↑(ProbabilityTheory.exponentialCDFReal r) x = if 0 ≤ x then 1 - (-(r * x)).exp else 0
This theorem states that the cumulative distribution function (CDF) of the exponential distribution is equivalent to `1 - exp (-(r * x))`, where `r` is the rate parameter of the exponential distribution and `x` is the random variable. Specifically, if `r` is greater than zero and `x` is non-negative, then the CDF at `x` is `1 - exp (-(r * x))`. If `x` is negative, the CDF is zero.
More concisely: For the exponential distribution with rate parameter `r > 0`, the cumulative distribution function is given by `1 - exp(-rx)` for `x >= 0`, and is zero for `x < 0`.
|
ProbabilityTheory.lintegral_exponentialPDF_eq_one
theorem ProbabilityTheory.lintegral_exponentialPDF_eq_one :
∀ {r : ℝ}, 0 < r → ∫⁻ (x : ℝ), ProbabilityTheory.exponentialPDF r x = 1
This theorem states that for any real number `r` that is greater than zero, the integral of the probability density function (pdf) of the exponential distribution with respect to `x` equals 1. In mathematical terms, it asserts that $\int_{-\infty}^{+\infty} PDF_{exp}(r, x) dx = 1$ for $r > 0$, where $PDF_{exp}(r, x)$ represents the pdf of the exponential distribution parameterized by `r`. This is a fundamental property of pdfs in probability theory, indicating that the total probability across all possible values of a random variable must equal 1.
More concisely: For any positive real number `r`, the integral of the exponential distribution's pdf with respect to `x` over the whole real line equals 1. In mathematical notation, $\int_{-\infty}^{+\infty} PDF_{exp}(r, x) dx = 1$.
|
ProbabilityTheory.measurable_exponentialPDFReal
theorem ProbabilityTheory.measurable_exponentialPDFReal :
∀ (r : ℝ), Measurable (ProbabilityTheory.exponentialPDFReal r)
The theorem states that the probability density function (pdf) of the exponential distribution is measurable for any rate parameter `r`. In mathematical terms, this means that for any given `r`, the function `ProbabilityTheory.exponentialPDFReal r` from the real numbers to the real numbers is a measurable function. Here, a function is considered measurable if, for every set that is measurable in the codomain, its preimage under the function is also measurable in the domain.
More concisely: The exponential PDF function `ProbabilityTheory.exponentialPDFReal` with rate parameter `r` is a measurable function from the real numbers to the real numbers.
|
ProbabilityTheory.exponentialPDFReal_pos
theorem ProbabilityTheory.exponentialPDFReal_pos :
∀ {x r : ℝ}, 0 < r → 0 < x → 0 < ProbabilityTheory.exponentialPDFReal r x
The theorem `ProbabilityTheory.exponentialPDFReal_pos` states that the probability density function (pdf) of an exponential distribution is positive for all positive real numbers. Specifically, for any two positive real numbers `x` and `r`, where `r` is the rate of the exponential distribution and `x` is the value at which the pdf is evaluated, the pdf given by `ProbabilityTheory.exponentialPDFReal r x` is greater than zero. This aligns with the expectation that a pdf should always be non-negative and only be zero where the probability of a random variable taking a certain value is zero.
More concisely: The exponential distribution's probability density function `ProbabilityTheory.exponentialPDFReal r x` is positive for all positive real numbers `x` and rate `r`.
|
ProbabilityTheory.exponentialPDFReal_nonneg
theorem ProbabilityTheory.exponentialPDFReal_nonneg :
∀ {r : ℝ}, 0 < r → ∀ (x : ℝ), 0 ≤ ProbabilityTheory.exponentialPDFReal r x
The theorem `ProbabilityTheory.exponentialPDFReal_nonneg` asserts that the probability density function (pdf) of the exponential distribution, given any positive rate parameter `r`, is always nonnegative for any real-valued `x`. In other words, for any rate `r` greater than 0, the function `ProbabilityTheory.exponentialPDFReal r x` returns a value that is equal to or greater than zero, regardless of the value of `x`. This is an important property of probability density functions as they represent a distribution of probabilities, and hence must not return negative values.
More concisely: For any positive rate parameter `r` in real numbers, the exponential probability density function `ProbabilityTheory.exponentialPDFReal r x` is nonnegative for all real-valued `x`.
|
ProbabilityTheory.exp_neg_integrableOn_Ioc
theorem ProbabilityTheory.exp_neg_integrableOn_Ioc :
∀ {b x : ℝ}, 0 < b → MeasureTheory.IntegrableOn (fun x => (-(b * x)).exp) (Set.Ioc 0 x) MeasureTheory.volume := by
sorry
The theorem "ProbabilityTheory.exp_neg_integrableOn_Ioc" states that for any positive real number 'b' and any real number 'x', the negative exponential function $e^{-(bx)}$ is integrable on the interval (0, x] with respect to the Lebesgue measure. In other words, the function is almost everywhere strongly measurable on this interval, and the integral of the absolute value of this function over the interval is finite.
More concisely: For any positive real number b, the negative exponential function $e^{-(bx)}$ is Lebesgue integrable on the interval (0, x].
|
ProbabilityTheory.lintegral_exponentialPDF_of_nonpos
theorem ProbabilityTheory.lintegral_exponentialPDF_of_nonpos :
∀ {x r : ℝ}, x ≤ 0 → ∫⁻ (y : ℝ) in Set.Iio x, ProbabilityTheory.exponentialPDF r y = 0
This theorem states that for any real numbers 'x' and 'r', if 'x' is less than or equal to zero, then the Lebesgue integral of the probability density function of the exponential distribution over the left-infinite right-open interval ending at 'x' is equal to zero. In mathematical terms, the area under the curve of the exponential distribution's density function, from negative infinity to any nonpositive number, is zero.
More concisely: For any real number x ≤ 0, the Lebesgue integral of the exponential distribution's probability density function over the left-infinite right-open interval (−∞, x) equals 0.
|