lintegral_Iic_eq_lintegral_Iio_add_Icc
theorem lintegral_Iic_eq_lintegral_Iio_add_Icc :
∀ {y z : ℝ} (f : ℝ → ENNReal),
z ≤ y → ∫⁻ (x : ℝ) in Set.Iic y, f x = (∫⁻ (x : ℝ) in Set.Iio z, f x) + ∫⁻ (x : ℝ) in Set.Icc z y, f x
The theorem `lintegral_Iic_eq_lintegral_Iio_add_Icc` states that for any real numbers `y` and `z` and a function `f` from the real numbers to the extended non-negative real numbers (denoted as `ENNReal`, which represents the set [0, ∞]), if `z` is less than or equal to `y`, then the Lebesgue integral of `f` over the interval from negative infinity to `y` (denoted by `Set.Iic y`) is equal to the sum of the Lebesgue integral of `f` over the interval from negative infinity to `z` (denoted by `Set.Iio z`) and the Lebesgue integral of `f` over the closed interval from `z` to `y` (denoted by `Set.Icc z y`). In other words, the Lebesgue integral over the entire interval can be split into two parts at the point `z`.
More concisely: For any real-valued function `f` and real numbers `y` and `z` with `z ≤ y`, the Lebesgue integral of `f` over the interval `[−∞, y]` equals the sum of the integrals over `[−∞, z]` and `[z, y]`.
|
ProbabilityTheory.gammaPDFReal_nonneg
theorem ProbabilityTheory.gammaPDFReal_nonneg :
∀ {a r : ℝ}, 0 < a → 0 < r → ∀ (x : ℝ), 0 ≤ ProbabilityTheory.gammaPDFReal a r x
This theorem asserts that the Probability Density Function (PDF) of the Gamma distribution, parameterized by a scale `a` and a rate `r`, is always nonnegative. In other words, for any real numbers `a` and `r` that are greater than zero and for any real number `x`, the value of the Gamma distribution's PDF at `x`, computed by the function `ProbabilityTheory.gammaPDFReal a r x`, is always greater than or equal to zero.
More concisely: The Gamma PDF function with parameters `a > 0` and `r > 0`, defined as `ProbabilityTheory.gammaPDFReal a r x`, is non-negative for all real numbers `x`.
|
ProbabilityTheory.gammaPDFReal_pos
theorem ProbabilityTheory.gammaPDFReal_pos :
∀ {x a r : ℝ}, 0 < a → 0 < r → 0 < x → 0 < ProbabilityTheory.gammaPDFReal a r x
The theorem states that the probability density function (pdf) of the gamma distribution, as defined by `ProbabilityTheory.gammaPDFReal`, is always positive for all positive real values of its parameters and random variable. More specifically, for any positive values of the shape parameter `a`, the rate parameter `r`, and the random variable `x`, the pdf of the gamma distribution, which is given by `r^a / Gamma(a) * x^(a - 1) * e^(-r * x)`, is always greater than zero. This is in line with the definition of a pdf, which is non-negative and integrates to one over its entire domain.
More concisely: The gamma PDF function `r^a / Gamma(a) * x^(a - 1) * e^(-r * x)` defined in Lean 4 is positive for all positive real values of shape parameter `a`, rate parameter `r`, and random variable `x`.
|
ProbabilityTheory.lintegral_gammaPDF_eq_one
theorem ProbabilityTheory.lintegral_gammaPDF_eq_one :
∀ {a r : ℝ}, 0 < a → 0 < r → ∫⁻ (x : ℝ), ProbabilityTheory.gammaPDF a r x = 1
This theorem states that for any two real numbers 'a' and 'r', if both 'a' and 'r' are greater than zero, then the integral (over all real numbers) of the probability density function (pdf) of the gamma distribution with parameters 'a' and 'r' equals one. This is a statement of a property which every probability density function should have, namely that the total probability under the curve of the pdf is equal to one.
More concisely: For any positive real numbers 'a' and 'r', the integral of the gamma distribution's pdf with parameters 'a' and 'r' over all real numbers equals 1.
|
ProbabilityTheory.isProbabilityMeasureGamma
theorem ProbabilityTheory.isProbabilityMeasureGamma :
∀ {a r : ℝ}, 0 < a → 0 < r → MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.gammaMeasure a r)
This theorem states that for all real numbers `a` and `r`, if both `a` and `r` are greater than zero, then the measure defined by the gamma distribution (i.e., `ProbabilityTheory.gammaMeasure a r`) is a probability measure. In other words, the gamma distribution with parameters `a` and `r`, when both are positive, qualifies as a probability measure under the rules of measure theory.
More concisely: For all positive real numbers `a` and `r`, the gamma distribution `ProbabilityTheory.gammaMeasure a r` is a probability measure.
|
ProbabilityTheory.measurable_gammaPDFReal
theorem ProbabilityTheory.measurable_gammaPDFReal : ∀ (a r : ℝ), Measurable (ProbabilityTheory.gammaPDFReal a r) := by
sorry
This theorem states that the probability density function (pdf) of the gamma distribution is measurable. In other words, for any two real numbers 'a' and 'r', which are the scale and rate parameters of the gamma distribution, the function that describes the gamma pdf is such that the preimage of every measurable set is also measurable.
More concisely: The gamma distribution's probability density function is a measurable function.
|
ProbabilityTheory.stronglyMeasurable_gammaPDFReal
theorem ProbabilityTheory.stronglyMeasurable_gammaPDFReal :
∀ (a r : ℝ), MeasureTheory.StronglyMeasurable (ProbabilityTheory.gammaPDFReal a r)
This theorem states that the probability density function (pdf) of the gamma distribution is "strongly measurable". In the context of this theorem, a function is deemed strongly measurable if it can be represented as the limit of a sequence of simple functions. Specifically, for any given scale and rate parameters `(a, r)` of the gamma distribution, the resulting pdf, represented by `ProbabilityTheory.gammaPDFReal a r`, is strongly measurable. This means that we can find a sequence of simple functions which converge to the gamma pdf under all real numbers in the limit.
More concisely: The gamma probability density function is strongly measurable, meaning it can be represented as the limit of a sequence of simple functions.
|
ProbabilityTheory.lintegral_gammaPDF_of_nonpos
theorem ProbabilityTheory.lintegral_gammaPDF_of_nonpos :
∀ {x a r : ℝ}, x ≤ 0 → ∫⁻ (y : ℝ) in Set.Iio x, ProbabilityTheory.gammaPDF a r y = 0
This theorem is stating that for any real numbers `x`, `a`, and `r`, if `x` is nonpositive (i.e., `x` is less than or equal to 0), then the Lebesgue integral of the probability density function (pdf) of the gamma distribution over all real numbers less than `x` equals 0. In other words, it's saying that the total probability of the gamma distribution on the interval from negative infinity to any nonpositive number (inclusive) is 0.
More concisely: For any real numbers `x`, `a`, and `r`, if `x` is nonpositive, then the Lebesgue integral of the gamma distribution pdf over the interval `(-\infty, x]` equals 0.
|